diff --git a/regression/cbmc/Bool/bool2.desc b/regression/cbmc/Bool/bool2.desc
index e298f35dce1..e1e55611867 100644
--- a/regression/cbmc/Bool/bool2.desc
+++ b/regression/cbmc/Bool/bool2.desc
@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 bool2.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Bool/bool3.desc b/regression/cbmc/Bool/bool3.desc
index 2cd8843c88c..ab33f1f0312 100644
--- a/regression/cbmc/Bool/bool3.desc
+++ b/regression/cbmc/Bool/bool3.desc
@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 bool3.c
 --json-ui
 ^EXIT=10$
diff --git a/regression/cbmc/c99_Bool/test.desc b/regression/cbmc/c99_Bool/test.desc
index 9afc07ce007..a454c448ed0 100644
--- a/regression/cbmc/c99_Bool/test.desc
+++ b/regression/cbmc/c99_Bool/test.desc
@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 main.c
 --function foo
 ^EXIT=0$
diff --git a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp
index d5910628470..97dfa97bb43 100644
--- a/src/solvers/smt2_incremental/convert_expr_to_smt.cpp
+++ b/src/solvers/smt2_incremental/convert_expr_to_smt.cpp
@@ -167,6 +167,8 @@ extension_for_type(const typet &type)
     return smt_bit_vector_theoryt::zero_extend;
   if(can_cast_type<pointer_typet>(type))
     return smt_bit_vector_theoryt::zero_extend;
+  if(can_cast_type<c_bool_typet>(type))
+    return smt_bit_vector_theoryt::zero_extend;
   UNREACHABLE;
 }