Debug

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

Hide file tree

Showing 2 changed files with 8 additions and 3 deletions.
diff --git a/.github/workflows/z3_trace_log_gen.yml b/.github/workflows/z3_trace_log_gen.yml
@@ -27,6 +27,11 @@ jobs:
         with:
           fetch-depth: 0 # needed, see GitHub Action "Changed Files"
 
+      - name: Debug
+        run: |
+          echo "matrix.versions.installz3: ${{ matrix.versions.installz3 }}"
+          echo "matrix.versions.z3: ${{ matrix.versions.z3 }}"
+
       - if: ${{ matrix.versions.installz3 }} == 'v1.3'
         name: Install Z3
         uses: pavpanchekha/[email protected] # see GitHub Action "Install 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 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)