After a brief interlude with Z3 4.4.1 on all platforms (Isabelle/87718883c8b9) we are back to the old situation of 4.4.0pre unstable, and Z3 4.4.1 is only for arm64-linux (Isabelle/796ae338eb9d).
The release notes concerning Z3 4.4.1 mainly say "A multitude of bugs has been fixed" https://github.com/Z3Prover/z3/blob/95c9ccb2959/RELEASE_NOTES but out smt setup seems to need such special unintended behaviour from 4.4.0. (This shows in real life, that "semantic versioning" does not quite work: bugs and required features are often indistinguishable.) Our NEWS file says "Z3 4.4.1 for arm64-linux, which approximates Z3 4.4.0pre, but sometimes failes or crashes". In practice this means: * A few AFP sessions don't work with this version (prover failure): Binding_Syntax_Theory, BenOr_Kozen_Reif, Grothendieck_Schemes, Padic_Ints. * A few examples in HOL-SMT_Examples.SMT_Tests produce a hard crash, e.g. in examples concerning lists; there is spurious non-termination elsewhere. Most other examples do work, though. It should be noted that the Z3 repository https://github.com/Z3Prover shows many traces of amendments for ARM64 in the past 2-3 years, but not yet at the stage of 4.4.1. Debian 9 + 10 providing a package for arm64-linux does not prove its quality, because non-mainstream tools are routinely broken on Debian. (Or maybe it is because of their rather big "typos.patch"?) Makarius _______________________________________________ isabelle-dev mailing list [email protected] https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev
