diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp
index bed62f95b28..3ac8cf3b484 100644
--- a/src/goto-symex/goto_symex_state.cpp
+++ b/src/goto-symex/goto_symex_state.cpp
@@ -17,6 +17,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/base_exceptions.h>
 #include <util/exception_utils.h>
 #include <util/expr_util.h>
+#include <util/format.h>
+#include <util/format_expr.h>
 #include <util/invariant.h>
 #include <util/prefix.h>
 #include <util/std_expr.h>
@@ -780,3 +782,14 @@ void goto_symex_statet::print_backtrace(std::ostream &out) const
     }
   }
 }
+
+/// Print the constant propagation map in a human-friendly format.
+/// This is primarily for use from the debugger; please don't delete me just
+/// because there aren't any current callers.
+void goto_symex_statet::output_propagation_map(std::ostream &out)
+{
+  for(const auto &name_value : propagation)
+  {
+    out << name_value.first << " <- " << format(name_value.second) << "\n";
+  }
+}
diff --git a/src/goto-symex/goto_symex_state.h b/src/goto-symex/goto_symex_state.h
index 74381d907de..b2dcd4741dc 100644
--- a/src/goto-symex/goto_symex_state.h
+++ b/src/goto-symex/goto_symex_state.h
@@ -67,6 +67,7 @@ class goto_symex_statet final
 
   // Map L1 names to (L2) constants
   std::map<irep_idt, exprt> propagation;
+  void output_propagation_map(std::ostream &);
 
   enum levelt { L0=0, L1=1, L2=2 };