Update solvers in our example projects

doc/Example-Gradle-Project-Kotlin/build.gradle.kts

@@ -12,27 +12,30 @@ import org.jetbrains.kotlin.gradle.tasks.KotlinCompile
 
 plugins {
     // Apply the kotlin.jvm plugin to add support for Kotlin.
-    kotlin("jvm") version "1.6.21"
+    kotlin("jvm") version "2.3.21"
 
     // Apply the application plugin to add support for building a CLI application in Java.
     application
 }
 
-// Set the used Java version
-java.sourceCompatibility = JavaVersion.VERSION_11
-
 // Globally define versions used for our dependencies
-val javasmtVersion = "3.12.0"
-val javasmtYices2Version = "3.12.0"
-val junit4Version = "4.13"
-val z3Version = "4.8.17"
-val smtInterpolVersion = "2.5-916-ga5843d8b"
+val javasmtVersion = "6.0.0-148-gba08f432a"
+val javasmtYices2Version = "6.0.0-141-g04134287c"
+
+val bitwuzlaVersion = "0.9.0-gd13ef925"
 val boolectorVersion = "3.2.2-g1a89c229"
 val cvc4Version = "1.8-prerelease-2020-06-24-g7825d8f28"
-val mathsat5Version = "5.6.6-sosy1"
-val optiMathsat5Version = "1.7.1-sosy0"
-val yices2Version = "2.6.2-396-g194350c1"
-val princessVersion = "2021-11-15"
+val cvc5Version = "2026-02-26-d22638a"
+val mathsat5Version = "5.6.15"
+val opensmtVersion = "2.9.2-ge4c80308"
+val smtInterpolVersion = "2.5-1242-g5c50fb6d"
+val princessVersion = "2025-11-17"
+val ostrichVersion = "2.0"
+val yices2Version = "2.7.0-gdc5687ca"
+val z3Version = "4.16.0"
+val z3LegacyVersion = "4.5.0-gd57a2a6dc"
+
+val junit6Version = "6.1.0"
 
 repositories {
     // Use MavenCentral as a source, but try using POMs first and if that fails just use the artifact
@@ -59,54 +62,70 @@ repositories {
     }
 }
 
+val architecture = "x64"
+
 dependencies {
     // Align versions of all Kotlin components
-    //implementation(platform("org.jetbrains.kotlin:kotlin-bom"))
-
-    // Use the Kotlin JDK 11 standard library.
-    //implementation("org.jetbrains.kotlin:kotlin-stdlib-jdk11")
+    implementation(platform("org.jetbrains.kotlin:kotlin-bom"))
 
-    // JUnit 4
-	testImplementation("junit:junit:$junit4Version")
+    // JUnit
+    testImplementation("org.junit.jupiter:junit-jupiter-api:$junit6Version")
+    testImplementation("org.junit.jupiter:junit-jupiter-params:$junit6Version")
+    testImplementation("org.junit.jupiter:junit-jupiter-engine:$junit6Version")
 
     // JavaSMT dependencies
     implementation("org.sosy-lab:java-smt:$javasmtVersion")
 
     // JavaSMT solver dependencies
+    // Princess
+    implementation("io.github.uuverifiers:princess_2.13:$princessVersion")
+    implementation("io.github.uuverifiers:ostrich_2.13:$ostrichVersion")
+
+    // SMTInterpol
+    implementation("de.uni-freiburg.informatik.ultimate:smtinterpol:$smtInterpolVersion")
+
+    // Mathsat5
+    runtimeOnly("org.sosy-lab:javasmt-solver-mathsat:$mathsat5Version:libmathsat5j-${architecture}@so")
+
     // Z3
-    runtimeOnly("org.sosy-lab:javasmt-solver-z3:$z3Version:com.microsoft.z3@jar")
-    runtimeOnly("org.sosy-lab:javasmt-solver-z3:$z3Version:libz3@so")
-    runtimeOnly("org.sosy-lab:javasmt-solver-z3:$z3Version:libz3java@so")
-
-    runtimeOnly("org.sosy-lab:javasmt-solver-mathsat5:$mathsat5Version:libmathsat5j@so")
+    runtimeOnly("org.sosy-lab:javasmt-solver-z3:$z3Version@jar")
+    runtimeOnly("org.sosy-lab:javasmt-solver-z3:$z3Version:libz3-${architecture}@so")
+    runtimeOnly("org.sosy-lab:javasmt-solver-z3:$z3Version:libz3java-${architecture}@so")
 
-    // Retrieve OptiMathSAT via Ivy (as it is currently not available in Maven)
-	runtimeOnly("org.sosy_lab:javasmt-solver-optimathsat:$optiMathsat5Version:liboptimathsat5j@so")
+    // Z3 4.5
+    runtimeOnly("org.sosy-lab:javasmt-solver-z3-legacy:$z3LegacyVersion:com.microsoft.z3legacy@jar")
+    runtimeOnly("org.sosy-lab:javasmt-solver-z3-legacy:$z3LegacyVersion:libz3legacy-${architecture}@so")
+    runtimeOnly("org.sosy-lab:javasmt-solver-z3-legacy:$z3LegacyVersion:libz3javalegacy-${architecture}@so")
 
-    // Retrieve CVC4 via Maven
+    // Bitwuzla
+    runtimeOnly("org.sosy-lab:javasmt-solver-bitwuzla:$bitwuzlaVersion@jar")
+    runtimeOnly("org.sosy-lab:javasmt-solver-bitwuzla:$bitwuzlaVersion:libbitwuzlaj-${architecture}@so")
+
+    // CVC4
     runtimeOnly("org.sosy-lab:javasmt-solver-cvc4:$cvc4Version:CVC4@jar")
     runtimeOnly("org.sosy-lab:javasmt-solver-cvc4:$cvc4Version:libcvc4@so")
     runtimeOnly("org.sosy-lab:javasmt-solver-cvc4:$cvc4Version:libcvc4jni@so")
     runtimeOnly("org.sosy-lab:javasmt-solver-cvc4:$cvc4Version:libcvc4parser@so")
 
-    // Retrieve Boolector via Maven
+    // CVC5
+    runtimeOnly("org.sosy-lab:javasmt-solver-cvc5:$cvc5Version@jar")
+    runtimeOnly("org.sosy-lab:javasmt-solver-cvc5:$cvc5Version:libcvc5jni-${architecture}@so")
+
+    // Boolector
     runtimeOnly("org.sosy-lab:javasmt-solver-boolector:$boolectorVersion:libboolector@so")
     runtimeOnly("org.sosy-lab:javasmt-solver-boolector:$boolectorVersion:libminisat@so")
     runtimeOnly("org.sosy-lab:javasmt-solver-boolector:$boolectorVersion:libpicosat@so")
 
-    // Retrieve Princess
-    runtimeOnly("io.github.uuverifiers:princess_2.13:$princessVersion@jar")
-
-    // Retrieve SMTInterpol
-    runtimeOnly("de.uni-freiburg.informatik.ultimate:smtinterpol:$smtInterpolVersion@jar")
-
-    // Example as to how to use Yices2
-    // First get JavaSMT for Yices2 from Maven (if you want to use only Yices2 use this dependency in the "implementation" part above instead of regual JavaSMT)
+    // Yices2
     runtimeOnly("org.sosy-lab:javasmt-yices2:$javasmtYices2Version@jar")
-    // And the Yices2 solver from Maven
-    runtimeOnly("org.sosy-lab:javasmt-solver-yices2:$yices2Version:libyices2j@so")
-
+    runtimeOnly("org.sosy-lab:javasmt-solver-yices2:$yices2Version@jar")
+    runtimeOnly("org.sosy-lab:javasmt-solver-yices2:$yices2Version:libyices2java-${architecture}@so")
+
+    // OpenSMT
+    runtimeOnly("org.sosy-lab:javasmt-solver-opensmt:$opensmtVersion@jar")
+    runtimeOnly("org.sosy-lab:javasmt-solver-opensmt:$opensmtVersion:libopensmtj-${architecture}@so")
 
+    // Tell implementation config to use the JavaSMT + dependencies from our dependencies folder
     implementation(fileTree("dir" to "build/dependencies", "include" to "*.jar"))
 }
 
@@ -126,11 +145,6 @@ application {
     mainClass.set("org.sosy_lab.java_smt_example.JavaSMTKotlinExampleKt")
 }
 
-// compile bytecode to java 11
-tasks.withType<KotlinCompile> {
-    kotlinOptions.jvmTarget = "11"
-}
-
 // Use a config to identify JavaSMT components
 configurations {
     register("javaSMTConfig").configure {
@@ -171,4 +185,4 @@ tasks.withType<Tar> {
 
 tasks.withType<Zip>{
     duplicatesStrategy = DuplicatesStrategy.EXCLUDE
-}
+}