Fixed script

viperproject · Sep 4, 2023 · cca0aec · cca0aec
1 parent 6781d98
commit cca0aec
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 6 deletions.
diff --git a/.github/workflows/z3_trace_log_gen.yml b/.github/workflows/z3_trace_log_gen.yml
@@ -56,12 +56,13 @@ jobs:
           # Compress the 'logs' directory using bzip2
           z3_v_clean=$(echo "${{ matrix.z3version }}" | sed 's/\./_/g')
           tar -cjf logs_z3_v_${z3_v_clean}.tar.bz2 logs/
+          echo "::set-output name=logs_path::$(realpath logs_z3_v_${z3_v_clean}.tar.bz2)"
 
         env:
-          MATRIX_Z3VERSION: ${{ matrix.z3version }}
+          MATRIX_Z3VERSION: ${z3_v_clean}
 
       - name: Upload build artifacts
         uses: actions/[email protected]
         with:
-          name: "logs_z3_${{ env.MATRIX_Z3VERSION }}.tar.bz2"
-          path: "logs_z3_${{ env.MATRIX_Z3VERSION }}.tar.bz2"
+          name: "logs_z3_${{ steps.run_z3_and_upload.env.MATRIX_Z3VERSION }}.tar.bz2"
+          path: ${{ steps.run_z3_and_upload.outputs.logs_path }}
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)