位向量策略导致 Z3Py 中的退出代码 139 [英] Bit Vector tactic leads to exit code 139 in Z3Py
本文介绍了位向量策略导致 Z3Py 中的退出代码 139的处理方法,对大家解决问题具有一定的参考价值,需要的朋友们下面随着小编来一起学习吧!
问题描述
这是一个简单的位向量问题:
This is a simple bit vector problem:
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
战术.
Python crashes with error code 139. Please note that, this is not my real problem, so I must use bit vector tactic in my project, though it doesn't have any problem with smt
tactic or even qfbv
tactic.
推荐答案
这似乎是 4.4.0 中的错误.使用 4.4.0 和 Ubuntu 16.04 LTS 和 Python 2.7,您可以重现该问题.但是在较新版本的 Z3 中,它已得到修复.我尝试了 4.4.2,它返回 sat
.
It seems to be a bug in 4.4.0. With 4.4.0 and Ubuntu 16.04 LTS and Python 2.7 you can reproduce the issue. However in newer versions of Z3, it has been fixed. I tried 4.4.2 and it returns sat
.
https://github.com/Z3Prover/z3/issues/685
这篇关于位向量策略导致 Z3Py 中的退出代码 139的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持IT屋!
查看全文