Can the verifier find a model even when the method is correct?

Oct 8, 2016 at 10:44 PM
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

Image

the BVD gives a model

Image

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.
Oct 23, 2016 at 6:42 PM
Edited Oct 23, 2016 at 6:43 PM
Good answers to this question can be found at Stack Exchange http://stackoverflow.com/questions/39937508/z3-model-for-correct-dafny-method .

My misundertanding was in thinking that Z3 only produces models when the answer to the query is "sat". In fact Z3 also produces models when the answer to the query is "unknown", which is what is happening in the case above. In fact Boogie's queries to Z3 are only ever answered by "unsat", "unknown", or "time out", so there is no way for Dafny to distinguish between definite counter-examples and possible counter-examples.
Marked as answer by rustanleino on 10/24/2016 at 12:05 PM