As discussed in #16 (comment), ideally scripts (and in particular profile-all.sh) would use the same version as the rest of the toolchain. This could easily be achieved by using the environment variable Z3_EXE (which is used by the other tools), instead of Z3_PATH. However, this is currently not possible due to the circumstances explained in viperproject/silicon#786.
For the script to be able to use newer versions of Z3, (at least) the following things probably need to be done:
- Fix
Invalid quantifier instances line from prover:
- Find documentation for the columns (since their amount has changed)
- Adapt
profile.py based on the documentation for the columns (at least process_output(output))
As discussed in #16 (comment), ideally scripts (and in particular
profile-all.sh) would use the same version as the rest of the toolchain. This could easily be achieved by using the environment variableZ3_EXE(which is used by the other tools), instead ofZ3_PATH. However, this is currently not possible due to the circumstances explained in viperproject/silicon#786.For the script to be able to use newer versions of Z3, (at least) the following things probably need to be done:
Invalid quantifier instances line from prover:profile.pybased on the documentation for the columns (at leastprocess_output(output))