MacOSX 上的 z3py：无法获取模型答案

【问题标题】：z3py on MacOSX: cannot get a modelMacOSX 上的 z3py：无法获取模型
【发布时间】：2013-05-09 01:05:41
【问题描述】：

我在 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。

【问题讨论】：

标签： z3 z3py

【解决方案1】：

这个问题对我的设置来说是非常具体的，但也许有人也会遇到它：根本原因是动态加载程序选择了错误版本的 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 设置为指向库的正确版本可解决此问题。

【讨论】：

【解决方案2】：

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

【讨论】：

与控制台上的内容相同。我觉得这可能与我的 python 安装有关。