diff --git a/src/ansi-c/goto-conversion/builtin_functions.cpp b/src/ansi-c/goto-conversion/builtin_functions.cpp
index ea6c30d173d..bf864fcdb1e 100644
--- a/src/ansi-c/goto-conversion/builtin_functions.cpp
+++ b/src/ansi-c/goto-conversion/builtin_functions.cpp
@@ -401,7 +401,7 @@ void goto_convertt::do_cpp_new(
   bool new_array = rhs.get(ID_statement) == ID_cpp_new_array;
 
   exprt count;
-  needs_destructiont new_vars;
+  clean_expr_resultt side_effects;
 
   if(new_array)
   {
@@ -409,7 +409,8 @@ void goto_convertt::do_cpp_new(
       static_cast<const exprt &>(rhs.find(ID_size)), object_size.type());
 
     // might have side-effect
-    new_vars.add(clean_expr(count, dest, ID_cpp));
+    side_effects.add(clean_expr(count, ID_cpp));
+    dest.destructive_append(side_effects.side_effects);
   }
 
   exprt tmp_symbol_expr;
@@ -495,9 +496,8 @@ void goto_convertt::do_cpp_new(
     typecast_exprt(tmp_symbol_expr, lhs.type()),
     rhs.find_source_location()));
 
-  new_vars.minimal_scope.push_front(
-    to_symbol_expr(tmp_symbol_expr).get_identifier());
-  destruct_locals(new_vars.minimal_scope, dest, ns);
+  side_effects.add_temporary(to_symbol_expr(tmp_symbol_expr).get_identifier());
+  destruct_locals(side_effects.temporaries, dest, ns);
 
   // grab initializer
   goto_programt tmp_initializer;
diff --git a/src/ansi-c/goto-conversion/goto_clean_expr.cpp b/src/ansi-c/goto-conversion/goto_clean_expr.cpp
index d5569bb4b33..c015c1fe414 100644
--- a/src/ansi-c/goto-conversion/goto_clean_expr.cpp
+++ b/src/ansi-c/goto-conversion/goto_clean_expr.cpp
@@ -166,9 +166,8 @@ void goto_convertt::rewrite_boolean(exprt &expr)
   expr.swap(tmp);
 }
 
-goto_convertt::needs_destructiont goto_convertt::clean_expr(
+goto_convertt::clean_expr_resultt goto_convertt::clean_expr(
   exprt &expr,
-  goto_programt &dest,
   const irep_idt &mode,
   bool result_is_used)
 {
@@ -189,20 +188,20 @@ goto_convertt::needs_destructiont goto_convertt::clean_expr(
     rewrite_boolean(expr);
 
     // recursive call
-    return clean_expr(expr, dest, mode, result_is_used);
+    return clean_expr(expr, mode, result_is_used);
   }
   else if(expr.id() == ID_if)
   {
     // first clean condition
-    needs_destructiont new_vars =
-      clean_expr(to_if_expr(expr).cond(), dest, mode, true);
+    clean_expr_resultt side_effects =
+      clean_expr(to_if_expr(expr).cond(), mode, true);
 
     // possibly done now
     if(
       !needs_cleaning(to_if_expr(expr).true_case()) &&
       !needs_cleaning(to_if_expr(expr).false_case()))
     {
-      return new_vars;
+      return side_effects;
     }
 
     // copy expression
@@ -236,30 +235,32 @@ goto_convertt::needs_destructiont goto_convertt::clean_expr(
     }
 #endif
 
-    goto_programt tmp_true;
-    new_vars.add(
-      clean_expr(if_expr.true_case(), tmp_true, mode, result_is_used));
+    clean_expr_resultt tmp_true(
+      clean_expr(if_expr.true_case(), mode, result_is_used));
 
-    goto_programt tmp_false;
-    new_vars.add(
-      clean_expr(if_expr.false_case(), tmp_false, mode, result_is_used));
+    clean_expr_resultt tmp_false(
+      clean_expr(if_expr.false_case(), mode, result_is_used));
 
     if(result_is_used)
     {
-      symbolt &new_symbol =
-        new_tmp_symbol(expr.type(), "if_expr", dest, source_location, mode);
+      symbolt &new_symbol = new_tmp_symbol(
+        expr.type(),
+        "if_expr",
+        side_effects.side_effects,
+        source_location,
+        mode);
 
       code_assignt assignment_true;
       assignment_true.lhs() = new_symbol.symbol_expr();
       assignment_true.rhs() = if_expr.true_case();
       assignment_true.add_source_location() = source_location;
-      convert(assignment_true, tmp_true, mode);
+      convert(assignment_true, tmp_true.side_effects, mode);
 
       code_assignt assignment_false;
       assignment_false.lhs() = new_symbol.symbol_expr();
       assignment_false.rhs() = if_expr.false_case();
       assignment_false.add_source_location() = source_location;
-      convert(assignment_false, tmp_false, mode);
+      convert(assignment_false, tmp_false.side_effects, mode);
 
       // overwrites expr
       expr = new_symbol.symbol_expr();
@@ -273,7 +274,7 @@ goto_convertt::needs_destructiont goto_convertt::clean_expr(
         // expression is just a constant
         code_expressiont code_expression(
           typecast_exprt(if_expr.true_case(), empty_typet()));
-        convert(code_expression, tmp_true, mode);
+        convert(code_expression, tmp_true.side_effects, mode);
       }
 
       if(if_expr.false_case().is_not_nil())
@@ -282,7 +283,7 @@ goto_convertt::needs_destructiont goto_convertt::clean_expr(
         // expression is just a constant
         code_expressiont code_expression(
           typecast_exprt(if_expr.false_case(), empty_typet()));
-        convert(code_expression, tmp_false, mode);
+        convert(code_expression, tmp_false.side_effects, mode);
       }
 
       expr = nil_exprt();
@@ -292,24 +293,26 @@ goto_convertt::needs_destructiont goto_convertt::clean_expr(
     generate_ifthenelse(
       if_expr.cond(),
       source_location,
-      tmp_true,
+      tmp_true.side_effects,
       if_expr.true_case().source_location(),
-      tmp_false,
+      tmp_false.side_effects,
       if_expr.false_case().source_location(),
-      dest,
+      side_effects.side_effects,
       mode);
 
-    destruct_locals(new_vars.minimal_scope, dest, ns);
-    new_vars.minimal_scope.clear();
+    destruct_locals(tmp_false.temporaries, side_effects.side_effects, ns);
+    destruct_locals(tmp_true.temporaries, side_effects.side_effects, ns);
+    destruct_locals(side_effects.temporaries, side_effects.side_effects, ns);
+    side_effects.temporaries.clear();
 
     if(expr.is_not_nil())
-      new_vars.minimal_scope.push_front(to_symbol_expr(expr).get_identifier());
+      side_effects.add_temporary(to_symbol_expr(expr).get_identifier());
 
-    return new_vars;
+    return side_effects;
   }
   else if(expr.id() == ID_comma)
   {
-    needs_destructiont new_vars;
+    clean_expr_resultt side_effects;
 
     if(result_is_used)
     {
@@ -323,15 +326,15 @@ goto_convertt::needs_destructiont goto_convertt::clean_expr(
         if(last)
         {
           result.swap(*it);
-          new_vars.add(clean_expr(result, dest, mode, true));
+          side_effects.add(clean_expr(result, mode, true));
         }
         else
         {
-          new_vars.add(clean_expr(*it, dest, mode, false));
+          side_effects.add(clean_expr(*it, mode, false));
 
           // remember these for later checks
           if(it->is_not_nil())
-            convert(code_expressiont(*it), dest, mode);
+            convert(code_expressiont(*it), side_effects.side_effects, mode);
         }
       }
 
@@ -341,30 +344,30 @@ goto_convertt::needs_destructiont goto_convertt::clean_expr(
     {
       Forall_operands(it, expr)
       {
-        new_vars.add(clean_expr(*it, dest, mode, false));
+        side_effects.add(clean_expr(*it, mode, false));
 
         // remember as expression statement for later checks
         if(it->is_not_nil())
-          convert(code_expressiont(*it), dest, mode);
+          convert(code_expressiont(*it), side_effects.side_effects, mode);
       }
 
       expr = nil_exprt();
     }
 
-    return new_vars;
+    return side_effects;
   }
   else if(expr.id() == ID_typecast)
   {
     typecast_exprt &typecast = to_typecast_expr(expr);
 
     // preserve 'result_is_used'
-    needs_destructiont new_vars =
-      clean_expr(typecast.op(), dest, mode, result_is_used);
+    clean_expr_resultt side_effects =
+      clean_expr(typecast.op(), mode, result_is_used);
 
     if(typecast.op().is_nil())
       expr.make_nil();
 
-    return new_vars;
+    return side_effects;
   }
   else if(expr.id() == ID_side_effect)
   {
@@ -374,14 +377,14 @@ goto_convertt::needs_destructiont goto_convertt::clean_expr(
     if(statement == ID_gcc_conditional_expression)
     {
       // need to do separately
-      return remove_gcc_conditional_expression(expr, dest, mode);
+      return remove_gcc_conditional_expression(expr, mode);
     }
     else if(statement == ID_statement_expression)
     {
       // need to do separately to prevent that
       // the operands of expr get 'cleaned'
       return remove_statement_expression(
-        to_side_effect_expr(expr), dest, mode, result_is_used);
+        to_side_effect_expr(expr), mode, result_is_used);
     }
     else if(statement == ID_assign)
     {
@@ -397,16 +400,15 @@ goto_convertt::needs_destructiont goto_convertt::clean_expr(
         to_side_effect_expr(side_effect_assign.rhs()).get_statement() ==
           ID_function_call)
       {
-        needs_destructiont new_vars =
-          clean_expr(side_effect_assign.lhs(), dest, mode);
+        clean_expr_resultt side_effects =
+          clean_expr(side_effect_assign.lhs(), mode);
         exprt lhs = side_effect_assign.lhs();
 
         const bool must_use_rhs = assignment_lhs_needs_temporary(lhs);
         if(must_use_rhs)
         {
-          new_vars.add(remove_function_call(
+          side_effects.add(remove_function_call(
             to_side_effect_expr_function_call(side_effect_assign.rhs()),
-            dest,
             mode,
             true));
         }
@@ -417,14 +419,14 @@ goto_convertt::needs_destructiont goto_convertt::clean_expr(
           side_effect_assign.rhs(), new_lhs.type());
         code_assignt assignment(std::move(new_lhs), new_rhs);
         assignment.add_source_location() = expr.source_location();
-        convert_assign(assignment, dest, mode);
+        convert_assign(assignment, side_effects.side_effects, mode);
 
         if(result_is_used)
           expr = must_use_rhs ? new_rhs : lhs;
         else
           expr.make_nil();
 
-        return new_vars;
+        return side_effects;
       }
     }
   }
@@ -437,20 +439,20 @@ goto_convertt::needs_destructiont goto_convertt::clean_expr(
   else if(expr.id() == ID_address_of)
   {
     address_of_exprt &addr = to_address_of_expr(expr);
-    return clean_expr_address_of(addr.object(), dest, mode);
+    return clean_expr_address_of(addr.object(), mode);
   }
 
-  needs_destructiont new_vars;
+  clean_expr_resultt side_effects;
 
   // TODO: evaluation order
 
   Forall_operands(it, expr)
-    new_vars.add(clean_expr(*it, dest, mode));
+    side_effects.add(clean_expr(*it, mode));
 
   if(expr.id() == ID_side_effect)
   {
-    new_vars.add(remove_side_effect(
-      to_side_effect_expr(expr), dest, mode, result_is_used, false));
+    side_effects.add(remove_side_effect(
+      to_side_effect_expr(expr), mode, result_is_used, false));
   }
   else if(expr.id() == ID_compound_literal)
   {
@@ -460,15 +462,13 @@ goto_convertt::needs_destructiont goto_convertt::clean_expr(
     expr = to_unary_expr(expr).op();
   }
 
-  return new_vars;
+  return side_effects;
 }
 
-goto_convertt::needs_destructiont goto_convertt::clean_expr_address_of(
-  exprt &expr,
-  goto_programt &dest,
-  const irep_idt &mode)
+goto_convertt::clean_expr_resultt
+goto_convertt::clean_expr_address_of(exprt &expr, const irep_idt &mode)
 {
-  needs_destructiont new_vars;
+  clean_expr_resultt side_effects;
 
   // The address of object constructors can be taken,
   // which is re-written into the address of a variable.
@@ -477,8 +477,9 @@ goto_convertt::needs_destructiont goto_convertt::clean_expr_address_of(
   {
     DATA_INVARIANT(
       expr.operands().size() == 1, "ID_compound_literal has a single operand");
-    new_vars.add(clean_expr(to_unary_expr(expr).op(), dest, mode));
-    expr = make_compound_literal(to_unary_expr(expr).op(), dest, mode);
+    side_effects.add(clean_expr(to_unary_expr(expr).op(), mode));
+    expr = make_compound_literal(
+      to_unary_expr(expr).op(), side_effects.side_effects, mode);
   }
   else if(expr.id() == ID_string_constant)
   {
@@ -488,13 +489,13 @@ goto_convertt::needs_destructiont goto_convertt::clean_expr_address_of(
   else if(expr.id() == ID_index)
   {
     index_exprt &index_expr = to_index_expr(expr);
-    new_vars.add(clean_expr_address_of(index_expr.array(), dest, mode));
-    new_vars.add(clean_expr(index_expr.index(), dest, mode));
+    side_effects.add(clean_expr_address_of(index_expr.array(), mode));
+    side_effects.add(clean_expr(index_expr.index(), mode));
   }
   else if(expr.id() == ID_dereference)
   {
     dereference_exprt &deref_expr = to_dereference_expr(expr);
-    new_vars.add(clean_expr(deref_expr.pointer(), dest, mode));
+    side_effects.add(clean_expr(deref_expr.pointer(), mode));
   }
   else if(expr.id() == ID_comma)
   {
@@ -512,44 +513,43 @@ goto_convertt::needs_destructiont goto_convertt::clean_expr_address_of(
         result.swap(*it);
       else
       {
-        new_vars.add(clean_expr(*it, dest, mode, false));
+        side_effects.add(clean_expr(*it, mode, false));
 
         // get any side-effects
         if(it->is_not_nil())
-          convert(code_expressiont(*it), dest, mode);
+          convert(code_expressiont(*it), side_effects.side_effects, mode);
       }
     }
 
     expr.swap(result);
 
     // do again
-    new_vars.add(clean_expr_address_of(expr, dest, mode));
+    side_effects.add(clean_expr_address_of(expr, mode));
   }
   else if(expr.id() == ID_side_effect)
   {
-    new_vars.add(
-      remove_side_effect(to_side_effect_expr(expr), dest, mode, true, true));
+    side_effects.add(
+      remove_side_effect(to_side_effect_expr(expr), mode, true, true));
   }
   else
     Forall_operands(it, expr)
-      new_vars.add(clean_expr_address_of(*it, dest, mode));
+      side_effects.add(clean_expr_address_of(*it, mode));
 
-  return new_vars;
+  return side_effects;
 }
 
-goto_convertt::needs_destructiont
+goto_convertt::clean_expr_resultt
 goto_convertt::remove_gcc_conditional_expression(
   exprt &expr,
-  goto_programt &dest,
   const irep_idt &mode)
 {
-  needs_destructiont new_vars;
+  clean_expr_resultt side_effects;
 
   {
     auto &binary_expr = to_binary_expr(expr);
 
     // first remove side-effects from condition
-    new_vars = clean_expr(to_binary_expr(expr).op0(), dest, mode);
+    side_effects = clean_expr(to_binary_expr(expr).op0(), mode);
 
     // now we can copy op0 safely
     if_exprt if_expr(
@@ -563,7 +563,7 @@ goto_convertt::remove_gcc_conditional_expression(
   }
 
   // there might still be junk in expr.op2()
-  new_vars.add(clean_expr(expr, dest, mode));
+  side_effects.add(clean_expr(expr, mode));
 
-  return new_vars;
+  return side_effects;
 }
diff --git a/src/ansi-c/goto-conversion/goto_convert.cpp b/src/ansi-c/goto-conversion/goto_convert.cpp
index ebe6286b6cd..d8b0db12aa8 100644
--- a/src/ansi-c/goto-conversion/goto_convert.cpp
+++ b/src/ansi-c/goto-conversion/goto_convert.cpp
@@ -761,7 +761,8 @@ void goto_convertt::convert_expression(
   else
   {
     // result _not_ used
-    needs_destructiont new_vars = clean_expr(expr, dest, mode, false);
+    clean_expr_resultt side_effects = clean_expr(expr, mode, false);
+    dest.destructive_append(side_effects.side_effects);
 
     // Any residual expression?
     // We keep it to add checks later.
@@ -773,7 +774,7 @@ void goto_convertt::convert_expression(
       copy(tmp, OTHER, dest);
     }
 
-    destruct_locals(new_vars.minimal_scope, dest, ns);
+    destruct_locals(side_effects.temporaries, dest, ns);
   }
 }
 
@@ -809,7 +810,8 @@ void goto_convertt::convert_frontend_decl(
     const auto declaration_iterator = std::prev(dest.instructions.end());
 
     auto initializer_location = initializer.find_source_location();
-    needs_destructiont new_vars = clean_expr(initializer, dest, mode);
+    clean_expr_resultt side_effects = clean_expr(initializer, mode);
+    dest.destructive_append(side_effects.side_effects);
 
     if(initializer.is_not_nil())
     {
@@ -819,7 +821,7 @@ void goto_convertt::convert_frontend_decl(
       convert_assign(assign, dest, mode);
     }
 
-    destruct_locals(new_vars.minimal_scope, dest, ns);
+    destruct_locals(side_effects.temporaries, dest, ns);
 
     return declaration_iterator;
   }();
@@ -860,7 +862,8 @@ void goto_convertt::convert_assign(
 {
   exprt lhs = code.lhs(), rhs = code.rhs();
 
-  needs_destructiont new_vars = clean_expr(lhs, dest, mode);
+  clean_expr_resultt side_effects = clean_expr(lhs, mode);
+  dest.destructive_append(side_effects.side_effects);
 
   if(rhs.id() == ID_side_effect && rhs.get(ID_statement) == ID_function_call)
   {
@@ -872,7 +875,10 @@ void goto_convertt::convert_assign(
       rhs.find_source_location());
 
     Forall_operands(it, rhs)
-      new_vars.add(clean_expr(*it, dest, mode));
+    {
+      side_effects.add(clean_expr(*it, mode));
+      dest.destructive_append(side_effects.side_effects);
+    }
 
     do_function_call(
       lhs,
@@ -886,7 +892,10 @@ void goto_convertt::convert_assign(
                                    rhs.get(ID_statement) == ID_cpp_new_array))
   {
     Forall_operands(it, rhs)
-      new_vars.add(clean_expr(*it, dest, mode));
+    {
+      side_effects.add(clean_expr(*it, mode));
+      dest.destructive_append(side_effects.side_effects);
+    }
 
     // TODO: This should be done in a separate pass
     do_cpp_new(lhs, to_side_effect_expr(rhs), dest);
@@ -900,7 +909,8 @@ void goto_convertt::convert_assign(
      rhs.get(ID_statement) == ID_gcc_conditional_expression))
   {
     // handle above side effects
-    new_vars.add(clean_expr(rhs, dest, mode));
+    side_effects.add(clean_expr(rhs, mode));
+    dest.destructive_append(side_effects.side_effects);
 
     code_assignt new_assign(code);
     new_assign.lhs() = lhs;
@@ -913,7 +923,10 @@ void goto_convertt::convert_assign(
     // preserve side effects that will be handled at later stages,
     // such as allocate, new operators of other languages, e.g. java, etc
     Forall_operands(it, rhs)
-      new_vars.add(clean_expr(*it, dest, mode));
+    {
+      side_effects.add(clean_expr(*it, mode));
+      dest.destructive_append(side_effects.side_effects);
+    }
 
     code_assignt new_assign(code);
     new_assign.lhs() = lhs;
@@ -924,7 +937,8 @@ void goto_convertt::convert_assign(
   else
   {
     // do everything else
-    new_vars.add(clean_expr(rhs, dest, mode));
+    side_effects.add(clean_expr(rhs, mode));
+    dest.destructive_append(side_effects.side_effects);
 
     code_assignt new_assign(code);
     new_assign.lhs() = lhs;
@@ -933,7 +947,7 @@ void goto_convertt::convert_assign(
     copy(new_assign, ASSIGN, dest);
   }
 
-  destruct_locals(new_vars.minimal_scope, dest, ns);
+  destruct_locals(side_effects.temporaries, dest, ns);
 }
 
 void goto_convertt::convert_cpp_delete(const codet &code, goto_programt &dest)
@@ -945,7 +959,8 @@ void goto_convertt::convert_cpp_delete(const codet &code, goto_programt &dest)
 
   exprt tmp_op = code.op0();
 
-  needs_destructiont new_vars = clean_expr(tmp_op, dest, ID_cpp);
+  clean_expr_resultt side_effects = clean_expr(tmp_op, ID_cpp);
+  dest.destructive_append(side_effects.side_effects);
 
   // we call the destructor, and then free
   const exprt &destructor =
@@ -995,7 +1010,7 @@ void goto_convertt::convert_cpp_delete(const codet &code, goto_programt &dest)
 
   convert(delete_call, dest, ID_cpp);
 
-  destruct_locals(new_vars.minimal_scope, dest, ns);
+  destruct_locals(side_effects.temporaries, dest, ns);
 }
 
 void goto_convertt::convert_assert(
@@ -1005,13 +1020,14 @@ void goto_convertt::convert_assert(
 {
   exprt cond = code.assertion();
 
-  needs_destructiont new_vars = clean_expr(cond, dest, mode);
+  clean_expr_resultt side_effects = clean_expr(cond, mode);
+  dest.destructive_append(side_effects.side_effects);
 
   source_locationt annotated_location = code.source_location();
   annotated_location.set("user-provided", true);
   dest.add(goto_programt::make_assertion(cond, annotated_location));
 
-  destruct_locals(new_vars.minimal_scope, dest, ns);
+  destruct_locals(side_effects.temporaries, dest, ns);
 }
 
 void goto_convertt::convert_skip(const codet &code, goto_programt &dest)
@@ -1027,11 +1043,12 @@ void goto_convertt::convert_assume(
 {
   exprt op = code.assumption();
 
-  needs_destructiont new_vars = clean_expr(op, dest, mode);
+  clean_expr_resultt side_effects = clean_expr(op, mode);
+  dest.destructive_append(side_effects.side_effects);
 
   dest.add(goto_programt::make_assumption(op, code.source_location()));
 
-  destruct_locals(new_vars.minimal_scope, dest, ns);
+  destruct_locals(side_effects.temporaries, dest, ns);
 }
 
 void goto_convertt::convert_loop_contracts(
@@ -1099,23 +1116,22 @@ void goto_convertt::convert_for(
 
   exprt cond = code.cond();
 
-  goto_programt sideeffects;
-  needs_destructiont new_vars = clean_expr(cond, sideeffects, mode);
+  clean_expr_resultt side_effects = clean_expr(cond, mode);
 
   // save break/continue targets
   break_continue_targetst old_targets(targets);
 
   // do the u label
-  goto_programt::targett u = sideeffects.instructions.begin();
+  goto_programt::targett u = side_effects.side_effects.instructions.begin();
 
   // do the v label
   goto_programt tmp_v;
   goto_programt::targett v = tmp_v.add(goto_programt::instructiont());
-  destruct_locals(new_vars.minimal_scope, tmp_v, ns);
+  destruct_locals(side_effects.temporaries, tmp_v, ns);
 
   // do the z and Z labels
   goto_programt tmp_z;
-  destruct_locals(new_vars.minimal_scope, tmp_z, ns);
+  destruct_locals(side_effects.temporaries, tmp_z, ns);
   goto_programt::targett z =
     tmp_z.add(goto_programt::make_skip(code.source_location()));
   goto_programt::targett Z = tmp_z.instructions.begin();
@@ -1131,15 +1147,16 @@ void goto_convertt::convert_for(
   {
     exprt tmp_B = code.iter();
 
-    needs_destructiont new_vars_iter = clean_expr(tmp_B, tmp_x, mode, false);
-    destruct_locals(new_vars_iter.minimal_scope, tmp_x, ns);
+    clean_expr_resultt side_effects_iter = clean_expr(tmp_B, mode, false);
+    tmp_x.destructive_append(side_effects_iter.side_effects);
+    destruct_locals(side_effects_iter.temporaries, tmp_x, ns);
 
     if(tmp_x.instructions.empty())
       tmp_x.add(goto_programt::make_skip(code.source_location()));
   }
 
   // optimize the v label
-  if(sideeffects.instructions.empty())
+  if(side_effects.side_effects.instructions.empty())
     u = v;
 
   // set the targets
@@ -1162,7 +1179,7 @@ void goto_convertt::convert_for(
   // assigns clause, loop invariant and decreases clause
   convert_loop_contracts(code, y);
 
-  dest.destructive_append(sideeffects);
+  dest.destructive_append(side_effects.side_effects);
   dest.destructive_append(tmp_v);
   dest.destructive_append(tmp_w);
   dest.destructive_append(tmp_x);
@@ -1244,8 +1261,7 @@ void goto_convertt::convert_dowhile(
 
   exprt cond = code.cond();
 
-  goto_programt sideeffects;
-  needs_destructiont new_vars = clean_expr(cond, sideeffects, mode);
+  clean_expr_resultt side_effects = clean_expr(cond, mode);
 
   //    do P while(c);
   //--------------------
@@ -1264,13 +1280,13 @@ void goto_convertt::convert_dowhile(
   goto_programt tmp_y;
   goto_programt::targett y = tmp_y.add(goto_programt::make_incomplete_goto(
     boolean_negate(cond), condition_location));
-  destruct_locals(new_vars.minimal_scope, tmp_y, ns);
+  destruct_locals(side_effects.temporaries, tmp_y, ns);
   goto_programt::targett W = tmp_y.add(
     goto_programt::make_incomplete_goto(true_exprt{}, condition_location));
 
   // do the z label and C labels
   goto_programt tmp_z;
-  destruct_locals(new_vars.minimal_scope, tmp_z, ns);
+  destruct_locals(side_effects.temporaries, tmp_z, ns);
   goto_programt::targett z =
     tmp_z.add(goto_programt::make_skip(code.source_location()));
   goto_programt::targett C = tmp_z.instructions.begin();
@@ -1280,10 +1296,10 @@ void goto_convertt::convert_dowhile(
 
   // do the x label
   goto_programt::targett x;
-  if(sideeffects.instructions.empty())
+  if(side_effects.side_effects.instructions.empty())
     x = y;
   else
-    x = sideeffects.instructions.begin();
+    x = side_effects.side_effects.instructions.begin();
 
   // set the targets
   targets.set_break(z);
@@ -1301,7 +1317,7 @@ void goto_convertt::convert_dowhile(
   convert_loop_contracts(code, y);
 
   dest.destructive_append(tmp_w);
-  dest.destructive_append(sideeffects);
+  dest.destructive_append(side_effects.side_effects);
   dest.destructive_append(tmp_y);
   dest.destructive_append(tmp_z);
 
@@ -1373,8 +1389,7 @@ void goto_convertt::convert_switch(
   // do the value we switch over
   exprt argument = code.value();
 
-  goto_programt sideeffects;
-  needs_destructiont new_vars = clean_expr(argument, sideeffects, mode);
+  clean_expr_resultt side_effects = clean_expr(argument, mode);
 
   // Avoid potential performance penalties caused by evaluating the value
   // multiple times (as the below chain-of-ifs does). "needs_cleaning" isn't
@@ -1386,17 +1401,16 @@ void goto_convertt::convert_switch(
     symbolt &new_symbol = new_tmp_symbol(
       argument.type(),
       "switch_value",
-      sideeffects,
+      side_effects.side_effects,
       code.source_location(),
       mode);
 
     code_assignt copy_value{
       new_symbol.symbol_expr(), argument, code.source_location()};
-    convert(copy_value, sideeffects, mode);
+    convert(copy_value, side_effects.side_effects, mode);
 
     argument = new_symbol.symbol_expr();
-    new_vars.minimal_scope.push_front(
-      to_symbol_expr(argument).get_identifier());
+    side_effects.add_temporary(to_symbol_expr(argument).get_identifier());
   }
 
   // save break/default/cases targets
@@ -1444,7 +1458,7 @@ void goto_convertt::convert_switch(
     source_location.set_case_number(std::to_string(case_number));
     case_number++;
 
-    if(new_vars.minimal_scope.empty())
+    if(side_effects.temporaries.empty())
     {
       guard_expr.add_source_location() = source_location;
 
@@ -1459,7 +1473,7 @@ void goto_convertt::convert_switch(
       goto_programt::targett try_next =
         tmp_cases.add(goto_programt::make_incomplete_goto(
           std::move(guard_expr), source_location));
-      destruct_locals(new_vars.minimal_scope, tmp_cases, ns);
+      destruct_locals(side_effects.temporaries, tmp_cases, ns);
       tmp_cases.add(goto_programt::make_goto(
         case_pair.first, true_exprt{}, source_location));
       goto_programt::targett next_case =
@@ -1471,7 +1485,7 @@ void goto_convertt::convert_switch(
   tmp_cases.add(goto_programt::make_goto(
     targets.default_target, targets.default_target->source_location()));
 
-  dest.destructive_append(sideeffects);
+  dest.destructive_append(side_effects.side_effects);
   dest.destructive_append(tmp_cases);
   dest.destructive_append(tmp);
   dest.destructive_append(tmp_z);
@@ -1514,16 +1528,14 @@ void goto_convertt::convert_return(
     code.find_source_location());
 
   code_frontend_returnt new_code(code);
-  needs_destructiont new_vars;
+  clean_expr_resultt side_effects;
 
   if(new_code.has_return_value())
   {
     bool result_is_used = new_code.return_value().type().id() != ID_empty;
 
-    goto_programt sideeffects;
-    new_vars =
-      clean_expr(new_code.return_value(), sideeffects, mode, result_is_used);
-    dest.destructive_append(sideeffects);
+    side_effects = clean_expr(new_code.return_value(), mode, result_is_used);
+    dest.destructive_append(side_effects.side_effects);
 
     // remove void-typed return value
     if(!result_is_used)
@@ -1540,7 +1552,7 @@ void goto_convertt::convert_return(
     // Now add a 'set return value' instruction to set the return value.
     dest.add(goto_programt::make_set_return_value(
       new_code.return_value(), new_code.source_location()));
-    destruct_locals(new_vars.minimal_scope, dest, ns);
+    destruct_locals(side_effects.temporaries, dest, ns);
   }
   else
   {
@@ -1673,11 +1685,12 @@ void goto_convertt::convert_ifthenelse(
   }
 
   exprt tmp_guard = code.cond();
-  needs_destructiont new_vars = clean_expr(tmp_guard, dest, mode);
+  clean_expr_resultt side_effects = clean_expr(tmp_guard, mode);
+  dest.destructive_append(side_effects.side_effects);
 
   // convert 'then'-branch
   goto_programt tmp_then;
-  destruct_locals(new_vars.minimal_scope, tmp_then, ns);
+  destruct_locals(side_effects.temporaries, tmp_then, ns);
   convert(code.then_case(), tmp_then, mode);
   source_locationt then_end_location =
     code.then_case().get_statement() == ID_block
@@ -1685,7 +1698,7 @@ void goto_convertt::convert_ifthenelse(
       : code.then_case().source_location();
 
   goto_programt tmp_else;
-  destruct_locals(new_vars.minimal_scope, tmp_else, ns);
+  destruct_locals(side_effects.temporaries, tmp_else, ns);
   source_locationt else_end_location;
 
   if(has_else)
@@ -1938,13 +1951,14 @@ void goto_convertt::generate_conditional_branch(
   {
     // simple branch
     exprt cond = guard;
-    needs_destructiont new_vars = clean_expr(cond, dest, mode);
+    clean_expr_resultt side_effects = clean_expr(cond, mode);
+    dest.destructive_append(side_effects.side_effects);
 
     dest.add(goto_programt::make_goto(target_true, cond, source_location));
     goto_programt tmp_destruct;
-    destruct_locals(new_vars.minimal_scope, tmp_destruct, ns);
+    destruct_locals(side_effects.temporaries, tmp_destruct, ns);
     dest.insert_before_swap(target_true, tmp_destruct);
-    destruct_locals(new_vars.minimal_scope, dest, ns);
+    destruct_locals(side_effects.temporaries, dest, ns);
   }
 }
 
@@ -2014,17 +2028,18 @@ void goto_convertt::generate_conditional_branch(
   }
 
   exprt cond = guard;
-  needs_destructiont new_vars = clean_expr(cond, dest, mode);
+  clean_expr_resultt side_effects = clean_expr(cond, mode);
+  dest.destructive_append(side_effects.side_effects);
 
   // true branch
   dest.add(goto_programt::make_goto(target_true, cond, source_location));
   goto_programt tmp_destruct;
-  destruct_locals(new_vars.minimal_scope, tmp_destruct, ns);
+  destruct_locals(side_effects.temporaries, tmp_destruct, ns);
   dest.insert_before_swap(target_true, tmp_destruct);
 
   // false branch
   dest.add(goto_programt::make_goto(target_false, source_location));
-  destruct_locals(new_vars.minimal_scope, tmp_destruct, ns);
+  destruct_locals(side_effects.temporaries, tmp_destruct, ns);
   dest.insert_before_swap(target_false, tmp_destruct);
 }
 
diff --git a/src/ansi-c/goto-conversion/goto_convert_class.h b/src/ansi-c/goto-conversion/goto_convert_class.h
index 750eb2a07ac..e124a1dec7f 100644
--- a/src/ansi-c/goto-conversion/goto_convert_class.h
+++ b/src/ansi-c/goto-conversion/goto_convert_class.h
@@ -56,19 +56,22 @@ class goto_convertt : public messaget
   std::string tmp_symbol_prefix;
   lifetimet lifetime = lifetimet::STATIC_GLOBAL;
 
-  struct needs_destructiont
+  struct clean_expr_resultt
   {
-    std::list<irep_idt> minimal_scope;
+    std::list<irep_idt> temporaries;
+    goto_programt side_effects;
 
-    needs_destructiont() = default;
+    clean_expr_resultt() = default;
 
-    explicit needs_destructiont(irep_idt id) : minimal_scope({id})
+    void add(clean_expr_resultt &&other)
     {
+      temporaries.splice(temporaries.begin(), other.temporaries);
+      side_effects.destructive_append(other.side_effects);
     }
 
-    void add(needs_destructiont &&other)
+    void add_temporary(const irep_idt &id)
     {
-      minimal_scope.splice(minimal_scope.begin(), other.minimal_scope);
+      temporaries.push_front(id);
     }
   };
 
@@ -97,14 +100,11 @@ class goto_convertt : public messaget
   // into the program logic
   //
 
-  [[nodiscard]] needs_destructiont clean_expr(
-    exprt &expr,
-    goto_programt &dest,
-    const irep_idt &mode,
-    bool result_is_used = true);
+  [[nodiscard]] clean_expr_resultt
+  clean_expr(exprt &expr, const irep_idt &mode, bool result_is_used = true);
 
-  [[nodiscard]] needs_destructiont
-  clean_expr_address_of(exprt &expr, goto_programt &dest, const irep_idt &mode);
+  [[nodiscard]] clean_expr_resultt
+  clean_expr_address_of(exprt &expr, const irep_idt &mode);
 
   static bool needs_cleaning(const exprt &expr);
 
@@ -125,58 +125,46 @@ class goto_convertt : public messaget
 
   void rewrite_boolean(exprt &dest);
 
-  [[nodiscard]] needs_destructiont remove_side_effect(
+  [[nodiscard]] clean_expr_resultt remove_side_effect(
     side_effect_exprt &expr,
-    goto_programt &dest,
     const irep_idt &mode,
     bool result_is_used,
     bool address_taken);
-  [[nodiscard]] needs_destructiont remove_assignment(
+  [[nodiscard]] clean_expr_resultt remove_assignment(
     side_effect_exprt &expr,
-    goto_programt &dest,
     bool result_is_used,
     bool address_taken,
     const irep_idt &mode);
-  [[nodiscard]] needs_destructiont remove_pre(
+  [[nodiscard]] clean_expr_resultt remove_pre(
     side_effect_exprt &expr,
-    goto_programt &dest,
     bool result_is_used,
     bool address_taken,
     const irep_idt &mode);
-  [[nodiscard]] needs_destructiont remove_post(
+  [[nodiscard]] clean_expr_resultt remove_post(
     side_effect_exprt &expr,
-    goto_programt &dest,
     const irep_idt &mode,
     bool result_is_used);
-  [[nodiscard]] needs_destructiont remove_function_call(
+  [[nodiscard]] clean_expr_resultt remove_function_call(
     side_effect_expr_function_callt &expr,
-    goto_programt &dest,
     const irep_idt &mode,
     bool result_is_used);
-  [[nodiscard]] needs_destructiont remove_cpp_new(
+  [[nodiscard]] clean_expr_resultt
+  remove_cpp_new(side_effect_exprt &expr, bool result_is_used);
+  [[nodiscard]] clean_expr_resultt remove_cpp_delete(side_effect_exprt &expr);
+  [[nodiscard]] clean_expr_resultt remove_malloc(
     side_effect_exprt &expr,
-    goto_programt &dest,
-    bool result_is_used);
-  void remove_cpp_delete(side_effect_exprt &expr, goto_programt &dest);
-  [[nodiscard]] needs_destructiont remove_malloc(
-    side_effect_exprt &expr,
-    goto_programt &dest,
     const irep_idt &mode,
     bool result_is_used);
-  [[nodiscard]] needs_destructiont
-  remove_temporary_object(side_effect_exprt &expr, goto_programt &dest);
-  [[nodiscard]] needs_destructiont remove_statement_expression(
+  [[nodiscard]] clean_expr_resultt
+  remove_temporary_object(side_effect_exprt &expr);
+  [[nodiscard]] clean_expr_resultt remove_statement_expression(
     side_effect_exprt &expr,
-    goto_programt &dest,
     const irep_idt &mode,
     bool result_is_used);
-  [[nodiscard]] needs_destructiont remove_gcc_conditional_expression(
-    exprt &expr,
-    goto_programt &dest,
-    const irep_idt &mode);
-  [[nodiscard]] needs_destructiont remove_overflow(
+  [[nodiscard]] clean_expr_resultt
+  remove_gcc_conditional_expression(exprt &expr, const irep_idt &mode);
+  [[nodiscard]] clean_expr_resultt remove_overflow(
     side_effect_expr_overflowt &expr,
-    goto_programt &dest,
     bool result_is_used,
     const irep_idt &mode);
 
diff --git a/src/ansi-c/goto-conversion/goto_convert_function_call.cpp b/src/ansi-c/goto-conversion/goto_convert_function_call.cpp
index badf8384a26..2fdc5c3e616 100644
--- a/src/ansi-c/goto-conversion/goto_convert_function_call.cpp
+++ b/src/ansi-c/goto-conversion/goto_convert_function_call.cpp
@@ -43,15 +43,17 @@ void goto_convertt::do_function_call(
 
   exprt::operandst new_arguments = arguments;
 
-  needs_destructiont new_vars;
+  clean_expr_resultt side_effects;
 
   if(!new_lhs.is_nil())
-    new_vars.add(clean_expr(new_lhs, dest, mode));
+    side_effects.add(clean_expr(new_lhs, mode));
 
-  new_vars.add(clean_expr(new_function, dest, mode));
+  side_effects.add(clean_expr(new_function, mode));
 
   for(auto &new_argument : new_arguments)
-    new_vars.add(clean_expr(new_argument, dest, mode));
+    side_effects.add(clean_expr(new_argument, mode));
+
+  dest.destructive_append(side_effects.side_effects);
 
   // split on the function
 
@@ -83,7 +85,7 @@ void goto_convertt::do_function_call(
       function.find_source_location());
   }
 
-  destruct_locals(new_vars.minimal_scope, dest, ns);
+  destruct_locals(side_effects.temporaries, dest, ns);
 }
 
 void goto_convertt::do_function_call_if(
diff --git a/src/ansi-c/goto-conversion/goto_convert_side_effect.cpp b/src/ansi-c/goto-conversion/goto_convert_side_effect.cpp
index 61a8587fe0a..28943332d12 100644
--- a/src/ansi-c/goto-conversion/goto_convert_side_effect.cpp
+++ b/src/ansi-c/goto-conversion/goto_convert_side_effect.cpp
@@ -24,9 +24,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "destructor.h"
 
-goto_convertt::needs_destructiont goto_convertt::remove_assignment(
+goto_convertt::clean_expr_resultt goto_convertt::remove_assignment(
   side_effect_exprt &expr,
-  goto_programt &dest,
   bool result_is_used,
   bool address_taken,
   const irep_idt &mode)
@@ -35,7 +34,7 @@ goto_convertt::needs_destructiont goto_convertt::remove_assignment(
 
   std::optional<exprt> replacement_expr_opt;
 
-  needs_destructiont new_vars;
+  clean_expr_resultt side_effects;
 
   if(statement == ID_assign)
   {
@@ -48,8 +47,8 @@ goto_convertt::needs_destructiont goto_convertt::remove_assignment(
     {
       if(!old_assignment.rhs().is_constant())
       {
-        new_vars.minimal_scope.push_front(
-          make_temp_symbol(old_assignment.rhs(), "assign", dest, mode));
+        side_effects.add_temporary(make_temp_symbol(
+          old_assignment.rhs(), "assign", side_effects.side_effects, mode));
       }
 
       replacement_expr_opt =
@@ -61,7 +60,7 @@ goto_convertt::needs_destructiont goto_convertt::remove_assignment(
     code_assignt new_assignment(std::move(new_lhs), std::move(new_rhs));
     new_assignment.add_source_location() = expr.source_location();
 
-    convert_assign(new_assignment, dest, mode);
+    convert_assign(new_assignment, side_effects.side_effects, mode);
   }
   else if(
     statement == ID_assign_plus || statement == ID_assign_minus ||
@@ -120,8 +119,8 @@ goto_convertt::needs_destructiont goto_convertt::remove_assignment(
       result_is_used && !address_taken &&
       assignment_lhs_needs_temporary(binary_expr.op0()))
     {
-      new_vars.minimal_scope.push_front(
-        make_temp_symbol(rhs, "assign", dest, mode));
+      side_effects.add_temporary(
+        make_temp_symbol(rhs, "assign", side_effects.side_effects, mode));
       replacement_expr_opt =
         typecast_exprt::conditional_cast(rhs, new_lhs.type());
     }
@@ -131,7 +130,7 @@ goto_convertt::needs_destructiont goto_convertt::remove_assignment(
     code_assignt assignment(new_lhs, rhs);
     assignment.add_source_location() = expr.source_location();
 
-    convert(assignment, dest, mode);
+    convert(assignment, side_effects.side_effects, mode);
   }
   else
     UNREACHABLE;
@@ -143,10 +142,11 @@ goto_convertt::needs_destructiont goto_convertt::remove_assignment(
       typecast_exprt::conditional_cast(*replacement_expr_opt, expr.type());
     expr.swap(new_lhs);
 
-    return new_vars;
+    return side_effects;
   }
 
-  destruct_locals(new_vars.minimal_scope, dest, ns);
+  destruct_locals(side_effects.temporaries, side_effects.side_effects, ns);
+  side_effects.temporaries.clear();
 
   if(result_is_used)
   {
@@ -173,12 +173,11 @@ goto_convertt::needs_destructiont goto_convertt::remove_assignment(
   else
     expr.make_nil();
 
-  return {};
+  return side_effects;
 }
 
-goto_convertt::needs_destructiont goto_convertt::remove_pre(
+goto_convertt::clean_expr_resultt goto_convertt::remove_pre(
   side_effect_exprt &expr,
-  goto_programt &dest,
   bool result_is_used,
   bool address_taken,
   const irep_idt &mode)
@@ -242,14 +241,15 @@ goto_convertt::needs_destructiont goto_convertt::remove_pre(
 
   const bool cannot_use_lhs =
     result_is_used && !address_taken && assignment_lhs_needs_temporary(lhs);
-  needs_destructiont new_vars;
+  clean_expr_resultt side_effects;
   if(cannot_use_lhs)
-    new_vars.minimal_scope.push_front(make_temp_symbol(rhs, "pre", dest, mode));
+    side_effects.add_temporary(
+      make_temp_symbol(rhs, "pre", side_effects.side_effects, mode));
 
   code_assignt assignment(lhs, rhs);
   assignment.add_source_location() = expr.find_source_location();
 
-  convert(assignment, dest, mode);
+  convert(assignment, side_effects.side_effects, mode);
 
   if(result_is_used)
   {
@@ -268,12 +268,11 @@ goto_convertt::needs_destructiont goto_convertt::remove_pre(
   else
     expr.make_nil();
 
-  return new_vars;
+  return side_effects;
 }
 
-goto_convertt::needs_destructiont goto_convertt::remove_post(
+goto_convertt::clean_expr_resultt goto_convertt::remove_post(
   side_effect_exprt &expr,
-  goto_programt &dest,
   const irep_idt &mode,
   bool result_is_used)
 {
@@ -334,7 +333,7 @@ goto_convertt::needs_destructiont goto_convertt::remove_post(
 
   // fix up the expression, if needed
 
-  needs_destructiont new_vars;
+  clean_expr_resultt side_effects;
 
   if(result_is_used)
   {
@@ -346,32 +345,33 @@ goto_convertt::needs_destructiont goto_convertt::remove_post(
       suffix += "_" + id2string(base_name);
     }
 
-    new_vars.minimal_scope.push_front(
-      make_temp_symbol(tmp, suffix, dest, mode));
+    side_effects.add_temporary(
+      make_temp_symbol(tmp, suffix, side_effects.side_effects, mode));
     expr.swap(tmp);
   }
   else
     expr.make_nil();
 
-  dest.destructive_append(tmp1);
-  dest.destructive_append(tmp2);
+  side_effects.side_effects.destructive_append(tmp1);
+  side_effects.side_effects.destructive_append(tmp2);
 
-  return new_vars;
+  return side_effects;
 }
 
-goto_convertt::needs_destructiont goto_convertt::remove_function_call(
+goto_convertt::clean_expr_resultt goto_convertt::remove_function_call(
   side_effect_expr_function_callt &expr,
-  goto_programt &dest,
   const irep_idt &mode,
   bool result_is_used)
 {
+  clean_expr_resultt side_effects;
+
   if(!result_is_used)
   {
     code_function_callt call(expr.function(), expr.arguments());
     call.add_source_location() = expr.source_location();
-    convert_function_call(call, dest, mode);
+    convert_function_call(call, side_effects.side_effects, mode);
     expr.make_nil();
-    return {};
+    return side_effects;
   }
 
   // get name of function, if available
@@ -398,7 +398,7 @@ goto_convertt::needs_destructiont goto_convertt::remove_function_call(
     symbol_table);
 
   PRECONDITION(expr.type().id() != ID_code);
-  dest.add(
+  side_effects.side_effects.add(
     goto_programt::make_decl(new_symbol.symbol_expr(), new_symbol.location));
 
   {
@@ -406,12 +406,14 @@ goto_convertt::needs_destructiont goto_convertt::remove_function_call(
     code_function_callt call(
       new_symbol.symbol_expr(), expr.function(), expr.arguments());
     call.add_source_location() = new_symbol.location;
-    convert_function_call(call, dest, mode);
+    convert_function_call(call, side_effects.side_effects, mode);
   }
 
   static_cast<exprt &>(expr) = new_symbol.symbol_expr();
 
-  return needs_destructiont{to_symbol_expr(expr).get_identifier()};
+  side_effects.add_temporary(to_symbol_expr(expr).get_identifier());
+
+  return side_effects;
 }
 
 void goto_convertt::replace_new_object(const exprt &object, exprt &dest)
@@ -423,10 +425,8 @@ void goto_convertt::replace_new_object(const exprt &object, exprt &dest)
       replace_new_object(object, *it);
 }
 
-goto_convertt::needs_destructiont goto_convertt::remove_cpp_new(
-  side_effect_exprt &expr,
-  goto_programt &dest,
-  bool result_is_used)
+goto_convertt::clean_expr_resultt
+goto_convertt::remove_cpp_new(side_effect_exprt &expr, bool result_is_used)
 {
   const symbolt &new_symbol = get_fresh_aux_symbol(
     expr.type(),
@@ -436,29 +436,29 @@ goto_convertt::needs_destructiont goto_convertt::remove_cpp_new(
     ID_cpp,
     symbol_table);
 
+  clean_expr_resultt side_effects;
+
   PRECONDITION(expr.type().id() != ID_code);
-  dest.add(
+  side_effects.side_effects.add(
     goto_programt::make_decl(new_symbol.symbol_expr(), new_symbol.location));
 
   const code_assignt call(new_symbol.symbol_expr(), expr);
 
-  convert(call, dest, ID_cpp);
+  convert(call, side_effects.side_effects, ID_cpp);
 
   if(result_is_used)
   {
     static_cast<exprt &>(expr) = new_symbol.symbol_expr();
-    return needs_destructiont{to_symbol_expr(expr).get_identifier()};
+    side_effects.add_temporary(to_symbol_expr(expr).get_identifier());
   }
   else
-  {
     expr.make_nil();
-    return {};
-  }
+
+  return side_effects;
 }
 
-void goto_convertt::remove_cpp_delete(
-  side_effect_exprt &expr,
-  goto_programt &dest)
+goto_convertt::clean_expr_resultt
+goto_convertt::remove_cpp_delete(side_effect_exprt &expr)
 {
   DATA_INVARIANT(expr.operands().size() == 1, "cpp_delete expects one operand");
 
@@ -467,17 +467,21 @@ void goto_convertt::remove_cpp_delete(
   tmp.copy_to_operands(to_unary_expr(expr).op());
   tmp.set(ID_destructor, expr.find(ID_destructor));
 
-  convert_cpp_delete(tmp, dest);
+  clean_expr_resultt side_effects;
+  convert_cpp_delete(tmp, side_effects.side_effects);
 
   expr.make_nil();
+
+  return side_effects;
 }
 
-goto_convertt::needs_destructiont goto_convertt::remove_malloc(
+goto_convertt::clean_expr_resultt goto_convertt::remove_malloc(
   side_effect_exprt &expr,
-  goto_programt &dest,
   const irep_idt &mode,
   bool result_is_used)
 {
+  clean_expr_resultt side_effects;
+
   if(result_is_used)
   {
     const symbolt &new_symbol = get_fresh_aux_symbol(
@@ -490,44 +494,47 @@ goto_convertt::needs_destructiont goto_convertt::remove_malloc(
 
     code_frontend_declt decl(new_symbol.symbol_expr());
     decl.add_source_location() = new_symbol.location;
-    convert_frontend_decl(decl, dest, mode);
+    convert_frontend_decl(decl, side_effects.side_effects, mode);
 
     code_assignt call(new_symbol.symbol_expr(), expr);
     call.add_source_location() = expr.source_location();
 
     static_cast<exprt &>(expr) = new_symbol.symbol_expr();
 
-    convert(call, dest, mode);
+    convert(call, side_effects.side_effects, mode);
 
-    return needs_destructiont{to_symbol_expr(expr).get_identifier()};
+    side_effects.add_temporary(to_symbol_expr(expr).get_identifier());
   }
   else
-  {
-    convert(code_expressiont(std::move(expr)), dest, mode);
+    convert(code_expressiont(std::move(expr)), side_effects.side_effects, mode);
 
-    return {};
-  }
+  return side_effects;
 }
 
-goto_convertt::needs_destructiont goto_convertt::remove_temporary_object(
-  side_effect_exprt &expr,
-  goto_programt &dest)
+goto_convertt::clean_expr_resultt
+goto_convertt::remove_temporary_object(side_effect_exprt &expr)
 {
+  clean_expr_resultt side_effects;
+
   const irep_idt &mode = expr.get(ID_mode);
   INVARIANT_WITH_DIAGNOSTICS(
     expr.operands().size() <= 1,
     "temporary_object takes zero or one operands",
     expr.find_source_location());
 
-  symbolt &new_symbol =
-    new_tmp_symbol(expr.type(), "obj", dest, expr.find_source_location(), mode);
+  symbolt &new_symbol = new_tmp_symbol(
+    expr.type(),
+    "obj",
+    side_effects.side_effects,
+    expr.find_source_location(),
+    mode);
 
   if(expr.operands().size() == 1)
   {
     const code_assignt assignment(
       new_symbol.symbol_expr(), to_unary_expr(expr).op());
 
-    convert(assignment, dest, mode);
+    convert(assignment, side_effects.side_effects, mode);
   }
 
   if(expr.find(ID_initializer).is_not_nil())
@@ -539,20 +546,23 @@ goto_convertt::needs_destructiont goto_convertt::remove_temporary_object(
     exprt initializer = static_cast<const exprt &>(expr.find(ID_initializer));
     replace_new_object(new_symbol.symbol_expr(), initializer);
 
-    convert(to_code(initializer), dest, mode);
+    convert(to_code(initializer), side_effects.side_effects, mode);
   }
 
   static_cast<exprt &>(expr) = new_symbol.symbol_expr();
 
-  return needs_destructiont{to_symbol_expr(expr).get_identifier()};
+  side_effects.add_temporary(to_symbol_expr(expr).get_identifier());
+
+  return side_effects;
 }
 
-goto_convertt::needs_destructiont goto_convertt::remove_statement_expression(
+goto_convertt::clean_expr_resultt goto_convertt::remove_statement_expression(
   side_effect_exprt &expr,
-  goto_programt &dest,
   const irep_idt &mode,
   bool result_is_used)
 {
+  clean_expr_resultt side_effects;
+
   // This is a gcc extension of the form ({ ....; expr; })
   // The value is that of the final expression.
   // The expression is copied into a temporary before the
@@ -562,9 +572,9 @@ goto_convertt::needs_destructiont goto_convertt::remove_statement_expression(
 
   if(!result_is_used)
   {
-    convert(code, dest, mode);
+    convert(code, side_effects.side_effects, mode);
     expr.make_nil();
-    return {};
+    return side_effects;
   }
 
   INVARIANT_WITH_DIAGNOSTICS(
@@ -583,7 +593,11 @@ goto_convertt::needs_destructiont goto_convertt::remove_statement_expression(
   source_locationt source_location = last.find_source_location();
 
   symbolt &new_symbol = new_tmp_symbol(
-    expr.type(), "statement_expression", dest, source_location, mode);
+    expr.type(),
+    "statement_expression",
+    side_effects.side_effects,
+    source_location,
+    mode);
 
   symbol_exprt tmp_symbol_expr(new_symbol.name, new_symbol.type);
   tmp_symbol_expr.add_source_location() = source_location;
@@ -607,20 +621,17 @@ goto_convertt::needs_destructiont goto_convertt::remove_statement_expression(
     UNREACHABLE;
   }
 
-  {
-    goto_programt tmp;
-    convert(code, tmp, mode);
-    dest.destructive_append(tmp);
-  }
+  convert(code, side_effects.side_effects, mode);
 
   static_cast<exprt &>(expr) = tmp_symbol_expr;
 
-  return needs_destructiont{to_symbol_expr(expr).get_identifier()};
+  side_effects.add_temporary(to_symbol_expr(expr).get_identifier());
+
+  return side_effects;
 }
 
-goto_convertt::needs_destructiont goto_convertt::remove_overflow(
+goto_convertt::clean_expr_resultt goto_convertt::remove_overflow(
   side_effect_expr_overflowt &expr,
-  goto_programt &dest,
   bool result_is_used,
   const irep_idt &mode)
 {
@@ -629,14 +640,14 @@ goto_convertt::needs_destructiont goto_convertt::remove_overflow(
   const exprt &rhs = expr.rhs();
   const exprt &result = expr.result();
 
-  needs_destructiont new_vars;
+  clean_expr_resultt side_effects;
 
   if(result.type().id() != ID_pointer)
   {
     // result of the arithmetic operation is _not_ used, just evaluate side
     // effects
     exprt tmp = result;
-    new_vars.add(clean_expr(tmp, dest, mode, false));
+    side_effects.add(clean_expr(tmp, mode, false));
 
     // the is-there-an-overflow result may be used
     if(result_is_used)
@@ -667,8 +678,11 @@ goto_convertt::needs_destructiont goto_convertt::remove_overflow(
 
     if(result_is_used)
     {
-      new_vars.minimal_scope.push_front(
-        make_temp_symbol(overflow_with_result, "overflow_result", dest, mode));
+      side_effects.add_temporary(make_temp_symbol(
+        overflow_with_result,
+        "overflow_result",
+        side_effects.side_effects,
+        mode));
     }
 
     const struct_typet::componentst &result_comps =
@@ -679,7 +693,7 @@ goto_convertt::needs_destructiont goto_convertt::remove_overflow(
       typecast_exprt::conditional_cast(
         member_exprt{overflow_with_result, result_comps[0]}, arith_type),
       expr.source_location()};
-    convert_assign(result_assignment, dest, mode);
+    convert_assign(result_assignment, side_effects.side_effects, mode);
 
     if(result_is_used)
     {
@@ -692,12 +706,11 @@ goto_convertt::needs_destructiont goto_convertt::remove_overflow(
       expr.make_nil();
   }
 
-  return new_vars;
+  return side_effects;
 }
 
-goto_convertt::needs_destructiont goto_convertt::remove_side_effect(
+goto_convertt::clean_expr_resultt goto_convertt::remove_side_effect(
   side_effect_exprt &expr,
-  goto_programt &dest,
   const irep_idt &mode,
   bool result_is_used,
   bool address_taken)
@@ -707,7 +720,7 @@ goto_convertt::needs_destructiont goto_convertt::remove_side_effect(
   if(statement == ID_function_call)
   {
     return remove_function_call(
-      to_side_effect_expr_function_call(expr), dest, mode, result_is_used);
+      to_side_effect_expr_function_call(expr), mode, result_is_used);
   }
   else if(
     statement == ID_assign || statement == ID_assign_plus ||
@@ -717,36 +730,35 @@ goto_convertt::needs_destructiont goto_convertt::remove_side_effect(
     statement == ID_assign_lshr || statement == ID_assign_ashr ||
     statement == ID_assign_shl || statement == ID_assign_mod)
   {
-    return remove_assignment(expr, dest, result_is_used, address_taken, mode);
+    return remove_assignment(expr, result_is_used, address_taken, mode);
   }
   else if(statement == ID_postincrement || statement == ID_postdecrement)
   {
-    return remove_post(expr, dest, mode, result_is_used);
+    return remove_post(expr, mode, result_is_used);
   }
   else if(statement == ID_preincrement || statement == ID_predecrement)
   {
-    return remove_pre(expr, dest, result_is_used, address_taken, mode);
+    return remove_pre(expr, result_is_used, address_taken, mode);
   }
   else if(statement == ID_cpp_new || statement == ID_cpp_new_array)
   {
-    return remove_cpp_new(expr, dest, result_is_used);
+    return remove_cpp_new(expr, result_is_used);
   }
   else if(statement == ID_cpp_delete || statement == ID_cpp_delete_array)
   {
-    remove_cpp_delete(expr, dest);
-    return {};
+    return remove_cpp_delete(expr);
   }
   else if(statement == ID_allocate)
   {
-    return remove_malloc(expr, dest, mode, result_is_used);
+    return remove_malloc(expr, mode, result_is_used);
   }
   else if(statement == ID_temporary_object)
   {
-    return remove_temporary_object(expr, dest);
+    return remove_temporary_object(expr);
   }
   else if(statement == ID_statement_expression)
   {
-    return remove_statement_expression(expr, dest, mode, result_is_used);
+    return remove_statement_expression(expr, mode, result_is_used);
   }
   else if(statement == ID_nondet)
   {
@@ -760,23 +772,25 @@ goto_convertt::needs_destructiont goto_convertt::remove_side_effect(
   }
   else if(statement == ID_throw)
   {
+    clean_expr_resultt side_effects;
+
     codet code = code_expressiont(side_effect_expr_throwt(
       expr.find(ID_exception_list), expr.type(), expr.source_location()));
     code.op0().operands().swap(expr.operands());
     code.add_source_location() = expr.source_location();
-    dest.add(goto_programt::instructiont(
+    side_effects.side_effects.add(goto_programt::instructiont(
       std::move(code), expr.source_location(), THROW, nil_exprt(), {}));
 
     // the result can't be used, these are void
     expr.make_nil();
-    return {};
+    return side_effects;
   }
   else if(
     statement == ID_overflow_plus || statement == ID_overflow_minus ||
     statement == ID_overflow_mult)
   {
     return remove_overflow(
-      to_side_effect_expr_overflow(expr), dest, result_is_used, mode);
+      to_side_effect_expr_overflow(expr), result_is_used, mode);
   }
   else
   {
diff --git a/src/goto-instrument/contracts/utils.h b/src/goto-instrument/contracts/utils.h
index b25f43467d8..b6e859c1fdc 100644
--- a/src/goto-instrument/contracts/utils.h
+++ b/src/goto-instrument/contracts/utils.h
@@ -46,7 +46,9 @@ class cleanert : public goto_convertt
   [[nodiscard]] std::list<irep_idt>
   clean(exprt &guard, goto_programt &dest, const irep_idt &mode)
   {
-    return goto_convertt::clean_expr(guard, dest, mode, true).minimal_scope;
+    auto clean_result = goto_convertt::clean_expr(guard, mode, true);
+    dest.destructive_append(clean_result.side_effects);
+    return clean_result.temporaries;
   }
 
   void do_havoc_slice(