无法验证：!m_var2expr.empty() 在 z3 python 上

Question

这是引发异常的代码。import z3solver = 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 OKz3_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 unsatNot(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.2Z3 版本 4.8.0 - 64 位（由 brew 安装）Python 3.6.7（由 pyenv 安装）点Z3 0.2.0pip z3-solver 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

我怀疑您的安装以某种方式被破坏了。从头开始重新安装可能会解决问题。