Update docker-ci{,-for-pr}.yml to use Z3 v4.12.4 by default

HolSmt now supports proof reconstruction for Z3 v4.12.4, so we can now use it by default to run the HolSmt self-tests.
HOL-Theorem-Prover · Feb 8, 2024 · a14bc3f · a14bc3f
1 parent 5e77b60
commit a14bc3f
Show file tree

Hide file tree

Showing 2 changed files with 4 additions and 4 deletions.
diff --git a/.github/workflows/docker-ci-for-pr.yml b/.github/workflows/docker-ci-for-pr.yml
@@ -24,7 +24,7 @@ jobs:
           push: false
           build-args: |
             SML=poly
-            Z3_VERSION=2.19
+            Z3_VERSION=4.12.4
             CVC_VERSION=5
             BUILDOPTS=--stdknl -j2 -t
 
@@ -45,6 +45,6 @@ jobs:
           push: false
           build-args: |
             SML=poly
-            Z3_VERSION=2.19
+            Z3_VERSION=4.12.4
             CVC_VERSION=5
             BUILDOPTS=--expk -j2 -t
diff --git a/.github/workflows/docker-ci.yml b/.github/workflows/docker-ci.yml
@@ -42,7 +42,7 @@ jobs:
           push: true
           build-args: |
             SML=poly
-            Z3_VERSION=2.19
+            Z3_VERSION=4.12.4
             CVC_VERSION=5
             # NOTE: the arg value cannot be quoted here:
             BUILDOPTS=--stdknl -j2 -t
@@ -80,7 +80,7 @@ jobs:
           push: true
           build-args: |
             SML=poly
-            Z3_VERSION=2.19
+            Z3_VERSION=4.12.4
             CVC_VERSION=5
             # NOTE: the arg value cannot be quoted here:
             BUILDOPTS=--expk -j2 -t