Z3Python: ForAll causes my code hangup, or returns Unsat, why?

Question

I am still struggling with the problem of findiong a value so that a * b == b with all value of b. The expected result is a == 1. I have two solutions below.

(A) I implemented this with ForAll quantifier in below code (correct me if there is a solution without using any quantifier). The idea is to prove f and g are equivalent.

from z3 import *

a, b, a1, tmp1 = BitVecs('a b a1 tmp1', 32)

f = True
f = And(f, tmp1 == b)
f = And(f, a1 == a * tmp1)

g= True
g = And(g, a1 == b)

s = Solver()
s.add(ForAll([b, tmp1, a1], f == g))

if s.check() == sat:
    print 'a =', s.model()[a]
else:
    print 'Unsat'

However, this simple code runs forever without giving back result. I think that is because of the ForAll. Any idea on how to fix the problem?

(B) I tried again with another version. This time I dont prove two formulas to be equivalent, but put them all into one formula f. Logically, I think this is true, but please correct me if I am wrong here:

from z3 import *

a, b, a1, tmp = BitVecs('a b a1 tmp', 32)

f = True
f = And(f, tmp == b)
f = And(f, a1 == a * tmp)
f = And(f, a1 == b)

s = Solver()
s.add(ForAll([b, a1], f))

if s.check() == sat:
    print 'a =', s.model()[a]
else:
    print 'Unsat'

This time the code does not hang, but immediately returns 'Unsat'. Any idea on how to fix this?

Thanks a lot.

Answer 1

The direct formulation of your problem provides the answer you were expecting: http://rise4fun.com/Z3Py/N07sW

The versions you propose use auxiliary variables, a1, tmp, tmp1 and you use universal quantification over these variables. This does not correspond to the formula you intended.