diff --git a/doc/Example-Ivy-Project/README.md b/doc/Example-Ivy-Project/README.md
new file mode 100644
index 0000000000..6d94b06f17
--- /dev/null
+++ b/doc/Example-Ivy-Project/README.md
@@ -0,0 +1,23 @@
+<!--
+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 <https://www.sosy-lab.org>
+
+SPDX-License-Identifier: Apache-2.0
+-->
+
+This is an example application for using JavaSMT with Ant/Ivy.
+The example application prints a table of the available SMT solvers, along with their version
+number.
+
+The project supports the following build steps:
+
+- `resolve` retrieve dependencies with Ivy
+- `compile` compile the project
+- `package` build a .jar
+- `run` run the program
+- `clean` clean the project
+
+Calling `ant` with no target will build and then execute the project.
\ No newline at end of file
diff --git a/doc/Example-Ivy-Project/build.xml b/doc/Example-Ivy-Project/build.xml
new file mode 100644
index 0000000000..b315efc27a
--- /dev/null
+++ b/doc/Example-Ivy-Project/build.xml
@@ -0,0 +1,97 @@
+<!--
+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 <https://www.sosy-lab.org>
+
+SPDX-License-Identifier: Apache-2.0
+-->
+
+<project xmlns:ivy="antlib:org.apache.ivy.ant" name="javasmt-ivy-example" default="run">
+    <!-- Organization and module name for the project -->
+    <property name="project.organization" value="org.sosy_lab.java_smt_example"/>
+    <property name="project.module" value="${ant.project.name}"/>
+    <property name="project.jar" value="${project.module}.jar"/>
+
+    <!-- Path to the "main" function -->
+    <property name="project.main" value="example.Main"/>
+
+    <target name="download-ivy" unless="skip.download">
+        <mkdir dir="lib"/>
+        <get src="https://repo1.maven.org/maven2/org/apache/ivy/ivy/2.5.0/ivy-2.5.0.jar"
+             dest="lib/ivy.jar" usetimestamp="true"/>
+    </target>
+
+    <target name="init-ivy" depends="download-ivy">
+        <path id="ivy.path">
+            <fileset dir="lib" includes="*.jar"/>
+        </path>
+        <taskdef resource="org/apache/ivy/ant/antlib.xml" uri="antlib:org.apache.ivy.ant" classpathref="ivy.path"/>
+        <ivy:settings file="lib/ivy-settings.xml"/>
+    </target>
+
+    <target name="resolve" depends="init-ivy" description="--> retrieve dependencies with Ivy">
+        <ivy:resolve log="download-only"/>
+        <ivy:retrieve pattern="lib/java/[conf]/([arch]/)[artifact](-[classifier]).[ext]"/>
+    </target>
+
+    <target name="install" depends="resolve">
+        <mkdir dir="lib/native/x86_64-windows"/>
+        <copy todir="lib/native/x86_64-windows">
+            <fileset dir="lib/java/default/x64">
+                <include name="*.dll"/>
+            </fileset>
+        </copy>
+        <mkdir dir="lib/native/arm64-windows"/>
+        <copy todir="lib/native/arm64-windows">
+            <fileset dir="lib/java/default/arm64">
+                <include name="*.dll"/>
+            </fileset>
+        </copy>
+    </target>
+
+    <target name="compile" depends="install" description="--> compile the project">
+        <mkdir dir="build"/>
+        <path id="classpath.build">
+            <pathelement location="build"/>
+            <fileset dir="lib/java" includes="**/*.jar"/>
+        </path>
+        <javac srcdir="src" destdir="build" classpathref="classpath.build"/>
+    </target>
+
+    <target name="package" depends="compile" description="--> build a .jar">
+        <manifestclasspath property="classpath.jar" jarfile="${project.jar}">
+            <classpath>
+                <fileset dir="lib/java/default" includes="*.jar"/>
+            </classpath>
+        </manifestclasspath>
+        <jar basedir="build"
+             destfile="${project.jar}"
+             includes="**"
+             whenmanifestonly="fail">
+            <manifest>
+                <attribute name="Class-Path" value="${classpath.jar}"/>
+                <attribute name="Main-Class" value="${project.main}"/>
+            </manifest>
+        </jar>
+    </target>
+
+    <target name="run" depends="package" description="--> run the program">
+        <java jar="${project.jar}" fork="true"/>
+    </target>
+
+    <target name="clean" description="--> clean the project">
+        <delete includeemptydirs="true" quiet="true">
+            <fileset dir=".">
+                <include name="build/**"/>
+                <include name="lib/ivy.jar"/>
+                <include name="lib/java/**"/>
+                <include name="lib/native/x86_64-windows/**"/>
+                <include name="lib/native/arm64-windows/**"/>
+                <include name="${project.jar}"/>
+            </fileset>
+            <fileset dir="lib/java"/>
+        </delete>
+    </target>
+</project>
diff --git a/doc/Example-Ivy-Project/ivy.xml b/doc/Example-Ivy-Project/ivy.xml
new file mode 100644
index 0000000000..bdbe362cef
--- /dev/null
+++ b/doc/Example-Ivy-Project/ivy.xml
@@ -0,0 +1,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 <https://www.sosy-lab.org>
+
+SPDX-License-Identifier: Apache-2.0
+-->
+
+<ivy-module version="2.0">
+    <info organisation="${project.organization}" module="${project.module}"/>
+    <dependencies>
+        <dependency org="org.sosy_lab" name="java-smt" rev="5.0.1-362-g3846f26ca" conf="default->runtime-x64,runtime-arm64"/>
+    </dependencies>
+</ivy-module>
diff --git a/doc/Example-Ivy-Project/lib/ivy-settings.xml b/doc/Example-Ivy-Project/lib/ivy-settings.xml
new file mode 100644
index 0000000000..1da8869609
--- /dev/null
+++ b/doc/Example-Ivy-Project/lib/ivy-settings.xml
@@ -0,0 +1,25 @@
+<?xml version="1.0" encoding="UTF-8"?>
+
+<!--
+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 <https://www.sosy-lab.org>
+
+SPDX-License-Identifier: Apache-2.0
+-->
+
+<ivysettings>
+    <settings defaultResolver="Sosy-Lab"/>
+    <property name="ivy.repo.url" value="https://www.sosy-lab.org/ivy"/>
+    <resolvers>
+        <url name="Sosy-Lab" descriptor="required">
+            <ivy pattern="${ivy.repo.url}/[organisation]/[module]/ivy-[revision].xml"/>
+            <artifact pattern="${ivy.repo.url}/[organisation]/[module]/([arch]/)[artifact]-[revision](-[classifier]).[ext]"/>
+        </url>
+    </resolvers>
+
+    <caches defaultCacheDir="${user.home}/.ivy2/cache"
+            artifactPattern="[organisation]/[module]/[type]s/([arch]/)[artifact]-[revision](-[classifier]).[ext]"/>
+</ivysettings>
diff --git a/doc/Example-Ivy-Project/lib/native/arm64-linux/libbitwuzlaj.so b/doc/Example-Ivy-Project/lib/native/arm64-linux/libbitwuzlaj.so
new file mode 120000
index 0000000000..372f592128
--- /dev/null
+++ b/doc/Example-Ivy-Project/lib/native/arm64-linux/libbitwuzlaj.so
@@ -0,0 +1 @@
+../../java/default/arm64/libbitwuzlaj.so
\ No newline at end of file
diff --git a/doc/Example-Ivy-Project/lib/native/arm64-linux/libmathsat5j.so b/doc/Example-Ivy-Project/lib/native/arm64-linux/libmathsat5j.so
new file mode 120000
index 0000000000..c7eaf57210
--- /dev/null
+++ b/doc/Example-Ivy-Project/lib/native/arm64-linux/libmathsat5j.so
@@ -0,0 +1 @@
+../../java/default/arm64/libmathsat5j.so
\ No newline at end of file
diff --git a/doc/Example-Ivy-Project/lib/native/arm64-linux/libopensmtj.so b/doc/Example-Ivy-Project/lib/native/arm64-linux/libopensmtj.so
new file mode 120000
index 0000000000..8aadd048bf
--- /dev/null
+++ b/doc/Example-Ivy-Project/lib/native/arm64-linux/libopensmtj.so
@@ -0,0 +1 @@
+../../java/default/arm64/libopensmtj.so
\ No newline at end of file
diff --git a/doc/Example-Ivy-Project/lib/native/arm64-linux/libz3.so b/doc/Example-Ivy-Project/lib/native/arm64-linux/libz3.so
new file mode 120000
index 0000000000..7252d0c3c0
--- /dev/null
+++ b/doc/Example-Ivy-Project/lib/native/arm64-linux/libz3.so
@@ -0,0 +1 @@
+../../java/default/arm64/libz3.so
\ No newline at end of file
diff --git a/doc/Example-Ivy-Project/lib/native/arm64-linux/libz3java.so b/doc/Example-Ivy-Project/lib/native/arm64-linux/libz3java.so
new file mode 120000
index 0000000000..934e062ea2
--- /dev/null
+++ b/doc/Example-Ivy-Project/lib/native/arm64-linux/libz3java.so
@@ -0,0 +1 @@
+../../java/default/arm64/libz3java.so
\ No newline at end of file
diff --git a/doc/Example-Ivy-Project/lib/native/arm64-macosx/libz3.dylib b/doc/Example-Ivy-Project/lib/native/arm64-macosx/libz3.dylib
new file mode 120000
index 0000000000..590d25fa37
--- /dev/null
+++ b/doc/Example-Ivy-Project/lib/native/arm64-macosx/libz3.dylib
@@ -0,0 +1 @@
+../../java/default/arm64/libz3.dylib
\ No newline at end of file
diff --git a/doc/Example-Ivy-Project/lib/native/arm64-macosx/libz3java.dylib b/doc/Example-Ivy-Project/lib/native/arm64-macosx/libz3java.dylib
new file mode 120000
index 0000000000..397941ff52
--- /dev/null
+++ b/doc/Example-Ivy-Project/lib/native/arm64-macosx/libz3java.dylib
@@ -0,0 +1 @@
+../../java/default/arm64/libz3java.dylib
\ No newline at end of file
diff --git a/doc/Example-Ivy-Project/lib/native/x86_64-linux/libbitwuzlaj.so b/doc/Example-Ivy-Project/lib/native/x86_64-linux/libbitwuzlaj.so
new file mode 120000
index 0000000000..ef45bf4c23
--- /dev/null
+++ b/doc/Example-Ivy-Project/lib/native/x86_64-linux/libbitwuzlaj.so
@@ -0,0 +1 @@
+../../java/default/x64/libbitwuzlaj.so
\ No newline at end of file
diff --git a/doc/Example-Ivy-Project/lib/native/x86_64-linux/libmathsat5j.so b/doc/Example-Ivy-Project/lib/native/x86_64-linux/libmathsat5j.so
new file mode 120000
index 0000000000..c734ccd975
--- /dev/null
+++ b/doc/Example-Ivy-Project/lib/native/x86_64-linux/libmathsat5j.so
@@ -0,0 +1 @@
+../../java/default/x64/libmathsat5j.so
\ No newline at end of file
diff --git a/doc/Example-Ivy-Project/lib/native/x86_64-linux/libopensmtj.so b/doc/Example-Ivy-Project/lib/native/x86_64-linux/libopensmtj.so
new file mode 120000
index 0000000000..e613c908c0
--- /dev/null
+++ b/doc/Example-Ivy-Project/lib/native/x86_64-linux/libopensmtj.so
@@ -0,0 +1 @@
+../../java/default/x64/libopensmtj.so
\ No newline at end of file
diff --git a/doc/Example-Ivy-Project/lib/native/x86_64-linux/libz3.so b/doc/Example-Ivy-Project/lib/native/x86_64-linux/libz3.so
new file mode 120000
index 0000000000..e2423e093d
--- /dev/null
+++ b/doc/Example-Ivy-Project/lib/native/x86_64-linux/libz3.so
@@ -0,0 +1 @@
+../../java/default/x64/libz3.so
\ No newline at end of file
diff --git a/doc/Example-Ivy-Project/lib/native/x86_64-linux/libz3java.so b/doc/Example-Ivy-Project/lib/native/x86_64-linux/libz3java.so
new file mode 120000
index 0000000000..392351c46a
--- /dev/null
+++ b/doc/Example-Ivy-Project/lib/native/x86_64-linux/libz3java.so
@@ -0,0 +1 @@
+../../java/default/x64/libz3java.so
\ No newline at end of file
diff --git a/doc/Example-Ivy-Project/lib/native/x86_64-macosx/libz3.dylib b/doc/Example-Ivy-Project/lib/native/x86_64-macosx/libz3.dylib
new file mode 120000
index 0000000000..898516499b
--- /dev/null
+++ b/doc/Example-Ivy-Project/lib/native/x86_64-macosx/libz3.dylib
@@ -0,0 +1 @@
+../../java/default/x64/libz3.dylib
\ No newline at end of file
diff --git a/doc/Example-Ivy-Project/lib/native/x86_64-macosx/libz3java.dylib b/doc/Example-Ivy-Project/lib/native/x86_64-macosx/libz3java.dylib
new file mode 120000
index 0000000000..1c865209db
--- /dev/null
+++ b/doc/Example-Ivy-Project/lib/native/x86_64-macosx/libz3java.dylib
@@ -0,0 +1 @@
+../../java/default/x64/libz3java.dylib
\ No newline at end of file
diff --git a/doc/Example-Ivy-Project/src/example/Main.java b/doc/Example-Ivy-Project/src/example/Main.java
new file mode 100644
index 0000000000..4a6298c944
--- /dev/null
+++ b/doc/Example-Ivy-Project/src/example/Main.java
@@ -0,0 +1,34 @@
+// 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 <https://www.sosy-lab.org>
+//
+// SPDX-License-Identifier: Apache-2.0
+
+package example;
+
+import org.sosy_lab.common.ShutdownNotifier;
+import org.sosy_lab.common.configuration.Configuration;
+import org.sosy_lab.common.configuration.InvalidConfigurationException;
+import org.sosy_lab.common.log.LogManager;
+import org.sosy_lab.java_smt.SolverContextFactory;
+import org.sosy_lab.java_smt.SolverContextFactory.Solvers;
+import org.sosy_lab.java_smt.api.SolverContext;
+
+public class Main {
+  public static void main(String[] args) {
+    Configuration config = Configuration.defaultConfiguration();
+    LogManager logger = LogManager.createNullLogManager();
+    ShutdownNotifier notifier = ShutdownNotifier.createDummy();
+
+    for (Solvers solver : Solvers.values()) {
+      try (SolverContext context =
+          SolverContextFactory.createSolverContext(config, logger, notifier, solver)) {
+        System.out.println(solver + ", " + context.getVersion());
+      } catch (InvalidConfigurationException e) {
+        System.out.println(solver + " not available");
+      }
+    }
+  }
+}