验证失败：z3 python 上的 !m_var2expr.empty()

Question

这是抛出异常的代码。

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

这是代码的输出。

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

异常的原因是什么？

我的环境如下

macOS 10.13.2
Z3 版本 4.8.0 - 64 位（由 brew 安装）
Python 3.6.7（由 pyenv 安装）
pip z3 0.2.0
pip z3-求解器 4.8.0.0

Answer 1

对我来说运行得很好：

$ 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)

我也在 Mac，我有：

$ z3 --version
Z3 version 4.8.3 - 64 bit

我怀疑你的安装有问题。从头开始重新安装可能会解决问题。

验证失败：z3 python 上的 !m_var2expr.empty()

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

python

z3

z3py