Change Makefile in regression/cbmc-incr-smt2 to support testing with multiple solvers.

Previously the command that was enabling the new SMT backend (and providing
the script for invoking the appropriate SMT solver) was passed as part of the
options passed in `test.desc`.

Since this was removed, and passed as part of the test configuration in the
`CMakeLists.txt`, we need to do the same here.

Author: NlightNFotis

regression/cbmc-incr-smt2/Makefile

@@ -1,4 +1,4 @@
-default: test
+default: test.z3
 
 include ../../src/config.inc
 include ../../src/common
@@ -9,10 +9,13 @@ else
 	exclude_broken_windows_tests=
 endif
 
-test:
-	@../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation --slice-formula" $(exclude_broken_windows_tests)
+test.z3:
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --incremental-smt2-solver 'z3 --smt2 -in' --validate-goto-model --validate-ssa-equation --slice-formula" $(exclude_broken_windows_tests)
 
-tests.log: ../test.pl test
+test.cvc5:
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --incremental-smt2-solver 'cvc5 --lang smt --incremental' --validate-goto-model --validate-ssa-equation --slice-formula" $(exclude_broken_windows_tests)
+
+tests.log: ../test.pl test.z3
 
 clean:
 	find . -name '*.out' -execdir $(RM) '{}' \;