pysmt z3 solver crashing?

Question

I am having trouble with the pysmt solvers. I am getting the following error message:

AttributeError: 'module' object has no attribute 'Z3_mk_and'

whenever I try to both: (1) Instantiate a solver via Solver() and (2) Run pysmt-install --check

Here is the full stack trace, incited from method 1:

Traceback (most recent call last):
  File "ex.py", line 15, in <module>
    solver = s.Solver()
  File "/Users/harper/anaconda2/lib/python2.7/site-packages/pysmt/shortcuts.py", line 910, in Solver
    return get_env().factory.Solver(name=name,
  File "/Users/harper/anaconda2/lib/python2.7/site-packages/pysmt/environment.py", line 158, in factory
    self._factory = pysmt.factory.Factory(self)
  File "/Users/harper/anaconda2/lib/python2.7/site-packages/pysmt/factory.py", line 86, in __init__
    self._get_available_solvers()
  File "/Users/harper/anaconda2/lib/python2.7/site-packages/pysmt/factory.py", line 222, in _get_available_solvers
    from pysmt.solvers.z3 import Z3Solver
  File "/Users/harper/anaconda2/lib/python2.7/site-packages/pysmt/solvers/z3.py", line 295, in <module>
    class Z3Converter(Converter, DagWalker):
  File "/Users/harper/anaconda2/lib/python2.7/site-packages/pysmt/solvers/z3.py", line 859, in Z3Converter
    walk_and     = make_walk_nary(z3.Z3_mk_and)
AttributeError: 'module' object has no attribute 'Z3_mk_and'

I've tried so much to fix this, like uninstalling and reinstalling z3 (supposedly successfully), and pip installing z3-solver (which fails), and I can't figure out what's wrong.

Answer 1

This has nothing really to do with z3; but rather directly with pysmt itself. Most likely pysmt isn't keeping up-to-date with changes in z3. You should file a ticket directly at their site: https://github.com/pysmt/pysmt/issues

Answer 2

Please note that the proper way to install a solver for pysmt is through pysmt-install. This guarantees that the version of the solver has been tested.