Duh

viperproject · Sep 9, 2023 · aeb78aa · aeb78aa
1 parent 71fd9e5
commit aeb78aa
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 10 deletions.
diff --git a/.github/workflows/z3_trace_log_gen.yml b/.github/workflows/z3_trace_log_gen.yml
@@ -28,16 +28,12 @@ jobs:
           fetch-depth: 0 # needed, see GitHub Action "Changed Files"
 
       - name: Install Z3
-        if: ${{ matrix.versions.installz3 }} == 'v1.3'
         uses: pavpanchekha/[email protected] # see GitHub Action "Install Z3"
-        with:
-          version: ${{ matrix.versions.z3 }} 
-
-      - name: Install Z3
-        if: ${{ matrix.versions.installz3 }} == '1.2.2'
+        if: ${{ matrix.versions.installz3 }} == 'v1.3'
         uses: pavpanchekha/[email protected] # see GitHub Action "Install Z3"
+        if: ${{ matrix.versions.installz3 }} == '1.2.2'
         with:
-          version: ${{ matrix.versions.z3 }}
+          version: ${{ matrix.versions.z3 }} 
 
       # this fetches all changed (added/modified) smt2 files in the repository 
       - name: Fetch changed smt2 files

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 y (_ BitVec 64))
-(assert (forall ((x (_ BitVec 64)) (y (_ BitVec 64)))
-    (= (bvsub (bvadd x y) (bvshl (bvand x y) (_ bv1 64))) (bvxor x y))))
+(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))))
 
 (check-sat)