位向量策略导致 Z3Py 中的退出代码 139答案

【问题标题】：Bit Vector tactic leads to exit code 139 in Z3Py位向量策略导致 Z3Py 中的退出代码 139
【发布时间】：2016-07-16 08:56:20
【问题描述】：

这是一个简单的位向量问题：

import z3

s = z3.Tactic('bv').solver()
m = z3.Function('m', z3.BitVecSort(32), z3.BitVecSort(32))
a, b = z3.BitVecs('a b', 32)

axioms = [
    a == m(12432),
    z3.Not(a == b)
]

s.add(axioms)
print(s.check())

Python 崩溃并显示错误代码 139。请注意，这不是我真正的问题，所以我必须在我的项目中使用位向量策略，尽管 @987654322 没有任何问题@战术甚至qfbv战术。

【问题讨论】：

我无法重现您的错误。我在 Ubuntu 14.04 上尝试了 Z3 4.4.1 和 Z3 master，在 OS X 10.9.5 上也尝试了 Z3 master。我还尝试了 Python 2.7 和 3.4。在所有这些情况下，您的脚本都会为我返回 sat。

标签： python z3 smt z3py bitvector

【解决方案1】：

这似乎是 4.4.0 中的一个错误。使用 4.4.0 和 Ubuntu 16.04 LTS 和 Python 2.7，您可以重现该问题。但是在较新版本的 Z3 中，它已被修复。我尝试了 4.4.2，它返回 sat。

https://github.com/Z3Prover/z3/issues/685

【讨论】：