AttributeError while synthesizing strategies

[ankitamitra]

I followed the instructions provided all the way up to Learning and Synthesis When I try to run the command to load formulas from leipzig benchmark and run the procedure to synthesize best strategy for every formula as follows: (venv) $ python synthesis/learning.py experiments/configs/leipzig/config_apprentice.json
--benchmark_dir examples/QF_NIA/leipzig/
--max_timeout 10
--num_iters 5
--iters_inc 5
--pop_size 1
--eval_dir eval/synthesis/
--smt_batch_size 100
--full_pass 2
--num_threads 10
--experiment_name leipzig_example

I get the following error:

I have not modified any of the files during setup, and everything works perfectly up until this step. Any ideas on how to get around this? Any help would be greatly appreciated!

[mbalunovic]

Hi, I think the issue is probably incorrect version of Z3. I checked again and the installation script works for me. Could you check if you have Z3 4.6.2 installed?

$ z3 --version
Z3 version 4.6.2 - 64 bit

Also, please make sure you installed Python bindings for Z3 4.6.2.