diff --git a/jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp b/jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp
index c590c545bb5..380282d32ff 100644
--- a/jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_concurrency_instrumentation.cpp
@@ -253,7 +253,7 @@ static void instrument_synchronized_code(
   catch_block.add(monitorexit);
 
   // Re-throw exception
-  side_effect_expr_throwt throw_expr;
+  side_effect_expr_throwt throw_expr(irept(), typet(), code.source_location());
   throw_expr.copy_to_operands(catch_var);
   catch_block.add(code_expressiont(throw_expr));
 
diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp
index 6105841a75c..3c85b9c7401 100644
--- a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp
@@ -812,9 +812,10 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
     code_declt declare_cloned(local_symexpr);
     clone_body.move_to_operands(declare_cloned);
 
+    source_locationt location;
+    location.set_function(local_name);
     side_effect_exprt java_new_array(
-      ID_java_new_array,
-      java_reference_type(symbol_type));
+      ID_java_new_array, java_reference_type(symbol_type), location);
     dereference_exprt old_array(this_symbol.symbol_expr(), symbol_type);
     dereference_exprt new_array(local_symexpr, symbol_type);
     member_exprt old_length(
@@ -860,7 +861,7 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
     copy_loop.cond()=
       binary_relation_exprt(index_symexpr, ID_lt, old_length);
 
-    side_effect_exprt inc(ID_assign);
+    side_effect_exprt inc(ID_assign, typet(), location);
     inc.operands().resize(2);
     inc.op0()=index_symexpr;
     inc.op1()=plus_exprt(index_symexpr, from_integer(1, index_symexpr.type()));
diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
index 63b2198431f..21cac212cd4 100644
--- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
@@ -2328,8 +2328,7 @@ void java_bytecode_convert_methodt::convert_athrow(
   }
   else
   {
-    side_effect_expr_throwt throw_expr;
-    throw_expr.add_source_location() = location;
+    side_effect_expr_throwt throw_expr(irept(), typet(), location);
     throw_expr.copy_to_operands(op[0]);
     c = code_expressiont(throw_expr);
   }
@@ -2454,14 +2453,11 @@ void java_bytecode_convert_methodt::convert_multianewarray(
   codet &c,
   exprt::operandst &results)
 {
+  PRECONDITION(!location.get_line().empty());
   const reference_typet ref_type = java_reference_type(arg0.type());
-
-  side_effect_exprt java_new_array(ID_java_new_array, ref_type);
+  side_effect_exprt java_new_array(ID_java_new_array, ref_type, location);
   java_new_array.operands() = op;
 
-  if(!location.get_line().empty())
-    java_new_array.add_source_location() = location;
-
   code_blockt create;
 
   if(max_array_length != 0)
@@ -2516,12 +2512,9 @@ void java_bytecode_convert_methodt::convert_newarray(
 
   const reference_typet ref_type = java_array_type(element_type);
 
-  side_effect_exprt java_new_array(ID_java_new_array, ref_type);
+  side_effect_exprt java_new_array(ID_java_new_array, ref_type, location);
   java_new_array.copy_to_operands(op[0]);
 
-  if(!location.get_line().empty())
-    java_new_array.add_source_location() = location;
-
   c = code_blockt();
 
   if(max_array_length != 0)
@@ -2543,7 +2536,7 @@ void java_bytecode_convert_methodt::convert_new(
   exprt::operandst &results)
 {
   const reference_typet ref_type = java_reference_type(arg0.type());
-  side_effect_exprt java_new_expr(ID_java_new, ref_type);
+  side_effect_exprt java_new_expr(ID_java_new, ref_type, location);
 
   if(!location.get_line().empty())
     java_new_expr.add_source_location() = location;
diff --git a/jbmc/src/java_bytecode/java_bytecode_instrument.cpp b/jbmc/src/java_bytecode/java_bytecode_instrument.cpp
index 76ee70ee262..9eee6a4131d 100644
--- a/jbmc/src/java_bytecode/java_bytecode_instrument.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_instrument.cpp
@@ -122,10 +122,10 @@ codet java_bytecode_instrumentt::throw_exception(
       ID_java,
       symbol_table);
 
-  side_effect_exprt new_instance(ID_java_new, exc_ptr_type);
+  side_effect_exprt new_instance(ID_java_new, exc_ptr_type, original_loc);
   code_assignt assign_new(new_symbol.symbol_expr(), new_instance);
 
-  side_effect_expr_throwt throw_expr;
+  side_effect_expr_throwt throw_expr(irept(), typet(), original_loc);
   throw_expr.copy_to_operands(new_symbol.symbol_expr());
 
   code_blockt throw_code;
diff --git a/jbmc/src/java_bytecode/java_bytecode_typecheck_expr.cpp b/jbmc/src/java_bytecode/java_bytecode_typecheck_expr.cpp
index deeb269eb76..88ba3ab02e4 100644
--- a/jbmc/src/java_bytecode/java_bytecode_typecheck_expr.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_typecheck_expr.cpp
@@ -160,6 +160,6 @@ void java_bytecode_typecheckt::typecheck_expr_member(member_exprt &expr)
             << component_name << "` in class hierarchy" << eom;
 
   // We replace by a non-det of same type
-  side_effect_expr_nondett nondet(expr.type());
+  side_effect_expr_nondett nondet(expr.type(), expr.source_location());
   expr.swap(nondet);
 }
diff --git a/jbmc/src/java_bytecode/java_entry_point.cpp b/jbmc/src/java_bytecode/java_entry_point.cpp
index 6c56faa228c..5d14e771bb5 100644
--- a/jbmc/src/java_bytecode/java_entry_point.cpp
+++ b/jbmc/src/java_bytecode/java_entry_point.cpp
@@ -162,7 +162,7 @@ static void java_static_lifetime_init(
         // Call the literal initializer method instead of a nondet initializer:
 
         // For arguments we can't parse yet:
-        side_effect_expr_nondett nondet_bool(java_boolean_type());
+        side_effect_expr_nondett nondet_bool(java_boolean_type(), sym.location);
 
         // Argument order is: name, isAnnotation, isArray, isInterface,
         // isSynthetic, isLocalClass, isMemberClass, isEnum
diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp
index 24939ebe1a0..d9461898a10 100644
--- a/jbmc/src/java_bytecode/java_object_factory.cpp
+++ b/jbmc/src/java_bytecode/java_object_factory.cpp
@@ -69,13 +69,15 @@ class java_object_factoryt
     const typet &target_type,
     allocation_typet alloc_type,
     size_t depth,
-    update_in_placet update_in_place);
+    update_in_placet update_in_place,
+    const source_locationt &location);
 
   void allocate_nondet_length_array(
     code_blockt &assignments,
     const exprt &lhs,
     const exprt &max_length_expr,
-    const typet &element_type);
+    const typet &element_type,
+    const source_locationt &location);
 
 public:
   java_object_factoryt(
@@ -102,7 +104,8 @@ class java_object_factoryt
     code_blockt &assignments,
     const exprt &expr,
     size_t depth,
-    update_in_placet);
+    update_in_placet,
+    const source_locationt &location);
 
   void gen_nondet_init(
     code_blockt &assignments,
@@ -114,7 +117,8 @@ class java_object_factoryt
     bool override_,
     const typet &override_type,
     size_t depth,
-    update_in_placet);
+    update_in_placet,
+    const source_locationt &location);
 
 private:
   void gen_nondet_pointer_init(
@@ -123,7 +127,8 @@ class java_object_factoryt
     allocation_typet alloc_type,
     const pointer_typet &pointer_type,
     size_t depth,
-    const update_in_placet &update_in_place);
+    const update_in_placet &update_in_place,
+    const source_locationt &location);
 
   void gen_nondet_struct_init(
     code_blockt &assignments,
@@ -134,13 +139,15 @@ class java_object_factoryt
     allocation_typet alloc_type,
     const struct_typet &struct_type,
     size_t depth,
-    const update_in_placet &update_in_place);
+    const update_in_placet &update_in_place,
+    const source_locationt &location);
 
   symbol_exprt gen_nondet_subtype_pointer_init(
     code_blockt &assignments,
     allocation_typet alloc_type,
     const pointer_typet &substitute_pointer_type,
-    size_t depth);
+    size_t depth,
+    const source_locationt &location);
 };
 
 /// Generates code for allocating a dynamic object. This is used in
@@ -173,7 +180,8 @@ exprt allocate_dynamic_object(
   {
     INVARIANT(!object_size.is_nil(), "Size of Java objects should be known");
     // malloc expression
-    side_effect_exprt malloc_expr(ID_allocate, pointer_type(allocate_type));
+    side_effect_exprt malloc_expr(
+      ID_allocate, pointer_type(allocate_type), loc);
     malloc_expr.copy_to_operands(object_size);
     malloc_expr.copy_to_operands(false_exprt());
     // create a symbol for the malloc expression so we can initialize
@@ -371,7 +379,8 @@ void java_object_factoryt::gen_pointer_target_init(
   const typet &target_type,
   allocation_typet alloc_type,
   size_t depth,
-  update_in_placet update_in_place)
+  update_in_placet update_in_place,
+  const source_locationt &location)
 {
   PRECONDITION(expr.type().id()==ID_pointer);
   PRECONDITION(update_in_place!=update_in_placet::MAY_UPDATE_IN_PLACE);
@@ -382,10 +391,7 @@ void java_object_factoryt::gen_pointer_target_init(
        "java::array["))
   {
     gen_nondet_array_init(
-      assignments,
-      expr,
-      depth+1,
-      update_in_place);
+      assignments, expr, depth + 1, update_in_place, location);
   }
   else
   {
@@ -425,14 +431,15 @@ void java_object_factoryt::gen_pointer_target_init(
     gen_nondet_init(
       assignments,
       init_expr,
-      false,   // is_sub
-      "",      // class_identifier
-      false,   // skip_classid
+      false, // is_sub
+      "",    // class_identifier
+      false, // skip_classid
       alloc_type,
-      false,   // override
-      typet(), // override type immaterial
-      depth+1,
-      update_in_place);
+      false,
+      typet(),
+      depth + 1,
+      update_in_place,
+      location);
   }
 }
 
@@ -503,7 +510,7 @@ static mp_integer max_value(const typet &type)
 /// \return code allocation object and assigning `lhs`
 static codet make_allocate_code(const symbol_exprt &lhs, const exprt &size)
 {
-  side_effect_exprt alloc(ID_allocate, lhs.type());
+  side_effect_exprt alloc(ID_allocate, lhs.type(), lhs.source_location());
   alloc.copy_to_operands(size);
   alloc.copy_to_operands(false_exprt());
   return code_assignt(lhs, alloc);
@@ -599,7 +606,7 @@ bool initialize_nondet_string_fields(
     ID_java,
     symbol_table);
   const symbol_exprt length_expr = length_sym.symbol_expr();
-  const side_effect_expr_nondett nondet_length(length_expr.type());
+  const side_effect_expr_nondett nondet_length(length_expr.type(), loc);
   code.add(code_declt(length_expr));
   code.add(code_assignt(length_expr, nondet_length));
 
@@ -687,7 +694,8 @@ void java_object_factoryt::gen_nondet_pointer_init(
   allocation_typet alloc_type,
   const pointer_typet &pointer_type,
   size_t depth,
-  const update_in_placet &update_in_place)
+  const update_in_placet &update_in_place,
+  const source_locationt &location)
 {
   PRECONDITION(expr.type().id()==ID_pointer);
   const pointer_typet &replacement_pointer_type =
@@ -709,7 +717,7 @@ void java_object_factoryt::gen_nondet_pointer_init(
       replacement_pointer_type, ns.follow(replacement_pointer_type.subtype()));
 
     const symbol_exprt real_pointer_symbol = gen_nondet_subtype_pointer_init(
-      assignments, alloc_type, replacement_pointer_type, depth);
+      assignments, alloc_type, replacement_pointer_type, depth, location);
 
     // Having created a pointer to object of type replacement_pointer_type
     // we now assign it back to the original pointer with a cast
@@ -771,7 +779,8 @@ void java_object_factoryt::gen_nondet_pointer_init(
       subtype,
       alloc_type,
       depth,
-      update_in_placet::MUST_UPDATE_IN_PLACE);
+      update_in_placet::MUST_UPDATE_IN_PLACE,
+      location);
   }
 
   // if we MUST_UPDATE_IN_PLACE, then the job is done, we copy the code emitted
@@ -793,7 +802,8 @@ void java_object_factoryt::gen_nondet_pointer_init(
     subtype,
     alloc_type,
     depth,
-    update_in_placet::NO_UPDATE_IN_PLACE);
+    update_in_placet::NO_UPDATE_IN_PLACE,
+    location);
 
   auto set_null_inst=get_null_assignment(expr, pointer_type);
 
@@ -828,7 +838,7 @@ void java_object_factoryt::gen_nondet_pointer_init(
     //             tmp$<temporary_counter>>
     // }
     code_ifthenelset null_check;
-    null_check.cond()=side_effect_expr_nondett(bool_typet());
+    null_check.cond() = side_effect_expr_nondett(bool_typet(), location);
     null_check.then_case()=set_null_inst;
     null_check.else_case()=non_null_inst;
 
@@ -847,7 +857,8 @@ void java_object_factoryt::gen_nondet_pointer_init(
       "No-update and must-update should have already been resolved");
 
     code_ifthenelset update_check;
-    update_check.cond()=side_effect_expr_nondett(bool_typet());
+    update_check.cond() =
+      side_effect_expr_nondett(bool_typet(), expr.source_location());
     update_check.then_case()=update_in_place_assignments;
     update_check.else_case()=new_object_assignments;
 
@@ -883,7 +894,8 @@ symbol_exprt java_object_factoryt::gen_nondet_subtype_pointer_init(
   code_blockt &assignments,
   allocation_typet alloc_type,
   const pointer_typet &replacement_pointer,
-  size_t depth)
+  size_t depth,
+  const source_locationt &location)
 {
   symbolt new_symbol = get_fresh_aux_symbol(
     replacement_pointer,
@@ -897,14 +909,15 @@ symbol_exprt java_object_factoryt::gen_nondet_subtype_pointer_init(
   gen_nondet_init(
     assignments,
     new_symbol.symbol_expr(),
-    false,   // is_sub
-    "",      // class_identifier
-    false,   // skip_classid
+    false, // is_sub
+    "",    // class_identifier
+    false, // skip_classid
     alloc_type,
     false,   // override
     typet(), // override_type
     depth,
-    update_in_placet::NO_UPDATE_IN_PLACE);
+    update_in_placet::NO_UPDATE_IN_PLACE,
+    location);
 
   return new_symbol.symbol_expr();
 }
@@ -947,7 +960,8 @@ void java_object_factoryt::gen_nondet_struct_init(
   allocation_typet alloc_type,
   const struct_typet &struct_type,
   size_t depth,
-  const update_in_placet &update_in_place)
+  const update_in_placet &update_in_place,
+  const source_locationt &location)
 {
   PRECONDITION(ns.follow(expr.type()).id()==ID_struct);
   PRECONDITION(struct_type.id()==ID_struct);
@@ -1049,12 +1063,13 @@ void java_object_factoryt::gen_nondet_struct_init(
         me,
         _is_sub,
         class_identifier,
-        false,   // skip_classid
+        false, // skip_classid
         alloc_type,
         false,   // override
         typet(), // override_type
         depth,
-        substruct_in_place);
+        substruct_in_place,
+        location);
     }
   }
 
@@ -1122,7 +1137,8 @@ void java_object_factoryt::gen_nondet_init(
   bool override_,
   const typet &override_type,
   size_t depth,
-  update_in_placet update_in_place)
+  update_in_placet update_in_place,
+  const source_locationt &location)
 {
   const typet &type=
     override_ ? ns.follow(override_type) : ns.follow(expr.type());
@@ -1147,7 +1163,8 @@ void java_object_factoryt::gen_nondet_init(
       alloc_type,
       pointer_type,
       depth,
-      update_in_place);
+      update_in_place,
+      location);
   }
   else if(type.id()==ID_struct)
   {
@@ -1176,15 +1193,15 @@ void java_object_factoryt::gen_nondet_init(
       alloc_type,
       struct_type,
       depth,
-      update_in_place);
+      update_in_place,
+      location);
   }
   else
   {
     // types different from pointer or structure:
     // bool, int, float, byte, char, ...
-    exprt rhs=type.id()==ID_c_bool?
-      get_nondet_bool(type):
-      side_effect_expr_nondett(type);
+    exprt rhs = type.id() == ID_c_bool ? get_nondet_bool(type)
+                                       : side_effect_expr_nondett(type, loc);
     code_assignt assign(expr, rhs);
     assign.add_source_location()=loc;
 
@@ -1209,7 +1226,8 @@ void java_object_factoryt::allocate_nondet_length_array(
   code_blockt &assignments,
   const exprt &lhs,
   const exprt &max_length_expr,
-  const typet &element_type)
+  const typet &element_type,
+  const source_locationt &location)
 {
   symbolt &length_sym = get_fresh_aux_symbol(
     java_int_type(),
@@ -1232,7 +1250,8 @@ void java_object_factoryt::allocate_nondet_length_array(
     false,                   // override
     typet(),                 // override type is immaterial
     0,                       // depth is immaterial, always non-null
-    update_in_placet::NO_UPDATE_IN_PLACE);
+    update_in_placet::NO_UPDATE_IN_PLACE,
+    location);
 
   // Insert assumptions to bound its length:
   binary_relation_exprt
@@ -1244,7 +1263,7 @@ void java_object_factoryt::allocate_nondet_length_array(
   assignments.move_to_operands(assume_inst1);
   assignments.move_to_operands(assume_inst2);
 
-  side_effect_exprt java_new_array(ID_java_new_array, lhs.type());
+  side_effect_exprt java_new_array(ID_java_new_array, lhs.type(), loc);
   java_new_array.copy_to_operands(length_sym_expr);
   java_new_array.set(ID_length_upper_bound, max_length_expr);
   java_new_array.type().subtype().set(ID_element_type, element_type);
@@ -1263,7 +1282,8 @@ void java_object_factoryt::gen_nondet_array_init(
   code_blockt &assignments,
   const exprt &expr,
   size_t depth,
-  update_in_placet update_in_place)
+  update_in_placet update_in_place,
+  const source_locationt &location)
 {
   PRECONDITION(expr.type().id()==ID_pointer);
   PRECONDITION(expr.type().subtype().id()==ID_symbol);
@@ -1282,10 +1302,7 @@ void java_object_factoryt::gen_nondet_array_init(
   if(update_in_place==update_in_placet::NO_UPDATE_IN_PLACE)
   {
     allocate_nondet_length_array(
-      assignments,
-      expr,
-      max_length_expr,
-      element_type);
+      assignments, expr, max_length_expr, element_type, location);
   }
 
   // Otherwise we're updating the array in place, and use the
@@ -1375,15 +1392,16 @@ void java_object_factoryt::gen_nondet_array_init(
   gen_nondet_init(
     assignments,
     arraycellref,
-    false, // is_sub
+    false,      // is_sub
     irep_idt(), // class_identifier
-    false, // skip_classid
+    false,      // skip_classid
     // These are variable in number, so use dynamic allocator:
     allocation_typet::DYNAMIC,
-    true,  // override
+    true, // override
     element_type,
     depth,
-    child_update_in_place);
+    child_update_in_place,
+    location);
 
   exprt java_one=from_integer(1, java_int_type());
   code_assignt incr(counter_expr, plus_exprt(counter_expr, java_one));
@@ -1474,7 +1492,8 @@ exprt object_factory(
     false,   // override
     typet(), // override_type is immaterial
     1,       // initial depth
-    update_in_placet::NO_UPDATE_IN_PLACE);
+    update_in_placet::NO_UPDATE_IN_PLACE,
+    loc);
 
   declare_created_symbols(symbols_created, loc, init_code);
 
@@ -1547,7 +1566,8 @@ void gen_nondet_init(
     false,   // override
     typet(), // override_type is immaterial
     1,       // initial depth
-    update_in_place);
+    update_in_place,
+    loc);
 
   declare_created_symbols(symbols_created, loc, init_code);
 
diff --git a/jbmc/src/java_bytecode/java_static_initializers.cpp b/jbmc/src/java_bytecode/java_static_initializers.cpp
index 74513546f4e..e486b38a9f3 100644
--- a/jbmc/src/java_bytecode/java_static_initializers.cpp
+++ b/jbmc/src/java_bytecode/java_static_initializers.cpp
@@ -788,11 +788,13 @@ codet stub_global_initializer_factoryt::get_stub_initializer_body(
         ? object_factory_parameters.max_nonnull_tree_depth + 1
         : object_factory_parameters.max_nonnull_tree_depth;
 
+    source_locationt location;
+    location.set_function(function_id);
     gen_nondet_init(
       new_global_symbol,
       static_init_body,
       symbol_table,
-      source_locationt(),
+      location,
       false,
       allocation_typet::DYNAMIC,
       parameters,
diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
index 75a6f9483ce..e7c8c8058c7 100644
--- a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
+++ b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
@@ -547,7 +547,7 @@ refined_string_exprt java_string_library_preprocesst::make_nondet_string_expr(
   /// \todo refactor with initialize_nonddet_string_struct
   const refined_string_exprt str = decl_string_expr(loc, symbol_table, code);
 
-  side_effect_expr_nondett nondet_length(str.length().type());
+  const side_effect_expr_nondett nondet_length(str.length().type(), loc);
   code.add(code_assignt(str.length(), nondet_length), loc);
 
   exprt nondet_array_expr =
@@ -667,7 +667,7 @@ exprt make_nondet_infinite_char_array(
     symbol_table);
   const symbol_exprt data_expr = data_sym.symbol_expr();
   code.add(code_declt(data_expr), loc);
-  side_effect_expr_nondett nondet_data(data_expr.type());
+  const side_effect_expr_nondett nondet_data(data_expr.type(), loc);
   code.add(code_assignt(data_expr, nondet_data), loc);
   return data_expr;
 }
diff --git a/jbmc/src/java_bytecode/remove_java_new.cpp b/jbmc/src/java_bytecode/remove_java_new.cpp
index e2b4bfacd5f..26b48b637d9 100644
--- a/jbmc/src/java_bytecode/remove_java_new.cpp
+++ b/jbmc/src/java_bytecode/remove_java_new.cpp
@@ -84,7 +84,7 @@ goto_programt::targett remove_java_newt::lower_java_new(
   CHECK_RETURN(object_size.is_not_nil());
 
   // we produce a malloc side-effect, which stays
-  side_effect_exprt malloc_expr(ID_allocate, rhs.type());
+  side_effect_exprt malloc_expr(ID_allocate, rhs.type(), location);
   malloc_expr.copy_to_operands(object_size);
   // could use true and get rid of the code below
   malloc_expr.copy_to_operands(false_exprt());
@@ -135,7 +135,7 @@ goto_programt::targett remove_java_newt::lower_java_new_array(
   CHECK_RETURN(!object_size.is_nil());
 
   // we produce a malloc side-effect, which stays
-  side_effect_exprt malloc_expr(ID_allocate, rhs.type());
+  side_effect_exprt malloc_expr(ID_allocate, rhs.type(), location);
   malloc_expr.copy_to_operands(object_size);
   // code use true and get rid of the code below
   malloc_expr.copy_to_operands(false_exprt());
@@ -188,7 +188,7 @@ goto_programt::targett remove_java_newt::lower_java_new_array(
     allocate_data_type = data.type();
 
   side_effect_exprt data_java_new_expr(
-    ID_java_new_array_data, allocate_data_type);
+    ID_java_new_array_data, allocate_data_type, location);
 
   // The instruction may specify a (hopefully small) upper bound on the
   // array size, in which case we allocate a fixed-length array that may
@@ -276,7 +276,7 @@ goto_programt::targett remove_java_newt::lower_java_new_array(
     CHECK_RETURN(sub_type.id() == ID_pointer);
     sub_java_new.type() = sub_type;
 
-    side_effect_exprt inc(ID_assign);
+    side_effect_exprt inc(ID_assign, typet(), location);
     inc.operands().resize(2);
     inc.op0() = tmp_i;
     inc.op1() = plus_exprt(tmp_i, from_integer(1, tmp_i.type()));
diff --git a/jbmc/src/java_bytecode/replace_java_nondet.cpp b/jbmc/src/java_bytecode/replace_java_nondet.cpp
index 1ad46ecebd8..1ac75ce78c4 100644
--- a/jbmc/src/java_bytecode/replace_java_nondet.cpp
+++ b/jbmc/src/java_bytecode/replace_java_nondet.cpp
@@ -279,7 +279,8 @@ static goto_programt::targett check_and_replace_target(
     const auto &nondet_var =
       to_code_return(target_instruction->code).return_value();
 
-    side_effect_expr_nondett inserted_expr(nondet_var.type());
+    side_effect_expr_nondett inserted_expr(
+      nondet_var.type(), target_instruction->source_location);
     inserted_expr.set_nullable(
       instr_info.get_nullable_type() ==
       nondet_instruction_infot::is_nullablet::TRUE);
@@ -292,7 +293,8 @@ static goto_programt::targett check_and_replace_target(
     // Assume that the LHS of *this* assignment is the actual nondet variable
     const auto &nondet_var = to_code_assign(target_instruction->code).lhs();
 
-    side_effect_expr_nondett inserted_expr(nondet_var.type());
+    side_effect_expr_nondett inserted_expr(
+      nondet_var.type(), target_instruction->source_location);
     inserted_expr.set_nullable(
       instr_info.get_nullable_type() ==
       nondet_instruction_infot::is_nullablet::TRUE);
diff --git a/src/analyses/flow_insensitive_analysis.cpp b/src/analyses/flow_insensitive_analysis.cpp
index b9fe025a203..a91186a84c3 100644
--- a/src/analyses/flow_insensitive_analysis.cpp
+++ b/src/analyses/flow_insensitive_analysis.cpp
@@ -210,7 +210,8 @@ bool flow_insensitive_analysis_baset::do_function_call(
 
     goto_programt temp;
 
-    exprt rhs=side_effect_expr_nondett(code.lhs().type());
+    exprt rhs =
+      side_effect_expr_nondett(code.lhs().type(), l_call->source_location);
 
     goto_programt::targett r=temp.add_instruction();
     r->make_return();
diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp
index 8c039f23c0a..2933f680e8e 100644
--- a/src/analyses/goto_check.cpp
+++ b/src/analyses/goto_check.cpp
@@ -1703,7 +1703,7 @@ void goto_checkt::goto_check(
           if(!base_type_eq(lhs.type(), address_of_expr.type(), ns))
             address_of_expr.make_typecast(lhs.type());
           const if_exprt rhs(
-            side_effect_expr_nondett(bool_typet()),
+            side_effect_expr_nondett(bool_typet(), i.source_location),
             address_of_expr,
             lhs,
             lhs.type());
diff --git a/src/ansi-c/c_nondet_symbol_factory.cpp b/src/ansi-c/c_nondet_symbol_factory.cpp
index 8200e70a84e..9b5ca5d4f77 100644
--- a/src/ansi-c/c_nondet_symbol_factory.cpp
+++ b/src/ansi-c/c_nondet_symbol_factory.cpp
@@ -43,11 +43,12 @@ static const symbolt &c_new_tmp_symbol(
 }
 
 /// \param type: Desired type (C_bool or plain bool)
+/// \param loc: source location
 /// \return nondet expr of that type
-static exprt c_get_nondet_bool(const typet &type)
+static exprt c_get_nondet_bool(const typet &type, const source_locationt &loc)
 {
   // We force this to 0 and 1 and won't consider other values
-  return typecast_exprt(side_effect_expr_nondett(bool_typet()), type);
+  return typecast_exprt(side_effect_expr_nondett(bool_typet(), loc), type);
 }
 
 class symbol_factoryt
@@ -173,7 +174,7 @@ void symbol_factoryt::gen_nondet_init(
       set_null_inst.add_source_location()=loc;
 
       code_ifthenelset null_check;
-      null_check.cond()=side_effect_expr_nondett(bool_typet());
+      null_check.cond() = side_effect_expr_nondett(bool_typet(), loc);
       null_check.then_case()=set_null_inst;
       null_check.else_case()=non_null_inst;
 
@@ -187,9 +188,8 @@ void symbol_factoryt::gen_nondet_init(
     //   <expr> = NONDET(_BOOL);
     // Else add the following code to assignments:
     //   <expr> = NONDET(type);
-    exprt rhs=type.id()==ID_c_bool?
-      c_get_nondet_bool(type):
-      side_effect_expr_nondett(type);
+    exprt rhs = type.id() == ID_c_bool ? c_get_nondet_bool(type, loc)
+                                       : side_effect_expr_nondett(type, loc);
     code_assignt assign(expr, rhs);
     assign.add_source_location()=loc;
 
diff --git a/src/ansi-c/c_typecheck_code.cpp b/src/ansi-c/c_typecheck_code.cpp
index b2117cebc1f..be2d711416d 100644
--- a/src/ansi-c/c_typecheck_code.cpp
+++ b/src/ansi-c/c_typecheck_code.cpp
@@ -675,7 +675,8 @@ void c_typecheck_baset::typecheck_return(codet &code)
       warning().source_location = code.source_location();
       warning() << "non-void function should return a value" << eom;
 
-      code.copy_to_operands(side_effect_expr_nondett(return_type));
+      code.copy_to_operands(
+        side_effect_expr_nondett(return_type, code.source_location()));
     }
   }
   else if(code.operands().size()==1)
diff --git a/src/ansi-c/c_typecheck_expr.cpp b/src/ansi-c/c_typecheck_expr.cpp
index 24567080b52..b8b0e7fe595 100644
--- a/src/ansi-c/c_typecheck_expr.cpp
+++ b/src/ansi-c/c_typecheck_expr.cpp
@@ -466,9 +466,7 @@ void c_typecheck_baset::typecheck_expr_builtin_va_arg(exprt &expr)
 
   // turn into function call
   side_effect_expr_function_callt result(
-    function, {arg}, new_type.return_type());
-
-  result.add_source_location()=expr.source_location();
+    function, {arg}, new_type.return_type(), expr.source_location());
 
   expr.swap(result);
 
@@ -884,8 +882,7 @@ void c_typecheck_baset::typecheck_side_effect_statement_expression(
       static_cast<const typet &>(fc.function().type().find(ID_return_type));
 
     side_effect_expr_function_callt sideeffect(
-      fc.function(), fc.arguments(), return_type);
-    sideeffect.add_source_location()=fc.source_location();
+      fc.function(), fc.arguments(), return_type, fc.source_location());
 
     expr.type()=sideeffect.type();
 
@@ -897,8 +894,8 @@ void c_typecheck_baset::typecheck_side_effect_statement_expression(
     }
     else
     {
-      side_effect_exprt assign(ID_assign, sideeffect.type());
-      assign.add_source_location()=fc.source_location();
+      side_effect_exprt assign(
+        ID_assign, sideeffect.type(), fc.source_location());
       assign.move_to_operands(fc.lhs(), sideeffect);
 
       code_expressiont code_expr(assign);
@@ -965,7 +962,8 @@ void c_typecheck_baset::typecheck_expr_sizeof(exprt &expr)
   // The type may contain side-effects.
   if(!clean_code.empty())
   {
-    side_effect_exprt side_effect_expr(ID_statement_expression, void_type());
+    side_effect_exprt side_effect_expr(
+      ID_statement_expression, void_type(), expr.source_location());
     code_blockt decl_block(clean_code);
     decl_block.set_statement(ID_decl_block);
     side_effect_expr.copy_to_operands(decl_block);
@@ -1021,7 +1019,8 @@ void c_typecheck_baset::typecheck_expr_typecast(exprt &expr)
   // The type may contain side-effects.
   if(!clean_code.empty())
   {
-    side_effect_exprt side_effect_expr(ID_statement_expression, void_type());
+    side_effect_exprt side_effect_expr(
+      ID_statement_expression, void_type(), expr.source_location());
     code_blockt decl_block(clean_code);
     decl_block.set_statement(ID_decl_block);
     side_effect_expr.copy_to_operands(decl_block);
@@ -2327,8 +2326,7 @@ exprt c_typecheck_baset::do_special_functions(
       throw 0;
     }
 
-    side_effect_exprt malloc_expr(ID_allocate, expr.type());
-    malloc_expr.add_source_location()=source_location;
+    side_effect_exprt malloc_expr(ID_allocate, expr.type(), source_location);
     malloc_expr.operands()=expr.arguments();
 
     return malloc_expr;
diff --git a/src/cpp/cpp_constructor.cpp b/src/cpp/cpp_constructor.cpp
index dd69741ff12..ea1670035a9 100644
--- a/src/cpp/cpp_constructor.cpp
+++ b/src/cpp/cpp_constructor.cpp
@@ -160,8 +160,7 @@ codet cpp_typecheckt::cpp_constructor(
       // Override constantness
       object_tc.type().set(ID_C_constant, false);
       object_tc.set(ID_C_lvalue, true);
-      side_effect_exprt assign(ID_assign);
-      assign.add_source_location()=source_location;
+      side_effect_exprt assign(ID_assign, typet(), source_location);
       assign.copy_to_operands(object_tc, operands_tc.front());
       typecheck_side_effect_assignment(assign);
       new_code.expression()=assign;
@@ -213,8 +212,7 @@ codet cpp_typecheckt::cpp_constructor(
       if(!component.get_bool("from_base"))
         val=true_exprt();
 
-      side_effect_exprt assign(ID_assign);
-      assign.add_source_location()=source_location;
+      side_effect_exprt assign(ID_assign, typet(), source_location);
       assign.move_to_operands(member, val);
       typecheck_side_effect_assignment(assign);
       code_expressiont code_exp(assign);
diff --git a/src/cpp/cpp_typecheck_code.cpp b/src/cpp/cpp_typecheck_code.cpp
index 634e4c76b97..924c189b80f 100644
--- a/src/cpp/cpp_typecheck_code.cpp
+++ b/src/cpp/cpp_typecheck_code.cpp
@@ -316,8 +316,7 @@ void cpp_typecheckt::typecheck_member_initializer(codet &code)
         symbol_expr.set(ID_C_lvalue, true);
         code.op0().type().remove(ID_C_reference);
 
-        side_effect_exprt assign(ID_assign);
-        assign.add_source_location() = code.source_location();
+        side_effect_exprt assign(ID_assign, typet(), code.source_location());
         assign.copy_to_operands(symbol_expr, code.op0());
         typecheck_side_effect_assignment(assign);
         code_expressiont new_code(assign);
diff --git a/src/cpp/cpp_typecheck_conversions.cpp b/src/cpp/cpp_typecheck_conversions.cpp
index 3ae9219fde7..f7f0dbcbfa5 100644
--- a/src/cpp/cpp_typecheck_conversions.cpp
+++ b/src/cpp/cpp_typecheck_conversions.cpp
@@ -893,8 +893,8 @@ bool cpp_typecheckt::user_defined_conversion_sequence(
           const dereference_exprt deref(address);
 
           // create temporary object
-          side_effect_exprt tmp_object_expr(ID_temporary_object, type);
-          tmp_object_expr.add_source_location()=expr.source_location();
+          side_effect_exprt tmp_object_expr(
+            ID_temporary_object, type, expr.source_location());
           tmp_object_expr.copy_to_operands(deref);
           tmp_object_expr.set(ID_C_lvalue, true);
 
diff --git a/src/cpp/cpp_typecheck_expr.cpp b/src/cpp/cpp_typecheck_expr.cpp
index 33378fb3429..2ffd3524407 100644
--- a/src/cpp/cpp_typecheck_expr.cpp
+++ b/src/cpp/cpp_typecheck_expr.cpp
@@ -1969,10 +1969,10 @@ void cpp_typecheckt::typecheck_side_effect_function_call(
     if(expr.arguments().empty())
     {
       // create temporary object
-      side_effect_exprt tmp_object_expr(ID_temporary_object, pod);
+      side_effect_exprt tmp_object_expr(
+        ID_temporary_object, pod, expr.source_location());
       tmp_object_expr.set(ID_C_lvalue, true);
       tmp_object_expr.set(ID_mode, ID_cpp);
-      tmp_object_expr.add_source_location()=expr.source_location();
       expr.swap(tmp_object_expr);
     }
     else if(expr.arguments().size()==1)
@@ -2171,10 +2171,10 @@ void cpp_typecheckt::typecheck_side_effect_function_call(
     expr.type()=this_type.subtype();
 
     // create temporary object
-    side_effect_exprt tmp_object_expr(ID_temporary_object, this_type.subtype());
+    side_effect_exprt tmp_object_expr(
+      ID_temporary_object, this_type.subtype(), expr.source_location());
     tmp_object_expr.set(ID_C_lvalue, true);
     tmp_object_expr.set(ID_mode, ID_cpp);
-    tmp_object_expr.add_source_location()=expr.source_location();
 
     exprt member;
 
diff --git a/src/cpp/parse.cpp b/src/cpp/parse.cpp
index dabfebb85b7..eeb021684fa 100644
--- a/src/cpp/parse.cpp
+++ b/src/cpp/parse.cpp
@@ -5807,7 +5807,7 @@ bool Parser::rThrowExpr(exprt &exp)
 
   int t=lex.LookAhead(0);
 
-  exp=side_effect_expr_throwt();
+  exp = side_effect_expr_throwt(irept(), typet(), source_locationt());
   set_location(exp, tk);
 
   if(t==':' || t==';')
@@ -6399,7 +6399,7 @@ bool Parser::rPostfixExpr(exprt &exp)
       lex.get_token(op);
 
       {
-        side_effect_exprt tmp(ID_postincrement);
+        side_effect_exprt tmp(ID_postincrement, typet(), source_locationt());
         tmp.move_to_operands(exp);
         set_location(tmp, op);
         exp.swap(tmp);
@@ -6410,7 +6410,7 @@ bool Parser::rPostfixExpr(exprt &exp)
       lex.get_token(op);
 
       {
-        side_effect_exprt tmp(ID_postdecrement);
+        side_effect_exprt tmp(ID_postdecrement, typet(), source_locationt());
         tmp.move_to_operands(exp);
         set_location(tmp, op);
         exp.swap(tmp);
diff --git a/src/goto-instrument/accelerate/accelerate.cpp b/src/goto-instrument/accelerate/accelerate.cpp
index 50cff3f5b35..639abfefd58 100644
--- a/src/goto-instrument/accelerate/accelerate.cpp
+++ b/src/goto-instrument/accelerate/accelerate.cpp
@@ -212,7 +212,9 @@ void acceleratet::insert_looping_path(
   ++loop_body;
 
   goto_programt::targett jump=program.insert_before(loop_body);
-  jump->make_goto(loop_body, side_effect_expr_nondett(bool_typet()));
+  jump->make_goto(
+    loop_body,
+    side_effect_expr_nondett(bool_typet(), loop_body->source_location));
 
   program.destructive_insert(loop_body, looping_path);
 
diff --git a/src/goto-instrument/accelerate/acceleration_utils.cpp b/src/goto-instrument/accelerate/acceleration_utils.cpp
index fde3406be70..a04c5ef1a22 100644
--- a/src/goto-instrument/accelerate/acceleration_utils.cpp
+++ b/src/goto-instrument/accelerate/acceleration_utils.cpp
@@ -338,7 +338,7 @@ void acceleration_utilst::push_nondet(exprt &expr)
   if(expr.id()==ID_not &&
      expr.op0().id()==ID_nondet)
   {
-    expr=side_effect_expr_nondett(expr.type());
+    expr = side_effect_expr_nondett(expr.type(), expr.source_location());
   }
   else if(expr.id()==ID_equal ||
           expr.id()==ID_lt ||
@@ -349,7 +349,7 @@ void acceleration_utilst::push_nondet(exprt &expr)
     if(expr.op0().id()==ID_nondet ||
        expr.op1().id()==ID_nondet)
     {
-      expr=side_effect_expr_nondett(expr.type());
+      expr = side_effect_expr_nondett(expr.type(), expr.source_location());
     }
   }
 }
@@ -412,7 +412,9 @@ bool acceleration_utilst::do_assumptions(
 
   program.assume(not_exprt(condition));
 
-  program.assign(loop_counter, side_effect_expr_nondett(loop_counter.type()));
+  program.assign(
+    loop_counter,
+    side_effect_expr_nondett(loop_counter.type(), source_locationt()));
 
   for(std::map<exprt, polynomialt>::iterator p_it=polynomials.begin();
       p_it!=polynomials.end();
@@ -597,7 +599,8 @@ bool acceleration_utilst::do_arrays(
       it!=arrays_written.end();
       ++it)
   {
-    program.assign(*it, side_effect_expr_nondett(it->type()));
+    program.assign(
+      *it, side_effect_expr_nondett(it->type(), source_locationt()));
   }
 
   // Now add in all the effects of this loop on the arrays.
@@ -1051,7 +1054,8 @@ bool acceleration_utilst::assign_array(
     fresh_symbol("polynomial::array", arr.type()).symbol_expr();
 
   // First make the fresh nondet array.
-  program.assign(fresh_array, side_effect_expr_nondett(arr.type()));
+  program.assign(
+    fresh_array, side_effect_expr_nondett(arr.type(), lhs.source_location()));
 
   // Then assume that the fresh array has the appropriate values at the indices
   // the loop updated.
diff --git a/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp b/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp
index cd68b658489..3d5927264b1 100644
--- a/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp
+++ b/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp
@@ -302,7 +302,9 @@ bool disjunctive_polynomial_accelerationt::accelerate(
   // assume(no overflows in previous code);
 
   program.add_instruction(ASSUME)->guard=pre_guard;
-  program.assign(loop_counter, side_effect_expr_nondett(loop_counter.type()));
+  program.assign(
+    loop_counter,
+    side_effect_expr_nondett(loop_counter.type(), source_locationt()));
 
   for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
       it!=polynomials.end();
diff --git a/src/goto-instrument/accelerate/polynomial_accelerator.cpp b/src/goto-instrument/accelerate/polynomial_accelerator.cpp
index 5b4bd8fd44c..9c5a9d95f98 100644
--- a/src/goto-instrument/accelerate/polynomial_accelerator.cpp
+++ b/src/goto-instrument/accelerate/polynomial_accelerator.cpp
@@ -237,7 +237,10 @@ bool polynomial_acceleratort::accelerate(
 
   program.add_instruction(ASSUME)->guard=guard;
 
-  program.assign(loop_counter, side_effect_expr_nondett(loop_counter.type()));
+  program.assign(
+    loop_counter,
+    side_effect_expr_nondett(
+      loop_counter.type(), loop_counter.source_location()));
 
   for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
       it!=polynomials.end();
diff --git a/src/goto-instrument/code_contracts.cpp b/src/goto-instrument/code_contracts.cpp
index 98d0d1248eb..7a8412afcce 100644
--- a/src/goto-instrument/code_contracts.cpp
+++ b/src/goto-instrument/code_contracts.cpp
@@ -131,10 +131,10 @@ static void check_apply_invariants(
   if(!loop_head->is_goto())
   {
     goto_programt::targett jump=havoc_code.add_instruction(GOTO);
-    jump->guard=side_effect_expr_nondett(bool_typet());
+    jump->guard =
+      side_effect_expr_nondett(bool_typet(), loop_head->source_location);
     jump->targets.push_back(loop_end);
     jump->function=loop_head->function;
-    jump->source_location=loop_head->source_location;
   }
 
   // Now havoc at the loop head. Use insert_swap to
@@ -295,7 +295,8 @@ void code_contractst::add_contract_check(
 
   // if(nondet)
   goto_programt::targett g=check.add_instruction();
-  g->make_goto(skip, side_effect_expr_nondett(bool_typet()));
+  g->make_goto(
+    skip, side_effect_expr_nondett(bool_typet(), skip->source_location));
   g->function=skip->function;
   g->source_location=skip->source_location;
 
diff --git a/src/goto-instrument/havoc_loops.cpp b/src/goto-instrument/havoc_loops.cpp
index 01bc2701dd8..74bc41e0681 100644
--- a/src/goto-instrument/havoc_loops.cpp
+++ b/src/goto-instrument/havoc_loops.cpp
@@ -92,7 +92,8 @@ void havoc_loopst::build_havoc_code(
       m_it++)
   {
     exprt lhs=*m_it;
-    exprt rhs=side_effect_expr_nondett(lhs.type());
+    exprt rhs =
+      side_effect_expr_nondett(lhs.type(), loop_head->source_location);
 
     goto_programt::targett t=dest.add_instruction(ASSIGN);
     t->function=loop_head->function;
diff --git a/src/goto-instrument/interrupt.cpp b/src/goto-instrument/interrupt.cpp
index 4d3416a3b38..38863e490fc 100644
--- a/src/goto-instrument/interrupt.cpp
+++ b/src/goto-instrument/interrupt.cpp
@@ -104,7 +104,7 @@ void interrupt(
 
       t_goto->make_goto(t_orig);
       t_goto->source_location=source_location;
-      t_goto->guard=side_effect_expr_nondett(bool_typet());
+      t_goto->guard = side_effect_expr_nondett(bool_typet(), source_location);
       t_goto->function=original_instruction.function;
 
       t_call->make_function_call(isr_call);
@@ -133,7 +133,7 @@ void interrupt(
 
       t_goto->make_goto(t_orig);
       t_goto->source_location=source_location;
-      t_goto->guard=side_effect_expr_nondett(bool_typet());
+      t_goto->guard = side_effect_expr_nondett(bool_typet(), source_location);
       t_goto->function=i_it->function;
 
       t_call->make_function_call(isr_call);
diff --git a/src/goto-instrument/loop_utils.cpp b/src/goto-instrument/loop_utils.cpp
index ee02a3b1695..4ab59238bc9 100644
--- a/src/goto-instrument/loop_utils.cpp
+++ b/src/goto-instrument/loop_utils.cpp
@@ -45,7 +45,8 @@ void build_havoc_code(
       m_it++)
   {
     exprt lhs=*m_it;
-    exprt rhs=side_effect_expr_nondett(lhs.type());
+    exprt rhs =
+      side_effect_expr_nondett(lhs.type(), loop_head->source_location);
 
     goto_programt::targett t=dest.add_instruction(ASSIGN);
     t->function=loop_head->function;
diff --git a/src/goto-instrument/nondet_static.cpp b/src/goto-instrument/nondet_static.cpp
index cfa058baad7..bd48a721e9b 100644
--- a/src/goto-instrument/nondet_static.cpp
+++ b/src/goto-instrument/nondet_static.cpp
@@ -60,7 +60,10 @@ void nondet_static(
 
       const goto_programt::instructiont original_instruction = instruction;
       i_it->make_assignment();
-      i_it->code=code_assignt(sym, side_effect_expr_nondett(sym.type()));
+      i_it->code = code_assignt(
+        sym,
+        side_effect_expr_nondett(
+          sym.type(), original_instruction.source_location));
       i_it->source_location = original_instruction.source_location;
       i_it->function = original_instruction.function;
     }
diff --git a/src/goto-instrument/nondet_volatile.cpp b/src/goto-instrument/nondet_volatile.cpp
index 1e9024e48d0..142f4b7e7f9 100644
--- a/src/goto-instrument/nondet_volatile.cpp
+++ b/src/goto-instrument/nondet_volatile.cpp
@@ -48,7 +48,7 @@ void nondet_volatile_rhs(const symbol_tablet &symbol_table, exprt &expr)
       t.remove(ID_C_volatile);
 
       // replace by nondet
-      side_effect_expr_nondett nondet_expr(t);
+      side_effect_expr_nondett nondet_expr(t, expr.source_location());
       expr.swap(nondet_expr);
     }
   }
diff --git a/src/goto-instrument/wmm/shared_buffers.cpp b/src/goto-instrument/wmm/shared_buffers.cpp
index ed410dfb0b8..2f0ab8d23cf 100644
--- a/src/goto-instrument/wmm/shared_buffers.cpp
+++ b/src/goto-instrument/wmm/shared_buffers.cpp
@@ -464,7 +464,8 @@ void shared_bufferst::nondet_flush(
 
   const symbol_exprt choice0_expr=symbol_exprt(choice0, bool_typet());
   const symbol_exprt delay_expr=symbol_exprt(choice2, bool_typet());
-  const exprt nondet_bool_expr=side_effect_expr_nondett(bool_typet());
+  const exprt nondet_bool_expr =
+    side_effect_expr_nondett(bool_typet(), source_location);
 
   // throw Boolean dice
   assignment(goto_program, target, source_location, choice0, nondet_bool_expr);
@@ -1184,8 +1185,8 @@ void shared_bufferst::cfg_visitort::weak_memory(
                     instruction.function, "1");
                   const symbol_exprt choice1_expr=symbol_exprt(choice1,
                     bool_typet());
-                  const exprt nondet_bool_expr=side_effect_expr_nondett(
-                    bool_typet());
+                  const exprt nondet_bool_expr =
+                    side_effect_expr_nondett(bool_typet(), source_location);
 
                   // throw Boolean dice
                   shared_buffers.assignment(
diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp
index cbe45869e06..41c03b22831 100644
--- a/src/goto-programs/builtin_functions.cpp
+++ b/src/goto-programs/builtin_functions.cpp
@@ -50,8 +50,8 @@ void goto_convertt::do_prob_uniform(
     throw 0;
   }
 
-  side_effect_exprt rhs("prob_uniform", lhs.type());
-  rhs.add_source_location()=function.source_location();
+  auto rhs =
+    side_effect_exprt("prob_uniform", lhs.type(), function.source_location());
 
   if(lhs.type().id()!=ID_unsignedbv &&
      lhs.type().id()!=ID_signedbv)
@@ -128,8 +128,7 @@ void goto_convertt::do_prob_coin(
     throw 0;
   }
 
-  side_effect_exprt rhs("prob_coin", lhs.type());
-  rhs.add_source_location()=function.source_location();
+  side_effect_exprt rhs("prob_coin", lhs.type(), function.source_location());
 
   if(lhs.type()!=bool_typet())
   {
@@ -194,7 +193,8 @@ void goto_convertt::do_printf(
   {
     typet return_type=
       static_cast<const typet &>(function.type().find(ID_return_type));
-    side_effect_exprt printf_code(ID_printf, return_type);
+    side_effect_exprt printf_code(
+      ID_printf, return_type, function.source_location());
 
     printf_code.operands()=arguments;
     printf_code.add_source_location()=function.source_location();
@@ -284,7 +284,8 @@ void goto_convertt::do_scanf(
               #else
               const index_exprt lhs(
                 dereference_exprt(ptr, type), from_integer(0, index_type()));
-              const side_effect_expr_nondett rhs(type.subtype());
+              const side_effect_expr_nondett rhs(
+                type.subtype(), function.source_location());
               code_assignt assign(lhs, rhs);
               assign.add_source_location()=function.source_location();
               copy(assign, ASSIGN, dest);
@@ -294,7 +295,8 @@ void goto_convertt::do_scanf(
             {
               // make it nondet for now
               const dereference_exprt lhs(ptr, type);
-              const side_effect_expr_nondett rhs(type);
+              const side_effect_expr_nondett rhs(
+                type, function.source_location());
               code_assignt assign(lhs, rhs);
               assign.add_source_location()=function.source_location();
               copy(assign, ASSIGN, dest);
@@ -897,15 +899,13 @@ void goto_convertt::do_function_call_symbol(
     // can only be 0 or 1.
     if(lhs.type().id()==ID_c_bool)
     {
-      rhs=side_effect_expr_nondett(bool_typet());
-      rhs.add_source_location()=function.source_location();
+      rhs = side_effect_expr_nondett(bool_typet(), function.source_location());
       rhs.set(ID_C_identifier, identifier);
       rhs=typecast_exprt(rhs, lhs.type());
     }
     else
     {
-      rhs=side_effect_expr_nondett(lhs.type());
-      rhs.add_source_location()=function.source_location();
+      rhs = side_effect_expr_nondett(lhs.type(), function.source_location());
       rhs.set(ID_C_identifier, identifier);
     }
 
@@ -1117,7 +1117,10 @@ void goto_convertt::do_function_call_symbol(
     exprt list_arg=make_va_list(arguments[0]);
 
     {
-      side_effect_exprt rhs(ID_gcc_builtin_va_arg_next, list_arg.type());
+      side_effect_exprt rhs(
+        ID_gcc_builtin_va_arg_next,
+        list_arg.type(),
+        function.source_location());
       rhs.copy_to_operands(list_arg);
       rhs.set(ID_C_va_arg_type, to_code_type(function.type()).return_type());
       goto_programt::targett t1=dest.add_instruction(ASSIGN);
diff --git a/src/goto-programs/generate_function_bodies.cpp b/src/goto-programs/generate_function_bodies.cpp
index d6cf18d5987..5e10607f651 100644
--- a/src/goto-programs/generate_function_bodies.cpp
+++ b/src/goto-programs/generate_function_bodies.cpp
@@ -245,7 +245,8 @@ class havoc_generate_function_bodiest : public generate_function_bodiest,
       {
         auto assign_instruction = add_instruction();
         assign_instruction->make_assignment(
-          code_assignt(lhs, side_effect_expr_nondett(lhs_type)));
+          code_assignt(
+            lhs, side_effect_expr_nondett(lhs_type, lhs.source_location())));
       }
     }
   }
@@ -304,8 +305,9 @@ class havoc_generate_function_bodiest : public generate_function_bodiest,
     {
       auto return_instruction = add_instruction();
       return_instruction->make_return();
-      return_instruction->code =
-        code_returnt(side_effect_expr_nondett(function.type.return_type()));
+      return_instruction->code = code_returnt(
+        side_effect_expr_nondett(
+          function.type.return_type(), function_symbol.location));
     }
     auto end_function_instruction = add_instruction();
     end_function_instruction->make_end_function();
diff --git a/src/goto-programs/goto_convert_functions.cpp b/src/goto-programs/goto_convert_functions.cpp
index 91df5cb4447..6701ae12f5e 100644
--- a/src/goto-programs/goto_convert_functions.cpp
+++ b/src/goto-programs/goto_convert_functions.cpp
@@ -128,7 +128,7 @@ void goto_convert_functionst::add_return(
 
   #endif
 
-  side_effect_expr_nondett rhs(f.type.return_type());
+  const side_effect_expr_nondett rhs(f.type.return_type(), source_location);
 
   goto_programt::targett t=f.body.add_instruction();
   t->make_return();
diff --git a/src/goto-programs/goto_convert_side_effect.cpp b/src/goto-programs/goto_convert_side_effect.cpp
index 2aeab13da62..642290834ce 100644
--- a/src/goto-programs/goto_convert_side_effect.cpp
+++ b/src/goto-programs/goto_convert_side_effect.cpp
@@ -676,8 +676,9 @@ void goto_convertt::remove_side_effect(
   else if(statement==ID_throw)
   {
     goto_programt::targett t=dest.add_instruction(THROW);
-    t->code=
-      code_expressiont(side_effect_expr_throwt(expr.find(ID_exception_list)));
+    t->code = code_expressiont(
+      side_effect_expr_throwt(
+        expr.find(ID_exception_list), expr.type(), expr.source_location()));
     t->code.op0().operands().swap(expr.operands());
     t->code.add_source_location()=expr.source_location();
     t->source_location=expr.source_location();
diff --git a/src/goto-programs/goto_inline_class.cpp b/src/goto-programs/goto_inline_class.cpp
index 97b486caa63..253aaa51268 100644
--- a/src/goto-programs/goto_inline_class.cpp
+++ b/src/goto-programs/goto_inline_class.cpp
@@ -85,7 +85,7 @@ void goto_inlinet::parameter_assignments(
                 << "not enough arguments, "
                 << "inserting non-deterministic value" << eom;
 
-      actual=side_effect_expr_nondett(par_type);
+      actual = side_effect_expr_nondett(par_type, source_location);
     }
     else
       actual=*it1;
diff --git a/src/goto-programs/interpreter.cpp b/src/goto-programs/interpreter.cpp
index 99cb239156f..4ec0c2ac729 100644
--- a/src/goto-programs/interpreter.cpp
+++ b/src/goto-programs/interpreter.cpp
@@ -514,7 +514,7 @@ exprt interpretert::get_value(
   if(use_non_det &&
      memory[integer2ulong(offset)].initialized!=
      memory_cellt::initializedt::WRITTEN_BEFORE_READ)
-    return side_effect_expr_nondett(type);
+    return side_effect_expr_nondett(type, source_locationt());
   mp_vectort rhs;
   rhs.push_back(memory[integer2ulong(offset)].value);
   return get_value(type, rhs);
diff --git a/src/goto-programs/remove_calls_no_body.cpp b/src/goto-programs/remove_calls_no_body.cpp
index 62121dcfe17..2d9f716e593 100644
--- a/src/goto-programs/remove_calls_no_body.cpp
+++ b/src/goto-programs/remove_calls_no_body.cpp
@@ -44,8 +44,7 @@ void remove_calls_no_bodyt::remove_call_no_body(
   // return value
   if(lhs.is_not_nil())
   {
-    side_effect_expr_nondett rhs(lhs.type());
-    rhs.add_source_location() = target->source_location;
+    side_effect_expr_nondett rhs(lhs.type(), target->source_location);
 
     code_assignt code(lhs, rhs);
     code.add_source_location() = target->source_location;
diff --git a/src/goto-programs/remove_returns.cpp b/src/goto-programs/remove_returns.cpp
index 5dd5c3445dd..75c862c62f4 100644
--- a/src/goto-programs/remove_returns.cpp
+++ b/src/goto-programs/remove_returns.cpp
@@ -191,7 +191,8 @@ void remove_returnst::do_function_calls(
           if(!is_stub)
             rhs=return_value;
           else
-            rhs=side_effect_expr_nondett(function_call.lhs().type());
+            rhs = side_effect_expr_nondett(
+              function_call.lhs().type(), i_it->source_location);
 
           goto_programt::targett t_a=goto_program.insert_after(i_it);
           t_a->make_assignment();
diff --git a/src/goto-programs/string_abstraction.cpp b/src/goto-programs/string_abstraction.cpp
index dd3ecbfc1ef..3a6dccea30d 100644
--- a/src/goto-programs/string_abstraction.cpp
+++ b/src/goto-programs/string_abstraction.cpp
@@ -906,7 +906,7 @@ exprt string_abstractiont::build_unknown(whatt what, bool write)
 
   case whatt::LENGTH:
   case whatt::SIZE:
-    result=side_effect_expr_nondett(type);
+    result = side_effect_expr_nondett(type, source_locationt());
     break;
   }
 
diff --git a/src/goto-programs/string_instrumentation.cpp b/src/goto-programs/string_instrumentation.cpp
index 677a85f80e5..be5ccacfbbc 100644
--- a/src/goto-programs/string_instrumentation.cpp
+++ b/src/goto-programs/string_instrumentation.cpp
@@ -302,8 +302,8 @@ void string_instrumentationt::do_sprintf(
     goto_programt::targett return_assignment=tmp.add_instruction(ASSIGN);
     return_assignment->source_location=target->source_location;
 
-    exprt rhs=side_effect_expr_nondett(call.lhs().type());
-    rhs.add_source_location()=target->source_location;
+    exprt rhs =
+      side_effect_expr_nondett(call.lhs().type(), target->source_location);
 
     return_assignment->code=code_assignt(call.lhs(), rhs);
   }
@@ -345,8 +345,8 @@ void string_instrumentationt::do_snprintf(
     goto_programt::targett return_assignment=tmp.add_instruction(ASSIGN);
     return_assignment->source_location=target->source_location;
 
-    exprt rhs=side_effect_expr_nondett(call.lhs().type());
-    rhs.add_source_location()=target->source_location;
+    exprt rhs =
+      side_effect_expr_nondett(call.lhs().type(), target->source_location);
 
     return_assignment->code=code_assignt(call.lhs(), rhs);
   }
@@ -378,8 +378,8 @@ void string_instrumentationt::do_fscanf(
     goto_programt::targett return_assignment=tmp.add_instruction(ASSIGN);
     return_assignment->source_location=target->source_location;
 
-    exprt rhs=side_effect_expr_nondett(call.lhs().type());
-    rhs.add_source_location()=target->source_location;
+    exprt rhs =
+      side_effect_expr_nondett(call.lhs().type(), target->source_location);
 
     return_assignment->code=code_assignt(call.lhs(), rhs);
   }
@@ -583,8 +583,7 @@ void string_instrumentationt::do_format_string_write(
 
           const dereference_exprt lhs(argument, arg_type.subtype());
 
-          side_effect_expr_nondett rhs(lhs.type());
-          rhs.add_source_location()=target->source_location;
+          side_effect_expr_nondett rhs(lhs.type(), target->source_location);
 
           assignment->code=code_assignt(lhs, rhs);
 
@@ -627,8 +626,7 @@ void string_instrumentationt::do_format_string_write(
 
         dereference_exprt lhs(arguments[i], arg_type.subtype());
 
-        side_effect_expr_nondett rhs(lhs.type());
-        rhs.add_source_location()=target->source_location;
+        side_effect_expr_nondett rhs(lhs.type(), target->source_location);
 
         assignment->code=code_assignt(lhs, rhs);
       }
@@ -813,7 +811,8 @@ void string_instrumentationt::do_strerror(
 
   {
     goto_programt::targett assignment1=tmp.add_instruction(ASSIGN);
-    exprt nondet_size=side_effect_expr_nondett(size_type());
+    exprt nondet_size =
+      side_effect_expr_nondett(size_type(), it->source_location);
 
     assignment1->code=code_assignt(symbol_size.symbol_expr(), nondet_size);
     assignment1->source_location=it->source_location;
@@ -945,6 +944,7 @@ void string_instrumentationt::invalidate_buffer(
         ID_gt,
         from_integer(limit, unsigned_int_type()));
 
-  const side_effect_expr_nondett nondet(buf_type.subtype());
+  const side_effect_expr_nondett nondet(
+    buf_type.subtype(), target->source_location);
   invalidate->code=code_assignt(deref, nondet);
 }
diff --git a/src/goto-programs/wp.cpp b/src/goto-programs/wp.cpp
index 542e9bd482d..91029d1f987 100644
--- a/src/goto-programs/wp.cpp
+++ b/src/goto-programs/wp.cpp
@@ -230,7 +230,7 @@ exprt wp_decl(
 {
   // Model decl(var) as var = nondet()
   const exprt &var = code.symbol();
-  side_effect_expr_nondett nondet(var.type());
+  side_effect_expr_nondett nondet(var.type(), source_locationt());
   code_assignt assignment(var, nondet);
 
   return wp_assign(assignment, post, ns);
diff --git a/src/goto-symex/auto_objects.cpp b/src/goto-symex/auto_objects.cpp
index f411130474c..3485b8ce3a3 100644
--- a/src/goto-symex/auto_objects.cpp
+++ b/src/goto-symex/auto_objects.cpp
@@ -70,7 +70,7 @@ void goto_symext::initialize_auto_object(
         make_auto_object(type.subtype(), state), pointer_type);
 
       if_exprt rhs(
-        side_effect_expr_nondett(bool_typet()),
+        side_effect_expr_nondett(bool_typet(), expr.source_location()),
         null_pointer_exprt(pointer_type),
         address_of_expr);
 
diff --git a/src/goto-symex/rewrite_union.cpp b/src/goto-symex/rewrite_union.cpp
index 61cd69ee49b..eddbf4bdf6b 100644
--- a/src/goto-symex/rewrite_union.cpp
+++ b/src/goto-symex/rewrite_union.cpp
@@ -100,7 +100,7 @@ void rewrite_union(
   {
     const union_exprt &union_expr=to_union_expr(expr);
     exprt offset=from_integer(0, index_type());
-    side_effect_expr_nondett nondet(expr.type());
+    side_effect_expr_nondett nondet(expr.type(), expr.source_location());
     byte_update_exprt tmp(
       byte_update_id(), nondet, offset, union_expr.op());
     expr=tmp;
diff --git a/src/goto-symex/symex_function_call.cpp b/src/goto-symex/symex_function_call.cpp
index feda391ac99..8e2f0707b86 100644
--- a/src/goto-symex/symex_function_call.cpp
+++ b/src/goto-symex/symex_function_call.cpp
@@ -72,7 +72,8 @@ void goto_symext::parameter_assignments(
                        "not enough arguments, inserting non-deterministic value"
                     << log.eom;
 
-      rhs=side_effect_expr_nondett(parameter_type);
+      rhs = side_effect_expr_nondett(
+        parameter_type, state.source.pc->source_location);
     }
     else
       rhs=*it1;
@@ -265,8 +266,8 @@ void goto_symext::symex_function_call_code(
 
     if(call.lhs().is_not_nil())
     {
-      side_effect_expr_nondett rhs(call.lhs().type());
-      rhs.add_source_location()=call.source_location();
+      const auto rhs =
+        side_effect_expr_nondett(call.lhs().type(), call.source_location());
       code_assignt code(call.lhs(), rhs);
       symex_assign(state, code);
     }
diff --git a/src/goto-symex/symex_other.cpp b/src/goto-symex/symex_other.cpp
index b6f62d2dcd6..9fed77da727 100644
--- a/src/goto-symex/symex_other.cpp
+++ b/src/goto-symex/symex_other.cpp
@@ -34,7 +34,8 @@ void goto_symext::havoc_rec(
 
     code_assignt assignment;
     assignment.lhs()=lhs;
-    assignment.rhs()=side_effect_expr_nondett(dest.type());
+    assignment.rhs() =
+      side_effect_expr_nondett(dest.type(), state.source.pc->source_location);
 
     symex_assign(state, assignment);
   }
diff --git a/src/jsil/jsil_parse_tree.cpp b/src/jsil/jsil_parse_tree.cpp
index 8263b843c98..cd72effc3f7 100644
--- a/src/jsil/jsil_parse_tree.cpp
+++ b/src/jsil/jsil_parse_tree.cpp
@@ -71,7 +71,8 @@ void jsil_declarationt::to_symbol(symbolt &symbol) const
   code_returnt r(symbol_exprt(returns.get(ID_value)));
 
   irept throws(find(ID_throw));
-  side_effect_expr_throwt t(symbol_exprt(throws.get(ID_value)));
+  side_effect_expr_throwt t(
+    symbol_exprt(throws.get(ID_value)), nil_typet(), s.source_location());
   code_expressiont ct(t);
 
   if(insert_at_label(r, returns.get(ID_label), code))
diff --git a/src/util/expr_initializer.cpp b/src/util/expr_initializer.cpp
index e7504dd861d..3d8ec337e32 100644
--- a/src/util/expr_initializer.cpp
+++ b/src/util/expr_initializer.cpp
@@ -69,7 +69,7 @@ exprt expr_initializert<nondet>::expr_initializer_rec(
   {
     exprt result;
     if(nondet)
-      result = side_effect_expr_nondett(type);
+      result = side_effect_expr_nondett(type, source_location);
     else
       result = from_integer(0, type);
 
@@ -81,7 +81,7 @@ exprt expr_initializert<nondet>::expr_initializer_rec(
   {
     exprt result;
     if(nondet)
-      result = side_effect_expr_nondett(type);
+      result = side_effect_expr_nondett(type, source_location);
     else
       result = constant_exprt(ID_0, type);
 
@@ -93,7 +93,7 @@ exprt expr_initializert<nondet>::expr_initializer_rec(
   {
     exprt result;
     if(nondet)
-      result = side_effect_expr_nondett(type);
+      result = side_effect_expr_nondett(type, source_location);
     else
     {
       const std::size_t width = to_bitvector_type(type).get_width();
@@ -109,7 +109,7 @@ exprt expr_initializert<nondet>::expr_initializer_rec(
   {
     exprt result;
     if(nondet)
-      result = side_effect_expr_nondett(type);
+      result = side_effect_expr_nondett(type, source_location);
     else
     {
       exprt sub_zero = expr_initializer_rec(type.subtype(), source_location);
@@ -149,11 +149,7 @@ exprt expr_initializert<nondet>::expr_initializer_rec(
       if(array_type.size().id()==ID_infinity)
       {
         if(nondet)
-        {
-          side_effect_expr_nondett result(type);
-          result.add_source_location() = source_location;
-          return result;
-        }
+          return side_effect_expr_nondett(type, source_location);
 
         array_of_exprt value(tmpval, array_type);
         value.add_source_location()=source_location;
@@ -162,11 +158,7 @@ exprt expr_initializert<nondet>::expr_initializer_rec(
       else if(to_integer(array_type.size(), array_size))
       {
         if(nondet)
-        {
-          side_effect_expr_nondett result(type);
-          result.add_source_location() = source_location;
-          return result;
-        }
+          return side_effect_expr_nondett(type, source_location);
 
         error().source_location=source_location;
         error() << "failed to zero-initialize array of non-fixed size `"
@@ -194,11 +186,7 @@ exprt expr_initializert<nondet>::expr_initializer_rec(
     if(to_integer(vector_type.size(), vector_size))
     {
       if(nondet)
-      {
-        side_effect_expr_nondett result(type);
-        result.add_source_location() = source_location;
-        return result;
-      }
+        return side_effect_expr_nondett(type, source_location);
 
       error().source_location=source_location;
       error() << "failed to zero-initialize vector of non-fixed size `"
@@ -326,7 +314,7 @@ exprt expr_initializert<nondet>::expr_initializer_rec(
   {
     exprt result;
     if(nondet)
-      result = side_effect_expr_nondett(type);
+      result = side_effect_expr_nondett(type, source_location);
     else
       result = constant_exprt(irep_idt(), type);
 
diff --git a/src/util/nondet_bool.h b/src/util/nondet_bool.h
index 700b85ec5b0..7d39b21bd4c 100644
--- a/src/util/nondet_bool.h
+++ b/src/util/nondet_bool.h
@@ -21,7 +21,8 @@ inline exprt get_nondet_bool(const typet &type)
 {
   // We force this to 0 and 1 and won't consider
   // other values.
-  return typecast_exprt(side_effect_expr_nondett(bool_typet()), type);
+  return typecast_exprt(
+    side_effect_expr_nondett(bool_typet(), source_locationt()), type);
 }
 
 #endif // CPROVER_UTIL_NONDET_BOOL_H
diff --git a/src/util/std_code.cpp b/src/util/std_code.cpp
index 1bdd6763ba0..0f399a4a41b 100644
--- a/src/util/std_code.cpp
+++ b/src/util/std_code.cpp
@@ -118,3 +118,34 @@ code_blockt create_fatal_assertion(
   result.add_source_location() = loc;
   return result;
 }
+
+side_effect_exprt::side_effect_exprt(
+  const irep_idt &statement,
+  const typet &_type,
+  const source_locationt &loc)
+  : exprt(ID_side_effect, _type)
+{
+  set_statement(statement);
+  add_source_location() = loc;
+}
+
+side_effect_expr_nondett::side_effect_expr_nondett(
+  const typet &_type,
+  const source_locationt &loc)
+  : side_effect_exprt(ID_nondet, _type, loc)
+{
+  set_nullable(true);
+}
+
+side_effect_expr_function_callt::side_effect_expr_function_callt(
+  const exprt &_function,
+  const exprt::operandst &_arguments,
+  const typet &_type,
+  const source_locationt &loc)
+  : side_effect_exprt(ID_function_call, _type, loc)
+{
+  operands().resize(2);
+  op1().id(ID_arguments);
+  function() = _function;
+  arguments() = _arguments;
+}
diff --git a/src/util/std_code.h b/src/util/std_code.h
index 99640a12423..1e047ff9525 100644
--- a/src/util/std_code.h
+++ b/src/util/std_code.h
@@ -1271,19 +1271,24 @@ inline const code_expressiont &to_code_expression(const codet &code)
 class side_effect_exprt:public exprt
 {
 public:
-  DEPRECATED("Use side_effect_exprt(statement, type) instead")
-  explicit side_effect_exprt(const irep_idt &statement):
-    exprt(ID_side_effect)
+  DEPRECATED("Use side_effect_exprt(statement, type, loc) instead")
+  explicit side_effect_exprt(const irep_idt &statement) : exprt(ID_side_effect)
   {
     set_statement(statement);
   }
 
+  DEPRECATED("Use side_effect_exprt(statement, type, loc) instead")
   side_effect_exprt(const irep_idt &statement, const typet &_type):
     exprt(ID_side_effect, _type)
   {
     set_statement(statement);
   }
 
+  side_effect_exprt(
+    const irep_idt &statement,
+    const typet &_type,
+    const source_locationt &loc);
+
   const irep_idt &get_statement() const
   {
     return get(ID_statement);
@@ -1335,18 +1340,21 @@ inline const side_effect_exprt &to_side_effect_expr(const exprt &expr)
 class side_effect_expr_nondett:public side_effect_exprt
 {
 public:
-  DEPRECATED("Use side_effect_expr_nondett(statement, type) instead")
+  DEPRECATED("Use side_effect_expr_nondett(statement, type, loc) instead")
   side_effect_expr_nondett():side_effect_exprt(ID_nondet)
   {
     set_nullable(true);
   }
 
+  DEPRECATED("Use side_effect_expr_nondett(statement, type, loc) instead")
   explicit side_effect_expr_nondett(const typet &_type):
     side_effect_exprt(ID_nondet, _type)
   {
     set_nullable(true);
   }
 
+  side_effect_expr_nondett(const typet &_type, const source_locationt &loc);
+
   void set_nullable(bool nullable)
   {
     set(ID_is_nondet_nullable, nullable);
@@ -1387,13 +1395,19 @@ inline const side_effect_expr_nondett &to_side_effect_expr_nondet(
 class side_effect_expr_function_callt:public side_effect_exprt
 {
 public:
-  DEPRECATED("Use side_effect_expr_function_callt(...) instead")
-  side_effect_expr_function_callt():side_effect_exprt(ID_function_call)
+  DEPRECATED(
+    "Use side_effect_expr_function_callt("
+    "function, arguments, type, loc) instead")
+  side_effect_expr_function_callt()
+    : side_effect_exprt(ID_function_call, typet(), source_locationt())
   {
     operands().resize(2);
     op1().id(ID_arguments);
   }
 
+  DEPRECATED(
+    "Use side_effect_expr_function_callt("
+    "function, arguments, type, loc) instead")
   side_effect_expr_function_callt(
     const exprt &_function,
     const exprt::operandst &_arguments)
@@ -1405,6 +1419,9 @@ class side_effect_expr_function_callt:public side_effect_exprt
     arguments() = _arguments;
   }
 
+  DEPRECATED(
+    "Use side_effect_expr_function_callt("
+    "function, arguments, type, loc) instead")
   side_effect_expr_function_callt(
     const exprt &_function,
     const exprt::operandst &_arguments,
@@ -1417,6 +1434,12 @@ class side_effect_expr_function_callt:public side_effect_exprt
     arguments() = _arguments;
   }
 
+  side_effect_expr_function_callt(
+    const exprt &_function,
+    const exprt::operandst &_arguments,
+    const typet &_type,
+    const source_locationt &loc);
+
   exprt &function()
   {
     return op0();
@@ -1473,8 +1496,11 @@ class side_effect_expr_throwt:public side_effect_exprt
   {
   }
 
-  explicit side_effect_expr_throwt(const irept &exception_list):
-    side_effect_exprt(ID_throw)
+  explicit side_effect_expr_throwt(
+    const irept &exception_list,
+    const typet &type,
+    const source_locationt &loc)
+    : side_effect_exprt(ID_throw, type, loc)
   {
     set(ID_exception_list, exception_list);
   }