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 <>
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" 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 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"?)


isabelle-dev mailing list

Last updated: Mar 04 2024 at 10:08 UTC