diff --git a/src/goto-instrument/model_argc_argv.cpp b/src/goto-instrument/model_argc_argv.cpp
index b47071a2c42..eab95aed6a8 100644
--- a/src/goto-instrument/model_argc_argv.cpp
+++ b/src/goto-instrument/model_argc_argv.cpp
@@ -143,7 +143,8 @@ bool model_argc_argv(
     to_code(value),
     goto_model.symbol_table,
     init_instructions,
-    message_handler);
+    message_handler,
+    main_symbol.mode);
 
   Forall_goto_program_instructions(it, init_instructions)
   {
diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp
index 13685785d71..de4f0001113 100644
--- a/src/goto-programs/builtin_functions.cpp
+++ b/src/goto-programs/builtin_functions.cpp
@@ -438,7 +438,7 @@ void goto_convertt::do_cpp_new(
       count.make_typecast(object_size.type());
 
     // might have side-effect
-    clean_expr(count, dest);
+    clean_expr(count, dest, ID_cpp);
   }
 
   exprt tmp_symbol_expr;
@@ -473,7 +473,7 @@ void goto_convertt::do_cpp_new(
     new_call.lhs()=tmp_symbol_expr;
     new_call.add_source_location()=rhs.source_location();
 
-    convert(new_call, dest);
+    convert(new_call, dest, ID_cpp);
   }
   else if(rhs.operands().size()==1)
   {
@@ -509,7 +509,7 @@ void goto_convertt::do_cpp_new(
       if(new_call.arguments()[i].type()!=code_type.parameters()[i].type())
         new_call.arguments()[i].make_typecast(code_type.parameters()[i].type());
 
-    convert(new_call, dest);
+    convert(new_call, dest, ID_cpp);
   }
   else
   {
@@ -551,7 +551,7 @@ void goto_convertt::cpp_new_initializer(
       const dereference_exprt deref_lhs(lhs, rhs.type().subtype());
 
       replace_new_object(deref_lhs, initializer);
-      convert(to_code(initializer), dest);
+      convert(to_code(initializer), dest, ID_cpp);
     }
     else
       UNREACHABLE;
diff --git a/src/goto-programs/convert_nondet.cpp b/src/goto-programs/convert_nondet.cpp
index 30fdca79ddf..79620c97a5f 100644
--- a/src/goto-programs/convert_nondet.cpp
+++ b/src/goto-programs/convert_nondet.cpp
@@ -35,7 +35,8 @@ static goto_programt::targett insert_nondet_init_code(
   const goto_programt::targett &target,
   symbol_table_baset &symbol_table,
   message_handlert &message_handler,
-  const object_factory_parameterst &object_factory_parameters)
+  const object_factory_parameterst &object_factory_parameters,
+  const irep_idt &mode)
 {
   // Return if the instruction isn't an assignment
   const auto next_instr=std::next(target);
@@ -96,7 +97,8 @@ static goto_programt::targett insert_nondet_init_code(
 
   // Convert this code into goto instructions
   goto_programt new_instructions;
-  goto_convert(init_code, symbol_table, new_instructions, message_handler);
+  goto_convert(
+    init_code, symbol_table, new_instructions, message_handler, mode);
 
   // Insert the new instructions into the instruction list
   goto_program.destructive_insert(next_instr, new_instructions);
@@ -116,25 +118,28 @@ void convert_nondet(
   goto_programt &goto_program,
   symbol_table_baset &symbol_table,
   message_handlert &message_handler,
-  const object_factory_parameterst &object_factory_parameters)
+  const object_factory_parameterst &object_factory_parameters,
+  const irep_idt &mode)
 {
   for(auto instruction_iterator=goto_program.instructions.begin(),
         end=goto_program.instructions.end();
       instruction_iterator!=end;)
   {
-    instruction_iterator=insert_nondet_init_code(
+    instruction_iterator = insert_nondet_init_code(
       goto_program,
       instruction_iterator,
       symbol_table,
       message_handler,
-      object_factory_parameters);
+      object_factory_parameters,
+      mode);
   }
 }
 
 void convert_nondet(
   goto_model_functiont &function,
   message_handlert &message_handler,
-  const object_factory_parameterst &object_factory_parameters)
+  const object_factory_parameterst &object_factory_parameters,
+  const irep_idt &mode)
 {
   object_factory_parameterst parameters = object_factory_parameters;
   parameters.function_id = function.get_function_id();
@@ -142,7 +147,8 @@ void convert_nondet(
     function.get_goto_function().body,
     function.get_symbol_table(),
     message_handler,
-    parameters);
+    parameters,
+    mode);
 
   function.compute_location_numbers();
 }
@@ -167,7 +173,8 @@ void convert_nondet(
         f_it.second.body,
         symbol_table,
         message_handler,
-        object_factory_parameters);
+        object_factory_parameters,
+        symbol.mode);
     }
   }
 
diff --git a/src/goto-programs/convert_nondet.h b/src/goto-programs/convert_nondet.h
index 51355d8d904..7bd3c2ce3ce 100644
--- a/src/goto-programs/convert_nondet.h
+++ b/src/goto-programs/convert_nondet.h
@@ -13,6 +13,7 @@ Author: Reuben Thomas, reuben.thomas@diffblue.com
 #define CPROVER_GOTO_PROGRAMS_CONVERT_NONDET_H
 
 #include <cstddef> // size_t
+#include <util/irep.h>
 
 class goto_functionst;
 class symbol_table_baset;
@@ -48,6 +49,7 @@ void convert_nondet(
 void convert_nondet(
   goto_model_functiont &function,
   message_handlert &message_handler,
-  const object_factory_parameterst &object_factory_parameters);
+  const object_factory_parameterst &object_factory_parameters,
+  const irep_idt &mode);
 
 #endif
diff --git a/src/goto-programs/goto_clean_expr.cpp b/src/goto-programs/goto_clean_expr.cpp
index 0660f80335f..682e5ff0dbf 100644
--- a/src/goto-programs/goto_clean_expr.cpp
+++ b/src/goto-programs/goto_clean_expr.cpp
@@ -21,18 +21,18 @@ Author: Daniel Kroening, kroening@kroening.com
 
 symbol_exprt goto_convertt::make_compound_literal(
   const exprt &expr,
-  goto_programt &dest)
+  goto_programt &dest,
+  const irep_idt &mode)
 {
   const source_locationt source_location=expr.find_source_location();
 
-  symbolt &new_symbol=
-    get_fresh_aux_symbol(
-      expr.type(),
-      tmp_symbol_prefix,
-      "literal",
-      source_location,
-      irep_idt(),
-      symbol_table);
+  symbolt &new_symbol = get_fresh_aux_symbol(
+    expr.type(),
+    tmp_symbol_prefix,
+    "literal",
+    source_location,
+    mode,
+    symbol_table);
   new_symbol.is_static_lifetime=source_location.get_function().empty();
   new_symbol.value=expr;
 
@@ -48,7 +48,7 @@ symbol_exprt goto_convertt::make_compound_literal(
 
   code_assignt code_assign(result, expr);
   code_assign.add_source_location()=source_location;
-  convert(code_assign, dest);
+  convert(code_assign, dest, mode);
 
   // now create a 'dead' instruction
   if(!new_symbol.is_static_lifetime)
@@ -163,6 +163,7 @@ void goto_convertt::rewrite_boolean(exprt &expr)
 void goto_convertt::clean_expr(
   exprt &expr,
   goto_programt &dest,
+  const irep_idt &mode,
   bool result_is_used)
 {
   // this cleans:
@@ -182,13 +183,13 @@ void goto_convertt::clean_expr(
     rewrite_boolean(expr);
 
     // recursive call
-    clean_expr(expr, dest, result_is_used);
+    clean_expr(expr, dest, mode, result_is_used);
     return;
   }
   else if(expr.id()==ID_if)
   {
     // first clean condition
-    clean_expr(to_if_expr(expr).cond(), dest, true);
+    clean_expr(to_if_expr(expr).cond(), dest, mode, true);
 
     // possibly done now
     if(!needs_cleaning(to_if_expr(expr).true_case()) &&
@@ -230,27 +231,27 @@ void goto_convertt::clean_expr(
     #endif
 
     goto_programt tmp_true;
-    clean_expr(if_expr.true_case(), tmp_true, result_is_used);
+    clean_expr(if_expr.true_case(), tmp_true, mode, result_is_used);
 
     goto_programt tmp_false;
-    clean_expr(if_expr.false_case(), tmp_false, result_is_used);
+    clean_expr(if_expr.false_case(), tmp_false, mode, result_is_used);
 
     if(result_is_used)
     {
-      symbolt &new_symbol = new_tmp_symbol(
-        expr.type(), "if_expr", dest, source_location, expr.get(ID_mode));
+      symbolt &new_symbol =
+        new_tmp_symbol(expr.type(), "if_expr", dest, 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);
+      convert(assignment_true, tmp_true, 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);
+      convert(assignment_false, tmp_false, mode);
 
       // overwrites expr
       expr=new_symbol.symbol_expr();
@@ -264,7 +265,7 @@ void 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);
+        convert(code_expression, tmp_true, mode);
       }
 
       if(if_expr.false_case().is_not_nil())
@@ -273,7 +274,7 @@ void 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);
+        convert(code_expression, tmp_false, mode);
       }
 
       expr=nil_exprt();
@@ -281,8 +282,7 @@ void goto_convertt::clean_expr(
 
     // generate guard for argument side-effects
     generate_ifthenelse(
-      if_expr.cond(), tmp_true, tmp_false,
-      source_location, dest);
+      if_expr.cond(), tmp_true, tmp_false, source_location, dest, mode);
 
     return;
   }
@@ -300,15 +300,15 @@ void goto_convertt::clean_expr(
         if(last)
         {
           result.swap(*it);
-          clean_expr(result, dest, true);
+          clean_expr(result, dest, mode, true);
         }
         else
         {
-          clean_expr(*it, dest, false);
+          clean_expr(*it, dest, mode, false);
 
           // remember these for later checks
           if(it->is_not_nil())
-            convert(code_expressiont(*it), dest);
+            convert(code_expressiont(*it), dest, mode);
         }
       }
 
@@ -318,11 +318,11 @@ void goto_convertt::clean_expr(
     {
       Forall_operands(it, expr)
       {
-        clean_expr(*it, dest, false);
+        clean_expr(*it, dest, mode, false);
 
         // remember as expression statement for later checks
         if(it->is_not_nil())
-          convert(code_expressiont(*it), dest);
+          convert(code_expressiont(*it), dest, mode);
       }
 
       expr=nil_exprt();
@@ -340,7 +340,7 @@ void goto_convertt::clean_expr(
     }
 
     // preserve 'result_is_used'
-    clean_expr(expr.op0(), dest, result_is_used);
+    clean_expr(expr.op0(), dest, mode, result_is_used);
 
     if(expr.op0().is_nil())
       expr.make_nil();
@@ -355,7 +355,7 @@ void goto_convertt::clean_expr(
     if(statement==ID_gcc_conditional_expression)
     {
       // need to do separately
-      remove_gcc_conditional_expression(expr, dest);
+      remove_gcc_conditional_expression(expr, dest, mode);
       return;
     }
     else if(statement==ID_statement_expression)
@@ -363,7 +363,7 @@ void goto_convertt::clean_expr(
       // need to do separately to prevent that
       // the operands of expr get 'cleaned'
       remove_statement_expression(
-        to_side_effect_expr(expr), dest, result_is_used);
+        to_side_effect_expr(expr), dest, mode, result_is_used);
       return;
     }
     else if(statement==ID_assign)
@@ -374,7 +374,7 @@ void goto_convertt::clean_expr(
       if(expr.op1().id()==ID_side_effect &&
          to_side_effect_expr(expr.op1()).get_statement()==ID_function_call)
       {
-        clean_expr(expr.op0(), dest);
+        clean_expr(expr.op0(), dest, mode);
         exprt lhs=expr.op0();
 
         // turn into code
@@ -382,7 +382,7 @@ void goto_convertt::clean_expr(
         assignment.lhs()=lhs;
         assignment.rhs()=expr.op1();
         assignment.add_source_location()=expr.source_location();
-        convert_assign(assignment, dest);
+        convert_assign(assignment, dest, mode);
 
         if(result_is_used)
           expr.swap(lhs);
@@ -409,7 +409,7 @@ void goto_convertt::clean_expr(
     assert(expr.operands().size()==2);
     // check if there are side-effects
     goto_programt tmp;
-    clean_expr(expr.op1(), tmp, true);
+    clean_expr(expr.op1(), tmp, mode, true);
     if(tmp.instructions.empty())
     {
       error().source_location=expr.find_source_location();
@@ -422,18 +422,18 @@ void goto_convertt::clean_expr(
   else if(expr.id()==ID_address_of)
   {
     assert(expr.operands().size()==1);
-    clean_expr_address_of(expr.op0(), dest);
+    clean_expr_address_of(expr.op0(), dest, mode);
     return;
   }
 
   // TODO: evaluation order
 
   Forall_operands(it, expr)
-    clean_expr(*it, dest);
+    clean_expr(*it, dest, mode);
 
   if(expr.id()==ID_side_effect)
   {
-    remove_side_effect(to_side_effect_expr(expr), dest, result_is_used);
+    remove_side_effect(to_side_effect_expr(expr), dest, mode, result_is_used);
   }
   else if(expr.id()==ID_compound_literal)
   {
@@ -445,7 +445,8 @@ void goto_convertt::clean_expr(
 
 void goto_convertt::clean_expr_address_of(
   exprt &expr,
-  goto_programt &dest)
+  goto_programt &dest,
+  const irep_idt &mode)
 {
   // The address of object constructors can be taken,
   // which is re-written into the address of a variable.
@@ -453,8 +454,8 @@ void goto_convertt::clean_expr_address_of(
   if(expr.id()==ID_compound_literal)
   {
     assert(expr.operands().size()==1);
-    clean_expr(expr.op0(), dest);
-    expr=make_compound_literal(expr.op0(), dest);
+    clean_expr(expr.op0(), dest, mode);
+    expr = make_compound_literal(expr.op0(), dest, mode);
   }
   else if(expr.id()==ID_string_constant)
   {
@@ -464,13 +465,13 @@ void goto_convertt::clean_expr_address_of(
   else if(expr.id()==ID_index)
   {
     assert(expr.operands().size()==2);
-    clean_expr_address_of(expr.op0(), dest);
-    clean_expr(expr.op1(), dest);
+    clean_expr_address_of(expr.op0(), dest, mode);
+    clean_expr(expr.op1(), dest, mode);
   }
   else if(expr.id()==ID_dereference)
   {
     assert(expr.operands().size()==1);
-    clean_expr(expr.op0(), dest);
+    clean_expr(expr.op0(), dest, mode);
   }
   else if(expr.id()==ID_comma)
   {
@@ -488,27 +489,28 @@ void goto_convertt::clean_expr_address_of(
         result.swap(*it);
       else
       {
-        clean_expr(*it, dest, false);
+        clean_expr(*it, dest, mode, false);
 
         // get any side-effects
         if(it->is_not_nil())
-          convert(code_expressiont(*it), dest);
+          convert(code_expressiont(*it), dest, mode);
       }
     }
 
     expr.swap(result);
 
     // do again
-    clean_expr_address_of(expr, dest);
+    clean_expr_address_of(expr, dest, mode);
   }
   else
     Forall_operands(it, expr)
-      clean_expr_address_of(*it, dest);
+      clean_expr_address_of(*it, dest, mode);
 }
 
 void goto_convertt::remove_gcc_conditional_expression(
   exprt &expr,
-  goto_programt &dest)
+  goto_programt &dest,
+  const irep_idt &mode)
 {
   if(expr.operands().size()!=2)
   {
@@ -518,7 +520,7 @@ void goto_convertt::remove_gcc_conditional_expression(
   }
 
   // first remove side-effects from condition
-  clean_expr(expr.op0(), dest);
+  clean_expr(expr.op0(), dest, mode);
 
   // now we can copy op0 safely
   if_exprt if_expr;
@@ -535,5 +537,5 @@ void goto_convertt::remove_gcc_conditional_expression(
   expr.swap(if_expr);
 
   // there might still be junk in expr.op2()
-  clean_expr(expr, dest);
+  clean_expr(expr, dest, mode);
 }
diff --git a/src/goto-programs/goto_convert.cpp b/src/goto-programs/goto_convert.cpp
index c662c5a4c2f..236dd782db6 100644
--- a/src/goto-programs/goto_convert.cpp
+++ b/src/goto-programs/goto_convert.cpp
@@ -103,7 +103,7 @@ Function: goto_convertt::finish_gotos
 
 \*******************************************************************/
 
-void goto_convertt::finish_gotos(goto_programt &dest)
+void goto_convertt::finish_gotos(goto_programt &dest, const irep_idt &mode)
 {
   for(const auto &g_it : targets.gotos)
   {
@@ -199,7 +199,8 @@ void goto_convertt::finish_gotos(goto_programt &dest)
             i.code.add_source_location(),
             unwind_to_size,
             destructor_code,
-            goto_stack);
+            goto_stack,
+            mode);
           dest.destructive_insert(g_it.first, destructor_code);
           // This should leave iterators intact, as long as
           // goto_programt::instructionst is std::list.
@@ -294,21 +295,25 @@ void goto_convertt::finish_guarded_gotos(goto_programt &dest)
   guarded_gotos.clear();
 }
 
-void goto_convertt::goto_convert(const codet &code, goto_programt &dest)
+void goto_convertt::goto_convert(
+  const codet &code,
+  goto_programt &dest,
+  const irep_idt &mode)
 {
-  goto_convert_rec(code, dest);
+  goto_convert_rec(code, dest, mode);
 }
 
 void goto_convertt::goto_convert_rec(
   const codet &code,
-  goto_programt &dest)
+  goto_programt &dest,
+  const irep_idt &mode)
 {
   // Check that guarded_gotos was cleared after any previous use of this
   // converter instance:
   PRECONDITION(guarded_gotos.empty());
-  convert(code, dest);
+  convert(code, dest, mode);
 
-  finish_gotos(dest);
+  finish_gotos(dest, mode);
   finish_computed_gotos(dest);
   finish_guarded_gotos(dest);
   finish_catch_push_targets(dest);
@@ -326,7 +331,8 @@ void goto_convertt::copy(
 
 void goto_convertt::convert_label(
   const code_labelt &code,
-  goto_programt &dest)
+  goto_programt &dest,
+  const irep_idt &mode)
 {
   if(code.operands().size()!=1)
   {
@@ -355,11 +361,11 @@ void goto_convertt::convert_label(
     code_blockt thread_body;
     thread_body.add(to_code(code.op0()));
     thread_body.add_source_location()=code.source_location();
-    generate_thread_block(thread_body, dest);
+    generate_thread_block(thread_body, dest, mode);
   }
   else
   {
-    convert(to_code(code.op0()), tmp);
+    convert(to_code(code.op0()), tmp, mode);
 
     goto_programt::targett target=tmp.instructions.begin();
     dest.destructive_append(tmp);
@@ -378,10 +384,11 @@ void goto_convertt::convert_gcc_local_label(
 
 void goto_convertt::convert_switch_case(
   const code_switch_caset &code,
-  goto_programt &dest)
+  goto_programt &dest,
+  const irep_idt &mode)
 {
   goto_programt tmp;
-  convert(code.code(), tmp);
+  convert(code.code(), tmp, mode);
 
   goto_programt::targett target=tmp.instructions.begin();
   dest.destructive_append(tmp);
@@ -409,7 +416,8 @@ void goto_convertt::convert_switch_case(
 
 void goto_convertt::convert_gcc_switch_case_range(
   const codet &code,
-  goto_programt &dest)
+  goto_programt &dest,
+  const irep_idt &mode)
 {
   if(code.operands().size()!=3)
   {
@@ -420,7 +428,7 @@ void goto_convertt::convert_gcc_switch_case_range(
   }
 
   goto_programt tmp;
-  convert(to_code(code.op2()), tmp);
+  convert(to_code(code.op2()), tmp, mode);
 
   // goto_programt::targett target=tmp.instructions.begin();
   dest.destructive_append(tmp);
@@ -443,50 +451,51 @@ void goto_convertt::convert_gcc_switch_case_range(
 /// converts 'code' and appends the result to 'dest'
 void goto_convertt::convert(
   const codet &code,
-  goto_programt &dest)
+  goto_programt &dest,
+  const irep_idt &mode)
 {
   const irep_idt &statement=code.get_statement();
 
   if(statement==ID_block)
-    convert_block(to_code_block(code), dest);
+    convert_block(to_code_block(code), dest, mode);
   else if(statement==ID_decl)
-    convert_decl(to_code_decl(code), dest);
+    convert_decl(to_code_decl(code), dest, mode);
   else if(statement==ID_decl_type)
     convert_decl_type(code, dest);
   else if(statement==ID_expression)
-    convert_expression(to_code_expression(code), dest);
+    convert_expression(to_code_expression(code), dest, mode);
   else if(statement==ID_assign)
-    convert_assign(to_code_assign(code), dest);
+    convert_assign(to_code_assign(code), dest, mode);
   else if(statement==ID_init)
-    convert_init(code, dest);
+    convert_init(code, dest, mode);
   else if(statement==ID_assert)
-    convert_assert(to_code_assert(code), dest);
+    convert_assert(to_code_assert(code), dest, mode);
   else if(statement==ID_assume)
-    convert_assume(to_code_assume(code), dest);
+    convert_assume(to_code_assume(code), dest, mode);
   else if(statement==ID_function_call)
-    convert_function_call(to_code_function_call(code), dest);
+    convert_function_call(to_code_function_call(code), dest, mode);
   else if(statement==ID_label)
-    convert_label(to_code_label(code), dest);
+    convert_label(to_code_label(code), dest, mode);
   else if(statement==ID_gcc_local_label)
     convert_gcc_local_label(code, dest);
   else if(statement==ID_switch_case)
-    convert_switch_case(to_code_switch_case(code), dest);
+    convert_switch_case(to_code_switch_case(code), dest, mode);
   else if(statement==ID_gcc_switch_case_range)
-    convert_gcc_switch_case_range(code, dest);
+    convert_gcc_switch_case_range(code, dest, mode);
   else if(statement==ID_for)
-    convert_for(to_code_for(code), dest);
+    convert_for(to_code_for(code), dest, mode);
   else if(statement==ID_while)
-    convert_while(to_code_while(code), dest);
+    convert_while(to_code_while(code), dest, mode);
   else if(statement==ID_dowhile)
-    convert_dowhile(code, dest);
+    convert_dowhile(code, dest, mode);
   else if(statement==ID_switch)
-    convert_switch(to_code_switch(code), dest);
+    convert_switch(to_code_switch(code), dest, mode);
   else if(statement==ID_break)
-    convert_break(to_code_break(code), dest);
+    convert_break(to_code_break(code), dest, mode);
   else if(statement==ID_return)
-    convert_return(to_code_return(code), dest);
+    convert_return(to_code_return(code), dest, mode);
   else if(statement==ID_continue)
-    convert_continue(to_code_continue(code), dest);
+    convert_continue(to_code_continue(code), dest, mode);
   else if(statement==ID_goto)
     convert_goto(code, dest);
   else if(statement==ID_gcc_computed_goto)
@@ -496,7 +505,7 @@ void goto_convertt::convert(
   else if(statement=="non-deterministic-goto")
     convert_non_deterministic_goto(code, dest);
   else if(statement==ID_ifthenelse)
-    convert_ifthenelse(to_code_ifthenelse(code), dest);
+    convert_ifthenelse(to_code_ifthenelse(code), dest, mode);
   else if(statement==ID_specc_notify)
     convert_specc_notify(code, dest);
   else if(statement==ID_specc_wait)
@@ -515,19 +524,19 @@ void goto_convertt::convert(
           statement=="cpp_delete[]")
     convert_cpp_delete(code, dest);
   else if(statement==ID_msc_try_except)
-    convert_msc_try_except(code, dest);
+    convert_msc_try_except(code, dest, mode);
   else if(statement==ID_msc_try_finally)
-    convert_msc_try_finally(code, dest);
+    convert_msc_try_finally(code, dest, mode);
   else if(statement==ID_msc_leave)
-    convert_msc_leave(code, dest);
+    convert_msc_leave(code, dest, mode);
   else if(statement==ID_try_catch) // C++ try/catch
-    convert_try_catch(code, dest);
+    convert_try_catch(code, dest, mode);
   else if(statement==ID_CPROVER_try_catch) // CPROVER-homemade
-    convert_CPROVER_try_catch(code, dest);
+    convert_CPROVER_try_catch(code, dest, mode);
   else if(statement==ID_CPROVER_throw) // CPROVER-homemade
-    convert_CPROVER_throw(code, dest);
+    convert_CPROVER_throw(code, dest, mode);
   else if(statement==ID_CPROVER_try_finally)
-    convert_CPROVER_try_finally(code, dest);
+    convert_CPROVER_try_finally(code, dest, mode);
   else if(statement==ID_asm)
     convert_asm(to_code_asm(code), dest);
   else if(statement==ID_static_assert)
@@ -556,7 +565,7 @@ void goto_convertt::convert(
   else if(statement==ID_decl_block)
   {
     forall_operands(it, code)
-      convert(to_code(*it), dest);
+      convert(to_code(*it), dest, mode);
   }
   else if(statement==ID_push_catch ||
           statement==ID_pop_catch ||
@@ -576,7 +585,8 @@ void goto_convertt::convert(
 
 void goto_convertt::convert_block(
   const code_blockt &code,
-  goto_programt &dest)
+  goto_programt &dest,
+  const irep_idt &mode)
 {
   const source_locationt &end_location=code.end_location();
 
@@ -587,7 +597,7 @@ void goto_convertt::convert_block(
   forall_operands(it, code)
   {
     const codet &b_code=to_code(*it);
-    convert(b_code, dest);
+    convert(b_code, dest, mode);
   }
 
   // see if we need to do any destructors -- may have been processed
@@ -599,7 +609,7 @@ void goto_convertt::convert_block(
     // don't do destructors when we are unreachable
   }
   else
-    unwind_destructor_stack(end_location, old_stack_size, dest);
+    unwind_destructor_stack(end_location, old_stack_size, dest, mode);
 
   // remove those destructors
   targets.destructor_stack.resize(old_stack_size);
@@ -607,7 +617,8 @@ void goto_convertt::convert_block(
 
 void goto_convertt::convert_expression(
   const code_expressiont &code,
-  goto_programt &dest)
+  goto_programt &dest,
+  const irep_idt &mode)
 {
   if(code.operands().size()!=1)
   {
@@ -630,11 +641,11 @@ void goto_convertt::convert_expression(
     tmp_code.then_case().add_source_location()=expr.source_location();
     tmp_code.else_case()=code_expressiont(if_expr.false_case());
     tmp_code.else_case().add_source_location()=expr.source_location();
-    convert_ifthenelse(tmp_code, dest);
+    convert_ifthenelse(tmp_code, dest, mode);
   }
   else
   {
-    clean_expr(expr, dest, false); // result _not_ used
+    clean_expr(expr, dest, mode, false); // result _not_ used
 
     // Any residual expression?
     // We keep it to add checks later.
@@ -650,7 +661,8 @@ void goto_convertt::convert_expression(
 
 void goto_convertt::convert_decl(
   const code_declt &code,
-  goto_programt &dest)
+  goto_programt &dest,
+  const irep_idt &mode)
 {
   const exprt &op0=code.op0();
 
@@ -689,7 +701,7 @@ void goto_convertt::convert_decl(
     code_assignt assign(code.op0(), initializer);
     assign.add_source_location()=tmp.source_location();
 
-    convert_assign(assign, dest);
+    convert_assign(assign, dest, mode);
   }
 
   // now create a 'dead' instruction -- will be added after the
@@ -724,12 +736,13 @@ void goto_convertt::convert_decl_type(
 
 void goto_convertt::convert_assign(
   const code_assignt &code,
-  goto_programt &dest)
+  goto_programt &dest,
+  const irep_idt &mode)
 {
   exprt lhs=code.lhs(),
         rhs=code.rhs();
 
-  clean_expr(lhs, dest);
+  clean_expr(lhs, dest, mode);
 
   if(rhs.id()==ID_side_effect &&
      rhs.get(ID_statement)==ID_function_call)
@@ -742,16 +755,16 @@ void goto_convertt::convert_assign(
     }
 
     Forall_operands(it, rhs)
-      clean_expr(*it, dest);
+      clean_expr(*it, dest, mode);
 
-    do_function_call(lhs, rhs.op0(), rhs.op1().operands(), dest);
+    do_function_call(lhs, rhs.op0(), rhs.op1().operands(), dest, mode);
   }
   else if(rhs.id()==ID_side_effect &&
           (rhs.get(ID_statement)==ID_cpp_new ||
            rhs.get(ID_statement)==ID_cpp_new_array))
   {
     Forall_operands(it, rhs)
-      clean_expr(*it, dest);
+      clean_expr(*it, dest, mode);
 
     // TODO: This should be done in a separate pass
     do_cpp_new(lhs, to_side_effect_expr(rhs), dest);
@@ -764,7 +777,7 @@ void goto_convertt::convert_assign(
      rhs.get(ID_statement) == ID_statement_expression))
   {
     // handle above side effects
-    clean_expr(rhs, dest);
+    clean_expr(rhs, dest, mode);
 
     if(lhs.id() == ID_typecast)
     {
@@ -791,7 +804,7 @@ 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)
-      clean_expr(*it, dest);
+      clean_expr(*it, dest, mode);
 
     code_assignt new_assign(code);
     new_assign.lhs()=lhs;
@@ -802,7 +815,7 @@ void goto_convertt::convert_assign(
   else
   {
     // do everything else
-    clean_expr(rhs, dest);
+    clean_expr(rhs, dest, mode);
 
     if(lhs.id()==ID_typecast)
     {
@@ -827,7 +840,8 @@ void goto_convertt::convert_assign(
 
 void goto_convertt::convert_init(
   const codet &code,
-  goto_programt &dest)
+  goto_programt &dest,
+  const irep_idt &mode)
 {
   if(code.operands().size()!=2)
   {
@@ -840,7 +854,7 @@ void goto_convertt::convert_init(
   codet assignment=code;
   assignment.set_statement(ID_assign);
 
-  convert(to_code_assign(assignment), dest);
+  convert(to_code_assign(assignment), dest, mode);
 }
 
 void goto_convertt::convert_cpp_delete(
@@ -856,7 +870,7 @@ void goto_convertt::convert_cpp_delete(
 
   exprt tmp_op=code.op0();
 
-  clean_expr(tmp_op, dest);
+  clean_expr(tmp_op, dest, ID_cpp);
 
   // we call the destructor, and then free
   const exprt &destructor=
@@ -884,7 +898,7 @@ void goto_convertt::convert_cpp_delete(
 
       codet tmp_code=to_code(destructor);
       replace_new_object(deref_op, tmp_code);
-      convert(tmp_code, dest);
+      convert(tmp_code, dest, ID_cpp);
     }
     else
       UNREACHABLE;
@@ -904,16 +918,17 @@ void goto_convertt::convert_cpp_delete(
   delete_call.lhs().make_nil();
   delete_call.add_source_location()=code.source_location();
 
-  convert(delete_call, dest);
+  convert(delete_call, dest, ID_cpp);
 }
 
 void goto_convertt::convert_assert(
   const code_assertt &code,
-  goto_programt &dest)
+  goto_programt &dest,
+  const irep_idt &mode)
 {
   exprt cond=code.assertion();
 
-  clean_expr(cond, dest);
+  clean_expr(cond, dest, mode);
 
   goto_programt::targett t=dest.add_instruction(ASSERT);
   t->guard.swap(cond);
@@ -933,11 +948,12 @@ void goto_convertt::convert_skip(
 
 void goto_convertt::convert_assume(
   const code_assumet &code,
-  goto_programt &dest)
+  goto_programt &dest,
+  const irep_idt &mode)
 {
   exprt op=code.assumption();
 
-  clean_expr(op, dest);
+  clean_expr(op, dest, mode);
 
   goto_programt::targett t=dest.add_instruction(ASSUME);
   t->guard.swap(op);
@@ -946,7 +962,8 @@ void goto_convertt::convert_assume(
 
 void goto_convertt::convert_loop_invariant(
   const codet &code,
-  goto_programt::targett loop)
+  goto_programt::targett loop,
+  const irep_idt &mode)
 {
   exprt invariant=
     static_cast<const exprt&>(code.find(ID_C_spec_loop_invariant));
@@ -955,7 +972,7 @@ void goto_convertt::convert_loop_invariant(
     return;
 
   goto_programt no_sideeffects;
-  clean_expr(invariant, no_sideeffects);
+  clean_expr(invariant, no_sideeffects, mode);
   if(!no_sideeffects.instructions.empty())
   {
     error().source_location=code.find_source_location();
@@ -969,7 +986,8 @@ void goto_convertt::convert_loop_invariant(
 
 void goto_convertt::convert_for(
   const code_fort &code,
-  goto_programt &dest)
+  goto_programt &dest,
+  const irep_idt &mode)
 {
   // turn for(A; c; B) { P } into
   //  A; while(c) { P; B; }
@@ -984,12 +1002,12 @@ void goto_convertt::convert_for(
 
   // A;
   if(code.init().is_not_nil())
-    convert(to_code(code.init()), dest);
+    convert(to_code(code.init()), dest, mode);
 
   exprt cond=code.cond();
 
   goto_programt sideeffects;
-  clean_expr(cond, sideeffects);
+  clean_expr(cond, sideeffects, mode);
 
   // save break/continue targets
   break_continue_targetst old_targets(targets);
@@ -1018,7 +1036,7 @@ void goto_convertt::convert_for(
   {
     exprt tmp_B=code.iter();
 
-    clean_expr(tmp_B, tmp_x, false);
+    clean_expr(tmp_B, tmp_x, mode, false);
 
     if(tmp_x.instructions.empty())
     {
@@ -1043,7 +1061,7 @@ void goto_convertt::convert_for(
 
   // do the w label
   goto_programt tmp_w;
-  convert(code.body(), tmp_w);
+  convert(code.body(), tmp_w, mode);
 
   // y: goto u;
   goto_programt tmp_y;
@@ -1053,7 +1071,7 @@ void goto_convertt::convert_for(
   y->source_location=code.source_location();
 
   // loop invariant
-  convert_loop_invariant(code, y);
+  convert_loop_invariant(code, y, mode);
 
   dest.destructive_append(sideeffects);
   dest.destructive_append(tmp_v);
@@ -1068,7 +1086,8 @@ void goto_convertt::convert_for(
 
 void goto_convertt::convert_while(
   const code_whilet &code,
-  goto_programt &dest)
+  goto_programt &dest,
+  const irep_idt &mode)
 {
   const exprt &cond=code.cond();
   const source_locationt &source_location=code.source_location();
@@ -1092,7 +1111,7 @@ void goto_convertt::convert_while(
 
   goto_programt tmp_branch;
   generate_conditional_branch(
-    boolean_negate(cond), z, source_location, tmp_branch);
+    boolean_negate(cond), z, source_location, tmp_branch, mode);
 
   // do the v label
   goto_programt::targett v=tmp_branch.instructions.begin();
@@ -1107,7 +1126,7 @@ void goto_convertt::convert_while(
 
   // do the x label
   goto_programt tmp_x;
-  convert(code.body(), tmp_x);
+  convert(code.body(), tmp_x, mode);
 
   // y: if(c) goto v;
   y->make_goto(v);
@@ -1115,7 +1134,7 @@ void goto_convertt::convert_while(
   y->source_location=code.source_location();
 
   // loop invariant
-  convert_loop_invariant(code, y);
+  convert_loop_invariant(code, y, mode);
 
   dest.destructive_append(tmp_branch);
   dest.destructive_append(tmp_x);
@@ -1128,7 +1147,8 @@ void goto_convertt::convert_while(
 
 void goto_convertt::convert_dowhile(
   const codet &code,
-  goto_programt &dest)
+  goto_programt &dest,
+  const irep_idt &mode)
 {
   if(code.operands().size()!=2)
   {
@@ -1143,7 +1163,7 @@ void goto_convertt::convert_dowhile(
   exprt cond=code.op0();
 
   goto_programt sideeffects;
-  clean_expr(cond, sideeffects);
+  clean_expr(cond, sideeffects, mode);
 
   //    do P while(c);
   //--------------------
@@ -1178,7 +1198,7 @@ void goto_convertt::convert_dowhile(
 
   // do the w label
   goto_programt tmp_w;
-  convert(to_code(code.op1()), tmp_w);
+  convert(to_code(code.op1()), tmp_w, mode);
   goto_programt::targett w=tmp_w.instructions.begin();
 
   // y: if(c) goto w;
@@ -1187,7 +1207,7 @@ void goto_convertt::convert_dowhile(
   y->source_location=condition_location;
 
   // loop invariant
-  convert_loop_invariant(code, y);
+  convert_loop_invariant(code, y, mode);
 
   dest.destructive_append(tmp_w);
   dest.destructive_append(sideeffects);
@@ -1227,7 +1247,8 @@ exprt goto_convertt::case_guard(
 
 void goto_convertt::convert_switch(
   const code_switcht &code,
-  goto_programt &dest)
+  goto_programt &dest,
+  const irep_idt &mode)
 {
   // switch(v) {
   //   case x: Px;
@@ -1261,7 +1282,7 @@ void goto_convertt::convert_switch(
   exprt argument=code.value();
 
   goto_programt sideeffects;
-  clean_expr(argument, sideeffects);
+  clean_expr(argument, sideeffects, mode);
 
   // save break/default/cases targets
   break_switch_targetst old_targets(targets);
@@ -1279,7 +1300,7 @@ void goto_convertt::convert_switch(
   targets.cases_map.clear();
 
   goto_programt tmp;
-  convert(code.body(), tmp);
+  convert(code.body(), tmp, mode);
 
   goto_programt tmp_cases;
 
@@ -1332,7 +1353,8 @@ void goto_convertt::convert_switch(
 
 void goto_convertt::convert_break(
   const code_breakt &code,
-  goto_programt &dest)
+  goto_programt &dest,
+  const irep_idt &mode)
 {
   if(!targets.break_set)
   {
@@ -1343,7 +1365,7 @@ void goto_convertt::convert_break(
 
   // need to process destructor stack
   unwind_destructor_stack(
-    code.source_location(), targets.break_stack_size, dest);
+    code.source_location(), targets.break_stack_size, dest, mode);
 
   // add goto
   goto_programt::targett t=dest.add_instruction();
@@ -1353,7 +1375,8 @@ void goto_convertt::convert_break(
 
 void goto_convertt::convert_return(
   const code_returnt &code,
-  goto_programt &dest)
+  goto_programt &dest,
+  const irep_idt &mode)
 {
   if(!targets.return_set)
   {
@@ -1378,7 +1401,7 @@ void goto_convertt::convert_return(
       new_code.return_value().type().id()!=ID_empty;
 
     goto_programt sideeffects;
-    clean_expr(new_code.return_value(), sideeffects, result_is_used);
+    clean_expr(new_code.return_value(), sideeffects, mode, result_is_used);
     dest.destructive_append(sideeffects);
 
     // remove void-typed return value
@@ -1413,7 +1436,7 @@ void goto_convertt::convert_return(
   }
 
   // Need to process _entire_ destructor stack.
-  unwind_destructor_stack(code.source_location(), 0, dest);
+  unwind_destructor_stack(code.source_location(), 0, dest, mode);
 
   // add goto to end-of-function
   goto_programt::targett t=dest.add_instruction();
@@ -1423,7 +1446,8 @@ void goto_convertt::convert_return(
 
 void goto_convertt::convert_continue(
   const code_continuet &code,
-  goto_programt &dest)
+  goto_programt &dest,
+  const irep_idt &mode)
 {
   if(!targets.continue_set)
   {
@@ -1434,7 +1458,7 @@ void goto_convertt::convert_continue(
 
   // need to process destructor stack
   unwind_destructor_stack(
-    code.source_location(), targets.continue_stack_size, dest);
+    code.source_location(), targets.continue_stack_size, dest, mode);
 
   // add goto
   goto_programt::targett t=dest.add_instruction();
@@ -1611,7 +1635,8 @@ void goto_convertt::convert_atomic_end(
 
 void goto_convertt::convert_ifthenelse(
   const code_ifthenelset &code,
-  goto_programt &dest)
+  goto_programt &dest,
+  const irep_idt &mode)
 {
   if(code.operands().size()!=3)
   {
@@ -1642,22 +1667,23 @@ void goto_convertt::convert_ifthenelse(
     new_if1.add_source_location()=source_location;
     new_if1.then_case()=code.then_case();
     new_if0.then_case()=new_if1;
-    return convert_ifthenelse(new_if0, dest);
+    return convert_ifthenelse(new_if0, dest, mode);
   }
 
   // convert 'then'-branch
   goto_programt tmp_then;
-  convert(to_code(code.then_case()), tmp_then);
+  convert(to_code(code.then_case()), tmp_then, mode);
 
   goto_programt tmp_else;
 
   if(has_else)
-    convert(to_code(code.else_case()), tmp_else);
+    convert(to_code(code.else_case()), tmp_else, mode);
 
   exprt tmp_guard=code.cond();
-  clean_expr(tmp_guard, dest);
+  clean_expr(tmp_guard, dest, mode);
 
-  generate_ifthenelse(tmp_guard, tmp_then, tmp_else, source_location, dest);
+  generate_ifthenelse(
+    tmp_guard, tmp_then, tmp_else, source_location, dest, mode);
 }
 
 void goto_convertt::collect_operands(
@@ -1692,7 +1718,8 @@ void goto_convertt::generate_ifthenelse(
   goto_programt &true_case,
   goto_programt &false_case,
   const source_locationt &source_location,
-  goto_programt &dest)
+  goto_programt &dest,
+  const irep_idt &mode)
 {
   if(is_empty(true_case) &&
      is_empty(false_case))
@@ -1781,7 +1808,12 @@ void goto_convertt::generate_ifthenelse(
   // Flip around if no 'true' case code.
   if(is_empty(true_case))
     return generate_ifthenelse(
-      boolean_negate(guard), false_case, true_case, source_location, dest);
+      boolean_negate(guard),
+      false_case,
+      true_case,
+      source_location,
+      dest,
+      mode);
 
   bool has_else=!is_empty(false_case);
 
@@ -1822,7 +1854,7 @@ void goto_convertt::generate_ifthenelse(
   // v: if(!c) goto z/y;
   goto_programt tmp_v;
   generate_conditional_branch(
-    boolean_negate(guard), has_else?y:z, source_location, tmp_v);
+    boolean_negate(guard), has_else ? y : z, source_location, tmp_v, mode);
 
   // w: P;
   goto_programt tmp_w;
@@ -1869,7 +1901,8 @@ void goto_convertt::generate_conditional_branch(
   const exprt &guard,
   goto_programt::targett target_true,
   const source_locationt &source_location,
-  goto_programt &dest)
+  goto_programt &dest,
+  const irep_idt &mode)
 {
   if(has_and_or(guard) && needs_cleaning(guard))
   {
@@ -1884,7 +1917,7 @@ void goto_convertt::generate_conditional_branch(
     target_false->source_location=source_location;
 
     generate_conditional_branch(
-      guard, target_true, target_false, source_location, dest);
+      guard, target_true, target_false, source_location, dest, mode);
 
     dest.destructive_append(tmp);
   }
@@ -1892,7 +1925,7 @@ void goto_convertt::generate_conditional_branch(
   {
     // simple branch
     exprt cond=guard;
-    clean_expr(cond, dest);
+    clean_expr(cond, dest, mode);
 
     goto_programt tmp;
     goto_programt::targett g=tmp.add_instruction();
@@ -1909,14 +1942,15 @@ void goto_convertt::generate_conditional_branch(
   goto_programt::targett target_true,
   goto_programt::targett target_false,
   const source_locationt &source_location,
-  goto_programt &dest)
+  goto_programt &dest,
+  const irep_idt &mode)
 {
   if(guard.id()==ID_not)
   {
     assert(guard.operands().size()==1);
     // simply swap targets
     generate_conditional_branch(
-      guard.op0(), target_false, target_true, source_location, dest);
+      guard.op0(), target_false, target_true, source_location, dest, mode);
     return;
   }
 
@@ -1934,7 +1968,7 @@ void goto_convertt::generate_conditional_branch(
 
     for(const auto &expr : op)
       generate_conditional_branch(
-        boolean_negate(expr), target_false, source_location, dest);
+        boolean_negate(expr), target_false, source_location, dest, mode);
 
     goto_programt::targett t_true=dest.add_instruction();
     t_true->make_goto(target_true);
@@ -1956,7 +1990,8 @@ void goto_convertt::generate_conditional_branch(
     collect_operands(guard, guard.id(), op);
 
     for(const auto &expr : op)
-      generate_conditional_branch(expr, target_true, source_location, dest);
+      generate_conditional_branch(
+        expr, target_true, source_location, dest, mode);
 
     goto_programt::targett t_false=dest.add_instruction();
     t_false->make_goto(target_false);
@@ -1967,7 +2002,7 @@ void goto_convertt::generate_conditional_branch(
   }
 
   exprt cond=guard;
-  clean_expr(cond, dest);
+  clean_expr(cond, dest, mode);
 
   goto_programt::targett t_true=dest.add_instruction();
   t_true->make_goto(target_true);
@@ -2070,6 +2105,7 @@ symbolt &goto_convertt::new_tmp_symbol(
   const source_locationt &source_location,
   const irep_idt &mode)
 {
+  PRECONDITION(!mode.empty());
   symbolt &new_symbol = get_fresh_aux_symbol(
     type,
     tmp_symbol_prefix,
@@ -2081,7 +2117,7 @@ symbolt &goto_convertt::new_tmp_symbol(
   code_declt decl;
   decl.symbol()=new_symbol.symbol_expr();
   decl.add_source_location()=source_location;
-  convert_decl(decl, dest);
+  convert_decl(decl, dest, mode);
 
   return new_symbol;
 }
@@ -2089,19 +2125,20 @@ symbolt &goto_convertt::new_tmp_symbol(
 void goto_convertt::make_temp_symbol(
   exprt &expr,
   const std::string &suffix,
-  goto_programt &dest)
+  goto_programt &dest,
+  const irep_idt &mode)
 {
   const source_locationt source_location=expr.find_source_location();
 
-  symbolt &new_symbol = new_tmp_symbol(
-    expr.type(), suffix, dest, source_location, expr.get(ID_mode));
+  symbolt &new_symbol =
+    new_tmp_symbol(expr.type(), suffix, dest, source_location, mode);
 
   code_assignt assignment;
   assignment.lhs()=new_symbol.symbol_expr();
   assignment.rhs()=expr;
   assignment.add_source_location()=source_location;
 
-  convert(assignment, dest);
+  convert(assignment, dest, mode);
 
   expr=new_symbol.symbol_expr();
 }
@@ -2130,7 +2167,8 @@ void goto_convert(
   const codet &code,
   symbol_table_baset &symbol_table,
   goto_programt &dest,
-  message_handlert &message_handler)
+  message_handlert &message_handler,
+  const irep_idt &mode)
 {
   const std::size_t errors_before=
     message_handler.get_message_count(messaget::M_ERROR);
@@ -2139,7 +2177,7 @@ void goto_convert(
 
   try
   {
-    goto_convert.goto_convert(code, dest);
+    goto_convert.goto_convert(code, dest, mode);
   }
 
   catch(int)
@@ -2175,7 +2213,8 @@ void goto_convert(
 
   const symbolt &symbol=s_it->second;
 
-  ::goto_convert(to_code(symbol.value), symbol_table, dest, message_handler);
+  ::goto_convert(
+    to_code(symbol.value), symbol_table, dest, message_handler, symbol.mode);
 }
 
 /// Generates the necessary goto-instructions to represent a thread-block.
@@ -2193,13 +2232,14 @@ void goto_convert(
 /// \param [out] dest: resulting goto-instructions.
 void goto_convertt::generate_thread_block(
   const code_blockt &thread_body,
-  goto_programt &dest)
+  goto_programt &dest,
+  const irep_idt &mode)
 {
   goto_programt preamble, body, postamble;
 
   goto_programt::targett c=body.add_instruction();
   c->make_skip();
-  convert(thread_body, body);
+  convert(thread_body, body, mode);
 
   goto_programt::targett e=postamble.add_instruction(END_THREAD);
   e->source_location=thread_body.source_location();
diff --git a/src/goto-programs/goto_convert.h b/src/goto-programs/goto_convert.h
index 814731fbdb4..debcf251ca4 100644
--- a/src/goto-programs/goto_convert.h
+++ b/src/goto-programs/goto_convert.h
@@ -22,7 +22,8 @@ void goto_convert(
   const codet &code,
   symbol_table_baset &symbol_table,
   goto_programt &dest,
-  message_handlert &message_handler);
+  message_handlert &message_handler,
+  const irep_idt &mode);
 
 // start from "main"
 void goto_convert(
diff --git a/src/goto-programs/goto_convert_class.h b/src/goto-programs/goto_convert_class.h
index 84a90cb59cf..b362566893e 100644
--- a/src/goto-programs/goto_convert_class.h
+++ b/src/goto-programs/goto_convert_class.h
@@ -26,7 +26,8 @@ Author: Daniel Kroening, kroening@kroening.com
 class goto_convertt:public messaget
 {
 public:
-  void goto_convert(const codet &code, goto_programt &dest);
+  void
+  goto_convert(const codet &code, goto_programt &dest, const irep_idt &mode);
 
   goto_convertt(
     symbol_table_baset &_symbol_table,
@@ -47,7 +48,10 @@ class goto_convertt:public messaget
   namespacet ns;
   std::string tmp_symbol_prefix;
 
-  void goto_convert_rec(const codet &code, goto_programt &dest);
+  void goto_convert_rec(
+    const codet &code,
+    goto_programt &dest,
+    const irep_idt &mode);
 
   //
   // tools for symbols
@@ -64,7 +68,8 @@ class goto_convertt:public messaget
 
   symbol_exprt make_compound_literal(
     const exprt &expr,
-    goto_programt &dest);
+    goto_programt &dest,
+    const irep_idt &mode);
 
   //
   // translation of C expressions (with side effects)
@@ -74,18 +79,19 @@ class goto_convertt:public messaget
   void clean_expr(
     exprt &expr,
     goto_programt &dest,
-    bool result_is_used=true);
+    const irep_idt &mode,
+    bool result_is_used = true);
 
-  void clean_expr_address_of(
-    exprt &expr,
-    goto_programt &dest);
+  void
+  clean_expr_address_of(exprt &expr, goto_programt &dest, const irep_idt &mode);
 
   static bool needs_cleaning(const exprt &expr);
 
   void make_temp_symbol(
     exprt &expr,
     const std::string &suffix,
-    goto_programt &);
+    goto_programt &,
+    const irep_idt &mode);
 
   void rewrite_boolean(exprt &dest);
 
@@ -95,22 +101,27 @@ class goto_convertt:public messaget
   void remove_side_effect(
     side_effect_exprt &expr,
     goto_programt &dest,
+    const irep_idt &mode,
     bool result_is_used);
   void remove_assignment(
     side_effect_exprt &expr,
     goto_programt &dest,
-    bool result_is_used);
+    bool result_is_used,
+    const irep_idt &mode);
   void remove_pre(
     side_effect_exprt &expr,
     goto_programt &dest,
-    bool result_is_used);
+    bool result_is_used,
+    const irep_idt &mode);
   void remove_post(
     side_effect_exprt &expr,
     goto_programt &dest,
+    const irep_idt &mode,
     bool result_is_used);
   void remove_function_call(
     side_effect_exprt &expr,
     goto_programt &dest,
+    const irep_idt &mode,
     bool result_is_used);
   void remove_cpp_new(
     side_effect_exprt &expr,
@@ -123,6 +134,7 @@ class goto_convertt:public messaget
   void remove_malloc(
     side_effect_exprt &expr,
     goto_programt &dest,
+    const irep_idt &mode,
     bool result_is_used);
   void remove_temporary_object(
     side_effect_exprt &expr,
@@ -131,10 +143,12 @@ class goto_convertt:public messaget
   void remove_statement_expression(
     side_effect_exprt &expr,
     goto_programt &dest,
+    const irep_idt &mode,
     bool result_is_used);
   void remove_gcc_conditional_expression(
     exprt &expr,
-    goto_programt &dest);
+    goto_programt &dest,
+    const irep_idt &mode);
 
   virtual void do_cpp_new(
     const exprt &lhs,
@@ -168,13 +182,15 @@ class goto_convertt:public messaget
     const exprt &lhs,
     const exprt &function,
     const exprt::operandst &arguments,
-    goto_programt &dest);
+    goto_programt &dest,
+    const irep_idt &mode);
 
   virtual void do_function_call_if(
     const exprt &lhs,
     const if_exprt &function,
     const exprt::operandst &arguments,
-    goto_programt &dest);
+    goto_programt &dest,
+    const irep_idt &mode);
 
   virtual void do_function_call_symbol(
     const exprt &lhs,
@@ -195,35 +211,87 @@ class goto_convertt:public messaget
   //
   // conversion
   //
-  void convert_block(const code_blockt &code, goto_programt &dest);
-  void convert_decl(const code_declt &code, goto_programt &dest);
+  void convert_block(
+    const code_blockt &code,
+    goto_programt &dest,
+    const irep_idt &mode);
+  void convert_decl(
+    const code_declt &code,
+    goto_programt &dest,
+    const irep_idt &mode);
   void convert_decl_type(const codet &code, goto_programt &dest);
-  void convert_expression(const code_expressiont &code, goto_programt &dest);
-  void convert_assign(const code_assignt &code, goto_programt &dest);
+  void convert_expression(
+    const code_expressiont &code,
+    goto_programt &dest,
+    const irep_idt &mode);
+  void convert_assign(
+    const code_assignt &code,
+    goto_programt &dest,
+    const irep_idt &mode);
   void convert_cpp_delete(const codet &code, goto_programt &dest);
-  void convert_loop_invariant(const codet &code, goto_programt::targett loop);
-  void convert_for(const code_fort &code, goto_programt &dest);
-  void convert_while(const code_whilet &code, goto_programt &dest);
-  void convert_dowhile(const codet &code, goto_programt &dest);
-  void convert_assume(const code_assumet &code, goto_programt &dest);
-  void convert_assert(const code_assertt &code, goto_programt &dest);
-  void convert_switch(const code_switcht &code, goto_programt &dest);
-  void convert_break(const code_breakt &code, goto_programt &dest);
-  void convert_return(const code_returnt &code, goto_programt &dest);
-  void convert_continue(const code_continuet &code, goto_programt &dest);
-  void convert_ifthenelse(const code_ifthenelset &code, goto_programt &dest);
-  void convert_init(const codet &code, goto_programt &dest);
+  void convert_loop_invariant(
+    const codet &code,
+    goto_programt::targett loop,
+    const irep_idt &mode);
+  void
+  convert_for(const code_fort &code, goto_programt &dest, const irep_idt &mode);
+  void convert_while(
+    const code_whilet &code,
+    goto_programt &dest,
+    const irep_idt &mode);
+  void
+  convert_dowhile(const codet &code, goto_programt &dest, const irep_idt &mode);
+  void convert_assume(
+    const code_assumet &code,
+    goto_programt &dest,
+    const irep_idt &mode);
+  void convert_assert(
+    const code_assertt &code,
+    goto_programt &dest,
+    const irep_idt &mode);
+  void convert_switch(
+    const code_switcht &code,
+    goto_programt &dest,
+    const irep_idt &mode);
+  void convert_break(
+    const code_breakt &code,
+    goto_programt &dest,
+    const irep_idt &mode);
+  void convert_return(
+    const code_returnt &code,
+    goto_programt &dest,
+    const irep_idt &mode);
+  void convert_continue(
+    const code_continuet &code,
+    goto_programt &dest,
+    const irep_idt &mode);
+  void convert_ifthenelse(
+    const code_ifthenelset &code,
+    goto_programt &dest,
+    const irep_idt &mode);
+  void
+  convert_init(const codet &code, goto_programt &dest, const irep_idt &mode);
   void convert_goto(const codet &code, goto_programt &dest);
   void convert_gcc_computed_goto(const codet &code, goto_programt &dest);
   void convert_skip(const codet &code, goto_programt &dest);
   void convert_non_deterministic_goto(const codet &code, goto_programt &dest);
-  void convert_label(const code_labelt &code, goto_programt &dest);
+  void convert_label(
+    const code_labelt &code,
+    goto_programt &dest,
+    const irep_idt &mode);
   void convert_gcc_local_label(const codet &code, goto_programt &dest);
-  void convert_switch_case(const code_switch_caset &code, goto_programt &dest);
-  void convert_gcc_switch_case_range(const codet &code, goto_programt &dest);
+  void convert_switch_case(
+    const code_switch_caset &code,
+    goto_programt &dest,
+    const irep_idt &mode);
+  void convert_gcc_switch_case_range(
+    const codet &code,
+    goto_programt &dest,
+    const irep_idt &mode);
   void convert_function_call(
     const code_function_callt &code,
-    goto_programt &dest);
+    goto_programt &dest,
+    const irep_idt &mode);
   void convert_specc_notify(const codet &code, goto_programt &dest);
   void convert_specc_wait(const codet &code, goto_programt &dest);
   void convert_specc_par(const codet &code, goto_programt &dest);
@@ -233,16 +301,37 @@ class goto_convertt:public messaget
   void convert_end_thread(const codet &code, goto_programt &dest);
   void convert_atomic_begin(const codet &code, goto_programt &dest);
   void convert_atomic_end(const codet &code, goto_programt &dest);
-  void convert_msc_try_finally(const codet &code, goto_programt &dest);
-  void convert_msc_try_except(const codet &code, goto_programt &dest);
-  void convert_msc_leave(const codet &code, goto_programt &dest);
-  void convert_try_catch(const codet &code, goto_programt &dest);
-  void convert_CPROVER_try_catch(const codet &code, goto_programt &dest);
-  void convert_CPROVER_try_finally(const codet &code, goto_programt &dest);
-  void convert_CPROVER_throw(const codet &code, goto_programt &dest);
+  void convert_msc_try_finally(
+    const codet &code,
+    goto_programt &dest,
+    const irep_idt &mode);
+  void convert_msc_try_except(
+    const codet &code,
+    goto_programt &dest,
+    const irep_idt &mode);
+  void convert_msc_leave(
+    const codet &code,
+    goto_programt &dest,
+    const irep_idt &mode);
+  void convert_try_catch(
+    const codet &code,
+    goto_programt &dest,
+    const irep_idt &mode);
+  void convert_CPROVER_try_catch(
+    const codet &code,
+    goto_programt &dest,
+    const irep_idt &mode);
+  void convert_CPROVER_try_finally(
+    const codet &code,
+    goto_programt &dest,
+    const irep_idt &mode);
+  void convert_CPROVER_throw(
+    const codet &code,
+    goto_programt &dest,
+    const irep_idt &mode);
   void convert_asm(const code_asmt &code, goto_programt &dest);
 
-  void convert(const codet &code, goto_programt &dest);
+  void convert(const codet &code, goto_programt &dest, const irep_idt &mode);
 
   void copy(
     const codet &code,
@@ -259,18 +348,20 @@ class goto_convertt:public messaget
   void unwind_destructor_stack(
     const source_locationt &,
     std::size_t stack_size,
-    goto_programt &dest);
+    goto_programt &dest,
+    const irep_idt &mode);
   void unwind_destructor_stack(
     const source_locationt &,
     std::size_t stack_size,
     goto_programt &dest,
-    destructor_stackt &stack);
+    destructor_stackt &stack,
+    const irep_idt &mode);
 
   //
   // gotos
   //
 
-  void finish_gotos(goto_programt &dest);
+  void finish_gotos(goto_programt &dest, const irep_idt &mode);
   void finish_computed_gotos(goto_programt &dest);
   void finish_guarded_gotos(goto_programt &dest);
 
@@ -481,7 +572,8 @@ class goto_convertt:public messaget
     goto_programt &true_case,
     goto_programt &false_case,
     const source_locationt &,
-    goto_programt &dest);
+    goto_programt &dest,
+    const irep_idt &mode);
 
   // if(guard) goto target_true; else goto target_false;
   void generate_conditional_branch(
@@ -489,14 +581,16 @@ class goto_convertt:public messaget
     goto_programt::targett target_true,
     goto_programt::targett target_false,
     const source_locationt &,
-    goto_programt &dest);
+    goto_programt &dest,
+    const irep_idt &mode);
 
   // if(guard) goto target;
   void generate_conditional_branch(
     const exprt &guard,
     goto_programt::targett target_true,
     const source_locationt &,
-    goto_programt &dest);
+    goto_programt &dest,
+    const irep_idt &mode);
 
   // turn a OP b OP c into a list a, b, c
   static void collect_operands(
@@ -507,7 +601,8 @@ class goto_convertt:public messaget
   // START_THREAD; ... END_THREAD;
   void generate_thread_block(
     const code_blockt &thread_body,
-    goto_programt &dest);
+    goto_programt &dest,
+    const irep_idt &mode);
 
   //
   // misc
diff --git a/src/goto-programs/goto_convert_exceptions.cpp b/src/goto-programs/goto_convert_exceptions.cpp
index 14e0ff6208f..5686b41400c 100644
--- a/src/goto-programs/goto_convert_exceptions.cpp
+++ b/src/goto-programs/goto_convert_exceptions.cpp
@@ -15,7 +15,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 void goto_convertt::convert_msc_try_finally(
   const codet &code,
-  goto_programt &dest)
+  goto_programt &dest,
+  const irep_idt &mode)
 {
   if(code.operands().size()!=2)
   {
@@ -36,7 +37,7 @@ void goto_convertt::convert_msc_try_finally(
     targets.destructor_stack.push_back(to_code(code.op1()));
 
     // do 'try' code
-    convert(to_code(code.op0()), dest);
+    convert(to_code(code.op0()), dest, mode);
 
     // pop 'finally' from destructor stack
     targets.destructor_stack.pop_back();
@@ -45,7 +46,7 @@ void goto_convertt::convert_msc_try_finally(
   }
 
   // now add 'finally' code
-  convert(to_code(code.op1()), dest);
+  convert(to_code(code.op1()), dest, mode);
 
   // this is the target for 'leave'
   dest.destructive_append(tmp);
@@ -53,7 +54,8 @@ void goto_convertt::convert_msc_try_finally(
 
 void goto_convertt::convert_msc_try_except(
   const codet &code,
-  goto_programt &dest)
+  goto_programt &dest,
+  const irep_idt &mode)
 {
   if(code.operands().size()!=3)
   {
@@ -62,14 +64,15 @@ void goto_convertt::convert_msc_try_except(
     throw 0;
   }
 
-  convert(to_code(code.op0()), dest);
+  convert(to_code(code.op0()), dest, mode);
 
   // todo: generate exception tracking
 }
 
 void goto_convertt::convert_msc_leave(
   const codet &code,
-  goto_programt &dest)
+  goto_programt &dest,
+  const irep_idt &mode)
 {
   if(!targets.leave_set)
   {
@@ -85,7 +88,7 @@ void goto_convertt::convert_msc_leave(
   {
     codet d_code=targets.destructor_stack[d-1];
     d_code.add_source_location()=code.source_location();
-    convert(d_code, dest);
+    convert(d_code, dest, mode);
   }
 
   goto_programt::targett t=dest.add_instruction();
@@ -95,7 +98,8 @@ void goto_convertt::convert_msc_leave(
 
 void goto_convertt::convert_try_catch(
   const codet &code,
-  goto_programt &dest)
+  goto_programt &dest,
+  const irep_idt &mode)
 {
   assert(code.operands().size()>=2);
 
@@ -117,7 +121,7 @@ void goto_convertt::convert_try_catch(
   end_target->make_skip();
 
   // the first operand is the 'try' block
-  convert(to_code(code.op0()), dest);
+  convert(to_code(code.op0()), dest, mode);
 
   // add the CATCH-pop to the end of the 'try' block
   goto_programt::targett catch_pop_instruction=dest.add_instruction();
@@ -136,7 +140,7 @@ void goto_convertt::convert_try_catch(
       code_push_catcht::exception_list_entryt(block.get(ID_exception_id)));
 
     goto_programt tmp;
-    convert(block, tmp);
+    convert(block, tmp, mode);
     catch_push_instruction->targets.push_back(tmp.instructions.begin());
     dest.destructive_append(tmp);
 
@@ -152,7 +156,8 @@ void goto_convertt::convert_try_catch(
 
 void goto_convertt::convert_CPROVER_try_catch(
   const codet &code,
-  goto_programt &dest)
+  goto_programt &dest,
+  const irep_idt &mode)
 {
   if(code.operands().size()!=2)
   {
@@ -178,7 +183,7 @@ void goto_convertt::convert_CPROVER_try_catch(
   targets.destructor_stack.push_back(catch_code);
 
   // now convert 'try' code
-  convert(to_code(code.op0()), dest);
+  convert(to_code(code.op0()), dest, mode);
 
   // pop 'catch' code off stack
   targets.destructor_stack.pop_back();
@@ -189,7 +194,8 @@ void goto_convertt::convert_CPROVER_try_catch(
 
 void goto_convertt::convert_CPROVER_throw(
   const codet &code,
-  goto_programt &dest)
+  goto_programt &dest,
+  const irep_idt &mode)
 {
   // set the 'exception' flag
   {
@@ -205,7 +211,7 @@ void goto_convertt::convert_CPROVER_throw(
   {
     // need to process destructor stack
     unwind_destructor_stack(
-      code.source_location(), targets.throw_stack_size, dest);
+      code.source_location(), targets.throw_stack_size, dest, mode);
 
     // add goto
     goto_programt::targett t=dest.add_instruction();
@@ -215,7 +221,7 @@ void goto_convertt::convert_CPROVER_throw(
   else // otherwise, we do a return
   {
     // need to process destructor stack
-    unwind_destructor_stack(code.source_location(), 0, dest);
+    unwind_destructor_stack(code.source_location(), 0, dest, mode);
 
     // add goto
     goto_programt::targett t=dest.add_instruction();
@@ -226,7 +232,8 @@ void goto_convertt::convert_CPROVER_throw(
 
 void goto_convertt::convert_CPROVER_try_finally(
   const codet &code,
-  goto_programt &dest)
+  goto_programt &dest,
+  const irep_idt &mode)
 {
   if(code.operands().size()!=2)
   {
@@ -239,13 +246,13 @@ void goto_convertt::convert_CPROVER_try_finally(
   targets.destructor_stack.push_back(to_code(code.op1()));
 
   // do 'try' code
-  convert(to_code(code.op0()), dest);
+  convert(to_code(code.op0()), dest, mode);
 
   // pop 'finally' from destructor stack
   targets.destructor_stack.pop_back();
 
   // now add 'finally' code
-  convert(to_code(code.op1()), dest);
+  convert(to_code(code.op1()), dest, mode);
 }
 
 symbol_exprt goto_convertt::exception_flag()
@@ -273,20 +280,19 @@ symbol_exprt goto_convertt::exception_flag()
 void goto_convertt::unwind_destructor_stack(
   const source_locationt &source_location,
   std::size_t final_stack_size,
-  goto_programt &dest)
+  goto_programt &dest,
+  const irep_idt &mode)
 {
   unwind_destructor_stack(
-    source_location,
-    final_stack_size,
-    dest,
-    targets.destructor_stack);
+    source_location, final_stack_size, dest, targets.destructor_stack, mode);
 }
 
 void goto_convertt::unwind_destructor_stack(
   const source_locationt &source_location,
   std::size_t final_stack_size,
   goto_programt &dest,
-  destructor_stackt &destructor_stack)
+  destructor_stackt &destructor_stack,
+  const irep_idt &mode)
 {
   // There might be exceptions happening in the exception
   // handler. We thus pop off the stack, and then later
@@ -301,7 +307,7 @@ void goto_convertt::unwind_destructor_stack(
     // pop now to avoid doing this again
     destructor_stack.pop_back();
 
-    convert(d_code, dest);
+    convert(d_code, dest, mode);
   }
 
   // Now restore old stack.
diff --git a/src/goto-programs/goto_convert_function_call.cpp b/src/goto-programs/goto_convert_function_call.cpp
index f1511b76a77..1913ed2c30d 100644
--- a/src/goto-programs/goto_convert_function_call.cpp
+++ b/src/goto-programs/goto_convert_function_call.cpp
@@ -23,20 +23,23 @@ Author: Daniel Kroening, kroening@kroening.com
 
 void goto_convertt::convert_function_call(
   const code_function_callt &function_call,
-  goto_programt &dest)
+  goto_programt &dest,
+  const irep_idt &mode)
 {
   do_function_call(
     function_call.lhs(),
     function_call.function(),
     function_call.arguments(),
-    dest);
+    dest,
+    mode);
 }
 
 void goto_convertt::do_function_call(
   const exprt &lhs,
   const exprt &function,
   const exprt::operandst &arguments,
-  goto_programt &dest)
+  goto_programt &dest,
+  const irep_idt &mode)
 {
   // make it all side effect free
 
@@ -46,9 +49,9 @@ void goto_convertt::do_function_call(
   exprt::operandst new_arguments=arguments;
 
   if(!new_lhs.is_nil())
-    clean_expr(new_lhs, dest);
+    clean_expr(new_lhs, dest, mode);
 
-  clean_expr(new_function, dest);
+  clean_expr(new_function, dest, mode);
 
   // the arguments of __noop do not get evaluated
   if(new_function.id()==ID_symbol &&
@@ -58,13 +61,14 @@ void goto_convertt::do_function_call(
   }
 
   Forall_expr(it, new_arguments)
-    clean_expr(*it, dest);
+    clean_expr(*it, dest, mode);
 
   // split on the function
 
   if(new_function.id()==ID_if)
   {
-    do_function_call_if(new_lhs, to_if_expr(new_function), new_arguments, dest);
+    do_function_call_if(
+      new_lhs, to_if_expr(new_function), new_arguments, dest, mode);
   }
   else if(new_function.id()==ID_symbol)
   {
@@ -92,7 +96,8 @@ void goto_convertt::do_function_call_if(
   const exprt &lhs,
   const if_exprt &function,
   const exprt::operandst &arguments,
-  goto_programt &dest)
+  goto_programt &dest,
+  const irep_idt &mode)
 {
   // case split
 
@@ -121,7 +126,7 @@ void goto_convertt::do_function_call_if(
   goto_programt tmp_y;
   goto_programt::targett y;
 
-  do_function_call(lhs, function.false_case(), arguments, tmp_y);
+  do_function_call(lhs, function.false_case(), arguments, tmp_y, mode);
 
   if(tmp_y.instructions.empty())
     y=tmp_y.add_instruction(SKIP);
@@ -137,7 +142,7 @@ void goto_convertt::do_function_call_if(
   // w: f();
   goto_programt tmp_w;
 
-  do_function_call(lhs, function.true_case(), arguments, tmp_w);
+  do_function_call(lhs, function.true_case(), arguments, tmp_w, mode);
 
   if(tmp_w.instructions.empty())
     tmp_w.add_instruction(SKIP);
diff --git a/src/goto-programs/goto_convert_functions.cpp b/src/goto-programs/goto_convert_functions.cpp
index 6d6b2b7441e..f2c1895c68a 100644
--- a/src/goto-programs/goto_convert_functions.cpp
+++ b/src/goto-programs/goto_convert_functions.cpp
@@ -141,6 +141,7 @@ void goto_convert_functionst::convert_function(
   goto_functionst::goto_functiont &f)
 {
   const symbolt &symbol=ns.lookup(identifier);
+  const irep_idt mode = symbol.mode;
 
   if(f.body_available())
     return; // already converted
@@ -184,7 +185,7 @@ void goto_convert_functionst::convert_function(
     f.type.return_type().id()!=ID_constructor &&
     f.type.return_type().id()!=ID_destructor;
 
-  goto_convert_rec(code, f.body);
+  goto_convert_rec(code, f.body, mode);
 
   // add non-det return value, if needed
   if(targets.has_return_value)
diff --git a/src/goto-programs/goto_convert_side_effect.cpp b/src/goto-programs/goto_convert_side_effect.cpp
index def8d98b170..0438f812b28 100644
--- a/src/goto-programs/goto_convert_side_effect.cpp
+++ b/src/goto-programs/goto_convert_side_effect.cpp
@@ -36,7 +36,8 @@ bool goto_convertt::has_function_call(const exprt &expr)
 void goto_convertt::remove_assignment(
   side_effect_exprt &expr,
   goto_programt &dest,
-  bool result_is_used)
+  bool result_is_used,
+  const irep_idt &mode)
 {
   const irep_idt statement=expr.get_statement();
 
@@ -45,7 +46,7 @@ void goto_convertt::remove_assignment(
     exprt tmp=expr;
     tmp.id(ID_code);
     // just interpret as code
-    convert_assign(to_code_assign(to_code(tmp)), dest);
+    convert_assign(to_code_assign(to_code(tmp)), dest, mode);
   }
   else if(statement==ID_assign_plus ||
           statement==ID_assign_minus ||
@@ -120,7 +121,7 @@ void goto_convertt::remove_assignment(
     code_assignt assignment(expr.op0(), rhs);
     assignment.add_source_location()=expr.source_location();
 
-    convert(assignment, dest);
+    convert(assignment, dest, mode);
   }
   else
     UNREACHABLE;
@@ -139,7 +140,8 @@ void goto_convertt::remove_assignment(
 void goto_convertt::remove_pre(
   side_effect_exprt &expr,
   goto_programt &dest,
-  bool result_is_used)
+  bool result_is_used,
+  const irep_idt &mode)
 {
   if(expr.operands().size()!=1)
   {
@@ -211,7 +213,7 @@ void goto_convertt::remove_pre(
   code_assignt assignment(expr.op0(), rhs);
   assignment.add_source_location()=expr.find_source_location();
 
-  convert(assignment, dest);
+  convert(assignment, dest, mode);
 
   if(result_is_used)
   {
@@ -226,6 +228,7 @@ void goto_convertt::remove_pre(
 void goto_convertt::remove_post(
   side_effect_exprt &expr,
   goto_programt &dest,
+  const irep_idt &mode,
   bool result_is_used)
 {
   goto_programt tmp1, tmp2;
@@ -312,14 +315,14 @@ void goto_convertt::remove_post(
   code_assignt assignment(expr.op0(), rhs);
   assignment.add_source_location()=expr.find_source_location();
 
-  convert(assignment, tmp2);
+  convert(assignment, tmp2, mode);
 
   // fix up the expression, if needed
 
   if(result_is_used)
   {
     exprt tmp=expr.op0();
-    make_temp_symbol(tmp, "post", dest);
+    make_temp_symbol(tmp, "post", dest, mode);
     expr.swap(tmp);
   }
   else
@@ -332,6 +335,7 @@ void goto_convertt::remove_post(
 void goto_convertt::remove_function_call(
   side_effect_exprt &expr,
   goto_programt &dest,
+  const irep_idt &mode,
   bool result_is_used)
 {
   if(!result_is_used)
@@ -342,7 +346,7 @@ void goto_convertt::remove_function_call(
     call.arguments()=expr.op1().operands();
     call.add_source_location()=expr.source_location();
     call.lhs().make_nil();
-    convert_function_call(call, dest);
+    convert_function_call(call, dest, mode);
     expr.make_nil();
     return;
   }
@@ -394,7 +398,7 @@ void goto_convertt::remove_function_call(
     code_declt decl;
     decl.symbol()=new_symbol.symbol_expr();
     decl.add_source_location()=new_symbol.location;
-    convert_decl(decl, dest);
+    convert_decl(decl, dest, mode);
   }
 
   {
@@ -404,7 +408,7 @@ void goto_convertt::remove_function_call(
     call.function()=expr.op0();
     call.arguments()=expr.op1().operands();
     call.add_source_location()=new_symbol.location;
-    convert_function_call(call, dest);
+    convert_function_call(call, dest, mode);
   }
 
   static_cast<exprt &>(expr)=new_symbol.symbol_expr();
@@ -440,7 +444,7 @@ void goto_convertt::remove_cpp_new(
   code_declt decl;
   decl.symbol()=new_symbol.symbol_expr();
   decl.add_source_location()=new_symbol.location;
-  convert_decl(decl, dest);
+  convert_decl(decl, dest, ID_cpp);
 
   call=code_assignt(new_symbol.symbol_expr(), expr);
 
@@ -449,7 +453,7 @@ void goto_convertt::remove_cpp_new(
   else
     expr.make_nil();
 
-  convert(call, dest);
+  convert(call, dest, ID_cpp);
 }
 
 void goto_convertt::remove_cpp_delete(
@@ -474,6 +478,7 @@ void goto_convertt::remove_cpp_delete(
 void goto_convertt::remove_malloc(
   side_effect_exprt &expr,
   goto_programt &dest,
+  const irep_idt &mode,
   bool result_is_used)
 {
   codet call;
@@ -493,7 +498,7 @@ void goto_convertt::remove_malloc(
     code_declt decl;
     decl.symbol()=new_symbol.symbol_expr();
     decl.add_source_location()=new_symbol.location;
-    convert_decl(decl, dest);
+    convert_decl(decl, dest, mode);
 
     call=code_assignt(new_symbol.symbol_expr(), expr);
     call.add_source_location()=expr.source_location();
@@ -506,7 +511,7 @@ void goto_convertt::remove_malloc(
     call.move_to_operands(expr);
   }
 
-  convert(call, dest);
+  convert(call, dest, mode);
 }
 
 void goto_convertt::remove_temporary_object(
@@ -514,6 +519,7 @@ void goto_convertt::remove_temporary_object(
   goto_programt &dest,
   bool result_is_used)
 {
+  const irep_idt &mode = expr.get(ID_mode);
   if(expr.operands().size()!=1 &&
      !expr.operands().empty())
   {
@@ -523,13 +529,13 @@ void goto_convertt::remove_temporary_object(
   }
 
   symbolt &new_symbol = new_tmp_symbol(
-    expr.type(), "obj", dest, expr.find_source_location(), expr.get(ID_mode));
+    expr.type(), "obj", dest, expr.find_source_location(), mode);
 
   if(expr.operands().size()==1)
   {
     const code_assignt assignment(new_symbol.symbol_expr(), expr.op0());
 
-    convert(assignment, dest);
+    convert(assignment, dest, mode);
   }
 
   if(expr.find(ID_initializer).is_not_nil())
@@ -538,7 +544,7 @@ void 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);
+    convert(to_code(initializer), dest, mode);
   }
 
   static_cast<exprt &>(expr)=new_symbol.symbol_expr();
@@ -547,6 +553,7 @@ void goto_convertt::remove_temporary_object(
 void goto_convertt::remove_statement_expression(
   side_effect_exprt &expr,
   goto_programt &dest,
+  const irep_idt &mode,
   bool result_is_used)
 {
   // This is a gcc extension of the form ({ ....; expr; })
@@ -572,7 +579,7 @@ void goto_convertt::remove_statement_expression(
 
   if(!result_is_used)
   {
-    convert(code, dest);
+    convert(code, dest, mode);
     expr.make_nil();
     return;
   }
@@ -598,11 +605,7 @@ void 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,
-    expr.get(ID_mode));
+    expr.type(), "statement_expression", dest, source_location, mode);
 
   symbol_exprt tmp_symbol_expr(new_symbol.name, new_symbol.type);
   tmp_symbol_expr.add_source_location()=source_location;
@@ -631,7 +634,7 @@ void goto_convertt::remove_statement_expression(
 
   {
     goto_programt tmp;
-    convert(code, tmp);
+    convert(code, tmp, mode);
     dest.destructive_append(tmp);
   }
 
@@ -641,12 +644,13 @@ void goto_convertt::remove_statement_expression(
 void goto_convertt::remove_side_effect(
   side_effect_exprt &expr,
   goto_programt &dest,
+  const irep_idt &mode,
   bool result_is_used)
 {
   const irep_idt &statement=expr.get_statement();
 
   if(statement==ID_function_call)
-    remove_function_call(expr, dest, result_is_used);
+    remove_function_call(expr, dest, mode, result_is_used);
   else if(statement==ID_assign ||
           statement==ID_assign_plus ||
           statement==ID_assign_minus ||
@@ -659,13 +663,13 @@ void goto_convertt::remove_side_effect(
           statement==ID_assign_ashr ||
           statement==ID_assign_shl ||
           statement==ID_assign_mod)
-    remove_assignment(expr, dest, result_is_used);
+    remove_assignment(expr, dest, result_is_used, mode);
   else if(statement==ID_postincrement ||
           statement==ID_postdecrement)
-    remove_post(expr, dest, result_is_used);
+    remove_post(expr, dest, mode, result_is_used);
   else if(statement==ID_preincrement ||
           statement==ID_predecrement)
-    remove_pre(expr, dest, result_is_used);
+    remove_pre(expr, dest, result_is_used, mode);
   else if(statement==ID_cpp_new ||
           statement==ID_cpp_new_array)
     remove_cpp_new(expr, dest, result_is_used);
@@ -673,11 +677,11 @@ void goto_convertt::remove_side_effect(
           statement==ID_cpp_delete_array)
     remove_cpp_delete(expr, dest, result_is_used);
   else if(statement==ID_allocate)
-    remove_malloc(expr, dest, result_is_used);
+    remove_malloc(expr, dest, mode, result_is_used);
   else if(statement==ID_temporary_object)
     remove_temporary_object(expr, dest, result_is_used);
   else if(statement==ID_statement_expression)
-    remove_statement_expression(expr, dest, result_is_used);
+    remove_statement_expression(expr, dest, mode, result_is_used);
   else if(statement==ID_nondet)
   {
     // these are fine
diff --git a/src/java_bytecode/remove_java_new.cpp b/src/java_bytecode/remove_java_new.cpp
index c1354c53e16..1d88c7ddbcd 100644
--- a/src/java_bytecode/remove_java_new.cpp
+++ b/src/java_bytecode/remove_java_new.cpp
@@ -309,7 +309,7 @@ goto_programt::targett remove_java_newt::lower_java_new_array(
     for_loop.iter() = inc;
     for_loop.body() = for_body;
 
-    goto_convert(for_loop, symbol_table, tmp, get_message_handler());
+    goto_convert(for_loop, symbol_table, tmp, get_message_handler(), ID_java);
 
     // lower new side effects recursively
     lower_java_new(tmp);
diff --git a/src/jbmc/jbmc_parse_options.cpp b/src/jbmc/jbmc_parse_options.cpp
index 031d7aec587..c75816a83fe 100644
--- a/src/jbmc/jbmc_parse_options.cpp
+++ b/src/jbmc/jbmc_parse_options.cpp
@@ -756,10 +756,7 @@ void jbmc_parse_optionst::process_goto_function(
         ? std::stoul(cmdline.get_value("java-max-input-tree-depth"))
         : MAX_NONDET_TREE_DEPTH;
 
-    convert_nondet(
-      function,
-      get_message_handler(),
-      factory_params);
+    convert_nondet(function, get_message_handler(), factory_params, ID_java);
 
     // add generic checks
     goto_check(ns, options, ID_java, function.get_goto_function());