update Readme and format tables.

Author: kfriedberger

README.md

@@ -60,19 +60,19 @@ Only a few SMT solvers provide support for theories like Arrays, Floating Point,
 
 JavaSMT supports several SMT solvers (see [Getting Started](doc/Getting-started.md) for installation):
 
-| SMT Solver |       Linux x64       |     Linux arm64     | Windows x64 | Windows arm64 |                       MacOS x64                        | MacOS arm64 | Description |
-| --- |:---------------------:|:-------------------:|:---:|:---:|:------------------------------------------------------:|:---:|:--- |
-| [Bitwuzla](https://bitwuzla.github.io/) |  :heavy_check_mark:²  | :heavy_check_mark:² | :heavy_check_mark: |  |                                                        |  | a fast solver for bitvector logic |
-| [Boolector](https://boolector.github.io/) |  :heavy_check_mark:   |                     |  |  |                                                        |  | a fast solver for bitvector logic, misses formula introspection, deprecated |
-| [CVC4](https://cvc4.github.io/) |  :heavy_check_mark:   |                     |  |  |                                                        |  |  |
-| [CVC5](https://cvc5.github.io/) |  :heavy_check_mark:  |  :heavy_check_mark:  |  :heavy_check_mark:  |  |  :heavy_check_mark:  |  :heavy_check_mark:  |  |
-| [MathSAT5](http://mathsat.fbk.eu/) |  :heavy_check_mark:   | :heavy_check_mark:  | :heavy_check_mark: |  | [maybe](https://github.com/sosy-lab/java-smt/pull/430)³ |  |  |
-| [OpenSMT](https://verify.inf.usi.ch/opensmt) |  :heavy_check_mark:²  | :heavy_check_mark:² |  |  |                                                        |  |  |
-| [OptiMathSAT](http://optimathsat.disi.unitn.it/) |  :heavy_check_mark:   |                     |  |  |                                                        |  | based on MathSAT5, with support for optimization queries |
-| [Princess](http://www.philipp.ruemmer.org/princess.shtml) |  :heavy_check_mark:   | :heavy_check_mark:  | :heavy_check_mark: | :heavy_check_mark: |                   :heavy_check_mark:                   | :heavy_check_mark: | Java-based SMT solver |
-| [SMTInterpol](https://ultimate.informatik.uni-freiburg.de/smtinterpol/) |  :heavy_check_mark:   | :heavy_check_mark:  | :heavy_check_mark: | :heavy_check_mark: |                   :heavy_check_mark:                   | :heavy_check_mark: | Java-based SMT solver |
-| [Yices2](https://yices.csl.sri.com/) |  :heavy_check_mark:   |                     | [maybe](https://github.com/sosy-lab/java-smt/pull/215) |  | [maybe](https://github.com/sosy-lab/java-smt/pull/400)³ |  |  |
-| [Z3](https://github.com/Z3Prover/z3) |  :heavy_check_mark:²  | :heavy_check_mark:² | :heavy_check_mark: | :heavy_check_mark: |                   :heavy_check_mark:                   | :heavy_check_mark: | mature and well-known solver |
+| SMT Solver | Linux x64 | Linux arm64 | Windows x64 | Windows arm64 | MacOS x64 | MacOS arm64 | Description |
+| --- |:---:|:---:|:---:|:---:|:---:|:---:|:--- |
+| [Bitwuzla](https://bitwuzla.github.io/) | :heavy_check_mark:² | :heavy_check_mark:² | :heavy_check_mark: |  |  |  | a fast solver for bitvector logic |
+| [Boolector](https://boolector.github.io/) | :heavy_check_mark: |  |  |  |  |  | a fast solver for bitvector logic, misses formula introspection, deprecated |
+| [CVC4](https://cvc4.github.io/) | :heavy_check_mark: |  |  |  |  |  |  |
+| [CVC5](https://cvc5.github.io/) | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: |  | :heavy_check_mark: | :heavy_check_mark: |  |
+| [MathSAT5](http://mathsat.fbk.eu/) | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: |  | [maybe](https://github.com/sosy-lab/java-smt/pull/430)⁴ |  |  |
+| [OpenSMT](https://verify.inf.usi.ch/opensmt) | :heavy_check_mark:² | :heavy_check_mark:² |  |  |  |  |  |
+| [OptiMathSAT](http://optimathsat.disi.unitn.it/) | :heavy_check_mark: |  |  |  |  |  | based on MathSAT5, with support for optimization queries |
+| [Princess](http://www.philipp.ruemmer.org/princess.shtml) | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | Java-based SMT solver |
+| [SMTInterpol](https://ultimate.informatik.uni-freiburg.de/smtinterpol/) | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | Java-based SMT solver |
+| [Yices2](https://yices.csl.sri.com/) | :heavy_check_mark: |  | [maybe](https://github.com/sosy-lab/java-smt/pull/215) |  | [maybe](https://github.com/sosy-lab/java-smt/pull/400)⁴ |  |  |
+| [Z3](https://github.com/Z3Prover/z3) | :heavy_check_mark:³ | :heavy_check_mark:³ | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | mature and well-known solver |
 
 We support a reasonable list of operating systems and versions.
 - Our main target is Linux (mainly Ubuntu or comparable Linux distributions).
@@ -88,7 +88,9 @@ available with Ubuntu 18.04 or later.
 
 ² Solver requires at least `GLIBC_2.29`/`GLIBCXX_3.4.26` or `GLIBC_2.34`/`GLIBCXX_3.4.29`,
 available with Ubuntu 22.04 or later.  
-³ We do not provide a signed solver library for macOS. The user needs to compile and sign it.
+³ Solver requires at least `GLIBC_2.38`/`GLIBCXX_3.4.31`,
+available with Ubuntu 24.04 or later.  
+⁴ We do not provide a signed solver library for macOS. The user needs to compile and sign it.
 
 #### Solver Features
 
@@ -109,7 +111,7 @@ If something specific is missing, please [look for or file an issue](https://git
 
 #### Multithreading Support
 
-| SMT Solver | Concurrent context usage⁴ | Concurrent prover usage⁵ |
+| SMT Solver | Concurrent context usage⁵ | Concurrent prover usage⁶ |
 | --- |:---:|:---:|
 | [Bitwuzla](https://bitwuzla.github.io/) | :heavy_check_mark: |  |
 | [Boolector](https://boolector.github.io/) | :heavy_check_mark: |  |
@@ -126,13 +128,13 @@ If something specific is missing, please [look for or file an issue](https://git
 Interruption using a [ShutdownNotifier][] may be used to interrupt a solver from any thread.
 Formulas are translatable in between contexts/provers/threads using _FormulaManager.translateFrom()_.
 
-⁴ Multiple contexts, but all operations on each context only from a single thread.  
-⁵ Multiple provers on one or more contexts, with each prover using its own thread.
+⁵ Multiple contexts, but all operations on each context only from a single thread.  
+⁶ Multiple provers on one or more contexts, with each prover using its own thread.
 
 #### Garbage Collection in Native Solvers
 
 JavaSMT exposes an API for performing garbage collection on solvers implemented in a native language.
-As a native solver has no way of knowing whether the created formula object is still referenced 
+As a native solver has no way of knowing whether the created formula object is still referenced
 by the client application, this API is necessary to avoid leaking memory.
 Note that several solvers already support _hash consing_ and thus,
 there is never more than one copy of an identical formula object in memory.
@@ -141,9 +143,9 @@ in the application, it is not necessary to perform any garbage collection at all
 Additionally, the memory for formulas created on user-side (i.e., via JavaSMT) is negligible
 compared to solver-internal memory-consumption when solving a hard SMT query.
 
-- **Z3**: The parameter `solver.z3.usePhantomReferences` may be used to control 
-  whether JavaSMT will attempt to decrease references on Z3 formula 
-  objects once they are no longer referenced.
+- **Z3**: The parameter `solver.z3.usePhantomReferences` may be used to control
+  whether JavaSMT will attempt to decrease references on Z3 formula objects
+  once they are no longer referenced.
 - **MathSAT5**: Currently we do not support performing garbage collection for MathSAT5.
 - **CVC4, CVC5, Bitwuzla, OpenSMT**: Solvers using SWIG bindings do perform garbage collection.
 - **Other native SMT solvers**: we do not perform garbage collection.