diff --git a/regression/cbmc-cover/pointer-function-parameters-struct-simple-recursion-3/test.desc b/regression/cbmc-cover/pointer-function-parameters-struct-simple-recursion-3/test.desc
index de61e8009ea..d718acf6f82 100644
--- a/regression/cbmc-cover/pointer-function-parameters-struct-simple-recursion-3/test.desc
+++ b/regression/cbmc-cover/pointer-function-parameters-struct-simple-recursion-3/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --function func --min-null-tree-depth 2 --max-nondet-tree-depth 10 --cover branch
 ^EXIT=0$
diff --git a/regression/cbmc/CMakeLists.txt b/regression/cbmc/CMakeLists.txt
index 1785e0f124b..bb900107e38 100644
--- a/regression/cbmc/CMakeLists.txt
+++ b/regression/cbmc/CMakeLists.txt
@@ -1,3 +1,3 @@
 add_test_pl_tests(
-    "$<TARGET_FILE:cbmc>" -X smt-backend
+    "$<TARGET_FILE:cbmc> --validate-goto-model" -X smt-backend
 )
diff --git a/regression/cbmc/Float-zero-sum1/test.desc b/regression/cbmc/Float-zero-sum1/test.desc
index 4d2a93e6e26..26cf28c608c 100644
--- a/regression/cbmc/Float-zero-sum1/test.desc
+++ b/regression/cbmc/Float-zero-sum1/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --floatbv --no-simplify
 ^EXIT=0$
diff --git a/regression/cbmc/Float22/test.desc b/regression/cbmc/Float22/test.desc
index b7d95a28215..a8eaa6d68f7 100644
--- a/regression/cbmc/Float22/test.desc
+++ b/regression/cbmc/Float22/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --floatbv
 ^EXIT=0$
diff --git a/regression/cbmc/Function10/test.desc b/regression/cbmc/Function10/test.desc
index 9efefbc7362..52168c7eba4 100644
--- a/regression/cbmc/Function10/test.desc
+++ b/regression/cbmc/Function10/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Function12/test.desc b/regression/cbmc/Function12/test.desc
index 9efefbc7362..52168c7eba4 100644
--- a/regression/cbmc/Function12/test.desc
+++ b/regression/cbmc/Function12/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Function_Pointer10/test.desc b/regression/cbmc/Function_Pointer10/test.desc
index 9efefbc7362..52168c7eba4 100644
--- a/regression/cbmc/Function_Pointer10/test.desc
+++ b/regression/cbmc/Function_Pointer10/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Function_Pointer11/test.desc b/regression/cbmc/Function_Pointer11/test.desc
index 9efefbc7362..52168c7eba4 100644
--- a/regression/cbmc/Function_Pointer11/test.desc
+++ b/regression/cbmc/Function_Pointer11/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Function_Pointer8/test.desc b/regression/cbmc/Function_Pointer8/test.desc
index 33900ad2b78..fb5fd7bb84f 100644
--- a/regression/cbmc/Function_Pointer8/test.desc
+++ b/regression/cbmc/Function_Pointer8/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=10$
diff --git a/regression/cbmc/Global_Initialization2/test.desc b/regression/cbmc/Global_Initialization2/test.desc
index 9efefbc7362..52168c7eba4 100644
--- a/regression/cbmc/Global_Initialization2/test.desc
+++ b/regression/cbmc/Global_Initialization2/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Linking7/return_type.desc b/regression/cbmc/Linking7/return_type.desc
index e51bc4611dd..5f02c2bd929 100644
--- a/regression/cbmc/Linking7/return_type.desc
+++ b/regression/cbmc/Linking7/return_type.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 return_type1.c
 return_type2.c
 ^EXIT=0$
diff --git a/regression/cbmc/Makefile b/regression/cbmc/Makefile
index d86a43477e6..41cc877803e 100644
--- a/regression/cbmc/Makefile
+++ b/regression/cbmc/Makefile
@@ -1,13 +1,12 @@
-default: tests.log
+default: test
 
 test:
-	@../test.pl -p -c ../../../src/cbmc/cbmc -X smt-backend
+	@../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"
 
-tests.log: ../test.pl
-	@../test.pl -p -c ../../../src/cbmc/cbmc -X smt-backend
+tests.log: ../test.pl test
 
 show:
 	@for dir in *; do \
diff --git a/regression/cbmc/Malloc16/test.desc b/regression/cbmc/Malloc16/test.desc
index a1b2c8b18ec..5efa9ce40f8 100644
--- a/regression/cbmc/Malloc16/test.desc
+++ b/regression/cbmc/Malloc16/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.i
 --32
 ^EXIT=0$
diff --git a/regression/cbmc/Zero_Initialization1/test.desc b/regression/cbmc/Zero_Initialization1/test.desc
index 9efefbc7362..52168c7eba4 100644
--- a/regression/cbmc/Zero_Initialization1/test.desc
+++ b/regression/cbmc/Zero_Initialization1/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/array-function-parameters/test.desc b/regression/cbmc/array-function-parameters/test.desc
index 8e3b164c669..ccaff096c31 100644
--- a/regression/cbmc/array-function-parameters/test.desc
+++ b/regression/cbmc/array-function-parameters/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 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/atomic_section_seq1/test.desc b/regression/cbmc/atomic_section_seq1/test.desc
index 6de79559914..6b765c70f48 100644
--- a/regression/cbmc/atomic_section_seq1/test.desc
+++ b/regression/cbmc/atomic_section_seq1/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=10$
diff --git a/regression/cbmc/compact-trace/test.desc b/regression/cbmc/compact-trace/test.desc
index 60be5f3c51c..8645ae07ac2 100644
--- a/regression/cbmc/compact-trace/test.desc
+++ b/regression/cbmc/compact-trace/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --compact-trace
 activate-multi-line-match
diff --git a/regression/cbmc/constructor1/test.desc b/regression/cbmc/constructor1/test.desc
index 9efefbc7362..52168c7eba4 100644
--- a/regression/cbmc/constructor1/test.desc
+++ b/regression/cbmc/constructor1/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/enum1/test.desc b/regression/cbmc/enum1/test.desc
index 9efefbc7362..52168c7eba4 100644
--- a/regression/cbmc/enum1/test.desc
+++ b/regression/cbmc/enum1/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/enum2/test.desc b/regression/cbmc/enum2/test.desc
index 9efefbc7362..52168c7eba4 100644
--- a/regression/cbmc/enum2/test.desc
+++ b/regression/cbmc/enum2/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/gcc_statement_expression3/test.desc b/regression/cbmc/gcc_statement_expression3/test.desc
index 9c96469df12..a27d6e3414c 100644
--- a/regression/cbmc/gcc_statement_expression3/test.desc
+++ b/regression/cbmc/gcc_statement_expression3/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/memset1/test.desc b/regression/cbmc/memset1/test.desc
index db4ec3e73bf..259a711423d 100644
--- a/regression/cbmc/memset1/test.desc
+++ b/regression/cbmc/memset1/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=10$
diff --git a/regression/cbmc/memset2/test.desc b/regression/cbmc/memset2/test.desc
index 9efefbc7362..52168c7eba4 100644
--- a/regression/cbmc/memset2/test.desc
+++ b/regression/cbmc/memset2/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/memset3/test.desc b/regression/cbmc/memset3/test.desc
index be58134bdcb..32894d6b475 100644
--- a/regression/cbmc/memset3/test.desc
+++ b/regression/cbmc/memset3/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --pointer-check
 ^EXIT=10$
diff --git a/regression/cbmc/noop1/test.desc b/regression/cbmc/noop1/test.desc
index 9efefbc7362..52168c7eba4 100644
--- a/regression/cbmc/noop1/test.desc
+++ b/regression/cbmc/noop1/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/path-branch-pointer-call/test.desc b/regression/cbmc/path-branch-pointer-call/test.desc
index 5ea1d977cab..76945048e1f 100644
--- a/regression/cbmc/path-branch-pointer-call/test.desc
+++ b/regression/cbmc/path-branch-pointer-call/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --paths lifo
 ^EXIT=0$
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..cae522dd641 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
+KNOWNBUG
 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-non-recursive/test.desc b/regression/cbmc/pointer-function-parameters-struct-non-recursive/test.desc
index a90929db40c..f7acdd4cde1 100644
--- a/regression/cbmc/pointer-function-parameters-struct-non-recursive/test.desc
+++ b/regression/cbmc/pointer-function-parameters-struct-non-recursive/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --function func --min-null-tree-depth 10
 ^EXIT=10$
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..9eefe10ac84 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
+KNOWNBUG
 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..cae522dd641 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
+KNOWNBUG
 main.c
 --function func --min-null-tree-depth 10 --max-nondet-tree-depth 3 --pointer-check
 ^EXIT=0$
diff --git a/regression/cbmc/reachability-slice-interproc2/test.desc b/regression/cbmc/reachability-slice-interproc2/test.desc
index b10acfc02b3..997ec438bc2 100644
--- a/regression/cbmc/reachability-slice-interproc2/test.desc
+++ b/regression/cbmc/reachability-slice-interproc2/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --reachability-slice --show-goto-functions
 ^EXIT=0$
diff --git a/regression/cbmc/return1/test.desc b/regression/cbmc/return1/test.desc
index 9efefbc7362..52168c7eba4 100644
--- a/regression/cbmc/return1/test.desc
+++ b/regression/cbmc/return1/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/show_properties1/test.desc b/regression/cbmc/show_properties1/test.desc
index 96b4816a1fb..e424c9fdf48 100644
--- a/regression/cbmc/show_properties1/test.desc
+++ b/regression/cbmc/show_properties1/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --pointer-check --show-properties
 ^EXIT=0$
diff --git a/regression/cbmc/simplify-full-test/test.desc b/regression/cbmc/simplify-full-test/test.desc
index 9efefbc7362..52168c7eba4 100644
--- a/regression/cbmc/simplify-full-test/test.desc
+++ b/regression/cbmc/simplify-full-test/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/simplify-function-call-array-element-pointer/test.desc b/regression/cbmc/simplify-function-call-array-element-pointer/test.desc
index 9efefbc7362..52168c7eba4 100644
--- a/regression/cbmc/simplify-function-call-array-element-pointer/test.desc
+++ b/regression/cbmc/simplify-function-call-array-element-pointer/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/simplify-function-call-array-pointer/test.desc b/regression/cbmc/simplify-function-call-array-pointer/test.desc
index 9efefbc7362..52168c7eba4 100644
--- a/regression/cbmc/simplify-function-call-array-pointer/test.desc
+++ b/regression/cbmc/simplify-function-call-array-pointer/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/simplify-function-call-pointer-access/test.desc b/regression/cbmc/simplify-function-call-pointer-access/test.desc
index 9efefbc7362..52168c7eba4 100644
--- a/regression/cbmc/simplify-function-call-pointer-access/test.desc
+++ b/regression/cbmc/simplify-function-call-pointer-access/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/stack-trace/test.desc b/regression/cbmc/stack-trace/test.desc
index eceab4a2d07..6a120b41a60 100644
--- a/regression/cbmc/stack-trace/test.desc
+++ b/regression/cbmc/stack-trace/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --stack-trace
 activate-multi-line-match
diff --git a/regression/cbmc/switch6/test.desc b/regression/cbmc/switch6/test.desc
index 9efefbc7362..52168c7eba4 100644
--- a/regression/cbmc/switch6/test.desc
+++ b/regression/cbmc/switch6/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/trace-values/trace-values.desc b/regression/cbmc/trace-values/trace-values.desc
index f05af5e719e..eb6a5080ad6 100644
--- a/regression/cbmc/trace-values/trace-values.desc
+++ b/regression/cbmc/trace-values/trace-values.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 trace-values.c
 --trace
 ^EXIT=10$
diff --git a/regression/cbmc/typedef-param-anon-union1/test.desc b/regression/cbmc/typedef-param-anon-union1/test.desc
index 34c29cefda9..9b0e5d16145 100644
--- a/regression/cbmc/typedef-param-anon-union1/test.desc
+++ b/regression/cbmc/typedef-param-anon-union1/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --show-symbol-table --function fun
 // Enable multi-line checking
diff --git a/regression/cbmc/typedef-param-union1/test.desc b/regression/cbmc/typedef-param-union1/test.desc
index 37ab0aee08c..e2e7354154d 100644
--- a/regression/cbmc/typedef-param-union1/test.desc
+++ b/regression/cbmc/typedef-param-union1/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --show-symbol-table --function fun
 // Enable multi-line checking