diff --git a/regression/cbmc-cpp/Address_of_Method1/test.desc b/regression/cbmc-cpp/Address_of_Method1/test.desc
index 7791be248c7..af1345b7343 100644
--- a/regression/cbmc-cpp/Address_of_Method1/test.desc
+++ b/regression/cbmc-cpp/Address_of_Method1/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG winbug macos-assert-broken
+KNOWNBUG macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Anonymous_members1/test.desc b/regression/cbmc-cpp/Anonymous_members1/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Anonymous_members1/test.desc
+++ b/regression/cbmc-cpp/Anonymous_members1/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Assignment1/test.desc b/regression/cbmc-cpp/Assignment1/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Assignment1/test.desc
+++ b/regression/cbmc-cpp/Assignment1/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/CMakeLists.txt b/regression/cbmc-cpp/CMakeLists.txt
index 84f3b2328c7..e9280edac73 100644
--- a/regression/cbmc-cpp/CMakeLists.txt
+++ b/regression/cbmc-cpp/CMakeLists.txt
@@ -4,12 +4,6 @@ else()
   set(gcc_only "")
 endif()
 
-if("${CMAKE_SYSTEM_NAME}" STREQUAL "Windows")
-  set(exclude_win_broken_tests -X winbug)
-else()
-  set(exclude_win_broken_tests "")
-endif()
-
 if("${CMAKE_SYSTEM_NAME}" STREQUAL "Darwin")
   set(exclude_mac_broken_tests -X macos-assert-broken)
 else()
@@ -17,5 +11,5 @@ else()
 endif()
 
 add_test_pl_tests(
-    "$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation" ${gcc_only} ${exclude_win_broken_tests} ${exclude_mac_broken_tests}
+    "$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation" ${gcc_only} ${exclude_mac_broken_tests}
 )
diff --git a/regression/cbmc-cpp/Class_Members1/test.desc b/regression/cbmc-cpp/Class_Members1/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Class_Members1/test.desc
+++ b/regression/cbmc-cpp/Class_Members1/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Comma_Operator1/test.desc b/regression/cbmc-cpp/Comma_Operator1/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Comma_Operator1/test.desc
+++ b/regression/cbmc-cpp/Comma_Operator1/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/ConditionalExpression1/test.desc b/regression/cbmc-cpp/ConditionalExpression1/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/ConditionalExpression1/test.desc
+++ b/regression/cbmc-cpp/ConditionalExpression1/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/ConditionalExpression2/test.desc b/regression/cbmc-cpp/ConditionalExpression2/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/ConditionalExpression2/test.desc
+++ b/regression/cbmc-cpp/ConditionalExpression2/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Constructor1/test.desc b/regression/cbmc-cpp/Constructor1/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Constructor1/test.desc
+++ b/regression/cbmc-cpp/Constructor1/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Constructor12/test.desc b/regression/cbmc-cpp/Constructor12/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Constructor12/test.desc
+++ b/regression/cbmc-cpp/Constructor12/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Constructor13/test.desc b/regression/cbmc-cpp/Constructor13/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Constructor13/test.desc
+++ b/regression/cbmc-cpp/Constructor13/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Constructor2/test.desc b/regression/cbmc-cpp/Constructor2/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Constructor2/test.desc
+++ b/regression/cbmc-cpp/Constructor2/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Constructor3/test.desc b/regression/cbmc-cpp/Constructor3/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Constructor3/test.desc
+++ b/regression/cbmc-cpp/Constructor3/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Constructor4/test.desc b/regression/cbmc-cpp/Constructor4/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Constructor4/test.desc
+++ b/regression/cbmc-cpp/Constructor4/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Constructor5/test.desc b/regression/cbmc-cpp/Constructor5/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Constructor5/test.desc
+++ b/regression/cbmc-cpp/Constructor5/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Constructor6/test.desc b/regression/cbmc-cpp/Constructor6/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Constructor6/test.desc
+++ b/regression/cbmc-cpp/Constructor6/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Constructor9/test.desc b/regression/cbmc-cpp/Constructor9/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Constructor9/test.desc
+++ b/regression/cbmc-cpp/Constructor9/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Conversion5/test.desc b/regression/cbmc-cpp/Conversion5/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Conversion5/test.desc
+++ b/regression/cbmc-cpp/Conversion5/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Conversion6/test.desc b/regression/cbmc-cpp/Conversion6/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Conversion6/test.desc
+++ b/regression/cbmc-cpp/Conversion6/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Conversion_Operator2/test.desc b/regression/cbmc-cpp/Conversion_Operator2/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Conversion_Operator2/test.desc
+++ b/regression/cbmc-cpp/Conversion_Operator2/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Conversion_Operator3/test.desc b/regression/cbmc-cpp/Conversion_Operator3/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Conversion_Operator3/test.desc
+++ b/regression/cbmc-cpp/Conversion_Operator3/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Conversion_Operator4/test.desc b/regression/cbmc-cpp/Conversion_Operator4/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Conversion_Operator4/test.desc
+++ b/regression/cbmc-cpp/Conversion_Operator4/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Default_Arguments1/test.desc b/regression/cbmc-cpp/Default_Arguments1/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Default_Arguments1/test.desc
+++ b/regression/cbmc-cpp/Default_Arguments1/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Default_Arguments2/test.desc b/regression/cbmc-cpp/Default_Arguments2/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Default_Arguments2/test.desc
+++ b/regression/cbmc-cpp/Default_Arguments2/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Destructor_with_PtrMember/test.desc b/regression/cbmc-cpp/Destructor_with_PtrMember/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Destructor_with_PtrMember/test.desc
+++ b/regression/cbmc-cpp/Destructor_with_PtrMember/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Float1/test.desc b/regression/cbmc-cpp/Float1/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Float1/test.desc
+++ b/regression/cbmc-cpp/Float1/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Friend5/test.desc b/regression/cbmc-cpp/Friend5/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Friend5/test.desc
+++ b/regression/cbmc-cpp/Friend5/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Function_Arguments2/test.desc b/regression/cbmc-cpp/Function_Arguments2/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Function_Arguments2/test.desc
+++ b/regression/cbmc-cpp/Function_Arguments2/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Function_Arguments5/test.desc b/regression/cbmc-cpp/Function_Arguments5/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Function_Arguments5/test.desc
+++ b/regression/cbmc-cpp/Function_Arguments5/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Function_Pointer1/test.desc b/regression/cbmc-cpp/Function_Pointer1/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Function_Pointer1/test.desc
+++ b/regression/cbmc-cpp/Function_Pointer1/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Implicit_Conversion1/test.desc b/regression/cbmc-cpp/Implicit_Conversion1/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Implicit_Conversion1/test.desc
+++ b/regression/cbmc-cpp/Implicit_Conversion1/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Implicit_Conversion4/test.desc b/regression/cbmc-cpp/Implicit_Conversion4/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Implicit_Conversion4/test.desc
+++ b/regression/cbmc-cpp/Implicit_Conversion4/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Implicit_Conversion6/test.desc b/regression/cbmc-cpp/Implicit_Conversion6/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Implicit_Conversion6/test.desc
+++ b/regression/cbmc-cpp/Implicit_Conversion6/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Implicit_Conversion7/test.desc b/regression/cbmc-cpp/Implicit_Conversion7/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Implicit_Conversion7/test.desc
+++ b/regression/cbmc-cpp/Implicit_Conversion7/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Inheritance1/test.desc b/regression/cbmc-cpp/Inheritance1/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Inheritance1/test.desc
+++ b/regression/cbmc-cpp/Inheritance1/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Inheritance3/test.desc b/regression/cbmc-cpp/Inheritance3/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Inheritance3/test.desc
+++ b/regression/cbmc-cpp/Inheritance3/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Inheritance4/test.desc b/regression/cbmc-cpp/Inheritance4/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Inheritance4/test.desc
+++ b/regression/cbmc-cpp/Inheritance4/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Initializer1/test.desc b/regression/cbmc-cpp/Initializer1/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Initializer1/test.desc
+++ b/regression/cbmc-cpp/Initializer1/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Label0/test.desc b/regression/cbmc-cpp/Label0/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Label0/test.desc
+++ b/regression/cbmc-cpp/Label0/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Linking1/test.desc b/regression/cbmc-cpp/Linking1/test.desc
index 49ced91341b..4c1cb5611fa 100644
--- a/regression/cbmc-cpp/Linking1/test.desc
+++ b/regression/cbmc-cpp/Linking1/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 module.cpp
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Makefile b/regression/cbmc-cpp/Makefile
index 790f788c5da..febf12571a3 100644
--- a/regression/cbmc-cpp/Makefile
+++ b/regression/cbmc-cpp/Makefile
@@ -4,7 +4,7 @@ include ../../src/config.inc
 include ../../src/common
 
 ifeq ($(BUILD_ENV_),MSVC)
-	excluded_tests = -X gcc-only -X winbug
+	excluded_tests = -X gcc-only
 else
 ifeq ($(BUILD_ENV_),OSX)
 	# In MacOS, a change in the assert.h header file
diff --git a/regression/cbmc-cpp/Member_Access_in_Class/test.desc b/regression/cbmc-cpp/Member_Access_in_Class/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Member_Access_in_Class/test.desc
+++ b/regression/cbmc-cpp/Member_Access_in_Class/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Mutable1/test.desc b/regression/cbmc-cpp/Mutable1/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Mutable1/test.desc
+++ b/regression/cbmc-cpp/Mutable1/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Overloading_Functions1/test.desc b/regression/cbmc-cpp/Overloading_Functions1/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Overloading_Functions1/test.desc
+++ b/regression/cbmc-cpp/Overloading_Functions1/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Overloading_Functions3/test.desc b/regression/cbmc-cpp/Overloading_Functions3/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Overloading_Functions3/test.desc
+++ b/regression/cbmc-cpp/Overloading_Functions3/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Overloading_Increment1/test.desc b/regression/cbmc-cpp/Overloading_Increment1/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Overloading_Increment1/test.desc
+++ b/regression/cbmc-cpp/Overloading_Increment1/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Overloading_Members1/test.desc b/regression/cbmc-cpp/Overloading_Members1/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Overloading_Members1/test.desc
+++ b/regression/cbmc-cpp/Overloading_Members1/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Overloading_Operators12/test.desc b/regression/cbmc-cpp/Overloading_Operators12/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Overloading_Operators12/test.desc
+++ b/regression/cbmc-cpp/Overloading_Operators12/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Overloading_Operators13/test.desc b/regression/cbmc-cpp/Overloading_Operators13/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Overloading_Operators13/test.desc
+++ b/regression/cbmc-cpp/Overloading_Operators13/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Overloading_Operators2/test.desc b/regression/cbmc-cpp/Overloading_Operators2/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Overloading_Operators2/test.desc
+++ b/regression/cbmc-cpp/Overloading_Operators2/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Overloading_Operators7/test.desc b/regression/cbmc-cpp/Overloading_Operators7/test.desc
index 7791be248c7..af1345b7343 100644
--- a/regression/cbmc-cpp/Overloading_Operators7/test.desc
+++ b/regression/cbmc-cpp/Overloading_Operators7/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG winbug macos-assert-broken
+KNOWNBUG macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Overloading_Operators8/test.desc b/regression/cbmc-cpp/Overloading_Operators8/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Overloading_Operators8/test.desc
+++ b/regression/cbmc-cpp/Overloading_Operators8/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Pointer_Conversion2/test.desc b/regression/cbmc-cpp/Pointer_Conversion2/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Pointer_Conversion2/test.desc
+++ b/regression/cbmc-cpp/Pointer_Conversion2/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Protection2/test.desc b/regression/cbmc-cpp/Protection2/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Protection2/test.desc
+++ b/regression/cbmc-cpp/Protection2/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Qualifier2/test.desc b/regression/cbmc-cpp/Qualifier2/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Qualifier2/test.desc
+++ b/regression/cbmc-cpp/Qualifier2/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Reference2/test.desc b/regression/cbmc-cpp/Reference2/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Reference2/test.desc
+++ b/regression/cbmc-cpp/Reference2/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Reference3/test.desc b/regression/cbmc-cpp/Reference3/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Reference3/test.desc
+++ b/regression/cbmc-cpp/Reference3/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Reference6/test.desc b/regression/cbmc-cpp/Reference6/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Reference6/test.desc
+++ b/regression/cbmc-cpp/Reference6/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Reference7/test.desc b/regression/cbmc-cpp/Reference7/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Reference7/test.desc
+++ b/regression/cbmc-cpp/Reference7/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Resolver6/test.desc b/regression/cbmc-cpp/Resolver6/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Resolver6/test.desc
+++ b/regression/cbmc-cpp/Resolver6/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Resolver7/test.desc b/regression/cbmc-cpp/Resolver7/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Resolver7/test.desc
+++ b/regression/cbmc-cpp/Resolver7/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Resolver8/test.desc b/regression/cbmc-cpp/Resolver8/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Resolver8/test.desc
+++ b/regression/cbmc-cpp/Resolver8/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Static_Method1/test.desc b/regression/cbmc-cpp/Static_Method1/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Static_Method1/test.desc
+++ b/regression/cbmc-cpp/Static_Method1/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/String_Literal1/test.desc b/regression/cbmc-cpp/String_Literal1/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/String_Literal1/test.desc
+++ b/regression/cbmc-cpp/String_Literal1/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Templates10/test.desc b/regression/cbmc-cpp/Templates10/test.desc
index 7791be248c7..af1345b7343 100644
--- a/regression/cbmc-cpp/Templates10/test.desc
+++ b/regression/cbmc-cpp/Templates10/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG winbug macos-assert-broken
+KNOWNBUG macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Templates11/test.desc b/regression/cbmc-cpp/Templates11/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Templates11/test.desc
+++ b/regression/cbmc-cpp/Templates11/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Templates12/test.desc b/regression/cbmc-cpp/Templates12/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Templates12/test.desc
+++ b/regression/cbmc-cpp/Templates12/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Templates13/test.desc b/regression/cbmc-cpp/Templates13/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Templates13/test.desc
+++ b/regression/cbmc-cpp/Templates13/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Templates14/test.desc b/regression/cbmc-cpp/Templates14/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Templates14/test.desc
+++ b/regression/cbmc-cpp/Templates14/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Templates16/test.desc b/regression/cbmc-cpp/Templates16/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Templates16/test.desc
+++ b/regression/cbmc-cpp/Templates16/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Templates19/test.desc b/regression/cbmc-cpp/Templates19/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Templates19/test.desc
+++ b/regression/cbmc-cpp/Templates19/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Templates20/test.desc b/regression/cbmc-cpp/Templates20/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Templates20/test.desc
+++ b/regression/cbmc-cpp/Templates20/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Templates21/test.desc b/regression/cbmc-cpp/Templates21/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Templates21/test.desc
+++ b/regression/cbmc-cpp/Templates21/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Templates22/test.desc b/regression/cbmc-cpp/Templates22/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Templates22/test.desc
+++ b/regression/cbmc-cpp/Templates22/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Templates23/test.desc b/regression/cbmc-cpp/Templates23/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Templates23/test.desc
+++ b/regression/cbmc-cpp/Templates23/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Templates24/test.desc b/regression/cbmc-cpp/Templates24/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Templates24/test.desc
+++ b/regression/cbmc-cpp/Templates24/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Templates25/test.desc b/regression/cbmc-cpp/Templates25/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Templates25/test.desc
+++ b/regression/cbmc-cpp/Templates25/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Templates26/test.desc b/regression/cbmc-cpp/Templates26/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Templates26/test.desc
+++ b/regression/cbmc-cpp/Templates26/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Templates27/test.desc b/regression/cbmc-cpp/Templates27/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Templates27/test.desc
+++ b/regression/cbmc-cpp/Templates27/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Templates28/test.desc b/regression/cbmc-cpp/Templates28/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Templates28/test.desc
+++ b/regression/cbmc-cpp/Templates28/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Templates3/test.desc b/regression/cbmc-cpp/Templates3/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Templates3/test.desc
+++ b/regression/cbmc-cpp/Templates3/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Templates30/test.desc b/regression/cbmc-cpp/Templates30/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Templates30/test.desc
+++ b/regression/cbmc-cpp/Templates30/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Templates6/test.desc b/regression/cbmc-cpp/Templates6/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/Templates6/test.desc
+++ b/regression/cbmc-cpp/Templates6/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/argv1/test.desc b/regression/cbmc-cpp/argv1/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/argv1/test.desc
+++ b/regression/cbmc-cpp/argv1/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/const_cast1/test.desc b/regression/cbmc-cpp/const_cast1/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/const_cast1/test.desc
+++ b/regression/cbmc-cpp/const_cast1/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/cpp-new/test.desc b/regression/cbmc-cpp/cpp-new/test.desc
index 97928218517..45cafea94a7 100644
--- a/regression/cbmc-cpp/cpp-new/test.desc
+++ b/regression/cbmc-cpp/cpp-new/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 --pointer-check
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/cpp1/test.desc b/regression/cbmc-cpp/cpp1/test.desc
index cacc33efcba..ffcde464af0 100644
--- a/regression/cbmc-cpp/cpp1/test.desc
+++ b/regression/cbmc-cpp/cpp1/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 --unwind 1 --unwinding-assertions
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/for1/test.desc b/regression/cbmc-cpp/for1/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/for1/test.desc
+++ b/regression/cbmc-cpp/for1/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/initialization3/test.desc b/regression/cbmc-cpp/initialization3/test.desc
index 9cae882a31f..08c699b62bc 100644
--- a/regression/cbmc-cpp/initialization3/test.desc
+++ b/regression/cbmc-cpp/initialization3/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=10$
diff --git a/regression/cbmc-cpp/initialization5/test.desc b/regression/cbmc-cpp/initialization5/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/initialization5/test.desc
+++ b/regression/cbmc-cpp/initialization5/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/lvalue1/test.desc b/regression/cbmc-cpp/lvalue1/test.desc
index 38fa43140bd..b472091d639 100644
--- a/regression/cbmc-cpp/lvalue1/test.desc
+++ b/regression/cbmc-cpp/lvalue1/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/namespace1/test.desc b/regression/cbmc-cpp/namespace1/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/namespace1/test.desc
+++ b/regression/cbmc-cpp/namespace1/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/namespace2/test.desc b/regression/cbmc-cpp/namespace2/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/namespace2/test.desc
+++ b/regression/cbmc-cpp/namespace2/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/namespace3/test.desc b/regression/cbmc-cpp/namespace3/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/namespace3/test.desc
+++ b/regression/cbmc-cpp/namespace3/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/new1/test.desc b/regression/cbmc-cpp/new1/test.desc
index 404ace834a8..8008aaf4e1f 100644
--- a/regression/cbmc-cpp/new1/test.desc
+++ b/regression/cbmc-cpp/new1/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 --pointer-check
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/operators/test.desc b/regression/cbmc-cpp/operators/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/operators/test.desc
+++ b/regression/cbmc-cpp/operators/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/reinterpret_cast1/test.desc b/regression/cbmc-cpp/reinterpret_cast1/test.desc
index 89db603c00c..30919594e35 100644
--- a/regression/cbmc-cpp/reinterpret_cast1/test.desc
+++ b/regression/cbmc-cpp/reinterpret_cast1/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 --little-endian
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/static_cast1/test.desc b/regression/cbmc-cpp/static_cast1/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/static_cast1/test.desc
+++ b/regression/cbmc-cpp/static_cast1/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/static_cast3/test.desc b/regression/cbmc-cpp/static_cast3/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/static_cast3/test.desc
+++ b/regression/cbmc-cpp/static_cast3/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/static_cast5/test.desc b/regression/cbmc-cpp/static_cast5/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/static_cast5/test.desc
+++ b/regression/cbmc-cpp/static_cast5/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/typecast_ambiguity3/test.desc b/regression/cbmc-cpp/typecast_ambiguity3/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/typecast_ambiguity3/test.desc
+++ b/regression/cbmc-cpp/typecast_ambiguity3/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/typedef4/test.desc b/regression/cbmc-cpp/typedef4/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/typedef4/test.desc
+++ b/regression/cbmc-cpp/typedef4/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/virtual10/test.desc b/regression/cbmc-cpp/virtual10/test.desc
index 307a2ce0d75..8eaeb8fdd30 100644
--- a/regression/cbmc-cpp/virtual10/test.desc
+++ b/regression/cbmc-cpp/virtual10/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/virtual2/test.desc b/regression/cbmc-cpp/virtual2/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/cbmc-cpp/virtual2/test.desc
+++ b/regression/cbmc-cpp/virtual2/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/virtual9/test.desc b/regression/cbmc-cpp/virtual9/test.desc
index 307a2ce0d75..8eaeb8fdd30 100644
--- a/regression/cbmc-cpp/virtual9/test.desc
+++ b/regression/cbmc-cpp/virtual9/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-incr-smt2/CMakeLists.txt b/regression/cbmc-incr-smt2/CMakeLists.txt
index 0591dd946e3..2e8e54e434c 100644
--- a/regression/cbmc-incr-smt2/CMakeLists.txt
+++ b/regression/cbmc-incr-smt2/CMakeLists.txt
@@ -1,20 +1,13 @@
-
-if("${CMAKE_SYSTEM_NAME}" STREQUAL "Windows")
-    set(exclude_win_broken_tests "-X;winbug")
-else()
-    set(exclude_win_broken_tests "")
-endif()
-
 add_test_pl_profile(
     "cbmc-incr-smt2-z3"
     "$<TARGET_FILE:cbmc> --incremental-smt2-solver 'z3 --smt2 -in' --validate-goto-model --validate-ssa-equation"
-    "-C;${exclude_win_broken_tests};-s;new-smt-z3"
+    "-C;-s;new-smt-z3"
     "CORE"
 )
 
 add_test_pl_profile(
     "cbmc-incr-smt2-cvc5"
     "$<TARGET_FILE:cbmc> --incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental' --validate-goto-model --validate-ssa-equation"
-    "-C;${exclude_win_broken_tests};-s;new-smt-cvc5"
+    "-C;-s;new-smt-cvc5"
     "CORE"
 )
diff --git a/regression/cbmc-incr-smt2/Makefile b/regression/cbmc-incr-smt2/Makefile
index 30b1ba812d2..9a5b8bf4195 100644
--- a/regression/cbmc-incr-smt2/Makefile
+++ b/regression/cbmc-incr-smt2/Makefile
@@ -3,19 +3,13 @@ default: test
 include ../../src/config.inc
 include ../../src/common
 
-ifeq ($(BUILD_ENV_),MSVC)
-	exclude_broken_windows_tests=-X winbug
-else
-	exclude_broken_windows_tests=
-endif
-
 test: test.z3 test.cvc5
 
 test.z3:
-	@../test.pl -e -p -c "../../../src/cbmc/cbmc --incremental-smt2-solver 'z3 --smt2 -in' --validate-goto-model --validate-ssa-equation" $(exclude_broken_windows_tests)
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --incremental-smt2-solver 'z3 --smt2 -in' --validate-goto-model --validate-ssa-equation"
 
 test.cvc5:
-	@../test.pl -e -p -c "../../../src/cbmc/cbmc --incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental' --validate-goto-model --validate-ssa-equation" $(exclude_broken_windows_tests)
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental' --validate-goto-model --validate-ssa-equation"
 
 tests.log: ../test.pl test
 
diff --git a/regression/cbmc/export-symex-ready-goto/test-bad-usage.desc b/regression/cbmc/export-symex-ready-goto/test-bad-usage.desc
index 6decca9ccec..7d49270fbe2 100644
--- a/regression/cbmc/export-symex-ready-goto/test-bad-usage.desc
+++ b/regression/cbmc/export-symex-ready-goto/test-bad-usage.desc
@@ -1,6 +1,6 @@
-CORE winbug
+CORE
 test.c
---export-symex-ready-goto ""
+--export-symex-ready-goto ''
 ^ERROR: Please provide a filename to write the goto-binary to.$
 ^EXIT=6$
 ^SIGNAL=0$
diff --git a/regression/cpp/CMakeLists.txt b/regression/cpp/CMakeLists.txt
index 7f333263aef..ef52ac2126f 100644
--- a/regression/cpp/CMakeLists.txt
+++ b/regression/cpp/CMakeLists.txt
@@ -4,12 +4,6 @@ else()
   set(gcc_only "")
 endif()
 
-if("${CMAKE_SYSTEM_NAME}" STREQUAL "Windows")
-  set(exclude_win_broken_tests -X winbug)
-else()
-  set(exclude_win_broken_tests "")
-endif()
-
 if("${CMAKE_SYSTEM_NAME}" STREQUAL "Darwin")
   set(exclude_mac_broken_tests -X macos-assert-broken)
 else()
@@ -17,5 +11,5 @@ else()
 endif()
 
 add_test_pl_tests(
-    "$<TARGET_FILE:goto-cc>" ${gcc_only} ${exclude_win_broken_tests} ${exclude_mac_broken_tests}
+    "$<TARGET_FILE:goto-cc>" ${gcc_only} ${exclude_mac_broken_tests}
 )
diff --git a/regression/cpp/Function_Overloading3/test.desc b/regression/cpp/Function_Overloading3/test.desc
index 1e5b2f25f26..a003b07b93c 100644
--- a/regression/cpp/Function_Overloading3/test.desc
+++ b/regression/cpp/Function_Overloading3/test.desc
@@ -1,4 +1,4 @@
-CORE winbug
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cpp/Makefile b/regression/cpp/Makefile
index ad98930bc22..694d00ac475 100644
--- a/regression/cpp/Makefile
+++ b/regression/cpp/Makefile
@@ -10,7 +10,7 @@ else
 endif
 
 ifeq ($(BUILD_ENV_),MSVC)
-	excluded_tests = -X gcc-only -X winbug
+	excluded_tests = -X gcc-only
 else
 ifeq ($(BUILD_ENV_),OSX)
 	# In MacOS, a change in the assert.h header file
diff --git a/regression/cpp/Method_qualifier1/test.desc b/regression/cpp/Method_qualifier1/test.desc
index 81dc5b681cd..dee97b866c5 100644
--- a/regression/cpp/Method_qualifier1/test.desc
+++ b/regression/cpp/Method_qualifier1/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cpp/Unary_Function_Overload1/test.desc b/regression/cpp/Unary_Function_Overload1/test.desc
index 1e5b2f25f26..a003b07b93c 100644
--- a/regression/cpp/Unary_Function_Overload1/test.desc
+++ b/regression/cpp/Unary_Function_Overload1/test.desc
@@ -1,4 +1,4 @@
-CORE winbug
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cpp/Unary_Function_Overload2/test.desc b/regression/cpp/Unary_Function_Overload2/test.desc
index 1e5b2f25f26..a003b07b93c 100644
--- a/regression/cpp/Unary_Function_Overload2/test.desc
+++ b/regression/cpp/Unary_Function_Overload2/test.desc
@@ -1,4 +1,4 @@
-CORE winbug
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cpp/Unary_Function_Overload3/test.desc b/regression/cpp/Unary_Function_Overload3/test.desc
index 1e5b2f25f26..a003b07b93c 100644
--- a/regression/cpp/Unary_Function_Overload3/test.desc
+++ b/regression/cpp/Unary_Function_Overload3/test.desc
@@ -1,4 +1,4 @@
-CORE winbug
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cpp/auto1/test.desc b/regression/cpp/auto1/test.desc
index aab3870cd27..cd53776c993 100644
--- a/regression/cpp/auto1/test.desc
+++ b/regression/cpp/auto1/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 -std=c++11
 ^EXIT=0$
diff --git a/regression/cpp/enum5/test.desc b/regression/cpp/enum5/test.desc
index c6e03fda074..52dec601d3f 100644
--- a/regression/cpp/enum5/test.desc
+++ b/regression/cpp/enum5/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cpp/switch1/test.desc b/regression/cpp/switch1/test.desc
index c6e03fda074..52dec601d3f 100644
--- a/regression/cpp/switch1/test.desc
+++ b/regression/cpp/switch1/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/goto-inspect/CMakeLists.txt b/regression/goto-inspect/CMakeLists.txt
index d6fbe4092e3..c979f8208b5 100644
--- a/regression/goto-inspect/CMakeLists.txt
+++ b/regression/goto-inspect/CMakeLists.txt
@@ -1,11 +1,9 @@
 if("${CMAKE_SYSTEM_NAME}" STREQUAL "Windows")
   set(is_windows true)
-  set(exclude_win_broken_tests -X winbug)
 else()
   set(is_windows false)
-  set(exclude_win_broken_tests "")
 endif()
 
 add_test_pl_tests(
-  "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-inspect> ${is_windows}" ${exclude_win_broken_tests}
+  "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:goto-inspect> ${is_windows}"
 )
diff --git a/regression/goto-inspect/Makefile b/regression/goto-inspect/Makefile
index ffd53798ddb..616ac044677 100644
--- a/regression/goto-inspect/Makefile
+++ b/regression/goto-inspect/Makefile
@@ -6,17 +6,16 @@ include ../../src/common
 ifeq ($(BUILD_ENV_),MSVC)
 	exe=../../../src/goto-cc/goto-cl
 	is_windows=true
-	excluded_tests = -X winbug
 else
 	exe=../../../src/goto-cc/goto-cc
 	is_windows=false
 endif
 
 test:
-	@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/goto-inspect/goto-inspect $(is_windows)' $(excluded_tests)
+	@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/goto-inspect/goto-inspect $(is_windows)'
 
 tests.log:
-	@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/goto-inspect/goto-inspect $(is_windows)' $(excluded_tests)
+	@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/goto-inspect/goto-inspect $(is_windows)'
 
 clean:
 	find . -name '*.out' -execdir $(RM) '{}' \;
diff --git a/regression/goto-inspect/show-goto-functions/negative.desc b/regression/goto-inspect/show-goto-functions/negative.desc
index f6762c1c344..2e0b71d6fce 100644
--- a/regression/goto-inspect/show-goto-functions/negative.desc
+++ b/regression/goto-inspect/show-goto-functions/negative.desc
@@ -1,6 +1,6 @@
-CORE winbug
+CORE
 main.c
-" "
+' '
 ^EXIT=6$
 ^SIGNAL=0$
 --
@@ -13,10 +13,3 @@ END_FUNCTION
 --
 This is testing the behaviour of the goto-inspect binary in case a binary
 is present, but no inspection option is present.
-
-This is labelled `winbug` to avoid running on windows because of issues with
-the empty string in line 3 (simulating the lack of an option) not working as
-it should (it is contrary to the behaviour of unix systems). The behaviour
-has been verified manually on a machine as working as expected, but getting
-the test to run automatically is a lot more involved, so we're opting to
-skipping this on that platform for now.
diff --git a/regression/systemc/Array2/test.desc b/regression/systemc/Array2/test.desc
index 9595069fcc1..d295e6bd4ac 100644
--- a/regression/systemc/Array2/test.desc
+++ b/regression/systemc/Array2/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 -DNO_IO -DNO_STRING
 ^EXIT=0$
diff --git a/regression/systemc/Array3/test.desc b/regression/systemc/Array3/test.desc
index 9595069fcc1..d295e6bd4ac 100644
--- a/regression/systemc/Array3/test.desc
+++ b/regression/systemc/Array3/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 -DNO_IO -DNO_STRING
 ^EXIT=0$
diff --git a/regression/systemc/Array4/test.desc b/regression/systemc/Array4/test.desc
index 9595069fcc1..d295e6bd4ac 100644
--- a/regression/systemc/Array4/test.desc
+++ b/regression/systemc/Array4/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 -DNO_IO -DNO_STRING
 ^EXIT=0$
diff --git a/regression/systemc/BitvectorCpp1/test.desc b/regression/systemc/BitvectorCpp1/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/systemc/BitvectorCpp1/test.desc
+++ b/regression/systemc/BitvectorCpp1/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/systemc/BitvectorCpp2/test.desc b/regression/systemc/BitvectorCpp2/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/systemc/BitvectorCpp2/test.desc
+++ b/regression/systemc/BitvectorCpp2/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/systemc/BitvectorSc3/test.desc b/regression/systemc/BitvectorSc3/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/systemc/BitvectorSc3/test.desc
+++ b/regression/systemc/BitvectorSc3/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/systemc/CMakeLists.txt b/regression/systemc/CMakeLists.txt
index b26338cc7d1..d332c611228 100644
--- a/regression/systemc/CMakeLists.txt
+++ b/regression/systemc/CMakeLists.txt
@@ -1,9 +1,3 @@
-if("${CMAKE_SYSTEM_NAME}" STREQUAL "Windows")
-  set(exclude_win_broken_tests -X winbug)
-else()
-  set(exclude_win_broken_tests "")
-endif()
-
 if("${CMAKE_SYSTEM_NAME}" STREQUAL "Darwin")
   set(exclude_mac_broken_tests -X macos-assert-broken)
 else()
@@ -11,5 +5,5 @@ else()
 endif()
 
 add_test_pl_tests(
-    "$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation" ${exclude_win_broken_tests} ${exclude_mac_broken_tests}
+    "$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation" ${exclude_mac_broken_tests}
 )
diff --git a/regression/systemc/EqualOp3/test.desc b/regression/systemc/EqualOp3/test.desc
index 876245bf3ac..e778f120e58 100644
--- a/regression/systemc/EqualOp3/test.desc
+++ b/regression/systemc/EqualOp3/test.desc
@@ -1,4 +1,4 @@
-CORE winbug
+CORE
 main.cpp
 
 ^EXIT=10$
diff --git a/regression/systemc/ForwardDecl1/test.desc b/regression/systemc/ForwardDecl1/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/systemc/ForwardDecl1/test.desc
+++ b/regression/systemc/ForwardDecl1/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/systemc/FunTempl1/test.desc b/regression/systemc/FunTempl1/test.desc
index 7a484a166fa..91d9cf8b52e 100644
--- a/regression/systemc/FunTempl1/test.desc
+++ b/regression/systemc/FunTempl1/test.desc
@@ -1,4 +1,4 @@
-CORE winbug
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/systemc/Makefile b/regression/systemc/Makefile
index 588589d35a5..e801537c045 100644
--- a/regression/systemc/Makefile
+++ b/regression/systemc/Makefile
@@ -10,7 +10,7 @@ else
 endif
 
 ifeq ($(BUILD_ENV_),MSVC)
-	excluded_tests = -X gcc-only -X winbug
+	excluded_tests = -X gcc-only
 else
 ifeq ($(BUILD_ENV_),OSX)
 	# In MacOS, a change in the assert.h header file
diff --git a/regression/systemc/Masc1/test.desc b/regression/systemc/Masc1/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/systemc/Masc1/test.desc
+++ b/regression/systemc/Masc1/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/systemc/MascInst1/test.desc b/regression/systemc/MascInst1/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/systemc/MascInst1/test.desc
+++ b/regression/systemc/MascInst1/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/systemc/Reference1/test.desc b/regression/systemc/Reference1/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/systemc/Reference1/test.desc
+++ b/regression/systemc/Reference1/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/systemc/This1/test.desc b/regression/systemc/This1/test.desc
index fb16a88c617..22942ea2648 100644
--- a/regression/systemc/This1/test.desc
+++ b/regression/systemc/This1/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/systemc/Tuple1/test.desc b/regression/systemc/Tuple1/test.desc
index 9595069fcc1..d295e6bd4ac 100644
--- a/regression/systemc/Tuple1/test.desc
+++ b/regression/systemc/Tuple1/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 -DNO_IO -DNO_STRING
 ^EXIT=0$
diff --git a/regression/systemc/Tuple2/test.desc b/regression/systemc/Tuple2/test.desc
index 9595069fcc1..d295e6bd4ac 100644
--- a/regression/systemc/Tuple2/test.desc
+++ b/regression/systemc/Tuple2/test.desc
@@ -1,4 +1,4 @@
-CORE winbug macos-assert-broken
+CORE macos-assert-broken
 main.cpp
 -DNO_IO -DNO_STRING
 ^EXIT=0$