Support current Z3 versions + Use Z3_EXE (instead of Z3_PATH) - Githubissues

viperproject / gobra-libs

Standard library for the Gobra verifier for Go. Contains definitions and lemmas useful for verifying large projects.

MIT License

2 stars 1 forks source link

Support current Z3 versions + Use Z3_EXE (instead of Z3_PATH) #19

Open dnezam opened 4 months ago

dnezam commented 4 months ago

As discussed in https://github.com/viperproject/gobra-libs/pull/16#discussion_r1580996212, 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 https://github.com/viperproject/silicon/issues/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))

jcp19 commented 4 months ago

Thanks!