Change regression testing suite to support running tests with cvc5.

This allows us to test against more than one solvers in the new
backend (currently tested - cvc5, z3).

This ensures that we don't invariably issue output that is solver
specific, tying the new backend to a single solver by accident.

Author: NlightNFotis

regression/cbmc-incr-smt2/CMakeLists.txt

@@ -1,10 +1,20 @@
 
 if("${CMAKE_SYSTEM_NAME}" STREQUAL "Windows")
-    set(exclude_win_broken_tests -X winbug)
+    set(exclude_win_broken_tests "-X;winbug")
 else()
     set(exclude_win_broken_tests "")
 endif()
 
-add_test_pl_tests(
-    "$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation --slice-formula" ${exclude_win_broken_tests}
+add_test_pl_profile(
+    "cbmc-incr-smt2-z3"
+    "$<TARGET_FILE:cbmc> --incremental-smt2-solver 'z3 --smt2 -in' --validate-goto-model --validate-ssa-equation --slice-formula"
+    "-C;${exclude_win_broken_tests};-s;new-smt-z3"
+    "CORE"
+)
+
+add_test_pl_profile(
+    "cbmc-incr-smt2-cvc5"
+    "$<TARGET_FILE:cbmc> --incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental' --validate-goto-model --validate-ssa-equation --slice-formula"
+    "-C;${exclude_win_broken_tests};-s;new-smt-cvc5"
+    "CORE"
 )

regression/cbmc-incr-smt2/bitvector-arithmetic-operators/overflow_behaviour.desc

@@ -1,6 +1,6 @@
 CORE
 overflow_behaviour.c
---incremental-smt2-solver 'z3 --smt2 -in' --trace
+--trace
 \[main\.assertion\.1\] line \d+ Wrap-around to INT_MIN when adding to INT_MAX: SUCCESS
 \[main\.assertion\.2\] line \d+ Wrap-around to INT_MAX when subtracting from INT_MIN: SUCCESS
 \[main\.assertion\.3\] line \d+ INT_MAX minus INT_MIN equals -1: SUCCESS

regression/cbmc-incr-smt2/bitvector-arithmetic-operators/polynomial.desc

@@ -1,6 +1,6 @@
 CORE
 polynomial.c
---incremental-smt2-solver 'z3 --smt2 -in' --trace
+--trace
 \[main\.assertion\.1\] line \d+ No negative solution: FAILURE
 \[main\.assertion\.2\] line \d+ No positive solution: FAILURE
 x=-8\ \(11111111 11111111 11111111 11111000\)

regression/cbmc-incr-smt2/bitvector-arithmetic-operators/simple_equation.desc

@@ -1,6 +1,6 @@
 CORE
 simple_equation.c
---incremental-smt2-solver 'z3 --smt2 -in' --trace --verbosity 10
+--trace --verbosity 10
 \[main\.assertion\.1\] line \d+ a plus a always equals two times a: SUCCESS
 \[main\.assertion\.2\] line \d+ a minus a always equals 0: SUCCESS
 \[main\.assertion\.3\] line \d+ a plus its additive inverse equals 0: SUCCESS

regression/cbmc-incr-smt2/bitvector-arithmetic-operators/unsigned_behaviour.desc

@@ -1,6 +1,6 @@
 CORE
 unsigned_behaviour.c
---incremental-smt2-solver 'z3 --smt2 -in' --trace
+--trace
 \[main\.assertion\.1\] line \d+ a plus b should be more than 27: FAILURE
 \[main\.assertion\.2\] line \d+ a plus b should be more than 27: FAILURE
 \[main\.assertion\.3\] line \d+ c plus d should be more than 27: FAILURE

regression/cbmc-incr-smt2/bitvector-bitwise-operators/bitwise.desc

@@ -1,6 +1,6 @@
 CORE
 bitwise_ops.c
---incremental-smt2-solver 'z3 --smt2 -in' --slice-formula
+--slice-formula
 \[main\.assertion\.1\] line \d+ This is going to fail for bit-opposites: FAILURE
 \[main\.assertion\.2\] line \d+ This is going to hold for all values != 0: SUCCESS
 \[main\.assertion\.3\] line \d+ This is going to fail for the same value in A and B: FAILURE

regression/cbmc-incr-smt2/bitvector-bitwise-operators/shift_left.desc

@@ -1,6 +1,6 @@
 CORE
 shift_left.c
---incremental-smt2-solver 'z3 --smt2 -in' --slice-formula
+--slice-formula
 \[main\.assertion\.1\] line \d Shifted result should be greater than one: FAILURE
 ^EXIT=10$
 ^SIGNAL=0$

regression/cbmc-incr-smt2/bitvector-bitwise-operators/shift_right.c

@@ -10,6 +10,10 @@ int main()
 {
   int first;
   uint8_t second;
+  // This assumption is here in order to constrain the value the solver
+  // can produce to just 128 so that we don't get test failures for different
+  // values returned by different SMT solvers.
+  __CPROVER_assume((second & 1) == 0);
 
   int place;
   __CPROVER_assume(place >= 1);

regression/cbmc-incr-smt2/bitvector-bitwise-operators/shift_right.desc

@@ -1,6 +1,6 @@
 CORE
 shift_right.c
---incremental-smt2-solver 'z3 --smt2 -in' --slice-formula --trace
+--slice-formula --trace
 \[main\.assertion\.1\] line \d+ Right shifting a uint with leftmost bit set is a logical shift: FAILURE
 \[main\.assertion\.2\] line \d+ Right shifting a positive number has a lower bound of 0: SUCCESS
 \[main\.assertion\.3\] line \d+ Right shifting a negative number has a lower bound value of -1: SUCCESS

regression/cbmc-incr-smt2/bitvector-flag-tests/div_by_zero.desc

@@ -1,6 +1,6 @@
 CORE
 div_by_zero.c
---incremental-smt2-solver 'z3 --smt2 -in' --div-by-zero-check --trace
+--div-by-zero-check --trace
 \[main\.division-by-zero\.1\] line \d division by zero in x / y: FAILURE
 \[main\.division-by-zero\.2\] line \d+ division by zero in x / z: SUCCESS
 y=0