在某些条件下证明 2 个公式等价？

Question

如果a == 0，两个公式a1 == a + b 和a1 == b 是等价的。我想用 Z3 python 找到这个必需的条件（a == 0）。我写了下面的代码：

from z3 import *

def equivalence(F, G):
    s = Solver()
    s.add(Not(F == G))
    r = s.check()
    if r == unsat:
        print 'Equ'
        print s.model()
    else:
        print 'Not Equ'

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

g = True
tmp = BitVec('tmp', 32)
g = And(g, tmp == a)
tmp1 = BitVec('tmp1', 32)
g = And(g, tmp1 == b)
tmp2 = BitVec('tmp2', 32)
g = And(g, tmp2 == (tmp1 + tmp))
a1 = BitVec('a1', 32) 
g = And(g, a1 == tmp2)

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

equivalence(Exists([a], g), f)

但是，上面的代码总是返回"Not Equ" 作为输出。那么显然我也无法将模型（a === 0）作为"f" 和"g" 相等的条件。

关于代码哪里出错以及如何修复它的任何想法？非常感谢！

Answer 1

帖子中的代码与所提出的问题不对应。 在 smt-lib 邮件列表中提出并回答了类似的问题。