Stream: Mirror: Isabelle Development Mailing List

Topic: [isabelle-dev] Back to Z3 4.4.0pre for all platforms exce...


view this post on Zulip Email Gateway (Nov 16 2021 at 21:37):

From: Makarius <makarius@sketis.net>
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
isabelle-dev@in.tum.de
https://mailman46.in.tum.de/mailman/listinfo/isabelle-dev


Last updated: Mar 28 2024 at 08:18 UTC