Changed smt file

.github/workflows/z3_trace_log_gen.yml

@@ -30,21 +30,20 @@ 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 }}" 
           mkdir logs
           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)"
 

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)