diff --git a/regression/cbmc/double_deref/double_deref_with_pointer_arithmetic.desc b/regression/cbmc/double_deref/double_deref_with_pointer_arithmetic.desc
index df655168340..6b470ed9b09 100644
--- a/regression/cbmc/double_deref/double_deref_with_pointer_arithmetic.desc
+++ b/regression/cbmc/double_deref/double_deref_with_pointer_arithmetic.desc
@@ -1,7 +1,7 @@
 CORE
 double_deref_with_pointer_arithmetic.c
 --show-vcc
-^\{-[0-9]+\} derefd_pointer::derefd_pointer!0#1 = \{ symex_dynamic::dynamic_object1#3\[\[0\]\], symex_dynamic::dynamic_object1#3\[\[1\]\] \}\[cast\(mod #source_location=""\(main::argc!0@1#1, 2\), signedbv\[64\]\)\]
+^\{-[0-9]+\} derefd_pointer::derefd_pointer!0#1 = \{ symex_dynamic::dynamic_object1#3\[\[0\]\], symex_dynamic::dynamic_object1#3\[\[1\]\] \}\[cast\(mod\(main::argc!0@1#1, 2\), signedbv\[64\]\)\]
 ^\{1\} \(derefd_pointer::derefd_pointer!0#1 = address_of\(symex_dynamic::dynamic_object[23]\) \? main::argc!0@1#1 = 2 : \(derefd_pointer::derefd_pointer!0#1 = address_of\(symex_dynamic::dynamic_object[23]\) \? main::argc!0@1#1 = 1 : symex::invalid_object!0#0 = main::argc!0@1#1\)\)
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/src/goto-programs/goto_program.cpp b/src/goto-programs/goto_program.cpp
index 9eb4c45a07e..82277ed4e30 100644
--- a/src/goto-programs/goto_program.cpp
+++ b/src/goto-programs/goto_program.cpp
@@ -121,11 +121,56 @@ std::ostream &goto_programt::output_instruction(
     if(instruction.get_other().id() == ID_code)
     {
       const auto &code = instruction.get_other();
-      if(code.get_statement() == ID_havoc_object)
+      if(code.get_statement() == ID_array_copy)
+      {
+        out << "ARRAY_COPY " << format(code.op0()) << ' ' << format(code.op1())
+            << '\n';
+        break;
+      }
+      else if(code.get_statement() == ID_array_replace)
+      {
+        out << "ARRAY_REPLACE " << format(code.op0()) << ' '
+            << format(code.op1()) << '\n';
+        break;
+      }
+      else if(code.get_statement() == ID_array_set)
+      {
+        out << "ARRAY_SET " << format(code.op0()) << ' ' << format(code.op1())
+            << '\n';
+        break;
+      }
+      else if(code.get_statement() == ID_havoc_object)
       {
         out << "HAVOC_OBJECT " << format(code.op0()) << '\n';
         break;
       }
+      else if(code.get_statement() == ID_fence)
+      {
+        out << "FENCE";
+        if(code.get_bool(ID_WWfence))
+          out << " WW";
+        if(code.get_bool(ID_RRfence))
+          out << " RR";
+        if(code.get_bool(ID_RWfence))
+          out << " RW";
+        if(code.get_bool(ID_WRfence))
+          out << " WR";
+        out << '\n';
+        break;
+      }
+      else if(code.get_statement() == ID_input)
+      {
+        out << "INPUT";
+        for(const auto &op : code.operands())
+          out << ' ' << format(op);
+        out << '\n';
+        break;
+      }
+      else if(code.get_statement() == ID_output)
+      {
+        out << "OUTPUT " << format(code.op0()) << '\n';
+        break;
+      }
       // fallthrough
     }
 
diff --git a/src/util/format_expr.cpp b/src/util/format_expr.cpp
index 085802829c7..b7091fd488c 100644
--- a/src/util/format_expr.cpp
+++ b/src/util/format_expr.cpp
@@ -223,7 +223,7 @@ std::ostream &fallback_format_rec(std::ostream &os, const exprt &expr)
   os << expr.id();
 
   for(const auto &s : expr.get_named_sub())
-    if(s.first != ID_type)
+    if(s.first != ID_type && s.first != ID_C_source_location)
       os << ' ' << s.first << "=\"" << s.second.id() << '"';
 
   if(expr.has_operands())
@@ -571,6 +571,32 @@ void format_expr_configt::setup()
               << format(saturating_plus.rhs()) << ')';
   };
 
+  expr_map[ID_object_address] =
+    [](std::ostream &os, const exprt &expr) -> std::ostream & {
+    const auto &object_address_expr = to_object_address_expr(expr);
+    return os << u8"\u275d" << object_address_expr.object_identifier()
+              << u8"\u275e";
+  };
+
+  expr_map[ID_object_size] =
+    [](std::ostream &os, const exprt &expr) -> std::ostream & {
+    const auto &object_size_expr = to_object_size_expr(expr);
+    return os << "object_size(" << format(object_size_expr.op()) << ')';
+  };
+
+  expr_map[ID_pointer_offset] =
+    [](std::ostream &os, const exprt &expr) -> std::ostream & {
+    const auto &pointer_offset_expr = to_pointer_offset_expr(expr);
+    return os << "pointer_offset(" << format(pointer_offset_expr.op()) << ')';
+  };
+
+  expr_map[ID_field_address] =
+    [](std::ostream &os, const exprt &expr) -> std::ostream & {
+    const auto &field_address_expr = to_field_address_expr(expr);
+    return os << format(field_address_expr.base()) << u8".\u275d"
+              << field_address_expr.component_name() << u8"\u275e";
+  };
+
   fallback = [](std::ostream &os, const exprt &expr) -> std::ostream & {
     return fallback_format_rec(os, expr);
   };
diff --git a/src/util/pointer_expr.h b/src/util/pointer_expr.h
index 7154f07fb45..632a8fbc198 100644
--- a/src/util/pointer_expr.h
+++ b/src/util/pointer_expr.h
@@ -1012,6 +1012,29 @@ class object_size_exprt : public unary_exprt
   }
 };
 
+/// \brief Cast an exprt to a \ref object_size_exprt
+///
+/// \a expr must be known to be \ref object_size_exprt.
+///
+/// \param expr: Source expression
+/// \return Object of type \ref object_size_exprt
+inline const object_size_exprt &to_object_size_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_object_size);
+  const object_size_exprt &ret = static_cast<const object_size_exprt &>(expr);
+  validate_expr(ret);
+  return ret;
+}
+
+/// \copydoc to_object_size_expr(const exprt &)
+inline object_size_exprt &to_object_size_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_object_size);
+  object_size_exprt &ret = static_cast<object_size_exprt &>(expr);
+  validate_expr(ret);
+  return ret;
+}
+
 template <>
 inline bool can_cast_expr<object_size_exprt>(const exprt &base)
 {