Add IC3/PDR engine for unbounded safety verification

.github/workflows/test.yml

@@ -105,13 +105,33 @@ jobs:
       run: sbt universal:packageBin
 
   test-macos:
-    runs-on: macos-13
+    runs-on: macos-14
 
     steps:
     - uses: actions/checkout@v2
-    - uses: olafurpg/setup-scala@v10
+
+    - name: Set up JDK 11
+      uses: actions/setup-java@v4
+      with:
+        distribution: 'zulu'
+        java-version: '11'
+
+    - name: Cache SBT ivy cache
+      uses: actions/cache@v4
       with:
-        java-version: openjdk@1.11
+        path: ~/.ivy2/cache
+        key: ${{ runner.os }}-sbt-ivy-cache-${{ hashFiles('**/build.sbt') }}
+
+    - name: Cache SBT
+      uses: actions/cache@v4
+      with:
+        path: ~/.sbt
+        key: ${{ runner.os }}-sbt-${{ hashFiles('**/build.sbt') }}
+
+    - name: Set up SBT
+      uses: coursier/setup-action@v1
+      with:
+        apps: sbt
 
     - name: Cache Z3
       id: cache-z3

build.sbt

@@ -15,6 +15,16 @@ libraryDependencies += "org.scalatest" %% "scalatest" % "3.2.2" % "test"
 libraryDependencies += "com.github.scopt" %% "scopt" % "3.7.1"
 libraryDependencies += "org.json4s" %% "json4s-jackson" % "4.0.3"
 
+// Fork the JVM for run/test so that javaOptions take effect. The java.library.path
+// setting is needed for Z3 JNI native library loading (libz3java). While the setup
+// scripts (setup-z3-linux.sh, etc.) set LD_LIBRARY_PATH for shell use, java.library.path
+// must be set at JVM startup to locate native libraries when running via sbt.
+fork in run := true
+javaOptions in run += s"-Djava.library.path=${baseDirectory.value}/z3/bin"
+
+fork in Test := true
+javaOptions in Test += s"-Djava.library.path=${baseDirectory.value}/z3/bin"
+
 // do not require tests before building a fat JAR
 test in assembly := {}