diff --git a/.idea/JavaSMT.iml b/.idea/JavaSMT.iml
index 47bdfebbd0..13a12e47a1 100644
--- a/.idea/JavaSMT.iml
+++ b/.idea/JavaSMT.iml
@@ -1,390 +1,56 @@
 <?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" />
     <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" />
       <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>
         <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!/" />
-        </CLASSES>
-        <JAVADOC />
-        <SOURCES />
-      </library>
-    </orderEntry>
-    <orderEntry type="module-library">
-      <library>
-        <CLASSES>
-          <root url="jar://$MODULE_DIR$/lib/java/test/diffutils.jar!/" />
-        </CLASSES>
-        <JAVADOC />
-        <SOURCES />
-      </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!/" />
-        </CLASSES>
-        <JAVADOC />
-        <SOURCES />
-      </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/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/runtime-princess/princess-smt-parser_2.13.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/runtime-princess/scala-library.jar!/" />
+          <root url="file://$MODULE_DIR$/lib/java/test" />
         </CLASSES>
         <JAVADOC />
         <SOURCES />
-      </library>
-    </orderEntry>
-    <orderEntry type="module-library">
-      <library>
-        <CLASSES>
-          <root url="jar://$MODULE_DIR$/lib/java/runtime-princess/java-cup-runtime.jar!/" />
-        </CLASSES>
-        <JAVADOC />
-        <SOURCES />
-      </library>
-    </orderEntry>
-    <orderEntry type="module-library">
-      <library>
-        <CLASSES>
-          <root url="jar://$MODULE_DIR$/lib/java/test/hamcrest-core.jar!/" />
-        </CLASSES>
-        <JAVADOC />
-        <SOURCES />
-      </library>
-    </orderEntry>
-    <orderEntry type="module-library">
-      <library>
-        <CLASSES>
-          <root url="jar://$MODULE_DIR$/lib/java/build/error_prone_annotations.jar!/" />
-        </CLASSES>
-        <JAVADOC />
-        <SOURCES />
-      </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!/" />
-        </CLASSES>
-        <JAVADOC />
-        <SOURCES />
-      </library>
-    </orderEntry>
-    <orderEntry type="module-library">
-      <library>
-        <CLASSES>
-          <root url="jar://$MODULE_DIR$/lib/java/runtime-princess/smt-parser.jar!/" />
-        </CLASSES>
-        <JAVADOC />
-        <SOURCES />
-      </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!/" />
-        </CLASSES>
-        <JAVADOC />
-        <SOURCES />
-      </library>
-    </orderEntry>
+        <jarDirectory url="file://$MODULE_DIR$/lib/java/test" 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">
@@ -591,4 +257,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/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..aaaa482069
--- /dev/null
+++ b/.idea/libraries/cvc4.xml
@@ -0,0 +1,14 @@
+<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
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..e6a0c1125b
--- /dev/null
+++ b/.idea/libraries/cvc5.xml
@@ -0,0 +1,14 @@
+<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
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..732fd4b18d
--- /dev/null
+++ b/.idea/libraries/princess.xml
@@ -0,0 +1,16 @@
+<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
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..7cd3e27d86
--- /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="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
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..63053f86b9
--- /dev/null
+++ b/.idea/libraries/yices.xml
@@ -0,0 +1,14 @@
+<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
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/.idea/misc.xml b/.idea/misc.xml
index 79d44e380e..8ca8685d64 100644
--- a/.idea/misc.xml
+++ b/.idea/misc.xml
@@ -1,52 +1,40 @@
 <?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" />
   </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>
-        <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" />
-          <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" />
+        <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="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="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" />
-          <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" />
+        <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="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>
@@ -54,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
+-->
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. -->