Failed to verify: !m_var2expr.empty() on z3 python

Question

This is the code which throws the exception.

import z3
solver = z3.Solver()
v1, v2, v3, v4 = [z3.Bool("v{}".format(i)) for i in range(1,5)]
z3_prop1 = z3.And(z3.Or(z3.Or(z3.Not(z3.And(v1,v2)), z3.And(False, v3)),
       z3.And(z3.And(False, v2), z3.Or(z3.Not(False), v1))),
    z3.And(z3.And(z3.And(v3, v2), z3.And(v4, v1)),
        z3.Or(z3.Or(v2, v3), z3.And(v4, False))))
print(z3_prop1)
solver.reset()
solver.add(z3_prop1)
print("CHECK", solver.check()) # z3_prop1 is OK
z3_prop2 = z3.Not(z3_prop1)
solver.reset()
print(z3_prop2)
solver.add(z3_prop2)
print("CHECK", solver.check()) # z3_prop2 throws Error

This is the output of the code.

And(Or(Or(Not(And(v1, v2)), And(False, v3)),
   And(And(False, v2), Or(Not(False), v1))),
And(And(And(v3, v2), And(v4, v1)),
    Or(Or(v2, v3), And(v4, False))))
CHECK unsat
Not(And(Or(Or(Not(And(v1, v2)), And(False, v3)),
       And(And(False, v2), Or(Not(False), v1))),
    And(And(And(v3, v2), And(v4, v1)),
        Or(Or(v2, v3), And(v4, False)))))
Failed to verify: !m_var2expr.empty()
libc++abi.dylib: terminating with uncaught foreign exception
[1]    10607 abort      python -m src.z3_solver

What is the reason of the exception?

My environment is following.

• macOS 10.13.2
• Z3 version 4.8.0 - 64 bit (Installed by brew)
• Python 3.6.7 (Installed by pyenv)
• pip z3 0.2.0
• pip z3-solver 4.8.0.0

Answer 1

Runs just fine for me:

$ python a.py
And(Or(Or(Not(And(v1, v2)), And(False, v3)),
       And(And(False, v2), Or(Not(False), v1))),
    And(And(And(v3, v2), And(v4, v1)),
        Or(Or(v2, v3), And(v4, False))))
('CHECK', unsat)
Not(And(Or(Or(Not(And(v1, v2)), And(False, v3)),
           And(And(False, v2), Or(Not(False), v1))),
        And(And(And(v3, v2), And(v4, v1)),
            Or(Or(v2, v3), And(v4, False)))))
('CHECK', sat)

I'm on a Mac as well, and I have:

$ z3 --version
Z3 version 4.8.3 - 64 bit

I suspect your installation is busted somehow. Reinstalling from scratch might solve the issue.