diff -r 87718883c8b9 -r b6f6e3ca2bdc NEWS
--- a/NEWS	Mon Nov 15 23:51:41 2021 +0100
+++ b/NEWS	Mon Nov 15 23:52:08 2021 +0100
@@ -205,6 +205,7 @@
       Vampire 4.6 (with Open Source license)
       veriT 2021.06-rmx
       Zipperposition 2.1
+      Z3 4.4.1
   - Adjusted default provers:
       cvc4 vampire verit e spass z3 zipperposition
   - Adjusted Zipperposition's slicing.
@@ -223,8 +224,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
@@ -941,8 +942,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