z3 - このコードが Unsat (ForAll と Implies を使用した式) を返すのはなぜですか?

Question

与えられた 2 つの方程式c == a + 4とt == c + b、if a == -4、 then t == b。私は反対のことをt == bしようとしていますa.

ForAllとImpliesでこれを行うコードを以下に示します。

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([c, t, b], Implies(g, t == b)))

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

ただし、上記のコードを実行するとUnsatが返されます。これは -4 (または 0xfffffffc) を返すと予想されるので、かなり混乱しています。

私が間違っている場所はありますか？

ありがとう！