From 294c9134525b23683daca509a30bff2de17a4e21 Mon Sep 17 00:00:00 2001
From: ojyrkinen <oskari.jyrkinen@gmail.com>
Date: Thu, 31 Aug 2023 10:43:38 +0200
Subject: [PATCH] Changed smt file

---
 .github/workflows/z3_trace_log_gen.yml      | 11 +++++------
 smt-problems/small_forall_example copy.smt2 |  6 +++---
 2 files changed, 8 insertions(+), 9 deletions(-)

diff --git a/.github/workflows/z3_trace_log_gen.yml b/.github/workflows/z3_trace_log_gen.yml
index 1564d1bd..ca17ec27 100644
--- a/.github/workflows/z3_trace_log_gen.yml
+++ b/.github/workflows/z3_trace_log_gen.yml
@@ -30,7 +30,7 @@ jobs:
             smt:
               - '**/*.smt2'
 
-      - name: Run Z3 Solver on 
+      - name: Run Z3 Solver 
         id: run_z3_and_upload
         run: |
           echo "List all the files that have changed: ${{ steps.changed-smt2-files.outputs.smt_all_changed_files }}" 
@@ -38,13 +38,12 @@ jobs:
           for file in ${{ steps.changed-smt2-files.outputs.smt_all_changed_files }}; do
             echo "Processing $file"
             # Run Z3 solver here for $file
-            # z3 trace=true proof=true trace-file-name=${file%.smt2}.log ./$file
-            # gzip -c ${file%.smt2} > logs
+            z3 trace=true proof=true trace-file-name=${file%.smt2}.log ./$file
             # Get the filename without extension
-            # base_name=$(basename "${file%.*}")
+            base_name=$(basename "${file%.*}")
             # Compress the file and save it to logs directory
-            # gzip -c "$file" > "$logs/${base_name}.log.gz"
-            # echo "Compressed $file and saved to $logs/${base_name}.log.gz"
+            gzip -c "$file" > "$logs/${base_name}.log.gz"
+            echo "Compressed $file and saved to $logs/${base_name}.log.gz"
           done
           echo "::set-output name=logs_path::$(realpath logs)"
 
diff --git a/smt-problems/small_forall_example copy.smt2 b/smt-problems/small_forall_example copy.smt2
index ba6b351b..2d3efa7a 100644
--- a/smt-problems/small_forall_example copy.smt2	
+++ b/smt-problems/small_forall_example copy.smt2	
@@ -1,6 +1,6 @@
 (declare-const x (_ BitVec 64))
-(declare-const w (_ BitVec 64))
-(assert (forall ((x (_ BitVec 64)) (w (_ BitVec 64)))
-    (= (bvsub (bvadd x w) (bvshl (bvand x w) (_ bv1 64))) (bvxor x w))))
+(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)