这是一个简单的位向量问题:
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。请注意,这不是我真正的问题,所以我必须在我的项目中使用位向量策略,尽管它对smt
策略甚至qfbv
策略没有任何问题。你知道吗
这似乎是4.4.0中的一个bug。使用4.4.0和ubuntu16.04 LTS以及python2.7,您可以重现这个问题。但是在Z3的更新版本中,它已经被修复了。我尝试了4.4.2,它返回
sat
。你知道吗https://github.com/Z3Prover/z3/issues/685
相关问题 更多 >
编程相关推荐