Added new tags for SMT regression tests

As per the proposal described in #5982, this PR introduces new tags that
can be used to label tests that are known to be broken with specific solvers.
It also updates the Makefile targets to use these solver-specific tags.

Author: SaswatPadhi

regression/cbmc/CMakeLists.txt

@@ -20,7 +20,7 @@ add_test_pl_profile(
 add_test_pl_profile(
     "cbmc-cprover-smt2"
     "$<TARGET_FILE:cbmc> --cprover-smt2"
-    "-C;-X;broken-smt-backend;-X;thorough-smt-backend;${gcc_only_string}-s;cprover-smt2"
+    "-C;-X;broken-smt-backend;-X;thorough-smt-backend;-X;broken-cprover-smt-backend;-X;thorough-cprover-smt-backend;${gcc_only_string}-s;cprover-smt2"
     "CORE"
 )
 

regression/cbmc/Makefile

@@ -13,14 +13,25 @@ test:
 	@../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation" -X smt-backend $(GCC_ONLY)
 
 test-cprover-smt2:
-	@../test.pl -e -p -c "../../../src/cbmc/cbmc --cprover-smt2" -X broken-smt-backend -X thorough-smt-backend $(GCC_ONLY)
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --cprover-smt2" \
+					  -X broken-smt-backend -X thorough-smt-backend \
+					  -X broken-cprover-smt-backend -X thorough-cprover-smt-backend \
+					  -s cprover-smt2 $(GCC_ONLY)
+
+test-z3:
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --z3" \
+					  -X broken-smt-backend -X thorough-smt-backend \
+					  -X broken-z3-smt-backend -X thorough-z3-smt-backend \
+					  -s z3 $(GCC_ONLY)
 
 test-paths-lifo:
-	@../test.pl -e -p -c "../../../src/cbmc/cbmc --paths lifo" -X thorough-paths -X smt-backend -X paths-lifo-expected-failure $(GCC_ONLY)
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --paths lifo" \
+					  -X thorough-paths -X smt-backend -X paths-lifo-expected-failure \
+					  -s paths-lifo $(GCC_ONLY)
 
 tests.log: ../test.pl test
 
 clean:
 	find . -name '*.out' -execdir $(RM) '{}' \;
 	find . -name '*.smt2' -execdir $(RM) '{}' \;
-	$(RM) tests.log tests-paths-lifo.log tests-cprover-smt2.log
+	$(RM) tests*.log

regression/readme.md

@@ -1,12 +1,42 @@
-# CProver regression tests
+# CProver Regression Tests
 
 This folder contains the CProver regression test-suite.
 
-## Notes
+## Tags
 
-* Tests marked as `winbug` are currently known to be failing
-  on Windows, but passing on other platforms. The reason for
-  this is not known, and it's currently being investigated.
-  This was discovered during work done to port CI from travis
-  and codebuild to github actions. Worth noting that those tests
-  were not being run on Windows before.
+### Backend
+
+- `smt-backend`:
+  These tests _require_ the SMT backend and do not work with the SAT backend.
+  For example, quantified predicates are not fully supported in SAT.
+- `broken-smt-backend`:
+  These tests are blocked on missing / buggy goto -> SMT translation rules,
+  and therefore do not work with any SMT solver.
+- `thorough-smt-backend`:
+  These tests are too slow to be run in CI with the SMT backend.
+
+### Solver
+
+- `broken-cprover-smt-backend`:
+  These tests are known to not work with CPROVER SMT2.
+- `thorough-cprover-smt-backend`:
+  These tests are too slow to be run in CI with CPROVER SMT2.
+- `broken-z3-smt-backend`:
+  These tests are known to not work with Z3 (the version running on our CI).
+- `thorough-z3-smt-backend`:
+  These tests are too slow to be run in CI with Z3.
+
+### Platform
+
+- `winbug`:
+  These tests are currently known to be failing on Windows,
+  but passing on other platforms.
+  The reason for this is not known, and it's currently being investigated.
+  This was discovered during work done to port CI from [Travis]
+  and [AWS CodeBuild] to [GitHub Actions].
+  Worth noting that those tests were not being run on Windows before.
+
+
+[AWS CodeBuild]: https://aws.amazon.com/codebuild/
+[GitHub Actions]: https://github.com/features/actions
+[Travis]: https://travis-ci.com/