Z3 update (#254)

* Bumped version

* Added legacy solver

* Added dep to build

* Renamed package

* Updated to use legacy version

* Updated libraries

* Moved to using internal theta zip

* Disabled tests on Mac

* Updated README

* Updated name of new Z3

* Disabled macos-11 test

* Fixed versioning of legacy solver

* Skipping interpolation tests on mac

* Removed junit engine from deps

* Modified dylibs

* Retrying mac support for itp

* Added retry step, and corrected dependency

* Retry pattern on more commands

.github/actions/benchexec-test/action.yml

@@ -20,29 +20,32 @@ runs:
       run: |
         mkdir -p xml
         cp $GITHUB_ACTION_PATH/theta.xml xml/
-    - name: Get sv-benchmarks
-      shell: bash
-      run: |
-        git clone --filter=blob:none --no-checkout --depth 1 --sparse https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks.git
-        cd sv-benchmarks
-        git sparse-checkout add c
-        git checkout
-    - name: Get archive
-      shell: bash
-      run: |
-        wget https://github.com/ftsrg/theta/releases/download/svcomp24/theta.zip
-        unzip theta.zip
-        mv Theta theta
+    - name: Get sv-benchmarks (retry max. 3 times)
+      uses: nick-fields/retry@7152eba30c6575329ac0576536151aca5a72780e # v3.0.0
+      with:
+        timeout_minutes: 15
+        max_attempts: 3
+        shell: bash
+        command: git clone --filter=blob:none --no-checkout --depth 1 --sparse https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks.git
+    - name: Get C folder (retry max. 3 times)
+      uses: nick-fields/retry@7152eba30c6575329ac0576536151aca5a72780e # v3.0.0
+      with:
+        timeout_minutes: 15
+        max_attempts: 3
+        shell: bash
+        command: |
+          cd sv-benchmarks
+          git sparse-checkout add c
+          git checkout
     - uses: actions/download-artifact@9bc31d5ccc31df68ecc42ccf4149144866c47d8a # v3.0.2
-      name: Get JAR
+      name: Get zip
       with:
-        name: ThetaJars
-        path: jar/
-    - name: Add new jar to archive
+        name: Theta_SV-COMP
+        path: release/
+    - name: Unzip 
       shell: bash
       run: |
-        mv jar/xcfa/xcfa-cli/build/libs/*-all.jar theta/theta.jar
-        ls -l theta
+        unzip release/Theta.zip
     - name: Cut setfile if too long
       id: setfile 
       shell: bash
@@ -56,7 +59,7 @@ runs:
       shell: bash
       if: steps.setfile.outputs.length != '0'
       run: |
-        benchexec xml/theta.xml --no-container --tool-directory theta -t ${{ inputs.task }}
+        benchexec xml/theta.xml --no-container --tool-directory Theta -t ${{ inputs.task }}
     - name: Upload results
       uses: actions/upload-artifact@0b7f8abb1508181956e8e162db84b466c27e18ce # v3.1.2
       if: steps.setfile.outputs.length != '0'

.github/actions/cache-build/action.yml

@@ -16,5 +16,5 @@ runs:
     - name: build gradle
       uses: gradle/gradle-build-action@40b6781dcdec2762ad36556682ac74e31030cfe2 # v2.5.1
       with:
-        arguments: ${{ inputs.arguments }}
+        arguments: ${{ inputs.arguments }} --info --stacktrace
 

.github/workflows/linux-build-test-deploy.yml

@@ -51,7 +51,7 @@ jobs:
       matrix:
         task: [ReachSafety-Arrays, ReachSafety-BitVectors, ReachSafety-ControlFlow, ReachSafety-ECA, ReachSafety-Floats, ReachSafety-Heap, ReachSafety-Loops, ReachSafety-ProductLines, ReachSafety-Recursive, ReachSafety-Sequentialized, ReachSafety-XCSP, ReachSafety-Combinations, ReachSafety-Hardware, ConcurrencySafety-Main, NoDataRace-Main, ConcurrencySafety-NoOverflows, ConcurrencySafety-MemSafety]
     runs-on: ubuntu-latest
-    needs: build
+    needs: create-archives
     steps:
       - name: Checkout repository
         uses: actions/checkout@c85c95e3d7251135ab7dc9ce3241c5835cc595a9 # v3.5.3

.github/workflows/mac-build-test.yml

@@ -15,7 +15,7 @@ jobs:
     strategy:
       fail-fast: false
       matrix:
-        os: [macos-latest, macos-13, macos-12, macos-11]
+        os: [macos-latest, macos-13, macos-12]
     runs-on: ${{ matrix.os }}
     steps:
       - name: Checkout repository

build.gradle.kts

@@ -28,7 +28,7 @@ buildscript {
 
 allprojects {
     group = "hu.bme.mit.theta"
-    version = "5.0.1"
+    version = "5.0.2"
 
     apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts"))
 }

buildSrc/src/main/kotlin/Deps.kt

@@ -13,6 +13,7 @@
  *  See the License for the specific language governing permissions and
  *  limitations under the License.
  */
+
 object Deps {
 
     val guava = "com.google.guava:guava:${Versions.guava}"
@@ -25,6 +26,7 @@ object Deps {
     }
 
     val z3 = "lib/com.microsoft.z3.jar"
+    val z3legacy = "lib/com.microsoft.z3legacy.jar"
 
     val jcommander = "com.beust:jcommander:${Versions.jcommander}"