1

我在 Mac 上看到 z3py 的一个奇怪问题，想知道是否有人以前见过这个：

$ cat bug.py
from z3 import *       
x = Int('x')
s = Solver()
s.add(x > 5)
print(s.check())
print(s.model())
$ python bug.py
sat
[x = ]

模型中缺少 x 的值。我尝试了主分支和不稳定分支，结果相同。但是，如果在类似的 .smt2 文件上运行，z3 本身确实会给出正确的模型。我的配置是 Mac OSX 10.6.8，Python 2.7.4。

4

2 回答 2

3

这个问题对我的设置来说是非常具体的，但也许有人也会遇到它：根本原因是动态加载器选择了错误版本的 libgomp —— 即用于编译和运行的版本不匹配.

下面是这个问题更严重的表现：

$ python
Python 2.7.4 (default, May  9 2013, 18:51:46)
[GCC 4.2.1 (Apple Inc. build 5664)] on darwin
Type "help", "copyright", "credits" or "license" for more information.
>>> from z3 import *
>>> IntVal(1)

>>>

数值不打印，即正确的输出是

>>> IntVal(1)
1
>>>

将 DYLD_LIBRARY_PATH 设置为指向库的正确版本可解决此问题。

于 2013-05-10T15:55:20.917 回答
2

在我的 Mac OSX 10.8.3 上，我没有看到 Z3 4.1 和 Python 2.7.2 有任何问题。我想知道这是否是某种终端问题以某种原因吞噬了角色。如果将输出重定向到文件，您会看到什么？（即，尝试“python bug.py > out”。文件“out”的内容是否正常？）

于 2013-05-09T07:28:32.677 回答