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.
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.)