diff --git a/regression/cbmc/array-cell-sensitivity12/test_execution.desc b/regression/cbmc/array-cell-sensitivity12/test_execution.desc
index 70141323480..d33e4045438 100644
--- a/regression/cbmc/array-cell-sensitivity12/test_execution.desc
+++ b/regression/cbmc/array-cell-sensitivity12/test_execution.desc
@@ -1,4 +1,4 @@
-CORE no-new-smt
+CORE
 test.c
 
 ^VERIFICATION FAILED$
diff --git a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
index 0d8a91a6f89..00cfcf0bab2 100644
--- a/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
+++ b/src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp
@@ -377,6 +377,7 @@ smt_termt
 smt2_incremental_decision_proceduret::convert_expr_to_smt(const exprt &expr)
 {
   define_index_identifiers(expr);
+  define_dependent_functions(expr);
   const exprt substituted = substitute_defined_padding(
     substitute_identifiers(expr, expression_identifiers));
   track_expression_objects(substituted, ns, object_map);