A model of a simple formula 'Exists([y],ForAll([x],Phi))' should be 'y=2' but Z3 it is returning '[]'

Question

Note the following Z3-Py code:

x, y = Ints('x y')

negS0= (x >= 2)
s1 = (y > 1)
s2 = (y <= x)

s = Solver()
phi = Exists([y],ForAll([x], Implies(negS0, And(s1,s2))))
s.add(phi)
print(s.check())
print(s.model())

This prints:

sat
[]

My question is: why is the model empty? I mean, I think y=2 should be a model...

Note that the same result happens with x and y being Real.

Answer 1

z3 will not include any quantified variable (in your case neither y nor x) in its model. Note that you cannot put x in a model anyhow, because the formula is true for all x: That's the meaning of universal quantification. For the outer-most existentials (like your y), z3 can indeed print the model value for that, but it chooses not to do so since it can be confusing: Imagine you had a phi2, which also had an outer-most existential named y: How would you know which y it would be that it prints in the model?

So, z3 keeps things simple and simply prints the top-level declared variables in the model. And since a top-level declaration is equivalent to an outermost existential, you can simply drop it:

from z3 import *

x, y = Ints('x y')

negS0= (x >= 2)
s1 = (y > 1)
s2 = (y <= x)

s = Solver()
phi = ForAll([x], Implies(negS0, And(s1,s2)))
s.add(phi)
print(s.check())
print(s.model())

This prints:

sat
[y = 2]

like you predicted. Note that this y is unambiguous, since it's declared at the top-level. (Of course, you can redefine it to be something else due to the loosely typed nature of Python bindings and still get yourself confused, but that's a different discussion.)