Update Yices to version 2.8.0

.appveyor.yml

@@ -45,6 +45,7 @@ build_script:
       Copy-Item -Path "lib\java\runtime-mathsat\x64\*.dll" -Destination "lib\native\x86_64-windows\" -Force
       Copy-Item -Path "lib\java\runtime-bitwuzla\x64\*.dll" -Destination "lib\native\x86_64-windows\" -Force
       Copy-Item -Path "lib\java\runtime-cvc5\x64\*.dll" -Destination "lib\native\x86_64-windows\" -Force
+      Copy-Item -Path "lib\java\runtime-yices2\x64\*.dll" -Destination "lib\native\x86_64-windows\" -Force
 
 test_script:
   - ant unit-tests

README.md

@@ -61,20 +61,20 @@ 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: | :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 |
-| [Z3_WITH_INTERPOLATION](https://github.com/Z3Prover/z3) | :heavy_check_mark: | :heavy_check_mark: |  |  |  |  | an older version of Z3 that still provides interpolation support |
+| 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:                    | :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:  |                     | :heavy_check_mark: |                    | [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                                                |
+| [Z3_WITH_INTERPOLATION](https://github.com/Z3Prover/z3)                 | :heavy_check_mark:  | :heavy_check_mark:  |                    |                    |                                                         |                    | an older version of Z3 that still provides interpolation support            |
 
 We support a reasonable list of operating systems and versions.
 - Our main target is Linux (mainly Ubuntu or comparable Linux distributions).
@@ -114,19 +114,19 @@ If something specific is missing, please [look for or file an issue](https://git
 
 #### Multithreading Support
 
-| SMT Solver | Concurrent context usage⁵ | Concurrent prover usage⁶ |
-| --- |:---:|:---:|
-| [Bitwuzla](https://bitwuzla.github.io/) | :heavy_check_mark: |  |
-| [Boolector](https://boolector.github.io/) | :heavy_check_mark: |  |
-| [CVC4](https://cvc4.github.io/) | :heavy_check_mark: | :heavy_check_mark: |
-| [CVC5](https://cvc4.github.io/) | :question: |  |
-| [MathSAT5](http://mathsat.fbk.eu/) | :heavy_check_mark: |  |
-| [OpenSMT](https://verify.inf.usi.ch/opensmt) | :question: |  |
-| [OptiMathSAT](http://optimathsat.disi.unitn.it/) | :heavy_check_mark: |  |
-| [Princess](http://www.philipp.ruemmer.org/princess.shtml) | :heavy_check_mark: |  |
-| [SMTInterpol](https://ultimate.informatik.uni-freiburg.de/smtinterpol/) | :heavy_check_mark: |  |
-| [Yices2](https://yices.csl.sri.com/) |  |  |
-| [Z3](https://github.com/Z3Prover/z3) | :heavy_check_mark: |  |
+| SMT Solver                                                              | Concurrent context usage⁵ | Concurrent prover usage⁶ |
+|-------------------------------------------------------------------------|:-------------------------:|:------------------------:|
+| [Bitwuzla](https://bitwuzla.github.io/)                                 |    :heavy_check_mark:     |                          |
+| [Boolector](https://boolector.github.io/)                               |    :heavy_check_mark:     |                          |
+| [CVC4](https://cvc4.github.io/)                                         |    :heavy_check_mark:     |    :heavy_check_mark:    |
+| [CVC5](https://cvc4.github.io/)                                         |    :heavy_check_mark:     |                          |
+| [MathSAT5](http://mathsat.fbk.eu/)                                      |    :heavy_check_mark:     |                          |
+| [OpenSMT](https://verify.inf.usi.ch/opensmt)                            |    :heavy_check_mark:     |                          |
+| [OptiMathSAT](http://optimathsat.disi.unitn.it/)                        |    :heavy_check_mark:     |                          |
+| [Princess](http://www.philipp.ruemmer.org/princess.shtml)               |    :heavy_check_mark:     |                          |
+| [SMTInterpol](https://ultimate.informatik.uni-freiburg.de/smtinterpol/) |    :heavy_check_mark:     |                          |
+| [Yices2](https://yices.csl.sri.com/)                                    |    :heavy_check_mark:     |                          |
+| [Z3](https://github.com/Z3Prover/z3)                                    |    :heavy_check_mark:     |                          |
 
 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()_.

build/build-maven-publish.xml

@@ -266,10 +266,13 @@ SPDX-License-Identifier: Apache-2.0
         <!-- get revision from dependencies -->
         <ivy:artifactproperty name="[artifact].revision" value="[revision]"/>
         <property name="stage.solver" value="yices2"/>
-        <property name="stage.revision" value="${libyices2j.revision}"/>
+        <property name="stage.revision" value="${yices.revision}"/>
+        <property name="libDir.x64" value="lib/java/runtime-yices2/x64"/>
         <!-- prepare the pom-file -->
         <generate-solver-pom-file/>
         <!-- then publish the file -->
-        <stage-solver-file filename="libyices2j" classifier="libyices2j" fileending="so"/>
+        <stage-solver-file filename="yices" fileending="jar"/>
+        <stage-solver-file filename="libyices2java" classifier="libyices2java-x64" filedirectory="${libDir.x64}" fileending="so"/>
+        <stage-solver-file filename="yices2java" classifier="yices2java-x64" filedirectory="${libDir.x64}" fileending="dll"/>
     </target>
 </project>