Follow recent development / stable release of the important Z3 project, with current multi-platform support.
This probably requires significant changes of the Isabelle/SMT setup.
Follow recent development / stable release of the important Z3 project, with current multi-platform support.
This probably requires significant changes of the Isabelle/SMT setup.
Not yet for the Isabelle2021 release, unless someone does it very quickly and thoroughly during 01-Nov-2020..15-Dec-2020.
Basically currently the proof format of Z3 has bugs that we cannot solve on the Isabelle side (https://github.com/Z3Prover/z3/issues/5073). Fixing those requires either internal Z3 knowledge or time from a Z3 developer.
Additionally, Nikolaj Bjorner is reworking the proof format. Currently it looks like a lot more work on the Isabelle side (trimming the proof). Also handling of inprocessing is not clear yet.
Not ready for the Isabelle2021-1 release, approx. 15-Dec-2021. Note that veriT is more and more taking over.
See also 796ae338eb9d: use z3-4.4.1 for arm64-linux, which often works like pre-4.4.0 and sometimes crashes.