diff --git a/regression/ansi-c/CMakeLists.txt b/regression/ansi-c/CMakeLists.txt
index 38859c1cab8..f87c8f132a1 100644
--- a/regression/ansi-c/CMakeLists.txt
+++ b/regression/ansi-c/CMakeLists.txt
@@ -7,15 +7,10 @@ elseif("${CMAKE_SYSTEM_NAME}" STREQUAL "Darwin")
         "$<TARGET_FILE:goto-cc>"
     )
 
-    # In MacOS, a change in the assert.h header file
-    # is causing template errors when exercising the
-    # C++ front end (because of a transitive include
-    # of <type_traits>) for files that include the
-    # <assert.h> or <cassert> headers.
     add_test_pl_profile(
         "ansi-c-c++-front-end"
         "$<TARGET_FILE:goto-cc> -xc++ -D_Bool=bool"
-        "-C;-I;test-c++-front-end;-s;c++-front-end-X;macos-assert-broken"
+        "-C;-I;test-c++-front-end;-s;c++-front-end"
         "CORE"
     )
 else()
diff --git a/regression/ansi-c/Makefile b/regression/ansi-c/Makefile
index 1048644af67..727fa8cbc91 100644
--- a/regression/ansi-c/Makefile
+++ b/regression/ansi-c/Makefile
@@ -11,15 +11,6 @@ endif
 
 ifeq ($(BUILD_ENV_),MSVC)
 	excluded_tests = -X gcc-only -X clang-only
-else
-ifeq ($(BUILD_ENV_),OSX)
-	# In MacOS, a change in the assert.h header file
-	# is causing template errors when exercising the
-	# C++ front end (because of a transitive include
-	# of <type_traits>) for files that include the
-	# <assert.h> or <cassert> headers.
-  excluded_tests = -X macos-assert-broken
-endif
 endif
 
 test:
diff --git a/regression/ansi-c/array_initialization2/test.desc b/regression/ansi-c/array_initialization2/test.desc
index dbb23d0d23a..b9903aa3c3d 100644
--- a/regression/ansi-c/array_initialization2/test.desc
+++ b/regression/ansi-c/array_initialization2/test.desc
@@ -1,4 +1,4 @@
-CORE test-c++-front-end macos-assert-broken
+CORE test-c++-front-end
 main.c
 
 ^EXIT=0$
diff --git a/regression/ansi-c/float_constant2/test.desc b/regression/ansi-c/float_constant2/test.desc
index dbb23d0d23a..b9903aa3c3d 100644
--- a/regression/ansi-c/float_constant2/test.desc
+++ b/regression/ansi-c/float_constant2/test.desc
@@ -1,4 +1,4 @@
-CORE test-c++-front-end macos-assert-broken
+CORE test-c++-front-end
 main.c
 
 ^EXIT=0$
diff --git a/regression/ansi-c/goto_convert_switch_range_case_valid/test.desc b/regression/ansi-c/goto_convert_switch_range_case_valid/test.desc
index 6f2f5c63ca3..13796643406 100644
--- a/regression/ansi-c/goto_convert_switch_range_case_valid/test.desc
+++ b/regression/ansi-c/goto_convert_switch_range_case_valid/test.desc
@@ -1,4 +1,4 @@
-CORE test-c++-front-end macos-assert-broken
+CORE test-c++-front-end
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Address_of_Method1/test.desc b/regression/cbmc-cpp/Address_of_Method1/test.desc
index af1345b7343..6666d172f47 100644
--- a/regression/cbmc-cpp/Address_of_Method1/test.desc
+++ b/regression/cbmc-cpp/Address_of_Method1/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG macos-assert-broken
+KNOWNBUG
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Anonymous_members1/test.desc b/regression/cbmc-cpp/Anonymous_members1/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Anonymous_members1/test.desc
+++ b/regression/cbmc-cpp/Anonymous_members1/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Assignment1/test.desc b/regression/cbmc-cpp/Assignment1/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Assignment1/test.desc
+++ b/regression/cbmc-cpp/Assignment1/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/CMakeLists.txt b/regression/cbmc-cpp/CMakeLists.txt
index e9280edac73..4d141f395e6 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 "Darwin")
-  set(exclude_mac_broken_tests -X macos-assert-broken)
-else()
-  set(exclude_mac_broken_tests "")
-endif()
-
 add_test_pl_tests(
-    "$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation" ${gcc_only} ${exclude_mac_broken_tests}
+    "$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation" ${gcc_only}
 )
diff --git a/regression/cbmc-cpp/Class_Members1/test.desc b/regression/cbmc-cpp/Class_Members1/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Class_Members1/test.desc
+++ b/regression/cbmc-cpp/Class_Members1/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Comma_Operator1/test.desc b/regression/cbmc-cpp/Comma_Operator1/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Comma_Operator1/test.desc
+++ b/regression/cbmc-cpp/Comma_Operator1/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/ConditionalExpression1/test.desc b/regression/cbmc-cpp/ConditionalExpression1/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/ConditionalExpression1/test.desc
+++ b/regression/cbmc-cpp/ConditionalExpression1/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/ConditionalExpression2/test.desc b/regression/cbmc-cpp/ConditionalExpression2/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/ConditionalExpression2/test.desc
+++ b/regression/cbmc-cpp/ConditionalExpression2/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Constructor1/test.desc b/regression/cbmc-cpp/Constructor1/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Constructor1/test.desc
+++ b/regression/cbmc-cpp/Constructor1/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Constructor12/test.desc b/regression/cbmc-cpp/Constructor12/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Constructor12/test.desc
+++ b/regression/cbmc-cpp/Constructor12/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Constructor13/test.desc b/regression/cbmc-cpp/Constructor13/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Constructor13/test.desc
+++ b/regression/cbmc-cpp/Constructor13/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Constructor2/test.desc b/regression/cbmc-cpp/Constructor2/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Constructor2/test.desc
+++ b/regression/cbmc-cpp/Constructor2/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Constructor3/test.desc b/regression/cbmc-cpp/Constructor3/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Constructor3/test.desc
+++ b/regression/cbmc-cpp/Constructor3/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Constructor4/test.desc b/regression/cbmc-cpp/Constructor4/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Constructor4/test.desc
+++ b/regression/cbmc-cpp/Constructor4/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Constructor5/test.desc b/regression/cbmc-cpp/Constructor5/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Constructor5/test.desc
+++ b/regression/cbmc-cpp/Constructor5/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Constructor6/test.desc b/regression/cbmc-cpp/Constructor6/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Constructor6/test.desc
+++ b/regression/cbmc-cpp/Constructor6/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Constructor9/test.desc b/regression/cbmc-cpp/Constructor9/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Constructor9/test.desc
+++ b/regression/cbmc-cpp/Constructor9/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Conversion5/test.desc b/regression/cbmc-cpp/Conversion5/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Conversion5/test.desc
+++ b/regression/cbmc-cpp/Conversion5/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Conversion6/test.desc b/regression/cbmc-cpp/Conversion6/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Conversion6/test.desc
+++ b/regression/cbmc-cpp/Conversion6/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Conversion_Operator2/test.desc b/regression/cbmc-cpp/Conversion_Operator2/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Conversion_Operator2/test.desc
+++ b/regression/cbmc-cpp/Conversion_Operator2/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Conversion_Operator3/test.desc b/regression/cbmc-cpp/Conversion_Operator3/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Conversion_Operator3/test.desc
+++ b/regression/cbmc-cpp/Conversion_Operator3/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Conversion_Operator4/test.desc b/regression/cbmc-cpp/Conversion_Operator4/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Conversion_Operator4/test.desc
+++ b/regression/cbmc-cpp/Conversion_Operator4/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Default_Arguments1/test.desc b/regression/cbmc-cpp/Default_Arguments1/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Default_Arguments1/test.desc
+++ b/regression/cbmc-cpp/Default_Arguments1/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Default_Arguments2/test.desc b/regression/cbmc-cpp/Default_Arguments2/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Default_Arguments2/test.desc
+++ b/regression/cbmc-cpp/Default_Arguments2/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 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 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Destructor_with_PtrMember/test.desc
+++ b/regression/cbmc-cpp/Destructor_with_PtrMember/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Float1/test.desc b/regression/cbmc-cpp/Float1/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Float1/test.desc
+++ b/regression/cbmc-cpp/Float1/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Friend5/test.desc b/regression/cbmc-cpp/Friend5/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Friend5/test.desc
+++ b/regression/cbmc-cpp/Friend5/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/FunctionParam1/test.desc b/regression/cbmc-cpp/FunctionParam1/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/FunctionParam1/test.desc
+++ b/regression/cbmc-cpp/FunctionParam1/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Function_Arguments2/test.desc b/regression/cbmc-cpp/Function_Arguments2/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Function_Arguments2/test.desc
+++ b/regression/cbmc-cpp/Function_Arguments2/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Function_Arguments5/test.desc b/regression/cbmc-cpp/Function_Arguments5/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Function_Arguments5/test.desc
+++ b/regression/cbmc-cpp/Function_Arguments5/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Function_Pointer1/test.desc b/regression/cbmc-cpp/Function_Pointer1/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Function_Pointer1/test.desc
+++ b/regression/cbmc-cpp/Function_Pointer1/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Implicit_Conversion1/test.desc b/regression/cbmc-cpp/Implicit_Conversion1/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Implicit_Conversion1/test.desc
+++ b/regression/cbmc-cpp/Implicit_Conversion1/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Implicit_Conversion4/test.desc b/regression/cbmc-cpp/Implicit_Conversion4/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Implicit_Conversion4/test.desc
+++ b/regression/cbmc-cpp/Implicit_Conversion4/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Implicit_Conversion6/test.desc b/regression/cbmc-cpp/Implicit_Conversion6/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Implicit_Conversion6/test.desc
+++ b/regression/cbmc-cpp/Implicit_Conversion6/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Implicit_Conversion7/test.desc b/regression/cbmc-cpp/Implicit_Conversion7/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Implicit_Conversion7/test.desc
+++ b/regression/cbmc-cpp/Implicit_Conversion7/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Inheritance1/test.desc b/regression/cbmc-cpp/Inheritance1/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Inheritance1/test.desc
+++ b/regression/cbmc-cpp/Inheritance1/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Inheritance3/test.desc b/regression/cbmc-cpp/Inheritance3/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Inheritance3/test.desc
+++ b/regression/cbmc-cpp/Inheritance3/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Inheritance4/test.desc b/regression/cbmc-cpp/Inheritance4/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Inheritance4/test.desc
+++ b/regression/cbmc-cpp/Inheritance4/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Initializer1/test.desc b/regression/cbmc-cpp/Initializer1/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Initializer1/test.desc
+++ b/regression/cbmc-cpp/Initializer1/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Label0/test.desc b/regression/cbmc-cpp/Label0/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Label0/test.desc
+++ b/regression/cbmc-cpp/Label0/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Linking1/test.desc b/regression/cbmc-cpp/Linking1/test.desc
index 4c1cb5611fa..2449051ba1d 100644
--- a/regression/cbmc-cpp/Linking1/test.desc
+++ b/regression/cbmc-cpp/Linking1/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 module.cpp
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Makefile b/regression/cbmc-cpp/Makefile
index febf12571a3..b08769d4551 100644
--- a/regression/cbmc-cpp/Makefile
+++ b/regression/cbmc-cpp/Makefile
@@ -5,15 +5,6 @@ include ../../src/common
 
 ifeq ($(BUILD_ENV_),MSVC)
 	excluded_tests = -X gcc-only
-else
-ifeq ($(BUILD_ENV_),OSX)
-	# In MacOS, a change in the assert.h header file
-	# is causing template errors when exercising the
-	# C++ front end (because of a transitive include
-	# of <type_traits>) for files that include the
-	# <assert.h> or <cassert> headers.
-  excluded_tests = -X macos-assert-broken
-endif
 endif
 
 test:
diff --git a/regression/cbmc-cpp/Member_Access_in_Class/test.desc b/regression/cbmc-cpp/Member_Access_in_Class/test.desc
index 22942ea2648..91d9cf8b52e 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 macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/MethodParam1/test.desc b/regression/cbmc-cpp/MethodParam1/test.desc
index f70a1e1a8ee..2e6283f7316 100644
--- a/regression/cbmc-cpp/MethodParam1/test.desc
+++ b/regression/cbmc-cpp/MethodParam1/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 instance is SATISFIABLE$
diff --git a/regression/cbmc-cpp/Mutable1/test.desc b/regression/cbmc-cpp/Mutable1/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Mutable1/test.desc
+++ b/regression/cbmc-cpp/Mutable1/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Overloading_Functions1/test.desc b/regression/cbmc-cpp/Overloading_Functions1/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Overloading_Functions1/test.desc
+++ b/regression/cbmc-cpp/Overloading_Functions1/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Overloading_Functions3/test.desc b/regression/cbmc-cpp/Overloading_Functions3/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Overloading_Functions3/test.desc
+++ b/regression/cbmc-cpp/Overloading_Functions3/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Overloading_Increment1/test.desc b/regression/cbmc-cpp/Overloading_Increment1/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Overloading_Increment1/test.desc
+++ b/regression/cbmc-cpp/Overloading_Increment1/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Overloading_Members1/test.desc b/regression/cbmc-cpp/Overloading_Members1/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Overloading_Members1/test.desc
+++ b/regression/cbmc-cpp/Overloading_Members1/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Overloading_Operators12/test.desc b/regression/cbmc-cpp/Overloading_Operators12/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Overloading_Operators12/test.desc
+++ b/regression/cbmc-cpp/Overloading_Operators12/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Overloading_Operators13/test.desc b/regression/cbmc-cpp/Overloading_Operators13/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Overloading_Operators13/test.desc
+++ b/regression/cbmc-cpp/Overloading_Operators13/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Overloading_Operators2/test.desc b/regression/cbmc-cpp/Overloading_Operators2/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Overloading_Operators2/test.desc
+++ b/regression/cbmc-cpp/Overloading_Operators2/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Overloading_Operators7/test.desc b/regression/cbmc-cpp/Overloading_Operators7/test.desc
index af1345b7343..6666d172f47 100644
--- a/regression/cbmc-cpp/Overloading_Operators7/test.desc
+++ b/regression/cbmc-cpp/Overloading_Operators7/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG macos-assert-broken
+KNOWNBUG
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Overloading_Operators8/test.desc b/regression/cbmc-cpp/Overloading_Operators8/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Overloading_Operators8/test.desc
+++ b/regression/cbmc-cpp/Overloading_Operators8/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Pointer_Conversion2/test.desc b/regression/cbmc-cpp/Pointer_Conversion2/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Pointer_Conversion2/test.desc
+++ b/regression/cbmc-cpp/Pointer_Conversion2/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Protection2/test.desc b/regression/cbmc-cpp/Protection2/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Protection2/test.desc
+++ b/regression/cbmc-cpp/Protection2/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Qualifier2/test.desc b/regression/cbmc-cpp/Qualifier2/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Qualifier2/test.desc
+++ b/regression/cbmc-cpp/Qualifier2/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Reference2/test.desc b/regression/cbmc-cpp/Reference2/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Reference2/test.desc
+++ b/regression/cbmc-cpp/Reference2/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Reference3/test.desc b/regression/cbmc-cpp/Reference3/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Reference3/test.desc
+++ b/regression/cbmc-cpp/Reference3/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Reference6/test.desc b/regression/cbmc-cpp/Reference6/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Reference6/test.desc
+++ b/regression/cbmc-cpp/Reference6/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Reference7/test.desc b/regression/cbmc-cpp/Reference7/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Reference7/test.desc
+++ b/regression/cbmc-cpp/Reference7/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Resolver6/test.desc b/regression/cbmc-cpp/Resolver6/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Resolver6/test.desc
+++ b/regression/cbmc-cpp/Resolver6/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Resolver7/test.desc b/regression/cbmc-cpp/Resolver7/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Resolver7/test.desc
+++ b/regression/cbmc-cpp/Resolver7/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Resolver8/test.desc b/regression/cbmc-cpp/Resolver8/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Resolver8/test.desc
+++ b/regression/cbmc-cpp/Resolver8/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Static_Method1/test.desc b/regression/cbmc-cpp/Static_Method1/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Static_Method1/test.desc
+++ b/regression/cbmc-cpp/Static_Method1/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/String_Literal1/test.desc b/regression/cbmc-cpp/String_Literal1/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/String_Literal1/test.desc
+++ b/regression/cbmc-cpp/String_Literal1/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Templates10/test.desc b/regression/cbmc-cpp/Templates10/test.desc
index af1345b7343..6666d172f47 100644
--- a/regression/cbmc-cpp/Templates10/test.desc
+++ b/regression/cbmc-cpp/Templates10/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG macos-assert-broken
+KNOWNBUG
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Templates11/test.desc b/regression/cbmc-cpp/Templates11/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Templates11/test.desc
+++ b/regression/cbmc-cpp/Templates11/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Templates12/test.desc b/regression/cbmc-cpp/Templates12/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Templates12/test.desc
+++ b/regression/cbmc-cpp/Templates12/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Templates13/test.desc b/regression/cbmc-cpp/Templates13/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Templates13/test.desc
+++ b/regression/cbmc-cpp/Templates13/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Templates14/test.desc b/regression/cbmc-cpp/Templates14/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Templates14/test.desc
+++ b/regression/cbmc-cpp/Templates14/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Templates16/test.desc b/regression/cbmc-cpp/Templates16/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Templates16/test.desc
+++ b/regression/cbmc-cpp/Templates16/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Templates19/test.desc b/regression/cbmc-cpp/Templates19/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Templates19/test.desc
+++ b/regression/cbmc-cpp/Templates19/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Templates20/test.desc b/regression/cbmc-cpp/Templates20/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Templates20/test.desc
+++ b/regression/cbmc-cpp/Templates20/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Templates21/test.desc b/regression/cbmc-cpp/Templates21/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Templates21/test.desc
+++ b/regression/cbmc-cpp/Templates21/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Templates22/test.desc b/regression/cbmc-cpp/Templates22/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Templates22/test.desc
+++ b/regression/cbmc-cpp/Templates22/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Templates23/test.desc b/regression/cbmc-cpp/Templates23/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Templates23/test.desc
+++ b/regression/cbmc-cpp/Templates23/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Templates24/test.desc b/regression/cbmc-cpp/Templates24/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Templates24/test.desc
+++ b/regression/cbmc-cpp/Templates24/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Templates25/test.desc b/regression/cbmc-cpp/Templates25/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Templates25/test.desc
+++ b/regression/cbmc-cpp/Templates25/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Templates26/test.desc b/regression/cbmc-cpp/Templates26/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Templates26/test.desc
+++ b/regression/cbmc-cpp/Templates26/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Templates27/test.desc b/regression/cbmc-cpp/Templates27/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Templates27/test.desc
+++ b/regression/cbmc-cpp/Templates27/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Templates28/test.desc b/regression/cbmc-cpp/Templates28/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Templates28/test.desc
+++ b/regression/cbmc-cpp/Templates28/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Templates3/test.desc b/regression/cbmc-cpp/Templates3/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Templates3/test.desc
+++ b/regression/cbmc-cpp/Templates3/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Templates30/test.desc b/regression/cbmc-cpp/Templates30/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Templates30/test.desc
+++ b/regression/cbmc-cpp/Templates30/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/Templates6/test.desc b/regression/cbmc-cpp/Templates6/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/Templates6/test.desc
+++ b/regression/cbmc-cpp/Templates6/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/argv1/test.desc b/regression/cbmc-cpp/argv1/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/argv1/test.desc
+++ b/regression/cbmc-cpp/argv1/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/const_cast1/test.desc b/regression/cbmc-cpp/const_cast1/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/const_cast1/test.desc
+++ b/regression/cbmc-cpp/const_cast1/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/cpp-new/test.desc b/regression/cbmc-cpp/cpp-new/test.desc
index 45cafea94a7..dc9499da1a5 100644
--- a/regression/cbmc-cpp/cpp-new/test.desc
+++ b/regression/cbmc-cpp/cpp-new/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 --pointer-check
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/cpp1/test.desc b/regression/cbmc-cpp/cpp1/test.desc
index ffcde464af0..e6c5f4f102d 100644
--- a/regression/cbmc-cpp/cpp1/test.desc
+++ b/regression/cbmc-cpp/cpp1/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 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 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/for1/test.desc
+++ b/regression/cbmc-cpp/for1/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/initialization3/test.desc b/regression/cbmc-cpp/initialization3/test.desc
index 08c699b62bc..e778f120e58 100644
--- a/regression/cbmc-cpp/initialization3/test.desc
+++ b/regression/cbmc-cpp/initialization3/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=10$
diff --git a/regression/cbmc-cpp/initialization5/test.desc b/regression/cbmc-cpp/initialization5/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/initialization5/test.desc
+++ b/regression/cbmc-cpp/initialization5/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/lvalue1/test.desc b/regression/cbmc-cpp/lvalue1/test.desc
index b472091d639..5c2cf626c3a 100644
--- a/regression/cbmc-cpp/lvalue1/test.desc
+++ b/regression/cbmc-cpp/lvalue1/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/namespace1/test.desc b/regression/cbmc-cpp/namespace1/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/namespace1/test.desc
+++ b/regression/cbmc-cpp/namespace1/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/namespace2/test.desc b/regression/cbmc-cpp/namespace2/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/namespace2/test.desc
+++ b/regression/cbmc-cpp/namespace2/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/namespace3/test.desc b/regression/cbmc-cpp/namespace3/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/namespace3/test.desc
+++ b/regression/cbmc-cpp/namespace3/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/new1/test.desc b/regression/cbmc-cpp/new1/test.desc
index 8008aaf4e1f..261ae194d03 100644
--- a/regression/cbmc-cpp/new1/test.desc
+++ b/regression/cbmc-cpp/new1/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 --pointer-check
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/operators/test.desc b/regression/cbmc-cpp/operators/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/operators/test.desc
+++ b/regression/cbmc-cpp/operators/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/reinterpret_cast1/test.desc b/regression/cbmc-cpp/reinterpret_cast1/test.desc
index 30919594e35..5249662e6aa 100644
--- a/regression/cbmc-cpp/reinterpret_cast1/test.desc
+++ b/regression/cbmc-cpp/reinterpret_cast1/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 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 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/static_cast1/test.desc
+++ b/regression/cbmc-cpp/static_cast1/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/static_cast3/test.desc b/regression/cbmc-cpp/static_cast3/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/static_cast3/test.desc
+++ b/regression/cbmc-cpp/static_cast3/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/static_cast5/test.desc b/regression/cbmc-cpp/static_cast5/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/static_cast5/test.desc
+++ b/regression/cbmc-cpp/static_cast5/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/typecast_ambiguity3/test.desc b/regression/cbmc-cpp/typecast_ambiguity3/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/typecast_ambiguity3/test.desc
+++ b/regression/cbmc-cpp/typecast_ambiguity3/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/typedef4/test.desc b/regression/cbmc-cpp/typedef4/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/typedef4/test.desc
+++ b/regression/cbmc-cpp/typedef4/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/union2/test.desc b/regression/cbmc-cpp/union2/test.desc
index 30919594e35..5249662e6aa 100644
--- a/regression/cbmc-cpp/union2/test.desc
+++ b/regression/cbmc-cpp/union2/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 --little-endian
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/virtual10/test.desc b/regression/cbmc-cpp/virtual10/test.desc
index 8eaeb8fdd30..7ed391809e9 100644
--- a/regression/cbmc-cpp/virtual10/test.desc
+++ b/regression/cbmc-cpp/virtual10/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/virtual2/test.desc b/regression/cbmc-cpp/virtual2/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/cbmc-cpp/virtual2/test.desc
+++ b/regression/cbmc-cpp/virtual2/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cbmc-cpp/virtual9/test.desc b/regression/cbmc-cpp/virtual9/test.desc
index 8eaeb8fdd30..7ed391809e9 100644
--- a/regression/cbmc-cpp/virtual9/test.desc
+++ b/regression/cbmc-cpp/virtual9/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cpp/Bit_fields1/main.cpp b/regression/cpp/Bit_fields1/main.cpp
index 435da18867c..44a9b5d8242 100644
--- a/regression/cpp/Bit_fields1/main.cpp
+++ b/regression/cpp/Bit_fields1/main.cpp
@@ -9,6 +9,7 @@ struct some_struct {
 
   // an anonymous bitfield
   signed int :2;
+  signed int d : 2, : 6;
 
   // with typedef
   INT x:1;
diff --git a/regression/cpp/CMakeLists.txt b/regression/cpp/CMakeLists.txt
index ef52ac2126f..2f9b458d43f 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 "Darwin")
-  set(exclude_mac_broken_tests -X macos-assert-broken)
-else()
-  set(exclude_mac_broken_tests "")
-endif()
-
 add_test_pl_tests(
-    "$<TARGET_FILE:goto-cc>" ${gcc_only} ${exclude_mac_broken_tests}
+    "$<TARGET_FILE:goto-cc>" ${gcc_only}
 )
diff --git a/regression/cpp/Makefile b/regression/cpp/Makefile
index 694d00ac475..708253aaceb 100644
--- a/regression/cpp/Makefile
+++ b/regression/cpp/Makefile
@@ -11,15 +11,6 @@ endif
 
 ifeq ($(BUILD_ENV_),MSVC)
 	excluded_tests = -X gcc-only
-else
-ifeq ($(BUILD_ENV_),OSX)
-	# In MacOS, a change in the assert.h header file
-	# is causing template errors when exercising the
-	# C++ front end (because of a transitive include
-	# of <type_traits>) for files that include the
-	# <assert.h> or <cassert> headers.
-  excluded_tests = -X macos-assert-broken
-endif
 endif
 
 test:
diff --git a/regression/cpp/Method_qualifier1/test.desc b/regression/cpp/Method_qualifier1/test.desc
index dee97b866c5..c6b2fc72af0 100644
--- a/regression/cpp/Method_qualifier1/test.desc
+++ b/regression/cpp/Method_qualifier1/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cpp/auto1/test.desc b/regression/cpp/auto1/test.desc
index cd53776c993..3862862ffd3 100644
--- a/regression/cpp/auto1/test.desc
+++ b/regression/cpp/auto1/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 -std=c++11
 ^EXIT=0$
diff --git a/regression/cpp/enum5/test.desc b/regression/cpp/enum5/test.desc
index 52dec601d3f..a003b07b93c 100644
--- a/regression/cpp/enum5/test.desc
+++ b/regression/cpp/enum5/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cpp/switch1/test.desc b/regression/cpp/switch1/test.desc
index 52dec601d3f..a003b07b93c 100644
--- a/regression/cpp/switch1/test.desc
+++ b/regression/cpp/switch1/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/cpp/virtual1/test.desc b/regression/cpp/virtual1/test.desc
index 52dec601d3f..a003b07b93c 100644
--- a/regression/cpp/virtual1/test.desc
+++ b/regression/cpp/virtual1/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/systemc/Array2/test.desc b/regression/systemc/Array2/test.desc
index d295e6bd4ac..d091759e812 100644
--- a/regression/systemc/Array2/test.desc
+++ b/regression/systemc/Array2/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 -DNO_IO -DNO_STRING
 ^EXIT=0$
diff --git a/regression/systemc/Array3/test.desc b/regression/systemc/Array3/test.desc
index d295e6bd4ac..d091759e812 100644
--- a/regression/systemc/Array3/test.desc
+++ b/regression/systemc/Array3/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 -DNO_IO -DNO_STRING
 ^EXIT=0$
diff --git a/regression/systemc/Array4/test.desc b/regression/systemc/Array4/test.desc
index d295e6bd4ac..d091759e812 100644
--- a/regression/systemc/Array4/test.desc
+++ b/regression/systemc/Array4/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 -DNO_IO -DNO_STRING
 ^EXIT=0$
diff --git a/regression/systemc/BitvectorCpp1/test.desc b/regression/systemc/BitvectorCpp1/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/systemc/BitvectorCpp1/test.desc
+++ b/regression/systemc/BitvectorCpp1/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/systemc/BitvectorCpp2/test.desc b/regression/systemc/BitvectorCpp2/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/systemc/BitvectorCpp2/test.desc
+++ b/regression/systemc/BitvectorCpp2/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/systemc/BitvectorSc3/test.desc b/regression/systemc/BitvectorSc3/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/systemc/BitvectorSc3/test.desc
+++ b/regression/systemc/BitvectorSc3/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/systemc/CMakeLists.txt b/regression/systemc/CMakeLists.txt
index d332c611228..8ebf053fd6d 100644
--- a/regression/systemc/CMakeLists.txt
+++ b/regression/systemc/CMakeLists.txt
@@ -1,9 +1,3 @@
-if("${CMAKE_SYSTEM_NAME}" STREQUAL "Darwin")
-  set(exclude_mac_broken_tests -X macos-assert-broken)
-else()
-  set(exclude_mac_broken_tests "")
-endif()
-
 add_test_pl_tests(
-    "$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation" ${exclude_mac_broken_tests}
+    "$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation"
 )
diff --git a/regression/systemc/ForwardDecl1/test.desc b/regression/systemc/ForwardDecl1/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/systemc/ForwardDecl1/test.desc
+++ b/regression/systemc/ForwardDecl1/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/systemc/Makefile b/regression/systemc/Makefile
index e801537c045..417577be4a7 100644
--- a/regression/systemc/Makefile
+++ b/regression/systemc/Makefile
@@ -11,15 +11,6 @@ endif
 
 ifeq ($(BUILD_ENV_),MSVC)
 	excluded_tests = -X gcc-only
-else
-ifeq ($(BUILD_ENV_),OSX)
-	# In MacOS, a change in the assert.h header file
-	# is causing template errors when exercising the
-	# C++ front end (because of a transitive include
-	# of <type_traits>) for files that include the
-	# <assert.h> or <cassert> headers.
-  excluded_tests = -X macos-assert-broken
-endif
 endif
 
 default: tests.log
diff --git a/regression/systemc/Masc1/test.desc b/regression/systemc/Masc1/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/systemc/Masc1/test.desc
+++ b/regression/systemc/Masc1/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/systemc/MascInst1/test.desc b/regression/systemc/MascInst1/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/systemc/MascInst1/test.desc
+++ b/regression/systemc/MascInst1/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/systemc/Reference1/test.desc b/regression/systemc/Reference1/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/systemc/Reference1/test.desc
+++ b/regression/systemc/Reference1/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/systemc/This1/test.desc b/regression/systemc/This1/test.desc
index 22942ea2648..91d9cf8b52e 100644
--- a/regression/systemc/This1/test.desc
+++ b/regression/systemc/This1/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 
 ^EXIT=0$
diff --git a/regression/systemc/Tuple1/test.desc b/regression/systemc/Tuple1/test.desc
index d295e6bd4ac..d091759e812 100644
--- a/regression/systemc/Tuple1/test.desc
+++ b/regression/systemc/Tuple1/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 -DNO_IO -DNO_STRING
 ^EXIT=0$
diff --git a/regression/systemc/Tuple2/test.desc b/regression/systemc/Tuple2/test.desc
index d295e6bd4ac..d091759e812 100644
--- a/regression/systemc/Tuple2/test.desc
+++ b/regression/systemc/Tuple2/test.desc
@@ -1,4 +1,4 @@
-CORE macos-assert-broken
+CORE
 main.cpp
 -DNO_IO -DNO_STRING
 ^EXIT=0$
diff --git a/src/cpp/parse.cpp b/src/cpp/parse.cpp
index f0c71a6a5d6..ab12c9b70fa 100644
--- a/src/cpp/parse.cpp
+++ b/src/cpp/parse.cpp
@@ -2880,7 +2880,7 @@ bool Parser::rDeclaratorWithInit(
     bit_field_type.add_subtype().make_nil();
     set_location(bit_field_type, tk);
 
-    merge_types(bit_field_type, dw.type());
+    dw.type() = std::move(bit_field_type);
 
     return true;
   }