Upgrade z3 version to 4.12.5 (#148)

* Upgrade z3 version to 4.12.4 * Core: fix fp-fma rounding * Z3: upgrade to 4.12.5 * More fp tests * update github actions * Escape gradle args for windows * Upgrade version to 0.5.17
UnitTestBot · Jan 30, 2024 · eaedb86 · eaedb86
1 parent c1335bb
commit eaedb86
Show file tree

Hide file tree

Showing 15 changed files with 123 additions and 296 deletions.
diff --git a/.github/workflows/build-and-run-tests.yml b/.github/workflows/build-and-run-tests.yml
@@ -20,37 +20,28 @@ jobs:
     runs-on: ${{ matrix.os }}
 
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
 
       - name: Set up JDK 1.8
-        uses: actions/setup-java@v3
+        uses: actions/setup-java@v4
         with:
           java-version: 8
           distribution: 'zulu'
           cache: gradle
 
+      - name: Setup gradle
+        uses: gradle/actions/setup-gradle@v3
+
       - name: Build and run z3 tests on macOS
-        uses: gradle/gradle-build-action@v2
         if: runner.os == 'macOS'
-        with:
-          arguments: |
-            :ksmt-z3:build
-             --no-daemon
-             --continue
-             -PrunBenchmarksBasedTests=false
+        run: ./gradlew :ksmt-z3:build --no-daemon --continue -PrunBenchmarksBasedTests=false
 
       - name: Build and run simple tests on Linux or Windows
-        uses: gradle/gradle-build-action@v2
         if: runner.os != 'macOS'
-        with:
-          arguments: |
-            build
-             --no-daemon
-             --continue
-             -PrunBenchmarksBasedTests=false
+        run: ./gradlew build --no-daemon --continue -PrunBenchmarksBasedTests=false
 
       - name: Upload ksmt test reports
-        uses: actions/upload-artifact@v3
+        uses: actions/upload-artifact@v4
         if: always()
         with:
           name: ksmt-tests-report-${{ matrix.os }}

diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml
@@ -10,19 +10,21 @@ jobs:
     runs-on: ubuntu-latest
 
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
 
       - name: Set up JDK 1.8
-        uses: actions/setup-java@v3
+        uses: actions/setup-java@v4
         with:
           java-version: 8
           distribution: 'zulu'
           cache: gradle
 
+      - name: Setup gradle
+        uses: gradle/actions/setup-gradle@v3
+
       - name: Build artifacts
-        uses: gradle/gradle-build-action@v2
-        with:
-          arguments: |
+        run: >
+            ./gradlew
             publishAllPublicationsToCentralRepository
             publishAllPublicationsToReleaseDirRepository
             --no-daemon

diff --git a/.github/workflows/run-long-tests.yml b/.github/workflows/run-long-tests.yml
@@ -69,11 +69,11 @@ jobs:
     runs-on: ${{ matrix.os }}
 
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
 
       - name: Prepare test data (cache)
         id: test-data-cache
-        uses: actions/cache@v3
+        uses: actions/cache@v4
         env:
           cache-name: cache-test-data
         with:
@@ -82,20 +82,23 @@ jobs:
 
       - name: Set up JDK 1.8
         if: steps.test-data-cache.outputs.cache-hit != 'true'
-        uses: actions/setup-java@v3
+        uses: actions/setup-java@v4
         with:
           java-version: 8
           distribution: 'zulu'
           cache: gradle
 
+      - name: Setup gradle
+        if: steps.test-data-cache.outputs.cache-hit != 'true'
+        uses: gradle/actions/setup-gradle@v3
+
       - name: Prepare test data (download)
         if: steps.test-data-cache.outputs.cache-hit != 'true'
-        uses: gradle/gradle-build-action@v2
-        with:
-          arguments: |
+        run: >
+            ./gradlew
             :ksmt-test:downloadPreparedSmtLibBenchmarkTestData
             --no-daemon
-            -PtestDataRevision=${{ env.TEST_DATA_REVISION }}
+            '-PtestDataRevision=${{ env.TEST_DATA_REVISION }}'
 
   run_tests:
     needs: [setup, prepare_test_data]
@@ -111,11 +114,11 @@ jobs:
     runs-on: ${{ matrix.os }}
 
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
 
       - name: Prepare test data (cache)
         id: test-data-cache
-        uses: actions/cache@v3
+        uses: actions/cache@v4
         env:
           cache-name: cache-test-data
         with:
@@ -129,34 +132,31 @@ jobs:
           exit 1
 
       - name: Set up JDK 1.8
-        uses: actions/setup-java@v3
+        uses: actions/setup-java@v4
         with:
           java-version: 8
           distribution: 'zulu'
           cache: gradle
 
+      - name: Setup gradle
+        uses: gradle/actions/setup-gradle@v3
+
       # Since ksmt-test/testData/testData.zip exists task will not download it again
       - name: Prepare test data (unpack)
-        uses: gradle/gradle-build-action@v2
-        with:
-          arguments: |
+        run: >
+            ./gradlew
             :ksmt-test:downloadPreparedSmtLibBenchmarkTestData
             --no-daemon
-            -PtestDataRevision=${{ env.TEST_DATA_REVISION }}
+            '-PtestDataRevision=${{ env.TEST_DATA_REVISION }}'
 
       # We don't want to run basic KSMT tests on each chunk
       - name: Build project
-        uses: gradle/gradle-build-action@v2
         if: ${{ matrix.chunk == '0' }}
-        with:
-          arguments: |
-            build
-            --no-daemon
+        run: ./gradlew build --no-daemon
 
       - name: Run ${{ matrix.test }}
-        uses: gradle/gradle-build-action@v2
-        with:
-          arguments: |
+        run: >
+            ./gradlew
             :ksmt-test:test --tests  ${{ format('"io.ksmt.test.benchmarks.{0}"', matrix.test) }}
             --no-daemon
             --continue
@@ -165,7 +165,7 @@ jobs:
             -PbenchmarkChunk=${{ matrix.chunk }}
 
       - name: Upload ksmt test reports
-        uses: actions/upload-artifact@v3
+        uses: actions/upload-artifact@v4
         if: always()
         with:
           name: ${{ format('ksmt-test-report-{0}-{1}-{2}', matrix.os, matrix.test, matrix.chunk) }}
@@ -179,36 +179,37 @@ jobs:
     if: ${{ always() }}
 
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
 
-      - uses: actions/download-artifact@v3
+      - uses: actions/download-artifact@v4
         with:
           path: reports
 
       - name: Set up JDK 1.8
-        uses: actions/setup-java@v3
+        uses: actions/setup-java@v4
         with:
           java-version: 8
           distribution: 'zulu'
 
+      - name: Setup gradle
+        uses: gradle/actions/setup-gradle@v3
+
       - name: Merge test report [ubuntu-latest]
-        uses: gradle/gradle-build-action@v2
-        with:
-          arguments: |
+        run: >
+            ./gradlew
             :ksmt-test:mergeTestReports
             --no-daemon
             -PtestReportMergePrefix=ksmt-test-report-ubuntu-latest
 
       - name: Merge test report [windows-latest]
-        uses: gradle/gradle-build-action@v2
-        with:
-          arguments: |
+        run: >
+            ./gradlew
             :ksmt-test:mergeTestReports
             --no-daemon
             -PtestReportMergePrefix=ksmt-test-report-windows-latest
             
       - name: Upload merged test reports
-        uses: actions/upload-artifact@v3
+        uses: actions/upload-artifact@v4
         with:
           name: ksmt-test-report
           path: ksmt-test-report-*
diff --git a/README.md b/README.md
@@ -11,7 +11,7 @@ Get the most out of SMT solving with KSMT features:
 * Streamlined [solver delivery](#ksmt-distribution) with no need for building a solver or implementing JVM bindings
 
 [![KSMT: build](https://github.com/UnitTestBot/ksmt/actions/workflows/build-and-run-tests.yml/badge.svg)](https://github.com/UnitTestBot/ksmt/actions/workflows/build-and-run-tests.yml)
-[![Maven Central](https://img.shields.io/maven-central/v/io.ksmt/ksmt-core)](https://central.sonatype.com/artifact/io.ksmt/ksmt-core/0.5.16)
+[![Maven Central](https://img.shields.io/maven-central/v/io.ksmt/ksmt-core)](https://central.sonatype.com/artifact/io.ksmt/ksmt-core/0.5.17)
 [![javadoc](https://javadoc.io/badge2/io.ksmt/ksmt-core/javadoc.svg)](https://javadoc.io/doc/io.ksmt/ksmt-core)
 
 ## Get started
@@ -20,9 +20,9 @@ To start using KSMT, install it via [Gradle](https://gradle.org/):
 
 ```kotlin
 // core 
-implementation("io.ksmt:ksmt-core:0.5.16")
+implementation("io.ksmt:ksmt-core:0.5.17")
 // z3 solver
-implementation("io.ksmt:ksmt-z3:0.5.16")
+implementation("io.ksmt:ksmt-z3:0.5.17")
 ```
 
 Find basic instructions in the [Getting started](docs/getting-started.md) guide and try it out with the 

diff --git a/buildSrc/src/main/kotlin/io.ksmt.ksmt-base.gradle.kts b/buildSrc/src/main/kotlin/io.ksmt.ksmt-base.gradle.kts
@@ -11,7 +11,7 @@ plugins {
 }
 
 group = "io.ksmt"
-version = "0.5.16"
+version = "0.5.17"
 
 repositories {
     mavenCentral()

diff --git a/docs/getting-started.md b/docs/getting-started.md
@@ -34,7 +34,7 @@ repositories {
 ```kotlin
 dependencies {
     // core 
-    implementation("io.ksmt:ksmt-core:0.5.16")    
+    implementation("io.ksmt:ksmt-core:0.5.17")    
 }
 ```
 
@@ -43,9 +43,9 @@ dependencies {
 ```kotlin
 dependencies {
     // z3 
-    implementation("io.ksmt:ksmt-z3:0.5.16")
+    implementation("io.ksmt:ksmt-z3:0.5.17")
     // bitwuzla
-    implementation("io.ksmt:ksmt-bitwuzla:0.5.16")
+    implementation("io.ksmt:ksmt-bitwuzla:0.5.17")
 }
 ```
 

diff --git a/examples/build.gradle.kts b/examples/build.gradle.kts
@@ -9,11 +9,11 @@ repositories {
 
 dependencies {
     // core
-    implementation("io.ksmt:ksmt-core:0.5.16")
+    implementation("io.ksmt:ksmt-core:0.5.17")
     // z3 solver
-    implementation("io.ksmt:ksmt-z3:0.5.16")
+    implementation("io.ksmt:ksmt-z3:0.5.17")
     // Runner and portfolio solver
-    implementation("io.ksmt:ksmt-runner:0.5.16")
+    implementation("io.ksmt:ksmt-runner:0.5.17")
 }
 
 java {