What do you think about this:
a, b, a1 = BitVecs('a b a1', 32)
f = True
f = And(f, a1 == a * b)
g= True
g = And(f, a1 == b)
s = Solver()
s.add(ForAll(b, ForAll(a1,f == g)))
if s.check() == sat:
print 'a =', s.model()[a]
else:
print 'Unsat
output:
a = 1
Other form:
a, b, a1 = BitVecs('a b a1', 32)
f = True
f = And(f, a1 == a * b)
g= True
g = And(g, a1 == b)
s = Solver()
s.add(ForAll(b, ForAll(a1,f == g)))
if s.check() == sat:
print 'a =', s.model()[a]
else:
print 'Unsat'
output:
a = 1