diff --git a/src/analyses/variable-sensitivity/full_struct_abstract_object.cpp b/src/analyses/variable-sensitivity/full_struct_abstract_object.cpp
index a512725c6cf..a1279b65b90 100644
--- a/src/analyses/variable-sensitivity/full_struct_abstract_object.cpp
+++ b/src/analyses/variable-sensitivity/full_struct_abstract_object.cpp
@@ -79,7 +79,8 @@ abstract_object_pointert full_struct_abstract_objectt::read_component(
   const namespacet &ns) const
 {
 #ifdef DEBUG
-  std::cout << "Reading component " << member_expr.get_component_name() << '\n';
+  std::cout << "Reading component " << to_member_expr(expr).get_component_name()
+            << '\n';
 #endif
 
   if(is_top())
@@ -115,10 +116,10 @@ abstract_object_pointert full_struct_abstract_objectt::write_component(
   const abstract_object_pointert &value,
   bool merging_write) const
 {
+  const member_exprt member_expr = to_member_expr(expr);
 #ifdef DEBUG
   std::cout << "Writing component " << member_expr.get_component_name() << '\n';
 #endif
-  const member_exprt member_expr = to_member_expr(expr);
 
   if(is_bottom())
   {
diff --git a/src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp b/src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp
index d6bff1f151d..ffdffdf6477 100644
--- a/src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp
+++ b/src/analyses/variable-sensitivity/variable_sensitivity_domain.cpp
@@ -227,8 +227,9 @@ bool variable_sensitivity_domaint::merge(
   trace_ptrt to)
 {
 #ifdef DEBUG
-  std::cout << "Merging from/to:\n " << from->location_number << " --> "
-            << to->location_number << '\n';
+  std::cout << "Merging from/to:\n "
+            << from->current_location()->location_number << " --> "
+            << to->current_location()->location_number << '\n';
 #endif
   auto widen_mode =
     from->should_widen(*to) ? widen_modet::could_widen : widen_modet::no;
diff --git a/src/goto-instrument/accelerate/accelerate.cpp b/src/goto-instrument/accelerate/accelerate.cpp
index 782c0b91edd..0889ce81285 100644
--- a/src/goto-instrument/accelerate/accelerate.cpp
+++ b/src/goto-instrument/accelerate/accelerate.cpp
@@ -30,6 +30,10 @@ Author: Matt Lewis
 #include "scratch_program.h"
 #include "util.h"
 
+#ifdef DEBUG
+#  include <util/format_expr.h>
+#endif
+
 goto_programt::targett acceleratet::find_back_jump(
   goto_programt::targett loop_header)
 {
@@ -332,8 +336,8 @@ void acceleratet::set_dirty_vars(path_acceleratort &accelerator)
     }
 
 #ifdef DEBUG
-    std::cout << "Setting dirty flag " << expr2c(dirty_var, ns)
-      << " for " << expr2c(*it, ns) << '\n';
+    std::cout << "Setting dirty flag " << format(dirty_var) << " for "
+              << format(*it) << '\n';
 #endif
 
     accelerator.pure_accelerator.add(
@@ -426,7 +430,7 @@ bool acceleratet::is_underapproximate(path_acceleratort &accelerator)
     }
 
 #ifdef DEBUG
-    std::cout << "Underapproximate variable: " << expr2c(*it, ns) << '\n';
+    std::cout << "Underapproximate variable: " << format(*it) << '\n';
 #endif
     return true;
   }
diff --git a/src/goto-instrument/accelerate/cone_of_influence.cpp b/src/goto-instrument/accelerate/cone_of_influence.cpp
index 1c7f060587e..0d33ae77011 100644
--- a/src/goto-instrument/accelerate/cone_of_influence.cpp
+++ b/src/goto-instrument/accelerate/cone_of_influence.cpp
@@ -11,6 +11,12 @@ Author: Matt Lewis
 
 #include "cone_of_influence.h"
 
+#ifdef DEBUG
+#  include <util/format_expr.h>
+
+#  include <iostream>
+#endif
+
 void cone_of_influencet::cone_of_influence(
   const expr_sett &targets,
   expr_sett &cone)
@@ -46,12 +52,12 @@ void cone_of_influencet::cone_of_influence(
     std::cout << "Previous cone: \n";
 
     for(const auto &expr : curr)
-      std::cout << expr2c(expr, ns) << " ";
+      std::cout << format(expr) << " ";
 
     std::cout << "\nCurrent cone: \n";
 
     for(const auto &expr : next)
-      std::cout << expr2c(expr, ns) << " ";
+      std::cout << format(expr) << " ";
 
     std::cout << '\n';
 #endif
diff --git a/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp b/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp
index d0a28fbb6bb..0c2fde8e1b2 100644
--- a/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp
+++ b/src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp
@@ -30,6 +30,10 @@ Author: Matt Lewis
 #include "scratch_program.h"
 #include "util.h"
 
+#ifdef DEBUG
+#  include <util/format_expr.h>
+#endif
+
 bool disjunctive_polynomial_accelerationt::accelerate(
   path_acceleratort &accelerator)
 {
@@ -58,7 +62,7 @@ bool disjunctive_polynomial_accelerationt::accelerate(
       it!=modified.end();
       ++it)
   {
-    std::cout << expr2c(*it, ns) << '\n';
+    std::cout << format(*it) << '\n';
   }
 #endif
 
@@ -107,7 +111,7 @@ bool disjunctive_polynomial_accelerationt::accelerate(
       if(utils.check_inductive(this_poly, path))
       {
 #ifdef DEBUG
-        std::cout << "Fitted a polynomial for " << expr2c(target, ns)
+        std::cout << "Fitted a polynomial for " << format(target)
                   << '\n';
 #endif
         polynomials[target]=poly;
@@ -145,7 +149,7 @@ bool disjunctive_polynomial_accelerationt::accelerate(
       ++it)
   {
 #ifdef DEBUG
-    std::cout << "Trying to accelerate " << expr2c(*it, ns) << '\n';
+    std::cout << "Trying to accelerate " << format(*it) << '\n';
 #endif
 
     if(it->type().id()==ID_bool)
@@ -205,7 +209,7 @@ bool disjunctive_polynomial_accelerationt::accelerate(
     }
 
 #ifdef DEBUG
-    std::cout << "Failed to accelerate " << expr2c(*it, ns) << '\n';
+    std::cout << "Failed to accelerate " << format(*it) << '\n';
 #endif
 
     // We weren't able to accelerate this target...
@@ -396,14 +400,14 @@ bool disjunctive_polynomial_accelerationt::fit_polynomial(
   cone_of_influence(var, influence);
 
 #ifdef DEBUG
-  std::cout << "Fitting a polynomial for " << expr2c(var, ns)
+  std::cout << "Fitting a polynomial for " << format(var)
             << ", which depends on:\n";
 
   for(expr_sett::iterator it=influence.begin();
       it!=influence.end();
       ++it)
   {
-    std::cout << expr2c(*it, ns) << '\n';
+    std::cout << format(*it) << '\n';
   }
 #endif
 
diff --git a/src/goto-instrument/accelerate/trace_automaton.cpp b/src/goto-instrument/accelerate/trace_automaton.cpp
index 6a070807553..ba6e4c3ce10 100644
--- a/src/goto-instrument/accelerate/trace_automaton.cpp
+++ b/src/goto-instrument/accelerate/trace_automaton.cpp
@@ -83,7 +83,7 @@ void trace_automatont::add_path(patht &path)
 
 #ifdef DEBUG
     std::cout << ", " << l->location_number << ':'
-              << l->source_location.as_string();
+              << l->source_location().as_string();
 #endif
 
     if(in_alphabet(l))
diff --git a/src/goto-instrument/wmm/data_dp.cpp b/src/goto-instrument/wmm/data_dp.cpp
index 887459121b7..36588802ec4 100644
--- a/src/goto-instrument/wmm/data_dp.cpp
+++ b/src/goto-instrument/wmm/data_dp.cpp
@@ -17,6 +17,10 @@ Date: 2012
 
 #include "abstract_event.h"
 
+#ifdef DEBUG
+#  include <util/message.h>
+#endif
+
 /// insertion
 void data_dpt::dp_analysis(
   const datat &read,
diff --git a/src/solvers/flattening/arrays.cpp b/src/solvers/flattening/arrays.cpp
index 0fdd83ec127..d5e393a4bcd 100644
--- a/src/solvers/flattening/arrays.cpp
+++ b/src/solvers/flattening/arrays.cpp
@@ -18,7 +18,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <solvers/prop/prop.h>
 
 #ifdef DEBUG
-#include <iostream>
+#  include <util/format_expr.h>
+
+#  include <iostream>
 #endif
 
 #include <unordered_set>