From e32ccf62c45c6d5890d9ab8dc7aef33199740565 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 25 Dec 2018 10:44:16 +0000
Subject: [PATCH 1/2] Make Powershell stop on errors

We had failing regression tests, but this went unnoticed because the goto-cl
regression tests were successful (which were the last common run in the cmdlet).
---
 buildspec-windows.yml | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/buildspec-windows.yml b/buildspec-windows.yml
index 47b011814a8..60e93b5eb48 100644
--- a/buildspec-windows.yml
+++ b/buildspec-windows.yml
@@ -64,6 +64,9 @@ 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 = "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/goto-cl test BUILD_ENV=MSVC" '
 
       - |

From 3ef168ac87c665e8b59d8e1a145a5fe32877f12f Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Sat, 29 Dec 2018 21:10:38 +0000
Subject: [PATCH 2/2] Do not use global variable that requires an initializer
 function

In particular don't use one that depends on other globals to be initialized
first.
---
 .../anonymous-java.lang.thread/test.desc          |  2 +-
 .../anonymous-java.lang.thread/test2.desc         |  2 +-
 .../explicit-thread-blocks/test.desc              |  2 +-
 .../explicit-thread-blocks/test2.desc             |  2 +-
 .../jbmc-concurrency/get-current-thread/test.desc |  2 +-
 .../get-current-thread/test4.desc                 |  2 +-
 .../get-current-thread/test5.desc                 |  2 +-
 .../get-current-thread/test6.desc                 |  2 +-
 .../jbmc-concurrency/java-lang-runnable/test.desc |  2 +-
 .../java-lang-runnable/test2.desc                 |  2 +-
 .../java-lang-runnable/test3.desc                 |  2 +-
 .../java-lang-runnable/test4.desc                 |  2 +-
 .../jbmc-concurrency/java-lang-thread/test.desc   |  2 +-
 .../jbmc-concurrency/java-lang-thread/test2.desc  |  2 +-
 .../jbmc-concurrency/java-lang-thread/test3.desc  |  2 +-
 .../jbmc-concurrency/java-lang-thread/test4.desc  |  2 +-
 .../jbmc-concurrency/several-threads/test.desc    |  2 +-
 .../jbmc-concurrency/several-threads/test2.desc   |  2 +-
 .../jbmc-concurrency/several-threads/test3.desc   |  2 +-
 .../synchronized-blocks/test1.desc                |  2 +-
 .../synchronized-blocks/test2.desc                |  2 +-
 .../synchronized-blocks/test3.desc                |  2 +-
 .../synchronized-blocks/test_sync.desc            |  2 +-
 .../synchronized-blocks/test_sync_baseline.desc   |  2 +-
 .../synchronized-method-illegal-state/test.desc   |  2 +-
 .../synchronized-methods/test1.desc               |  2 +-
 .../synchronized-methods/test2.desc               |  2 +-
 .../synchronized-methods/test3.desc               |  2 +-
 .../synchronized-methods/test_sync.desc           |  2 +-
 .../synchronized-methods/test_sync_baseline.desc  |  2 +-
 .../jbmc-concurrency/synchronized/test.desc       |  2 +-
 jbmc/regression/jbmc/static_init1/test1.desc      |  2 +-
 jbmc/regression/jbmc/static_init2/test1.desc      |  2 +-
 jbmc/regression/jbmc/static_init_order/test3.desc |  2 +-
 jbmc/regression/jbmc/static_init_order/test4.desc |  2 +-
 .../java_bytecode/java_static_initializers.cpp    | 15 +++++++++------
 36 files changed, 44 insertions(+), 41 deletions(-)

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 e86695bcf0b..386cc37503d 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 @@
-KNOWNBUG
+CORE
 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 7abf671b92b..c39ba088b5b 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 @@
-KNOWNBUG
+CORE
 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 1504fb15b63..01ab8385b37 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 @@
-KNOWNBUG
+CORE
 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 9f780aeaeef..545f4effa2b 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 @@
-KNOWNBUG
+CORE
 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 6b44afcffc3..124afa21ae7 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 @@
-KNOWNBUG
+CORE
 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 53ae3cb75c0..8ceb063f4f9 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 @@
-KNOWNBUG
+CORE
 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 2d6eb10ff2c..6522d6f95a2 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 @@
-KNOWNBUG
+CORE
 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 e149d7dbbd5..6bb22f0f8f9 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 @@
-KNOWNBUG
+CORE
 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 f8497452001..60b60587f48 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 @@
-KNOWNBUG
+CORE
 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 c55453ab122..02c95662b4b 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 @@
-KNOWNBUG
+CORE
 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 91e86c91d8d..3b9c0e1421f 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 @@
-KNOWNBUG
+CORE
 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 696f4caa341..eb5d686f26a 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 @@
-KNOWNBUG
+CORE
 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 1e700fbb638..8eec4067339 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 @@
-KNOWNBUG
+CORE
 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 19d8e21c2a9..dbde3635d9f 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 @@
-KNOWNBUG
+CORE
 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 ddecee43b79..a4e55bfa5ec 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 @@
-KNOWNBUG
+CORE
 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 31524f4d506..0fc102be1da 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 @@
-KNOWNBUG
+CORE
 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 598a2270e9b..cfd4860376d 100644
--- a/jbmc/regression/jbmc-concurrency/several-threads/test.desc
+++ b/jbmc/regression/jbmc-concurrency/several-threads/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 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 60027b5eea0..acfc61c48c6 100644
--- a/jbmc/regression/jbmc-concurrency/several-threads/test2.desc
+++ b/jbmc/regression/jbmc-concurrency/several-threads/test2.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 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 76c507cb2c1..cbcd840a1e0 100644
--- a/jbmc/regression/jbmc-concurrency/several-threads/test3.desc
+++ b/jbmc/regression/jbmc-concurrency/several-threads/test3.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 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 7ab4ac1be3a..f284db38cf3 100644
--- a/jbmc/regression/jbmc-concurrency/synchronized-blocks/test1.desc
+++ b/jbmc/regression/jbmc-concurrency/synchronized-blocks/test1.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 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 3ad43306642..ec805ab619a 100644
--- a/jbmc/regression/jbmc-concurrency/synchronized-blocks/test2.desc
+++ b/jbmc/regression/jbmc-concurrency/synchronized-blocks/test2.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 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 3ad43306642..ec805ab619a 100644
--- a/jbmc/regression/jbmc-concurrency/synchronized-blocks/test3.desc
+++ b/jbmc/regression/jbmc-concurrency/synchronized-blocks/test3.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 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 61916f0b547..824bc5b0d11 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 @@
-KNOWNBUG
+CORE
 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 3533c599649..550429547e4 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 @@
-KNOWNBUG
+CORE
 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 64df33e2853..22eaef591e3 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 @@
-KNOWNBUG
+CORE
 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 03f933e43c4..32be2704a71 100644
--- a/jbmc/regression/jbmc-concurrency/synchronized-methods/test1.desc
+++ b/jbmc/regression/jbmc-concurrency/synchronized-methods/test1.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 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 2bb231e01b4..4420b0af9f2 100644
--- a/jbmc/regression/jbmc-concurrency/synchronized-methods/test2.desc
+++ b/jbmc/regression/jbmc-concurrency/synchronized-methods/test2.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 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 5a3b0ef3046..e79944afd03 100644
--- a/jbmc/regression/jbmc-concurrency/synchronized-methods/test3.desc
+++ b/jbmc/regression/jbmc-concurrency/synchronized-methods/test3.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 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 7e2cdeaec5b..3d6edf4b922 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 @@
-KNOWNBUG
+CORE
 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 61916f0b547..824bc5b0d11 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 @@
-KNOWNBUG
+CORE
 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 b0d5612e028..5921af6c569 100644
--- a/jbmc/regression/jbmc-concurrency/synchronized/test.desc
+++ b/jbmc/regression/jbmc-concurrency/synchronized/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 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 75eb56c36f3..8bc396cff4d 100644
--- a/jbmc/regression/jbmc/static_init1/test1.desc
+++ b/jbmc/regression/jbmc/static_init1/test1.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 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 75eb56c36f3..8bc396cff4d 100644
--- a/jbmc/regression/jbmc/static_init2/test1.desc
+++ b/jbmc/regression/jbmc/static_init2/test1.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 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 250f1882331..6ec4686fa57 100644
--- a/jbmc/regression/jbmc/static_init_order/test3.desc
+++ b/jbmc/regression/jbmc/static_init_order/test3.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 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 dd7464b0d74..d008222606e 100644
--- a/jbmc/regression/jbmc/static_init_order/test4.desc
+++ b/jbmc/regression/jbmc/static_init_order/test4.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 static_init_order.class
 --function static_init_order.test2 --java-threading
 ^EXIT=10$
diff --git a/jbmc/src/java_bytecode/java_static_initializers.cpp b/jbmc/src/java_bytecode/java_static_initializers.cpp
index d39905a1190..80e230afb65 100644
--- a/jbmc/src/java_bytecode/java_static_initializers.cpp
+++ b/jbmc/src/java_bytecode/java_static_initializers.cpp
@@ -44,7 +44,10 @@ enum class clinit_statest
   INIT_COMPLETE
 };
 
-const typet clinit_states_type = java_byte_type();
+static typet clinit_states_type()
+{
+  return java_byte_type();
+}
 
 // Disable linter here to allow a std::string constant, since that holds
 // a length, whereas a cstr would require strlen every time.
@@ -158,7 +161,7 @@ static code_assignt
 gen_clinit_assign(const exprt &expr, const clinit_statest state)
 {
   mp_integer initv(static_cast<int>(state));
-  constant_exprt init_s = from_integer(initv, clinit_states_type);
+  constant_exprt init_s = from_integer(initv, clinit_states_type());
   return code_assignt(expr, init_s);
 }
 
@@ -174,7 +177,7 @@ static equal_exprt
 gen_clinit_eqexpr(const exprt &expr, const clinit_statest state)
 {
   mp_integer initv(static_cast<int>(state));
-  constant_exprt init_s = from_integer(initv, clinit_states_type);
+  constant_exprt init_s = from_integer(initv, clinit_states_type());
   return equal_exprt(expr, init_s);
 }
 
@@ -312,7 +315,7 @@ static void create_clinit_wrapper_symbols(
   if(thread_safe)
   {
     exprt not_init_value = from_integer(
-      static_cast<int>(clinit_statest::NOT_INIT), clinit_states_type);
+      static_cast<int>(clinit_statest::NOT_INIT), clinit_states_type());
 
     // Create two global static synthetic "fields" for the class "id"
     // these two variables hold the state of the class initialization algorithm
@@ -320,7 +323,7 @@ static void create_clinit_wrapper_symbols(
     add_new_variable_symbol(
       symbol_table,
       clinit_state_var_name(class_name),
-      clinit_states_type,
+      clinit_states_type(),
       not_init_value,
       false,
       true);
@@ -328,7 +331,7 @@ static void create_clinit_wrapper_symbols(
     add_new_variable_symbol(
       symbol_table,
       clinit_thread_local_state_var_name(class_name),
-      clinit_states_type,
+      clinit_states_type(),
       not_init_value,
       true,
       true);