diff --git a/regression/cbmc/dynamic_size1/stack_object.desc b/regression/cbmc/dynamic_size1/stack_object.desc
index c6ac74c15fb..242e2c1d4c0 100644
--- a/regression/cbmc/dynamic_size1/stack_object.desc
+++ b/regression/cbmc/dynamic_size1/stack_object.desc
@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 stack_object.c
 --pointer-check
 ^EXIT=0$
diff --git a/regression/cbmc/ptr_arithmetic_on_null/type_conflict.desc b/regression/cbmc/ptr_arithmetic_on_null/type_conflict.desc
index c7a44b02a42..0f5cbf5fcea 100644
--- a/regression/cbmc/ptr_arithmetic_on_null/type_conflict.desc
+++ b/regression/cbmc/ptr_arithmetic_on_null/type_conflict.desc
@@ -1,4 +1,4 @@
-CORE gcc-only no-new-smt
+CORE gcc-only
 main.c
 -DMISSING_CAST
 pointer subtraction over different types