Test

viperproject · Sep 9, 2023 · 084590e · 084590e
1 parent ac546d1
commit 084590e
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 4 deletions.
diff --git a/.github/workflows/z3_trace_log_gen.yml b/.github/workflows/z3_trace_log_gen.yml
@@ -27,7 +27,13 @@ jobs:
         with:
           fetch-depth: 0 # needed, see GitHub Action "Changed Files"
 
-      - name: Debug
+      - name: Debug v1.3
+        run: |
+          echo "matrix.versions.installz3: ${{ matrix.versions.installz3 }}"
+          echo "matrix.versions.z3: ${{ matrix.versions.z3 }}"
+        if: ${{ matrix.versions.installz3 }} == 'v1.3' 
+
+      - name: Debug 1.2.2
         run: |
           echo "matrix.versions.installz3: ${{ matrix.versions.installz3 }}"
           echo "matrix.versions.z3: ${{ matrix.versions.z3 }}"

diff --git a/smt-problems/small_forall_example_2.smt2 b/smt-problems/small_forall_example_2.smt2
@@ -1,6 +1,6 @@
 (declare-const x (_ BitVec 64))
-(declare-const z (_ BitVec 64))
-(assert (forall ((x (_ BitVec 64)) (z (_ BitVec 64)))
-    (= (bvsub (bvadd x z) (bvshl (bvand x z) (_ bv1 64))) (bvxor x z))))
+(declare-const y (_ BitVec 64))
+(assert (forall ((x (_ BitVec 64)) (y (_ BitVec 64)))
+    (= (bvsub (bvadd x y) (bvshl (bvand x y) (_ bv1 64))) (bvxor x y))))
 
 (check-sat)