getSolvers() {
public Solvers solver;
private static final String OS = System.getProperty("os.name").toLowerCase().replace(" ", "");
- private static final boolean IS_WINDOWS = OS.startsWith("windows");
- private static final boolean IS_MAC = OS.startsWith("macos");
private static final boolean IS_LINUX = OS.startsWith("linux");
+ private static final boolean IS_X64 = System.getProperty("os.arch").contains("64");
- /**
- * Let's allow to disable some checks on certain combinations of operating systems and solvers,
- * because of missing support.
- *
- * We update this list, whenever a new solver or operating system is added.
- */
+ /** Disable some checks on certain combinations of operating systems and solvers, because of missing dependencies. */
private static boolean isOperatingSystemSupported(Solvers solver) {
- switch (solver) {
- case SMTINTERPOL:
- case PRINCESS:
- // any operating system is allowed, Java is already available.
- return true;
- case BOOLECTOR:
- case CVC4:
- case CVC5:
- case OPENSMT:
- case YICES2:
- return IS_LINUX;
- case MATHSAT5:
- case BITWUZLA:
- return IS_LINUX || IS_WINDOWS;
- case Z3:
- return IS_LINUX || IS_WINDOWS || IS_MAC;
- default:
- throw new AssertionError("unexpected solver: " + solver);
- }
+ return switch (solver) {
+ case SMTINTERPOL, PRINCESS -> true; // Java-based solvers should work on all platforms
+ default -> IS_LINUX && IS_X64; // this example only includes Linux x64 binaries for native solvers
+ };
}
private Configuration config;
diff --git a/doc/Example-Maven-Web-Project/Dockerfile b/doc/Example-Maven-Web-Project/Dockerfile
new file mode 100644
index 0000000000..01a3683671
--- /dev/null
+++ b/doc/Example-Maven-Web-Project/Dockerfile
@@ -0,0 +1,32 @@
+# This file is part of JavaSMT,
+# an API wrapper for a collection of SMT solvers:
+# https://github.com/sosy-lab/java-smt
+#
+# SPDX-FileCopyrightText: 2026 Dirk Beyer
+#
+# SPDX-License-Identifier: Apache-2.0
+
+FROM ubuntu:24.04
+
+# Avoid interactive prompts during apt installations
+ENV DEBIAN_FRONTEND=noninteractive
+
+# 1. Update and install Java 17 + Tomcat 10
+RUN apt-get update && apt-get install -y \
+ openjdk-17-jdk \
+ tomcat10 \
+ && rm -rf /var/lib/apt/lists/*
+
+# 2. Set the environment so Tomcat knows where everything is
+ENV CATALINA_HOME=/usr/share/tomcat10
+ENV CATALINA_BASE=/var/lib/tomcat10
+
+# 3. Expose the default Tomcat port
+EXPOSE 8080
+
+# 4. Clean out default apps and copy your WAR file to the container
+RUN rm -rf $CATALINA_BASE/webapps/*
+COPY ./target/java-smt-web-example-2.0.war $CATALINA_BASE/webapps/ROOT.war
+
+# 5. Run Tomcat in the foreground
+CMD ["/usr/share/tomcat10/bin/catalina.sh", "run"]
diff --git a/doc/Example-Maven-Web-Project/README.md b/doc/Example-Maven-Web-Project/README.md
index 21e657d909..ab837b6a97 100644
--- a/doc/Example-Maven-Web-Project/README.md
+++ b/doc/Example-Maven-Web-Project/README.md
@@ -3,32 +3,93 @@ This file is part of JavaSMT,
an API wrapper for a collection of SMT solvers:
https://github.com/sosy-lab/java-smt
-SPDX-FileCopyrightText: 2021 Dirk Beyer
+SPDX-FileCopyrightText: 2026 Dirk Beyer
SPDX-License-Identifier: Apache-2.0
-->
-This is an example web-application for using JavaSMT with Maven.
-The example application prints a table of the available SMT solvers,
-their version number and supported features.
-
-The Maven workflow in this project supports the following steps:
-
-- Compiling: `mvn compile` downloads all dependencies and compiles the project.
-- Testing: `mvn test` executes the Sudoku example test.
-- Packaging: `mvn package` creates a war file for the example application.
- Dependencies like other jar files and binaries for SMT solvers are included in the war file.
-- Running: the war file can be applied with your tomcat instance.
- On Ubuntu you can use the following commands:
- - Install tomcat9 (required once only):
- `sudo apt install tomcat9` and `sudo service tomcat9 start`
- - Copy the war file to the webapps directory:
- `sudo cp target/java-smt-web-example-VERSION.war /var/lib/tomcat9/webapps/`.
- The running instance of tomcat9 will automatically unpack the war file.
- - Open `http://localhost:8080/java-smt-web-example-VERSION/SolverOverviewServlet`,
- and you should see a table of the available SMT solvers.
-
-Please note that the Maven repository currently only contains release versions
-and no snapshots, thus the newest features and bugfixes might be missing.
-If a Maven step is not working or more steps are required,
-please ask or report an issue [in the project](https://github.com/sosy-lab/java-smt).
+# JavaSMT Maven Web Example
+
+This project shows how to use JavaSMT in a Maven-based web environment (WAR-based).
+It includes a servlet that lists available solvers and a test case that solves a Sudoku puzzle.
+The configuration in `pom.xml` handles the download and setup of native solver libraries (e.g., Z3, MathSAT5, CVC5) so they can be bundled into the WAR file.
+
+## Prerequisites
+
+* Java 17 or newer.
+* Apache Maven.
+* A servlet container like Apache Tomcat (e.g., version 10 or newer).
+* Native solvers are only provided for **Linux x64** in this example.
+ Some solvers like Z3 and MathSAT5 also support Windows or ARM64 platform, if dependencies are adjusted in `pom.xml`.
+ Java-only solvers (SMTInterpol, Princess) work on all platforms.
+* When using Linux, please use Ubuntu 24.04 or newer, as we provide latest solver versions for GLIBC_2.33 or newer.
+
+## Usage
+
+### Compile and Build
+
+Run the following to download dependencies and build the WAR file:
+```bash
+mvn clean package
+```
+Native libraries will be copied, renamed, and included in `WEB-INF/lib` of the generated WAR file.
+
+### Run the Solver Overview Servlet
+
+The WAR file can be deployed to your servlet container.
+On Ubuntu with Tomcat, you can use the following steps:
+
+1. Install Tomcat (required once):
+ ```bash
+ sudo apt install tomcat10
+ sudo service tomcat10 start
+ ```
+2. Copy the WAR file to the `webapps` directory:
+ ```bash
+ sudo cp target/java-smt-web-example-VERSION.war /var/lib/tomcat10/webapps/
+ ```
+ Tomcat will automatically unpack the WAR file.
+3. Open the following URL in your browser:
+ `http://localhost:8080/java-smt-web-example-VERSION/SolverOverviewServlet`
+ You should see a table of the available SMT solvers.
+
+
+### Run the Solver Overview Servlet in a Docker Container
+
+You can also run the servlet in a Docker container. Here’s how:
+0. Compile and package the WAR file as described above.
+1. Build the Docker image from `Dockerfile`:
+ ```bash
+ podman build -t java-smt-web-example .
+ ```
+2. Run the Docker container:
+ ```bash
+ podman run -p 8080:8080 java-smt-web-example
+ ```
+3. Access the servlet at `http://localhost:8080/SolverOverviewServlet` in your browser.
+
+
+### Run Sudoku Test
+
+The `SudokuTest` runs against all available solvers during the build process.
+
+```bash
+mvn test
+```
+
+## Project Structure
+
+* `src/main/java/org/sosy_lab/SolverOverviewServlet.java`: Servlet implementation.
+* `src/test/java/org/sosy_lab/java_smt_web_example/SudokuTest.java`: Parameterized JUnit test.
+* `src/main/webapp/WEB-INF/web.xml`: Web application configuration.
+* `pom.xml`: Maven configuration including dependency management and native library handling.
+
+## Native Library Handling
+
+JavaSMT backends often require native binaries. This project automates the following steps:
+1. Download native libraries via Maven dependencies (using `classifier` and `type`).
+2. Copy them to a temporary directory using `maven-dependency-plugin`.
+3. Rename them (e.g., from `javasmt-solver-z3-libz3java-x64.so` to `libz3java.so`) using `maven-antrun-plugin` to match JavaSMT expectations.
+4. Bundle the renamed libraries into `WEB-INF/lib` of the WAR file using `maven-war-plugin`.
+
+For more details, see the [JavaSMT documentation](https://github.com/sosy-lab/java-smt).
diff --git a/doc/Example-Maven-Web-Project/pom.xml b/doc/Example-Maven-Web-Project/pom.xml
index d32c8c1339..c95f4ce0a2 100644
--- a/doc/Example-Maven-Web-Project/pom.xml
+++ b/doc/Example-Maven-Web-Project/pom.xml
@@ -5,7 +5,7 @@ This file is part of JavaSMT,
an API wrapper for a collection of SMT solvers:
https://github.com/sosy-lab/java-smt
-SPDX-FileCopyrightText: 2025 Dirk Beyer
+SPDX-FileCopyrightText: 2026 Dirk Beyer
SPDX-License-Identifier: Apache-2.0
-->
@@ -16,7 +16,7 @@ SPDX-License-Identifier: Apache-2.0
org.sosy_lab.java_smt_web_example
java-smt-web-example
- 1.12
+ 2.0
war
java-smt-maven-web-example
Example Maven project to show how to use JavaSMT with native solver libraries in a web project.
@@ -74,29 +74,51 @@ SPDX-License-Identifier: Apache-2.0
x64
- 5.0.0
- 0.7.0-13.1-g595512ae
+ 6.0.0
+ 0.8.2-339-g550ed911
3.2.2-g1a89c229
1.8-prerelease-2020-06-24-g7825d8f28
- 1.0.5-g4cb2ab9eb
- 5.6.11-glibc2.27
- 2.8.0-sosy0-ge831bf23
- 4.1.1-734-g3732f7e08
- 2.6.2-396-g194350c1
- 4.13.4
+ 2026-02-26-d22638a
+ 5.6.15
+ 2.9.0-gef441e1c
+ 2.5-1242-g5c50fb6d
+ 2025-11-17
+ 2.0
+ 5.0.1-1258-gdad634a69
+ 2.6.4-264-g553897f5
+ 4.15.4
+ 4.5.0-gd57a2a6dc
+
org.sosy-lab
java-smt
${javasmt.version}
+
+
+ de.uni-freiburg.informatik.ultimate
+ smtinterpol
+ ${smtinterpol.version}
+
+
+ io.github.uuverifiers
+ princess_2.13
+ ${princess.version}
+
+
+ io.github.uuverifiers
+ ostrich_2.13
+ ${ostrich.version}
+
+
org.sosy-lab
- javasmt-solver-mathsat5
+ javasmt-solver-mathsat
${mathsat.version}
libmathsat5j-${system.arch}
so
@@ -123,12 +145,33 @@ SPDX-License-Identifier: Apache-2.0
libz3java-${system.arch}
+
+
+ org.sosy-lab
+ javasmt-solver-z3-legacy
+ ${z3-legacy.version}
+ com.microsoft.z3legacy
+
+
+ org.sosy-lab
+ javasmt-solver-z3-legacy
+ ${z3-legacy.version}
+ so
+ libz3legacy-${system.arch}
+
+
+ org.sosy-lab
+ javasmt-solver-z3-legacy
+ ${z3-legacy.version}
+ so
+ libz3javalegacy-${system.arch}
+
+
org.sosy-lab
javasmt-solver-bitwuzla
${bitwuzla.version}
- jar
org.sosy-lab
@@ -166,7 +209,6 @@ SPDX-License-Identifier: Apache-2.0
org.sosy-lab
javasmt-solver-cvc4
${cvc4.version}
- jar
CVC4
@@ -191,48 +233,18 @@ SPDX-License-Identifier: Apache-2.0
libcvc4parser
-
-
- org.sosy-lab
- javasmt-solver-cvc5
- ${cvc5.version}
- jar
- cvc5
-
-
- org.sosy-lab
- javasmt-solver-cvc5
- ${cvc5.version}
- so
- libcvc5
-
-
- org.sosy-lab
- javasmt-solver-cvc5
- ${cvc5.version}
- so
- libcvc5jni
-
-
- org.sosy-lab
- javasmt-solver-cvc5
- ${cvc5.version}
- so
- libcvc5parser
-
+
org.sosy-lab
javasmt-solver-cvc5
${cvc5.version}
- so
- libpoly
org.sosy-lab
javasmt-solver-cvc5
${cvc5.version}
so
- libpolyxx
+ libcvc5jni-${system.arch}
@@ -240,7 +252,12 @@ SPDX-License-Identifier: Apache-2.0
org.sosy-lab
javasmt-yices2
${javasmt-yices.version}
- jar
+
+
+ org.sosy-lab
+ javasmt-solver-yices2
+
+
org.sosy-lab
@@ -255,7 +272,6 @@ SPDX-License-Identifier: Apache-2.0
org.sosy-lab
javasmt-solver-opensmt
${opensmt.version}
- jar
org.sosy-lab
@@ -282,263 +298,118 @@ SPDX-License-Identifier: Apache-2.0
-
-
-
-
- maven-surefire-plugin
- 3.0.0
-
-
+
+ org.apache.maven.plugins
+ maven-surefire-plugin
+ 3.5.4
+
+ -Djava.library.path=${project.dependency.path}
+
+
+
+
+
+ org.apache.maven.plugins
+ maven-war-plugin
+ 3.5.0
+
+
+
+ true
+
+
+
+
+ ${project.dependency.path}
+
+ **/*.so
+ **/*.dll
+ **/*.dylib
+
+ WEB-INF/lib
+
+
+
+
+
+
+ maven-jar-plugin
+ 3.5.0
+
+
+
+
- -Djava.library.path=${project.dependency.path}
-
-
-
- org.apache.maven.plugins
- maven-war-plugin
- 3.4.0
-
-
-
- true
-
-
-
-
- target/dependency
-
-
- libmathsat5j.so
- libz3.so
- libz3java.so
- libboolector.so
- libminisat.so
- libpicosat.so
- libcvc4.so
- libcvc4jni.so
- libcvc4parser.so
- libyices2j.so
- libcvc5.so
- libcvc5jni.so
- libcvc5parser.so
- libpoly.so
- libpolyxx.so
- libyices2j.so
- libopensmtj.so
-
- WEB-INF/lib
-
-
-
-
-
- maven-jar-plugin
- 3.4.0
-
-
-
-
- true
- ${project.dependency.relativepath}
- org.sosy_lab.SolverOverviewServlet
-
-
-
-
-
-
-
+ true
+ ${project.dependency.relativepath}/
+ org.sosy_lab.SolverOverviewServlet
+
+
+
+
+
+
-
org.apache.maven.plugins
maven-dependency-plugin
3.1.1
-
- copy
+ copy-natives-temp
initialize
- copy
+ copy-dependencies
+
+ ${project.build.directory}/temp-natives
+ so,dll,dylib
+ true
+
-
-
- copy-dependencies
- validate
+ copy-all-jars
+ initialize
copy-dependencies
+
+ ${project.dependency.path}
+ jar
+
+
+
+
+
+ org.apache.maven.plugins
+ maven-antrun-plugin
+ 3.1.0
+
+
+ rename-natives
+ process-resources
+
+ run
+
+
+
+
+
+
+
+
+
+
+
-
- ${project.dependency.path}
-
-
-
-
-
-
- org.sosy-lab
- javasmt-solver-mathsat5
- so
- libmathsat5j-${system.arch}
- libmathsat5j.so
-
-
-
-
- org.sosy-lab
- javasmt-solver-z3
- so
- libz3java-${system.arch}
- libz3java.so
-
-
- org.sosy-lab
- javasmt-solver-z3
- so
- libz3-${system.arch}
- libz3.so
-
-
-
-
- org.sosy-lab
- javasmt-solver-bitwuzla
- so
- libbitwuzlaj-${system.arch}
- libbitwuzlaj.so
-
-
-
-
- org.sosy-lab
- javasmt-solver-boolector
- so
- libboolector
- libboolector.so
-
-
- org.sosy-lab
- javasmt-solver-boolector
- so
- libminisat
- libminisat.so
-
-
- org.sosy-lab
- javasmt-solver-boolector
- so
- libpicosat
- libpicosat.so
-
-
-
-
- org.sosy-lab
- javasmt-solver-cvc4
- so
- libcvc4
- libcvc4.so
-
-
- org.sosy-lab
- javasmt-solver-cvc4
- so
- libcvc4jni
- libcvc4jni.so
-
-
- org.sosy-lab
- javasmt-solver-cvc4
- so
- libcvc4parser
- libcvc4parser.so
-
-
-
-
- org.sosy-lab
- javasmt-solver-cvc5
- so
- libcvc5
- libcvc5.so
-
-
- org.sosy-lab
- javasmt-solver-cvc5
- so
- libcvc5jni
- libcvc5jni.so
-
-
- org.sosy-lab
- javasmt-solver-cvc5
- so
- libcvc5parser
- libcvc5parser.so
-
-
- org.sosy-lab
- javasmt-solver-cvc5
- so
- libpoly
- libpoly.so
-
-
- org.sosy-lab
- javasmt-solver-cvc5
- so
- libpolyxx
- libpolyxx.so
-
-
-
-
- org.sosy-lab
- javasmt-solver-yices2
- so
- libyices2j
- libyices2j.so
-
-
-
-
- org.sosy-lab
- javasmt-solver-opensmt
- so
- libopensmtj-${system.arch}
- libopensmtj.so
-
-
-
diff --git a/doc/Example-Maven-Web-Project/src/main/java/org/sosy_lab/SolverOverviewServlet.java b/doc/Example-Maven-Web-Project/src/main/java/org/sosy_lab/SolverOverviewServlet.java
index 83179dd2fa..2833d832d8 100644
--- a/doc/Example-Maven-Web-Project/src/main/java/org/sosy_lab/SolverOverviewServlet.java
+++ b/doc/Example-Maven-Web-Project/src/main/java/org/sosy_lab/SolverOverviewServlet.java
@@ -2,7 +2,7 @@
// an API wrapper for a collection of SMT solvers:
// https://github.com/sosy-lab/java-smt
//
-// SPDX-FileCopyrightText: 2024 Dirk Beyer
+// SPDX-FileCopyrightText: 2026 Dirk Beyer
//
// SPDX-License-Identifier: Apache-2.0
diff --git a/doc/Example-Maven-Web-Project/src/test/java/org/sosy_lab/java_smt_web_example/SudokuTest.java b/doc/Example-Maven-Web-Project/src/test/java/org/sosy_lab/java_smt_web_example/SudokuTest.java
index 0a091c1604..d59de501fd 100644
--- a/doc/Example-Maven-Web-Project/src/test/java/org/sosy_lab/java_smt_web_example/SudokuTest.java
+++ b/doc/Example-Maven-Web-Project/src/test/java/org/sosy_lab/java_smt_web_example/SudokuTest.java
@@ -2,7 +2,7 @@
// an API wrapper for a collection of SMT solvers:
// https://github.com/sosy-lab/java-smt
//
-// SPDX-FileCopyrightText: 2024 Dirk Beyer
+// SPDX-FileCopyrightText: 2026 Dirk Beyer
//
// SPDX-License-Identifier: Apache-2.0
@@ -85,36 +85,15 @@ public static List getSolvers() {
public Solvers solver;
private static final String OS = System.getProperty("os.name").toLowerCase().replace(" ", "");
- private static final boolean IS_WINDOWS = OS.startsWith("windows");
- private static final boolean IS_MAC = OS.startsWith("macos");
private static final boolean IS_LINUX = OS.startsWith("linux");
+ private static final boolean IS_X64 = System.getProperty("os.arch").contains("64");
- /**
- * Let's allow to disable some checks on certain combinations of operating systems and solvers,
- * because of missing support.
- *
- * We update this list, whenever a new solver or operating system is added.
- */
+ /** Disable some checks on certain combinations of operating systems and solvers, because of missing dependencies. */
private static boolean isOperatingSystemSupported(Solvers solver) {
- switch (solver) {
- case SMTINTERPOL:
- case PRINCESS:
- // any operating system is allowed, Java is already available.
- return true;
- case BOOLECTOR:
- case CVC4:
- case CVC5:
- case OPENSMT:
- case YICES2:
- return IS_LINUX;
- case MATHSAT5:
- case BITWUZLA:
- return IS_LINUX || IS_WINDOWS;
- case Z3:
- return IS_LINUX || IS_WINDOWS || IS_MAC;
- default:
- throw new AssertionError("unexpected solver: " + solver);
- }
+ return switch (solver) {
+ case SMTINTERPOL, PRINCESS -> true; // Java-based solvers should work on all platforms
+ default -> IS_LINUX && IS_X64; // this example only includes Linux x64 binaries for native solvers
+ };
}
private Configuration config;
diff --git a/doc/Getting-started.md b/doc/Getting-started.md
index 8ee5819ffb..0e5bcde1bd 100644
--- a/doc/Getting-started.md
+++ b/doc/Getting-started.md
@@ -68,43 +68,58 @@ For Maven:
org.sosy-lab
java-smt
- 5.0.0-61-gea80187e
+ 6.0.0
```
-Currently, only `SMTInterpol` and `Princess` are automatically fetched from Maven Central,
-because they are written in Java and Scala, and thus are available on every machine.
-Shared object for other solvers, such as `MathSAT5` and `Z3`, can be added by using additional
-dependencies (example for Linux x64):
+Since release 6.0.0, JavaSMT does no longer include Java-based solvers automatically, but instead provides them as separate dependencies.
+This unifies the installation process for all solvers and allows users to only install the solvers they need.
+Solvers, such as `MathSAT5`, `SMTInterpol` and `Z3`, can be added by using additional dependencies (example for Linux x64):
```xml
-
+
org.sosy-lab
javasmt-solver-mathsat5
- 5.6.5
+ 5.6.15
+ libmathsat5j-x64
so
-
+
+
+ de.uni-freiburg.informatik.ultimate
+ smtinterpol
+ 2.5-1242-g5c50fb6d
+
+
+
org.sosy-lab
javasmt-solver-z3
- 4.8.10
+ 4.15.4
org.sosy-lab
javasmt-solver-z3
- 4.8.10
+ 4.15.4
+ libz3-x64
so
- libz3
org.sosy-lab
javasmt-solver-z3
- 4.8.10
+ 4.15.4
+ libz3java-x64
so
- libz3java
```
@@ -112,11 +127,13 @@ The XML snippets for other solvers available via Maven,
such as `Boolector`, `CVC4`, `CVC5`, `OpenSMT`, `Princess`, and `Yices2`,
can be found in the [`POM file`](Example-Maven-Project/pom.xml) of our [`Example-Maven-Project`](Example-Maven-Project).
-If you are not using Linux and we provide a solver binary for your system,
-you might need to set the dependencies accordingly, e.g.,
+If you are not using Linux, but Windows or macOS, or if you want to use a different architecture,
+such as `arm64`, you might need to set the dependencies accordingly, e.g.,
change the type from `so` to `dll` (for Windows) or `dylib` (for macOS),
and specify an architecture (e.g., `x64` or `arm64`).
-You can look up the required dependency files and filename extension in the [Ivy repository][].
+You can look up the required dependency files and filename extension in the [Ivy repository][] or [Maven Central][].
+Note that some solvers are not available for all platforms,
+so you might need to check the [Readme](../README.md) for supported platforms and solvers.
Additionally, you can add and configure some Maven plugins to load the libraries automatically
and place them in the correct directories when assembling your application.
@@ -142,8 +159,8 @@ And finally configure the classpath for your jar-plugin:
```
-See [`Example-Maven-Project`](Example-Maven-Project) for more information and a working example.
-See [`Example-Maven-Web-Project`](Example-Maven-Web-Project) for more information about a Dynamic-Web-Project runnable by Tomcat 9.
+See [`Example-Maven-Project`](Example-Maven-Project) for more information and a working example application.
+See [`Example-Maven-Web-Project`](Example-Maven-Web-Project) for more information about a Dynamic-Web-Project runnable by Tomcat.
### Manual Installation
@@ -156,25 +173,24 @@ In order to perform the manual installation, the following steps should be follo
**JavaSMT might not yet support the latest version on the solver's webpage,
but only the latest version in the [Ivy index](https://www.sosy-lab.org/ivy/org.sosy_lab/java-smt/).
Please file an issue, if the update of a solver library is required.**
- - Suppose the version `5.0.0` was chosen.
- Ivy description file [`ivy-5.0.0.xml`](https://www.sosy-lab.org/ivy/org.sosy_lab/java-smt/ivy-5.0.0.xml) can
+ - Suppose the version `6.0.0` was chosen.
+ Ivy description file [`ivy-6.0.0.xml`](https://www.sosy-lab.org/ivy/org.sosy_lab/java-smt/ivy-6.0.0.xml) can
be consulted in order to determine all the files which should be fetched.
- The artifacts tag specifies what files the release depends on.
- In the example case, those are `java-smt-5.0.0.jar` and (optionally)
- `java-smt-5.0.0-sources.jar`, located in the same directory.
+ In the example case, those are `java-smt-6.0.0.jar` and (optionally)
+ `java-smt-6.0.0-sources.jar`, located in the same directory.
- Finally, the dependencies can be manually followed and resolved.
- E.g. in the example, Z3 version `4.13.3` is specified,
- which is described by the corresponding [XML](https://www.sosy-lab.org/ivy/org.sosy_lab/javasmt-solver-z3/ivy-4.13.3.xml)
+ E.g. in the example, Z3 version `4.15.4` is specified,
+ which is described by the corresponding [XML](https://www.sosy-lab.org/ivy/org.sosy_lab/javasmt-solver-z3/ivy-4.15.4.xml)
file, specifying what binaries should be fetched from the corresponding
[directory](https://www.sosy-lab.org/ivy/org.sosy_lab/javasmt-solver-z3/).
### Binaries for Native Solvers
-When using Ivy or Maven for installation on a 64-bit Linux platform,
+When using Ivy for installation on a 64-bit Linux platform,
solver binaries for native solvers are downloaded automatically, if available.
The [Readme](../README.md) contains a list of solvers and supported platforms.
-Everything should work as is after installation.
Without Ivy or Maven you need to download and install the binaries manually as described above under [Manual Installation](#manual-installation).
You can either copy them into the directory of the JavaSMT JAR file,
@@ -229,7 +245,9 @@ can just use the JavaSMT API as follows:
If you want to use a custom loading mechanism, you can do so by implementing
a simple consumer interface and passing it to the `SolverContextFactory`.
-The following example uses the default Java class loader to load the native libraries:
+The following example uses the default Java class loader to load the native libraries,
+depending on the default environment variables `JAVA_LIBRARY_PATH` and `LD_LIBRARY_PATH`
+or option `-Djava.library.path`:
```java
SolverContext context = SolverContextFactory.createSolverContext(
@@ -305,7 +323,9 @@ Once the constraint is generated, we can solve it and get the model:
prover.addConstraint(constraint);
boolean isUnsat = prover.isUnsat();
if (!isUnsat) {
- Model model = prover.getModel();
+ try (Model model = prover.getModel()) {
+ // Do something with the model
+ }
}
}
```
diff --git a/doc/Maven-for-Developers.md b/doc/Maven-for-Developers.md
deleted file mode 100644
index 24b1ec1d79..0000000000
--- a/doc/Maven-for-Developers.md
+++ /dev/null
@@ -1,644 +0,0 @@
-
-
-____________________
-
-This documentation is intended for internal use only.
-Testing a Maven release is error-prone and complex.
-This document aims for helping in some steps.
-There is no guarantee for anything. Please test everything for yourself!
-____________________
-
-
-Local test for Maven (Still needs internet to pull dependencies for Maven)
-0. If you are only interested in the JavaSMT part and know basic Maven, skip to 13.
-1. Install Maven
-2. Install Sonatype Nexus Repository Manager 3 (Free Version!)
- 2.1 Download Nexus
- 2.2 Unpack .tar
- 2.3 Move Nexus-version and Sonatype-work folders to where you want them (/usr/local/ for example)
- 2.4 Change Folder permissions (chmod something)
-3. Start Nexus with ./nexus start (file located in nexus-version/bin/ folder with version being the nexus version you use)
- (You can stop it with ./nexus stop )
-4. Open a browser and enter: http://localhost:8081
-5. Press Log in in the top right corner and enter the name: "admin" and search for the password in the file located at Sonatype-work/nexus3/admin.password )
-6. Optional: Change Password
-7. Make a new User called "deployment" with a password of your choosing. (You can name it however you want. Just substitute deployment with your version from now on)
-8. Go to the Maven repository (~/.m2 most likely in the home dir. If you don't know where it is use this on the command line: mvn help:evaluate -Dexpression=settings.localRepository )
-9. If a settings.xml is present save it, else make a new one. (Or edit your current one if you know what you are doing)
-10. Enter the following into the settings.xml:
- (The urls are taken from the Nexus repository. You can find them at http://localhost:8081 after logging in in the left menu on browse and copy the url of maven-snapshot/releases)
- (The username and password have to match the ones you entered in step 7, it does not matter how they are named)
- (If you do not want to use the release or the snapshot repository you can simply omit it here and in all further steps.)
- (Difference release vs snapshot: snapshots can be overridden with the same version number by deploying again. Release can NEVER be overridden by deploying)
-
-```xml
-
-
-
- nexusrepo
- deployment
- the_password_for_the_deployment_user
-
-
-
-
-
-
- snapshot
-
-
- nexus-snapshot-repo
- my snapshot repo
- http://localhost:8081/repository/maven-snapshots/
-
-
-
-
-
- release
-
-
- nexus-release-repo
- my release repo
- http://localhost:8081/repository/maven-releases/
-
-
-
-
-
-
-
- release
-
-
-```
-
-11. If you want to test a Project, download the test Project from Maven with the following command:
- mvn archetype:generate -DgroupId=com.mycompany.app -DartifactId=my-app -DarchetypeArtifactId=maven-archetype-quickstart -DarchetypeVersion=1.4 -DinteractiveMode=false
-12. Now switch to the new folder called "my-app" and go through the existing pom.xml and copy the parts missing
- (copy it into a .xml so that you can read it easier):
-
-```xml
-
-
-
-
- 4.0.0
-
- com.mycompany.app
-
-
- my-app
-
- 1.0-SNAPSHOT
-
-
-
-
-
- junit
- junit
- 4.10
-
-
-
-
-
-
-
- nexusrepo
- My internal repository
- http://localhost:8081/repository/maven-snapshots/
-
-
-
- nexusrepo
- My internal repository
- http://localhost:8081/repository/maven-releases/
-
-
-
-
-
-
-
-
-
-
- maven-compiler-plugin
- 3.8.0
-
-
- 11
-
-
-
-
- maven-surefire-plugin
- 2.22.1
-
-
-
- maven-jar-plugin
- 3.0.2
-
-
-
- com.mycompany.app.App
-
-
-
-
-
- maven-deploy-plugin
- 2.8.1
-
-
- default-deploy
- deploy
-
- deploy
-
-
-
-
-
-
-
-
-```
-
-
-In this test project you can see and test some basic Maven ideas
-i.e. the folder structure, plugins, deployment etc.
-Besides the pom.xml you can see the /src folder that will bring you to the test project and the tests for said project.
-This folder layout is standard for maven and should be followed (src/main/java and src/test/java, after that you may change the names to your needs of course ;D )
-See: https://maven.apache.org/guides/introduction/introduction-to-the-standard-directory-layout.html
-We will cover changes in the JavaSMT example!
-Open a terminal in the directory with the pom.xml and you may enter the following example commands:
-mvn package // (tests and packages the project. You will get the test results in the cmd and a new folder target appears with the jar and class files etc.)
-mvn clean // (cleans the target folder etc.)
-mvn clean package // (first cleans, then uses package)
-mvn deploy // deploys the current project to the local Maven Repo with the set group/articactId and version and this pom.xml.
- This will use the active server from settings.xml.
- You should be able to see the project on said server in the browser-interface.
-
-## JavaSMT example from here:
------------------------------------------------------------------
-13. Use the following on the command line to deploy an artifact of your choice that was not compiled by Maven (For example shared libraries or our projects)
- Using a pom.xml for this works BUT you would create 2 deployments. One for the pom.xml and then one extra for the deploy-file goal, so just stick with this for now.
- url = url of the server
- repository = same name you gave in the entry of the settings.xml
- artifactId = name of the file (dependency) after deployment (do not use a file ending here)
- file = the file you want to deploy. You must be in the folder of the file or enter the path to it! You need the full filename including ending (.so for example).
- version = self-explanatory. Set it to your current version! Will get Appended to your artifactId for the final filename after deployment. No you can't just not enter one, i tried, i truly did....
- groupId = org.sosy-lab (most likely, for testing not relevant)
- packaging = file ending i.e. so, jar etc. for the final deployed file
- pomDescription = String that describes the artifact (Optional)
-
- The below is an example for mathsat5 deployment.
- You can look at it in the local nexus repo under "Browse" on the left side, maven-releases, org, sosy-lab, javasmt-mathsat5, 1.1
-
-
-mvn deploy:deploy-file -Durl=http://localhost:8081/repository/maven-releases/ -DrepositoryId=nexusrepo -Dfile=libmathsat5j.so -DgroupId=org.sosy-lab -DartifactId=javasmt-solver-mathsat5 -Dversion=1.1 -Dpackaging=so -DgeneratePom=false
-
-
- The below is an example for Z3 deployment:
- files= additional files (separated by a comma and NO spaces. If you use this you need to specify types and classifiers)
- classifiers=classifiers for the files (in the order they appear in files separated by a comma with no spaces)
- types= types of files (in the order they appear in files separated by a comma with no spaces)
-
-
-mvn deploy:deploy-file -Durl=http://localhost:8081/repository/maven-releases/ -DrepositoryId=nexusrepo -Dfile=lib/java/runtime-z3/com.microsoft.z3.jar -Dfiles=lib/java/runtime-z3/libz3java.so,lib/java/runtime-z3/libz3.so -Dtypes=so,so -DgroupId=org.sosy-lab -Dclassifiers=libz3java,libz3 -DartifactId=javasmt-solver-z3 -Dversion=4.8.9-sosy0 -Dpackaging=jar -DpomFile=solvers_maven_conf/maven_z3_pom.xml -DgeneratePom=false
-
-For deployment to Maven Central change the first part of the command to:
- mvn org.apache.maven.plugins:maven-gpg-plugin:1.3:sign-and-deploy-file
- Change url and repository to:
- -Durl=${ossrh-staging-repository-url} -DrepositoryId=${ossrh-server-id}
- Add to the end:
- -Pgpg
-
- Or simply take a look at the file /build/build-maven-publish.xml
-
- If you want to use those dependencies you need to rename them and copy them to a location that is checked
- by the sosy commons library!
- To perform this we need a little bit of user interaction.
-
-
-14. Use Mathsat5/Z3 with Maven:
- Open the pom.xml you want to use with JavaSMT and Mathsat5/Z3.
- (This assumes that you use the project provided. Meaning that there is the main-file
- my-app/src/main/java/com/mycompany/app/SolverOverviewTable.java and the test-file
- my-app/src/test/java/com/mycompany/app/SudokuTest.java
- You can change the folder structure as described above. Lets say you want
- javasmt-maven-example/src/main/java/org/sosy-lab/SolverOverviewTable.java then
- you just need to edit the following things: the folder structure itself, the groupId
- in the beginning of the pom.xml and the mainClass attribute of the maven-jar-plugin.
- Note: the name of the root dir in which the pom.xml resides is irrelevant for Maven.)
- Add this to the dependencies:
- (I assume you want to use both. Mathsat5 is 1 dependency with 1 solver binary.
- Z3 is 3 dependencies with 1 JAR and 2 binaries. If you don't want Z3 you need to remove
- all 3 here and 2 items from the copy
-
-```xml
-
- org.sosy-lab
- java-smt
- 3.7.0
-
-
- org.sosy-lab
- javasmt-solver-mathsat5
- 5.6.5
- so
-
-
-
- org.sosy-lab
- javasmt-solver-z3
- 1.2
-
-
- org.sosy-lab
- javasmt-solver-z3
- 1.2
- so
- libz3
-
-
- org.sosy-lab
- javasmt-solver-z3
- 1.2
- so
- libz3java
-
-
-
-
-
- junit
- junit
- 4.11
- test
-
-```
-
- Modify the plugins maven-surefire-plugin and maven-jar-plugin in pluginManagement:
-
-```xml
-
-
- maven-surefire-plugin
- 2.22.1
-
-
- -Djava.library.path=${project.build.directory}/dependency
-
-
-
- maven-jar-plugin
- 3.0.2
-
-
-
-
- true
- ${project.build.directory}/dependency
- com.mycompany.app.SolverOverviewTable
-
-
-
-
-```
-
- Additionally add the following to (NOT ).
- (If you really wanted it in there you need to execute it in later on!)
- is just like in .
-
-```xml
-
-
-
- org.apache.maven.plugins
- maven-dependency-plugin
- 3.1.1
-
-
-
- copy
- initialize
-
- properties
- copy
-
-
-
-
-
- copy-dependencies
- validate
-
- copy-dependencies
-
-
-
-
-
-
-
- org.sosy-lab
- javasmt-solver-mathsat5
- 5.6.5
- so
-
- ${project.build.directory}/dependency
- libmathsat5j.so
-
-
-
- org.sosy-lab
- javasmt-solver-z3
- 1.2
- so
- libz3java
-
- ${project.build.directory}/dependency
- libz3java.so
-
-
- org.sosy-lab
- javasmt-solver-z3
- 1.2
- so
- libz3
-
- ${project.build.directory}/dependency
- libz3.so
-
-
-
-
-```
-
- Due to the way org.sosy-lab.commons loads the native solver binaries it is currently not possible to build a single JAR
- that runs with Mathsat5/Z3 without any external dependencies.
- It is however possible to build a WAR file, see web tutorial below.
-
-15. Optional/Debug: You may need something to print our stuff like properties in Maven to debug your pom.xml.
- The following might help with that:
-
-```xml
-
- org.apache.maven.plugins
- maven-antrun-plugin
- 1.7
-
-
- compile
-
- run
-
-
-
-
- ******** Displaying value of a property ********
- ${java.library.path}
- ${org.sosy-lab:common:jar}
-
-
-
-
-
-```
-
-16. Web-Tutorial explaining how to create a Tomcat-Server:
-
- -Download Tomcat (i used the Tomcat 9 tarball): https://tomcat.apache.org/download-90.cgi
-
- -Extract at a location that you want to use for your server and set permissions.
-
- -We need to configure the admin login and the java location for the server first.
- In the extracted server folder go to the configuration folder and open tomcat-users.xml
- Insert the following inside the thingy:
-
-```xml
-
-
-
-```
-
- With this you can later deploy/delete war files to and from the server.
- You can of course set the username/password however you like.
- It is possible that the server later refuses those login details, i too had that problem,
- but then it went away and i don't know why. If you have this problem and find a solution please
- contact me (Daniel Baier)!
-
- To configure java you need to know where your default java is located. (It should be Java 8 +)
- Search for setenv.sh (on linux) in the bin folder of Tomcat. If its not there, create one.
- In there write:
-
- JRE_HOME=/path/to/your/java
- CATALINA_PID="$CATALINA_BASE/tomcat.pid"
-
- Technically you need to set CATALINA_HOME in the setenv too. However it should be set by default.
- (CATALINA_HOME default is your Tomcat folder)
-
- More information in the RUNNING.txt in the main folder of Tomcat.
-
- -You can now start your Tomcat 9 server with the startup.sh in the bin folder.
- You can stop it with the shutdown.sh in the same folder.
- You can access the server GUI via a Web-Browser and the IP: http://localhost:8080
- You can change/access/upload directly to the server via the "Manager App" in the top right corner.
- You need your login credentials specified above for that.
- In there you can upload via "Deploy" (War file to deploy).
- After deploying simply click the WAR in the Applications tab.
-
-
-17. Web-Tutorial explaining how to create a Dynamic Web Project (w Eclipse):
- (Simple example with 1 button that does something trivial)
-
- -Create a new Dynamic Web Project in Eclipse via new -> other -> Web
- (If you can't you are missing an extension for web projects.
- Most likely you won't be able to install a Server in Eclipse either.
- So download it from the marketplace.)
-
- -Choose a name
- Choose the runtime you downloaded (Tomcat 9 most likely)
- Module Version 4.0
- Default Configuration for your runtime
- EAR Membership simply EAR
- Click next twice and set the box to create a web.xml descriptor
-
- -Open your project in the project explorer, open Java Resources and create a package and a crate a new Servlet in there
- When creating a Servlet you need the "doPost" and "doGet" methods so just let them create automatically
- In this class (Servlet) you can now add your code to the code of the doGet method i.e.:
- Printwriter out = response.getWriter(); // We need this to print something. You need to import the IO package!
- out.println("Hallo Welt!");
-
- With this every time the servlet is used it will print "Hallo Welt!" on the screen.
-
- -Next we need a JSP Page to provide a frontend for the user:
- Right click WebContent in the project explorer -> new -> JSP File
- name it "index.jsp", choose the default options and finish.
- (We name it index because that one will be used as it is a standard, you may name if however you like)
- In this JSP add the following in the :
-
-```xml
- Welcome
-
-
-```
-
- This creates a button (type=submit) that has the text "Send" on it.
- Now go to WEB-INF/web.xml in your project.
- (insert the name of your JSP here if you don't want to name it index)
- Here you should be able to see a mapping to your Servlet.
- If not, add it yourself (this will assume your servlet is named MyServlet in a package named org.sosy-lab):
-
-```xml
-
-
- MyServlet
- MyServlet
- org.sosy-lab.MyServlet
-
-
- MyServlet
- /MyServlet
-
-```
-
- This mapping is not needed in an basic example (or at all).
- In servlet the description and display-name is optional and does what it says. (You can simply delete those 2 if you want)
- In servlet the servlet-class specifies the file you want to map to the servlet-name.
- In servlet-mapping you can map this servlet-name to one or more urls.
- You may access those urls later with the IP:port/MyServlet etc.
- (With IP:port being the IP/port you use for your server.
- By default you get the IP:port/MyServlet mapping anyway)
-
- If you want to test this you can right click the project and execute it with "run with".
- You will have to have installed the web development tools/server tools however
- and you have to choose/create a Tomcat server. Simply use the Tomcat server files you already downloaded.
-
-18. Web-Tutorial explaining how to create a WAR file with Maven:
-
- Now create a new folder (this will be the main folder of your Maven project).
- Name it however you like (i.e. MyProject) and enter it. In there create a new folder named "src" and your pom.xml.
- Enter the src folder, create a folder main here an copy your web project into this folder so that it looks like this:
- You may have to rename some folders to match the pattern below (src/main/java and src/main/webapp is a must!)
-
- MyProject
- |--pom.xml
- |--src
- |--main
- |--java
- | |--org
- | | |--sosy_lab
- | | | |--MyServlet.java
- |--webapp
- |--META-INF
- |--WEB-INF
- |--index.jsp
-
-
- More information here:
- https://maven.apache.org/guides/introduction/introduction-to-the-standard-directory-layout.html
-
-19. pom.xml for a web-project / how to create a WAR file with Maven:
-
- We will package the dependencies, including the native solver files, into the WAR.
- The pom looks nearly the same as the normal JAR pom, the differences are:
-
- ```xml
-
- war
-
-
-
-
- org.apache.maven.plugins
- maven-war-plugin
- 3.3.1
-
-
-
- true
-
-
-
-
- target/dependency
-
- libmathsat5j.so
- libz3.so
- libz3java.so
-
- WEB-INF/lib
-
-
-
-
- ```
-
- The rest needs to be set up exactly like before (except the jar plugin and the tests if you don't have any)
- Now mvn package should create a WAR file in the target directory for you that you may test on your own Tomcat server.
diff --git a/scripts/test-maven-central-bundle.sh b/scripts/test-maven-central-bundle.sh
new file mode 100644
index 0000000000..fe83da8cb9
--- /dev/null
+++ b/scripts/test-maven-central-bundle.sh
@@ -0,0 +1,211 @@
+#!/usr/bin/env bash
+
+#
+# This file is part of JavaSMT,
+# an API wrapper for a collection of SMT solvers:
+# https://github.com/sosy-lab/java-smt
+#
+# SPDX-FileCopyrightText: 2026 Dirk Beyer
+#
+# SPDX-License-Identifier: Apache-2.0
+#
+
+set -e
+
+# Colors
+RED='\033[0;31m'
+GREEN='\033[0;32m'
+YELLOW='\033[1;33m'
+BLUE='\033[0;34m'
+NC='\033[0m' # No Color
+
+# Extensions to check for each base file
+EXTENSIONS=("" ".asc" ".md5" ".sha1" ".sha256" ".sha512")
+
+# Ensure script is run from project root
+if [[ ! -f "build.xml" ]]; then
+ echo -e "${RED}Error: This script must be run from the project root.${NC}"
+ exit 1
+fi
+
+verify_bundle() {
+ local COMPONENT=$1
+ local VERSION=$2
+ local FULL_NAME=$3
+ local EXPECTED_DEP_STATUS=$4 # "none", "compile", or "compile+optional"
+ shift 4
+ local BASE_FILES=("$@")
+
+ local REL_DIR="org/sosy-lab/${FULL_NAME}/${VERSION}"
+ local ZIP_FILE="dist/maven-central-bundle/${COMPONENT}-${VERSION}-bundle.zip"
+ local TEMP_DIR=$(mktemp -d)
+ local POM_FILE="${TEMP_DIR}/${REL_DIR}/${FULL_NAME}-${VERSION}.pom"
+
+ echo -e "${BLUE}------------------------------------------------------------${NC}"
+ echo -e "${YELLOW}Testing component: ${COMPONENT} (version: ${VERSION})${NC}"
+ echo -e "${BLUE}------------------------------------------------------------${NC}"
+
+ # Cleanup local bundle dir for this component if it exists
+ rm -rf "dist/maven-central-bundle/${REL_DIR}"
+
+ # Execute ant command
+ echo -e "${BLUE}Executing ant publish-to-maven-central...${NC}"
+ ant publish-to-maven-central -Dpublish.component="${COMPONENT}" -Dpublish.version="${VERSION}" -Dpublish.upload=false
+ echo -e "${BLUE}------------------------------------------------------------${NC}"
+
+ # Check if zip file exists
+ if [[ ! -f "${ZIP_FILE}" ]]; then
+ echo -e "${RED}Error: Zip file ${ZIP_FILE} was not created.${NC}"
+ exit 1
+ fi
+
+ # Unzip to temp directory
+ echo -e "${BLUE}Unzipping bundle for verification...${NC}"
+ unzip -q "${ZIP_FILE}" -d "${TEMP_DIR}"
+
+ # Verify file structure
+ echo -e "${BLUE}Verifying file structure in the zip bundle...${NC}"
+
+ local EXPECTED_FILES_FILE="${TEMP_DIR}/expected_files.txt"
+ local ACTUAL_FILES_FILE="${TEMP_DIR}/actual_files.txt"
+
+ # Generate expected files list
+ for base in "${BASE_FILES[@]}"; do
+ for ext in "${EXTENSIONS[@]}"; do
+ echo "${REL_DIR}/${base}${ext}" >> "${EXPECTED_FILES_FILE}"
+ done
+ done
+ sort -o "${EXPECTED_FILES_FILE}" "${EXPECTED_FILES_FILE}"
+
+ # Generate actual files list
+ find "${TEMP_DIR}/${REL_DIR}" -type f | sed "s|^${TEMP_DIR}/||" | sort > "${ACTUAL_FILES_FILE}"
+
+ # Compare lists
+ local DIFF=$(diff -u "${EXPECTED_FILES_FILE}" "${ACTUAL_FILES_FILE}" || true)
+
+ local FAILED=0
+ if [[ -n "${DIFF}" ]]; then
+ echo -e "${RED}Verification failed for ${COMPONENT}!${NC}"
+ echo "Differences found:"
+ echo "${DIFF}"
+ FAILED=1
+ fi
+
+ # Verify POM content (dependencies)
+ echo -e "${BLUE}Verifying POM content (dependencies) for ${COMPONENT}...${NC}"
+ if [[ "$EXPECTED_DEP_STATUS" == "none" ]]; then
+ if grep -q "" "$POM_FILE"; then
+ echo -e "${RED}Error: POM for ${COMPONENT} should not have dependencies.${NC}"
+ FAILED=1
+ fi
+ elif [[ "$EXPECTED_DEP_STATUS" == "compile" ]]; then
+ if ! grep -q "compile" "$POM_FILE"; then
+ echo -e "${RED}Error: POM for ${COMPONENT} should have compile dependencies.${NC}"
+ FAILED=1
+ fi
+ if grep -q "true" "$POM_FILE"; then
+ echo -e "${RED}Error: POM for ${COMPONENT} should not have optional dependencies.${NC}"
+ FAILED=1
+ fi
+ elif [[ "$EXPECTED_DEP_STATUS" == "compile+optional" ]]; then
+ if ! grep -q "compile" "$POM_FILE"; then
+ echo -e "${RED}Error: POM for ${COMPONENT} should have compile dependencies.${NC}"
+ FAILED=1
+ fi
+ if ! grep -q "true" "$POM_FILE"; then
+ echo -e "${RED}Error: POM for ${COMPONENT} should have optional dependencies.${NC}"
+ FAILED=1
+ fi
+ fi
+
+ rm -rf "${TEMP_DIR}"
+ if [[ $FAILED -eq 0 ]]; then
+ echo -e "${GREEN}Verification successful for ${COMPONENT}!${NC}"
+ return 0
+ else
+ return 1
+ fi
+}
+
+# Cleanup all bundles before starting
+echo -e "${YELLOW}Cleaning up dist/ directory...${NC}"
+rm -rf dist/maven-central-bundle
+
+FAILED_TESTS=0
+
+# Test case: Z3
+Z3_VERSION="4.16.0"
+Z3_FULL_NAME="javasmt-solver-z3"
+Z3_BASE_FILES=(
+ "${Z3_FULL_NAME}-${Z3_VERSION}.jar"
+ "${Z3_FULL_NAME}-${Z3_VERSION}.pom"
+ "${Z3_FULL_NAME}-${Z3_VERSION}-javadoc.jar"
+ "${Z3_FULL_NAME}-${Z3_VERSION}-sources.jar"
+ "${Z3_FULL_NAME}-${Z3_VERSION}-libz3-arm64.dll"
+ "${Z3_FULL_NAME}-${Z3_VERSION}-libz3-arm64.dylib"
+ "${Z3_FULL_NAME}-${Z3_VERSION}-libz3-arm64.so"
+ "${Z3_FULL_NAME}-${Z3_VERSION}-libz3-x64.dll"
+ "${Z3_FULL_NAME}-${Z3_VERSION}-libz3-x64.dylib"
+ "${Z3_FULL_NAME}-${Z3_VERSION}-libz3-x64.so"
+ "${Z3_FULL_NAME}-${Z3_VERSION}-libz3java-arm64.dll"
+ "${Z3_FULL_NAME}-${Z3_VERSION}-libz3java-arm64.dylib"
+ "${Z3_FULL_NAME}-${Z3_VERSION}-libz3java-arm64.so"
+ "${Z3_FULL_NAME}-${Z3_VERSION}-libz3java-x64.dll"
+ "${Z3_FULL_NAME}-${Z3_VERSION}-libz3java-x64.dylib"
+ "${Z3_FULL_NAME}-${Z3_VERSION}-libz3java-x64.so"
+)
+
+if ! verify_bundle "javasmt-solver-z3" "${Z3_VERSION}" "${Z3_FULL_NAME}" "none" "${Z3_BASE_FILES[@]}"; then
+ FAILED_TESTS=$((FAILED_TESTS + 1))
+fi
+
+# Test case: MathSAT
+MATHSAT_VERSION="5.6.10"
+MATHSAT_FULL_NAME="javasmt-solver-mathsat"
+MATHSAT_BASE_FILES=(
+ "${MATHSAT_FULL_NAME}-${MATHSAT_VERSION}-libmathsat5j.so"
+ "${MATHSAT_FULL_NAME}-${MATHSAT_VERSION}-mathsat.dll"
+ "${MATHSAT_FULL_NAME}-${MATHSAT_VERSION}-mathsat5j.dll"
+ "${MATHSAT_FULL_NAME}-${MATHSAT_VERSION}-mpir.dll"
+ "${MATHSAT_FULL_NAME}-${MATHSAT_VERSION}.pom"
+)
+
+if ! verify_bundle "javasmt-solver-mathsat" "${MATHSAT_VERSION}" "${MATHSAT_FULL_NAME}" "none" "${MATHSAT_BASE_FILES[@]}"; then
+ FAILED_TESTS=$((FAILED_TESTS + 1))
+fi
+
+# Test case: JavaSMT-bindings for Yices2
+YICES_VERSION="6.0.0-141-g04134287c"
+YICES_FULL_NAME="javasmt-yices2"
+YICES_BASE_FILES=(
+ "${YICES_FULL_NAME}-${YICES_VERSION}.jar"
+ "${YICES_FULL_NAME}-${YICES_VERSION}.pom"
+ "${YICES_FULL_NAME}-${YICES_VERSION}-sources.jar"
+)
+
+if ! verify_bundle "javasmt-yices2" "${YICES_VERSION}" "${YICES_FULL_NAME}" "compile+optional" "${YICES_BASE_FILES[@]}"; then
+ FAILED_TESTS=$((FAILED_TESTS + 1))
+fi
+
+# Test case: JavaSMT (Core)
+JAVASMT_VERSION="6.0.0"
+JAVASMT_FULL_NAME="java-smt"
+JAVASMT_BASE_FILES=(
+ "${JAVASMT_FULL_NAME}-${JAVASMT_VERSION}.jar"
+ "${JAVASMT_FULL_NAME}-${JAVASMT_VERSION}.pom"
+ "${JAVASMT_FULL_NAME}-${JAVASMT_VERSION}-sources.jar"
+ "${JAVASMT_FULL_NAME}-${JAVASMT_VERSION}-javadoc.jar"
+)
+
+if ! verify_bundle "java-smt" "${JAVASMT_VERSION}" "${JAVASMT_FULL_NAME}" "compile+optional" "${JAVASMT_BASE_FILES[@]}"; then
+ FAILED_TESTS=$((FAILED_TESTS + 1))
+fi
+
+echo -e "${BLUE}------------------------------------------------------------${NC}"
+if [[ $FAILED_TESTS -eq 0 ]]; then
+ echo -e "${GREEN}All tests passed successfully!${NC}"
+ exit 0
+else
+ echo -e "${RED}$FAILED_TESTS test(s) failed!${NC}"
+ exit 1
+fi
diff --git a/solvers_maven_conf/maven_bitwuzla_pom_template.xml b/solvers_maven_conf/maven_bitwuzla_pom_template.xml
index 76ee8bc440..a9fb7301f5 100644
--- a/solvers_maven_conf/maven_bitwuzla_pom_template.xml
+++ b/solvers_maven_conf/maven_bitwuzla_pom_template.xml
@@ -6,7 +6,7 @@ This file is part of JavaSMT,
an API wrapper for a collection of SMT solvers:
https://github.com/sosy-lab/java-smt
-SPDX-FileCopyrightText: 2024 Dirk Beyer
+SPDX-FileCopyrightText: 2026 Dirk Beyer
SPDX-License-Identifier: Apache-2.0
-->
diff --git a/solvers_maven_conf/maven_boolector_pom_template.xml b/solvers_maven_conf/maven_boolector_pom_template.xml
index 4612f68a79..f8e12c6509 100644
--- a/solvers_maven_conf/maven_boolector_pom_template.xml
+++ b/solvers_maven_conf/maven_boolector_pom_template.xml
@@ -6,7 +6,7 @@ This file is part of JavaSMT,
an API wrapper for a collection of SMT solvers:
https://github.com/sosy-lab/java-smt
-SPDX-FileCopyrightText: 2021 Dirk Beyer
+SPDX-FileCopyrightText: 2026 Dirk Beyer
SPDX-License-Identifier: Apache-2.0
-->
diff --git a/solvers_maven_conf/maven_cvc4_pom_template.xml b/solvers_maven_conf/maven_cvc4_pom_template.xml
index 0a37bd83a2..771cd4e451 100644
--- a/solvers_maven_conf/maven_cvc4_pom_template.xml
+++ b/solvers_maven_conf/maven_cvc4_pom_template.xml
@@ -6,7 +6,7 @@ This file is part of JavaSMT,
an API wrapper for a collection of SMT solvers:
https://github.com/sosy-lab/java-smt
-SPDX-FileCopyrightText: 2021 Dirk Beyer
+SPDX-FileCopyrightText: 2026 Dirk Beyer
SPDX-License-Identifier: Apache-2.0
-->
@@ -14,7 +14,7 @@ SPDX-License-Identifier: Apache-2.0
4.0.0
org.sosy-lab
javasmt-solver-cvc4
- pom
+ jar
javasmt-solver-cvc4
${stage.revision}
SMT solver CVC4 for use in JavaSMT
diff --git a/solvers_maven_conf/maven_cvc5_pom_template.xml b/solvers_maven_conf/maven_cvc5_pom_template.xml
index 5ef05c1d8f..8c6dfa81c8 100644
--- a/solvers_maven_conf/maven_cvc5_pom_template.xml
+++ b/solvers_maven_conf/maven_cvc5_pom_template.xml
@@ -6,7 +6,7 @@ This file is part of JavaSMT,
an API wrapper for a collection of SMT solvers:
https://github.com/sosy-lab/java-smt
-SPDX-FileCopyrightText: 2021 Dirk Beyer
+SPDX-FileCopyrightText: 2026 Dirk Beyer
SPDX-License-Identifier: Apache-2.0
-->
@@ -14,7 +14,7 @@ SPDX-License-Identifier: Apache-2.0
4.0.0
org.sosy-lab
javasmt-solver-cvc5
- pom
+ jar
javasmt-solver-cvc5
${stage.revision}
SMT solver CVC5 for use in JavaSMT
diff --git a/solvers_maven_conf/maven_javasmt_yices2_pom_template.xml b/solvers_maven_conf/maven_javasmt-yices2_pom_template.xml
similarity index 95%
rename from solvers_maven_conf/maven_javasmt_yices2_pom_template.xml
rename to solvers_maven_conf/maven_javasmt-yices2_pom_template.xml
index 881f2fbef5..72d77aeb0c 100644
--- a/solvers_maven_conf/maven_javasmt_yices2_pom_template.xml
+++ b/solvers_maven_conf/maven_javasmt-yices2_pom_template.xml
@@ -6,7 +6,7 @@ This file is part of JavaSMT,
an API wrapper for a collection of SMT solvers:
https://github.com/sosy-lab/java-smt
-SPDX-FileCopyrightText: 2021 Dirk Beyer
+SPDX-FileCopyrightText: 2026 Dirk Beyer
SPDX-License-Identifier: Apache-2.0
-->
@@ -14,7 +14,7 @@ SPDX-License-Identifier: Apache-2.0
4.0.0
org.sosy-lab
javasmt-yices2
- pom
+ jar
javasmt-yices2
${stage.revision}
JavaSMT bindings for the SMT solver Yices
diff --git a/solvers_maven_conf/maven_mathsat_pom_template.xml b/solvers_maven_conf/maven_mathsat_pom_template.xml
index 6b840e4a2f..4185ff59a0 100644
--- a/solvers_maven_conf/maven_mathsat_pom_template.xml
+++ b/solvers_maven_conf/maven_mathsat_pom_template.xml
@@ -6,16 +6,16 @@ This file is part of JavaSMT,
an API wrapper for a collection of SMT solvers:
https://github.com/sosy-lab/java-smt
-SPDX-FileCopyrightText: 2025 Dirk Beyer
+SPDX-FileCopyrightText: 2026 Dirk Beyer
SPDX-License-Identifier: Apache-2.0
-->
4.0.0
org.sosy-lab
- javasmt-solver-mathsat5
+ javasmt-solver-mathsat
pom
- javasmt-solver-mathsat5
+ javasmt-solver-mathsat
${stage.revision}
Recompiled Version of the SMT solver Mathsat5 for use in JavaSMT
https://github.com/sosy-lab/java-smt
@@ -27,7 +27,7 @@ SPDX-License-Identifier: Apache-2.0
- MathSAT5 is copyrighted 2009-2020 by Fondazione Bruno Kessler, Trento, Italy,
+ MathSAT5 is copyrighted 2009-2026 by Fondazione Bruno Kessler, Trento, Italy,
University of Trento, Italy, and others. All rights reserved.
MathSAT5 is available for research and evaluation purposes only.
diff --git a/solvers_maven_conf/maven_opensmt_pom_template.xml b/solvers_maven_conf/maven_opensmt_pom_template.xml
index c712f68c43..1288926d18 100644
--- a/solvers_maven_conf/maven_opensmt_pom_template.xml
+++ b/solvers_maven_conf/maven_opensmt_pom_template.xml
@@ -6,7 +6,7 @@ This file is part of JavaSMT,
an API wrapper for a collection of SMT solvers:
https://github.com/sosy-lab/java-smt
-SPDX-FileCopyrightText: 2021 Dirk Beyer
+SPDX-FileCopyrightText: 2026 Dirk Beyer
SPDX-License-Identifier: Apache-2.0
-->
diff --git a/solvers_maven_conf/maven_yices2_pom_template.xml b/solvers_maven_conf/maven_yices2_pom_template.xml
index 5f5798694a..92a379b5be 100644
--- a/solvers_maven_conf/maven_yices2_pom_template.xml
+++ b/solvers_maven_conf/maven_yices2_pom_template.xml
@@ -6,7 +6,7 @@ This file is part of JavaSMT,
an API wrapper for a collection of SMT solvers:
https://github.com/sosy-lab/java-smt
-SPDX-FileCopyrightText: 2021 Dirk Beyer
+SPDX-FileCopyrightText: 2026 Dirk Beyer
SPDX-License-Identifier: Apache-2.0
-->
@@ -14,7 +14,7 @@ SPDX-License-Identifier: Apache-2.0
4.0.0
org.sosy-lab
javasmt-solver-yices2
- pom
+ jar
javasmt-solver-yices2
${stage.revision}
SMT solver Yices for use in JavaSMT
diff --git a/solvers_maven_conf/maven_z3-legacy_pom_template.xml b/solvers_maven_conf/maven_z3-legacy_pom_template.xml
new file mode 100644
index 0000000000..2cdc619fef
--- /dev/null
+++ b/solvers_maven_conf/maven_z3-legacy_pom_template.xml
@@ -0,0 +1,63 @@
+
+
+
+
+ 4.0.0
+ org.sosy-lab
+ javasmt-solver-z3-legacy
+ pom
+ javasmt-solver-z3
+ ${stage.revision}
+ SMT solver Z3 (legacy version with interpolation) for use in JavaSMT
+ https://github.com/sosy-lab/java-smt
+
+
+
+ MIT License
+ https://opensource.org/licenses/MIT
+
+
+
+
+ Software Systems Lab
+ https://www.sosy-lab.org/
+
+
+
+ https://github.com/sosy-lab/java-smt/
+ scm:git:git://github.com/sosy-lab/java-smt.git
+ scm:git:git@github.com:sosy-lab/java-smt.git
+
+
+
+
+ Karlheinz Friedberger
+ kfriedberger@gmail.com
+ Software Systems Lab
+ https://www.sosy-lab.org/people/friedberger/
+
+ project maintainer
+
+
+
+ Dirk Beyer
+ dirk.beyer@sosy-lab.org
+ https://www.sosy-lab.org/people/beyer/
+ Software Systems Lab
+ http://www.sosy-lab.org/
+
+ project manager
+
+
+
+
+
diff --git a/solvers_maven_conf/maven_z3_pom_template.xml b/solvers_maven_conf/maven_z3_pom_template.xml
index 079e44714f..4c5116e038 100644
--- a/solvers_maven_conf/maven_z3_pom_template.xml
+++ b/solvers_maven_conf/maven_z3_pom_template.xml
@@ -6,7 +6,7 @@ This file is part of JavaSMT,
an API wrapper for a collection of SMT solvers:
https://github.com/sosy-lab/java-smt
-SPDX-FileCopyrightText: 2021 Dirk Beyer
+SPDX-FileCopyrightText: 2026 Dirk Beyer
SPDX-License-Identifier: Apache-2.0
-->