[SMT-LIB] Some problem with ForAll quantifier in my SMT formula

[Jun Koi]

Hi,

I am sorry if this is not a right place to ask questions on SMT solver, but
I am really struggling, and have nobody to ask. Please ignore if this
bothers you, but any help will be highly appreciated!

My problem: I am trying to use SMT to find value of "a" value so that "a *
b == b" with all value of "b". The expected result is "a == 1". One minor
issue is that in the input formula, besides "a", "b", I have some auxiliary
variables (like tmp, tmp1, etc ..., which I must deal with). I use Z3
solver, with python binding. 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 this code?


*(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 so much!

Jun