I was under the impression that when Z3 finds a model, it's a model that satisfies the negation of a (the?) verification condition, and that means the negation of the VC is satisfiable, and therefore the VC is false, and so the method is not correct.
However, for the example below
the BVD gives a model
even though the method is correct.
Can someone explain where my misunderstanding is?
BTW I posted the same question to Stack Exchange, so feel free to answer it there too and reap some points.