z3py MacOSX上：不能得到一個模型

我看到有z3py一個奇怪的問題在Mac上，想知道是否有人已經看到了這一點之前：z3py MacOSX上：不能得到一個模型

$ 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。

來源

2013-05-09 Anton Belov

我在Mac OSX 10.8.3上看不到任何Z3 4.1和Python 2.7.2的問題。我想知道是否某種終端問題會因任何原因而吃掉角色。如果將輸出重定向到文件，你會看到什麼？（即嘗試「python bug.py> out」。文件「out」的內容看起來是否正常？）

來源

2013-05-09 07:28:32

與控制檯上的內容相同。我有一種感覺，它可能與我的python安裝有關。 – 2013-05-09 09:55:19

該問題對我的設置非常具體，但也許有人會遇到它：根本原因在於動態加載器拾取了錯誤版本的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-10 15:55:20

z3py MacOSX上：不能得到一個模型

回答

相關問題