Use -X broken-smt-backend instead of deleting files

This actually simplifies our CI scripts.

Author: tautschnig

.travis.yml

@@ -304,7 +304,7 @@ script:
   - if [ -e bin/gcc ] ; then export PATH=$PWD/bin:$PATH ; fi ;
   - env UBSAN_OPTIONS=print_stacktrace=1 make -C regression test-parallel "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j2 JOBS=2
   - UBSAN_OPTIONS=print_stacktrace=1 make -C regression/cbmc test-paths-lifo
-  - scripts/delete_failing_smt2_solver_tests ; env PATH=$PATH:`pwd`/src/solvers UBSAN_OPTIONS=print_stacktrace=1 make -C regression/cbmc test-cprover-smt2
+  - env PATH=$PATH:`pwd`/src/solvers UBSAN_OPTIONS=print_stacktrace=1 make -C regression/cbmc test-cprover-smt2
   - make -C unit "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j2
   - make -C unit test
   - env UBSAN_OPTIONS=print_stacktrace=1 make -C jbmc/regression test-parallel "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j2 JOBS=2

CODEOWNERS

@@ -59,7 +59,6 @@
 /jbmc/regression/
 
 /scripts/ @diffblue/devops @thk123 @forejtv @peterschrammel
-/scripts/delete_failing_smt2_solver_tests
 /scripts/expected_doxygen_warnings.txt
 
 /.travis.yml @diffblue/devops @thk123 @forejtv @peterschrammel

buildspec-linux-clang.yml

@@ -22,7 +22,6 @@ phases:
     commands:
       - make -C unit test CXX='ccache /usr/bin/clang++-7' CXX_FLAGS='-Qunused-arguments'
       - make -C regression test
-      - scripts/delete_failing_smt2_solver_tests
       - env PATH=$PATH:`pwd`/src/solvers make -C regression/cbmc test-cprover-smt2
       - make -C jbmc/unit test CXX='ccache /usr/bin/clang++-7' CXX_FLAGS='-Qunused-arguments'
       - make -C jbmc/regression test

buildspec.yml

@@ -26,7 +26,6 @@ phases:
       - make -C unit test
       - make -C regression test
       - make -C regression/cbmc test-paths-lifo
-      - scripts/delete_failing_smt2_solver_tests
       - env PATH=$PATH:`pwd`/src/solvers make -C regression/cbmc test-cprover-smt2
       - make -C jbmc/unit test
       - make -C jbmc/regression test

regression/cbmc/Makefile

@@ -4,7 +4,7 @@ test:
 	@../test.pl -p -c "../../../src/cbmc/cbmc --validate-goto-model" -X smt-backend
 
 test-cprover-smt2:
-	@../test.pl -p -c "../../../src/cbmc/cbmc --cprover-smt2"
+	@../test.pl -p -c "../../../src/cbmc/cbmc --cprover-smt2" -X broken-smt-backend
 
 test-paths-lifo:
 	@../test.pl -p -c "../../../src/cbmc/cbmc --paths lifo" -X thorough-paths -X smt-backend