--- a/NEWS Fri Nov 12 18:47:07 2021 +0100
+++ b/NEWS Tue Nov 16 21:53:09 2021 +0100
@@ -206,10 +206,12 @@
* Sledgehammer:
- Update of bundled provers:
- E 2.6
- Vampire 4.6 (with Open Source license)
- veriT 2021.06-rmx
- Zipperposition 2.1
+ . E 2.6
+ . Vampire 4.6 (with Open Source license)
+ . veriT 2021.06.1-rmx
+ . Zipperposition 2.1
+ . Z3 4.4.1 for arm64-linux, which approximates Z3 4.4.0pre,
+ but sometimes failes or crashes
- Adjusted default provers:
cvc4 vampire verit e spass z3 zipperposition
- Adjusted Zipperposition's slicing.
@@ -228,8 +230,8 @@
implementation defect. Very slight INCOMPATIBILITY.
* Nitpick: External solver "MiniSat" is available for all supported
-Isabelle platforms (including Windows and ARM); while "MiniSat_JNI" only
-works for Intel Linux and macOS.
+Isabelle platforms (including 64bit Windows and ARM); while
+"MiniSat_JNI" only works for Intel Linux and macOS.
* Theory HOL-Library.Lattice_Syntax has been superseded by bundle
"lattice_syntax": it can be used in a local context via 'include' or in
@@ -946,8 +948,8 @@
/usr/local/bin/isabelle-phabricator-upgrade and each installation root
directory (e.g. /var/www/phabricator-vcs/libphutil).
-* Experimental support for arm64-linux platform. The reference platform
-is Raspberry Pi 4 with 8 GB RAM running Pi OS (64 bit).
+* Almost complete support for arm64-linux platform. The reference
+platform is Raspberry Pi 4 with 8 GB RAM running Pi OS (64 bit).
* Support for Apple Silicon, using mostly x86_64-darwin runtime
translation via Rosetta 2 (e.g. Poly/ML and external provers), but also