Я установил пакет z3-solver из PyPi в моей среде Python3 с помощью Anaconda Prompt (pip install z3-solver) и все.
Пакет появляется в каталоге site-packages / (пакет содержит _init__.py и все необходимые файлы, включая z3.py). Однако когда я попытался запустить этот пример из Jupyter Notebook, он возвращает следующее сообщение: NameError : имя 'Int' не определено.
Я использовал Anaconda только в течение короткого времени, поэтому я не уверен, как работает установка. Это действительно странно, потому что команда 'pip install' в большинстве случаев работает нормально. Я сделал что-то не так или этот пакет требует дополнительной настройки?