diff --git a/regression/cbmc/Initialization6/test.desc b/regression/cbmc/Initialization6/test.desc
index 028f7170892..33900ad2b78 100644
--- a/regression/cbmc/Initialization6/test.desc
+++ b/regression/cbmc/Initialization6/test.desc
@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 main.c
 
 ^EXIT=10$
diff --git a/regression/cbmc/Pointer_byte_extract4/program-only.desc b/regression/cbmc/Pointer_byte_extract4/program-only.desc
index c3b3f95041f..7b738a3b40b 100644
--- a/regression/cbmc/Pointer_byte_extract4/program-only.desc
+++ b/regression/cbmc/Pointer_byte_extract4/program-only.desc
@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Pointer_byte_extract4/test.desc b/regression/cbmc/Pointer_byte_extract4/test.desc
index 1c039664a91..9efefbc7362 100644
--- a/regression/cbmc/Pointer_byte_extract4/test.desc
+++ b/regression/cbmc/Pointer_byte_extract4/test.desc
@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/byte_extract1/test.desc b/regression/cbmc/byte_extract1/test.desc
index ecf6bd304bc..d80821ffede 100644
--- a/regression/cbmc/byte_extract1/test.desc
+++ b/regression/cbmc/byte_extract1/test.desc
@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 main.c
 
 ^EXIT=10$
diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
index 0d8a91a6f89..f4ada079d0f 100644
--- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
+++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
@@ -111,6 +111,10 @@ void smt2_incremental_decision_proceduret::initialize_array_elements(
   identifier_table.emplace(array_identifier.identifier(), array_identifier);
   const std::vector<exprt> &elements = array.operands();
   const typet &index_type = array.type().index_type();
+  for(const auto &element : elements)
+  {
+    define_dependent_functions(element);
+  }
   for(std::size_t i = 0; i < elements.size(); ++i)
   {
     const smt_termt index = convert_expr_to_smt(from_integer(i, index_type));
@@ -125,6 +129,7 @@ void smt2_incremental_decision_proceduret::initialize_array_elements(
   const array_of_exprt &array,
   const smt_identifier_termt &array_identifier)
 {
+  define_dependent_functions(array.what());
   const smt_sortt index_type =
     convert_type_to_smt_sort(array.type().index_type());
   const smt_identifier_termt array_index_identifier{
@@ -170,6 +175,8 @@ void send_function_definition(
     &expression_identifiers,
   std::unordered_map<irep_idt, smt_identifier_termt> &identifier_table)
 {
+  if(identifier_table.count(symbol_identifier))
+    return;
   const smt_declare_function_commandt function{
     smt_identifier_termt(
       symbol_identifier, convert_type_to_smt_sort(expr.type())),
@@ -342,6 +349,8 @@ void smt2_incremental_decision_proceduret::define_index_identifiers(
       if(const auto with_expr = expr_try_dynamic_cast<with_exprt>(expr_node))
       {
         const auto index_expr = with_expr->where();
+        if(expression_identifiers.count(index_expr))
+          return;
         const auto index_term = convert_expr_to_smt(index_expr);
         const auto index_identifier =
           "index_" + std::to_string(index_sequence());