diff --git a/jbmc/regression/jbmc-strings/CMakeLists.txt b/jbmc/regression/jbmc-strings/CMakeLists.txt
index 2bc768b244b..168760e47b0 100644
--- a/jbmc/regression/jbmc-strings/CMakeLists.txt
+++ b/jbmc/regression/jbmc-strings/CMakeLists.txt
@@ -1,20 +1,10 @@
-if("${CMAKE_SYSTEM_NAME}" STREQUAL "Windows")
-  set(exclude_win_broken_tests -X winbug)
-else()
-  set(exclude_win_broken_tests "")
-endif()
-
 add_test_pl_tests(
-    "$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation" ${exclude_win_broken_tests}
+    "$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation"
 )
 
-if("${CMAKE_SYSTEM_NAME}" STREQUAL "Windows")
-  message(WARNING "skipping broken jbmc-strings/ tests on windows")
-else()
-  add_test_pl_profile(
-    "jbmc-strings-symex-driven-lazy-loading"
-    "$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading"
-    "-C;-X;symex-driven-lazy-loading-expected-failure;-s;symex-driven-loading"
-    "CORE"
-    )
-endif()
+add_test_pl_profile(
+  "jbmc-strings-symex-driven-lazy-loading"
+  "$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation --symex-driven-lazy-loading"
+  "-C;-X;symex-driven-lazy-loading-expected-failure;-s;symex-driven-loading"
+  "CORE"
+  )
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationCompareTo/test_fail1.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationCompareTo/test_fail1.desc
index c35aabde300..9355155a0cc 100644
--- a/jbmc/regression/jbmc-strings/ConstantEvaluationCompareTo/test_fail1.desc
+++ b/jbmc/regression/jbmc-strings/ConstantEvaluationCompareTo/test_fail1.desc
@@ -1,6 +1,6 @@
-CORE winbug
+CORE
 Main
---function Main.constantCompareToFail1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.constantCompareToFail1:()V.assertion.1"
+--function Main.constantCompareToFail1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Main.constantCompareToFail1:()V.assertion.1'
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationCompareTo/test_fail1_vcc.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationCompareTo/test_fail1_vcc.desc
index c4a9153a0d3..ba45cc280ee 100644
--- a/jbmc/regression/jbmc-strings/ConstantEvaluationCompareTo/test_fail1_vcc.desc
+++ b/jbmc/regression/jbmc-strings/ConstantEvaluationCompareTo/test_fail1_vcc.desc
@@ -1,6 +1,6 @@
-CORE winbug
+CORE
 Main
---function Main.constantCompareToFail1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.constantCompareToFail1:()V.assertion.1" --show-vcc
+--function Main.constantCompareToFail1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Main.constantCompareToFail1:()V.assertion.1' --show-vcc
 ^EXIT=0$
 ^SIGNAL=0$
 \{1\} false
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationCompareTo/test_fail2.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationCompareTo/test_fail2.desc
index e11bc92c7a5..c05fbaa1233 100644
--- a/jbmc/regression/jbmc-strings/ConstantEvaluationCompareTo/test_fail2.desc
+++ b/jbmc/regression/jbmc-strings/ConstantEvaluationCompareTo/test_fail2.desc
@@ -1,6 +1,6 @@
-CORE winbug
+CORE
 Main
---function Main.constantCompareToFail2 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.constantCompareToFail2:()V.assertion.1"
+--function Main.constantCompareToFail2 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Main.constantCompareToFail2:()V.assertion.1'
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationCompareTo/test_fail2_vcc.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationCompareTo/test_fail2_vcc.desc
index 468dad5ed32..8ec6f6ab55e 100644
--- a/jbmc/regression/jbmc-strings/ConstantEvaluationCompareTo/test_fail2_vcc.desc
+++ b/jbmc/regression/jbmc-strings/ConstantEvaluationCompareTo/test_fail2_vcc.desc
@@ -1,6 +1,6 @@
-CORE winbug
+CORE
 Main
---function Main.constantCompareToFail2 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.constantCompareToFail2:()V.assertion.1" --show-vcc
+--function Main.constantCompareToFail2 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Main.constantCompareToFail2:()V.assertion.1' --show-vcc
 ^EXIT=0$
 ^SIGNAL=0$
 \{1\} false
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationCompareTo/test_fail3.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationCompareTo/test_fail3.desc
index de1c53a9659..0dcf8740a94 100644
--- a/jbmc/regression/jbmc-strings/ConstantEvaluationCompareTo/test_fail3.desc
+++ b/jbmc/regression/jbmc-strings/ConstantEvaluationCompareTo/test_fail3.desc
@@ -1,6 +1,6 @@
-CORE winbug
+CORE
 Main
---function Main.constantCompareToFail3 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.constantCompareToFail3:()V.assertion.1"
+--function Main.constantCompareToFail3 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Main.constantCompareToFail3:()V.assertion.1'
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationCompareTo/test_fail3_vcc.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationCompareTo/test_fail3_vcc.desc
index fa1667802ae..383f4e4d6ba 100644
--- a/jbmc/regression/jbmc-strings/ConstantEvaluationCompareTo/test_fail3_vcc.desc
+++ b/jbmc/regression/jbmc-strings/ConstantEvaluationCompareTo/test_fail3_vcc.desc
@@ -1,6 +1,6 @@
-CORE winbug
+CORE
 Main
---function Main.constantCompareToFail3 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.constantCompareToFail3:()V.assertion.1" --show-vcc
+--function Main.constantCompareToFail3 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Main.constantCompareToFail3:()V.assertion.1' --show-vcc
 ^EXIT=0$
 ^SIGNAL=0$
 \{1\} false
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationCompareTo/test_fail4.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationCompareTo/test_fail4.desc
index 96daf68e7d3..51c651658cd 100644
--- a/jbmc/regression/jbmc-strings/ConstantEvaluationCompareTo/test_fail4.desc
+++ b/jbmc/regression/jbmc-strings/ConstantEvaluationCompareTo/test_fail4.desc
@@ -1,6 +1,6 @@
-CORE winbug
+CORE
 Main
---function Main.constantCompareToFail4 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.constantCompareToFail4:()V.assertion.1"
+--function Main.constantCompareToFail4 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Main.constantCompareToFail4:()V.assertion.1'
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationCompareTo/test_fail4_vcc.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationCompareTo/test_fail4_vcc.desc
index 60915b11165..7e507e30103 100644
--- a/jbmc/regression/jbmc-strings/ConstantEvaluationCompareTo/test_fail4_vcc.desc
+++ b/jbmc/regression/jbmc-strings/ConstantEvaluationCompareTo/test_fail4_vcc.desc
@@ -1,6 +1,6 @@
-CORE winbug
+CORE
 Main
---function Main.constantCompareToFail4 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.constantCompareToFail4:()V.assertion.1" --show-vcc
+--function Main.constantCompareToFail4 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Main.constantCompareToFail4:()V.assertion.1' --show-vcc
 ^EXIT=0$
 ^SIGNAL=0$
 \{1\} false
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationEndsWith/test_fail.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationEndsWith/test_fail.desc
index af5e14cb3f1..8e4192c9522 100644
--- a/jbmc/regression/jbmc-strings/ConstantEvaluationEndsWith/test_fail.desc
+++ b/jbmc/regression/jbmc-strings/ConstantEvaluationEndsWith/test_fail.desc
@@ -1,6 +1,6 @@
-CORE winbug
+CORE
 Main
---function Main.constantEndsWithFail --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.constantEndsWithFail:()V.assertion.1" 
+--function Main.constantEndsWithFail --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Main.constantEndsWithFail:()V.assertion.1' 
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationEndsWith/test_fail_vcc.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationEndsWith/test_fail_vcc.desc
index 8b3c69783dc..5307b3e87d1 100644
--- a/jbmc/regression/jbmc-strings/ConstantEvaluationEndsWith/test_fail_vcc.desc
+++ b/jbmc/regression/jbmc-strings/ConstantEvaluationEndsWith/test_fail_vcc.desc
@@ -1,6 +1,6 @@
-CORE winbug
+CORE
 Main
---function Main.constantEndsWithFail --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.constantEndsWithFail:()V.assertion.1" --show-vcc
+--function Main.constantEndsWithFail --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Main.constantEndsWithFail:()V.assertion.1' --show-vcc
 ^EXIT=0$
 ^SIGNAL=0$
 \{1\} false
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationEndsWith/test_pass.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationEndsWith/test_pass.desc
index 33cb714ced9..6985cbd8abb 100644
--- a/jbmc/regression/jbmc-strings/ConstantEvaluationEndsWith/test_pass.desc
+++ b/jbmc/regression/jbmc-strings/ConstantEvaluationEndsWith/test_pass.desc
@@ -1,6 +1,6 @@
-CORE winbug
+CORE
 Main
---function Main.constantEndsWithPass --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.constantEndsWithPass:()V.assertion.1"
+--function Main.constantEndsWithPass --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Main.constantEndsWithPass:()V.assertion.1'
 ^Generated [0-9]+ VCC\(s\), 0 remaining after simplification
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationIsEmpty/test_fail.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationIsEmpty/test_fail.desc
index b0331f03ce6..9eb9860688f 100644
--- a/jbmc/regression/jbmc-strings/ConstantEvaluationIsEmpty/test_fail.desc
+++ b/jbmc/regression/jbmc-strings/ConstantEvaluationIsEmpty/test_fail.desc
@@ -1,6 +1,6 @@
-CORE winbug
+CORE
 Main
---function Main.constantIsEmptyFail --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.constantIsEmptyFail:()V.assertion.1"
+--function Main.constantIsEmptyFail --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Main.constantIsEmptyFail:()V.assertion.1'
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationIsEmpty/test_fail_vcc.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationIsEmpty/test_fail_vcc.desc
index e37ffce28b8..c2f4f8e84a9 100644
--- a/jbmc/regression/jbmc-strings/ConstantEvaluationIsEmpty/test_fail_vcc.desc
+++ b/jbmc/regression/jbmc-strings/ConstantEvaluationIsEmpty/test_fail_vcc.desc
@@ -1,6 +1,6 @@
-CORE winbug
+CORE
 Main
---function Main.constantIsEmptyFail --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --show-vcc --property "java::Main.constantIsEmptyFail:()V.assertion.1" 
+--function Main.constantIsEmptyFail --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --show-vcc --property 'java::Main.constantIsEmptyFail:()V.assertion.1' 
 ^EXIT=0$
 ^SIGNAL=0$
 \{1\} false
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationIsEmpty/test_pass.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationIsEmpty/test_pass.desc
index 9ade987366e..a4cf753a114 100644
--- a/jbmc/regression/jbmc-strings/ConstantEvaluationIsEmpty/test_pass.desc
+++ b/jbmc/regression/jbmc-strings/ConstantEvaluationIsEmpty/test_pass.desc
@@ -1,6 +1,6 @@
-CORE winbug
+CORE
 Main
---function Main.constantIsEmptyPass --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.constantIsEmptyPass:()V.assertion.1"
+--function Main.constantIsEmptyPass --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Main.constantIsEmptyPass:()V.assertion.1'
 ^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend01/test.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend01/test.desc
index a43d09a59f1..01007a36c93 100644
--- a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend01/test.desc
+++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend01/test.desc
@@ -1,6 +1,6 @@
-CORE winbug
+CORE
 Main
---function Main.test --property "java::Main.test:()V.assertion.1" --property "java::Main.test:()V.assertion.2"
+--function Main.test --property 'java::Main.test:()V.assertion.1' --property 'java::Main.test:()V.assertion.2'
 ^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend02-WithEmptyString/test1.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend02-WithEmptyString/test1.desc
index a9ce13ef87f..546b3bf2656 100644
--- a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend02-WithEmptyString/test1.desc
+++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend02-WithEmptyString/test1.desc
@@ -1,6 +1,6 @@
-CORE winbug
+CORE
 Main
---function Main.test1 --property "java::Main.test1:()V.assertion.1" --property "java::Main.test1:()V.assertion.2"
+--function Main.test1 --property 'java::Main.test1:()V.assertion.1' --property 'java::Main.test1:()V.assertion.2'
 ^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend02-WithEmptyString/test2.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend02-WithEmptyString/test2.desc
index f250391b547..fec26a11e0a 100644
--- a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend02-WithEmptyString/test2.desc
+++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend02-WithEmptyString/test2.desc
@@ -1,6 +1,6 @@
-CORE winbug
+CORE
 Main
---function Main.test2 --property "java::Main.test2:()V.assertion.1" --property "java::Main.test2:()V.assertion.2"
+--function Main.test2 --property 'java::Main.test2:()V.assertion.1' --property 'java::Main.test2:()V.assertion.2'
 ^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend02-WithEmptyString/test3.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend02-WithEmptyString/test3.desc
index 46f38f5db66..774565b92c3 100644
--- a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend02-WithEmptyString/test3.desc
+++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend02-WithEmptyString/test3.desc
@@ -1,6 +1,6 @@
-CORE winbug
+CORE
 Main
---function Main.test3 --property "java::Main.test3:()V.assertion.1" --property "java::Main.test3:()V.assertion.2"
+--function Main.test3 --property 'java::Main.test3:()V.assertion.1' --property 'java::Main.test3:()V.assertion.2'
 ^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation01/test.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation01/test.desc
index a43d09a59f1..01007a36c93 100644
--- a/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation01/test.desc
+++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation01/test.desc
@@ -1,6 +1,6 @@
-CORE winbug
+CORE
 Main
---function Main.test --property "java::Main.test:()V.assertion.1" --property "java::Main.test:()V.assertion.2"
+--function Main.test --property 'java::Main.test:()V.assertion.1' --property 'java::Main.test:()V.assertion.2'
 ^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation02-WithEmptyString/test1.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation02-WithEmptyString/test1.desc
index a9ce13ef87f..546b3bf2656 100644
--- a/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation02-WithEmptyString/test1.desc
+++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation02-WithEmptyString/test1.desc
@@ -1,6 +1,6 @@
-CORE winbug
+CORE
 Main
---function Main.test1 --property "java::Main.test1:()V.assertion.1" --property "java::Main.test1:()V.assertion.2"
+--function Main.test1 --property 'java::Main.test1:()V.assertion.1' --property 'java::Main.test1:()V.assertion.2'
 ^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation02-WithEmptyString/test2.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation02-WithEmptyString/test2.desc
index f250391b547..fec26a11e0a 100644
--- a/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation02-WithEmptyString/test2.desc
+++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation02-WithEmptyString/test2.desc
@@ -1,6 +1,6 @@
-CORE winbug
+CORE
 Main
---function Main.test2 --property "java::Main.test2:()V.assertion.1" --property "java::Main.test2:()V.assertion.2"
+--function Main.test2 --property 'java::Main.test2:()V.assertion.1' --property 'java::Main.test2:()V.assertion.2'
 ^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation02-WithEmptyString/test3.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation02-WithEmptyString/test3.desc
index 46f38f5db66..774565b92c3 100644
--- a/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation02-WithEmptyString/test3.desc
+++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation02-WithEmptyString/test3.desc
@@ -1,6 +1,6 @@
-CORE winbug
+CORE
 Main
---function Main.test3 --property "java::Main.test3:()V.assertion.1" --property "java::Main.test3:()V.assertion.2"
+--function Main.test3 --property 'java::Main.test3:()V.assertion.1' --property 'java::Main.test3:()V.assertion.2'
 ^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation03-NegativeScenarios/test1.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation03-NegativeScenarios/test1.desc
index bc19c75ef87..055316e2df8 100644
--- a/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation03-NegativeScenarios/test1.desc
+++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation03-NegativeScenarios/test1.desc
@@ -1,6 +1,6 @@
-CORE symex-driven-lazy-loading-expected-failure winbug
+CORE symex-driven-lazy-loading-expected-failure
 Main
---function Main.test1 --property "java::Main.test1:(Ljava/lang/String;)V.assertion.1"
+--function Main.test1 --property 'java::Main.test1:(Ljava/lang/String;)V.assertion.1'
 ^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$
 ^EXIT=10$
 ^SIGNAL=0$
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation03-NegativeScenarios/test2.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation03-NegativeScenarios/test2.desc
index 2cb284faaae..d458bcd1552 100644
--- a/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation03-NegativeScenarios/test2.desc
+++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation03-NegativeScenarios/test2.desc
@@ -1,6 +1,6 @@
-CORE symex-driven-lazy-loading-expected-failure winbug
+CORE symex-driven-lazy-loading-expected-failure
 Main
---function Main.test2 --property "java::Main.test2:(Ljava/lang/String;)V.assertion.1"
+--function Main.test2 --property 'java::Main.test2:(Ljava/lang/String;)V.assertion.1'
 ^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$
 ^EXIT=10$
 ^SIGNAL=0$
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation03-NegativeScenarios/test3.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation03-NegativeScenarios/test3.desc
index ac082b366b8..9185969f2a1 100644
--- a/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation03-NegativeScenarios/test3.desc
+++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation03-NegativeScenarios/test3.desc
@@ -1,6 +1,6 @@
-CORE symex-driven-lazy-loading-expected-failure winbug
+CORE symex-driven-lazy-loading-expected-failure
 Main
---function Main.test3 --property "java::Main.test3:(Ljava/lang/String;)V.assertion.1"
+--function Main.test3 --property 'java::Main.test3:(Ljava/lang/String;)V.assertion.1'
 ^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$
 ^EXIT=10$
 ^SIGNAL=0$
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation04-StringEqual/test.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation04-StringEqual/test.desc
index 66beed79ac7..c35473b5555 100644
--- a/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation04-StringEqual/test.desc
+++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation04-StringEqual/test.desc
@@ -1,6 +1,6 @@
-CORE winbug
+CORE
 Main
---function Main.test --property "java::Main.test:()V.assertion.1" --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+--function Main.test --property 'java::Main.test:()V.assertion.1' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation06-2byteChar/test.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation06-2byteChar/test.desc
index a43d09a59f1..01007a36c93 100644
--- a/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation06-2byteChar/test.desc
+++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation06-2byteChar/test.desc
@@ -1,6 +1,6 @@
-CORE winbug
+CORE
 Main
---function Main.test --property "java::Main.test:()V.assertion.1" --property "java::Main.test:()V.assertion.2"
+--function Main.test --property 'java::Main.test:()V.assertion.1' --property 'java::Main.test:()V.assertion.2'
 ^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation07-NonPrintableChar/test.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation07-NonPrintableChar/test.desc
index a43d09a59f1..01007a36c93 100644
--- a/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation07-NonPrintableChar/test.desc
+++ b/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation07-NonPrintableChar/test.desc
@@ -1,6 +1,6 @@
-CORE winbug
+CORE
 Main
---function Main.test --property "java::Main.test:()V.assertion.1" --property "java::Main.test:()V.assertion.2"
+--function Main.test --property 'java::Main.test:()V.assertion.1' --property 'java::Main.test:()V.assertion.2'
 ^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation03-IndexOutOfRange/test.desc b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation03-IndexOutOfRange/test.desc
index 3e0f03f7d9f..79420aaac53 100644
--- a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation03-IndexOutOfRange/test.desc
+++ b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation03-IndexOutOfRange/test.desc
@@ -1,6 +1,6 @@
-CORE symex-driven-lazy-loading-expected-failure winbug
+CORE symex-driven-lazy-loading-expected-failure
 Main
---function Main.constantIndexOf --property "java::Main.constantIndexOf:(Ljava/lang/String;)V.assertion.1"
+--function Main.constantIndexOf --property 'java::Main.constantIndexOf:(Ljava/lang/String;)V.assertion.1'
 ^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test1.desc b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test1.desc
index 22f15f8650c..95ab592d88d 100644
--- a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test1.desc
+++ b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test1.desc
@@ -1,6 +1,6 @@
-CORE symex-driven-lazy-loading-expected-failure winbug
+CORE symex-driven-lazy-loading-expected-failure
 Main
---function Main.constantIndexOf --property "java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.1" --show-vcc
+--function Main.constantIndexOf --property 'java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.1' --show-vcc
 ^Generated 1 VCC\(s\), 1 remaining after simplification$
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test10.desc b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test10.desc
index 63a710af036..22f9e1a6b79 100644
--- a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test10.desc
+++ b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test10.desc
@@ -1,6 +1,6 @@
-CORE symex-driven-lazy-loading-expected-failure winbug
+CORE symex-driven-lazy-loading-expected-failure
 Main
---function Main.constantIndexOf --property "java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.10" --show-vcc
+--function Main.constantIndexOf --property 'java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.10' --show-vcc
 ^Generated 1 VCC\(s\), 1 remaining after simplification$
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test11.desc b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test11.desc
index e9d30eb7cee..9cbeaa679a9 100644
--- a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test11.desc
+++ b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test11.desc
@@ -1,6 +1,6 @@
-CORE symex-driven-lazy-loading-expected-failure winbug
+CORE symex-driven-lazy-loading-expected-failure
 Main
---function Main.constantIndexOf --property "java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.11" --show-vcc
+--function Main.constantIndexOf --property 'java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.11' --show-vcc
 ^Generated 1 VCC\(s\), 1 remaining after simplification$
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test12.desc b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test12.desc
index 22f2d76fae6..e169354a37c 100644
--- a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test12.desc
+++ b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test12.desc
@@ -1,6 +1,6 @@
-CORE symex-driven-lazy-loading-expected-failure winbug
+CORE symex-driven-lazy-loading-expected-failure
 Main
---function Main.constantIndexOf --property "java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.12" --show-vcc
+--function Main.constantIndexOf --property 'java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.12' --show-vcc
 ^Generated 1 VCC\(s\), 1 remaining after simplification$
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test2.desc b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test2.desc
index 86af87adcb5..8542527bfd3 100644
--- a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test2.desc
+++ b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test2.desc
@@ -1,6 +1,6 @@
-CORE symex-driven-lazy-loading-expected-failure winbug
+CORE symex-driven-lazy-loading-expected-failure
 Main
---function Main.constantIndexOf --property "java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.2" --show-vcc
+--function Main.constantIndexOf --property 'java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.2' --show-vcc
 ^Generated 1 VCC\(s\), 1 remaining after simplification$
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test3.desc b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test3.desc
index 29f7cdd39c7..8abaa890e14 100644
--- a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test3.desc
+++ b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test3.desc
@@ -1,6 +1,6 @@
-CORE symex-driven-lazy-loading-expected-failure winbug
+CORE symex-driven-lazy-loading-expected-failure
 Main
---function Main.constantIndexOf --property "java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.3" --show-vcc
+--function Main.constantIndexOf --property 'java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.3' --show-vcc
 ^Generated 1 VCC\(s\), 1 remaining after simplification$
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test4.desc b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test4.desc
index 02a1d161ace..e779b30406c 100644
--- a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test4.desc
+++ b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test4.desc
@@ -1,6 +1,6 @@
-CORE symex-driven-lazy-loading-expected-failure winbug
+CORE symex-driven-lazy-loading-expected-failure
 Main
---function Main.constantIndexOf --property "java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.4" --show-vcc
+--function Main.constantIndexOf --property 'java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.4' --show-vcc
 ^Generated 1 VCC\(s\), 1 remaining after simplification$
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test5.desc b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test5.desc
index b686c269cff..5995476cfed 100644
--- a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test5.desc
+++ b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test5.desc
@@ -1,6 +1,6 @@
-CORE symex-driven-lazy-loading-expected-failure winbug
+CORE symex-driven-lazy-loading-expected-failure
 Main
---function Main.constantIndexOf --property "java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.5" --show-vcc
+--function Main.constantIndexOf --property 'java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.5' --show-vcc
 ^Generated 1 VCC\(s\), 1 remaining after simplification$
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test6.desc b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test6.desc
index 38b7532f454..2e303020704 100644
--- a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test6.desc
+++ b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test6.desc
@@ -1,6 +1,6 @@
-CORE symex-driven-lazy-loading-expected-failure winbug
+CORE symex-driven-lazy-loading-expected-failure
 Main
---function Main.constantIndexOf --property "java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.6" --show-vcc
+--function Main.constantIndexOf --property 'java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.6' --show-vcc
 ^Generated 1 VCC\(s\), 1 remaining after simplification$
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test7.desc b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test7.desc
index e32f52f6d39..e8568ef006c 100644
--- a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test7.desc
+++ b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test7.desc
@@ -1,6 +1,6 @@
-CORE symex-driven-lazy-loading-expected-failure winbug
+CORE symex-driven-lazy-loading-expected-failure
 Main
---function Main.constantIndexOf --property "java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.7" --show-vcc
+--function Main.constantIndexOf --property 'java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.7' --show-vcc
 ^Generated 1 VCC\(s\), 1 remaining after simplification$
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test8.desc b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test8.desc
index f2a84eb59aa..8efb0716245 100644
--- a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test8.desc
+++ b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test8.desc
@@ -1,6 +1,6 @@
-CORE symex-driven-lazy-loading-expected-failure winbug
+CORE symex-driven-lazy-loading-expected-failure
 Main
---function Main.constantIndexOf --property "java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.8" --show-vcc
+--function Main.constantIndexOf --property 'java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.8' --show-vcc
 ^Generated 1 VCC\(s\), 1 remaining after simplification$
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test9.desc b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test9.desc
index 1dfc0f5ee0c..893822c9ffc 100644
--- a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test9.desc
+++ b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test9.desc
@@ -1,6 +1,6 @@
-CORE symex-driven-lazy-loading-expected-failure winbug
+CORE symex-driven-lazy-loading-expected-failure
 Main
---function Main.constantIndexOf --property "java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.9" --show-vcc
+--function Main.constantIndexOf --property 'java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.9' --show-vcc
 ^Generated 1 VCC\(s\), 1 remaining after simplification$
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation06-AssertionFailure/test.desc b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation06-AssertionFailure/test.desc
index e3eeb3fe1af..ea0f395abef 100644
--- a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation06-AssertionFailure/test.desc
+++ b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation06-AssertionFailure/test.desc
@@ -1,6 +1,6 @@
-CORE symex-driven-lazy-loading-expected-failure winbug
+CORE symex-driven-lazy-loading-expected-failure
 Main
---function Main.constantIndexOf --property "java::Main.constantIndexOf:()V.assertion.1"
+--function Main.constantIndexOf --property 'java::Main.constantIndexOf:()V.assertion.1'
 ^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$
 ^VERIFICATION FAILED$
 ^EXIT=10$
diff --git a/jbmc/regression/jbmc-strings/RegionMatches/test1.desc b/jbmc/regression/jbmc-strings/RegionMatches/test1.desc
index 7b1ea89d38b..a3252a3f6ea 100644
--- a/jbmc/regression/jbmc-strings/RegionMatches/test1.desc
+++ b/jbmc/regression/jbmc-strings/RegionMatches/test1.desc
@@ -1,6 +1,6 @@
 FUTURE
 RegionMatches
---max-nondet-string-length 1000 --function RegionMatches.constant --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::RegionMatches.constant:(I)V.assertion.1"
+--max-nondet-string-length 1000 --function RegionMatches.constant --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::RegionMatches.constant:(I)V.assertion.1'
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/jbmc-strings/RegionMatches/test2.desc b/jbmc/regression/jbmc-strings/RegionMatches/test2.desc
index 72731520e6e..d5d5c64eb05 100644
--- a/jbmc/regression/jbmc-strings/RegionMatches/test2.desc
+++ b/jbmc/regression/jbmc-strings/RegionMatches/test2.desc
@@ -1,6 +1,6 @@
 FUTURE
 RegionMatches
---max-nondet-string-length 1000 --function RegionMatches.constant --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::RegionMatches.constant:(I)V.assertion.2"
+--max-nondet-string-length 1000 --function RegionMatches.constant --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::RegionMatches.constant:(I)V.assertion.2'
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/jbmc/regression/jbmc-strings/RegionMatches/test3.desc b/jbmc/regression/jbmc-strings/RegionMatches/test3.desc
index 7823ba3c95b..3996a82579f 100644
--- a/jbmc/regression/jbmc-strings/RegionMatches/test3.desc
+++ b/jbmc/regression/jbmc-strings/RegionMatches/test3.desc
@@ -1,6 +1,6 @@
 FUTURE
 RegionMatches
---max-nondet-string-length 1000 --function RegionMatches.constant --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::RegionMatches.constant:(I)V.assertion.3"
+--max-nondet-string-length 1000 --function RegionMatches.constant --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::RegionMatches.constant:(I)V.assertion.3'
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/jbmc-strings/RegionMatches/test4.desc b/jbmc/regression/jbmc-strings/RegionMatches/test4.desc
index 73e74987ff9..7a4de12d393 100644
--- a/jbmc/regression/jbmc-strings/RegionMatches/test4.desc
+++ b/jbmc/regression/jbmc-strings/RegionMatches/test4.desc
@@ -1,6 +1,6 @@
 FUTURE
 RegionMatches
---max-nondet-string-length 1000 --function RegionMatches.constant --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::RegionMatches.constant:(I)V.assertion.4"
+--max-nondet-string-length 1000 --function RegionMatches.constant --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::RegionMatches.constant:(I)V.assertion.4'
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/jbmc/regression/jbmc-strings/StringBuilderAppend03/test1.desc b/jbmc/regression/jbmc-strings/StringBuilderAppend03/test1.desc
index d2f368ac5e4..f6f6e3ed961 100644
--- a/jbmc/regression/jbmc-strings/StringBuilderAppend03/test1.desc
+++ b/jbmc/regression/jbmc-strings/StringBuilderAppend03/test1.desc
@@ -1,6 +1,6 @@
-CORE winbug
+CORE
 test
---function test.nondet --max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::test.nondet:(Ljava/lang/String;)V.assertion.1"
+--function test.nondet --max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::test.nondet:(Ljava/lang/String;)V.assertion.1'
 ^EXIT=10$
 ^SIGNAL=0$
 \[.*assertion\.1\] .* line 9 .* FAILURE
diff --git a/jbmc/regression/jbmc-strings/StringBuilderAppend03/test2.desc b/jbmc/regression/jbmc-strings/StringBuilderAppend03/test2.desc
index e8b3483d3ac..273857f0a27 100644
--- a/jbmc/regression/jbmc-strings/StringBuilderAppend03/test2.desc
+++ b/jbmc/regression/jbmc-strings/StringBuilderAppend03/test2.desc
@@ -1,6 +1,6 @@
-CORE winbug
+CORE
 test
---function test.nondet --max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::test.nondet:(Ljava/lang/String;)V.assertion.2"
+--function test.nondet --max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::test.nondet:(Ljava/lang/String;)V.assertion.2'
 ^EXIT=10$
 ^SIGNAL=0$
 \[.*assertion\.2\] .* line 11.* FAILURE
diff --git a/jbmc/regression/jbmc-strings/StringBuilderAppend03/test3.desc b/jbmc/regression/jbmc-strings/StringBuilderAppend03/test3.desc
index 3528cddfee3..a5cb3085d60 100644
--- a/jbmc/regression/jbmc-strings/StringBuilderAppend03/test3.desc
+++ b/jbmc/regression/jbmc-strings/StringBuilderAppend03/test3.desc
@@ -1,6 +1,6 @@
-CORE symex-driven-lazy-loading-expected-failure winbug
+CORE symex-driven-lazy-loading-expected-failure
 test
---function test.nondet --max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::test.nondet:(Ljava/lang/String;)V.assertion.3"
+--function test.nondet --max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::test.nondet:(Ljava/lang/String;)V.assertion.3'
 ^EXIT=0$
 ^SIGNAL=0$
 \[.*assertion\.3\] .* line 13.* SUCCESS
diff --git a/jbmc/regression/jbmc-strings/StringBuilderSubstringConstantEvaluation2/test1.desc b/jbmc/regression/jbmc-strings/StringBuilderSubstringConstantEvaluation2/test1.desc
index 8214fd34db9..6abf4698a7f 100644
--- a/jbmc/regression/jbmc-strings/StringBuilderSubstringConstantEvaluation2/test1.desc
+++ b/jbmc/regression/jbmc-strings/StringBuilderSubstringConstantEvaluation2/test1.desc
@@ -1,6 +1,6 @@
-CORE symex-driven-lazy-loading-expected-failure winbug
+CORE symex-driven-lazy-loading-expected-failure
 Main
---function Main.test1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.test1:(Ljava/lang/StringBuilder;)V.assertion.1"
+--function Main.test1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Main.test1:(Ljava/lang/StringBuilder;)V.assertion.1'
 ^Generated 1 VCC\(s\), 1 remaining after simplification$
 ^EXIT=10$
 ^SIGNAL=0$
diff --git a/jbmc/regression/jbmc-strings/StringBuilderSubstringConstantEvaluation2/test2.desc b/jbmc/regression/jbmc-strings/StringBuilderSubstringConstantEvaluation2/test2.desc
index 35e43e66be4..b3c1dbf3fa7 100644
--- a/jbmc/regression/jbmc-strings/StringBuilderSubstringConstantEvaluation2/test2.desc
+++ b/jbmc/regression/jbmc-strings/StringBuilderSubstringConstantEvaluation2/test2.desc
@@ -1,6 +1,6 @@
-CORE symex-driven-lazy-loading-expected-failure winbug
+CORE symex-driven-lazy-loading-expected-failure
 Main
---function Main.test2 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.test2:(I)V.assertion.1"
+--function Main.test2 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Main.test2:(I)V.assertion.1'
 ^Generated 1 VCC\(s\), 1 remaining after simplification$
 ^EXIT=10$
 ^SIGNAL=0$
diff --git a/jbmc/regression/jbmc-strings/StringBuilderSubstringConstantEvaluation2/test3.desc b/jbmc/regression/jbmc-strings/StringBuilderSubstringConstantEvaluation2/test3.desc
index f2b22ce1836..cc4d2dce3a0 100644
--- a/jbmc/regression/jbmc-strings/StringBuilderSubstringConstantEvaluation2/test3.desc
+++ b/jbmc/regression/jbmc-strings/StringBuilderSubstringConstantEvaluation2/test3.desc
@@ -1,6 +1,6 @@
-CORE symex-driven-lazy-loading-expected-failure winbug
+CORE symex-driven-lazy-loading-expected-failure
 Main
---function Main.test3 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.test3:(Ljava/lang/StringBuilder;I)V.assertion.1"
+--function Main.test3 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Main.test3:(Ljava/lang/StringBuilder;I)V.assertion.1'
 ^Generated 1 VCC\(s\), 1 remaining after simplification$
 ^EXIT=10$
 ^SIGNAL=0$
diff --git a/jbmc/regression/jbmc-strings/StringCompareTo/testFail1.desc b/jbmc/regression/jbmc-strings/StringCompareTo/testFail1.desc
index 17e4d1ff49f..ef638484488 100644
--- a/jbmc/regression/jbmc-strings/StringCompareTo/testFail1.desc
+++ b/jbmc/regression/jbmc-strings/StringCompareTo/testFail1.desc
@@ -1,6 +1,6 @@
-CORE symex-driven-lazy-loading-expected-failure winbug
+CORE symex-driven-lazy-loading-expected-failure
 Main
---function Main.nondetFail --max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.nondetFail:(ZLjava/lang/String;Ljava/lang/String;)V.assertion.1" 
+--function Main.nondetFail --max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Main.nondetFail:(ZLjava/lang/String;Ljava/lang/String;)V.assertion.1' 
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/jbmc/regression/jbmc-strings/StringCompareTo/testFail2.desc b/jbmc/regression/jbmc-strings/StringCompareTo/testFail2.desc
index b25cdf79b65..aa6b301775c 100644
--- a/jbmc/regression/jbmc-strings/StringCompareTo/testFail2.desc
+++ b/jbmc/regression/jbmc-strings/StringCompareTo/testFail2.desc
@@ -1,6 +1,6 @@
-CORE symex-driven-lazy-loading-expected-failure winbug
+CORE symex-driven-lazy-loading-expected-failure
 Main
---function Main.nondetFail --max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.nondetFail:(ZLjava/lang/String;Ljava/lang/String;)V.assertion.2" 
+--function Main.nondetFail --max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Main.nondetFail:(ZLjava/lang/String;Ljava/lang/String;)V.assertion.2' 
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/jbmc/regression/jbmc-strings/StringCompareTo/testFail3.desc b/jbmc/regression/jbmc-strings/StringCompareTo/testFail3.desc
index 688930a9055..34fc3e5ea7a 100644
--- a/jbmc/regression/jbmc-strings/StringCompareTo/testFail3.desc
+++ b/jbmc/regression/jbmc-strings/StringCompareTo/testFail3.desc
@@ -1,6 +1,6 @@
-CORE symex-driven-lazy-loading-expected-failure winbug
+CORE symex-driven-lazy-loading-expected-failure
 Main
---function Main.nondetFail --max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.nondetFail:(ZLjava/lang/String;Ljava/lang/String;)V.assertion.3" 
+--function Main.nondetFail --max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Main.nondetFail:(ZLjava/lang/String;Ljava/lang/String;)V.assertion.3' 
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/jbmc/regression/jbmc-strings/StringCompareTo/testFail4.desc b/jbmc/regression/jbmc-strings/StringCompareTo/testFail4.desc
index bc7665b5fcc..3f161c794dc 100644
--- a/jbmc/regression/jbmc-strings/StringCompareTo/testFail4.desc
+++ b/jbmc/regression/jbmc-strings/StringCompareTo/testFail4.desc
@@ -1,6 +1,6 @@
-CORE symex-driven-lazy-loading-expected-failure winbug
+CORE symex-driven-lazy-loading-expected-failure
 Main
---function Main.nondetFail --max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.nondetFail:(ZLjava/lang/String;Ljava/lang/String;)V.assertion.4" 
+--function Main.nondetFail --max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Main.nondetFail:(ZLjava/lang/String;Ljava/lang/String;)V.assertion.4' 
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/jbmc/regression/jbmc-strings/StringCompareTo/testFail5.desc b/jbmc/regression/jbmc-strings/StringCompareTo/testFail5.desc
index 9c9913cc1d8..0827174cb3b 100644
--- a/jbmc/regression/jbmc-strings/StringCompareTo/testFail5.desc
+++ b/jbmc/regression/jbmc-strings/StringCompareTo/testFail5.desc
@@ -1,6 +1,6 @@
-CORE symex-driven-lazy-loading-expected-failure winbug
+CORE symex-driven-lazy-loading-expected-failure
 Main
---function Main.nondetFail --max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.nondetFail:(ZLjava/lang/String;Ljava/lang/String;)V.assertion.5" 
+--function Main.nondetFail --max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Main.nondetFail:(ZLjava/lang/String;Ljava/lang/String;)V.assertion.5' 
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/jbmc/regression/jbmc-strings/StringCompareTo/testFail6.desc b/jbmc/regression/jbmc-strings/StringCompareTo/testFail6.desc
index af59ef93dfe..643d252a4e3 100644
--- a/jbmc/regression/jbmc-strings/StringCompareTo/testFail6.desc
+++ b/jbmc/regression/jbmc-strings/StringCompareTo/testFail6.desc
@@ -1,6 +1,6 @@
-CORE symex-driven-lazy-loading-expected-failure winbug
+CORE symex-driven-lazy-loading-expected-failure
 Main
---function Main.nondetFail --max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.nondetFail:(ZLjava/lang/String;Ljava/lang/String;)V.assertion.6" 
+--function Main.nondetFail --max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Main.nondetFail:(ZLjava/lang/String;Ljava/lang/String;)V.assertion.6' 
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/jbmc/regression/jbmc-strings/StringCompareTo/testPass1.desc b/jbmc/regression/jbmc-strings/StringCompareTo/testPass1.desc
index d88e45df4ab..9e8a63b20e5 100644
--- a/jbmc/regression/jbmc-strings/StringCompareTo/testPass1.desc
+++ b/jbmc/regression/jbmc-strings/StringCompareTo/testPass1.desc
@@ -1,6 +1,6 @@
-CORE symex-driven-lazy-loading-expected-failure winbug
+CORE symex-driven-lazy-loading-expected-failure
 Main
---function Main.nondetPass --max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.nondetPass:(Ljava/lang/String;Ljava/lang/String;)V.assertion.1" 
+--function Main.nondetPass --max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Main.nondetPass:(Ljava/lang/String;Ljava/lang/String;)V.assertion.1' 
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/jbmc-strings/StringCompareTo/testPass2.desc b/jbmc/regression/jbmc-strings/StringCompareTo/testPass2.desc
index 66cdd5abbd7..d4fef8af6e4 100644
--- a/jbmc/regression/jbmc-strings/StringCompareTo/testPass2.desc
+++ b/jbmc/regression/jbmc-strings/StringCompareTo/testPass2.desc
@@ -1,6 +1,6 @@
-CORE symex-driven-lazy-loading-expected-failure winbug
+CORE symex-driven-lazy-loading-expected-failure
 Main
---function Main.nondetPass --max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.nondetPass:(Ljava/lang/String;Ljava/lang/String;)V.assertion.2" 
+--function Main.nondetPass --max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Main.nondetPass:(Ljava/lang/String;Ljava/lang/String;)V.assertion.2' 
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/jbmc-strings/StringCompareTo/testPass3.desc b/jbmc/regression/jbmc-strings/StringCompareTo/testPass3.desc
index 03eaf6e23c8..2d37fcadf03 100644
--- a/jbmc/regression/jbmc-strings/StringCompareTo/testPass3.desc
+++ b/jbmc/regression/jbmc-strings/StringCompareTo/testPass3.desc
@@ -1,6 +1,6 @@
-CORE symex-driven-lazy-loading-expected-failure winbug
+CORE symex-driven-lazy-loading-expected-failure
 Main
---function Main.nondetPass --max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.nondetPass:(Ljava/lang/String;Ljava/lang/String;)V.assertion.3" 
+--function Main.nondetPass --max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Main.nondetPass:(Ljava/lang/String;Ljava/lang/String;)V.assertion.3' 
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/jbmc-strings/StringCompareTo/testPass4.desc b/jbmc/regression/jbmc-strings/StringCompareTo/testPass4.desc
index c251c2d02df..b03a7cfc264 100644
--- a/jbmc/regression/jbmc-strings/StringCompareTo/testPass4.desc
+++ b/jbmc/regression/jbmc-strings/StringCompareTo/testPass4.desc
@@ -1,6 +1,6 @@
-CORE symex-driven-lazy-loading-expected-failure winbug
+CORE symex-driven-lazy-loading-expected-failure
 Main
---function Main.nondetPass --max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.nondetPass:(Ljava/lang/String;Ljava/lang/String;)V.assertion.4" 
+--function Main.nondetPass --max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Main.nondetPass:(Ljava/lang/String;Ljava/lang/String;)V.assertion.4' 
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/jbmc-strings/StringCompareTo/testPass5.desc b/jbmc/regression/jbmc-strings/StringCompareTo/testPass5.desc
index ee859b0bc68..173c89f9dbb 100644
--- a/jbmc/regression/jbmc-strings/StringCompareTo/testPass5.desc
+++ b/jbmc/regression/jbmc-strings/StringCompareTo/testPass5.desc
@@ -1,6 +1,6 @@
-CORE symex-driven-lazy-loading-expected-failure winbug
+CORE symex-driven-lazy-loading-expected-failure
 Main
---function Main.nondetPass --max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.nondetPass:(Ljava/lang/String;Ljava/lang/String;)V.assertion.5" 
+--function Main.nondetPass --max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Main.nondetPass:(Ljava/lang/String;Ljava/lang/String;)V.assertion.5' 
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/jbmc-strings/StringCompareTo/testPass6.desc b/jbmc/regression/jbmc-strings/StringCompareTo/testPass6.desc
index aa41056b36f..a5b0099514a 100644
--- a/jbmc/regression/jbmc-strings/StringCompareTo/testPass6.desc
+++ b/jbmc/regression/jbmc-strings/StringCompareTo/testPass6.desc
@@ -1,6 +1,6 @@
-CORE symex-driven-lazy-loading-expected-failure winbug
+CORE symex-driven-lazy-loading-expected-failure
 Main
---function Main.nondetPass --max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.nondetPass:(Ljava/lang/String;Ljava/lang/String;)V.assertion.6" 
+--function Main.nondetPass --max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Main.nondetPass:(Ljava/lang/String;Ljava/lang/String;)V.assertion.6' 
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/jbmc-strings/StringFormatBool/test-bool-length-true-fail.desc b/jbmc/regression/jbmc-strings/StringFormatBool/test-bool-length-true-fail.desc
index dc710a6a454..0c3bb03ce2b 100644
--- a/jbmc/regression/jbmc-strings/StringFormatBool/test-bool-length-true-fail.desc
+++ b/jbmc/regression/jbmc-strings/StringFormatBool/test-bool-length-true-fail.desc
@@ -1,6 +1,6 @@
-CORE winbug
+CORE
 Test
---function Test.testBoolLengthTrue --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Test.testBoolLengthTrue:()Ljava/lang/String;.assertion.1"
+--function Test.testBoolLengthTrue --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Test.testBoolLengthTrue:()Ljava/lang/String;.assertion.1'
 ^EXIT=10$
 ^SIGNAL=0$
 line 27 assertion at file Test.java .*: FAILURE
diff --git a/jbmc/regression/jbmc-strings/StringFormatBool/test-bool-length-true-pass.desc b/jbmc/regression/jbmc-strings/StringFormatBool/test-bool-length-true-pass.desc
index 576d4fb28cf..b4f480e0c97 100644
--- a/jbmc/regression/jbmc-strings/StringFormatBool/test-bool-length-true-pass.desc
+++ b/jbmc/regression/jbmc-strings/StringFormatBool/test-bool-length-true-pass.desc
@@ -1,6 +1,6 @@
 KNOWNBUG
 Test
---function Test.testBoolLengthTrue --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Test.testBoolLengthTrue:()Ljava/lang/String;.assertion.2"
+--function Test.testBoolLengthTrue --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Test.testBoolLengthTrue:()Ljava/lang/String;.assertion.2'
 ^EXIT=0$
 ^SIGNAL=0$
 line 29 assertion at file Test.java .*: SUCCESS
diff --git a/jbmc/regression/jbmc-strings/StringFormatBool/test-bool-length1.desc b/jbmc/regression/jbmc-strings/StringFormatBool/test-bool-length1.desc
index bf70c164113..54c2f6b20ce 100644
--- a/jbmc/regression/jbmc-strings/StringFormatBool/test-bool-length1.desc
+++ b/jbmc/regression/jbmc-strings/StringFormatBool/test-bool-length1.desc
@@ -1,6 +1,6 @@
-CORE winbug
+CORE
 Test
---function Test.testBoolLength --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Test.testBoolLength:(Z)Ljava/lang/String;.assertion.1"
+--function Test.testBoolLength --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Test.testBoolLength:(Z)Ljava/lang/String;.assertion.1'
 ^EXIT=10$
 ^SIGNAL=0$
 line 16 assertion at file Test.java .*: FAILURE
diff --git a/jbmc/regression/jbmc-strings/StringFormatBool/test-bool-length2.desc b/jbmc/regression/jbmc-strings/StringFormatBool/test-bool-length2.desc
index 870e98d0eca..5b68696d3fd 100644
--- a/jbmc/regression/jbmc-strings/StringFormatBool/test-bool-length2.desc
+++ b/jbmc/regression/jbmc-strings/StringFormatBool/test-bool-length2.desc
@@ -1,6 +1,6 @@
-CORE winbug
+CORE
 Test
---function Test.testBoolLength --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Test.testBoolLength:(Z)Ljava/lang/String;.assertion.2"
+--function Test.testBoolLength --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Test.testBoolLength:(Z)Ljava/lang/String;.assertion.2'
 ^EXIT=10$
 ^SIGNAL=0$
 line 18 assertion at file Test.java .*: FAILURE
diff --git a/jbmc/regression/jbmc-strings/StringFormatBool/test-bool-length3.desc b/jbmc/regression/jbmc-strings/StringFormatBool/test-bool-length3.desc
index ce8cb9821bd..9b7e79986f6 100644
--- a/jbmc/regression/jbmc-strings/StringFormatBool/test-bool-length3.desc
+++ b/jbmc/regression/jbmc-strings/StringFormatBool/test-bool-length3.desc
@@ -1,6 +1,6 @@
-CORE symex-driven-lazy-loading-expected-failure winbug
+CORE symex-driven-lazy-loading-expected-failure
 Test
---function Test.testBoolLength --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Test.testBoolLength:(Z)Ljava/lang/String;.assertion.3"
+--function Test.testBoolLength --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Test.testBoolLength:(Z)Ljava/lang/String;.assertion.3'
 ^EXIT=0$
 ^SIGNAL=0$
 line 20 assertion at file Test.java .*: SUCCESS
diff --git a/jbmc/regression/jbmc-strings/StringFormatBool/test-bool1.desc b/jbmc/regression/jbmc-strings/StringFormatBool/test-bool1.desc
index 961e18fdd09..903a856ecf4 100644
--- a/jbmc/regression/jbmc-strings/StringFormatBool/test-bool1.desc
+++ b/jbmc/regression/jbmc-strings/StringFormatBool/test-bool1.desc
@@ -1,6 +1,6 @@
-CORE winbug
+CORE
 Test
---function Test.testBool --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Test.testBool:(Z)Ljava/lang/String;.assertion.1"
+--function Test.testBool --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Test.testBool:(Z)Ljava/lang/String;.assertion.1'
 ^EXIT=10$
 ^SIGNAL=0$
 line 5 assertion at file Test.java .*: FAILURE
diff --git a/jbmc/regression/jbmc-strings/StringFormatBool/test-bool2.desc b/jbmc/regression/jbmc-strings/StringFormatBool/test-bool2.desc
index 3d7b32a77dd..acc978d1fc4 100644
--- a/jbmc/regression/jbmc-strings/StringFormatBool/test-bool2.desc
+++ b/jbmc/regression/jbmc-strings/StringFormatBool/test-bool2.desc
@@ -1,6 +1,6 @@
-CORE winbug
+CORE
 Test
---function Test.testBool --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Test.testBool:(Z)Ljava/lang/String;.assertion.2"
+--function Test.testBool --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Test.testBool:(Z)Ljava/lang/String;.assertion.2'
 ^EXIT=10$
 ^SIGNAL=0$
 line 7 assertion at file Test.java .*: FAILURE
diff --git a/jbmc/regression/jbmc-strings/StringFormatBool/test-bool3.desc b/jbmc/regression/jbmc-strings/StringFormatBool/test-bool3.desc
index 423523e62c1..188dc1eb9a0 100644
--- a/jbmc/regression/jbmc-strings/StringFormatBool/test-bool3.desc
+++ b/jbmc/regression/jbmc-strings/StringFormatBool/test-bool3.desc
@@ -1,6 +1,6 @@
-CORE symex-driven-lazy-loading-expected-failure winbug
+CORE symex-driven-lazy-loading-expected-failure
 Test
---function Test.testBool --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Test.testBool:(Z)Ljava/lang/String;.assertion.3"
+--function Test.testBool --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Test.testBool:(Z)Ljava/lang/String;.assertion.3'
 ^EXIT=0$
 ^SIGNAL=0$
 line 9 assertion at file Test.java .*: SUCCESS
diff --git a/jbmc/regression/jbmc-strings/StringFormatHex/test-hex-length-const-fail.desc b/jbmc/regression/jbmc-strings/StringFormatHex/test-hex-length-const-fail.desc
index 5d80adc0ef4..2c8753d7de8 100644
--- a/jbmc/regression/jbmc-strings/StringFormatHex/test-hex-length-const-fail.desc
+++ b/jbmc/regression/jbmc-strings/StringFormatHex/test-hex-length-const-fail.desc
@@ -1,6 +1,6 @@
-CORE winbug
+CORE
 Test
---function Test.testHexLengthConstFAIL --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Test.testHexLengthConstFAIL:()V.assertion.1"
+--function Test.testHexLengthConstFAIL --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Test.testHexLengthConstFAIL:()V.assertion.1'
 ^EXIT=10$
 ^SIGNAL=0$
 line 20 assertion at file Test.java .*: FAILURE
diff --git a/jbmc/regression/jbmc-strings/StringFormatHex/test-hex-length-const-pass.desc b/jbmc/regression/jbmc-strings/StringFormatHex/test-hex-length-const-pass.desc
index 40b6246738f..a4074daaffb 100644
--- a/jbmc/regression/jbmc-strings/StringFormatHex/test-hex-length-const-pass.desc
+++ b/jbmc/regression/jbmc-strings/StringFormatHex/test-hex-length-const-pass.desc
@@ -1,6 +1,6 @@
-CORE winbug
+CORE
 Test
---function Test.testHexLengthConstPASS --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Test.testHexLengthConstPASS:()V.assertion.1"
+--function Test.testHexLengthConstPASS --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Test.testHexLengthConstPASS:()V.assertion.1'
 ^EXIT=0$
 ^SIGNAL=0$
 line 15 assertion at file Test.java .*: SUCCESS
diff --git a/jbmc/regression/jbmc-strings/StringFormatHex/test-hex1.desc b/jbmc/regression/jbmc-strings/StringFormatHex/test-hex1.desc
index de9ce19294f..7d5b64cba12 100644
--- a/jbmc/regression/jbmc-strings/StringFormatHex/test-hex1.desc
+++ b/jbmc/regression/jbmc-strings/StringFormatHex/test-hex1.desc
@@ -1,6 +1,6 @@
-CORE winbug
+CORE
 Test
---function Test.testHex --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Test.testHex:(I)Ljava/lang/String;.assertion.1"
+--function Test.testHex --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Test.testHex:(I)Ljava/lang/String;.assertion.1'
 ^EXIT=10$
 ^SIGNAL=0$
 line 5 assertion at file Test.java .*: FAILURE
diff --git a/jbmc/regression/jbmc-strings/StringFormatHex/test-hex2.desc b/jbmc/regression/jbmc-strings/StringFormatHex/test-hex2.desc
index e600f254eaf..0824d98964e 100644
--- a/jbmc/regression/jbmc-strings/StringFormatHex/test-hex2.desc
+++ b/jbmc/regression/jbmc-strings/StringFormatHex/test-hex2.desc
@@ -1,6 +1,6 @@
-CORE winbug
+CORE
 Test
---function Test.testHex --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Test.testHex:(I)Ljava/lang/String;.assertion.2"
+--function Test.testHex --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Test.testHex:(I)Ljava/lang/String;.assertion.2'
 ^EXIT=10$
 ^SIGNAL=0$
 line 7 assertion at file Test.java .*: FAILURE
diff --git a/jbmc/regression/jbmc-strings/StringFormatHex/test-hex3.desc b/jbmc/regression/jbmc-strings/StringFormatHex/test-hex3.desc
index aacb598f29f..c622aa8f2df 100644
--- a/jbmc/regression/jbmc-strings/StringFormatHex/test-hex3.desc
+++ b/jbmc/regression/jbmc-strings/StringFormatHex/test-hex3.desc
@@ -1,6 +1,6 @@
-CORE symex-driven-lazy-loading-expected-failure winbug
+CORE symex-driven-lazy-loading-expected-failure
 Test
---function Test.testHex --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Test.testHex:(I)Ljava/lang/String;.assertion.3"
+--function Test.testHex --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Test.testHex:(I)Ljava/lang/String;.assertion.3'
 ^EXIT=0$
 ^SIGNAL=0$
 line 9 assertion at file Test.java .*: SUCCESS
diff --git a/jbmc/regression/jbmc-strings/StringFormatInt/test-int-length-const-fail.desc b/jbmc/regression/jbmc-strings/StringFormatInt/test-int-length-const-fail.desc
index 3ba56960791..d5b9a50998c 100644
--- a/jbmc/regression/jbmc-strings/StringFormatInt/test-int-length-const-fail.desc
+++ b/jbmc/regression/jbmc-strings/StringFormatInt/test-int-length-const-fail.desc
@@ -1,6 +1,6 @@
-CORE winbug
+CORE
 Test
---function Test.testIntLengthConstFAIL --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Test.testIntLengthConstFAIL:()V.assertion.1"
+--function Test.testIntLengthConstFAIL --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Test.testIntLengthConstFAIL:()V.assertion.1'
 ^EXIT=10$
 ^SIGNAL=0$
 line 25 assertion at file Test.java .*: FAILURE
diff --git a/jbmc/regression/jbmc-strings/StringFormatInt/test-int-length-const-pass.desc b/jbmc/regression/jbmc-strings/StringFormatInt/test-int-length-const-pass.desc
index 60e5e544eff..2cea3a143af 100644
--- a/jbmc/regression/jbmc-strings/StringFormatInt/test-int-length-const-pass.desc
+++ b/jbmc/regression/jbmc-strings/StringFormatInt/test-int-length-const-pass.desc
@@ -1,6 +1,6 @@
-CORE winbug
+CORE
 Test
---function Test.testIntLengthConstPASS --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Test.testIntLengthConstPASS:()V.assertion.1"
+--function Test.testIntLengthConstPASS --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Test.testIntLengthConstPASS:()V.assertion.1'
 ^EXIT=0$
 ^SIGNAL=0$
 line 20 assertion at file Test.java .*: SUCCESS
diff --git a/jbmc/regression/jbmc-strings/StringFormatInt/test-int-length.desc b/jbmc/regression/jbmc-strings/StringFormatInt/test-int-length.desc
index 20474e5d6d5..6c2ac9d92dd 100644
--- a/jbmc/regression/jbmc-strings/StringFormatInt/test-int-length.desc
+++ b/jbmc/regression/jbmc-strings/StringFormatInt/test-int-length.desc
@@ -1,6 +1,6 @@
-CORE winbug
+CORE
 Test
---function Test.testIntLength --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Test.testIntLength:(I)V.assertion.1"
+--function Test.testIntLength --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Test.testIntLength:(I)V.assertion.1'
  
 ^EXIT=10$
 ^SIGNAL=0$
diff --git a/jbmc/regression/jbmc-strings/StringFormatInt/test-int1.desc b/jbmc/regression/jbmc-strings/StringFormatInt/test-int1.desc
index fbd133f1ae9..499a7b5cea2 100644
--- a/jbmc/regression/jbmc-strings/StringFormatInt/test-int1.desc
+++ b/jbmc/regression/jbmc-strings/StringFormatInt/test-int1.desc
@@ -1,6 +1,6 @@
-CORE winbug
+CORE
 Test
---function Test.testInt --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Test.testInt:(I)Ljava/lang/String;.assertion.1"
+--function Test.testInt --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Test.testInt:(I)Ljava/lang/String;.assertion.1'
 ^EXIT=10$
 ^SIGNAL=0$
 line 5 assertion at file Test.java .*: FAILURE
diff --git a/jbmc/regression/jbmc-strings/StringFormatInt/test-int2.desc b/jbmc/regression/jbmc-strings/StringFormatInt/test-int2.desc
index 987767b2454..a8fdf853bff 100644
--- a/jbmc/regression/jbmc-strings/StringFormatInt/test-int2.desc
+++ b/jbmc/regression/jbmc-strings/StringFormatInt/test-int2.desc
@@ -1,6 +1,6 @@
-CORE symex-driven-lazy-loading-expected-failure winbug
+CORE symex-driven-lazy-loading-expected-failure
 Test
---function Test.testInt --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Test.testInt:(I)Ljava/lang/String;.assertion.2"
+--function Test.testInt --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Test.testInt:(I)Ljava/lang/String;.assertion.2'
 ^EXIT=0$
 ^SIGNAL=0$
 line 7 assertion at file Test.java .*: SUCCESS
diff --git a/jbmc/regression/jbmc-strings/StringFormatInt/test-int3.desc b/jbmc/regression/jbmc-strings/StringFormatInt/test-int3.desc
index 60cc991fe37..c44a7897597 100644
--- a/jbmc/regression/jbmc-strings/StringFormatInt/test-int3.desc
+++ b/jbmc/regression/jbmc-strings/StringFormatInt/test-int3.desc
@@ -1,6 +1,6 @@
-CORE winbug
+CORE
 Test
---function Test.testInt --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Test.testInt:(I)Ljava/lang/String;.assertion.3"
+--function Test.testInt --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Test.testInt:(I)Ljava/lang/String;.assertion.3'
 ^EXIT=10$
 ^SIGNAL=0$
 line 9 assertion at file Test.java .*: FAILURE
diff --git a/jbmc/regression/jbmc-strings/StringFormatSpecial/test-newline-fail.desc b/jbmc/regression/jbmc-strings/StringFormatSpecial/test-newline-fail.desc
index 9aa6d6fee52..d6662a8f9bf 100644
--- a/jbmc/regression/jbmc-strings/StringFormatSpecial/test-newline-fail.desc
+++ b/jbmc/regression/jbmc-strings/StringFormatSpecial/test-newline-fail.desc
@@ -1,6 +1,6 @@
-CORE winbug
+CORE
 Test
---function Test.newline --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Test.newline:()Ljava/lang/String;.assertion.1"
+--function Test.newline --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Test.newline:()Ljava/lang/String;.assertion.1'
 ^EXIT=10$
 ^SIGNAL=0$
 line 23 assertion at file Test.java .*: FAILURE
diff --git a/jbmc/regression/jbmc-strings/StringFormatSpecial/test-newline-length-fail.desc b/jbmc/regression/jbmc-strings/StringFormatSpecial/test-newline-length-fail.desc
index bdf046ca966..0d6441d2987 100644
--- a/jbmc/regression/jbmc-strings/StringFormatSpecial/test-newline-length-fail.desc
+++ b/jbmc/regression/jbmc-strings/StringFormatSpecial/test-newline-length-fail.desc
@@ -1,6 +1,6 @@
-CORE winbug
+CORE
 Test
---function Test.newlineLength --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Test.newlineLength:()Ljava/lang/String;.assertion.1"
+--function Test.newlineLength --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Test.newlineLength:()Ljava/lang/String;.assertion.1'
 ^EXIT=10$
 ^SIGNAL=0$
 line 32 assertion at file Test.java .*: FAILURE
diff --git a/jbmc/regression/jbmc-strings/StringFormatSpecial/test-newline-length-pass.desc b/jbmc/regression/jbmc-strings/StringFormatSpecial/test-newline-length-pass.desc
index 53a936e37eb..95aaa2d8586 100644
--- a/jbmc/regression/jbmc-strings/StringFormatSpecial/test-newline-length-pass.desc
+++ b/jbmc/regression/jbmc-strings/StringFormatSpecial/test-newline-length-pass.desc
@@ -1,6 +1,6 @@
-CORE symex-driven-lazy-loading-expected-failure winbug
+CORE symex-driven-lazy-loading-expected-failure
 Test
---function Test.newlineLength --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Test.newlineLength:()Ljava/lang/String;.assertion.2"
+--function Test.newlineLength --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Test.newlineLength:()Ljava/lang/String;.assertion.2'
 ^EXIT=0$
 ^SIGNAL=0$
 line 34 assertion at file Test.java .*: SUCCESS
diff --git a/jbmc/regression/jbmc-strings/StringFormatSpecial/test-newline-pass.desc b/jbmc/regression/jbmc-strings/StringFormatSpecial/test-newline-pass.desc
index f77103c4c7a..5425b0144a5 100644
--- a/jbmc/regression/jbmc-strings/StringFormatSpecial/test-newline-pass.desc
+++ b/jbmc/regression/jbmc-strings/StringFormatSpecial/test-newline-pass.desc
@@ -1,6 +1,6 @@
-CORE symex-driven-lazy-loading-expected-failure winbug
+CORE symex-driven-lazy-loading-expected-failure
 Test
---function Test.newline --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Test.newline:()Ljava/lang/String;.assertion.2"
+--function Test.newline --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Test.newline:()Ljava/lang/String;.assertion.2'
 ^EXIT=0$
 ^SIGNAL=0$
 line 25 assertion at file Test.java .*: SUCCESS
diff --git a/jbmc/regression/jbmc-strings/StringFormatSpecial/test-percent-fail.desc b/jbmc/regression/jbmc-strings/StringFormatSpecial/test-percent-fail.desc
index 43b9fbcd8b2..8dcf46f3421 100644
--- a/jbmc/regression/jbmc-strings/StringFormatSpecial/test-percent-fail.desc
+++ b/jbmc/regression/jbmc-strings/StringFormatSpecial/test-percent-fail.desc
@@ -1,6 +1,6 @@
-CORE winbug
+CORE
 Test
---function Test.percent --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Test.percent:()Ljava/lang/String;.assertion.1"
+--function Test.percent --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Test.percent:()Ljava/lang/String;.assertion.1'
 ^EXIT=10$
 ^SIGNAL=0$
 line 5 assertion at file Test.java .*: FAILURE
diff --git a/jbmc/regression/jbmc-strings/StringFormatSpecial/test-percent-length-fail.desc b/jbmc/regression/jbmc-strings/StringFormatSpecial/test-percent-length-fail.desc
index 74a9c515f49..491e62ca1c6 100644
--- a/jbmc/regression/jbmc-strings/StringFormatSpecial/test-percent-length-fail.desc
+++ b/jbmc/regression/jbmc-strings/StringFormatSpecial/test-percent-length-fail.desc
@@ -1,6 +1,6 @@
-CORE winbug
+CORE
 Test
---function Test.percentLength --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Test.percentLength:()Ljava/lang/String;.assertion.1"
+--function Test.percentLength --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Test.percentLength:()Ljava/lang/String;.assertion.1'
 ^EXIT=10$
 ^SIGNAL=0$
 line 14 assertion at file Test.java .*: FAILURE
diff --git a/jbmc/regression/jbmc-strings/StringFormatSpecial/test-percent-length-pass.desc b/jbmc/regression/jbmc-strings/StringFormatSpecial/test-percent-length-pass.desc
index 74aa9e95f99..83c128d9349 100644
--- a/jbmc/regression/jbmc-strings/StringFormatSpecial/test-percent-length-pass.desc
+++ b/jbmc/regression/jbmc-strings/StringFormatSpecial/test-percent-length-pass.desc
@@ -1,6 +1,6 @@
-CORE symex-driven-lazy-loading-expected-failure winbug
+CORE symex-driven-lazy-loading-expected-failure
 Test
---function Test.percentLength --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Test.percentLength:()Ljava/lang/String;.assertion.2"
+--function Test.percentLength --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Test.percentLength:()Ljava/lang/String;.assertion.2'
 ^EXIT=0$
 ^SIGNAL=0$
 line 16 assertion at file Test.java .*: SUCCESS
diff --git a/jbmc/regression/jbmc-strings/StringFormatSpecial/test-percent-pass.desc b/jbmc/regression/jbmc-strings/StringFormatSpecial/test-percent-pass.desc
index f7885b85a40..69dc57a37a0 100644
--- a/jbmc/regression/jbmc-strings/StringFormatSpecial/test-percent-pass.desc
+++ b/jbmc/regression/jbmc-strings/StringFormatSpecial/test-percent-pass.desc
@@ -1,6 +1,6 @@
-CORE symex-driven-lazy-loading-expected-failure winbug
+CORE symex-driven-lazy-loading-expected-failure
 Test
---function Test.percent --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Test.percent:()Ljava/lang/String;.assertion.2"
+--function Test.percent --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Test.percent:()Ljava/lang/String;.assertion.2'
 ^EXIT=0$
 ^SIGNAL=0$
 line 7 assertion at file Test.java .*: SUCCESS
diff --git a/jbmc/regression/jbmc-strings/StringFormatString/test-string2.desc b/jbmc/regression/jbmc-strings/StringFormatString/test-string2.desc
index ab13aa79067..97857047090 100644
--- a/jbmc/regression/jbmc-strings/StringFormatString/test-string2.desc
+++ b/jbmc/regression/jbmc-strings/StringFormatString/test-string2.desc
@@ -1,6 +1,6 @@
-CORE winbug
+CORE
 Test
---function Test.string2 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --max-nondet-string-length 20 --property "java::Test.string2:(Ljava/lang/String;Ljava/lang/String;)Ljava/lang/String;.assertion.1"
+--function Test.string2 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --max-nondet-string-length 20 --property 'java::Test.string2:(Ljava/lang/String;Ljava/lang/String;)Ljava/lang/String;.assertion.1'
 ^EXIT=0$
 ^SIGNAL=0$
 line 37 assertion at file Test.java .*: SUCCESS
diff --git a/jbmc/regression/jbmc-strings/StringFormatString/test-string3.desc b/jbmc/regression/jbmc-strings/StringFormatString/test-string3.desc
index 1607833f884..3e793deb0e6 100644
--- a/jbmc/regression/jbmc-strings/StringFormatString/test-string3.desc
+++ b/jbmc/regression/jbmc-strings/StringFormatString/test-string3.desc
@@ -1,6 +1,6 @@
-CORE winbug
+CORE
 Test
---function Test.string3 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --max-nondet-string-length 5 --property "java::Test.string3:(Ljava/lang/String;Ljava/lang/String;)Ljava/lang/String;.assertion.1"
+--function Test.string3 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --max-nondet-string-length 5 --property 'java::Test.string3:(Ljava/lang/String;Ljava/lang/String;)Ljava/lang/String;.assertion.1'
 ^EXIT=0$
 ^SIGNAL=0$
 line 45 assertion at file Test.java .*: SUCCESS
diff --git a/jbmc/regression/jbmc-strings/StringSubstringConstantEvaluation2/test1.desc b/jbmc/regression/jbmc-strings/StringSubstringConstantEvaluation2/test1.desc
index 4012e525080..d2762bf1166 100644
--- a/jbmc/regression/jbmc-strings/StringSubstringConstantEvaluation2/test1.desc
+++ b/jbmc/regression/jbmc-strings/StringSubstringConstantEvaluation2/test1.desc
@@ -1,6 +1,6 @@
-CORE symex-driven-lazy-loading-expected-failure winbug
+CORE symex-driven-lazy-loading-expected-failure
 Main
---function Main.test1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.test1:(Ljava/lang/String;)V.assertion.1"
+--function Main.test1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Main.test1:(Ljava/lang/String;)V.assertion.1'
 ^Generated 1 VCC\(s\), 1 remaining after simplification$
 ^EXIT=10$
 ^SIGNAL=0$
diff --git a/jbmc/regression/jbmc-strings/StringSubstringConstantEvaluation2/test2.desc b/jbmc/regression/jbmc-strings/StringSubstringConstantEvaluation2/test2.desc
index 35e43e66be4..b3c1dbf3fa7 100644
--- a/jbmc/regression/jbmc-strings/StringSubstringConstantEvaluation2/test2.desc
+++ b/jbmc/regression/jbmc-strings/StringSubstringConstantEvaluation2/test2.desc
@@ -1,6 +1,6 @@
-CORE symex-driven-lazy-loading-expected-failure winbug
+CORE symex-driven-lazy-loading-expected-failure
 Main
---function Main.test2 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.test2:(I)V.assertion.1"
+--function Main.test2 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Main.test2:(I)V.assertion.1'
 ^Generated 1 VCC\(s\), 1 remaining after simplification$
 ^EXIT=10$
 ^SIGNAL=0$
diff --git a/jbmc/regression/jbmc-strings/StringSubstringConstantEvaluation2/test3.desc b/jbmc/regression/jbmc-strings/StringSubstringConstantEvaluation2/test3.desc
index e3261f45501..886a96139c0 100644
--- a/jbmc/regression/jbmc-strings/StringSubstringConstantEvaluation2/test3.desc
+++ b/jbmc/regression/jbmc-strings/StringSubstringConstantEvaluation2/test3.desc
@@ -1,6 +1,6 @@
-CORE symex-driven-lazy-loading-expected-failure winbug
+CORE symex-driven-lazy-loading-expected-failure
 Main
---function Main.test3 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.test3:(Ljava/lang/String;I)V.assertion.1"
+--function Main.test3 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property 'java::Main.test3:(Ljava/lang/String;I)V.assertion.1'
 ^Generated 1 VCC\(s\), 1 remaining after simplification$
 ^EXIT=10$
 ^SIGNAL=0$
diff --git a/jbmc/regression/jbmc-strings/string-input-value/test1.desc b/jbmc/regression/jbmc-strings/string-input-value/test1.desc
index e740def8621..ae79c4a4ede 100644
--- a/jbmc/regression/jbmc-strings/string-input-value/test1.desc
+++ b/jbmc/regression/jbmc-strings/string-input-value/test1.desc
@@ -1,6 +1,6 @@
-CORE winbug
+CORE
 Test
---string-input-value fo --string-input-value barr --function Test.checkStringInputValue --string-input-value "" --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+--string-input-value fo --string-input-value barr --function Test.checkStringInputValue --string-input-value '' --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 assertion.1.*FAILURE
diff --git a/jbmc/regression/jbmc/CMakeLists.txt b/jbmc/regression/jbmc/CMakeLists.txt
index 865a61dbe17..7aef6667280 100644
--- a/jbmc/regression/jbmc/CMakeLists.txt
+++ b/jbmc/regression/jbmc/CMakeLists.txt
@@ -1,11 +1,5 @@
-if("${CMAKE_SYSTEM_NAME}" STREQUAL "Windows")
-  set(exclude_win_broken_tests -X winbug)
-else()
-  set(exclude_win_broken_tests "")
-endif()
-
 add_test_pl_tests(
-    "$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation --validate-trace" ${exclude_win_broken_tests}
+    "$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation --validate-trace"
 )
 
 if(DEFINED BDD_GUARDS)
@@ -14,7 +8,6 @@ if(DEFINED BDD_GUARDS)
             "$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation --validate-trace --symex-driven-lazy-loading"
             "-C;-X;symex-driven-lazy-loading-expected-failure;-s;symex-driven-loading"
             "CORE"
-            ${exclude_win_broken_tests}
     )
 else()
     add_test_pl_profile(
@@ -22,6 +15,5 @@ else()
             "$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation --validate-trace --symex-driven-lazy-loading"
             "-C;-X;symex-driven-lazy-loading-expected-failure;-X;bdd-expected-timeout;-s;symex-driven-loading"
             "CORE"
-            ${exclude_win_broken_tests}
     )
 endif()
diff --git a/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array-ref-static-values.desc b/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array-ref-static-values.desc
index 58ae31eac85..6cb0a122f1e 100644
--- a/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array-ref-static-values.desc
+++ b/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array-ref-static-values.desc
@@ -1,6 +1,6 @@
-CORE symex-driven-lazy-loading-expected-failure winbug
+CORE symex-driven-lazy-loading-expected-failure
 Test
---function Test.charArrayRef --property "java::Test.charArrayRef:()[C.assertion.2" --static-values static-values.json
+--function Test.charArrayRef --property 'java::Test.charArrayRef:()[C.assertion.2' --static-values static-values.json
 Generated 0 VCC[(]s[)], 0 remaining after simplification
 assertion at file Test.java line 31 .*: SUCCESS
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array-ref.desc b/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array-ref.desc
index 270f1ba198a..4598fef0877 100644
--- a/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array-ref.desc
+++ b/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array-ref.desc
@@ -1,6 +1,6 @@
-CORE symex-driven-lazy-loading-expected-failure winbug
+CORE symex-driven-lazy-loading-expected-failure
 Test
---function Test.charArrayRef --property "java::Test.charArrayRef:()[C.assertion.1"
+--function Test.charArrayRef --property 'java::Test.charArrayRef:()[C.assertion.1'
 Generated 0 VCC[(]s[)], 0 remaining after simplification
 assertion at file Test.java line 29 .*: SUCCESS
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array-static-values.desc b/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array-static-values.desc
index 0371e505376..a31e295710f 100644
--- a/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array-static-values.desc
+++ b/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array-static-values.desc
@@ -1,6 +1,6 @@
-CORE symex-driven-lazy-loading-expected-failure winbug
+CORE symex-driven-lazy-loading-expected-failure
 Test
---function Test.charArray --property "java::Test.charArray:()[C.assertion.2" --static-values static-values.json
+--function Test.charArray --property 'java::Test.charArray:()[C.assertion.2' --static-values static-values.json
 Generated 0 VCC[(]s[)], 0 remaining after simplification
 assertion at file Test.java line 21 .*: SUCCESS
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array1.desc b/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array1.desc
index f2d42d10738..e70aaf0604e 100644
--- a/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array1.desc
+++ b/jbmc/regression/jbmc/array-cell-sensitivity-static-fields/test-char-array1.desc
@@ -1,6 +1,6 @@
-CORE symex-driven-lazy-loading-expected-failure winbug
+CORE symex-driven-lazy-loading-expected-failure
 Test
---function Test.charArray --property "java::Test.charArray:()[C.assertion.1"
+--function Test.charArray --property 'java::Test.charArray:()[C.assertion.1'
 Generated 0 VCC[(]s[)], 0 remaining after simplification
 assertion at file Test.java line 20 .*: SUCCESS
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc/assume-inputs-interval/arg_assume_singleton.desc b/jbmc/regression/jbmc/assume-inputs-interval/arg_assume_singleton.desc
index 2048d525327..cac3205ebdf 100644
--- a/jbmc/regression/jbmc/assume-inputs-interval/arg_assume_singleton.desc
+++ b/jbmc/regression/jbmc/assume-inputs-interval/arg_assume_singleton.desc
@@ -1,6 +1,6 @@
-CORE symex-driven-lazy-loading-expected-failure winbug
+CORE symex-driven-lazy-loading-expected-failure
 My
---function My.intervalUnion --java-assume-inputs-interval [3:3] --property "java::My.intervalUnion:(I)V.assertion.1" --property "java::My.intervalUnion:(I)V.assertion.2" --property "java::My.intervalUnion:(I)V.assertion.3" --property "java::My.intervalUnion:(I)V.assertion.4" --property "java::My.intervalUnion:(I)V.assertion.6"
+--function My.intervalUnion --java-assume-inputs-interval [3:3] --property 'java::My.intervalUnion:(I)V.assertion.1' --property 'java::My.intervalUnion:(I)V.assertion.2' --property 'java::My.intervalUnion:(I)V.assertion.3' --property 'java::My.intervalUnion:(I)V.assertion.4' --property 'java::My.intervalUnion:(I)V.assertion.6'
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/jbmc/regression/jbmc/core-models-required/test.desc b/jbmc/regression/jbmc/core-models-required/test.desc
index 44a36ec8721..3419538db89 100644
--- a/jbmc/regression/jbmc/core-models-required/test.desc
+++ b/jbmc/regression/jbmc/core-models-required/test.desc
@@ -1,6 +1,6 @@
 KNOWNBUG
 HelloWorld
---function "HelloWorld.helloWorld:()Ljava/lang/String;" --context-include wrongpkg
+--function 'HelloWorld.helloWorld:()Ljava/lang/String;' --context-include wrongpkg
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/jbmc/regression/jbmc/enum/test_enum_switch.desc b/jbmc/regression/jbmc/enum/test_enum_switch.desc
index 9a466a34281..be5c5f18f47 100644
--- a/jbmc/regression/jbmc/enum/test_enum_switch.desc
+++ b/jbmc/regression/jbmc/enum/test_enum_switch.desc
@@ -1,6 +1,6 @@
-CORE symex-driven-lazy-loading-expected-failure winbug
+CORE symex-driven-lazy-loading-expected-failure
 Foo
---trace --depth 1024 --java-max-vla-length 16 --max-nondet-string-length 20 --string-printable --unwind 10 --function "Foo.foo" --java-unwind-enum-static
+--trace --depth 1024 --java-max-vla-length 16 --max-nondet-string-length 20 --string-printable --unwind 10 --function 'Foo.foo' --java-unwind-enum-static
 assertion at file Foo.java line 6 .*: FAILURE
 assertion at file Foo.java line 9 .*: FAILURE
 assertion at file Foo.java line 12 .*: FAILURE
diff --git a/jbmc/regression/jbmc/enum/test_enum_values_clone.desc b/jbmc/regression/jbmc/enum/test_enum_values_clone.desc
index 793b3e30e9e..0a854c59bd1 100644
--- a/jbmc/regression/jbmc/enum/test_enum_values_clone.desc
+++ b/jbmc/regression/jbmc/enum/test_enum_values_clone.desc
@@ -1,6 +1,6 @@
 CORE symex-driven-lazy-loading-expected-failure
 EnumIter
---java-max-vla-length 16 --max-nondet-string-length 20 --string-printable --unwind 2 --function "EnumIter.f" --java-unwind-enum-static --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+--java-max-vla-length 16 --max-nondet-string-length 20 --string-printable --unwind 2 --function 'EnumIter.f' --java-unwind-enum-static --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/jbmc/regression/jbmc/enum/test_enum_values_clone_name.desc b/jbmc/regression/jbmc/enum/test_enum_values_clone_name.desc
index 0cec876cc91..e4a8ceb9fa9 100644
--- a/jbmc/regression/jbmc/enum/test_enum_values_clone_name.desc
+++ b/jbmc/regression/jbmc/enum/test_enum_values_clone_name.desc
@@ -1,6 +1,6 @@
 CORE symex-driven-lazy-loading-expected-failure
 EnumIter
---java-max-vla-length 16 --max-nondet-string-length 20 --string-printable --unwind 2 --function "EnumIter.name" --java-unwind-enum-static --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+--java-max-vla-length 16 --max-nondet-string-length 20 --string-printable --unwind 2 --function 'EnumIter.name' --java-unwind-enum-static --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=0$
 ^SIGNAL=0$
 --
diff --git a/jbmc/regression/jbmc/nondet-array-size/test.desc b/jbmc/regression/jbmc/nondet-array-size/test.desc
index 8a4086f1e5a..15cae66a044 100644
--- a/jbmc/regression/jbmc/nondet-array-size/test.desc
+++ b/jbmc/regression/jbmc/nondet-array-size/test.desc
@@ -1,6 +1,6 @@
-CORE winbug
+CORE
 TestClass
---function "TestClass.minimalJbmc" --unwind 5 --max-nondet-string-length 10 --java-unwind-enum-static --trace --json-ui
+--function 'TestClass.minimalJbmc' --unwind 5 --max-nondet-string-length 10 --java-unwind-enum-static --trace --json-ui
 ^EXIT=10$
 ^SIGNAL=0$
 VERIFICATION FAILED
diff --git a/jbmc/regression/jbmc/nondet-static/test.desc b/jbmc/regression/jbmc/nondet-static/test.desc
index 37c7233dac3..decb30736a0 100644
--- a/jbmc/regression/jbmc/nondet-static/test.desc
+++ b/jbmc/regression/jbmc/nondet-static/test.desc
@@ -1,6 +1,6 @@
-CORE symex-driven-lazy-loading-expected-failure winbug
+CORE symex-driven-lazy-loading-expected-failure
 My
---function "My.<init>" --nondet-static --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
+--function 'My.<init>' --nondet-static --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 file My\.java line 104 function java::My\.\<init\>:\(I\)V.*FAILURE$
diff --git a/jbmc/regression/jbmc/parameter-annotation-not-null/test_kotlin.desc b/jbmc/regression/jbmc/parameter-annotation-not-null/test_kotlin.desc
index 419b00fb62c..e8e271e6439 100644
--- a/jbmc/regression/jbmc/parameter-annotation-not-null/test_kotlin.desc
+++ b/jbmc/regression/jbmc/parameter-annotation-not-null/test_kotlin.desc
@@ -1,6 +1,6 @@
-CORE winbug
+CORE
 MainKotlin
---function "MainKotlin.<init>" --show-properties
+--function 'MainKotlin.<init>' --show-properties
 ^EXIT=0$
 ^SIGNAL=0$
 Property java::MainKotlin.<init>:\(Ljava/lang/String;Ljava/lang/String;\)V.not-null-annotation-check.1:
diff --git a/regression/goto-instrument/CMakeLists.txt b/regression/goto-instrument/CMakeLists.txt
index 3508bd9e7c1..f7f08694f6a 100644
--- a/regression/goto-instrument/CMakeLists.txt
+++ b/regression/goto-instrument/CMakeLists.txt
@@ -4,12 +4,6 @@ else()
     set(is_windows false)
 endif()
 
-if("${CMAKE_SYSTEM_NAME}" STREQUAL "Windows")
-  set(exclude_win_broken_tests -X winbug)
-else()
-  set(exclude_win_broken_tests "")
-endif()
-
 add_test_pl_tests(
-    "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-instrument> $<TARGET_FILE:cbmc> ${is_windows}" ${exclude_win_broken_tests}
+    "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-instrument> $<TARGET_FILE:cbmc> ${is_windows}"
 )
diff --git a/regression/goto-instrument/restrict-function-pointer-to-complex-expression/test.desc b/regression/goto-instrument/restrict-function-pointer-to-complex-expression/test.desc
index b0df449e119..f073eea9512 100644
--- a/regression/goto-instrument/restrict-function-pointer-to-complex-expression/test.desc
+++ b/regression/goto-instrument/restrict-function-pointer-to-complex-expression/test.desc
@@ -1,6 +1,6 @@
-CORE winbug
+CORE
 test.c
---restrict-function-pointer "use_fg.function_pointer_call.1/f,g"
+--restrict-function-pointer 'use_fg.function_pointer_call.1/f,g'
 \[use_fg.assertion.2\] line \d+ assertion \(choice \? fptr : gptr\)\(10\) == 10 \+ choice: SUCCESS
 \[use_fg.assertion.1\] line \d+ dereferenced function pointer at use_fg.function_pointer_call.1 must be one of \[(f|g), (f|g)\]: SUCCESS
 ^EXIT=0$
diff --git a/regression/solver-hardness/CMakeLists.txt b/regression/solver-hardness/CMakeLists.txt
index 72b4e1d76c2..e6efa4082c6 100644
--- a/regression/solver-hardness/CMakeLists.txt
+++ b/regression/solver-hardness/CMakeLists.txt
@@ -1,7 +1,2 @@
-if(NOT "${CMAKE_SYSTEM_NAME}" STREQUAL "Windows")
-  add_test_pl_tests(
-    "../chain.sh $<TARGET_FILE:cbmc>")
-else()
-  message(WARNING "solver-hardness/ tests are failing on windows for unknown reasons. An investigation is pending.")
-endif()
-
+add_test_pl_tests(
+  "../chain.sh $<TARGET_FILE:cbmc>")
diff --git a/regression/solver-hardness/solver-hardness-simple/test.desc b/regression/solver-hardness/solver-hardness-simple/test.desc
index 7b6b908d419..27c80a470fb 100644
--- a/regression/solver-hardness/solver-hardness-simple/test.desc
+++ b/regression/solver-hardness/solver-hardness-simple/test.desc
@@ -1,6 +1,6 @@
-CORE winbug
+CORE
 main.c
---write-solver-stats-to "solver_hardness.json"
+--write-solver-stats-to 'solver_hardness.json'
 ^EXIT=10$
 ^SIGNAL=0$
 ^\[main.assertion.\d+\] line \d+ assertion a \+ b \< 10: FAILURE$