z3

Which version of Z3 does VeriEQL use?

I am trying to set up VeriEQL on my computer (Ubunty, Python 3.10) from this repository: https://github.com/VeriEQL/VeriEQL

However, when I run python __main__.py I get error message:

 File "/mnt/compression/VeriEQL/constants.py", line 33, in <lambda>
    And = lambda *args: Z3_And(*args, ctx=Z3_CONTEXT)
TypeError: And() got an unexpected keyword argument 'ctx'

I tried installing the following versions of z3 via pip install:

z3-solver-4.5.1.0
z3-solver-4.11.2.0
z3-solver-4.8.12.0
z3-solver-4.15.0.0

but the error persists.

And I do not know to to print z3 version from __main__.py to make sure that the installed version is indeed loaded.

Solution

  • Ok, that was a stupid question. It works with all versions (in particular, with 4.15.0), but needs a patch, which is included in the repository.

    On my machine the test passed after I created a new Python environment, installed the packages from requirements.txt and the required patch by

    cp ./z3py_libs/*.py sql_env/lib64/python3.10/site-packages/z3/4.15.0
cp ./z3py_libs/*.py sql_env/lib/python3.10/site-packages/z3/