From 8a61e0e405fbd9f7a3778925274209bcc9a24fcf Mon Sep 17 00:00:00 2001
From: Daniel Raffler <daniel-raffler@gmx.de>
Date: Sun, 29 Mar 2026 12:34:42 +0200
Subject: [PATCH 01/23] Intellij: Switch to Jdk17 in the project file

---
 .idea/JavaSMT.iml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.idea/JavaSMT.iml b/.idea/JavaSMT.iml
index 47bdfebbd0..787850f16f 100644
--- a/.idea/JavaSMT.iml
+++ b/.idea/JavaSMT.iml
@@ -22,7 +22,7 @@ SPDX-License-Identifier: Apache-2.0
       <excludeFolder url="file://$MODULE_DIR$/junit" />
       <excludeFolder url="file://$MODULE_DIR$/repository" />
     </content>
-    <orderEntry type="jdk" jdkName="11" jdkType="JavaSDK" />
+    <orderEntry type="jdk" jdkName="17" jdkType="JavaSDK" />
     <orderEntry type="sourceFolder" forTests="false" />
     <orderEntry type="module-library">
       <library>

From 6ff559d515a77562f10d5c489c7f86b7622ddf8a Mon Sep 17 00:00:00 2001
From: Daniel Raffler <daniel-raffler@gmx.de>
Date: Sun, 29 Mar 2026 12:37:04 +0200
Subject: [PATCH 02/23] Intellij: Add new `Nullable` managers to the
 configuration

---
 .idea/misc.xml | 43 +++++++++++++++++++++++++------------------
 1 file changed, 25 insertions(+), 18 deletions(-)

diff --git a/.idea/misc.xml b/.idea/misc.xml
index 79d44e380e..616a44460c 100644
--- a/.idea/misc.xml
+++ b/.idea/misc.xml
@@ -17,36 +17,43 @@ SPDX-License-Identifier: Apache-2.0
   <component name="NullableNotNullManager">
     <option name="myDefaultNullable" value="javax.annotation.Nullable" />
     <option name="myDefaultNotNull" value="javax.annotation.Nonnull" />
+    <option name="myOrdered" value="true" />
     <option name="myNullables">
       <value>
-        <list size="11">
-          <item index="0" class="java.lang.String" itemvalue="org.jetbrains.annotations.Nullable" />
-          <item index="1" class="java.lang.String" itemvalue="javax.annotation.Nullable" />
-          <item index="2" class="java.lang.String" itemvalue="edu.umd.cs.findbugs.annotations.Nullable" />
-          <item index="3" class="java.lang.String" itemvalue="android.support.annotation.Nullable" />
-          <item index="4" class="java.lang.String" itemvalue="javax.annotation.CheckForNull" />
+        <list size="14">
+          <item index="0" class="java.lang.String" itemvalue="org.checkerframework.checker.nullness.qual.Nullable" />
+          <item index="1" class="java.lang.String" itemvalue="org.checkerframework.checker.nullness.compatqual.NullableDecl" />
+          <item index="2" class="java.lang.String" itemvalue="org.checkerframework.checker.nullness.compatqual.NullableType" />
+          <item index="3" class="java.lang.String" itemvalue="javax.annotation.Nullable" />
+          <item index="4" class="java.lang.String" itemvalue="android.support.annotation.Nullable" />
           <item index="5" class="java.lang.String" itemvalue="androidx.annotation.Nullable" />
           <item index="6" class="java.lang.String" itemvalue="androidx.annotation.RecentlyNullable" />
-          <item index="7" class="java.lang.String" itemvalue="org.checkerframework.checker.nullness.qual.Nullable" />
-          <item index="8" class="java.lang.String" itemvalue="org.checkerframework.checker.nullness.compatqual.NullableDecl" />
-          <item index="9" class="java.lang.String" itemvalue="org.checkerframework.checker.nullness.compatqual.NullableType" />
-          <item index="10" class="java.lang.String" itemvalue="com.android.annotations.Nullable" />
+          <item index="7" class="java.lang.String" itemvalue="com.android.annotations.Nullable" />
+          <item index="8" class="java.lang.String" itemvalue="org.jspecify.annotations.Nullable" />
+          <item index="9" class="java.lang.String" itemvalue="org.jetbrains.annotations.Nullable" />
+          <item index="10" class="java.lang.String" itemvalue="org.eclipse.jdt.annotation.Nullable" />
+          <item index="11" class="java.lang.String" itemvalue="edu.umd.cs.findbugs.annotations.Nullable" />
+          <item index="12" class="java.lang.String" itemvalue="jakarta.annotation.Nullable" />
+          <item index="13" class="java.lang.String" itemvalue="javax.annotation.CheckForNull" />
         </list>
       </value>
     </option>
     <option name="myNotNulls">
       <value>
-        <list size="10">
-          <item index="0" class="java.lang.String" itemvalue="org.jetbrains.annotations.NotNull" />
-          <item index="1" class="java.lang.String" itemvalue="javax.annotation.Nonnull" />
-          <item index="2" class="java.lang.String" itemvalue="edu.umd.cs.findbugs.annotations.NonNull" />
+        <list size="13">
+          <item index="0" class="java.lang.String" itemvalue="org.checkerframework.checker.nullness.qual.NonNull" />
+          <item index="1" class="java.lang.String" itemvalue="org.checkerframework.checker.nullness.compatqual.NonNullDecl" />
+          <item index="2" class="java.lang.String" itemvalue="org.checkerframework.checker.nullness.compatqual.NonNullType" />
           <item index="3" class="java.lang.String" itemvalue="android.support.annotation.NonNull" />
           <item index="4" class="java.lang.String" itemvalue="androidx.annotation.NonNull" />
           <item index="5" class="java.lang.String" itemvalue="androidx.annotation.RecentlyNonNull" />
-          <item index="6" class="java.lang.String" itemvalue="org.checkerframework.checker.nullness.qual.NonNull" />
-          <item index="7" class="java.lang.String" itemvalue="org.checkerframework.checker.nullness.compatqual.NonNullDecl" />
-          <item index="8" class="java.lang.String" itemvalue="org.checkerframework.checker.nullness.compatqual.NonNullType" />
-          <item index="9" class="java.lang.String" itemvalue="com.android.annotations.NonNull" />
+          <item index="6" class="java.lang.String" itemvalue="javax.annotation.Nonnull" />
+          <item index="7" class="java.lang.String" itemvalue="com.android.annotations.NonNull" />
+          <item index="8" class="java.lang.String" itemvalue="org.jspecify.annotations.NonNull" />
+          <item index="9" class="java.lang.String" itemvalue="org.jetbrains.annotations.NotNull" />
+         <item index="10" class="java.lang.String" itemvalue="org.eclipse.jdt.annotation.NonNull" />
+          <item index="11" class="java.lang.String" itemvalue="edu.umd.cs.findbugs.annotations.NonNull" />
+          <item index="12" class="java.lang.String" itemvalue="jakarta.annotation.Nonnull" />
         </list>
       </value>
     </option>

From 19b3ccbb672d1a81677ec7760e8e0339dbcc469e Mon Sep 17 00:00:00 2001
From: Daniel Raffler <daniel-raffler@gmx.de>
Date: Sun, 29 Mar 2026 14:29:33 +0200
Subject: [PATCH 03/23] Intellij: Simplify module dependencies

---
 .idea/JavaSMT.iml | 291 ++++------------------------------------------
 1 file changed, 25 insertions(+), 266 deletions(-)

diff --git a/.idea/JavaSMT.iml b/.idea/JavaSMT.iml
index 787850f16f..c4da76cb3e 100644
--- a/.idea/JavaSMT.iml
+++ b/.idea/JavaSMT.iml
@@ -23,368 +23,127 @@ SPDX-License-Identifier: Apache-2.0
       <excludeFolder url="file://$MODULE_DIR$/repository" />
     </content>
     <orderEntry type="jdk" jdkName="17" jdkType="JavaSDK" />
-    <orderEntry type="sourceFolder" forTests="false" />
-    <orderEntry type="module-library">
-      <library>
-        <CLASSES>
-          <root url="file://$MODULE_DIR$/lib" />
-        </CLASSES>
-        <JAVADOC />
-        <SOURCES>
-          <root url="file://$MODULE_DIR$/lib" />
-        </SOURCES>
-        <jarDirectory url="file://$MODULE_DIR$/lib" recursive="false" />
-        <jarDirectory url="file://$MODULE_DIR$/lib" recursive="false" type="SOURCES" />
-      </library>
-    </orderEntry>
     <orderEntry type="module-library">
       <library>
         <CLASSES>
-          <root url="jar://$MODULE_DIR$/lib/java/core/guava.jar!/" />
-        </CLASSES>
-        <JAVADOC />
-        <SOURCES>
-          <root url="jar://$MODULE_DIR$/lib/java-contrib/guava-sources.jar!/" />
-        </SOURCES>
-      </library>
-    </orderEntry>
-    <orderEntry type="module-library">
-      <library>
-        <CLASSES>
-          <root url="jar://$MODULE_DIR$/lib/java/test/checker-compat-qual.jar!/" />
+          <root url="file://$MODULE_DIR$/lib/java/core" />
         </CLASSES>
         <JAVADOC />
         <SOURCES />
+        <jarDirectory url="file://$MODULE_DIR$/lib/java/core" recursive="false" />
       </library>
     </orderEntry>
     <orderEntry type="module-library">
       <library>
         <CLASSES>
-          <root url="jar://$MODULE_DIR$/lib/java/test/diffutils.jar!/" />
+          <root url="file://$MODULE_DIR$/lib/java/build" />
         </CLASSES>
         <JAVADOC />
         <SOURCES />
+        <jarDirectory url="file://$MODULE_DIR$/lib/java/build" recursive="false" />
       </library>
     </orderEntry>
     <orderEntry type="module-library">
       <library>
         <CLASSES>
-          <root url="jar://$MODULE_DIR$/lib/java/core/common.jar!/" />
-        </CLASSES>
-        <JAVADOC />
-        <SOURCES>
-          <root url="jar://$MODULE_DIR$/lib/java-contrib/common-sources.jar!/" />
-        </SOURCES>
-      </library>
-    </orderEntry>
-    <orderEntry type="module-library">
-      <library>
-        <CLASSES>
-          <root url="jar://$MODULE_DIR$/lib/java/build/auto-value-annotations.jar!/" />
-        </CLASSES>
-        <JAVADOC />
-        <SOURCES>
-          <root url="jar://$MODULE_DIR$/lib/java/build/auto-value-annotations.jar!/" />
-        </SOURCES>
-      </library>
-    </orderEntry>
-    <orderEntry type="module-library">
-      <library>
-        <CLASSES>
-          <root url="jar://$MODULE_DIR$/lib/java/test/jsr305.jar!/" />
-        </CLASSES>
-        <JAVADOC />
-        <SOURCES>
-          <root url="jar://$MODULE_DIR$/lib/java/test/jsr305.jar!/" />
-        </SOURCES>
-      </library>
-    </orderEntry>
-    <orderEntry type="module-library">
-      <library>
-        <CLASSES>
-          <root url="jar://$MODULE_DIR$/lib/java/test/junit.jar!/" />
+          <root url="file://$MODULE_DIR$/lib/java/test" />
         </CLASSES>
         <JAVADOC />
         <SOURCES />
+        <jarDirectory url="file://$MODULE_DIR$/lib/java/test" recursive="false" />
       </library>
     </orderEntry>
     <orderEntry type="module-library">
       <library>
         <CLASSES>
-          <root url="jar://$MODULE_DIR$/lib/java/test/guava-testlib.jar!/" />
-        </CLASSES>
-        <JAVADOC />
-        <SOURCES>
-          <root url="jar://$MODULE_DIR$/lib/java-contrib/guava-testlib-sources.jar!/" />
-        </SOURCES>
-      </library>
-    </orderEntry>
-    <orderEntry type="module-library">
-      <library>
-        <CLASSES>
-          <root url="jar://$MODULE_DIR$/lib/java/test/truth.jar!/" />
-        </CLASSES>
-        <JAVADOC />
-        <SOURCES>
-          <root url="jar://$MODULE_DIR$/lib/java-contrib/truth-sources.jar!/" />
-        </SOURCES>
-      </library>
-    </orderEntry>
-    <orderEntry type="module-library">
-      <library>
-        <CLASSES>
-          <root url="jar://$MODULE_DIR$/lib/java/core/checker-qual.jar!/" />
-        </CLASSES>
-        <JAVADOC />
-        <SOURCES>
-          <root url="jar://$MODULE_DIR$/lib/java-contrib/checker-qual-sources.jar!/" />
-        </SOURCES>
-      </library>
-    </orderEntry>
-    <orderEntry type="module-library">
-      <library>
-        <CLASSES>
-          <root url="jar://$MODULE_DIR$/lib/java/core/spotbugs-annotations.jar!/" />
-        </CLASSES>
-        <JAVADOC />
-        <SOURCES>
-          <root url="jar://$MODULE_DIR$/lib/java-contrib/spotbugs-annotations-sources.jar!/" />
-        </SOURCES>
-      </library>
-    </orderEntry>
-    <orderEntry type="module-library">
-      <library>
-        <CLASSES>
-          <root url="jar://$MODULE_DIR$/lib/java/core/spotbugs-annotations.jar!/" />
-        </CLASSES>
-        <JAVADOC />
-        <SOURCES>
-          <root url="jar://$MODULE_DIR$/lib/java-contrib/spotbugs-annotations-sources.jar!/" />
-        </SOURCES>
-      </library>
-    </orderEntry>
-    <orderEntry type="module-library">
-      <library>
-        <CLASSES>
-          <root url="jar://$MODULE_DIR$/lib/java/test/truth-java8-extension.jar!/" />
-        </CLASSES>
-        <JAVADOC />
-        <SOURCES>
-          <root url="jar://$MODULE_DIR$/lib/java-contrib/truth-java8-extension-sources.jar!/" />
-        </SOURCES>
-      </library>
-    </orderEntry>
-    <orderEntry type="module-library">
-      <library>
-        <CLASSES>
-          <root url="jar://$MODULE_DIR$/lib/java/runtime-smtinterpol/smtinterpol.jar!/" />
-        </CLASSES>
-        <JAVADOC />
-        <SOURCES>
-          <root url="jar://$MODULE_DIR$/lib/java-contrib/smtinterpol-sources.zip!/SMTInterpol/DeltaDebugger/src" />
-          <root url="jar://$MODULE_DIR$/lib/java-contrib/smtinterpol-sources.zip!/SMTInterpol/Library-SMTLIB/src" />
-          <root url="jar://$MODULE_DIR$/lib/java-contrib/smtinterpol-sources.zip!/SMTInterpol/ProoftreeCheck/src" />
-          <root url="jar://$MODULE_DIR$/lib/java-contrib/smtinterpol-sources.zip!/SMTInterpol/SMTInterpol/src" />
-          <root url="jar://$MODULE_DIR$/lib/java-contrib/smtinterpol-sources.zip!/SMTInterpol/SMTInterpolSamples/src" />
-          <root url="jar://$MODULE_DIR$/lib/java-contrib/smtinterpol-sources.zip!/SMTInterpol/SMTInterpolTest/src" />
-        </SOURCES>
-      </library>
-    </orderEntry>
-    <orderEntry type="module-library">
-      <library>
-        <CLASSES>
-          <root url="jar://$MODULE_DIR$/lib/java/runtime-princess/princess_2.13.jar!/" />
-        </CLASSES>
-        <JAVADOC />
-        <SOURCES>
-          <root url="jar://$MODULE_DIR$/lib/java-contrib/princess_2.13-sources.zip!/" />
-        </SOURCES>
-      </library>
-    </orderEntry>
-    <orderEntry type="module-library">
-      <library>
-        <CLASSES>
-          <root url="jar://$MODULE_DIR$/lib/java/runtime-princess/princess-parser_2.13.jar!/" />
+          <root url="file://$MODULE_DIR$/lib/java/runtime-bitwuzla" />
         </CLASSES>
         <JAVADOC />
         <SOURCES />
+        <jarDirectory url="file://$MODULE_DIR$/lib/java/runtime-bitwuzla" recursive="false" />
       </library>
     </orderEntry>
     <orderEntry type="module-library">
       <library>
         <CLASSES>
-          <root url="jar://$MODULE_DIR$/lib/java/runtime-princess/princess-smt-parser_2.13.jar!/" />
+          <root url="file://$MODULE_DIR$/lib/java/runtime-cvc4" />
         </CLASSES>
         <JAVADOC />
         <SOURCES />
+        <jarDirectory url="file://$MODULE_DIR$/lib/java/runtime-cvc4" recursive="false" />
       </library>
     </orderEntry>
     <orderEntry type="module-library">
       <library>
         <CLASSES>
-          <root url="jar://$MODULE_DIR$/lib/java/runtime-princess/scala-library.jar!/" />
+          <root url="file://$MODULE_DIR$/lib/java/runtime-cvc5" />
         </CLASSES>
         <JAVADOC />
         <SOURCES />
+        <jarDirectory url="file://$MODULE_DIR$/lib/java/runtime-cvc5" recursive="false" />
       </library>
     </orderEntry>
     <orderEntry type="module-library">
       <library>
         <CLASSES>
-          <root url="jar://$MODULE_DIR$/lib/java/runtime-princess/java-cup-runtime.jar!/" />
+          <root url="file://$MODULE_DIR$/lib/java/runtime-opensmt" />
         </CLASSES>
         <JAVADOC />
         <SOURCES />
+        <jarDirectory url="file://$MODULE_DIR$/lib/java/runtime-opensmt" recursive="false" />
       </library>
     </orderEntry>
     <orderEntry type="module-library">
       <library>
         <CLASSES>
-          <root url="jar://$MODULE_DIR$/lib/java/test/hamcrest-core.jar!/" />
+          <root url="file://$MODULE_DIR$/lib/java/runtime-princess" />
         </CLASSES>
         <JAVADOC />
         <SOURCES />
+        <jarDirectory url="file://$MODULE_DIR$/lib/java/runtime-princess" recursive="false" />
       </library>
     </orderEntry>
     <orderEntry type="module-library">
       <library>
         <CLASSES>
-          <root url="jar://$MODULE_DIR$/lib/java/build/error_prone_annotations.jar!/" />
+          <root url="file://$MODULE_DIR$/lib/java/runtime-smtinterpol" />
         </CLASSES>
         <JAVADOC />
         <SOURCES />
+        <jarDirectory url="file://$MODULE_DIR$/lib/java/runtime-smtinterpol" recursive="false" />
       </library>
     </orderEntry>
     <orderEntry type="module-library">
       <library>
         <CLASSES>
-          <root url="jar://$MODULE_DIR$/lib/java/build/error_prone_ant.jar!/" />
-        </CLASSES>
-        <JAVADOC />
-        <SOURCES>
-          <root url="jar://$MODULE_DIR$/lib/java/build/error_prone_ant.jar!/" />
-        </SOURCES>
-      </library>
-    </orderEntry>
-    <orderEntry type="module-library">
-      <library>
-        <CLASSES>
-          <root url="jar://$MODULE_DIR$/lib/java/runtime/java-cup-runtime.jar!/" />
+          <root url="file://$MODULE_DIR$/lib/java/runtime-yices2" />
         </CLASSES>
         <JAVADOC />
         <SOURCES />
+        <jarDirectory url="file://$MODULE_DIR$/lib/java/runtime-yices2" recursive="false" />
       </library>
     </orderEntry>
     <orderEntry type="module-library">
       <library>
         <CLASSES>
-          <root url="jar://$MODULE_DIR$/lib/java/runtime-princess/smt-parser.jar!/" />
+          <root url="file://$MODULE_DIR$/lib/java/runtime-z3" />
         </CLASSES>
         <JAVADOC />
         <SOURCES />
+        <jarDirectory url="file://$MODULE_DIR$/lib/java/runtime-z3" recursive="false" />
       </library>
     </orderEntry>
     <orderEntry type="module-library">
       <library>
         <CLASSES>
-          <root url="jar://$MODULE_DIR$/lib/java/runtime-z3/com.microsoft.z3.jar!/" />
-        </CLASSES>
-        <JAVADOC />
-        <SOURCES>
-          <root url="jar://$MODULE_DIR$/lib/java-contrib/com.microsoft.z3-sources.jar!/" />
-        </SOURCES>
-      </library>
-    </orderEntry>
-    <orderEntry type="module-library">
-      <library>
-        <CLASSES>
-          <root url="jar://$MODULE_DIR$/lib/java/runtime-z3-legacy/com.microsoft.z3legacy.jar!/" />
-        </CLASSES>
-        <JAVADOC />
-        <SOURCES />
-      </library>
-    </orderEntry>
-    <orderEntry type="module-library">
-      <library>
-        <CLASSES>
-          <root url="jar://$MODULE_DIR$/lib/java/runtime-cvc4/CVC4.jar!/" />
-        </CLASSES>
-        <JAVADOC />
-        <SOURCES />
-      </library>
-    </orderEntry>
-    <orderEntry type="module-library">
-      <library>
-        <CLASSES>
-          <root url="jar://$MODULE_DIR$/lib/java/runtime-cvc5/cvc5.jar!/" />
-        </CLASSES>
-        <JAVADOC />
-        <SOURCES />
-      </library>
-    </orderEntry>
-    <orderEntry type="module-library">
-      <library>
-        <CLASSES>
-          <root url="jar://$MODULE_DIR$/lib/java/runtime-opensmt/opensmt.jar!/" />
-        </CLASSES>
-        <JAVADOC />
-        <SOURCES />
-      </library>
-    </orderEntry>
-    <orderEntry type="module-library">
-      <library>
-        <CLASSES>
-          <root url="jar://$MODULE_DIR$/lib/java/runtime-bitwuzla/bitwuzla.jar!/" />
-        </CLASSES>
-        <JAVADOC />
-        <SOURCES />
-      </library>
-    </orderEntry>
-    <orderEntry type="module-library">
-      <library>
-        <CLASSES>
-          <root url="jar://$MODULE_DIR$/lib/java/runtime-bitwuzla/bitwuzla.jar!/" />
-        </CLASSES>
-        <JAVADOC />
-        <SOURCES />
-      </library>
-    </orderEntry>
-    <orderEntry type="module-library">
-      <library>
-        <CLASSES>
-          <root url="jar://$MODULE_DIR$/lib/java/runtime-princess/ostrich_2.13.jar!/" />
-        </CLASSES>
-        <JAVADOC />
-        <SOURCES />
-      </library>
-    </orderEntry>
-    <orderEntry type="module-library">
-      <library>
-        <CLASSES>
-          <root url="jar://$MODULE_DIR$/lib/java/runtime-princess/automaton.jar!/" />
-        </CLASSES>
-        <JAVADOC />
-        <SOURCES />
-      </library>
-    </orderEntry>
-    <orderEntry type="module-library">
-      <library>
-        <CLASSES>
-          <root url="jar://$MODULE_DIR$/lib/java/runtime-yices2/yices.jar!/" />
-        </CLASSES>
-        <JAVADOC />
-        <SOURCES />
-      </library>
-    </orderEntry>
-    <orderEntry type="module-library">
-      <library>
-        <CLASSES>
-          <root url="jar://$MODULE_DIR$/lib/java/core/jspecify.jar!/" />
+          <root url="file://$MODULE_DIR$/lib/java/runtime-z3-legacy" />
         </CLASSES>
         <JAVADOC />
         <SOURCES />
+        <jarDirectory url="file://$MODULE_DIR$/lib/java/runtime-z3-legacy" recursive="false" />
       </library>
     </orderEntry>
+    <orderEntry type="sourceFolder" forTests="false" />
   </component>
   <component name="org.twodividedbyzero.idea.findbugs">
     <option name="_basePreferences">

From 0b0bcf9d72f4caf2ae6b81691421e9e04308f56b Mon Sep 17 00:00:00 2001
From: Daniel Raffler <daniel-raffler@gmx.de>
Date: Sun, 29 Mar 2026 14:34:58 +0200
Subject: [PATCH 04/23] Intellij: Add solver sources for debugging

---
 .idea/JavaSMT.iml | 21 ++++++++++++++++-----
 1 file changed, 16 insertions(+), 5 deletions(-)

diff --git a/.idea/JavaSMT.iml b/.idea/JavaSMT.iml
index c4da76cb3e..575702445f 100644
--- a/.idea/JavaSMT.iml
+++ b/.idea/JavaSMT.iml
@@ -59,7 +59,9 @@ SPDX-License-Identifier: Apache-2.0
           <root url="file://$MODULE_DIR$/lib/java/runtime-bitwuzla" />
         </CLASSES>
         <JAVADOC />
-        <SOURCES />
+        <SOURCES>
+          <root url="jar://$MODULE_DIR$/lib/java-contrib/bitwuzla-sources.jar!/" />
+        </SOURCES>
         <jarDirectory url="file://$MODULE_DIR$/lib/java/runtime-bitwuzla" recursive="false" />
       </library>
     </orderEntry>
@@ -89,7 +91,9 @@ SPDX-License-Identifier: Apache-2.0
           <root url="file://$MODULE_DIR$/lib/java/runtime-opensmt" />
         </CLASSES>
         <JAVADOC />
-        <SOURCES />
+        <SOURCES>
+          <root url="jar://$MODULE_DIR$/lib/java-contrib/opensmt-sources.jar!/" />
+        </SOURCES>
         <jarDirectory url="file://$MODULE_DIR$/lib/java/runtime-opensmt" recursive="false" />
       </library>
     </orderEntry>
@@ -99,7 +103,10 @@ SPDX-License-Identifier: Apache-2.0
           <root url="file://$MODULE_DIR$/lib/java/runtime-princess" />
         </CLASSES>
         <JAVADOC />
-        <SOURCES />
+        <SOURCES>
+          <root url="jar://$MODULE_DIR$/lib/java-contrib/ostrich_2.13-sources.jar!/" />
+          <root url="jar://$MODULE_DIR$/lib/java-contrib/princess_2.13-sources.jar!/" />
+        </SOURCES>
         <jarDirectory url="file://$MODULE_DIR$/lib/java/runtime-princess" recursive="false" />
       </library>
     </orderEntry>
@@ -109,7 +116,9 @@ SPDX-License-Identifier: Apache-2.0
           <root url="file://$MODULE_DIR$/lib/java/runtime-smtinterpol" />
         </CLASSES>
         <JAVADOC />
-        <SOURCES />
+        <SOURCES>
+          <root url="jar://$MODULE_DIR$/lib/java-contrib/smtinterpol-sources.jar!/" />
+        </SOURCES>
         <jarDirectory url="file://$MODULE_DIR$/lib/java/runtime-smtinterpol" recursive="false" />
       </library>
     </orderEntry>
@@ -129,7 +138,9 @@ SPDX-License-Identifier: Apache-2.0
           <root url="file://$MODULE_DIR$/lib/java/runtime-z3" />
         </CLASSES>
         <JAVADOC />
-        <SOURCES />
+        <SOURCES>
+          <root url="jar://$MODULE_DIR$/lib/java-contrib/com.microsoft.z3-sources.jar!/" />
+        </SOURCES>
         <jarDirectory url="file://$MODULE_DIR$/lib/java/runtime-z3" recursive="false" />
       </library>
     </orderEntry>

From d720039936135b605356d21f98abb8c7122faccf Mon Sep 17 00:00:00 2001
From: Daniel Raffler <daniel-raffler@gmx.de>
Date: Sun, 29 Mar 2026 14:36:06 +0200
Subject: [PATCH 05/23] Intellij: Remove unused Nullable annotations

---
 .idea/misc.xml | 37 +++++++++++++++----------------------
 1 file changed, 15 insertions(+), 22 deletions(-)

diff --git a/.idea/misc.xml b/.idea/misc.xml
index 616a44460c..9ca39bc181 100644
--- a/.idea/misc.xml
+++ b/.idea/misc.xml
@@ -20,40 +20,33 @@ SPDX-License-Identifier: Apache-2.0
     <option name="myOrdered" value="true" />
     <option name="myNullables">
       <value>
-        <list size="14">
+        <list size="11">
           <item index="0" class="java.lang.String" itemvalue="org.checkerframework.checker.nullness.qual.Nullable" />
           <item index="1" class="java.lang.String" itemvalue="org.checkerframework.checker.nullness.compatqual.NullableDecl" />
           <item index="2" class="java.lang.String" itemvalue="org.checkerframework.checker.nullness.compatqual.NullableType" />
           <item index="3" class="java.lang.String" itemvalue="javax.annotation.Nullable" />
-          <item index="4" class="java.lang.String" itemvalue="android.support.annotation.Nullable" />
-          <item index="5" class="java.lang.String" itemvalue="androidx.annotation.Nullable" />
-          <item index="6" class="java.lang.String" itemvalue="androidx.annotation.RecentlyNullable" />
-          <item index="7" class="java.lang.String" itemvalue="com.android.annotations.Nullable" />
-          <item index="8" class="java.lang.String" itemvalue="org.jspecify.annotations.Nullable" />
-          <item index="9" class="java.lang.String" itemvalue="org.jetbrains.annotations.Nullable" />
-          <item index="10" class="java.lang.String" itemvalue="org.eclipse.jdt.annotation.Nullable" />
-          <item index="11" class="java.lang.String" itemvalue="edu.umd.cs.findbugs.annotations.Nullable" />
-          <item index="12" class="java.lang.String" itemvalue="jakarta.annotation.Nullable" />
-          <item index="13" class="java.lang.String" itemvalue="javax.annotation.CheckForNull" />
+          <item index="4" class="java.lang.String" itemvalue="androidx.annotation.RecentlyNullable" />
+          <item index="5" class="java.lang.String" itemvalue="org.jspecify.annotations.Nullable" />
+          <item index="6" class="java.lang.String" itemvalue="org.jetbrains.annotations.Nullable" />
+          <item index="7" class="java.lang.String" itemvalue="org.eclipse.jdt.annotation.Nullable" />
+          <item index="8" class="java.lang.String" itemvalue="edu.umd.cs.findbugs.annotations.Nullable" />
+          <item index="9" class="java.lang.String" itemvalue="jakarta.annotation.Nullable" />
+          <item index="10" class="java.lang.String" itemvalue="javax.annotation.CheckForNull" />
         </list>
       </value>
     </option>
     <option name="myNotNulls">
       <value>
-        <list size="13">
+        <list size="9">
           <item index="0" class="java.lang.String" itemvalue="org.checkerframework.checker.nullness.qual.NonNull" />
           <item index="1" class="java.lang.String" itemvalue="org.checkerframework.checker.nullness.compatqual.NonNullDecl" />
           <item index="2" class="java.lang.String" itemvalue="org.checkerframework.checker.nullness.compatqual.NonNullType" />
-          <item index="3" class="java.lang.String" itemvalue="android.support.annotation.NonNull" />
-          <item index="4" class="java.lang.String" itemvalue="androidx.annotation.NonNull" />
-          <item index="5" class="java.lang.String" itemvalue="androidx.annotation.RecentlyNonNull" />
-          <item index="6" class="java.lang.String" itemvalue="javax.annotation.Nonnull" />
-          <item index="7" class="java.lang.String" itemvalue="com.android.annotations.NonNull" />
-          <item index="8" class="java.lang.String" itemvalue="org.jspecify.annotations.NonNull" />
-          <item index="9" class="java.lang.String" itemvalue="org.jetbrains.annotations.NotNull" />
-         <item index="10" class="java.lang.String" itemvalue="org.eclipse.jdt.annotation.NonNull" />
-          <item index="11" class="java.lang.String" itemvalue="edu.umd.cs.findbugs.annotations.NonNull" />
-          <item index="12" class="java.lang.String" itemvalue="jakarta.annotation.Nonnull" />
+          <item index="3" class="java.lang.String" itemvalue="javax.annotation.Nonnull" />
+          <item index="4" class="java.lang.String" itemvalue="org.jspecify.annotations.NonNull" />
+          <item index="5" class="java.lang.String" itemvalue="org.jetbrains.annotations.NotNull" />
+          <item index="6" class="java.lang.String" itemvalue="org.eclipse.jdt.annotation.NonNull" />
+          <item index="7" class="java.lang.String" itemvalue="edu.umd.cs.findbugs.annotations.NonNull" />
+          <item index="8" class="java.lang.String" itemvalue="jakarta.annotation.Nonnull" />
         </list>
       </value>
     </option>

From 671639b6bc6f5d0fb171cddd0a37db16844e7830 Mon Sep 17 00:00:00 2001
From: Daniel Raffler <daniel-raffler@gmx.de>
Date: Sun, 29 Mar 2026 14:36:37 +0200
Subject: [PATCH 06/23] Intellij: Use `org.checkerframework.checker.nullness`
 by default

---
 .idea/misc.xml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/.idea/misc.xml b/.idea/misc.xml
index 9ca39bc181..43052c22c0 100644
--- a/.idea/misc.xml
+++ b/.idea/misc.xml
@@ -15,8 +15,8 @@ SPDX-License-Identifier: Apache-2.0
     <entry_points version="2.0" />
   </component>
   <component name="NullableNotNullManager">
-    <option name="myDefaultNullable" value="javax.annotation.Nullable" />
-    <option name="myDefaultNotNull" value="javax.annotation.Nonnull" />
+    <option name="myDefaultNullable" value="org.checkerframework.checker.nullness.qual.Nullable" />
+    <option name="myDefaultNotNull" value="org.checkerframework.checker.nullness.qual.NonNull" />
     <option name="myOrdered" value="true" />
     <option name="myNullables">
       <value>

From 11077c45a39debb6ca3992148579833712915800 Mon Sep 17 00:00:00 2001
From: Daniel Raffler <daniel-raffler@gmx.de>
Date: Mon, 30 Mar 2026 17:09:23 +0200
Subject: [PATCH 07/23] Intelij: Move module sources back up

---
 .idea/JavaSMT.iml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/.idea/JavaSMT.iml b/.idea/JavaSMT.iml
index 575702445f..4515f6094a 100644
--- a/.idea/JavaSMT.iml
+++ b/.idea/JavaSMT.iml
@@ -23,6 +23,7 @@ SPDX-License-Identifier: Apache-2.0
       <excludeFolder url="file://$MODULE_DIR$/repository" />
     </content>
     <orderEntry type="jdk" jdkName="17" jdkType="JavaSDK" />
+    <orderEntry type="sourceFolder" forTests="false" />
     <orderEntry type="module-library">
       <library>
         <CLASSES>
@@ -154,7 +155,6 @@ SPDX-License-Identifier: Apache-2.0
         <jarDirectory url="file://$MODULE_DIR$/lib/java/runtime-z3-legacy" recursive="false" />
       </library>
     </orderEntry>
-    <orderEntry type="sourceFolder" forTests="false" />
   </component>
   <component name="org.twodividedbyzero.idea.findbugs">
     <option name="_basePreferences">

From 6e9ba341cf258a3a8f26d1d27822f36b3ab68a05 Mon Sep 17 00:00:00 2001
From: Daniel Raffler <daniel-raffler@gmx.de>
Date: Mon, 30 Mar 2026 17:27:58 +0200
Subject: [PATCH 08/23] Intelij: Remove one more Nullable annotation

---
 .idea/misc.xml | 15 +++++++--------
 1 file changed, 7 insertions(+), 8 deletions(-)

diff --git a/.idea/misc.xml b/.idea/misc.xml
index 43052c22c0..c10bd7bbd1 100644
--- a/.idea/misc.xml
+++ b/.idea/misc.xml
@@ -20,18 +20,17 @@ SPDX-License-Identifier: Apache-2.0
     <option name="myOrdered" value="true" />
     <option name="myNullables">
       <value>
-        <list size="11">
+        <list size="10">
           <item index="0" class="java.lang.String" itemvalue="org.checkerframework.checker.nullness.qual.Nullable" />
           <item index="1" class="java.lang.String" itemvalue="org.checkerframework.checker.nullness.compatqual.NullableDecl" />
           <item index="2" class="java.lang.String" itemvalue="org.checkerframework.checker.nullness.compatqual.NullableType" />
           <item index="3" class="java.lang.String" itemvalue="javax.annotation.Nullable" />
-          <item index="4" class="java.lang.String" itemvalue="androidx.annotation.RecentlyNullable" />
-          <item index="5" class="java.lang.String" itemvalue="org.jspecify.annotations.Nullable" />
-          <item index="6" class="java.lang.String" itemvalue="org.jetbrains.annotations.Nullable" />
-          <item index="7" class="java.lang.String" itemvalue="org.eclipse.jdt.annotation.Nullable" />
-          <item index="8" class="java.lang.String" itemvalue="edu.umd.cs.findbugs.annotations.Nullable" />
-          <item index="9" class="java.lang.String" itemvalue="jakarta.annotation.Nullable" />
-          <item index="10" class="java.lang.String" itemvalue="javax.annotation.CheckForNull" />
+          <item index="4" class="java.lang.String" itemvalue="org.jspecify.annotations.Nullable" />
+          <item index="5" class="java.lang.String" itemvalue="org.jetbrains.annotations.Nullable" />
+          <item index="6" class="java.lang.String" itemvalue="org.eclipse.jdt.annotation.Nullable" />
+          <item index="7" class="java.lang.String" itemvalue="edu.umd.cs.findbugs.annotations.Nullable" />
+          <item index="8" class="java.lang.String" itemvalue="jakarta.annotation.Nullable" />
+          <item index="9" class="java.lang.String" itemvalue="javax.annotation.CheckForNull" />
         </list>
       </value>
     </option>

From 8a477c99a440c6210871cc1e89c83db27a2af85b Mon Sep 17 00:00:00 2001
From: Daniel Raffler <daniel-raffler@gmx.de>
Date: Mon, 30 Mar 2026 17:59:48 +0200
Subject: [PATCH 09/23] Intelij: Split off license headers

---
 .idea/JavaSMT.iml                                   | 13 +------------
 .idea/JavaSMT.iml.license                           |  9 +++++++++
 .idea/ant.xml                                       | 13 +------------
 .idea/ant.xml.license                               |  9 +++++++++
 .idea/checkstyle-idea.xml                           | 13 +------------
 .idea/checkstyle-idea.xml.license                   |  9 +++++++++
 .idea/codeStyleSettings.xml                         | 13 +------------
 .idea/codeStyleSettings.xml.license                 |  9 +++++++++
 .idea/compiler.xml                                  | 13 +------------
 .idea/compiler.xml.license                          |  9 +++++++++
 .idea/copyright/JavaSMT.xml                         | 10 ----------
 .idea/copyright/JavaSMT.xml.license                 |  9 +++++++++
 .idea/copyright/profiles_settings.xml               | 10 ----------
 .idea/copyright/profiles_settings.xml.license       |  9 +++++++++
 .idea/encodings.xml                                 | 13 +------------
 .idea/encodings.xml.license                         |  9 +++++++++
 .idea/inspectionProfiles/Project_Default.xml        | 10 ----------
 .../inspectionProfiles/Project_Default.xml.license  |  9 +++++++++
 .idea/inspectionProfiles/profiles_settings.xml      | 10 ----------
 .../profiles_settings.xml.license                   |  9 +++++++++
 .idea/junitgenerator-prj-settings.xml               | 13 +------------
 .idea/junitgenerator-prj-settings.xml.license       |  9 +++++++++
 .idea/misc.xml                                      | 13 +------------
 .idea/misc.xml.license                              |  9 +++++++++
 .idea/modules.xml                                   | 13 +------------
 .idea/modules.xml.license                           |  9 +++++++++
 .idea/vcs.xml                                       | 13 +------------
 .idea/vcs.xml.license                               |  9 +++++++++
 28 files changed, 136 insertions(+), 160 deletions(-)
 create mode 100644 .idea/JavaSMT.iml.license
 create mode 100644 .idea/ant.xml.license
 create mode 100644 .idea/checkstyle-idea.xml.license
 create mode 100644 .idea/codeStyleSettings.xml.license
 create mode 100644 .idea/compiler.xml.license
 create mode 100644 .idea/copyright/JavaSMT.xml.license
 create mode 100644 .idea/copyright/profiles_settings.xml.license
 create mode 100644 .idea/encodings.xml.license
 create mode 100644 .idea/inspectionProfiles/Project_Default.xml.license
 create mode 100644 .idea/inspectionProfiles/profiles_settings.xml.license
 create mode 100644 .idea/junitgenerator-prj-settings.xml.license
 create mode 100644 .idea/misc.xml.license
 create mode 100644 .idea/modules.xml.license
 create mode 100644 .idea/vcs.xml.license

diff --git a/.idea/JavaSMT.iml b/.idea/JavaSMT.iml
index 4515f6094a..e3e364d815 100644
--- a/.idea/JavaSMT.iml
+++ b/.idea/JavaSMT.iml
@@ -1,15 +1,4 @@
 <?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: 2020 Dirk Beyer <https://www.sosy-lab.org>
-
-SPDX-License-Identifier: Apache-2.0
--->
-
 <module type="JAVA_MODULE" version="4">
   <component name="NewModuleRootManager">
     <output url="file://$MODULE_DIR$/bin" />
@@ -361,4 +350,4 @@ SPDX-License-Identifier: Apache-2.0
       </map>
     </option>
   </component>
-</module>
+</module>
\ No newline at end of file
diff --git a/.idea/JavaSMT.iml.license b/.idea/JavaSMT.iml.license
new file mode 100644
index 0000000000..5bc96c012f
--- /dev/null
+++ b/.idea/JavaSMT.iml.license
@@ -0,0 +1,9 @@
+<!--
+This file is part of JavaSMT,
+an API wrapper for a collection of SMT solvers:
+https://github.com/sosy-lab/java-smt
+
+SPDX-FileCopyrightText: 2020 Dirk Beyer <https://www.sosy-lab.org>
+
+SPDX-License-Identifier: Apache-2.0
+-->
diff --git a/.idea/ant.xml b/.idea/ant.xml
index 3e3b7e7277..52ce37416f 100644
--- a/.idea/ant.xml
+++ b/.idea/ant.xml
@@ -1,19 +1,8 @@
 <?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: 2020 Dirk Beyer <https://www.sosy-lab.org>
-
-SPDX-License-Identifier: Apache-2.0
--->
-
 <project version="4">
   <component name="AntConfiguration">
     <buildFile url="file://$PROJECT_DIR$/build.xml">
       <executeOn event="beforeCompilation" target="build-dependencies" />
     </buildFile>
   </component>
-</project>
+</project>
\ No newline at end of file
diff --git a/.idea/ant.xml.license b/.idea/ant.xml.license
new file mode 100644
index 0000000000..5bc96c012f
--- /dev/null
+++ b/.idea/ant.xml.license
@@ -0,0 +1,9 @@
+<!--
+This file is part of JavaSMT,
+an API wrapper for a collection of SMT solvers:
+https://github.com/sosy-lab/java-smt
+
+SPDX-FileCopyrightText: 2020 Dirk Beyer <https://www.sosy-lab.org>
+
+SPDX-License-Identifier: Apache-2.0
+-->
diff --git a/.idea/checkstyle-idea.xml b/.idea/checkstyle-idea.xml
index a1e7fbf3b3..bcbddbdab8 100644
--- a/.idea/checkstyle-idea.xml
+++ b/.idea/checkstyle-idea.xml
@@ -1,15 +1,4 @@
 <?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: 2020 Dirk Beyer <https://www.sosy-lab.org>
-
-SPDX-License-Identifier: Apache-2.0
--->
-
 <project version="4">
   <component name="CheckStyle-IDEA">
     <option name="configuration">
@@ -25,4 +14,4 @@ SPDX-License-Identifier: Apache-2.0
       </map>
     </option>
   </component>
-</project>
+</project>
\ No newline at end of file
diff --git a/.idea/checkstyle-idea.xml.license b/.idea/checkstyle-idea.xml.license
new file mode 100644
index 0000000000..5bc96c012f
--- /dev/null
+++ b/.idea/checkstyle-idea.xml.license
@@ -0,0 +1,9 @@
+<!--
+This file is part of JavaSMT,
+an API wrapper for a collection of SMT solvers:
+https://github.com/sosy-lab/java-smt
+
+SPDX-FileCopyrightText: 2020 Dirk Beyer <https://www.sosy-lab.org>
+
+SPDX-License-Identifier: Apache-2.0
+-->
diff --git a/.idea/codeStyleSettings.xml b/.idea/codeStyleSettings.xml
index 9a4d556d44..f479196698 100644
--- a/.idea/codeStyleSettings.xml
+++ b/.idea/codeStyleSettings.xml
@@ -1,15 +1,4 @@
 <?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: 2020 Dirk Beyer <https://www.sosy-lab.org>
-
-SPDX-License-Identifier: Apache-2.0
--->
-
 <project version="4">
   <component name="ProjectCodeStyleSettingsManager">
     <option name="PER_PROJECT_SETTINGS">
@@ -189,4 +178,4 @@ SPDX-License-Identifier: Apache-2.0
     </option>
     <option name="USE_PER_PROJECT_SETTINGS" value="true" />
   </component>
-</project>
+</project>
\ No newline at end of file
diff --git a/.idea/codeStyleSettings.xml.license b/.idea/codeStyleSettings.xml.license
new file mode 100644
index 0000000000..5bc96c012f
--- /dev/null
+++ b/.idea/codeStyleSettings.xml.license
@@ -0,0 +1,9 @@
+<!--
+This file is part of JavaSMT,
+an API wrapper for a collection of SMT solvers:
+https://github.com/sosy-lab/java-smt
+
+SPDX-FileCopyrightText: 2020 Dirk Beyer <https://www.sosy-lab.org>
+
+SPDX-License-Identifier: Apache-2.0
+-->
diff --git a/.idea/compiler.xml b/.idea/compiler.xml
index 1214f58eab..9a8b7e5c45 100644
--- a/.idea/compiler.xml
+++ b/.idea/compiler.xml
@@ -1,15 +1,4 @@
 <?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: 2020 Dirk Beyer <https://www.sosy-lab.org>
-
-SPDX-License-Identifier: Apache-2.0
--->
-
 <project version="4">
   <component name="CompilerConfiguration">
     <option name="DEFAULT_COMPILER" value="Javac" />
@@ -30,4 +19,4 @@ SPDX-License-Identifier: Apache-2.0
       </profile>
     </annotationProcessing>
   </component>
-</project>
+</project>
\ No newline at end of file
diff --git a/.idea/compiler.xml.license b/.idea/compiler.xml.license
new file mode 100644
index 0000000000..5bc96c012f
--- /dev/null
+++ b/.idea/compiler.xml.license
@@ -0,0 +1,9 @@
+<!--
+This file is part of JavaSMT,
+an API wrapper for a collection of SMT solvers:
+https://github.com/sosy-lab/java-smt
+
+SPDX-FileCopyrightText: 2020 Dirk Beyer <https://www.sosy-lab.org>
+
+SPDX-License-Identifier: Apache-2.0
+-->
diff --git a/.idea/copyright/JavaSMT.xml b/.idea/copyright/JavaSMT.xml
index a9fee1de71..f6c7b5082b 100644
--- a/.idea/copyright/JavaSMT.xml
+++ b/.idea/copyright/JavaSMT.xml
@@ -1,13 +1,3 @@
-<!--
-This file is part of JavaSMT,
-an API wrapper for a collection of SMT solvers:
-https://github.com/sosy-lab/java-smt
-
-SPDX-FileCopyrightText: 2020 Dirk Beyer <https://www.sosy-lab.org>
-
-SPDX-License-Identifier: Apache-2.0
--->
-
 <component name="CopyrightManager">
   <copyright>
     <option name="notice" value="This file is part of JavaSMT,&#10;an API wrapper for a collection of SMT solvers:&#10;https://github.com/sosy-lab/java-smt&#10;&#10;SPDX-FileCopyrightText: &amp;#36;today.year Dirk Beyer &lt;https://www.sosy-lab.org&gt;&#10;&#10;SPDX-License-Identifier: Apache-2.0" />
diff --git a/.idea/copyright/JavaSMT.xml.license b/.idea/copyright/JavaSMT.xml.license
new file mode 100644
index 0000000000..5bc96c012f
--- /dev/null
+++ b/.idea/copyright/JavaSMT.xml.license
@@ -0,0 +1,9 @@
+<!--
+This file is part of JavaSMT,
+an API wrapper for a collection of SMT solvers:
+https://github.com/sosy-lab/java-smt
+
+SPDX-FileCopyrightText: 2020 Dirk Beyer <https://www.sosy-lab.org>
+
+SPDX-License-Identifier: Apache-2.0
+-->
diff --git a/.idea/copyright/profiles_settings.xml b/.idea/copyright/profiles_settings.xml
index 3cfcc9878e..40ef6891de 100644
--- a/.idea/copyright/profiles_settings.xml
+++ b/.idea/copyright/profiles_settings.xml
@@ -1,13 +1,3 @@
-<!--
-This file is part of JavaSMT,
-an API wrapper for a collection of SMT solvers:
-https://github.com/sosy-lab/java-smt
-
-SPDX-FileCopyrightText: 2020 Dirk Beyer <https://www.sosy-lab.org>
-
-SPDX-License-Identifier: Apache-2.0
--->
-
 <component name="CopyrightManager">
   <settings default="JavaSMT" />
 </component>
\ No newline at end of file
diff --git a/.idea/copyright/profiles_settings.xml.license b/.idea/copyright/profiles_settings.xml.license
new file mode 100644
index 0000000000..5bc96c012f
--- /dev/null
+++ b/.idea/copyright/profiles_settings.xml.license
@@ -0,0 +1,9 @@
+<!--
+This file is part of JavaSMT,
+an API wrapper for a collection of SMT solvers:
+https://github.com/sosy-lab/java-smt
+
+SPDX-FileCopyrightText: 2020 Dirk Beyer <https://www.sosy-lab.org>
+
+SPDX-License-Identifier: Apache-2.0
+-->
diff --git a/.idea/encodings.xml b/.idea/encodings.xml
index db30d8ee89..97626ba454 100644
--- a/.idea/encodings.xml
+++ b/.idea/encodings.xml
@@ -1,17 +1,6 @@
 <?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: 2020 Dirk Beyer <https://www.sosy-lab.org>
-
-SPDX-License-Identifier: Apache-2.0
--->
-
 <project version="4">
   <component name="Encoding">
     <file url="PROJECT" charset="UTF-8" />
   </component>
-</project>
+</project>
\ No newline at end of file
diff --git a/.idea/encodings.xml.license b/.idea/encodings.xml.license
new file mode 100644
index 0000000000..5bc96c012f
--- /dev/null
+++ b/.idea/encodings.xml.license
@@ -0,0 +1,9 @@
+<!--
+This file is part of JavaSMT,
+an API wrapper for a collection of SMT solvers:
+https://github.com/sosy-lab/java-smt
+
+SPDX-FileCopyrightText: 2020 Dirk Beyer <https://www.sosy-lab.org>
+
+SPDX-License-Identifier: Apache-2.0
+-->
diff --git a/.idea/inspectionProfiles/Project_Default.xml b/.idea/inspectionProfiles/Project_Default.xml
index be8f53a4b2..a62e60bb7f 100644
--- a/.idea/inspectionProfiles/Project_Default.xml
+++ b/.idea/inspectionProfiles/Project_Default.xml
@@ -1,13 +1,3 @@
-<!--
-This file is part of JavaSMT,
-an API wrapper for a collection of SMT solvers:
-https://github.com/sosy-lab/java-smt
-
-SPDX-FileCopyrightText: 2020 Dirk Beyer <https://www.sosy-lab.org>
-
-SPDX-License-Identifier: Apache-2.0
--->
-
 <component name="InspectionProjectProfileManager">
   <profile version="1.0">
     <option name="myName" value="Project Default" />
diff --git a/.idea/inspectionProfiles/Project_Default.xml.license b/.idea/inspectionProfiles/Project_Default.xml.license
new file mode 100644
index 0000000000..5bc96c012f
--- /dev/null
+++ b/.idea/inspectionProfiles/Project_Default.xml.license
@@ -0,0 +1,9 @@
+<!--
+This file is part of JavaSMT,
+an API wrapper for a collection of SMT solvers:
+https://github.com/sosy-lab/java-smt
+
+SPDX-FileCopyrightText: 2020 Dirk Beyer <https://www.sosy-lab.org>
+
+SPDX-License-Identifier: Apache-2.0
+-->
diff --git a/.idea/inspectionProfiles/profiles_settings.xml b/.idea/inspectionProfiles/profiles_settings.xml
index 1807f46726..3b312839bf 100644
--- a/.idea/inspectionProfiles/profiles_settings.xml
+++ b/.idea/inspectionProfiles/profiles_settings.xml
@@ -1,13 +1,3 @@
-<!--
-This file is part of JavaSMT,
-an API wrapper for a collection of SMT solvers:
-https://github.com/sosy-lab/java-smt
-
-SPDX-FileCopyrightText: 2020 Dirk Beyer <https://www.sosy-lab.org>
-
-SPDX-License-Identifier: Apache-2.0
--->
-
 <component name="InspectionProjectProfileManager">
   <settings>
     <option name="PROJECT_PROFILE" value="Project Default" />
diff --git a/.idea/inspectionProfiles/profiles_settings.xml.license b/.idea/inspectionProfiles/profiles_settings.xml.license
new file mode 100644
index 0000000000..5bc96c012f
--- /dev/null
+++ b/.idea/inspectionProfiles/profiles_settings.xml.license
@@ -0,0 +1,9 @@
+<!--
+This file is part of JavaSMT,
+an API wrapper for a collection of SMT solvers:
+https://github.com/sosy-lab/java-smt
+
+SPDX-FileCopyrightText: 2020 Dirk Beyer <https://www.sosy-lab.org>
+
+SPDX-License-Identifier: Apache-2.0
+-->
diff --git a/.idea/junitgenerator-prj-settings.xml b/.idea/junitgenerator-prj-settings.xml
index 5d18b2a084..d73e792aa7 100644
--- a/.idea/junitgenerator-prj-settings.xml
+++ b/.idea/junitgenerator-prj-settings.xml
@@ -1,17 +1,6 @@
 <?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: 2020 Dirk Beyer <https://www.sosy-lab.org>
-
-SPDX-License-Identifier: Apache-2.0
--->
-
 <project version="4">
   <component name="JUnitGeneratorProjectSettings">
     <option name="selectedTemplateKey" value="JUnit 4" />
   </component>
-</project>
+</project>
\ No newline at end of file
diff --git a/.idea/junitgenerator-prj-settings.xml.license b/.idea/junitgenerator-prj-settings.xml.license
new file mode 100644
index 0000000000..5bc96c012f
--- /dev/null
+++ b/.idea/junitgenerator-prj-settings.xml.license
@@ -0,0 +1,9 @@
+<!--
+This file is part of JavaSMT,
+an API wrapper for a collection of SMT solvers:
+https://github.com/sosy-lab/java-smt
+
+SPDX-FileCopyrightText: 2020 Dirk Beyer <https://www.sosy-lab.org>
+
+SPDX-License-Identifier: Apache-2.0
+-->
diff --git a/.idea/misc.xml b/.idea/misc.xml
index c10bd7bbd1..8ca8685d64 100644
--- a/.idea/misc.xml
+++ b/.idea/misc.xml
@@ -1,15 +1,4 @@
 <?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: 2020 Dirk Beyer <https://www.sosy-lab.org>
-
-SPDX-License-Identifier: Apache-2.0
--->
-
 <project version="4">
   <component name="EntryPointsManager">
     <entry_points version="2.0" />
@@ -53,4 +42,4 @@ SPDX-License-Identifier: Apache-2.0
   <component name="ProjectRootManager" version="2" languageLevel="JDK_17" project-jdk-name="17" project-jdk-type="JavaSDK">
     <output url="file://$PROJECT_DIR$/bin" />
   </component>
-</project>
+</project>
\ No newline at end of file
diff --git a/.idea/misc.xml.license b/.idea/misc.xml.license
new file mode 100644
index 0000000000..5bc96c012f
--- /dev/null
+++ b/.idea/misc.xml.license
@@ -0,0 +1,9 @@
+<!--
+This file is part of JavaSMT,
+an API wrapper for a collection of SMT solvers:
+https://github.com/sosy-lab/java-smt
+
+SPDX-FileCopyrightText: 2020 Dirk Beyer <https://www.sosy-lab.org>
+
+SPDX-License-Identifier: Apache-2.0
+-->
diff --git a/.idea/modules.xml b/.idea/modules.xml
index e70e3fe729..a13a73c19b 100644
--- a/.idea/modules.xml
+++ b/.idea/modules.xml
@@ -1,19 +1,8 @@
 <?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: 2020 Dirk Beyer <https://www.sosy-lab.org>
-
-SPDX-License-Identifier: Apache-2.0
--->
-
 <project version="4">
   <component name="ProjectModuleManager">
     <modules>
       <module fileurl="file://$PROJECT_DIR$/.idea/JavaSMT.iml" filepath="$PROJECT_DIR$/.idea/JavaSMT.iml" />
     </modules>
   </component>
-</project>
+</project>
\ No newline at end of file
diff --git a/.idea/modules.xml.license b/.idea/modules.xml.license
new file mode 100644
index 0000000000..5bc96c012f
--- /dev/null
+++ b/.idea/modules.xml.license
@@ -0,0 +1,9 @@
+<!--
+This file is part of JavaSMT,
+an API wrapper for a collection of SMT solvers:
+https://github.com/sosy-lab/java-smt
+
+SPDX-FileCopyrightText: 2020 Dirk Beyer <https://www.sosy-lab.org>
+
+SPDX-License-Identifier: Apache-2.0
+-->
diff --git a/.idea/vcs.xml b/.idea/vcs.xml
index 8f55ae7820..35eb1ddfbb 100644
--- a/.idea/vcs.xml
+++ b/.idea/vcs.xml
@@ -1,17 +1,6 @@
 <?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: 2020 Dirk Beyer <https://www.sosy-lab.org>
-
-SPDX-License-Identifier: Apache-2.0
--->
-
 <project version="4">
   <component name="VcsDirectoryMappings">
     <mapping directory="" vcs="Git" />
   </component>
-</project>
+</project>
\ No newline at end of file
diff --git a/.idea/vcs.xml.license b/.idea/vcs.xml.license
new file mode 100644
index 0000000000..5bc96c012f
--- /dev/null
+++ b/.idea/vcs.xml.license
@@ -0,0 +1,9 @@
+<!--
+This file is part of JavaSMT,
+an API wrapper for a collection of SMT solvers:
+https://github.com/sosy-lab/java-smt
+
+SPDX-FileCopyrightText: 2020 Dirk Beyer <https://www.sosy-lab.org>
+
+SPDX-License-Identifier: Apache-2.0
+-->

From f00e670b275c6c370686788ea9e79470fe61a679 Mon Sep 17 00:00:00 2001
From: Daniel Raffler <daniel-raffler@gmx.de>
Date: Mon, 30 Mar 2026 21:45:33 +0200
Subject: [PATCH 10/23] Intelij: Move solver dependencies to project libraries

---
 .idea/JavaSMT.iml                             | 110 ++----------------
 .idea/libraries/bitwuzla.xml                  |  14 +++
 .idea/libraries/bitwuzla.xml.license          |   9 ++
 .idea/libraries/cvc4.xml                      |  12 ++
 .idea/libraries/cvc4.xml.license              |   9 ++
 .idea/libraries/cvc5.xml                      |  12 ++
 .idea/libraries/cvc5.xml.license              |   9 ++
 .idea/libraries/opensmt.xml                   |  14 +++
 .idea/libraries/opensmt.xml.license           |   9 ++
 .idea/libraries/princess.xml                  |  15 +++
 .idea/libraries/princess.xml.license          |   9 ++
 .idea/libraries/smtinterpol.xml               |  15 +++
 .idea/libraries/smtinterpol.xml.license       |   9 ++
 .idea/libraries/yices.xml                     |  12 ++
 .idea/libraries/yices.xml.license             |   9 ++
 .idea/libraries/z3.xml                        |  14 +++
 .idea/libraries/z3.xml.license                |   9 ++
 .idea/libraries/z3legacy.xml                  |  10 ++
 .idea/libraries/z3legacy.xml.license          |   9 ++
 .../sosy_lab/java_smt/test/UnsatCoreTest.java |  10 ++
 20 files changed, 218 insertions(+), 101 deletions(-)
 create mode 100644 .idea/libraries/bitwuzla.xml
 create mode 100644 .idea/libraries/bitwuzla.xml.license
 create mode 100644 .idea/libraries/cvc4.xml
 create mode 100644 .idea/libraries/cvc4.xml.license
 create mode 100644 .idea/libraries/cvc5.xml
 create mode 100644 .idea/libraries/cvc5.xml.license
 create mode 100644 .idea/libraries/opensmt.xml
 create mode 100644 .idea/libraries/opensmt.xml.license
 create mode 100644 .idea/libraries/princess.xml
 create mode 100644 .idea/libraries/princess.xml.license
 create mode 100644 .idea/libraries/smtinterpol.xml
 create mode 100644 .idea/libraries/smtinterpol.xml.license
 create mode 100644 .idea/libraries/yices.xml
 create mode 100644 .idea/libraries/yices.xml.license
 create mode 100644 .idea/libraries/z3.xml
 create mode 100644 .idea/libraries/z3.xml.license
 create mode 100644 .idea/libraries/z3legacy.xml
 create mode 100644 .idea/libraries/z3legacy.xml.license

diff --git a/.idea/JavaSMT.iml b/.idea/JavaSMT.iml
index e3e364d815..0ce78f6bb1 100644
--- a/.idea/JavaSMT.iml
+++ b/.idea/JavaSMT.iml
@@ -43,107 +43,15 @@
         <jarDirectory url="file://$MODULE_DIR$/lib/java/test" recursive="false" />
       </library>
     </orderEntry>
-    <orderEntry type="module-library">
-      <library>
-        <CLASSES>
-          <root url="file://$MODULE_DIR$/lib/java/runtime-bitwuzla" />
-        </CLASSES>
-        <JAVADOC />
-        <SOURCES>
-          <root url="jar://$MODULE_DIR$/lib/java-contrib/bitwuzla-sources.jar!/" />
-        </SOURCES>
-        <jarDirectory url="file://$MODULE_DIR$/lib/java/runtime-bitwuzla" recursive="false" />
-      </library>
-    </orderEntry>
-    <orderEntry type="module-library">
-      <library>
-        <CLASSES>
-          <root url="file://$MODULE_DIR$/lib/java/runtime-cvc4" />
-        </CLASSES>
-        <JAVADOC />
-        <SOURCES />
-        <jarDirectory url="file://$MODULE_DIR$/lib/java/runtime-cvc4" recursive="false" />
-      </library>
-    </orderEntry>
-    <orderEntry type="module-library">
-      <library>
-        <CLASSES>
-          <root url="file://$MODULE_DIR$/lib/java/runtime-cvc5" />
-        </CLASSES>
-        <JAVADOC />
-        <SOURCES />
-        <jarDirectory url="file://$MODULE_DIR$/lib/java/runtime-cvc5" recursive="false" />
-      </library>
-    </orderEntry>
-    <orderEntry type="module-library">
-      <library>
-        <CLASSES>
-          <root url="file://$MODULE_DIR$/lib/java/runtime-opensmt" />
-        </CLASSES>
-        <JAVADOC />
-        <SOURCES>
-          <root url="jar://$MODULE_DIR$/lib/java-contrib/opensmt-sources.jar!/" />
-        </SOURCES>
-        <jarDirectory url="file://$MODULE_DIR$/lib/java/runtime-opensmt" recursive="false" />
-      </library>
-    </orderEntry>
-    <orderEntry type="module-library">
-      <library>
-        <CLASSES>
-          <root url="file://$MODULE_DIR$/lib/java/runtime-princess" />
-        </CLASSES>
-        <JAVADOC />
-        <SOURCES>
-          <root url="jar://$MODULE_DIR$/lib/java-contrib/ostrich_2.13-sources.jar!/" />
-          <root url="jar://$MODULE_DIR$/lib/java-contrib/princess_2.13-sources.jar!/" />
-        </SOURCES>
-        <jarDirectory url="file://$MODULE_DIR$/lib/java/runtime-princess" recursive="false" />
-      </library>
-    </orderEntry>
-    <orderEntry type="module-library">
-      <library>
-        <CLASSES>
-          <root url="file://$MODULE_DIR$/lib/java/runtime-smtinterpol" />
-        </CLASSES>
-        <JAVADOC />
-        <SOURCES>
-          <root url="jar://$MODULE_DIR$/lib/java-contrib/smtinterpol-sources.jar!/" />
-        </SOURCES>
-        <jarDirectory url="file://$MODULE_DIR$/lib/java/runtime-smtinterpol" recursive="false" />
-      </library>
-    </orderEntry>
-    <orderEntry type="module-library">
-      <library>
-        <CLASSES>
-          <root url="file://$MODULE_DIR$/lib/java/runtime-yices2" />
-        </CLASSES>
-        <JAVADOC />
-        <SOURCES />
-        <jarDirectory url="file://$MODULE_DIR$/lib/java/runtime-yices2" recursive="false" />
-      </library>
-    </orderEntry>
-    <orderEntry type="module-library">
-      <library>
-        <CLASSES>
-          <root url="file://$MODULE_DIR$/lib/java/runtime-z3" />
-        </CLASSES>
-        <JAVADOC />
-        <SOURCES>
-          <root url="jar://$MODULE_DIR$/lib/java-contrib/com.microsoft.z3-sources.jar!/" />
-        </SOURCES>
-        <jarDirectory url="file://$MODULE_DIR$/lib/java/runtime-z3" recursive="false" />
-      </library>
-    </orderEntry>
-    <orderEntry type="module-library">
-      <library>
-        <CLASSES>
-          <root url="file://$MODULE_DIR$/lib/java/runtime-z3-legacy" />
-        </CLASSES>
-        <JAVADOC />
-        <SOURCES />
-        <jarDirectory url="file://$MODULE_DIR$/lib/java/runtime-z3-legacy" recursive="false" />
-      </library>
-    </orderEntry>
+    <orderEntry type="library" name="bitwuzla" level="project" />
+    <orderEntry type="library" name="cvc4" level="project" />
+    <orderEntry type="library" name="cvc5" level="project" />
+    <orderEntry type="library" name="opensmt" level="project" />
+    <orderEntry type="library" name="princess" level="project" />
+    <orderEntry type="library" name="smtinterpol" level="project" />
+    <orderEntry type="library" name="yices" level="project" />
+    <orderEntry type="library" name="z3" level="project" />
+    <orderEntry type="library" name="z3legacy" level="project" />
   </component>
   <component name="org.twodividedbyzero.idea.findbugs">
     <option name="_basePreferences">
diff --git a/.idea/libraries/bitwuzla.xml b/.idea/libraries/bitwuzla.xml
new file mode 100644
index 0000000000..8cac34d992
--- /dev/null
+++ b/.idea/libraries/bitwuzla.xml
@@ -0,0 +1,14 @@
+<component name="libraryTable">
+  <library name="bitwuzla">
+    <CLASSES>
+      <root url="file://$PROJECT_DIR$/lib/java/runtime-bitwuzla" />
+    </CLASSES>
+    <JAVADOC>
+      <root url="jar://$PROJECT_DIR$/lib/java-contrib/bitwuzla-javadoc.jar!/" />
+    </JAVADOC>
+    <SOURCES>
+      <root url="jar://$PROJECT_DIR$/lib/java-contrib/bitwuzla-sources.jar!/" />
+    </SOURCES>
+    <jarDirectory url="file://$PROJECT_DIR$/lib/java/runtime-bitwuzla" recursive="false" />
+  </library>
+</component>
\ No newline at end of file
diff --git a/.idea/libraries/bitwuzla.xml.license b/.idea/libraries/bitwuzla.xml.license
new file mode 100644
index 0000000000..7e3675eb2b
--- /dev/null
+++ b/.idea/libraries/bitwuzla.xml.license
@@ -0,0 +1,9 @@
+<!--
+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 <https://www.sosy-lab.org>
+
+SPDX-License-Identifier: Apache-2.0
+-->
diff --git a/.idea/libraries/cvc4.xml b/.idea/libraries/cvc4.xml
new file mode 100644
index 0000000000..b369c95546
--- /dev/null
+++ b/.idea/libraries/cvc4.xml
@@ -0,0 +1,12 @@
+<component name="libraryTable">
+  <library name="cvc4">
+    <CLASSES>
+      <root url="file://$PROJECT_DIR$/lib/java/runtime-cvc4" />
+    </CLASSES>
+    <JAVADOC>
+      <root url="https://cvc4.github.io/documentation.html" />
+    </JAVADOC>
+    <SOURCES />
+    <jarDirectory url="file://$PROJECT_DIR$/lib/java/runtime-cvc4" recursive="false" />
+  </library>
+</component>
\ No newline at end of file
diff --git a/.idea/libraries/cvc4.xml.license b/.idea/libraries/cvc4.xml.license
new file mode 100644
index 0000000000..7e3675eb2b
--- /dev/null
+++ b/.idea/libraries/cvc4.xml.license
@@ -0,0 +1,9 @@
+<!--
+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 <https://www.sosy-lab.org>
+
+SPDX-License-Identifier: Apache-2.0
+-->
diff --git a/.idea/libraries/cvc5.xml b/.idea/libraries/cvc5.xml
new file mode 100644
index 0000000000..bc496be06b
--- /dev/null
+++ b/.idea/libraries/cvc5.xml
@@ -0,0 +1,12 @@
+<component name="libraryTable">
+  <library name="cvc5">
+    <CLASSES>
+      <root url="file://$PROJECT_DIR$/lib/java/runtime-cvc5" />
+    </CLASSES>
+    <JAVADOC>
+      <root url="https://cvc5.github.io/docs-ci/docs-main/" />
+    </JAVADOC>
+    <SOURCES />
+    <jarDirectory url="file://$PROJECT_DIR$/lib/java/runtime-cvc5" recursive="false" />
+  </library>
+</component>
\ No newline at end of file
diff --git a/.idea/libraries/cvc5.xml.license b/.idea/libraries/cvc5.xml.license
new file mode 100644
index 0000000000..7e3675eb2b
--- /dev/null
+++ b/.idea/libraries/cvc5.xml.license
@@ -0,0 +1,9 @@
+<!--
+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 <https://www.sosy-lab.org>
+
+SPDX-License-Identifier: Apache-2.0
+-->
diff --git a/.idea/libraries/opensmt.xml b/.idea/libraries/opensmt.xml
new file mode 100644
index 0000000000..1ede9c9fbf
--- /dev/null
+++ b/.idea/libraries/opensmt.xml
@@ -0,0 +1,14 @@
+<component name="libraryTable">
+  <library name="opensmt">
+    <CLASSES>
+      <root url="file://$PROJECT_DIR$/lib/java/runtime-opensmt" />
+    </CLASSES>
+    <JAVADOC>
+      <root url="jar://$PROJECT_DIR$/lib/java-contrib/opensmt-javadoc.jar!/" />
+    </JAVADOC>
+    <SOURCES>
+      <root url="jar://$PROJECT_DIR$/lib/java-contrib/opensmt-sources.jar!/" />
+    </SOURCES>
+    <jarDirectory url="file://$PROJECT_DIR$/lib/java/runtime-opensmt" recursive="false" />
+  </library>
+</component>
\ No newline at end of file
diff --git a/.idea/libraries/opensmt.xml.license b/.idea/libraries/opensmt.xml.license
new file mode 100644
index 0000000000..7e3675eb2b
--- /dev/null
+++ b/.idea/libraries/opensmt.xml.license
@@ -0,0 +1,9 @@
+<!--
+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 <https://www.sosy-lab.org>
+
+SPDX-License-Identifier: Apache-2.0
+-->
diff --git a/.idea/libraries/princess.xml b/.idea/libraries/princess.xml
new file mode 100644
index 0000000000..5566970491
--- /dev/null
+++ b/.idea/libraries/princess.xml
@@ -0,0 +1,15 @@
+<component name="libraryTable">
+  <library name="princess">
+    <CLASSES>
+      <root url="file://$PROJECT_DIR$/lib/java/runtime-princess" />
+    </CLASSES>
+    <JAVADOC>
+      <root url="https://philipp.ruemmer.org/princess/doc/#ap.package" />
+    </JAVADOC>
+    <SOURCES>
+      <root url="jar://$PROJECT_DIR$/lib/java-contrib/ostrich_2.13-sources.jar!/" />
+      <root url="jar://$PROJECT_DIR$/lib/java-contrib/princess_2.13-sources.jar!/" />
+    </SOURCES>
+    <jarDirectory url="file://$PROJECT_DIR$/lib/java/runtime-princess" recursive="false" />
+  </library>
+</component>
\ No newline at end of file
diff --git a/.idea/libraries/princess.xml.license b/.idea/libraries/princess.xml.license
new file mode 100644
index 0000000000..7e3675eb2b
--- /dev/null
+++ b/.idea/libraries/princess.xml.license
@@ -0,0 +1,9 @@
+<!--
+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 <https://www.sosy-lab.org>
+
+SPDX-License-Identifier: Apache-2.0
+-->
diff --git a/.idea/libraries/smtinterpol.xml b/.idea/libraries/smtinterpol.xml
new file mode 100644
index 0000000000..f471219341
--- /dev/null
+++ b/.idea/libraries/smtinterpol.xml
@@ -0,0 +1,15 @@
+<component name="libraryTable">
+  <library name="smtinterpol">
+    <CLASSES>
+      <root url="file://$PROJECT_DIR$/lib/java/runtime-smtinterpol" />
+    </CLASSES>
+    <JAVADOC>
+      <root url="https://ultimate.informatik.uni-freiburg.de/smtinterpol/doc/index.html" />
+    </JAVADOC>
+    <SOURCES>
+      <root url="jar://$PROJECT_DIR$/lib/java-contrib/smtinterpol-sources.jar!/smtinterpol/Library-SMTLIB/src" />
+      <root url="jar://$PROJECT_DIR$/lib/java-contrib/smtinterpol-sources.jar!/smtinterpol/SMTInterpol/src" />
+    </SOURCES>
+    <jarDirectory url="file://$PROJECT_DIR$/lib/java/runtime-smtinterpol" recursive="false" />
+  </library>
+</component>
\ No newline at end of file
diff --git a/.idea/libraries/smtinterpol.xml.license b/.idea/libraries/smtinterpol.xml.license
new file mode 100644
index 0000000000..7e3675eb2b
--- /dev/null
+++ b/.idea/libraries/smtinterpol.xml.license
@@ -0,0 +1,9 @@
+<!--
+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 <https://www.sosy-lab.org>
+
+SPDX-License-Identifier: Apache-2.0
+-->
diff --git a/.idea/libraries/yices.xml b/.idea/libraries/yices.xml
new file mode 100644
index 0000000000..e31f335b61
--- /dev/null
+++ b/.idea/libraries/yices.xml
@@ -0,0 +1,12 @@
+<component name="libraryTable">
+  <library name="yices">
+    <CLASSES>
+      <root url="file://$PROJECT_DIR$/lib/java/runtime-yices2" />
+    </CLASSES>
+    <JAVADOC>
+      <root url="https://yices.csl.sri.com/yices2-documentation.html" />
+    </JAVADOC>
+    <SOURCES />
+    <jarDirectory url="file://$PROJECT_DIR$/lib/java/runtime-yices2" recursive="false" />
+  </library>
+</component>
\ No newline at end of file
diff --git a/.idea/libraries/yices.xml.license b/.idea/libraries/yices.xml.license
new file mode 100644
index 0000000000..7e3675eb2b
--- /dev/null
+++ b/.idea/libraries/yices.xml.license
@@ -0,0 +1,9 @@
+<!--
+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 <https://www.sosy-lab.org>
+
+SPDX-License-Identifier: Apache-2.0
+-->
diff --git a/.idea/libraries/z3.xml b/.idea/libraries/z3.xml
new file mode 100644
index 0000000000..fa33e192e7
--- /dev/null
+++ b/.idea/libraries/z3.xml
@@ -0,0 +1,14 @@
+<component name="libraryTable">
+  <library name="z3">
+    <CLASSES>
+      <root url="file://$PROJECT_DIR$/lib/java/runtime-z3" />
+    </CLASSES>
+    <JAVADOC>
+      <root url="jar://$PROJECT_DIR$/lib/java-contrib/com.microsoft.z3-javadoc.jar!/" />
+    </JAVADOC>
+    <SOURCES>
+      <root url="jar://$PROJECT_DIR$/lib/java-contrib/com.microsoft.z3-sources.jar!/" />
+    </SOURCES>
+    <jarDirectory url="file://$PROJECT_DIR$/lib/java/runtime-z3" recursive="false" />
+  </library>
+</component>
\ No newline at end of file
diff --git a/.idea/libraries/z3.xml.license b/.idea/libraries/z3.xml.license
new file mode 100644
index 0000000000..7e3675eb2b
--- /dev/null
+++ b/.idea/libraries/z3.xml.license
@@ -0,0 +1,9 @@
+<!--
+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 <https://www.sosy-lab.org>
+
+SPDX-License-Identifier: Apache-2.0
+-->
diff --git a/.idea/libraries/z3legacy.xml b/.idea/libraries/z3legacy.xml
new file mode 100644
index 0000000000..8b0924407c
--- /dev/null
+++ b/.idea/libraries/z3legacy.xml
@@ -0,0 +1,10 @@
+<component name="libraryTable">
+  <library name="z3legacy">
+    <CLASSES>
+      <root url="file://$PROJECT_DIR$/lib/java/runtime-z3-legacy" />
+    </CLASSES>
+    <JAVADOC />
+    <SOURCES />
+    <jarDirectory url="file://$PROJECT_DIR$/lib/java/runtime-z3-legacy" recursive="false" />
+  </library>
+</component>
\ No newline at end of file
diff --git a/.idea/libraries/z3legacy.xml.license b/.idea/libraries/z3legacy.xml.license
new file mode 100644
index 0000000000..7e3675eb2b
--- /dev/null
+++ b/.idea/libraries/z3legacy.xml.license
@@ -0,0 +1,9 @@
+<!--
+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 <https://www.sosy-lab.org>
+
+SPDX-License-Identifier: Apache-2.0
+-->
diff --git a/src/org/sosy_lab/java_smt/test/UnsatCoreTest.java b/src/org/sosy_lab/java_smt/test/UnsatCoreTest.java
index a2af7cd4d2..c34833e65e 100644
--- a/src/org/sosy_lab/java_smt/test/UnsatCoreTest.java
+++ b/src/org/sosy_lab/java_smt/test/UnsatCoreTest.java
@@ -73,6 +73,16 @@ public void getUnsatCoreThrowsWithoutOptionTest() throws InterruptedException, S
     }
   }
 
+  @Test
+  public void test() throws SolverException, InterruptedException {
+    var var1 = bmgr.makeVariable("var");
+    try (var prover = context.newProverEnvironment()) {
+      prover.addConstraint(var1);
+      prover.addConstraint(bmgr.not(var1));
+      assertThat(prover.isUnsat()).isTrue();
+    }
+  }
+
   @Test
   public void simpleUnsatCoreOverAssumptionsTest() throws InterruptedException, SolverException {
     requireUnsatCoreOverAssumptions();

From 835e14401ca24d35b7aef19156e15e41f8e6f07a Mon Sep 17 00:00:00 2001
From: Daniel Raffler <daniel-raffler@gmx.de>
Date: Mon, 30 Mar 2026 21:52:23 +0200
Subject: [PATCH 11/23] Intellij: Revert unwanted changed

---
 src/org/sosy_lab/java_smt/test/UnsatCoreTest.java | 10 ----------
 1 file changed, 10 deletions(-)

diff --git a/src/org/sosy_lab/java_smt/test/UnsatCoreTest.java b/src/org/sosy_lab/java_smt/test/UnsatCoreTest.java
index c34833e65e..a2af7cd4d2 100644
--- a/src/org/sosy_lab/java_smt/test/UnsatCoreTest.java
+++ b/src/org/sosy_lab/java_smt/test/UnsatCoreTest.java
@@ -73,16 +73,6 @@ public void getUnsatCoreThrowsWithoutOptionTest() throws InterruptedException, S
     }
   }
 
-  @Test
-  public void test() throws SolverException, InterruptedException {
-    var var1 = bmgr.makeVariable("var");
-    try (var prover = context.newProverEnvironment()) {
-      prover.addConstraint(var1);
-      prover.addConstraint(bmgr.not(var1));
-      assertThat(prover.isUnsat()).isTrue();
-    }
-  }
-
   @Test
   public void simpleUnsatCoreOverAssumptionsTest() throws InterruptedException, SolverException {
     requireUnsatCoreOverAssumptions();

From 38bb486cccf306b27520994f619397d536d0976c Mon Sep 17 00:00:00 2001
From: Daniel Raffler <daniel-raffler@gmx.de>
Date: Wed, 1 Apr 2026 10:23:18 +0200
Subject: [PATCH 12/23] OpenSMT: Build jar with debug info

---
 build/build-publish-solvers/solver-opensmt.xml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/build/build-publish-solvers/solver-opensmt.xml b/build/build-publish-solvers/solver-opensmt.xml
index 99ffe3ac68..27bb2493d4 100644
--- a/build/build-publish-solvers/solver-opensmt.xml
+++ b/build/build-publish-solvers/solver-opensmt.xml
@@ -194,7 +194,7 @@ SPDX-License-Identifier: Apache-2.0
     <target name="build-opensmt-bindings-jni" depends="build-opensmt-wrapper">
         <!-- compile java proxies and create jar file -->
         <mkdir dir="${source.path}/build"/>
-        <javac release="11" srcdir="${source.path}/src/" destdir="${source.path}/build" includeantruntime="false" failonerror="true">
+        <javac release="11" srcdir="${source.path}/src/" destdir="${source.path}/build" debug="true" includeantruntime="false" failonerror="true">
             <include name="org/sosy_lab/java_smt/solvers/opensmt/api/*.java"/>
         </javac>
         <jar destfile="${opensmt.dist.dir}/opensmt-${opensmt.version}.jar" basedir="${source.path}/build"/>

From 726c4071c2d281ecc247d9cd19a686031d0cd553 Mon Sep 17 00:00:00 2001
From: Daniel Raffler <daniel-raffler@gmx.de>
Date: Wed, 1 Apr 2026 10:27:18 +0200
Subject: [PATCH 13/23] OpenSMT, Bitwuzla: Build solver jars for Java17

---
 build/build-publish-solvers/solver-bitwuzla.xml | 2 +-
 build/build-publish-solvers/solver-opensmt.xml  | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/build/build-publish-solvers/solver-bitwuzla.xml b/build/build-publish-solvers/solver-bitwuzla.xml
index d140f85a23..0c68a8727e 100644
--- a/build/build-publish-solvers/solver-bitwuzla.xml
+++ b/build/build-publish-solvers/solver-bitwuzla.xml
@@ -106,7 +106,7 @@ SPDX-License-Identifier: Apache-2.0
 
         <!-- Compile java proxies and create jar file -->
         <mkdir dir="${bitwuzla.path}/install/java/build"/>
-        <javac release="11" debug="true" srcdir="${source.path}/libbitwuzla/src/" destdir="${bitwuzla.path}/install/java/build" includeantruntime="false" failonerror="true">
+        <javac release="17" debug="true" srcdir="${source.path}/libbitwuzla/src/" destdir="${bitwuzla.path}/install/java/build" includeantruntime="false" failonerror="true">
             <include name="org/sosy_lab/java_smt/solvers/bitwuzla/api/*.java"/>
         </javac>
         <jar destfile="${bitwuzla.dist.dir}/bitwuzla-${bitwuzla.version}.jar" basedir="${bitwuzla.path}/install/java/build"/>
diff --git a/build/build-publish-solvers/solver-opensmt.xml b/build/build-publish-solvers/solver-opensmt.xml
index 27bb2493d4..f5f3afe8fd 100644
--- a/build/build-publish-solvers/solver-opensmt.xml
+++ b/build/build-publish-solvers/solver-opensmt.xml
@@ -194,7 +194,7 @@ SPDX-License-Identifier: Apache-2.0
     <target name="build-opensmt-bindings-jni" depends="build-opensmt-wrapper">
         <!-- compile java proxies and create jar file -->
         <mkdir dir="${source.path}/build"/>
-        <javac release="11" srcdir="${source.path}/src/" destdir="${source.path}/build" debug="true" includeantruntime="false" failonerror="true">
+        <javac release="17" srcdir="${source.path}/src/" destdir="${source.path}/build" debug="true" includeantruntime="false" failonerror="true">
             <include name="org/sosy_lab/java_smt/solvers/opensmt/api/*.java"/>
         </javac>
         <jar destfile="${opensmt.dist.dir}/opensmt-${opensmt.version}.jar" basedir="${source.path}/build"/>

From 04daeb225665f9d0bc7971f35b03adfc776964df Mon Sep 17 00:00:00 2001
From: Daniel Raffler <daniel-raffler@gmx.de>
Date: Wed, 1 Apr 2026 10:31:36 +0200
Subject: [PATCH 14/23] Revert: Wrong branch...

This reverts commits 38bb486cccf306b27520994f619397d536d0976c and 726c4071c2d281ecc247d9cd19a686031d0cd553.
---
 build/build-publish-solvers/solver-bitwuzla.xml | 2 +-
 build/build-publish-solvers/solver-opensmt.xml  | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/build/build-publish-solvers/solver-bitwuzla.xml b/build/build-publish-solvers/solver-bitwuzla.xml
index 0c68a8727e..d140f85a23 100644
--- a/build/build-publish-solvers/solver-bitwuzla.xml
+++ b/build/build-publish-solvers/solver-bitwuzla.xml
@@ -106,7 +106,7 @@ SPDX-License-Identifier: Apache-2.0
 
         <!-- Compile java proxies and create jar file -->
         <mkdir dir="${bitwuzla.path}/install/java/build"/>
-        <javac release="17" debug="true" srcdir="${source.path}/libbitwuzla/src/" destdir="${bitwuzla.path}/install/java/build" includeantruntime="false" failonerror="true">
+        <javac release="11" debug="true" srcdir="${source.path}/libbitwuzla/src/" destdir="${bitwuzla.path}/install/java/build" includeantruntime="false" failonerror="true">
             <include name="org/sosy_lab/java_smt/solvers/bitwuzla/api/*.java"/>
         </javac>
         <jar destfile="${bitwuzla.dist.dir}/bitwuzla-${bitwuzla.version}.jar" basedir="${bitwuzla.path}/install/java/build"/>
diff --git a/build/build-publish-solvers/solver-opensmt.xml b/build/build-publish-solvers/solver-opensmt.xml
index f5f3afe8fd..99ffe3ac68 100644
--- a/build/build-publish-solvers/solver-opensmt.xml
+++ b/build/build-publish-solvers/solver-opensmt.xml
@@ -194,7 +194,7 @@ SPDX-License-Identifier: Apache-2.0
     <target name="build-opensmt-bindings-jni" depends="build-opensmt-wrapper">
         <!-- compile java proxies and create jar file -->
         <mkdir dir="${source.path}/build"/>
-        <javac release="17" srcdir="${source.path}/src/" destdir="${source.path}/build" debug="true" includeantruntime="false" failonerror="true">
+        <javac release="11" srcdir="${source.path}/src/" destdir="${source.path}/build" includeantruntime="false" failonerror="true">
             <include name="org/sosy_lab/java_smt/solvers/opensmt/api/*.java"/>
         </javac>
         <jar destfile="${opensmt.dist.dir}/opensmt-${opensmt.version}.jar" basedir="${source.path}/build"/>

From 0549d78a2ef4a2bfac9951f410af16f457a7d60c Mon Sep 17 00:00:00 2001
From: Daniel Raffler <daniel-raffler@gmx.de>
Date: Sat, 11 Apr 2026 11:05:02 +0200
Subject: [PATCH 15/23] Intellij: Add sources and JavaDoc for cvc4

---
 .idea/libraries/cvc4.xml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/.idea/libraries/cvc4.xml b/.idea/libraries/cvc4.xml
index b369c95546..aaaa482069 100644
--- a/.idea/libraries/cvc4.xml
+++ b/.idea/libraries/cvc4.xml
@@ -4,9 +4,11 @@
       <root url="file://$PROJECT_DIR$/lib/java/runtime-cvc4" />
     </CLASSES>
     <JAVADOC>
-      <root url="https://cvc4.github.io/documentation.html" />
+      <root url="jar://$PROJECT_DIR$/lib/java-contrib/CVC4-javadoc.jar!/" />
     </JAVADOC>
-    <SOURCES />
+    <SOURCES>
+      <root url="jar://$PROJECT_DIR$/lib/java-contrib/CVC4-sources.jar!/" />
+    </SOURCES>
     <jarDirectory url="file://$PROJECT_DIR$/lib/java/runtime-cvc4" recursive="false" />
   </library>
 </component>
\ No newline at end of file

From a1572dcf2e8657a434c72c04bad99325372845fe Mon Sep 17 00:00:00 2001
From: Daniel Raffler <daniel-raffler@gmx.de>
Date: Sat, 11 Apr 2026 11:09:40 +0200
Subject: [PATCH 16/23] Intellij: Remove .apt-generated from src folders

---
 .idea/JavaSMT.iml | 1 -
 1 file changed, 1 deletion(-)

diff --git a/.idea/JavaSMT.iml b/.idea/JavaSMT.iml
index 0ce78f6bb1..13a12e47a1 100644
--- a/.idea/JavaSMT.iml
+++ b/.idea/JavaSMT.iml
@@ -5,7 +5,6 @@
     <exclude-output />
     <content url="file://$MODULE_DIR$">
       <sourceFolder url="file://$MODULE_DIR$/src" isTestSource="false" />
-      <sourceFolder url="file://$MODULE_DIR$/.apt-generated" isTestSource="false" />
       <excludeFolder url="file://$MODULE_DIR$/JUnit-coverage" />
       <excludeFolder url="file://$MODULE_DIR$/Javadoc" />
       <excludeFolder url="file://$MODULE_DIR$/junit" />

From 5594531e5ea0298cc75f69ea957d08027358311e Mon Sep 17 00:00:00 2001
From: Daniel Raffler <daniel-raffler@gmx.de>
Date: Mon, 13 Apr 2026 08:21:19 +0200
Subject: [PATCH 17/23] Add yices2 docs/sources to javasmt-yices2 dependency

We need to include 'contrib' here to get the sources/docs for the solver, and not just the java-smt yices backend
---
 lib/ivy.xml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lib/ivy.xml b/lib/ivy.xml
index ec89566edb..2b46531b85 100644
--- a/lib/ivy.xml
+++ b/lib/ivy.xml
@@ -201,7 +201,7 @@ SPDX-License-Identifier: Apache-2.0
         <dependency org="org.sosy_lab" name="javasmt-solver-z3-legacy" rev="4.5.0-gd57a2a6dc" conf="runtime-z3-legacy-x64->solver-z3-legacy-x64; runtime-z3-legacy-arm64->solver-z3-legacy-arm64" />
 
         <!-- additional JavaSMT components with Solver Binaries -->
-        <dependency org="org.sosy_lab" name="javasmt-yices2" rev="6.0.0-530-g472e8e81c" conf="runtime-yices2->runtime; contrib->sources,javadoc" />
+        <dependency org="org.sosy_lab" name="javasmt-yices2" rev="6.0.0-530-g472e8e81c" conf="runtime-yices2->runtime; contrib->sources,javadoc, contrib"/>
 
         <!-- Several JARs declare animal-sniffer-annotations.jar as dependency in their manifest, although they do not really need it.
              As long as this is the case we need to provide the JAR, otherwise javac complains. -->

From 59e5eff01fecccaf2fb1b10c0677c66b9e67d5f8 Mon Sep 17 00:00:00 2001
From: Daniel Raffler <daniel-raffler@gmx.de>
Date: Mon, 13 Apr 2026 08:22:16 +0200
Subject: [PATCH 18/23] Intellij: Add sources/docs for cvc5, princess,
 smtinterpol and yices to the project configuration

---
 .idea/libraries/cvc5.xml        | 6 ++++--
 .idea/libraries/princess.xml    | 3 ++-
 .idea/libraries/smtinterpol.xml | 2 +-
 .idea/libraries/yices.xml       | 6 ++++--
 4 files changed, 11 insertions(+), 6 deletions(-)

diff --git a/.idea/libraries/cvc5.xml b/.idea/libraries/cvc5.xml
index bc496be06b..e6a0c1125b 100644
--- a/.idea/libraries/cvc5.xml
+++ b/.idea/libraries/cvc5.xml
@@ -4,9 +4,11 @@
       <root url="file://$PROJECT_DIR$/lib/java/runtime-cvc5" />
     </CLASSES>
     <JAVADOC>
-      <root url="https://cvc5.github.io/docs-ci/docs-main/" />
+      <root url="jar://$PROJECT_DIR$/lib/java-contrib/cvc5-javadoc.jar!/" />
     </JAVADOC>
-    <SOURCES />
+    <SOURCES>
+      <root url="jar://$PROJECT_DIR$/lib/java-contrib/cvc5-sources.jar!/" />
+    </SOURCES>
     <jarDirectory url="file://$PROJECT_DIR$/lib/java/runtime-cvc5" recursive="false" />
   </library>
 </component>
\ No newline at end of file
diff --git a/.idea/libraries/princess.xml b/.idea/libraries/princess.xml
index 5566970491..732fd4b18d 100644
--- a/.idea/libraries/princess.xml
+++ b/.idea/libraries/princess.xml
@@ -4,7 +4,8 @@
       <root url="file://$PROJECT_DIR$/lib/java/runtime-princess" />
     </CLASSES>
     <JAVADOC>
-      <root url="https://philipp.ruemmer.org/princess/doc/#ap.package" />
+      <root url="jar://$PROJECT_DIR$/lib/java-contrib/ostrich_2.13-javadoc.jar!/" />
+      <root url="jar://$PROJECT_DIR$/lib/java-contrib/princess_2.13-javadoc.jar!/" />
     </JAVADOC>
     <SOURCES>
       <root url="jar://$PROJECT_DIR$/lib/java-contrib/ostrich_2.13-sources.jar!/" />
diff --git a/.idea/libraries/smtinterpol.xml b/.idea/libraries/smtinterpol.xml
index f471219341..7cd3e27d86 100644
--- a/.idea/libraries/smtinterpol.xml
+++ b/.idea/libraries/smtinterpol.xml
@@ -4,7 +4,7 @@
       <root url="file://$PROJECT_DIR$/lib/java/runtime-smtinterpol" />
     </CLASSES>
     <JAVADOC>
-      <root url="https://ultimate.informatik.uni-freiburg.de/smtinterpol/doc/index.html" />
+      <root url="jar://$PROJECT_DIR$/lib/java-contrib/smtinterpol-javadoc.jar!/" />
     </JAVADOC>
     <SOURCES>
       <root url="jar://$PROJECT_DIR$/lib/java-contrib/smtinterpol-sources.jar!/smtinterpol/Library-SMTLIB/src" />
diff --git a/.idea/libraries/yices.xml b/.idea/libraries/yices.xml
index e31f335b61..63053f86b9 100644
--- a/.idea/libraries/yices.xml
+++ b/.idea/libraries/yices.xml
@@ -4,9 +4,11 @@
       <root url="file://$PROJECT_DIR$/lib/java/runtime-yices2" />
     </CLASSES>
     <JAVADOC>
-      <root url="https://yices.csl.sri.com/yices2-documentation.html" />
+      <root url="jar://$PROJECT_DIR$/lib/java-contrib/yices-javadoc.jar!/" />
     </JAVADOC>
-    <SOURCES />
+    <SOURCES>
+      <root url="jar://$PROJECT_DIR$/lib/java-contrib/yices-sources.jar!/" />
+    </SOURCES>
     <jarDirectory url="file://$PROJECT_DIR$/lib/java/runtime-yices2" recursive="false" />
   </library>
 </component>
\ No newline at end of file

From 6c3023f557ac4ed5de9bd3c01c67105dac05f276 Mon Sep 17 00:00:00 2001
From: Daniel Raffler <daniel-raffler@gmx.de>
Date: Thu, 23 Apr 2026 13:55:56 +0200
Subject: [PATCH 19/23] Intellij: Update copyright dates for the configuration
 files

---
 .idea/JavaSMT.iml.license                              | 2 +-
 .idea/ant.xml.license                                  | 2 +-
 .idea/checkstyle-idea.xml.license                      | 2 +-
 .idea/codeStyleSettings.xml.license                    | 2 +-
 .idea/compiler.xml.license                             | 2 +-
 .idea/copyright/JavaSMT.xml.license                    | 2 +-
 .idea/copyright/profiles_settings.xml.license          | 2 +-
 .idea/encodings.xml.license                            | 2 +-
 .idea/inspectionProfiles/Project_Default.xml.license   | 2 +-
 .idea/inspectionProfiles/profiles_settings.xml.license | 2 +-
 .idea/junitgenerator-prj-settings.xml.license          | 2 +-
 .idea/misc.xml.license                                 | 2 +-
 .idea/modules.xml.license                              | 2 +-
 .idea/vcs.xml.license                                  | 2 +-
 14 files changed, 14 insertions(+), 14 deletions(-)

diff --git a/.idea/JavaSMT.iml.license b/.idea/JavaSMT.iml.license
index 5bc96c012f..7e3675eb2b 100644
--- a/.idea/JavaSMT.iml.license
+++ b/.idea/JavaSMT.iml.license
@@ -3,7 +3,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: 2020 Dirk Beyer <https://www.sosy-lab.org>
+SPDX-FileCopyrightText: 2026 Dirk Beyer <https://www.sosy-lab.org>
 
 SPDX-License-Identifier: Apache-2.0
 -->
diff --git a/.idea/ant.xml.license b/.idea/ant.xml.license
index 5bc96c012f..7e3675eb2b 100644
--- a/.idea/ant.xml.license
+++ b/.idea/ant.xml.license
@@ -3,7 +3,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: 2020 Dirk Beyer <https://www.sosy-lab.org>
+SPDX-FileCopyrightText: 2026 Dirk Beyer <https://www.sosy-lab.org>
 
 SPDX-License-Identifier: Apache-2.0
 -->
diff --git a/.idea/checkstyle-idea.xml.license b/.idea/checkstyle-idea.xml.license
index 5bc96c012f..7e3675eb2b 100644
--- a/.idea/checkstyle-idea.xml.license
+++ b/.idea/checkstyle-idea.xml.license
@@ -3,7 +3,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: 2020 Dirk Beyer <https://www.sosy-lab.org>
+SPDX-FileCopyrightText: 2026 Dirk Beyer <https://www.sosy-lab.org>
 
 SPDX-License-Identifier: Apache-2.0
 -->
diff --git a/.idea/codeStyleSettings.xml.license b/.idea/codeStyleSettings.xml.license
index 5bc96c012f..7e3675eb2b 100644
--- a/.idea/codeStyleSettings.xml.license
+++ b/.idea/codeStyleSettings.xml.license
@@ -3,7 +3,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: 2020 Dirk Beyer <https://www.sosy-lab.org>
+SPDX-FileCopyrightText: 2026 Dirk Beyer <https://www.sosy-lab.org>
 
 SPDX-License-Identifier: Apache-2.0
 -->
diff --git a/.idea/compiler.xml.license b/.idea/compiler.xml.license
index 5bc96c012f..7e3675eb2b 100644
--- a/.idea/compiler.xml.license
+++ b/.idea/compiler.xml.license
@@ -3,7 +3,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: 2020 Dirk Beyer <https://www.sosy-lab.org>
+SPDX-FileCopyrightText: 2026 Dirk Beyer <https://www.sosy-lab.org>
 
 SPDX-License-Identifier: Apache-2.0
 -->
diff --git a/.idea/copyright/JavaSMT.xml.license b/.idea/copyright/JavaSMT.xml.license
index 5bc96c012f..7e3675eb2b 100644
--- a/.idea/copyright/JavaSMT.xml.license
+++ b/.idea/copyright/JavaSMT.xml.license
@@ -3,7 +3,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: 2020 Dirk Beyer <https://www.sosy-lab.org>
+SPDX-FileCopyrightText: 2026 Dirk Beyer <https://www.sosy-lab.org>
 
 SPDX-License-Identifier: Apache-2.0
 -->
diff --git a/.idea/copyright/profiles_settings.xml.license b/.idea/copyright/profiles_settings.xml.license
index 5bc96c012f..7e3675eb2b 100644
--- a/.idea/copyright/profiles_settings.xml.license
+++ b/.idea/copyright/profiles_settings.xml.license
@@ -3,7 +3,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: 2020 Dirk Beyer <https://www.sosy-lab.org>
+SPDX-FileCopyrightText: 2026 Dirk Beyer <https://www.sosy-lab.org>
 
 SPDX-License-Identifier: Apache-2.0
 -->
diff --git a/.idea/encodings.xml.license b/.idea/encodings.xml.license
index 5bc96c012f..7e3675eb2b 100644
--- a/.idea/encodings.xml.license
+++ b/.idea/encodings.xml.license
@@ -3,7 +3,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: 2020 Dirk Beyer <https://www.sosy-lab.org>
+SPDX-FileCopyrightText: 2026 Dirk Beyer <https://www.sosy-lab.org>
 
 SPDX-License-Identifier: Apache-2.0
 -->
diff --git a/.idea/inspectionProfiles/Project_Default.xml.license b/.idea/inspectionProfiles/Project_Default.xml.license
index 5bc96c012f..7e3675eb2b 100644
--- a/.idea/inspectionProfiles/Project_Default.xml.license
+++ b/.idea/inspectionProfiles/Project_Default.xml.license
@@ -3,7 +3,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: 2020 Dirk Beyer <https://www.sosy-lab.org>
+SPDX-FileCopyrightText: 2026 Dirk Beyer <https://www.sosy-lab.org>
 
 SPDX-License-Identifier: Apache-2.0
 -->
diff --git a/.idea/inspectionProfiles/profiles_settings.xml.license b/.idea/inspectionProfiles/profiles_settings.xml.license
index 5bc96c012f..7e3675eb2b 100644
--- a/.idea/inspectionProfiles/profiles_settings.xml.license
+++ b/.idea/inspectionProfiles/profiles_settings.xml.license
@@ -3,7 +3,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: 2020 Dirk Beyer <https://www.sosy-lab.org>
+SPDX-FileCopyrightText: 2026 Dirk Beyer <https://www.sosy-lab.org>
 
 SPDX-License-Identifier: Apache-2.0
 -->
diff --git a/.idea/junitgenerator-prj-settings.xml.license b/.idea/junitgenerator-prj-settings.xml.license
index 5bc96c012f..7e3675eb2b 100644
--- a/.idea/junitgenerator-prj-settings.xml.license
+++ b/.idea/junitgenerator-prj-settings.xml.license
@@ -3,7 +3,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: 2020 Dirk Beyer <https://www.sosy-lab.org>
+SPDX-FileCopyrightText: 2026 Dirk Beyer <https://www.sosy-lab.org>
 
 SPDX-License-Identifier: Apache-2.0
 -->
diff --git a/.idea/misc.xml.license b/.idea/misc.xml.license
index 5bc96c012f..7e3675eb2b 100644
--- a/.idea/misc.xml.license
+++ b/.idea/misc.xml.license
@@ -3,7 +3,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: 2020 Dirk Beyer <https://www.sosy-lab.org>
+SPDX-FileCopyrightText: 2026 Dirk Beyer <https://www.sosy-lab.org>
 
 SPDX-License-Identifier: Apache-2.0
 -->
diff --git a/.idea/modules.xml.license b/.idea/modules.xml.license
index 5bc96c012f..7e3675eb2b 100644
--- a/.idea/modules.xml.license
+++ b/.idea/modules.xml.license
@@ -3,7 +3,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: 2020 Dirk Beyer <https://www.sosy-lab.org>
+SPDX-FileCopyrightText: 2026 Dirk Beyer <https://www.sosy-lab.org>
 
 SPDX-License-Identifier: Apache-2.0
 -->
diff --git a/.idea/vcs.xml.license b/.idea/vcs.xml.license
index 5bc96c012f..7e3675eb2b 100644
--- a/.idea/vcs.xml.license
+++ b/.idea/vcs.xml.license
@@ -3,7 +3,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: 2020 Dirk Beyer <https://www.sosy-lab.org>
+SPDX-FileCopyrightText: 2026 Dirk Beyer <https://www.sosy-lab.org>
 
 SPDX-License-Identifier: Apache-2.0
 -->

From c19311d06d4c21d675deec4ec184865ab8148bf1 Mon Sep 17 00:00:00 2001
From: Daniel Raffler <daniel-raffler@gmx.de>
Date: Thu, 23 Apr 2026 14:00:08 +0200
Subject: [PATCH 20/23] Intellij: Remove all other Nullable/NotNull annotations

---
 .idea/misc.xml | 17 ++---------------
 1 file changed, 2 insertions(+), 15 deletions(-)

diff --git a/.idea/misc.xml b/.idea/misc.xml
index 8ca8685d64..2a7daed4f3 100644
--- a/.idea/misc.xml
+++ b/.idea/misc.xml
@@ -9,32 +9,19 @@
     <option name="myOrdered" value="true" />
     <option name="myNullables">
       <value>
-        <list size="10">
+        <list size="3">
           <item index="0" class="java.lang.String" itemvalue="org.checkerframework.checker.nullness.qual.Nullable" />
           <item index="1" class="java.lang.String" itemvalue="org.checkerframework.checker.nullness.compatqual.NullableDecl" />
           <item index="2" class="java.lang.String" itemvalue="org.checkerframework.checker.nullness.compatqual.NullableType" />
-          <item index="3" class="java.lang.String" itemvalue="javax.annotation.Nullable" />
-          <item index="4" class="java.lang.String" itemvalue="org.jspecify.annotations.Nullable" />
-          <item index="5" class="java.lang.String" itemvalue="org.jetbrains.annotations.Nullable" />
-          <item index="6" class="java.lang.String" itemvalue="org.eclipse.jdt.annotation.Nullable" />
-          <item index="7" class="java.lang.String" itemvalue="edu.umd.cs.findbugs.annotations.Nullable" />
-          <item index="8" class="java.lang.String" itemvalue="jakarta.annotation.Nullable" />
-          <item index="9" class="java.lang.String" itemvalue="javax.annotation.CheckForNull" />
         </list>
       </value>
     </option>
     <option name="myNotNulls">
       <value>
-        <list size="9">
+        <list size="3">
           <item index="0" class="java.lang.String" itemvalue="org.checkerframework.checker.nullness.qual.NonNull" />
           <item index="1" class="java.lang.String" itemvalue="org.checkerframework.checker.nullness.compatqual.NonNullDecl" />
           <item index="2" class="java.lang.String" itemvalue="org.checkerframework.checker.nullness.compatqual.NonNullType" />
-          <item index="3" class="java.lang.String" itemvalue="javax.annotation.Nonnull" />
-          <item index="4" class="java.lang.String" itemvalue="org.jspecify.annotations.NonNull" />
-          <item index="5" class="java.lang.String" itemvalue="org.jetbrains.annotations.NotNull" />
-          <item index="6" class="java.lang.String" itemvalue="org.eclipse.jdt.annotation.NonNull" />
-          <item index="7" class="java.lang.String" itemvalue="edu.umd.cs.findbugs.annotations.NonNull" />
-          <item index="8" class="java.lang.String" itemvalue="jakarta.annotation.Nonnull" />
         </list>
       </value>
     </option>

From 0776ce76d248179330e755544cca474cc7dbcd79 Mon Sep 17 00:00:00 2001
From: BaierD <daniel.baier@sosy.ifi.lmu.de>
Date: Thu, 23 Apr 2026 16:11:26 +0200
Subject: [PATCH 21/23] Remove IntelliJJ library based dependencies and instead
 load all as a single module dependency, avoiding problems when loading
 dependencies

---
 .idea/JavaSMT.iml                       | 70 ++++++++++++++-----------
 .idea/libraries/bitwuzla.xml            | 14 -----
 .idea/libraries/bitwuzla.xml.license    |  9 ----
 .idea/libraries/cvc4.xml                | 14 -----
 .idea/libraries/cvc4.xml.license        |  9 ----
 .idea/libraries/cvc5.xml                | 14 -----
 .idea/libraries/cvc5.xml.license        |  9 ----
 .idea/libraries/opensmt.xml             | 14 -----
 .idea/libraries/opensmt.xml.license     |  9 ----
 .idea/libraries/princess.xml            | 16 ------
 .idea/libraries/princess.xml.license    |  9 ----
 .idea/libraries/smtinterpol.xml         | 15 ------
 .idea/libraries/smtinterpol.xml.license |  9 ----
 .idea/libraries/yices.xml               | 14 -----
 .idea/libraries/yices.xml.license       |  9 ----
 .idea/libraries/z3.xml                  | 14 -----
 .idea/libraries/z3.xml.license          |  9 ----
 .idea/libraries/z3legacy.xml            | 10 ----
 .idea/libraries/z3legacy.xml.license    |  9 ----
 19 files changed, 40 insertions(+), 236 deletions(-)
 delete mode 100644 .idea/libraries/bitwuzla.xml
 delete mode 100644 .idea/libraries/bitwuzla.xml.license
 delete mode 100644 .idea/libraries/cvc4.xml
 delete mode 100644 .idea/libraries/cvc4.xml.license
 delete mode 100644 .idea/libraries/cvc5.xml
 delete mode 100644 .idea/libraries/cvc5.xml.license
 delete mode 100644 .idea/libraries/opensmt.xml
 delete mode 100644 .idea/libraries/opensmt.xml.license
 delete mode 100644 .idea/libraries/princess.xml
 delete mode 100644 .idea/libraries/princess.xml.license
 delete mode 100644 .idea/libraries/smtinterpol.xml
 delete mode 100644 .idea/libraries/smtinterpol.xml.license
 delete mode 100644 .idea/libraries/yices.xml
 delete mode 100644 .idea/libraries/yices.xml.license
 delete mode 100644 .idea/libraries/z3.xml
 delete mode 100644 .idea/libraries/z3.xml.license
 delete mode 100644 .idea/libraries/z3legacy.xml
 delete mode 100644 .idea/libraries/z3legacy.xml.license

diff --git a/.idea/JavaSMT.iml b/.idea/JavaSMT.iml
index 13a12e47a1..fb1bded093 100644
--- a/.idea/JavaSMT.iml
+++ b/.idea/JavaSMT.iml
@@ -16,41 +16,51 @@
       <library>
         <CLASSES>
           <root url="file://$MODULE_DIR$/lib/java/core" />
-        </CLASSES>
-        <JAVADOC />
-        <SOURCES />
-        <jarDirectory url="file://$MODULE_DIR$/lib/java/core" recursive="false" />
-      </library>
-    </orderEntry>
-    <orderEntry type="module-library">
-      <library>
-        <CLASSES>
           <root url="file://$MODULE_DIR$/lib/java/build" />
-        </CLASSES>
-        <JAVADOC />
-        <SOURCES />
-        <jarDirectory url="file://$MODULE_DIR$/lib/java/build" recursive="false" />
-      </library>
-    </orderEntry>
-    <orderEntry type="module-library">
-      <library>
-        <CLASSES>
           <root url="file://$MODULE_DIR$/lib/java/test" />
+          <root url="jar://$MODULE_DIR$/lib/java/runtime-bitwuzla/bitwuzla.jar!/" />
+          <root url="jar://$MODULE_DIR$/lib/java/runtime-opensmt/opensmt.jar!/" />
+          <root url="jar://$MODULE_DIR$/lib/java/runtime-smtinterpol/smtinterpol.jar!/" />
+          <root url="jar://$MODULE_DIR$/lib/java/runtime-princess/scala-library.jar!/" />
+          <root url="jar://$MODULE_DIR$/lib/java/runtime-princess/princess-smt-parser_2.13.jar!/" />
+          <root url="jar://$MODULE_DIR$/lib/java/runtime-princess/princess_2.13.jar!/" />
+          <root url="jar://$MODULE_DIR$/lib/java/runtime-princess/princess-parser_2.13.jar!/" />
+          <root url="jar://$MODULE_DIR$/lib/java/runtime-princess/sourcecode_2.13.jar!/" />
+          <root url="jar://$MODULE_DIR$/lib/java/runtime-princess/org.sat4j.core.jar!/" />
+          <root url="jar://$MODULE_DIR$/lib/java/runtime-cvc5/cvc5.jar!/" />
+          <root url="jar://$MODULE_DIR$/lib/java/runtime-princess/ostrich_2.13.jar!/" />
+          <root url="jar://$MODULE_DIR$/lib/java/runtime-princess/scala-parser-combinators_2.13.jar!/" />
+          <root url="jar://$MODULE_DIR$/lib/java/runtime-princess/ostrich-ecma2020-parser_2.13.jar!/" />
+          <root url="jar://$MODULE_DIR$/lib/java/runtime-princess/geny_2.13.jar!/" />
+          <root url="jar://$MODULE_DIR$/lib/java/runtime-princess/fastparse_2.13.jar!/" />
+          <root url="jar://$MODULE_DIR$/lib/java/runtime-cvc4/CVC4.jar!/" />
+          <root url="jar://$MODULE_DIR$/lib/java/runtime-z3/com.microsoft.z3.jar!/" />
+          <root url="jar://$MODULE_DIR$/lib/java/runtime-z3-legacy/com.microsoft.z3legacy.jar!/" />
         </CLASSES>
-        <JAVADOC />
-        <SOURCES />
+        <JAVADOC>
+          <root url="file://$MODULE_DIR$/lib/java-contrib" />
+        </JAVADOC>
+        <NATIVE>
+          <root url="file://$MODULE_DIR$/lib/java/runtime-z3" />
+          <root url="file://$MODULE_DIR$/lib/java/runtime-bitwuzla" />
+          <root url="file://$MODULE_DIR$/lib/java/runtime-boolector" />
+          <root url="file://$MODULE_DIR$/lib/java/runtime-mathsat" />
+          <root url="file://$MODULE_DIR$/lib/java/runtime-optimathsat" />
+          <root url="file://$MODULE_DIR$/lib/java/runtime-opensmt" />
+          <root url="file://$MODULE_DIR$/lib/java/runtime-cvc4" />
+          <root url="file://$MODULE_DIR$/lib/java/runtime-cvc5" />
+          <root url="file://$MODULE_DIR$/lib/java/runtime-z3-legacy" />
+        </NATIVE>
+        <SOURCES>
+          <root url="file://$MODULE_DIR$/lib/java-contrib" />
+        </SOURCES>
+        <jarDirectory url="file://$MODULE_DIR$/lib/java/build" recursive="false" />
+        <jarDirectory url="file://$MODULE_DIR$/lib/java/core" recursive="false" />
         <jarDirectory url="file://$MODULE_DIR$/lib/java/test" recursive="false" />
+        <jarDirectory url="file://$MODULE_DIR$/lib/java-contrib" recursive="false" type="SOURCES" />
+        <jarDirectory url="file://$MODULE_DIR$/lib/java-contrib" recursive="false" type="JAVADOC" />
       </library>
     </orderEntry>
-    <orderEntry type="library" name="bitwuzla" level="project" />
-    <orderEntry type="library" name="cvc4" level="project" />
-    <orderEntry type="library" name="cvc5" level="project" />
-    <orderEntry type="library" name="opensmt" level="project" />
-    <orderEntry type="library" name="princess" level="project" />
-    <orderEntry type="library" name="smtinterpol" level="project" />
-    <orderEntry type="library" name="yices" level="project" />
-    <orderEntry type="library" name="z3" level="project" />
-    <orderEntry type="library" name="z3legacy" level="project" />
   </component>
   <component name="org.twodividedbyzero.idea.findbugs">
     <option name="_basePreferences">
@@ -257,4 +267,4 @@
       </map>
     </option>
   </component>
-</module>
\ No newline at end of file
+</module>
diff --git a/.idea/libraries/bitwuzla.xml b/.idea/libraries/bitwuzla.xml
deleted file mode 100644
index 8cac34d992..0000000000
--- a/.idea/libraries/bitwuzla.xml
+++ /dev/null
@@ -1,14 +0,0 @@
-<component name="libraryTable">
-  <library name="bitwuzla">
-    <CLASSES>
-      <root url="file://$PROJECT_DIR$/lib/java/runtime-bitwuzla" />
-    </CLASSES>
-    <JAVADOC>
-      <root url="jar://$PROJECT_DIR$/lib/java-contrib/bitwuzla-javadoc.jar!/" />
-    </JAVADOC>
-    <SOURCES>
-      <root url="jar://$PROJECT_DIR$/lib/java-contrib/bitwuzla-sources.jar!/" />
-    </SOURCES>
-    <jarDirectory url="file://$PROJECT_DIR$/lib/java/runtime-bitwuzla" recursive="false" />
-  </library>
-</component>
\ No newline at end of file
diff --git a/.idea/libraries/bitwuzla.xml.license b/.idea/libraries/bitwuzla.xml.license
deleted file mode 100644
index 7e3675eb2b..0000000000
--- a/.idea/libraries/bitwuzla.xml.license
+++ /dev/null
@@ -1,9 +0,0 @@
-<!--
-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 <https://www.sosy-lab.org>
-
-SPDX-License-Identifier: Apache-2.0
--->
diff --git a/.idea/libraries/cvc4.xml b/.idea/libraries/cvc4.xml
deleted file mode 100644
index aaaa482069..0000000000
--- a/.idea/libraries/cvc4.xml
+++ /dev/null
@@ -1,14 +0,0 @@
-<component name="libraryTable">
-  <library name="cvc4">
-    <CLASSES>
-      <root url="file://$PROJECT_DIR$/lib/java/runtime-cvc4" />
-    </CLASSES>
-    <JAVADOC>
-      <root url="jar://$PROJECT_DIR$/lib/java-contrib/CVC4-javadoc.jar!/" />
-    </JAVADOC>
-    <SOURCES>
-      <root url="jar://$PROJECT_DIR$/lib/java-contrib/CVC4-sources.jar!/" />
-    </SOURCES>
-    <jarDirectory url="file://$PROJECT_DIR$/lib/java/runtime-cvc4" recursive="false" />
-  </library>
-</component>
\ No newline at end of file
diff --git a/.idea/libraries/cvc4.xml.license b/.idea/libraries/cvc4.xml.license
deleted file mode 100644
index 7e3675eb2b..0000000000
--- a/.idea/libraries/cvc4.xml.license
+++ /dev/null
@@ -1,9 +0,0 @@
-<!--
-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 <https://www.sosy-lab.org>
-
-SPDX-License-Identifier: Apache-2.0
--->
diff --git a/.idea/libraries/cvc5.xml b/.idea/libraries/cvc5.xml
deleted file mode 100644
index e6a0c1125b..0000000000
--- a/.idea/libraries/cvc5.xml
+++ /dev/null
@@ -1,14 +0,0 @@
-<component name="libraryTable">
-  <library name="cvc5">
-    <CLASSES>
-      <root url="file://$PROJECT_DIR$/lib/java/runtime-cvc5" />
-    </CLASSES>
-    <JAVADOC>
-      <root url="jar://$PROJECT_DIR$/lib/java-contrib/cvc5-javadoc.jar!/" />
-    </JAVADOC>
-    <SOURCES>
-      <root url="jar://$PROJECT_DIR$/lib/java-contrib/cvc5-sources.jar!/" />
-    </SOURCES>
-    <jarDirectory url="file://$PROJECT_DIR$/lib/java/runtime-cvc5" recursive="false" />
-  </library>
-</component>
\ No newline at end of file
diff --git a/.idea/libraries/cvc5.xml.license b/.idea/libraries/cvc5.xml.license
deleted file mode 100644
index 7e3675eb2b..0000000000
--- a/.idea/libraries/cvc5.xml.license
+++ /dev/null
@@ -1,9 +0,0 @@
-<!--
-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 <https://www.sosy-lab.org>
-
-SPDX-License-Identifier: Apache-2.0
--->
diff --git a/.idea/libraries/opensmt.xml b/.idea/libraries/opensmt.xml
deleted file mode 100644
index 1ede9c9fbf..0000000000
--- a/.idea/libraries/opensmt.xml
+++ /dev/null
@@ -1,14 +0,0 @@
-<component name="libraryTable">
-  <library name="opensmt">
-    <CLASSES>
-      <root url="file://$PROJECT_DIR$/lib/java/runtime-opensmt" />
-    </CLASSES>
-    <JAVADOC>
-      <root url="jar://$PROJECT_DIR$/lib/java-contrib/opensmt-javadoc.jar!/" />
-    </JAVADOC>
-    <SOURCES>
-      <root url="jar://$PROJECT_DIR$/lib/java-contrib/opensmt-sources.jar!/" />
-    </SOURCES>
-    <jarDirectory url="file://$PROJECT_DIR$/lib/java/runtime-opensmt" recursive="false" />
-  </library>
-</component>
\ No newline at end of file
diff --git a/.idea/libraries/opensmt.xml.license b/.idea/libraries/opensmt.xml.license
deleted file mode 100644
index 7e3675eb2b..0000000000
--- a/.idea/libraries/opensmt.xml.license
+++ /dev/null
@@ -1,9 +0,0 @@
-<!--
-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 <https://www.sosy-lab.org>
-
-SPDX-License-Identifier: Apache-2.0
--->
diff --git a/.idea/libraries/princess.xml b/.idea/libraries/princess.xml
deleted file mode 100644
index 732fd4b18d..0000000000
--- a/.idea/libraries/princess.xml
+++ /dev/null
@@ -1,16 +0,0 @@
-<component name="libraryTable">
-  <library name="princess">
-    <CLASSES>
-      <root url="file://$PROJECT_DIR$/lib/java/runtime-princess" />
-    </CLASSES>
-    <JAVADOC>
-      <root url="jar://$PROJECT_DIR$/lib/java-contrib/ostrich_2.13-javadoc.jar!/" />
-      <root url="jar://$PROJECT_DIR$/lib/java-contrib/princess_2.13-javadoc.jar!/" />
-    </JAVADOC>
-    <SOURCES>
-      <root url="jar://$PROJECT_DIR$/lib/java-contrib/ostrich_2.13-sources.jar!/" />
-      <root url="jar://$PROJECT_DIR$/lib/java-contrib/princess_2.13-sources.jar!/" />
-    </SOURCES>
-    <jarDirectory url="file://$PROJECT_DIR$/lib/java/runtime-princess" recursive="false" />
-  </library>
-</component>
\ No newline at end of file
diff --git a/.idea/libraries/princess.xml.license b/.idea/libraries/princess.xml.license
deleted file mode 100644
index 7e3675eb2b..0000000000
--- a/.idea/libraries/princess.xml.license
+++ /dev/null
@@ -1,9 +0,0 @@
-<!--
-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 <https://www.sosy-lab.org>
-
-SPDX-License-Identifier: Apache-2.0
--->
diff --git a/.idea/libraries/smtinterpol.xml b/.idea/libraries/smtinterpol.xml
deleted file mode 100644
index 7cd3e27d86..0000000000
--- a/.idea/libraries/smtinterpol.xml
+++ /dev/null
@@ -1,15 +0,0 @@
-<component name="libraryTable">
-  <library name="smtinterpol">
-    <CLASSES>
-      <root url="file://$PROJECT_DIR$/lib/java/runtime-smtinterpol" />
-    </CLASSES>
-    <JAVADOC>
-      <root url="jar://$PROJECT_DIR$/lib/java-contrib/smtinterpol-javadoc.jar!/" />
-    </JAVADOC>
-    <SOURCES>
-      <root url="jar://$PROJECT_DIR$/lib/java-contrib/smtinterpol-sources.jar!/smtinterpol/Library-SMTLIB/src" />
-      <root url="jar://$PROJECT_DIR$/lib/java-contrib/smtinterpol-sources.jar!/smtinterpol/SMTInterpol/src" />
-    </SOURCES>
-    <jarDirectory url="file://$PROJECT_DIR$/lib/java/runtime-smtinterpol" recursive="false" />
-  </library>
-</component>
\ No newline at end of file
diff --git a/.idea/libraries/smtinterpol.xml.license b/.idea/libraries/smtinterpol.xml.license
deleted file mode 100644
index 7e3675eb2b..0000000000
--- a/.idea/libraries/smtinterpol.xml.license
+++ /dev/null
@@ -1,9 +0,0 @@
-<!--
-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 <https://www.sosy-lab.org>
-
-SPDX-License-Identifier: Apache-2.0
--->
diff --git a/.idea/libraries/yices.xml b/.idea/libraries/yices.xml
deleted file mode 100644
index 63053f86b9..0000000000
--- a/.idea/libraries/yices.xml
+++ /dev/null
@@ -1,14 +0,0 @@
-<component name="libraryTable">
-  <library name="yices">
-    <CLASSES>
-      <root url="file://$PROJECT_DIR$/lib/java/runtime-yices2" />
-    </CLASSES>
-    <JAVADOC>
-      <root url="jar://$PROJECT_DIR$/lib/java-contrib/yices-javadoc.jar!/" />
-    </JAVADOC>
-    <SOURCES>
-      <root url="jar://$PROJECT_DIR$/lib/java-contrib/yices-sources.jar!/" />
-    </SOURCES>
-    <jarDirectory url="file://$PROJECT_DIR$/lib/java/runtime-yices2" recursive="false" />
-  </library>
-</component>
\ No newline at end of file
diff --git a/.idea/libraries/yices.xml.license b/.idea/libraries/yices.xml.license
deleted file mode 100644
index 7e3675eb2b..0000000000
--- a/.idea/libraries/yices.xml.license
+++ /dev/null
@@ -1,9 +0,0 @@
-<!--
-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 <https://www.sosy-lab.org>
-
-SPDX-License-Identifier: Apache-2.0
--->
diff --git a/.idea/libraries/z3.xml b/.idea/libraries/z3.xml
deleted file mode 100644
index fa33e192e7..0000000000
--- a/.idea/libraries/z3.xml
+++ /dev/null
@@ -1,14 +0,0 @@
-<component name="libraryTable">
-  <library name="z3">
-    <CLASSES>
-      <root url="file://$PROJECT_DIR$/lib/java/runtime-z3" />
-    </CLASSES>
-    <JAVADOC>
-      <root url="jar://$PROJECT_DIR$/lib/java-contrib/com.microsoft.z3-javadoc.jar!/" />
-    </JAVADOC>
-    <SOURCES>
-      <root url="jar://$PROJECT_DIR$/lib/java-contrib/com.microsoft.z3-sources.jar!/" />
-    </SOURCES>
-    <jarDirectory url="file://$PROJECT_DIR$/lib/java/runtime-z3" recursive="false" />
-  </library>
-</component>
\ No newline at end of file
diff --git a/.idea/libraries/z3.xml.license b/.idea/libraries/z3.xml.license
deleted file mode 100644
index 7e3675eb2b..0000000000
--- a/.idea/libraries/z3.xml.license
+++ /dev/null
@@ -1,9 +0,0 @@
-<!--
-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 <https://www.sosy-lab.org>
-
-SPDX-License-Identifier: Apache-2.0
--->
diff --git a/.idea/libraries/z3legacy.xml b/.idea/libraries/z3legacy.xml
deleted file mode 100644
index 8b0924407c..0000000000
--- a/.idea/libraries/z3legacy.xml
+++ /dev/null
@@ -1,10 +0,0 @@
-<component name="libraryTable">
-  <library name="z3legacy">
-    <CLASSES>
-      <root url="file://$PROJECT_DIR$/lib/java/runtime-z3-legacy" />
-    </CLASSES>
-    <JAVADOC />
-    <SOURCES />
-    <jarDirectory url="file://$PROJECT_DIR$/lib/java/runtime-z3-legacy" recursive="false" />
-  </library>
-</component>
\ No newline at end of file
diff --git a/.idea/libraries/z3legacy.xml.license b/.idea/libraries/z3legacy.xml.license
deleted file mode 100644
index 7e3675eb2b..0000000000
--- a/.idea/libraries/z3legacy.xml.license
+++ /dev/null
@@ -1,9 +0,0 @@
-<!--
-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 <https://www.sosy-lab.org>
-
-SPDX-License-Identifier: Apache-2.0
--->

From fda8a791cbdc228b3f8d24d302c520481cc8f9ce Mon Sep 17 00:00:00 2001
From: BaierD <daniel.baier@sosy.ifi.lmu.de>
Date: Thu, 23 Apr 2026 16:19:16 +0200
Subject: [PATCH 22/23] Add Yices2 to IntelliJJ dependencies settings

---
 .idea/JavaSMT.iml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/.idea/JavaSMT.iml b/.idea/JavaSMT.iml
index fb1bded093..48fe7158ce 100644
--- a/.idea/JavaSMT.iml
+++ b/.idea/JavaSMT.iml
@@ -36,6 +36,7 @@
           <root url="jar://$MODULE_DIR$/lib/java/runtime-cvc4/CVC4.jar!/" />
           <root url="jar://$MODULE_DIR$/lib/java/runtime-z3/com.microsoft.z3.jar!/" />
           <root url="jar://$MODULE_DIR$/lib/java/runtime-z3-legacy/com.microsoft.z3legacy.jar!/" />
+          <root url="jar://$MODULE_DIR$/lib/java/runtime-yices2/yices.jar!/" />
         </CLASSES>
         <JAVADOC>
           <root url="file://$MODULE_DIR$/lib/java-contrib" />
@@ -50,6 +51,7 @@
           <root url="file://$MODULE_DIR$/lib/java/runtime-cvc4" />
           <root url="file://$MODULE_DIR$/lib/java/runtime-cvc5" />
           <root url="file://$MODULE_DIR$/lib/java/runtime-z3-legacy" />
+          <root url="file://$MODULE_DIR$/lib/java/runtime-yices2" />
         </NATIVE>
         <SOURCES>
           <root url="file://$MODULE_DIR$/lib/java-contrib" />
@@ -57,8 +59,8 @@
         <jarDirectory url="file://$MODULE_DIR$/lib/java/build" recursive="false" />
         <jarDirectory url="file://$MODULE_DIR$/lib/java/core" recursive="false" />
         <jarDirectory url="file://$MODULE_DIR$/lib/java/test" recursive="false" />
-        <jarDirectory url="file://$MODULE_DIR$/lib/java-contrib" recursive="false" type="SOURCES" />
         <jarDirectory url="file://$MODULE_DIR$/lib/java-contrib" recursive="false" type="JAVADOC" />
+        <jarDirectory url="file://$MODULE_DIR$/lib/java-contrib" recursive="false" type="SOURCES" />
       </library>
     </orderEntry>
   </component>

From aebba6694ab377dcc5c58dd85cd965edbd9143a0 Mon Sep 17 00:00:00 2001
From: BaierD <daniel.baier@sosy.ifi.lmu.de>
Date: Thu, 23 Apr 2026 16:46:19 +0200
Subject: [PATCH 23/23] Add explicit path for JavaDoc Jars to IntelliJ settings

---
 .idea/JavaSMT.iml | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/.idea/JavaSMT.iml b/.idea/JavaSMT.iml
index 48fe7158ce..b051361b77 100644
--- a/.idea/JavaSMT.iml
+++ b/.idea/JavaSMT.iml
@@ -3,6 +3,18 @@
   <component name="NewModuleRootManager">
     <output url="file://$MODULE_DIR$/bin" />
     <exclude-output />
+    <javadoc-paths>
+      <root url="jar://$MODULE_DIR$/lib/java-contrib/bitwuzla-javadoc.jar!/" />
+      <root url="jar://$MODULE_DIR$/lib/java-contrib/com.microsoft.z3-javadoc.jar!/" />
+      <root url="jar://$MODULE_DIR$/lib/java-contrib/CVC4-javadoc.jar!/" />
+      <root url="jar://$MODULE_DIR$/lib/java-contrib/cvc5-javadoc.jar!/" />
+      <root url="jar://$MODULE_DIR$/lib/java-contrib/javasmt-yices2-javadoc.jar!/" />
+      <root url="jar://$MODULE_DIR$/lib/java-contrib/opensmt-javadoc.jar!/" />
+      <root url="jar://$MODULE_DIR$/lib/java-contrib/ostrich_2.13-javadoc.jar!/" />
+      <root url="jar://$MODULE_DIR$/lib/java-contrib/princess_2.13-javadoc.jar!/" />
+      <root url="jar://$MODULE_DIR$/lib/java-contrib/smtinterpol-javadoc.jar!/" />
+      <root url="jar://$MODULE_DIR$/lib/java-contrib/yices-javadoc.jar!/" />
+    </javadoc-paths>
     <content url="file://$MODULE_DIR$">
       <sourceFolder url="file://$MODULE_DIR$/src" isTestSource="false" />
       <excludeFolder url="file://$MODULE_DIR$/JUnit-coverage" />