diff --git a/jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/test.desc b/jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/test.desc
index 386cc37503d..e86695bcf0b 100644
--- a/jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/test.desc
+++ b/jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 A.class
 --function 'A.me:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/test2.desc b/jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/test2.desc
index c39ba088b5b..7abf671b92b 100644
--- a/jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/test2.desc
+++ b/jbmc/regression/jbmc-concurrency/anonymous-java.lang.thread/test2.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 A.class
 --function 'A.me2:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^SIGNAL=0$
diff --git a/jbmc/regression/jbmc-concurrency/explicit-thread-blocks/test.desc b/jbmc/regression/jbmc-concurrency/explicit-thread-blocks/test.desc
index 01ab8385b37..1504fb15b63 100644
--- a/jbmc/regression/jbmc-concurrency/explicit-thread-blocks/test.desc
+++ b/jbmc/regression/jbmc-concurrency/explicit-thread-blocks/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 A.class
 --function 'A.me:()V' --java-threading
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-concurrency/explicit-thread-blocks/test2.desc b/jbmc/regression/jbmc-concurrency/explicit-thread-blocks/test2.desc
index 545f4effa2b..9f780aeaeef 100644
--- a/jbmc/regression/jbmc-concurrency/explicit-thread-blocks/test2.desc
+++ b/jbmc/regression/jbmc-concurrency/explicit-thread-blocks/test2.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 A.class
 --function 'A.me2:()V' --java-threading
 ^SIGNAL=0$
diff --git a/jbmc/regression/jbmc-concurrency/get-current-thread/test.desc b/jbmc/regression/jbmc-concurrency/get-current-thread/test.desc
index 124afa21ae7..6b44afcffc3 100644
--- a/jbmc/regression/jbmc-concurrency/get-current-thread/test.desc
+++ b/jbmc/regression/jbmc-concurrency/get-current-thread/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 A.class
 --function 'A.me:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-concurrency/get-current-thread/test4.desc b/jbmc/regression/jbmc-concurrency/get-current-thread/test4.desc
index 8ceb063f4f9..53ae3cb75c0 100644
--- a/jbmc/regression/jbmc-concurrency/get-current-thread/test4.desc
+++ b/jbmc/regression/jbmc-concurrency/get-current-thread/test4.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 A.class
 --function 'A.me4:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-concurrency/get-current-thread/test5.desc b/jbmc/regression/jbmc-concurrency/get-current-thread/test5.desc
index 6522d6f95a2..2d6eb10ff2c 100644
--- a/jbmc/regression/jbmc-concurrency/get-current-thread/test5.desc
+++ b/jbmc/regression/jbmc-concurrency/get-current-thread/test5.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 A.class
 --function 'A.me5:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-concurrency/get-current-thread/test6.desc b/jbmc/regression/jbmc-concurrency/get-current-thread/test6.desc
index 6bb22f0f8f9..e149d7dbbd5 100644
--- a/jbmc/regression/jbmc-concurrency/get-current-thread/test6.desc
+++ b/jbmc/regression/jbmc-concurrency/get-current-thread/test6.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 A.class
 --function 'A.me6:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-concurrency/java-lang-runnable/test.desc b/jbmc/regression/jbmc-concurrency/java-lang-runnable/test.desc
index 60b60587f48..f8497452001 100644
--- a/jbmc/regression/jbmc-concurrency/java-lang-runnable/test.desc
+++ b/jbmc/regression/jbmc-concurrency/java-lang-runnable/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 A.class
 --function 'A.me:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-concurrency/java-lang-runnable/test2.desc b/jbmc/regression/jbmc-concurrency/java-lang-runnable/test2.desc
index 02c95662b4b..c55453ab122 100644
--- a/jbmc/regression/jbmc-concurrency/java-lang-runnable/test2.desc
+++ b/jbmc/regression/jbmc-concurrency/java-lang-runnable/test2.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 A.class
 --function 'A.me2:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
 ^SIGNAL=0$
diff --git a/jbmc/regression/jbmc-concurrency/java-lang-runnable/test3.desc b/jbmc/regression/jbmc-concurrency/java-lang-runnable/test3.desc
index 3b9c0e1421f..91e86c91d8d 100644
--- a/jbmc/regression/jbmc-concurrency/java-lang-runnable/test3.desc
+++ b/jbmc/regression/jbmc-concurrency/java-lang-runnable/test3.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 A.class
 --function 'A.me4:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-concurrency/java-lang-runnable/test4.desc b/jbmc/regression/jbmc-concurrency/java-lang-runnable/test4.desc
index eb5d686f26a..696f4caa341 100644
--- a/jbmc/regression/jbmc-concurrency/java-lang-runnable/test4.desc
+++ b/jbmc/regression/jbmc-concurrency/java-lang-runnable/test4.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 A.class
 --function 'A.me3:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-concurrency/java-lang-thread/test.desc b/jbmc/regression/jbmc-concurrency/java-lang-thread/test.desc
index 8eec4067339..1e700fbb638 100644
--- a/jbmc/regression/jbmc-concurrency/java-lang-thread/test.desc
+++ b/jbmc/regression/jbmc-concurrency/java-lang-thread/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 A.class
 --function 'A.me:()V'  --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-concurrency/java-lang-thread/test2.desc b/jbmc/regression/jbmc-concurrency/java-lang-thread/test2.desc
index dbde3635d9f..19d8e21c2a9 100644
--- a/jbmc/regression/jbmc-concurrency/java-lang-thread/test2.desc
+++ b/jbmc/regression/jbmc-concurrency/java-lang-thread/test2.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 A.class
 --function 'A.me2:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
 ^SIGNAL=0$
diff --git a/jbmc/regression/jbmc-concurrency/java-lang-thread/test3.desc b/jbmc/regression/jbmc-concurrency/java-lang-thread/test3.desc
index a4e55bfa5ec..ddecee43b79 100644
--- a/jbmc/regression/jbmc-concurrency/java-lang-thread/test3.desc
+++ b/jbmc/regression/jbmc-concurrency/java-lang-thread/test3.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 A.class
 --function 'A.me4:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/jbmc-concurrency/java-lang-thread/test4.desc b/jbmc/regression/jbmc-concurrency/java-lang-thread/test4.desc
index 0fc102be1da..31524f4d506 100644
--- a/jbmc/regression/jbmc-concurrency/java-lang-thread/test4.desc
+++ b/jbmc/regression/jbmc-concurrency/java-lang-thread/test4.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 A.class
 --function 'A.me3:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/jbmc-concurrency/several-threads/test.desc b/jbmc/regression/jbmc-concurrency/several-threads/test.desc
index cfd4860376d..598a2270e9b 100644
--- a/jbmc/regression/jbmc-concurrency/several-threads/test.desc
+++ b/jbmc/regression/jbmc-concurrency/several-threads/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 A.class
 --function A.me --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-concurrency/several-threads/test2.desc b/jbmc/regression/jbmc-concurrency/several-threads/test2.desc
index acfc61c48c6..60027b5eea0 100644
--- a/jbmc/regression/jbmc-concurrency/several-threads/test2.desc
+++ b/jbmc/regression/jbmc-concurrency/several-threads/test2.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 A.class
 --function A.me2 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
 ^SIGNAL=0$
diff --git a/jbmc/regression/jbmc-concurrency/several-threads/test3.desc b/jbmc/regression/jbmc-concurrency/several-threads/test3.desc
index cbcd840a1e0..76c507cb2c1 100644
--- a/jbmc/regression/jbmc-concurrency/several-threads/test3.desc
+++ b/jbmc/regression/jbmc-concurrency/several-threads/test3.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 A.class
 --function A.me3 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading --unwind 3
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks/test1.desc b/jbmc/regression/jbmc-concurrency/synchronized-blocks/test1.desc
index f284db38cf3..7ab4ac1be3a 100644
--- a/jbmc/regression/jbmc-concurrency/synchronized-blocks/test1.desc
+++ b/jbmc/regression/jbmc-concurrency/synchronized-blocks/test1.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 A.class
 --function 'A.me0:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --show-goto-functions --java-threading
 ATOMIC_BEGIN
diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks/test2.desc b/jbmc/regression/jbmc-concurrency/synchronized-blocks/test2.desc
index ec805ab619a..3ad43306642 100644
--- a/jbmc/regression/jbmc-concurrency/synchronized-blocks/test2.desc
+++ b/jbmc/regression/jbmc-concurrency/synchronized-blocks/test2.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 A.class
 --function 'A.me0:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks/test3.desc b/jbmc/regression/jbmc-concurrency/synchronized-blocks/test3.desc
index ec805ab619a..3ad43306642 100644
--- a/jbmc/regression/jbmc-concurrency/synchronized-blocks/test3.desc
+++ b/jbmc/regression/jbmc-concurrency/synchronized-blocks/test3.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 A.class
 --function 'A.me0:()V' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks/test_sync.desc b/jbmc/regression/jbmc-concurrency/synchronized-blocks/test_sync.desc
index 824bc5b0d11..61916f0b547 100644
--- a/jbmc/regression/jbmc-concurrency/synchronized-blocks/test_sync.desc
+++ b/jbmc/regression/jbmc-concurrency/synchronized-blocks/test_sync.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 A.class
 --function 'A.me2:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-concurrency/synchronized-blocks/test_sync_baseline.desc b/jbmc/regression/jbmc-concurrency/synchronized-blocks/test_sync_baseline.desc
index 550429547e4..3533c599649 100644
--- a/jbmc/regression/jbmc-concurrency/synchronized-blocks/test_sync_baseline.desc
+++ b/jbmc/regression/jbmc-concurrency/synchronized-blocks/test_sync_baseline.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 A.class
 --function 'A.me1:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-concurrency/synchronized-method-illegal-state/test.desc b/jbmc/regression/jbmc-concurrency/synchronized-method-illegal-state/test.desc
index 22eaef591e3..64df33e2853 100644
--- a/jbmc/regression/jbmc-concurrency/synchronized-method-illegal-state/test.desc
+++ b/jbmc/regression/jbmc-concurrency/synchronized-method-illegal-state/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 Sync.class
 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --java-threading
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/jbmc-concurrency/synchronized-methods/test1.desc b/jbmc/regression/jbmc-concurrency/synchronized-methods/test1.desc
index 32be2704a71..03f933e43c4 100644
--- a/jbmc/regression/jbmc-concurrency/synchronized-methods/test1.desc
+++ b/jbmc/regression/jbmc-concurrency/synchronized-methods/test1.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 A.class
 --function 'A.me1:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --show-goto-functions
 ATOMIC_BEGIN
diff --git a/jbmc/regression/jbmc-concurrency/synchronized-methods/test2.desc b/jbmc/regression/jbmc-concurrency/synchronized-methods/test2.desc
index 4420b0af9f2..2bb231e01b4 100644
--- a/jbmc/regression/jbmc-concurrency/synchronized-methods/test2.desc
+++ b/jbmc/regression/jbmc-concurrency/synchronized-methods/test2.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 A.class
 --function 'A.me1:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --show-goto-functions
 ATOMIC_BEGIN
diff --git a/jbmc/regression/jbmc-concurrency/synchronized-methods/test3.desc b/jbmc/regression/jbmc-concurrency/synchronized-methods/test3.desc
index e79944afd03..5a3b0ef3046 100644
--- a/jbmc/regression/jbmc-concurrency/synchronized-methods/test3.desc
+++ b/jbmc/regression/jbmc-concurrency/synchronized-methods/test3.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 A.class
 --function 'A.me1:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-concurrency/synchronized-methods/test_sync.desc b/jbmc/regression/jbmc-concurrency/synchronized-methods/test_sync.desc
index 3d6edf4b922..7e2cdeaec5b 100644
--- a/jbmc/regression/jbmc-concurrency/synchronized-methods/test_sync.desc
+++ b/jbmc/regression/jbmc-concurrency/synchronized-methods/test_sync.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 A.class
 --function 'A.me3:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-concurrency/synchronized-methods/test_sync_baseline.desc b/jbmc/regression/jbmc-concurrency/synchronized-methods/test_sync_baseline.desc
index 824bc5b0d11..61916f0b547 100644
--- a/jbmc/regression/jbmc-concurrency/synchronized-methods/test_sync_baseline.desc
+++ b/jbmc/regression/jbmc-concurrency/synchronized-methods/test_sync_baseline.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 A.class
 --function 'A.me2:()V' --java-threading --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-concurrency/synchronized/test.desc b/jbmc/regression/jbmc-concurrency/synchronized/test.desc
index 5921af6c569..b0d5612e028 100644
--- a/jbmc/regression/jbmc-concurrency/synchronized/test.desc
+++ b/jbmc/regression/jbmc-concurrency/synchronized/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 Sync.class
 --java-threading --throw-runtime-exceptions --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc/static_init1/test1.desc b/jbmc/regression/jbmc/static_init1/test1.desc
index 8bc396cff4d..75eb56c36f3 100644
--- a/jbmc/regression/jbmc/static_init1/test1.desc
+++ b/jbmc/regression/jbmc/static_init1/test1.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 static_init.class
 --function static_init.main --java-threading
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc/static_init2/test1.desc b/jbmc/regression/jbmc/static_init2/test1.desc
index 8bc396cff4d..75eb56c36f3 100644
--- a/jbmc/regression/jbmc/static_init2/test1.desc
+++ b/jbmc/regression/jbmc/static_init2/test1.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 static_init.class
 --function static_init.main --java-threading
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc/static_init_order/test3.desc b/jbmc/regression/jbmc/static_init_order/test3.desc
index 6ec4686fa57..250f1882331 100644
--- a/jbmc/regression/jbmc/static_init_order/test3.desc
+++ b/jbmc/regression/jbmc/static_init_order/test3.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 static_init_order.class
 --function static_init_order.test1 --trace --java-threading
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc/static_init_order/test4.desc b/jbmc/regression/jbmc/static_init_order/test4.desc
index d008222606e..dd7464b0d74 100644
--- a/jbmc/regression/jbmc/static_init_order/test4.desc
+++ b/jbmc/regression/jbmc/static_init_order/test4.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 static_init_order.class
 --function static_init_order.test2 --java-threading
 ^EXIT=10$
diff --git a/regression/ansi-c/const1/const-array.desc b/regression/ansi-c/const1/const-array.desc
index d244eaf4c74..c2f198d356e 100644
--- a/regression/ansi-c/const1/const-array.desc
+++ b/regression/ansi-c/const1/const-array.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 const-array.c
  ^.*: .* is constant$
 ^   array\[1\] = 2;$
diff --git a/regression/ansi-c/const1/const-member.desc b/regression/ansi-c/const1/const-member.desc
index 7f3877192c0..729a68fdf30 100644
--- a/regression/ansi-c/const1/const-member.desc
+++ b/regression/ansi-c/const1/const-member.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 const-member.c
 
 ^.*: .* is constant$
diff --git a/regression/ansi-c/cprover_bool1/test.desc b/regression/ansi-c/cprover_bool1/test.desc
index 466da18b2b5..fc2b1874059 100644
--- a/regression/ansi-c/cprover_bool1/test.desc
+++ b/regression/ansi-c/cprover_bool1/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=0$