Z3 is actually returning unknown
. The method check
returns: sat
, unsat
or unknown
.
Here is a custom tactic that shows that the formula is indeed unsat.
#!/usr/bin/python
from z3 import *
a, b, c, t = BitVecs('a b c t', 32)
g = True
g = And(g, c == (a + 4))
g = And(g, t == (c + b))
s = Goal()
s.add(ForAll([t, a, c], Implies(t == a, g)))
T = Then("simplify", "der", "distribute-forall")
# print the simplified formula. Note that it is unsat
print T(s)
# Create a solver using the tactic above and qe
s = Then("simplify", "der", "distribute-forall", "qe", "smt").solver()
s.add(ForAll([t, a, c], Implies(t == a, g)))
print s.check()
Update The formula is of the form
forall t, a, c: t == a ==> c == (a + 4) and t == (c + b)
.
This formula is logically equivalent to:
forall a, c: c == (a + 4) and a == (c + b)
.
which is logically equivalent to
(forall a, c: c == (a + 4)) and (forall a, c: a == (c + b))
.
Both subformulas are logically equivalent to false. This is why the formula is unsatisfiable.
The comment you wrote suggests that you believe you created the slightly different formula
forall t, a, c: t == a ==> c == (a + 4) ==> t == (c + b)
.
This formula is sat
. To create this formula we have to replace
g = True
g = And(g, c == (a + 4))
g = And(g, t == (c + b))
with
g = Implies(c == (a + 4), t == (c + b))
The updated example is available here.