[isabelle-dev] Back to Z3 4.4.0pre for all platforms except arm64-linux

[Makarius]

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