diff --git a/.travis.yml b/.travis.yml
index db76e3f04ff..03238cfd093 100644
--- a/.travis.yml
+++ b/.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
diff --git a/CODEOWNERS b/CODEOWNERS
index 0e4fd4c8b7d..a11c70ec88d 100644
--- a/CODEOWNERS
+++ b/CODEOWNERS
@@ -60,7 +60,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 @chrisr-diffblue
diff --git a/buildspec-linux-clang.yml b/buildspec-linux-clang.yml
index 171826bd45b..cac3f692e61 100644
--- a/buildspec-linux-clang.yml
+++ b/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
diff --git a/buildspec-windows.yml b/buildspec-windows.yml
index dc8c4561c61..2c7995dc0ed 100644
--- a/buildspec-windows.yml
+++ b/buildspec-windows.yml
@@ -40,6 +40,10 @@ phases:
         $env:Path = "C:\tools\cygwin\bin;$env:Path"
         cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -C regression test BUILD_ENV=MSVC" '
 
+      - |
+        $env:Path = "$pwd\src\solvers;C:\tools\cygwin\bin;$env:Path"
+        cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -C regression/cbmc test-cprover-smt2 BUILD_ENV=MSVC" '
+
       - |
         $env:Path = "C:\tools\cygwin\bin;$env:Path"
         cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -C regression/cbmc test-paths-lifo BUILD_ENV=MSVC" '
diff --git a/buildspec.yml b/buildspec.yml
index e8a7a453e25..975e3eea7a7 100644
--- a/buildspec.yml
+++ b/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
diff --git a/regression/cbmc/Anonymous_Struct3/test.desc b/regression/cbmc/Anonymous_Struct3/test.desc
index 9efefbc7362..39d9265e8a7 100644
--- a/regression/cbmc/Anonymous_Struct3/test.desc
+++ b/regression/cbmc/Anonymous_Struct3/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Array_operations1/test.desc b/regression/cbmc/Array_operations1/test.desc
index 0b0aa0f57d5..81622f4d813 100644
--- a/regression/cbmc/Array_operations1/test.desc
+++ b/regression/cbmc/Array_operations1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 
 ^EXIT=10$
diff --git a/regression/cbmc/Bitfields3/paths.desc b/regression/cbmc/Bitfields3/paths.desc
index 81ec9c8ed2d..c6d543290f7 100644
--- a/regression/cbmc/Bitfields3/paths.desc
+++ b/regression/cbmc/Bitfields3/paths.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --pointer-check --bounds-check --paths lifo
 ^EXIT=0$
diff --git a/regression/cbmc/Bitfields3/test.desc b/regression/cbmc/Bitfields3/test.desc
index 96c9b4bcd7b..35db6e71ddb 100644
--- a/regression/cbmc/Bitfields3/test.desc
+++ b/regression/cbmc/Bitfields3/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --pointer-check --bounds-check
 ^EXIT=0$
diff --git a/regression/cbmc/CMakeLists.txt b/regression/cbmc/CMakeLists.txt
index 954598f0b0f..8d7709afb89 100644
--- a/regression/cbmc/CMakeLists.txt
+++ b/regression/cbmc/CMakeLists.txt
@@ -8,3 +8,15 @@ add_test_pl_profile(
     "-C;-X;thorough-paths;-X;smt-backend;-s;paths-lifo"
     "CORE"
 )
+
+add_test_pl_profile(
+    "cbmc-cprover-smt2"
+    "$<TARGET_FILE:cbmc> --cprover-smt2"
+    "-C;-X;broken-smt-backend;-s;cprover-smt2"
+    "CORE"
+)
+set_property(
+  TEST "cbmc-cprover-smt2-CORE"
+  PROPERTY ENVIRONMENT
+    "PATH=$ENV{PATH}:${CMAKE_BINARY_DIR}/bin"
+)
diff --git a/regression/cbmc/Empty_struct1/test.desc b/regression/cbmc/Empty_struct1/test.desc
index 9efefbc7362..39d9265e8a7 100644
--- a/regression/cbmc/Empty_struct1/test.desc
+++ b/regression/cbmc/Empty_struct1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Endianness4/test.desc b/regression/cbmc/Endianness4/test.desc
index 9efefbc7362..39d9265e8a7 100644
--- a/regression/cbmc/Endianness4/test.desc
+++ b/regression/cbmc/Endianness4/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Endianness6/test.desc b/regression/cbmc/Endianness6/test.desc
index 81ceb4c6dc0..1b8f7c29219 100644
--- a/regression/cbmc/Endianness6/test.desc
+++ b/regression/cbmc/Endianness6/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --big-endian
 ^EXIT=0$
diff --git a/regression/cbmc/Float-div2/test.desc b/regression/cbmc/Float-div2/test.desc
index b7d95a28215..8f1b838d89c 100644
--- a/regression/cbmc/Float-div2/test.desc
+++ b/regression/cbmc/Float-div2/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --floatbv
 ^EXIT=0$
diff --git a/regression/cbmc/Float-div3/test.desc b/regression/cbmc/Float-div3/test.desc
index b7d95a28215..8f1b838d89c 100644
--- a/regression/cbmc/Float-div3/test.desc
+++ b/regression/cbmc/Float-div3/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --floatbv
 ^EXIT=0$
diff --git a/regression/cbmc/Float-no-simp1/test.desc b/regression/cbmc/Float-no-simp1/test.desc
index 376d43d5dfa..ca85d6aa5f7 100644
--- a/regression/cbmc/Float-no-simp1/test.desc
+++ b/regression/cbmc/Float-no-simp1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --no-simplify
 ^EXIT=0$
diff --git a/regression/cbmc/Float-no-simp2/test.desc b/regression/cbmc/Float-no-simp2/test.desc
index 4d2a93e6e26..e0bfef5401b 100644
--- a/regression/cbmc/Float-no-simp2/test.desc
+++ b/regression/cbmc/Float-no-simp2/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --floatbv --no-simplify
 ^EXIT=0$
diff --git a/regression/cbmc/Float-no-simp3/test.desc b/regression/cbmc/Float-no-simp3/test.desc
index 4d2a93e6e26..e0bfef5401b 100644
--- a/regression/cbmc/Float-no-simp3/test.desc
+++ b/regression/cbmc/Float-no-simp3/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --floatbv --no-simplify
 ^EXIT=0$
diff --git a/regression/cbmc/Float-no-simp4/test.desc b/regression/cbmc/Float-no-simp4/test.desc
index 4d2a93e6e26..e0bfef5401b 100644
--- a/regression/cbmc/Float-no-simp4/test.desc
+++ b/regression/cbmc/Float-no-simp4/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --floatbv --no-simplify
 ^EXIT=0$
diff --git a/regression/cbmc/Float-no-simp5/test.desc b/regression/cbmc/Float-no-simp5/test.desc
index 4d2a93e6e26..e0bfef5401b 100644
--- a/regression/cbmc/Float-no-simp5/test.desc
+++ b/regression/cbmc/Float-no-simp5/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --floatbv --no-simplify
 ^EXIT=0$
diff --git a/regression/cbmc/Float-no-simp6/test.desc b/regression/cbmc/Float-no-simp6/test.desc
index 4d2a93e6e26..e0bfef5401b 100644
--- a/regression/cbmc/Float-no-simp6/test.desc
+++ b/regression/cbmc/Float-no-simp6/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --floatbv --no-simplify
 ^EXIT=0$
diff --git a/regression/cbmc/Float-no-simp7/test.desc b/regression/cbmc/Float-no-simp7/test.desc
index 4d2a93e6e26..e0bfef5401b 100644
--- a/regression/cbmc/Float-no-simp7/test.desc
+++ b/regression/cbmc/Float-no-simp7/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --floatbv --no-simplify
 ^EXIT=0$
diff --git a/regression/cbmc/Float-smt2-1/test.desc b/regression/cbmc/Float-smt2-1/test.desc
index be435602af4..c230386e8b2 100644
--- a/regression/cbmc/Float-smt2-1/test.desc
+++ b/regression/cbmc/Float-smt2-1/test.desc
@@ -1,4 +1,4 @@
-CORE smt-backend
+CORE smt-backend broken-smt-backend
 main.c
 --smt2
 ^EXIT=10$
diff --git a/regression/cbmc/Float-to-double2/test.desc b/regression/cbmc/Float-to-double2/test.desc
index 4d2a93e6e26..e0bfef5401b 100644
--- a/regression/cbmc/Float-to-double2/test.desc
+++ b/regression/cbmc/Float-to-double2/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --floatbv --no-simplify
 ^EXIT=0$
diff --git a/regression/cbmc/Float-to-int1/test.desc b/regression/cbmc/Float-to-int1/test.desc
index b7d95a28215..8f1b838d89c 100644
--- a/regression/cbmc/Float-to-int1/test.desc
+++ b/regression/cbmc/Float-to-int1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --floatbv
 ^EXIT=0$
diff --git a/regression/cbmc/Float-to-int2/test.desc b/regression/cbmc/Float-to-int2/test.desc
index b7d95a28215..8f1b838d89c 100644
--- a/regression/cbmc/Float-to-int2/test.desc
+++ b/regression/cbmc/Float-to-int2/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --floatbv
 ^EXIT=0$
diff --git a/regression/cbmc/Float-to-int3/test.desc b/regression/cbmc/Float-to-int3/test.desc
index b7d95a28215..8f1b838d89c 100644
--- a/regression/cbmc/Float-to-int3/test.desc
+++ b/regression/cbmc/Float-to-int3/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --floatbv
 ^EXIT=0$
diff --git a/regression/cbmc/Float-zero-sum1/test.desc b/regression/cbmc/Float-zero-sum1/test.desc
index 4d2a93e6e26..e0bfef5401b 100644
--- a/regression/cbmc/Float-zero-sum1/test.desc
+++ b/regression/cbmc/Float-zero-sum1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --floatbv --no-simplify
 ^EXIT=0$
diff --git a/regression/cbmc/Float12/test.desc b/regression/cbmc/Float12/test.desc
index 9efefbc7362..39d9265e8a7 100644
--- a/regression/cbmc/Float12/test.desc
+++ b/regression/cbmc/Float12/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Float13/test.desc b/regression/cbmc/Float13/test.desc
index 9efefbc7362..39d9265e8a7 100644
--- a/regression/cbmc/Float13/test.desc
+++ b/regression/cbmc/Float13/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Float20/test.desc b/regression/cbmc/Float20/test.desc
index b7d95a28215..8f1b838d89c 100644
--- a/regression/cbmc/Float20/test.desc
+++ b/regression/cbmc/Float20/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --floatbv
 ^EXIT=0$
diff --git a/regression/cbmc/Float22/test.desc b/regression/cbmc/Float22/test.desc
index b7d95a28215..8f1b838d89c 100644
--- a/regression/cbmc/Float22/test.desc
+++ b/regression/cbmc/Float22/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --floatbv
 ^EXIT=0$
diff --git a/regression/cbmc/Float23/test.desc b/regression/cbmc/Float23/test.desc
index 9efefbc7362..39d9265e8a7 100644
--- a/regression/cbmc/Float23/test.desc
+++ b/regression/cbmc/Float23/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Float3/test.desc b/regression/cbmc/Float3/test.desc
index b7d95a28215..8f1b838d89c 100644
--- a/regression/cbmc/Float3/test.desc
+++ b/regression/cbmc/Float3/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --floatbv
 ^EXIT=0$
diff --git a/regression/cbmc/Float4/test.desc b/regression/cbmc/Float4/test.desc
index b7d95a28215..8f1b838d89c 100644
--- a/regression/cbmc/Float4/test.desc
+++ b/regression/cbmc/Float4/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --floatbv
 ^EXIT=0$
diff --git a/regression/cbmc/Float5/test.desc b/regression/cbmc/Float5/test.desc
index b7d95a28215..8f1b838d89c 100644
--- a/regression/cbmc/Float5/test.desc
+++ b/regression/cbmc/Float5/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --floatbv
 ^EXIT=0$
diff --git a/regression/cbmc/Float6/test.desc b/regression/cbmc/Float6/test.desc
index b7d95a28215..8f1b838d89c 100644
--- a/regression/cbmc/Float6/test.desc
+++ b/regression/cbmc/Float6/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --floatbv
 ^EXIT=0$
diff --git a/regression/cbmc/Float8/test.desc b/regression/cbmc/Float8/test.desc
index 9efefbc7362..39d9265e8a7 100644
--- a/regression/cbmc/Float8/test.desc
+++ b/regression/cbmc/Float8/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Linking4/test.desc b/regression/cbmc/Linking4/test.desc
index d88e6744dbd..49c0d9da6cb 100644
--- a/regression/cbmc/Linking4/test.desc
+++ b/regression/cbmc/Linking4/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 link1.c
 link2.c
 ^EXIT=0$
diff --git a/regression/cbmc/Linking7/member-name-mismatch.desc b/regression/cbmc/Linking7/member-name-mismatch.desc
index 603d759e8d8..da68dba90a0 100644
--- a/regression/cbmc/Linking7/member-name-mismatch.desc
+++ b/regression/cbmc/Linking7/member-name-mismatch.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 module2.c
 ^EXIT=10$
diff --git a/regression/cbmc/Linking7/test.desc b/regression/cbmc/Linking7/test.desc
index 7e8989049b8..315426f8aae 100644
--- a/regression/cbmc/Linking7/test.desc
+++ b/regression/cbmc/Linking7/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 module.c
 ^EXIT=10$
diff --git a/regression/cbmc/Makefile b/regression/cbmc/Makefile
index 8242ae26e44..093c5b82a52 100644
--- a/regression/cbmc/Makefile
+++ b/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
diff --git a/regression/cbmc/Malloc23/test.desc b/regression/cbmc/Malloc23/test.desc
index a190cab817e..47408244d66 100644
--- a/regression/cbmc/Malloc23/test.desc
+++ b/regression/cbmc/Malloc23/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --pointer-check
 ^EXIT=10$
diff --git a/regression/cbmc/Multi_Dimensional_Array2/test.desc b/regression/cbmc/Multi_Dimensional_Array2/test.desc
index 9efefbc7362..39d9265e8a7 100644
--- a/regression/cbmc/Multi_Dimensional_Array2/test.desc
+++ b/regression/cbmc/Multi_Dimensional_Array2/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Pointer_Arithmetic11/test.desc b/regression/cbmc/Pointer_Arithmetic11/test.desc
index f5e039ba3ed..b0acb9b5913 100644
--- a/regression/cbmc/Pointer_Arithmetic11/test.desc
+++ b/regression/cbmc/Pointer_Arithmetic11/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --pointer-check --little-endian
 ^EXIT=0$
diff --git a/regression/cbmc/Pointer_byte_extract2/test.desc b/regression/cbmc/Pointer_byte_extract2/test.desc
index eb98d4f78ba..e6619de477a 100644
--- a/regression/cbmc/Pointer_byte_extract2/test.desc
+++ b/regression/cbmc/Pointer_byte_extract2/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --little-endian
 ^EXIT=10$
diff --git a/regression/cbmc/Pointer_byte_extract5/no-simplify.desc b/regression/cbmc/Pointer_byte_extract5/no-simplify.desc
index 36c5519b60c..59ce8fd1c87 100644
--- a/regression/cbmc/Pointer_byte_extract5/no-simplify.desc
+++ b/regression/cbmc/Pointer_byte_extract5/no-simplify.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.i
 --bounds-check --32 --no-simplify
 ^EXIT=10$
diff --git a/regression/cbmc/Pointer_byte_extract5/test.desc b/regression/cbmc/Pointer_byte_extract5/test.desc
index 48d0d5d9c53..3d50935641c 100644
--- a/regression/cbmc/Pointer_byte_extract5/test.desc
+++ b/regression/cbmc/Pointer_byte_extract5/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.i
 --bounds-check --32
 ^EXIT=10$
diff --git a/regression/cbmc/Pointer_byte_extract9/test.desc b/regression/cbmc/Pointer_byte_extract9/test.desc
index 0570ab7aba7..61e6035ff74 100644
--- a/regression/cbmc/Pointer_byte_extract9/test.desc
+++ b/regression/cbmc/Pointer_byte_extract9/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 
 ^EXIT=10$
diff --git a/regression/cbmc/Promotion3/test.desc b/regression/cbmc/Promotion3/test.desc
index 9efefbc7362..39d9265e8a7 100644
--- a/regression/cbmc/Promotion3/test.desc
+++ b/regression/cbmc/Promotion3/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Quantifiers-assertion/test.desc b/regression/cbmc/Quantifiers-assertion/test.desc
index 46ce7f990fa..35df3d2bcd3 100644
--- a/regression/cbmc/Quantifiers-assertion/test.desc
+++ b/regression/cbmc/Quantifiers-assertion/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 
 ^\*\* Results:$
diff --git a/regression/cbmc/Quantifiers-assignment/test.desc b/regression/cbmc/Quantifiers-assignment/test.desc
index a584f718857..998d3865da2 100644
--- a/regression/cbmc/Quantifiers-assignment/test.desc
+++ b/regression/cbmc/Quantifiers-assignment/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 
 ^\*\* Results:$
diff --git a/regression/cbmc/Quantifiers-invalid-var-range/test.desc b/regression/cbmc/Quantifiers-invalid-var-range/test.desc
index 44f67109c0d..5ca881d80d9 100644
--- a/regression/cbmc/Quantifiers-invalid-var-range/test.desc
+++ b/regression/cbmc/Quantifiers-invalid-var-range/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+KNOWNBUG broken-smt-backend
 main.c
 
 ^\*\* Results:$
diff --git a/regression/cbmc/Quantifiers-type/test.desc b/regression/cbmc/Quantifiers-type/test.desc
index 88f7f2726ae..1c199246a4c 100644
--- a/regression/cbmc/Quantifiers-type/test.desc
+++ b/regression/cbmc/Quantifiers-type/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+KNOWNBUG broken-smt-backend
 main.c
 
 ^\*\* Results:$
diff --git a/regression/cbmc/Union_Initialization1/test.desc b/regression/cbmc/Union_Initialization1/test.desc
index 9efefbc7362..39d9265e8a7 100644
--- a/regression/cbmc/Union_Initialization1/test.desc
+++ b/regression/cbmc/Union_Initialization1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/address_space_size_limit1/test.desc b/regression/cbmc/address_space_size_limit1/test.desc
index d68272d8db5..3bc849b0cbf 100644
--- a/regression/cbmc/address_space_size_limit1/test.desc
+++ b/regression/cbmc/address_space_size_limit1/test.desc
@@ -1,4 +1,4 @@
-CORE thorough-paths
+CORE thorough-paths broken-smt-backend
 test.c
 --no-simplify --unwind 300 --object-bits 8
 too many addressed objects
diff --git a/regression/cbmc/array-function-parameters/test.desc b/regression/cbmc/array-function-parameters/test.desc
index 8e3b164c669..b515f2c66cb 100644
--- a/regression/cbmc/array-function-parameters/test.desc
+++ b/regression/cbmc/array-function-parameters/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 test.c
 --function test --min-null-tree-depth 2 --max-nondet-tree-depth 2 --bounds-check
 \[test.assertion.1\] line \d+ assertion Test.lists\[0\]->next: SUCCESS
diff --git a/regression/cbmc/array-tests/test.desc b/regression/cbmc/array-tests/test.desc
index 969d6de00f8..85d41d5205e 100644
--- a/regression/cbmc/array-tests/test.desc
+++ b/regression/cbmc/array-tests/test.desc
@@ -1,4 +1,4 @@
-CORE thorough-paths
+CORE thorough-paths broken-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/bounds_check1/test.desc b/regression/cbmc/bounds_check1/test.desc
index cba5d453936..28805d2437b 100644
--- a/regression/cbmc/bounds_check1/test.desc
+++ b/regression/cbmc/bounds_check1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --bounds-check --pointer-check
 ^EXIT=10$
diff --git a/regression/cbmc/byte_update2/test.desc b/regression/cbmc/byte_update2/test.desc
index 9845e70d84b..9d95b7efe83 100644
--- a/regression/cbmc/byte_update2/test.desc
+++ b/regression/cbmc/byte_update2/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --little-endian
 ^EXIT=0$
diff --git a/regression/cbmc/byte_update3/test.desc b/regression/cbmc/byte_update3/test.desc
index 9845e70d84b..9d95b7efe83 100644
--- a/regression/cbmc/byte_update3/test.desc
+++ b/regression/cbmc/byte_update3/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --little-endian
 ^EXIT=0$
diff --git a/regression/cbmc/byte_update4/test.desc b/regression/cbmc/byte_update4/test.desc
index 9845e70d84b..9d95b7efe83 100644
--- a/regression/cbmc/byte_update4/test.desc
+++ b/regression/cbmc/byte_update4/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --little-endian
 ^EXIT=0$
diff --git a/regression/cbmc/byte_update5/test.desc b/regression/cbmc/byte_update5/test.desc
index 9845e70d84b..9d95b7efe83 100644
--- a/regression/cbmc/byte_update5/test.desc
+++ b/regression/cbmc/byte_update5/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --little-endian
 ^EXIT=0$
diff --git a/regression/cbmc/byte_update6/test.desc b/regression/cbmc/byte_update6/test.desc
index 9845e70d84b..9d95b7efe83 100644
--- a/regression/cbmc/byte_update6/test.desc
+++ b/regression/cbmc/byte_update6/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --little-endian
 ^EXIT=0$
diff --git a/regression/cbmc/byte_update7/test.desc b/regression/cbmc/byte_update7/test.desc
index 9845e70d84b..9d95b7efe83 100644
--- a/regression/cbmc/byte_update7/test.desc
+++ b/regression/cbmc/byte_update7/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --little-endian
 ^EXIT=0$
diff --git a/regression/cbmc/byte_update8/test.desc b/regression/cbmc/byte_update8/test.desc
index 9845e70d84b..9d95b7efe83 100644
--- a/regression/cbmc/byte_update8/test.desc
+++ b/regression/cbmc/byte_update8/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --little-endian
 ^EXIT=0$
diff --git a/regression/cbmc/byte_update9/test.desc b/regression/cbmc/byte_update9/test.desc
index 81ceb4c6dc0..1b8f7c29219 100644
--- a/regression/cbmc/byte_update9/test.desc
+++ b/regression/cbmc/byte_update9/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --big-endian
 ^EXIT=0$
diff --git a/regression/cbmc/compact-trace/test.desc b/regression/cbmc/compact-trace/test.desc
index 60be5f3c51c..de9fedec0a0 100644
--- a/regression/cbmc/compact-trace/test.desc
+++ b/regression/cbmc/compact-trace/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --compact-trace
 activate-multi-line-match
diff --git a/regression/cbmc/dynamic_size1/stack_object.desc b/regression/cbmc/dynamic_size1/stack_object.desc
index 242e2c1d4c0..a618be0f5ef 100644
--- a/regression/cbmc/dynamic_size1/stack_object.desc
+++ b/regression/cbmc/dynamic_size1/stack_object.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 stack_object.c
 --pointer-check
 ^EXIT=0$
diff --git a/regression/cbmc/graphml_witness1/test.desc b/regression/cbmc/graphml_witness1/test.desc
index cb22eaba5d0..636f6bd5fa7 100644
--- a/regression/cbmc/graphml_witness1/test.desc
+++ b/regression/cbmc/graphml_witness1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --graphml-witness -
 ^EXIT=10$
diff --git a/regression/cbmc/integer-assignments1/test.desc b/regression/cbmc/integer-assignments1/test.desc
index 5c7cefb0433..4354f466552 100644
--- a/regression/cbmc/integer-assignments1/test.desc
+++ b/regression/cbmc/integer-assignments1/test.desc
@@ -1,4 +1,4 @@
-CORE smt-backend
+CORE smt-backend broken-smt-backend
 main.c
 --trace --smt2
 ^EXIT=10$
diff --git a/regression/cbmc/memory_allocation1/test.desc b/regression/cbmc/memory_allocation1/test.desc
index 77c4e0af53a..12560af6f29 100644
--- a/regression/cbmc/memory_allocation1/test.desc
+++ b/regression/cbmc/memory_allocation1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --pointer-check
 ^EXIT=10$
diff --git a/regression/cbmc/pointer-function-parameters-struct-mutual-recursion/test.desc b/regression/cbmc/pointer-function-parameters-struct-mutual-recursion/test.desc
index 7b82cc87646..34ef0e95c22 100644
--- a/regression/cbmc/pointer-function-parameters-struct-mutual-recursion/test.desc
+++ b/regression/cbmc/pointer-function-parameters-struct-mutual-recursion/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --function func --min-null-tree-depth 10 --max-nondet-tree-depth 3 --pointer-check
 ^EXIT=0$
diff --git a/regression/cbmc/pointer-function-parameters-struct-simple-recursion-2/test.desc b/regression/cbmc/pointer-function-parameters-struct-simple-recursion-2/test.desc
index 716670ff6f7..bfd4bca0d54 100644
--- a/regression/cbmc/pointer-function-parameters-struct-simple-recursion-2/test.desc
+++ b/regression/cbmc/pointer-function-parameters-struct-simple-recursion-2/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --function func --min-null-tree-depth 10 --max-nondet-tree-depth 2 --pointer-check
 ^EXIT=0$
diff --git a/regression/cbmc/pointer-function-parameters-struct-simple-recursion/test.desc b/regression/cbmc/pointer-function-parameters-struct-simple-recursion/test.desc
index 7b82cc87646..34ef0e95c22 100644
--- a/regression/cbmc/pointer-function-parameters-struct-simple-recursion/test.desc
+++ b/regression/cbmc/pointer-function-parameters-struct-simple-recursion/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --function func --min-null-tree-depth 10 --max-nondet-tree-depth 3 --pointer-check
 ^EXIT=0$
diff --git a/regression/cbmc/scanf1/test.desc b/regression/cbmc/scanf1/test.desc
index 346519020ae..3dba1ea8007 100644
--- a/regression/cbmc/scanf1/test.desc
+++ b/regression/cbmc/scanf1/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.i
 --little-endian
 ^EXIT=10$
diff --git a/regression/cbmc/stack-trace/test.desc b/regression/cbmc/stack-trace/test.desc
index eceab4a2d07..6270581f4fd 100644
--- a/regression/cbmc/stack-trace/test.desc
+++ b/regression/cbmc/stack-trace/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --stack-trace
 activate-multi-line-match
diff --git a/regression/cbmc/struct6/test.desc b/regression/cbmc/struct6/test.desc
index da239c1965b..148fe24db7c 100644
--- a/regression/cbmc/struct6/test.desc
+++ b/regression/cbmc/struct6/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --bounds-check --pointer-check
 ^EXIT=0$
diff --git a/regression/cbmc/struct7/test.desc b/regression/cbmc/struct7/test.desc
index 96c9b4bcd7b..35db6e71ddb 100644
--- a/regression/cbmc/struct7/test.desc
+++ b/regression/cbmc/struct7/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --pointer-check --bounds-check
 ^EXIT=0$
diff --git a/regression/cbmc/trace-values/trace-values.desc b/regression/cbmc/trace-values/trace-values.desc
index f05af5e719e..b64fd79b8bf 100644
--- a/regression/cbmc/trace-values/trace-values.desc
+++ b/regression/cbmc/trace-values/trace-values.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 trace-values.c
 --trace
 ^EXIT=10$
diff --git a/regression/cbmc/trace_show_function_calls/test.desc b/regression/cbmc/trace_show_function_calls/test.desc
index 3be4b2cfbab..921cb7ca234 100644
--- a/regression/cbmc/trace_show_function_calls/test.desc
+++ b/regression/cbmc/trace_show_function_calls/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --trace --trace-show-function-calls
 ^EXIT=10$
diff --git a/regression/cbmc/uninterpreted_function/uf1.desc b/regression/cbmc/uninterpreted_function/uf1.desc
index 879865e93e3..cb6fb66d3c8 100644
--- a/regression/cbmc/uninterpreted_function/uf1.desc
+++ b/regression/cbmc/uninterpreted_function/uf1.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 uf1.c
 
 ^EXIT=10$
diff --git a/regression/cbmc/uninterpreted_function/uf2.desc b/regression/cbmc/uninterpreted_function/uf2.desc
index b0daa371dd8..7f1cf4603e5 100644
--- a/regression/cbmc/uninterpreted_function/uf2.desc
+++ b/regression/cbmc/uninterpreted_function/uf2.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 uf2.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/union12/test.desc b/regression/cbmc/union12/test.desc
index 82b3a34754a..d568171b1a6 100644
--- a/regression/cbmc/union12/test.desc
+++ b/regression/cbmc/union12/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --pointer-check
 ^EXIT=10$
diff --git a/regression/cbmc/union6/test.desc b/regression/cbmc/union6/test.desc
index 9845e70d84b..9d95b7efe83 100644
--- a/regression/cbmc/union6/test.desc
+++ b/regression/cbmc/union6/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --little-endian
 ^EXIT=0$
diff --git a/regression/cbmc/union7/test.desc b/regression/cbmc/union7/test.desc
index 81ceb4c6dc0..1b8f7c29219 100644
--- a/regression/cbmc/union7/test.desc
+++ b/regression/cbmc/union7/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --big-endian
 ^EXIT=0$
diff --git a/regression/cbmc/union9/test.desc b/regression/cbmc/union9/test.desc
index 9efefbc7362..39d9265e8a7 100644
--- a/regression/cbmc/union9/test.desc
+++ b/regression/cbmc/union9/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/variable-access-to-constant-array/test.desc b/regression/cbmc/variable-access-to-constant-array/test.desc
index 6de79559914..59d65ddf9f7 100644
--- a/regression/cbmc/variable-access-to-constant-array/test.desc
+++ b/regression/cbmc/variable-access-to-constant-array/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 
 ^EXIT=10$
diff --git a/regression/cbmc/void_pointer2/test.desc b/regression/cbmc/void_pointer2/test.desc
index 3556481d977..a59cfa54721 100644
--- a/regression/cbmc/void_pointer2/test.desc
+++ b/regression/cbmc/void_pointer2/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 --pointer-check --no-simplify --unwind 3
 ^EXIT=0$
diff --git a/regression/cbmc/void_pointer3/test.desc b/regression/cbmc/void_pointer3/test.desc
index 9efefbc7362..39d9265e8a7 100644
--- a/regression/cbmc/void_pointer3/test.desc
+++ b/regression/cbmc/void_pointer3/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/void_pointer4/test.desc b/regression/cbmc/void_pointer4/test.desc
index 6de79559914..59d65ddf9f7 100644
--- a/regression/cbmc/void_pointer4/test.desc
+++ b/regression/cbmc/void_pointer4/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE broken-smt-backend
 main.c
 
 ^EXIT=10$
diff --git a/scripts/delete_failing_smt2_solver_tests b/scripts/delete_failing_smt2_solver_tests
deleted file mode 100755
index 1cd691e5d74..00000000000
--- a/scripts/delete_failing_smt2_solver_tests
+++ /dev/null
@@ -1,87 +0,0 @@
-#!/bin/sh
-
-cd regression/cbmc
-rm Anonymous_Struct3/test.desc
-rm Array_operations1/test.desc
-rm Bitfields3/test.desc
-rm Bitfields3/paths.desc
-rm Empty_struct1/test.desc
-rm Endianness4/test.desc
-rm Endianness6/test.desc
-rm Float-div2/test.desc
-rm Float-div3/test.desc
-rm Float-no-simp1/test.desc
-rm Float-no-simp2/test.desc
-rm Float-no-simp3/test.desc
-rm Float-no-simp4/test.desc
-rm Float-no-simp5/test.desc
-rm Float-no-simp6/test.desc
-rm Float-no-simp7/test.desc
-rm Float-smt2-1/test.desc
-rm Float-to-double2/test.desc
-rm Float-to-int1/test.desc
-rm Float-to-int2/test.desc
-rm Float-to-int3/test.desc
-rm Float-zero-sum1/test.desc
-rm Float12/test.desc
-rm Float13/test.desc
-rm Float20/test.desc
-rm Float22/test.desc
-rm Float23/test.desc
-rm Float3/test.desc
-rm Float4/test.desc
-rm Float5/test.desc
-rm Float6/test.desc
-rm Float8/test.desc
-rm Linking4/test.desc
-rm Linking7/test.desc
-rm Linking7/member-name-mismatch.desc
-rm Malloc23/test.desc
-rm Multi_Dimensional_Array2/test.desc
-rm Pointer_Arithmetic11/test.desc
-rm Pointer_byte_extract2/test.desc
-rm Pointer_byte_extract5/no-simplify.desc
-rm Pointer_byte_extract5/test.desc
-rm Pointer_byte_extract9/test.desc
-rm Promotion3/test.desc
-rm Quantifiers-assertion/test.desc
-rm Quantifiers-assignment/test.desc
-rm Quantifiers-invalid-var-range/test.desc
-rm Quantifiers-type/test.desc
-rm Union_Initialization1/test.desc
-rm address_space_size_limit1/test.desc
-rm array-function-parameters/test.desc
-rm array-tests/test.desc
-rm bounds_check1/test.desc
-rm byte_update2/test.desc
-rm byte_update3/test.desc
-rm byte_update4/test.desc
-rm byte_update5/test.desc
-rm byte_update6/test.desc
-rm byte_update7/test.desc
-rm byte_update8/test.desc
-rm byte_update9/test.desc
-rm compact-trace/test.desc
-rm dynamic_size1/stack_object.desc
-rm graphml_witness1/test.desc
-rm integer-assignments1/test.desc
-rm memory_allocation1/test.desc
-rm pointer-function-parameters-struct-mutual-recursion/test.desc
-rm pointer-function-parameters-struct-simple-recursion/test.desc
-rm pointer-function-parameters-struct-simple-recursion-2/test.desc
-rm scanf1/test.desc
-rm stack-trace/test.desc
-rm struct6/test.desc
-rm struct7/test.desc
-rm trace-values/trace-values.desc
-rm trace_show_function_calls/test.desc
-rm uninterpreted_function/uf1.desc
-rm uninterpreted_function/uf2.desc
-rm union12/test.desc
-rm union6/test.desc
-rm union7/test.desc
-rm union9/test.desc
-rm variable-access-to-constant-array/test.desc
-rm void_pointer2/test.desc
-rm void_pointer3/test.desc
-rm void_pointer4/test.desc