Я вижу странную проблему с z3py на Mac, мне было интересно, видел ли кто-нибудь это раньше:
$ 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 отсутствует в модели. Я пробовал как основную, так и нестабильную ветки с тем же результатом. Однако сам z3 дает правильную модель, если запускать аналогичный файл .smt2. Моя конфигурация — Mac OSX 10.6.8, Python 2.7.4.
Проблема очень специфична для моей установки, но, возможно, кто-то тоже с ней столкнется: основная причина в том, что динамический загрузчик подхватил неправильную версию 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 для указания на правильную версию библиотеки устраняет проблему.
Я не вижу проблем с Z3 4.1 и Python 2.7.2 на моем Mac OSX 10.8.3. Интересно, это какая-то терминальная проблема, которая по какой-то причине съедает персонажей. Что вы увидите, если перенаправите вывод в файл? (т. е. попробуйте «python bug.py > out». Содержимое файла «out» выглядит нормально?)
