why this code returns Unsat?

Question

Given c == a + 4 and t == c + b, if b == -4, then t == a. I am trying to do the opposite, meaning given the above 2 equations and t == a, I try to find value of b.

This is pretty similar to the related question, but this time I only switch a and b, and I am really confused that the code returns different result.

Following the code posted at above link, I have below code (similar, only a and b swiched):

#!/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 = Solver()
s.add(ForAll([t, a, c], Implies(t == a, g)))
if s.check() == sat:
    print s.model()[b]
else:
    print 'Unsat'

However, on Ubuntu, running the above code returns unexpected result Unsat, but not value -4 (or 0xfffffffc)

Any idea why this is wrong?

Thanks so much.

Answer 1

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.