Why WP with Z3 proves \false when access to struct field is defined?

Question

I've written simple ACSL contract for two C functions:

struct S
{
    int n;
};

/*@ axiomatic Block {
    predicate isZero(int left) =
        left == 0;

    // Unused, but necessary for verification
    logic int getN(struct S *s) = s->n;
}*/

/*@ requires \valid(s);
    requires isZero(s->n);
    assigns \nothing;
    ensures \false; // Verified by Z3
*/
void g(struct S *s)
{
}

/*@ assigns \nothing;
    ensures \false; // Verified by Z3
*/
void f()
{
    struct S s;
    s.n = 0;
    g(&s);
}

As you can see, specifications establish that f() and g() ensure obviously false statement. The problem is in verification of g(), I've defined f() to show that preconditions of g() can be satisfied. Why Z3 manages to prove both contracts if logic function getN is defined?

I've launched this example in docker container that uses Ubuntu 20.04 to ensure that problem isn't caused by my environment. Frama-C version: 27.1 (Cobalt). Z3 version 4.12.2 - 64 bit.

In a shell:

CMD eval $(opam env --switch=4.14.1) && why3 --version && frama-c --version && z3 --version && frama-c -wp -rte -wp-prover="z3" -wp-timeout 100 /tmp/acsl/acsl.c

produces

Why3 platform, version 1.6.0
27.1 (Cobalt)
Z3 version 4.12.2 - 64 bit
[kernel] Parsing tmp/acsl/acsl.c (with preprocessing)
[rte:annot] annotating function f
[rte:annot] annotating function g
[wp] Running WP plugin...
[wp] 9 goals scheduled
[wp] Proved goals:    9 / 9
  Qed:             7
  Z3 4.12.2:       2

The problem may be in Z3 itself, because Alt-Ergo and CVC4 cannot prove these goals.

I've also reproduced this example in framac/frama-c:dev container from Docker hub. I've used this Dockerfile:

FROM framac/frama-c:dev
RUN wget https://github.com/Z3Prover/z3/releases/download/z3-4.12.2/z3-4.12.2-x64-glibc-2.31.zip
RUN unzip z3-4.12.2-x64-glibc-2.31.zip
RUN sudo cp z3-4.12.2-x64-glibc-2.31/bin/z3 /usr/local/bin/z3
RUN why3 config detect
RUN mkdir /tmp/acsl
CMD why3 --version && frama-c --version && z3 --version && frama-c -wp -rte -wp-prover="z3" -wp-timeout 100 /tmp/acsl/acsl.c