Search code examples
z3

z3 cannot prove transitive identity

I am trying z3 what can it do. So far so good, but I noticed that z3 fails on very trivial expression:

from z3 import *
a = Int("a")
b = Int("b")
c = Int("c")
prove(((a == b) and (b == c)) == ((a == c) and (c == b)))

$ python p.py
counterexample
[c = 1, b = 0, a = 0]
Solution

  • Python's and is not symbolic-aware. Instead, use z3's And method:

    from z3 import *
a = Int("a")
b = Int("b")
c = Int("c")
prove(And(a == b, b == c) == (And(a == c, c == b)))

    This prints:

    proved