Search code examples
z3z3py

Z3 query with existential quantifier return wrong result

I have constructed the following 

s=Solver()
s.add(ForAll([n],Implies(n>=0,x(n + 1) == If((x(n)==0),0,1))))
s.add(x(0) == 0)
s.add(Not(Exists([n],Implies(n>=1,(x(n)!=0)))))

The above query return unsat which did not seem to be correct?

Similarly 

s=Solver()
s.add(ForAll([n],Implies(n>=0,x(n + 1) == If((x(n)==0),1,1))))
s.add(x(0) == 0)
s.add(Not(Exists([n],Implies(n>=1,(x(n)!=0)))))

The above query return unsat which did not seem to be correct?

Please help me to understand what is wrong in the above queries?

Solution

  • Your existential alone is already unsatisfiable, which might be more apparent if you replace the implication by an if-then-else:

    not exists n :: 1 <= n ? x(n) != 0 : true

    Thus, for any n < 1, you assume that

    not exists n :: true

    That's clearly not true.