Fix tests to admit unquoted symbols and change solver to cvc5 for CI compatibility.

Author: NlightNFotis

regression/cbmc-incr-smt2/CMakeLists.txt

@@ -13,8 +13,8 @@ add_test_pl_profile(
 )
 
 add_test_pl_profile(
-    "cbmc-new-smt-backend-cv4"
-    "$<TARGET_FILE:cbmc> --incremental-smt2-solver 'cvc4 --lang smt' --validate-goto-model --validate-ssa-equation --slice-formula ${exclude_win_broken_tests}"
-    "-C;-s;new-smt-cvc4"
+    "cbmc-new-smt-backend-cvc5"
+    "$<TARGET_FILE:cbmc> --incremental-smt2-solver 'cvc5 --lang smt --incremental' --validate-goto-model --validate-ssa-equation --slice-formula ${exclude_win_broken_tests}"
+    "-C;-X;broken-cvc5;-s;new-smt-cvc5"
     "CORE"
 )

regression/cbmc-incr-smt2/nondeterministic-int-assert/control_flow.desc

@@ -1,22 +1,22 @@
 CORE
 control_flow.c
 --verbosity 10
-Passing problem to incremental SMT2 solving via "z3 --smt2 -in"
+Passing problem to incremental SMT2 solving via
 Sending command to SMT2 solver - \(set-option :produce-models true\)
 Sending command to SMT2 solver - \(set-logic QF_UFBV\)
 Sending command to SMT2 solver - \(declare-fun |goto_symex::&92;guard#1| \(\) Bool\)
 Sending command to SMT2 solver - \(define-fun |B1| \(\) Bool |goto_symex::&92;guard#1|\)
 Sending command to SMT2 solver - \(declare-fun |main::1::x!0@1#1| \(\) \(_ BitVec 32\)\)
-Sending command to SMT2 solver - \(assert \(|=| |goto_symex::&92;guard#1| \(|not| \(|=| |main::1::x!0@1#1| \(_ bv0 32\)\)\)\)\)
+Sending command to SMT2 solver - \(assert \(= |goto_symex::&92;guard#1| \(not \(= |main::1::x!0@1#1| \(_ bv0 32\)\)\)\)\)
 Sending command to SMT2 solver - \(declare-fun |main::1::y!0@1#4| \(\) \(_ BitVec 32\)\)
-Sending command to SMT2 solver - \(assert \(|=| |main::1::y!0@1#4| \(|ite| |goto_symex::&92;guard#1| \(_ bv9 32\) \(_ bv4 32\)\)\)\)
+Sending command to SMT2 solver - \(assert \(= |main::1::y!0@1#4| \(|ite| |goto_symex::&92;guard#1| \(_ bv9 32\) \(_ bv4 32\)\)\)\)
 Sending command to SMT2 solver - \(declare-fun |main::1::x!0@1#3| \(\) \(_ BitVec 32\)\)
-Sending command to SMT2 solver - \(assert \(|=| |main::1::x!0@1#3| \(|ite| |goto_symex::&92;guard#1| |main::1::x!0@1#1| \(_ bv0 32\)\)\)\)
+Sending command to SMT2 solver - \(assert \(= |main::1::x!0@1#3| \(|ite| |goto_symex::&92;guard#1| |main::1::x!0@1#1| \(_ bv0 32\)\)\)\)
 Sending command to SMT2 solver - \(declare-fun |main::1::z!0@1#2| \(\) \(_ BitVec 32\)\)
-Sending command to SMT2 solver - \(assert \(|=| |main::1::z!0@1#2| |main::1::y!0@1#4|\)\)
-Sending command to SMT2 solver - \(define-fun |B3| \(\) Bool \(|=| |main::1::x!0@1#1| \(_ bv0 32\)\)\)
-Sending command to SMT2 solver - \(assert \(|not| \(|not| \(|=| |main::1::x!0@1#3| |main::1::z!0@1#2|\)\)\)\)
-Sending command to SMT2 solver - \(define-fun |B4| \(\) Bool \(|not| false\)\)
+Sending command to SMT2 solver - \(assert \(= |main::1::z!0@1#2| |main::1::y!0@1#4|\)\)
+Sending command to SMT2 solver - \(define-fun |B3| \(\) Bool \(= |main::1::x!0@1#1| \(_ bv0 32\)\)\)
+Sending command to SMT2 solver - \(assert \(not \(not \(= |main::1::x!0@1#3| |main::1::z!0@1#2|\)\)\)\)
+Sending command to SMT2 solver - \(define-fun |B4| \(\) Bool \(not false\)\)
 Sending command to SMT2 solver - \(assert |B4|\)
 Sending command to SMT2 solver - \(check-sat\)
 Solver response - sat

regression/cbmc-incr-smt2/nondeterministic-int-assert/incremental_solver_called.desc

@@ -1,14 +1,14 @@
 CORE
 test.c
 --verbosity 10
-Passing problem to incremental SMT2 solving via "z3 --smt2 -in"
+Passing problem to incremental SMT2 solving via
 Sending command to SMT2 solver - \(set-option :produce-models true\)
 Sending command to SMT2 solver - \(set-logic QF_UFBV\)
 Sending command to SMT2 solver - \(define-fun |B0| \(\) Bool true\)
 Sending command to SMT2 solver - \(declare-fun |main::1::x!0@1#1| \(\) \(_ BitVec 32\)\)
-Sending command to SMT2 solver - \(define-fun |B1| \(\) Bool \(|=| |main::1::x!0@1#1| |main::1::x!0@1#1|\)\)
-Sending command to SMT2 solver - \(assert \(|not| \(|not| \(|=| |main::1::x!0@1#1| \(_ bv0 32\)\)\)\)\)
-Sending command to SMT2 solver - \(define-fun |B2| \(\) Bool \(|not| false\)\)
+Sending command to SMT2 solver - \(define-fun |B1| \(\) Bool \(= |main::1::x!0@1#1| |main::1::x!0@1#1|\)\)
+Sending command to SMT2 solver - \(assert \(not \(not \(= |main::1::x!0@1#1| \(_ bv0 32\)\)\)\)\)
+Sending command to SMT2 solver - \(define-fun |B2| \(\) Bool \(not false\)\)
 Sending command to SMT2 solver - \(assert |B2|\)
 Sending command to SMT2 solver - \(check-sat\)
 Solver response - sat

regression/cbmc-incr-smt2/nondeterministic-int-assert/stdbool.desc

@@ -1,7 +1,7 @@
 CORE
 stdbool_example.c
 --trace
-Passing problem to incremental SMT2 solving via "z3 --smt2 -in"
+Passing problem to incremental SMT2 solving via
 VERIFICATION FAILED
 equal=FALSE\s*\([0 ]+\)
 equal=TRUE\s*\([0 ]+1\)

regression/cbmc-incr-smt2/nondeterministic-int-assert/trace.desc

@@ -1,7 +1,7 @@
 CORE
 trace.c
 --trace
-Passing problem to incremental SMT2 solving via "z3 --smt2 -in"
+Passing problem to incremental SMT2 solving via
 Assert of inequality to 4\.: FAILURE
 Assert of inequality to 2\.: FAILURE
 y=4

regression/cbmc-incr-smt2/nondeterministic-int-assert/valid_unsat.desc

@@ -1,7 +1,7 @@
 CORE
 valid_unsat.c
 --verbosity 10
-Passing problem to incremental SMT2 solving via "z3 --smt2 -in"
+Passing problem to incremental SMT2 solving via
 Sending command to SMT2 solver - \(check-sat\)
 Solver response - unsat
 VERIFICATION SUCCESSFUL