Exclude broken tests on windows under jbmc/regression/jbmc-strings/

NlightNFotis · NlightNFotis · commit c9456f2106f9 · 2020-10-05T17:22:15.000+01:00
diff --git a/jbmc/regression/jbmc-strings/CMakeLists.txt b/jbmc/regression/jbmc-strings/CMakeLists.txt
@@ -1,5 +1,11 @@
+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"
+    "$<TARGET_FILE:jbmc> --validate-goto-model --validate-ssa-equation" ${exclude_win_broken_tests}
 )
 
 add_test_pl_profile(
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationCompareTo/test_fail1.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationCompareTo/test_fail1.desc
@@ -1,4 +1,4 @@
-CORE
+CORE winbug
 Main
 --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$
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationCompareTo/test_fail1_vcc.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationCompareTo/test_fail1_vcc.desc
@@ -1,4 +1,4 @@
-CORE
+CORE winbug
 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
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationCompareTo/test_fail2.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationCompareTo/test_fail2.desc
@@ -1,4 +1,4 @@
-CORE
+CORE winbug
 Main
 --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$
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationCompareTo/test_fail2_vcc.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationCompareTo/test_fail2_vcc.desc
@@ -1,4 +1,4 @@
-CORE
+CORE winbug
 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
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationCompareTo/test_fail3.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationCompareTo/test_fail3.desc
@@ -1,4 +1,4 @@
-CORE
+CORE winbug
 Main
 --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$
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationCompareTo/test_fail3_vcc.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationCompareTo/test_fail3_vcc.desc
@@ -1,4 +1,4 @@
-CORE
+CORE winbug
 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
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationCompareTo/test_fail4.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationCompareTo/test_fail4.desc
@@ -1,4 +1,4 @@
-CORE
+CORE winbug
 Main
 --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$
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationCompareTo/test_fail4_vcc.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationCompareTo/test_fail4_vcc.desc
@@ -1,4 +1,4 @@
-CORE
+CORE winbug
 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
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationEndsWith/test_fail.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationEndsWith/test_fail.desc
@@ -1,4 +1,4 @@
-CORE
+CORE winbug
 Main
 --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$
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationEndsWith/test_fail_vcc.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationEndsWith/test_fail_vcc.desc
@@ -1,4 +1,4 @@
-CORE
+CORE winbug
 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
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationEndsWith/test_pass.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationEndsWith/test_pass.desc
@@ -1,4 +1,4 @@
-CORE
+CORE winbug
 Main
 --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
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationIsEmpty/test_fail.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationIsEmpty/test_fail.desc
@@ -1,4 +1,4 @@
-CORE
+CORE winbug
 Main
 --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$
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationIsEmpty/test_fail_vcc.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationIsEmpty/test_fail_vcc.desc
@@ -1,4 +1,4 @@
-CORE
+CORE winbug
 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" 
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationIsEmpty/test_pass.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationIsEmpty/test_pass.desc
@@ -1,4 +1,4 @@
-CORE
+CORE winbug
 Main
 --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$
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend01/test.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend01/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE winbug
 Main
 --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$
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend02-WithEmptyString/test1.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend02-WithEmptyString/test1.desc
@@ -1,4 +1,4 @@
-CORE
+CORE winbug
 Main
 --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$
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend02-WithEmptyString/test2.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend02-WithEmptyString/test2.desc
@@ -1,4 +1,4 @@
-CORE
+CORE winbug
 Main
 --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$
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend02-WithEmptyString/test3.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringBuilderAppend02-WithEmptyString/test3.desc
@@ -1,4 +1,4 @@
-CORE
+CORE winbug
 Main
 --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$
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation01/test.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation01/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE winbug
 Main
 --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$
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation02-WithEmptyString/test1.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation02-WithEmptyString/test1.desc
@@ -1,4 +1,4 @@
-CORE
+CORE winbug
 Main
 --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$
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation02-WithEmptyString/test2.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation02-WithEmptyString/test2.desc
@@ -1,4 +1,4 @@
-CORE
+CORE winbug
 Main
 --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$
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation02-WithEmptyString/test3.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation02-WithEmptyString/test3.desc
@@ -1,4 +1,4 @@
-CORE
+CORE winbug
 Main
 --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$
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation03-NegativeScenarios/test1.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation03-NegativeScenarios/test1.desc
@@ -1,4 +1,4 @@
-CORE symex-driven-lazy-loading-expected-failure
+CORE symex-driven-lazy-loading-expected-failure winbug
 Main
 --function Main.test1 --property "java::Main.test1:(Ljava/lang/String;)V.assertion.1"
 ^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation03-NegativeScenarios/test2.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation03-NegativeScenarios/test2.desc
@@ -1,4 +1,4 @@
-CORE symex-driven-lazy-loading-expected-failure
+CORE symex-driven-lazy-loading-expected-failure winbug
 Main
 --function Main.test2 --property "java::Main.test2:(Ljava/lang/String;)V.assertion.1"
 ^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation03-NegativeScenarios/test3.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation03-NegativeScenarios/test3.desc
@@ -1,4 +1,4 @@
-CORE symex-driven-lazy-loading-expected-failure
+CORE symex-driven-lazy-loading-expected-failure winbug
 Main
 --function Main.test3 --property "java::Main.test3:(Ljava/lang/String;)V.assertion.1"
 ^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation04-StringEqual/test.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation04-StringEqual/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE winbug
 Main
 --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$
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation06-2byteChar/test.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation06-2byteChar/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE winbug
 Main
 --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$
diff --git a/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation07-NonPrintableChar/test.desc b/jbmc/regression/jbmc-strings/ConstantEvaluationStringConcatenation07-NonPrintableChar/test.desc
@@ -1,4 +1,4 @@
-CORE
+CORE winbug
 Main
 --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$
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation03-IndexOutOfRange/test.desc b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation03-IndexOutOfRange/test.desc
@@ -1,4 +1,4 @@
-CORE symex-driven-lazy-loading-expected-failure
+CORE symex-driven-lazy-loading-expected-failure winbug
 Main
 --function Main.constantIndexOf --property "java::Main.constantIndexOf:(Ljava/lang/String;)V.assertion.1"
 ^Generated [0-9]+ VCC\(s\), 0 remaining after simplification$
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test1.desc b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test1.desc
@@ -1,4 +1,4 @@
-CORE symex-driven-lazy-loading-expected-failure
+CORE symex-driven-lazy-loading-expected-failure winbug
 Main
 --function Main.constantIndexOf --property "java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.1" --show-vcc
 ^Generated 1 VCC\(s\), 1 remaining after simplification$
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test10.desc b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test10.desc
@@ -1,4 +1,4 @@
-CORE symex-driven-lazy-loading-expected-failure
+CORE symex-driven-lazy-loading-expected-failure winbug
 Main
 --function Main.constantIndexOf --property "java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.10" --show-vcc
 ^Generated 1 VCC\(s\), 1 remaining after simplification$
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test11.desc b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test11.desc
@@ -1,4 +1,4 @@
-CORE symex-driven-lazy-loading-expected-failure
+CORE symex-driven-lazy-loading-expected-failure winbug
 Main
 --function Main.constantIndexOf --property "java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.11" --show-vcc
 ^Generated 1 VCC\(s\), 1 remaining after simplification$
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test12.desc b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test12.desc
@@ -1,4 +1,4 @@
-CORE symex-driven-lazy-loading-expected-failure
+CORE symex-driven-lazy-loading-expected-failure winbug
 Main
 --function Main.constantIndexOf --property "java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.12" --show-vcc
 ^Generated 1 VCC\(s\), 1 remaining after simplification$
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test2.desc b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test2.desc
@@ -1,4 +1,4 @@
-CORE symex-driven-lazy-loading-expected-failure
+CORE symex-driven-lazy-loading-expected-failure winbug
 Main
 --function Main.constantIndexOf --property "java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.2" --show-vcc
 ^Generated 1 VCC\(s\), 1 remaining after simplification$
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test3.desc b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test3.desc
@@ -1,4 +1,4 @@
-CORE symex-driven-lazy-loading-expected-failure
+CORE symex-driven-lazy-loading-expected-failure winbug
 Main
 --function Main.constantIndexOf --property "java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.3" --show-vcc
 ^Generated 1 VCC\(s\), 1 remaining after simplification$
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test4.desc b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test4.desc
@@ -1,4 +1,4 @@
-CORE symex-driven-lazy-loading-expected-failure
+CORE symex-driven-lazy-loading-expected-failure winbug
 Main
 --function Main.constantIndexOf --property "java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.4" --show-vcc
 ^Generated 1 VCC\(s\), 1 remaining after simplification$
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test5.desc b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test5.desc
@@ -1,4 +1,4 @@
-CORE symex-driven-lazy-loading-expected-failure
+CORE symex-driven-lazy-loading-expected-failure winbug
 Main
 --function Main.constantIndexOf --property "java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.5" --show-vcc
 ^Generated 1 VCC\(s\), 1 remaining after simplification$
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test6.desc b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test6.desc
@@ -1,4 +1,4 @@
-CORE symex-driven-lazy-loading-expected-failure
+CORE symex-driven-lazy-loading-expected-failure winbug
 Main
 --function Main.constantIndexOf --property "java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.6" --show-vcc
 ^Generated 1 VCC\(s\), 1 remaining after simplification$
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test7.desc b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test7.desc
@@ -1,4 +1,4 @@
-CORE symex-driven-lazy-loading-expected-failure
+CORE symex-driven-lazy-loading-expected-failure winbug
 Main
 --function Main.constantIndexOf --property "java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.7" --show-vcc
 ^Generated 1 VCC\(s\), 1 remaining after simplification$
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test8.desc b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test8.desc
@@ -1,4 +1,4 @@
-CORE symex-driven-lazy-loading-expected-failure
+CORE symex-driven-lazy-loading-expected-failure winbug
 Main
 --function Main.constantIndexOf --property "java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.8" --show-vcc
 ^Generated 1 VCC\(s\), 1 remaining after simplification$
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test9.desc b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation04-NegativeScenarios/test9.desc
@@ -1,4 +1,4 @@
-CORE symex-driven-lazy-loading-expected-failure
+CORE symex-driven-lazy-loading-expected-failure winbug
 Main
 --function Main.constantIndexOf --property "java::Main.constantIndexOf:(Ljava/lang/String;CI)V.assertion.9" --show-vcc
 ^Generated 1 VCC\(s\), 1 remaining after simplification$
diff --git a/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation06-AssertionFailure/test.desc b/jbmc/regression/jbmc-strings/IndexOfConstantEvaluation06-AssertionFailure/test.desc
@@ -1,4 +1,4 @@
-CORE symex-driven-lazy-loading-expected-failure
+CORE symex-driven-lazy-loading-expected-failure winbug
 Main
 --function Main.constantIndexOf --property "java::Main.constantIndexOf:()V.assertion.1"
 ^Generated [0-9]+ VCC\(s\), 1 remaining after simplification$
diff --git a/jbmc/regression/jbmc-strings/StringBuilderAppend03/test1.desc b/jbmc/regression/jbmc-strings/StringBuilderAppend03/test1.desc
@@ -1,4 +1,4 @@
-CORE
+CORE winbug
 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"
 ^EXIT=10$
diff --git a/jbmc/regression/jbmc-strings/StringBuilderAppend03/test2.desc b/jbmc/regression/jbmc-strings/StringBuilderAppend03/test2.desc
@@ -1,4 +1,4 @@
-CORE
+CORE winbug
 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"
 ^EXIT=10$
diff --git a/jbmc/regression/jbmc-strings/StringBuilderAppend03/test3.desc b/jbmc/regression/jbmc-strings/StringBuilderAppend03/test3.desc
@@ -1,4 +1,4 @@
-CORE symex-driven-lazy-loading-expected-failure
+CORE symex-driven-lazy-loading-expected-failure winbug
 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"
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-strings/StringBuilderSubstringConstantEvaluation2/test1.desc b/jbmc/regression/jbmc-strings/StringBuilderSubstringConstantEvaluation2/test1.desc
@@ -1,4 +1,4 @@
-CORE symex-driven-lazy-loading-expected-failure
+CORE symex-driven-lazy-loading-expected-failure winbug
 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"
 ^Generated 1 VCC\(s\), 1 remaining after simplification$
diff --git a/jbmc/regression/jbmc-strings/StringBuilderSubstringConstantEvaluation2/test2.desc b/jbmc/regression/jbmc-strings/StringBuilderSubstringConstantEvaluation2/test2.desc
@@ -1,4 +1,4 @@
-CORE symex-driven-lazy-loading-expected-failure
+CORE symex-driven-lazy-loading-expected-failure winbug
 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"
 ^Generated 1 VCC\(s\), 1 remaining after simplification$
diff --git a/jbmc/regression/jbmc-strings/StringBuilderSubstringConstantEvaluation2/test3.desc b/jbmc/regression/jbmc-strings/StringBuilderSubstringConstantEvaluation2/test3.desc
@@ -1,4 +1,4 @@
-CORE symex-driven-lazy-loading-expected-failure
+CORE symex-driven-lazy-loading-expected-failure winbug
 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"
 ^Generated 1 VCC\(s\), 1 remaining after simplification$
diff --git a/jbmc/regression/jbmc-strings/StringCompareTo/testFail1.desc b/jbmc/regression/jbmc-strings/StringCompareTo/testFail1.desc
@@ -1,4 +1,4 @@
-CORE symex-driven-lazy-loading-expected-failure
+CORE symex-driven-lazy-loading-expected-failure winbug
 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" 
 ^EXIT=10$
diff --git a/jbmc/regression/jbmc-strings/StringCompareTo/testFail2.desc b/jbmc/regression/jbmc-strings/StringCompareTo/testFail2.desc
@@ -1,4 +1,4 @@
-CORE symex-driven-lazy-loading-expected-failure
+CORE symex-driven-lazy-loading-expected-failure winbug
 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" 
 ^EXIT=10$
diff --git a/jbmc/regression/jbmc-strings/StringCompareTo/testFail3.desc b/jbmc/regression/jbmc-strings/StringCompareTo/testFail3.desc
@@ -1,4 +1,4 @@
-CORE symex-driven-lazy-loading-expected-failure
+CORE symex-driven-lazy-loading-expected-failure winbug
 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" 
 ^EXIT=10$
diff --git a/jbmc/regression/jbmc-strings/StringCompareTo/testFail4.desc b/jbmc/regression/jbmc-strings/StringCompareTo/testFail4.desc
@@ -1,4 +1,4 @@
-CORE symex-driven-lazy-loading-expected-failure
+CORE symex-driven-lazy-loading-expected-failure winbug
 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" 
 ^EXIT=10$
diff --git a/jbmc/regression/jbmc-strings/StringCompareTo/testFail5.desc b/jbmc/regression/jbmc-strings/StringCompareTo/testFail5.desc
@@ -1,4 +1,4 @@
-CORE symex-driven-lazy-loading-expected-failure
+CORE symex-driven-lazy-loading-expected-failure winbug
 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" 
 ^EXIT=10$
diff --git a/jbmc/regression/jbmc-strings/StringCompareTo/testFail6.desc b/jbmc/regression/jbmc-strings/StringCompareTo/testFail6.desc
@@ -1,4 +1,4 @@
-CORE symex-driven-lazy-loading-expected-failure
+CORE symex-driven-lazy-loading-expected-failure winbug
 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" 
 ^EXIT=10$
diff --git a/jbmc/regression/jbmc-strings/StringCompareTo/testPass1.desc b/jbmc/regression/jbmc-strings/StringCompareTo/testPass1.desc
@@ -1,4 +1,4 @@
-CORE symex-driven-lazy-loading-expected-failure
+CORE symex-driven-lazy-loading-expected-failure winbug
 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" 
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-strings/StringCompareTo/testPass2.desc b/jbmc/regression/jbmc-strings/StringCompareTo/testPass2.desc
@@ -1,4 +1,4 @@
-CORE symex-driven-lazy-loading-expected-failure
+CORE symex-driven-lazy-loading-expected-failure winbug
 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" 
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-strings/StringCompareTo/testPass3.desc b/jbmc/regression/jbmc-strings/StringCompareTo/testPass3.desc
@@ -1,4 +1,4 @@
-CORE symex-driven-lazy-loading-expected-failure
+CORE symex-driven-lazy-loading-expected-failure winbug
 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" 
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-strings/StringCompareTo/testPass4.desc b/jbmc/regression/jbmc-strings/StringCompareTo/testPass4.desc
@@ -1,4 +1,4 @@
-CORE symex-driven-lazy-loading-expected-failure
+CORE symex-driven-lazy-loading-expected-failure winbug
 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" 
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-strings/StringCompareTo/testPass5.desc b/jbmc/regression/jbmc-strings/StringCompareTo/testPass5.desc
@@ -1,4 +1,4 @@
-CORE symex-driven-lazy-loading-expected-failure
+CORE symex-driven-lazy-loading-expected-failure winbug
 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" 
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-strings/StringCompareTo/testPass6.desc b/jbmc/regression/jbmc-strings/StringCompareTo/testPass6.desc
@@ -1,4 +1,4 @@
-CORE symex-driven-lazy-loading-expected-failure
+CORE symex-driven-lazy-loading-expected-failure winbug
 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" 
 ^EXIT=0$
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
@@ -1,4 +1,4 @@
-CORE
+CORE winbug
 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"
 ^EXIT=10$
diff --git a/jbmc/regression/jbmc-strings/StringFormatBool/test-bool-length1.desc b/jbmc/regression/jbmc-strings/StringFormatBool/test-bool-length1.desc
@@ -1,4 +1,4 @@
-CORE
+CORE winbug
 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"
 ^EXIT=10$
diff --git a/jbmc/regression/jbmc-strings/StringFormatBool/test-bool-length2.desc b/jbmc/regression/jbmc-strings/StringFormatBool/test-bool-length2.desc
@@ -1,4 +1,4 @@
-CORE
+CORE winbug
 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"
 ^EXIT=10$
diff --git a/jbmc/regression/jbmc-strings/StringFormatBool/test-bool-length3.desc b/jbmc/regression/jbmc-strings/StringFormatBool/test-bool-length3.desc
@@ -1,4 +1,4 @@
-CORE symex-driven-lazy-loading-expected-failure
+CORE symex-driven-lazy-loading-expected-failure winbug
 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"
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-strings/StringFormatBool/test-bool1.desc b/jbmc/regression/jbmc-strings/StringFormatBool/test-bool1.desc
diff --git a/jbmc/regression/jbmc-strings/StringFormatBool/test-bool2.desc b/jbmc/regression/jbmc-strings/StringFormatBool/test-bool2.desc
diff --git a/jbmc/regression/jbmc-strings/StringFormatBool/test-bool3.desc b/jbmc/regression/jbmc-strings/StringFormatBool/test-bool3.desc
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
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
diff --git a/jbmc/regression/jbmc-strings/StringFormatHex/test-hex1.desc b/jbmc/regression/jbmc-strings/StringFormatHex/test-hex1.desc
diff --git a/jbmc/regression/jbmc-strings/StringFormatHex/test-hex2.desc b/jbmc/regression/jbmc-strings/StringFormatHex/test-hex2.desc
diff --git a/jbmc/regression/jbmc-strings/StringFormatHex/test-hex3.desc b/jbmc/regression/jbmc-strings/StringFormatHex/test-hex3.desc
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
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
diff --git a/jbmc/regression/jbmc-strings/StringFormatInt/test-int-length.desc b/jbmc/regression/jbmc-strings/StringFormatInt/test-int-length.desc
diff --git a/jbmc/regression/jbmc-strings/StringFormatInt/test-int1.desc b/jbmc/regression/jbmc-strings/StringFormatInt/test-int1.desc
diff --git a/jbmc/regression/jbmc-strings/StringFormatInt/test-int2.desc b/jbmc/regression/jbmc-strings/StringFormatInt/test-int2.desc
diff --git a/jbmc/regression/jbmc-strings/StringFormatInt/test-int3.desc b/jbmc/regression/jbmc-strings/StringFormatInt/test-int3.desc
diff --git a/jbmc/regression/jbmc-strings/StringFormatSpecial/test-newline-fail.desc b/jbmc/regression/jbmc-strings/StringFormatSpecial/test-newline-fail.desc
diff --git a/jbmc/regression/jbmc-strings/StringFormatSpecial/test-newline-length-fail.desc b/jbmc/regression/jbmc-strings/StringFormatSpecial/test-newline-length-fail.desc
diff --git a/jbmc/regression/jbmc-strings/StringFormatSpecial/test-newline-length-pass.desc b/jbmc/regression/jbmc-strings/StringFormatSpecial/test-newline-length-pass.desc
diff --git a/jbmc/regression/jbmc-strings/StringFormatSpecial/test-newline-pass.desc b/jbmc/regression/jbmc-strings/StringFormatSpecial/test-newline-pass.desc
diff --git a/jbmc/regression/jbmc-strings/StringFormatSpecial/test-percent-fail.desc b/jbmc/regression/jbmc-strings/StringFormatSpecial/test-percent-fail.desc
diff --git a/jbmc/regression/jbmc-strings/StringFormatSpecial/test-percent-length-fail.desc b/jbmc/regression/jbmc-strings/StringFormatSpecial/test-percent-length-fail.desc
diff --git a/jbmc/regression/jbmc-strings/StringFormatSpecial/test-percent-length-pass.desc b/jbmc/regression/jbmc-strings/StringFormatSpecial/test-percent-length-pass.desc
diff --git a/jbmc/regression/jbmc-strings/StringFormatSpecial/test-percent-pass.desc b/jbmc/regression/jbmc-strings/StringFormatSpecial/test-percent-pass.desc
diff --git a/jbmc/regression/jbmc-strings/StringFormatString/test-string2.desc b/jbmc/regression/jbmc-strings/StringFormatString/test-string2.desc
diff --git a/jbmc/regression/jbmc-strings/StringFormatString/test-string3.desc b/jbmc/regression/jbmc-strings/StringFormatString/test-string3.desc
diff --git a/jbmc/regression/jbmc-strings/StringSubstringConstantEvaluation2/test1.desc b/jbmc/regression/jbmc-strings/StringSubstringConstantEvaluation2/test1.desc
diff --git a/jbmc/regression/jbmc-strings/StringSubstringConstantEvaluation2/test2.desc b/jbmc/regression/jbmc-strings/StringSubstringConstantEvaluation2/test2.desc
diff --git a/jbmc/regression/jbmc-strings/StringSubstringConstantEvaluation2/test3.desc b/jbmc/regression/jbmc-strings/StringSubstringConstantEvaluation2/test3.desc
diff --git a/jbmc/regression/jbmc-strings/string-input-value/test1.desc b/jbmc/regression/jbmc-strings/string-input-value/test1.desc

Original file line number	Diff line number	Diff line change
`@@ -1,4 +1,4 @@`
`1`		`-CORE`
	`1`	`+CORE winbug`
`2`	`2`	`Main`
`3`	`3`	--function Main.constantCompareToFail1 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar` --property "java::Main.constantCompareToFail1:()V.assertion.1"
`4`	`4`	`^VERIFICATION FAILED$`