diff --git a/src/analyses/constant_propagator.cpp b/src/analyses/constant_propagator.cpp
index 8a18888fbcf..bbf20546b68 100644
--- a/src/analyses/constant_propagator.cpp
+++ b/src/analyses/constant_propagator.cpp
@@ -13,6 +13,7 @@ Author: Peter Schrammel
 
 #ifdef DEBUG
 #include <iostream>
+#include <util/format_expr.h>
 #endif
 
 #include <util/find_symbols.h>
@@ -219,7 +220,7 @@ bool constant_propagator_domaint::two_way_propagate_rec(
   const namespacet &ns)
 {
 #ifdef DEBUG
-  std::cout << "two_way_propagate_rec: " << from_expr(ns, "", expr) << '\n';
+  std::cout << "two_way_propagate_rec: " << format(expr) << '\n';
 #endif
 
   bool change=false;
@@ -379,7 +380,7 @@ void constant_propagator_domaint::valuest::output(
 
   for(const auto &p : replace_const.expr_map)
   {
-    out << ' ' << p.first << "=" << from_expr(ns, "", p.second) << '\n';
+    out << ' ' << p.first << "=" << from_expr(ns, p.first, p.second) << '\n';
   }
 }
 
diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp
index e5bd4416fbd..27d5fc318da 100644
--- a/src/analyses/goto_check.cpp
+++ b/src/analyses/goto_check.cpp
@@ -28,7 +28,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/cprover_prefix.h>
 #include <util/options.h>
 
-#include <langapi/language_util.h>
+#include <langapi/language.h>
+#include <langapi/mode.h>
 
 #include "local_bitvector_analysis.h"
 
@@ -80,9 +81,8 @@ class goto_checkt
   void check_rec(
     const exprt &expr,
     guardt &guard,
-    bool address,
-    const irep_idt &mode);
-  void check(const exprt &expr, const irep_idt &mode);
+    bool address);
+  void check(const exprt &expr);
 
   void bounds_check(const index_exprt &expr, const guardt &guard);
   void div_by_zero_check(const div_exprt &expr, const guardt &guard);
@@ -94,8 +94,7 @@ class goto_checkt
     const dereference_exprt &expr,
     const guardt &guard,
     const exprt &access_lb,
-    const exprt &access_ub,
-    const irep_idt &mode);
+    const exprt &access_ub);
   void integer_overflow_check(const exprt &expr, const guardt &guard);
   void conversion_check(const exprt &expr, const guardt &guard);
   void float_overflow_check(const exprt &expr, const guardt &guard);
@@ -141,6 +140,8 @@ class goto_checkt
   typedef std::pair<exprt, exprt> allocationt;
   typedef std::list<allocationt> allocationst;
   allocationst allocations;
+
+  irep_idt mode;
 };
 
 void goto_checkt::collect_allocations(
@@ -917,8 +918,7 @@ void goto_checkt::pointer_validity_check(
   const dereference_exprt &expr,
   const guardt &guard,
   const exprt &access_lb,
-  const exprt &access_ub,
-  const irep_idt &mode)
+  const exprt &access_ub)
 {
   if(!enable_pointer_check)
     return;
@@ -1274,7 +1274,8 @@ void goto_checkt::add_guarded_claim(
 
     goto_programt::targett t=new_code.add_instruction(type);
 
-    std::string source_expr_string=from_expr(ns, "", src_expr);
+    std::string source_expr_string;
+    get_language_from_mode(mode)->from_expr(src_expr, source_expr_string, ns);
 
     t->guard.swap(new_expr);
     t->source_location=source_location;
@@ -1283,11 +1284,7 @@ void goto_checkt::add_guarded_claim(
   }
 }
 
-void goto_checkt::check_rec(
-  const exprt &expr,
-  guardt &guard,
-  bool address,
-  const irep_idt &mode)
+void goto_checkt::check_rec(const exprt &expr, guardt &guard, bool address)
 {
   // we don't look into quantifiers
   if(expr.id()==ID_exists || expr.id()==ID_forall)
@@ -1298,18 +1295,18 @@ void goto_checkt::check_rec(
     if(expr.id()==ID_dereference)
     {
       assert(expr.operands().size()==1);
-      check_rec(expr.op0(), guard, false, mode);
+      check_rec(expr.op0(), guard, false);
     }
     else if(expr.id()==ID_index)
     {
       assert(expr.operands().size()==2);
-      check_rec(expr.op0(), guard, true, mode);
-      check_rec(expr.op1(), guard, false, mode);
+      check_rec(expr.op0(), guard, true);
+      check_rec(expr.op1(), guard, false);
     }
     else
     {
       forall_operands(it, expr)
-        check_rec(*it, guard, true, mode);
+        check_rec(*it, guard, true);
     }
     return;
   }
@@ -1317,7 +1314,7 @@ void goto_checkt::check_rec(
   if(expr.id()==ID_address_of)
   {
     assert(expr.operands().size()==1);
-    check_rec(expr.op0(), guard, true, mode);
+    check_rec(expr.op0(), guard, true);
     return;
   }
   else if(expr.id()==ID_and || expr.id()==ID_or)
@@ -1334,7 +1331,7 @@ void goto_checkt::check_rec(
         throw "`"+expr.id_string()+"' takes Boolean operands only, but got "+
               op.pretty();
 
-      check_rec(op, guard, false, mode);
+      check_rec(op, guard, false);
 
       if(expr.id()==ID_or)
         guard.add(not_exprt(op));
@@ -1359,19 +1356,19 @@ void goto_checkt::check_rec(
       throw msg;
     }
 
-    check_rec(expr.op0(), guard, false, mode);
+    check_rec(expr.op0(), guard, false);
 
     {
       guardt old_guard=guard;
       guard.add(expr.op0());
-      check_rec(expr.op1(), guard, false, mode);
+      check_rec(expr.op1(), guard, false);
       guard.swap(old_guard);
     }
 
     {
       guardt old_guard=guard;
       guard.add(not_exprt(expr.op0()));
-      check_rec(expr.op2(), guard, false, mode);
+      check_rec(expr.op2(), guard, false);
       guard.swap(old_guard);
     }
 
@@ -1384,7 +1381,7 @@ void goto_checkt::check_rec(
     const dereference_exprt &deref=
       to_dereference_expr(member.struct_op());
 
-    check_rec(deref.op0(), guard, false, mode);
+    check_rec(deref.op0(), guard, false);
 
     exprt access_ub=nil_exprt();
 
@@ -1394,13 +1391,13 @@ void goto_checkt::check_rec(
     if(member_offset.is_not_nil() && size.is_not_nil())
       access_ub=plus_exprt(member_offset, size);
 
-    pointer_validity_check(deref, guard, member_offset, access_ub, mode);
+    pointer_validity_check(deref, guard, member_offset, access_ub);
 
     return;
   }
 
   forall_operands(it, expr)
-    check_rec(*it, guard, false, mode);
+    check_rec(*it, guard, false);
 
   if(expr.id()==ID_index)
   {
@@ -1462,21 +1459,21 @@ void goto_checkt::check_rec(
       to_dereference_expr(expr),
       guard,
       nil_exprt(),
-      size_of_expr(expr.type(), ns),
-      mode);
+      size_of_expr(expr.type(), ns));
 }
 
-void goto_checkt::check(const exprt &expr, const irep_idt &mode)
+void goto_checkt::check(const exprt &expr)
 {
   guardt guard;
-  check_rec(expr, guard, false, mode);
+  check_rec(expr, guard, false);
 }
 
 void goto_checkt::goto_check(
   goto_functiont &goto_function,
-  const irep_idt &mode)
+  const irep_idt &_mode)
 {
   assertions.clear();
+  mode = _mode;
 
   local_bitvector_analysist local_bitvector_analysis_obj(goto_function);
   local_bitvector_analysis=&local_bitvector_analysis_obj;
@@ -1497,7 +1494,7 @@ void goto_checkt::goto_check(
        i.is_target())
       assertions.clear();
 
-    check(i.guard, mode);
+    check(i.guard);
 
     // magic ERROR label?
     for(const auto &label : error_labels)
@@ -1523,20 +1520,20 @@ void goto_checkt::goto_check(
 
       if(statement==ID_expression)
       {
-        check(i.code, mode);
+        check(i.code);
       }
       else if(statement==ID_printf)
       {
         forall_operands(it, i.code)
-          check(*it, mode);
+          check(*it);
       }
     }
     else if(i.is_assign())
     {
       const code_assignt &code_assign=to_code_assign(i.code);
 
-      check(code_assign.lhs(), mode);
-      check(code_assign.rhs(), mode);
+      check(code_assign.lhs());
+      check(code_assign.rhs());
 
       // the LHS might invalidate any assertion
       invalidate(code_assign.lhs());
@@ -1576,7 +1573,7 @@ void goto_checkt::goto_check(
       }
 
       forall_operands(it, code_function_call)
-        check(*it, mode);
+        check(*it);
 
       // the call might invalidate any assertion
       assertions.clear();
@@ -1585,7 +1582,7 @@ void goto_checkt::goto_check(
     {
       if(i.code.operands().size()==1)
       {
-        check(i.code.op0(), mode);
+        check(i.code.op0());
         // the return value invalidate any assertion
         invalidate(i.code.op0());
       }
diff --git a/src/analyses/goto_rw.cpp b/src/analyses/goto_rw.cpp
index 6ce09759419..d02afd0ae6c 100644
--- a/src/analyses/goto_rw.cpp
+++ b/src/analyses/goto_rw.cpp
@@ -633,6 +633,8 @@ void guarded_range_domaint::output(
     if(itr!=begin())
       out << ";";
     out << itr->first << ":" << itr->second.first;
+    // we don't know what mode (language) we are in, so we rely on the default
+    // language to be reasonable for from_expr
     out << " if " << from_expr(ns, "", itr->second.second);
   }
   out << "]";
diff --git a/src/analyses/invariant_set.cpp b/src/analyses/invariant_set.cpp
index 526ceb88231..bd83043140e 100644
--- a/src/analyses/invariant_set.cpp
+++ b/src/analyses/invariant_set.cpp
@@ -131,6 +131,8 @@ std::string inv_object_storet::build_string(const exprt &expr) const
 
   // we also like "address_of" and "reference_to"
   // if the object is constant
+  // we don't know what mode (language) we are in, so we rely on the default
+  // language to be reasonable for from_expr
   if(is_constant_address(expr))
     return from_expr(ns, "", expr);
 
@@ -884,7 +886,6 @@ std::string inv_object_storet::to_string(
   unsigned a,
   const irep_idt &identifier) const
 {
-  // return from_expr(ns, "", get_expr(a));
   return id2string(map[a]);
 }
 
diff --git a/src/analyses/local_may_alias.cpp b/src/analyses/local_may_alias.cpp
index 69728c66e59..5164db6e3bc 100644
--- a/src/analyses/local_may_alias.cpp
+++ b/src/analyses/local_may_alias.cpp
@@ -457,7 +457,10 @@ void local_may_aliast::output(
           if(loc_info.aliases.find(j)==i)
           {
             assert(j<objects.size());
-            out << ' ' << from_expr(ns, "", objects[j]);
+            irep_idt identifier = "";
+            if(objects[j].id() == ID_symbol)
+              identifier = to_symbol_expr(objects[j]).get_identifier();
+            out << ' ' << from_expr(ns, identifier, objects[j]);
           }
 
         out << " }";
diff --git a/src/cbmc/bmc.cpp b/src/cbmc/bmc.cpp
index 69a255f9852..37bedbed2f4 100644
--- a/src/cbmc/bmc.cpp
+++ b/src/cbmc/bmc.cpp
@@ -239,17 +239,16 @@ void bmct::show_program()
   {
     std::cout << "// " << step.source.pc->location_number << " ";
     std::cout << step.source.pc->source_location.as_string() << "\n";
+    const irep_idt &function = step.source.pc->function;
 
     if(step.is_assignment())
     {
-      std::string string_value=
-        from_expr(ns, "", step.cond_expr);
+      std::string string_value = from_expr(ns, function, step.cond_expr);
       std::cout << "(" << count << ") " << string_value << "\n";
 
       if(!step.guard.is_true())
       {
-        std::string string_value=
-          from_expr(ns, "", step.guard);
+        std::string string_value = from_expr(ns, function, step.guard);
         std::cout << std::string(std::to_string(count).size()+3, ' ');
         std::cout << "guard: " << string_value << "\n";
       }
@@ -258,15 +257,13 @@ void bmct::show_program()
     }
     else if(step.is_assert())
     {
-      std::string string_value=
-        from_expr(ns, "", step.cond_expr);
+      std::string string_value = from_expr(ns, function, step.cond_expr);
       std::cout << "(" << count << ") ASSERT("
                 << string_value <<") " << "\n";
 
       if(!step.guard.is_true())
       {
-        std::string string_value=
-          from_expr(ns, "", step.guard);
+        std::string string_value = from_expr(ns, function, step.guard);
         std::cout << std::string(std::to_string(count).size()+3, ' ');
         std::cout << "guard: " << string_value << "\n";
       }
@@ -275,15 +272,13 @@ void bmct::show_program()
     }
     else if(step.is_assume())
     {
-      std::string string_value=
-        from_expr(ns, "", step.cond_expr);
+      std::string string_value = from_expr(ns, function, step.cond_expr);
       std::cout << "(" << count << ") ASSUME("
                 << string_value <<") " << "\n";
 
       if(!step.guard.is_true())
       {
-        std::string string_value=
-          from_expr(ns, "", step.guard);
+        std::string string_value = from_expr(ns, function, step.guard);
         std::cout << std::string(std::to_string(count).size()+3, ' ');
         std::cout << "guard: " << string_value << "\n";
       }
@@ -292,8 +287,7 @@ void bmct::show_program()
     }
     else if(step.is_constraint())
     {
-      std::string string_value=
-        from_expr(ns, "", step.cond_expr);
+      std::string string_value = from_expr(ns, function, step.cond_expr);
       std::cout << "(" << count << ") CONSTRAINT("
                 << string_value <<") " << "\n";
 
@@ -301,16 +295,14 @@ void bmct::show_program()
     }
     else if(step.is_shared_read() || step.is_shared_write())
     {
-      std::string string_value=
-        from_expr(ns, "", step.ssa_lhs);
+      std::string string_value = from_expr(ns, function, step.ssa_lhs);
       std::cout << "(" << count << ") SHARED_"
                 << (step.is_shared_write()?"WRITE":"READ")
                 << "(" << string_value <<")\n";
 
       if(!step.guard.is_true())
       {
-        std::string string_value=
-          from_expr(ns, "", step.guard);
+        std::string string_value = from_expr(ns, function, step.guard);
         std::cout << std::string(std::to_string(count).size()+3, ' ');
         std::cout << "guard: " << string_value << "\n";
       }
diff --git a/src/cbmc/show_vcc.cpp b/src/cbmc/show_vcc.cpp
index 620ace0bb99..6a5b051cff9 100644
--- a/src/cbmc/show_vcc.cpp
+++ b/src/cbmc/show_vcc.cpp
@@ -53,7 +53,7 @@ void bmct::show_vcc_plain(std::ostream &out)
         if(!p_it->ignore)
         {
           std::string string_value=
-            from_expr(ns, "", p_it->cond_expr);
+            from_expr(ns, p_it->source.pc->function, p_it->cond_expr);
           out << "{-" << count << "} " << string_value << "\n";
 
           #if 0
@@ -69,7 +69,7 @@ void bmct::show_vcc_plain(std::ostream &out)
     out << "|--------------------------" << "\n";
 
     std::string string_value=
-      from_expr(ns, "", s_it->cond_expr);
+      from_expr(ns, s_it->source.pc->function, s_it->cond_expr);
     out << "{" << 1 << "} " << string_value << "\n";
 
     out << "\n";
@@ -119,13 +119,13 @@ void bmct::show_vcc_json(std::ostream &out)
          !p_it->ignore)
       {
         std::string string_value=
-          from_expr(ns, "", p_it->cond_expr);
+          from_expr(ns, p_it->source.pc->function, p_it->cond_expr);
         json_constraints.push_back(json_stringt(string_value));
       }
     }
 
     std::string string_value=
-      from_expr(ns, "", s_it->cond_expr);
+      from_expr(ns, s_it->source.pc->function, s_it->cond_expr);
     object["expression"]=json_stringt(string_value);
   }
 
diff --git a/src/goto-cc/compile.cpp b/src/goto-cc/compile.cpp
index c2473ff9dc6..b639489fa7d 100644
--- a/src/goto-cc/compile.cpp
+++ b/src/goto-cc/compile.cpp
@@ -465,9 +465,9 @@ bool compilet::parse(const std::string &file_name)
   if(override_language!="")
   {
     if(override_language=="c++" || override_language=="c++-header")
-      languagep=get_language_from_mode("cpp");
+      languagep = get_language_from_mode(ID_cpp);
     else
-      languagep=get_language_from_mode("C");
+      languagep = get_language_from_mode(ID_C);
   }
   else
     languagep=get_language_from_filename(file_name);
diff --git a/src/goto-instrument/cover_instrument_condition.cpp b/src/goto-instrument/cover_instrument_condition.cpp
index 47cf555ca22..32ed359654e 100644
--- a/src/goto-instrument/cover_instrument_condition.cpp
+++ b/src/goto-instrument/cover_instrument_condition.cpp
@@ -33,7 +33,7 @@ void cover_condition_instrumentert::instrument(
 
     for(const auto &c : conditions)
     {
-      const std::string c_string = from_expr(ns, "", c);
+      const std::string c_string = from_expr(ns, i_it->function, c);
 
       const std::string comment_t = "condition `" + c_string + "' true";
       const irep_idt function = i_it->function;
diff --git a/src/goto-instrument/cover_instrument_decision.cpp b/src/goto-instrument/cover_instrument_decision.cpp
index c6cda3c397a..5427f38bff0 100644
--- a/src/goto-instrument/cover_instrument_decision.cpp
+++ b/src/goto-instrument/cover_instrument_decision.cpp
@@ -32,7 +32,7 @@ void cover_decision_instrumentert::instrument(
 
     for(const auto &d : decisions)
     {
-      const std::string d_string = from_expr(ns, "", d);
+      const std::string d_string = from_expr(ns, i_it->function, d);
 
       const std::string comment_t = "decision `" + d_string + "' true";
       const irep_idt function = i_it->function;
diff --git a/src/goto-instrument/cover_instrument_mcdc.cpp b/src/goto-instrument/cover_instrument_mcdc.cpp
index 4873975e423..fe1c90f5b77 100644
--- a/src/goto-instrument/cover_instrument_mcdc.cpp
+++ b/src/goto-instrument/cover_instrument_mcdc.cpp
@@ -673,7 +673,7 @@ void cover_mcdc_instrumentert::instrument(
                                   ? "decision/condition"
                                   : is_decision ? "decision" : "condition";
 
-      std::string p_string = from_expr(ns, "", p);
+      std::string p_string = from_expr(ns, i_it->function, p);
 
       std::string comment_t = description + " `" + p_string + "' true";
       const irep_idt function = i_it->function;
@@ -710,7 +710,7 @@ void cover_mcdc_instrumentert::instrument(
 
     for(const auto &p : controlling)
     {
-      std::string p_string = from_expr(ns, "", p);
+      std::string p_string = from_expr(ns, i_it->function, p);
 
       std::string description =
         "MC/DC independence condition `" + p_string + "'";
diff --git a/src/goto-instrument/cover_instrument_other.cpp b/src/goto-instrument/cover_instrument_other.cpp
index 740eecd1a67..e7d0795d7f7 100644
--- a/src/goto-instrument/cover_instrument_other.cpp
+++ b/src/goto-instrument/cover_instrument_other.cpp
@@ -57,7 +57,8 @@ void cover_cover_instrumentert::instrument(
       code_function_call.arguments().size() == 1)
     {
       const exprt c = code_function_call.arguments()[0];
-      std::string comment = "condition `" + from_expr(ns, "", c) + "'";
+      std::string comment =
+        "condition `" + from_expr(ns, i_it->function, c) + "'";
       i_it->guard = not_exprt(c);
       i_it->type = ASSERT;
       i_it->code.clear();
diff --git a/src/goto-instrument/dot.cpp b/src/goto-instrument/dot.cpp
index 84f5cf6c907..02bb5cf4148 100644
--- a/src/goto-instrument/dot.cpp
+++ b/src/goto-instrument/dot.cpp
@@ -111,7 +111,7 @@ void dott::write_dot_subgraph(
           tmp.str("Goto");
         else
         {
-          std::string t = from_expr(ns, "", it->guard);
+          std::string t = from_expr(ns, it->function, it->guard);
           while(t[ t.size()-1 ]=='\n')
             t = t.substr(0, t.size()-1);
           tmp << escape(t) << "?";
@@ -119,14 +119,14 @@ void dott::write_dot_subgraph(
       }
       else if(it->is_assume())
       {
-        std::string t = from_expr(ns, "", it->guard);
+        std::string t = from_expr(ns, it->function, it->guard);
         while(t[ t.size()-1 ]=='\n')
           t = t.substr(0, t.size()-1);
         tmp << "Assume\\n(" << escape(t) << ")";
       }
       else if(it->is_assert())
       {
-        std::string t = from_expr(ns, "", it->guard);
+        std::string t = from_expr(ns, it->function, it->guard);
         while(t[ t.size()-1 ]=='\n')
           t = t.substr(0, t.size()-1);
         tmp << "Assert\\n(" << escape(t) << ")";
@@ -145,7 +145,7 @@ void dott::write_dot_subgraph(
         tmp.str("Atomic End");
       else if(it->is_function_call())
       {
-        std::string t = from_expr(ns, "", it->code);
+        std::string t = from_expr(ns, it->function, it->code);
         while(t[ t.size()-1 ]=='\n')
           t = t.substr(0, t.size()-1);
         tmp.str(escape(t));
@@ -162,7 +162,7 @@ void dott::write_dot_subgraph(
               it->is_return() ||
               it->is_other())
       {
-        std::string t = from_expr(ns, "", it->code);
+        std::string t = from_expr(ns, it->function, it->code);
         while(t[ t.size()-1 ]=='\n')
           t = t.substr(0, t.size()-1);
         tmp.str(escape(t));
diff --git a/src/goto-instrument/rw_set.cpp b/src/goto-instrument/rw_set.cpp
index 39681fe5660..d6a2380dd78 100644
--- a/src/goto-instrument/rw_set.cpp
+++ b/src/goto-instrument/rw_set.cpp
@@ -29,7 +29,7 @@ void rw_set_baset::output(std::ostream &out) const
       it++)
   {
     out << it->second.object << " if "
-        << from_expr(ns, "", it->second.guard) << '\n';
+        << from_expr(ns, it->second.object, it->second.guard) << '\n';
   }
 
   out << '\n';
@@ -40,7 +40,7 @@ void rw_set_baset::output(std::ostream &out) const
       it++)
   {
     out << it->second.object << " if "
-        << from_expr(ns, "", it->second.guard) << '\n';
+        << from_expr(ns, it->second.object, it->second.guard) << '\n';
   }
 }
 
diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp
index 35e67c16b5e..a1dc45880ed 100644
--- a/src/goto-programs/builtin_functions.cpp
+++ b/src/goto-programs/builtin_functions.cpp
@@ -1002,7 +1002,7 @@ void goto_convertt::do_function_call_symbol(
     t->source_location.set("user-provided", true);
     t->source_location.set_property_class(ID_assertion);
     t->source_location.set_comment(
-      "assertion "+id2string(from_expr(ns, "", t->guard)));
+      "assertion " + id2string(from_expr(ns, identifier, t->guard)));
 
     // let's double-check the type of the argument
     if(t->guard.type().id()!=ID_bool)
diff --git a/src/goto-programs/goto_trace.cpp b/src/goto-programs/goto_trace.cpp
index d93fc3f7055..b98a5f813f9 100644
--- a/src/goto-programs/goto_trace.cpp
+++ b/src/goto-programs/goto_trace.cpp
@@ -110,7 +110,7 @@ void goto_trace_stept::output(
 
       if(comment!="")
         out << "  " << comment << "\n";
-      out << "  " << from_expr(ns, "", pc->guard) << "\n";
+      out << "  " << from_expr(ns, pc->function, pc->guard) << "\n";
       out << "\n";
     }
   }
@@ -273,7 +273,8 @@ void show_goto_trace(
         out << "  " << step.comment << "\n";
 
         if(step.pc->is_assert())
-          out << "  " << from_expr(ns, "", step.pc->guard) << "\n";
+          out << "  " << from_expr(ns, step.pc->function, step.pc->guard)
+              << '\n';
 
         out << "\n";
       }
@@ -288,7 +289,8 @@ void show_goto_trace(
           out << "  " << step.pc->source_location << "\n";
 
         if(step.pc->is_assume())
-          out << "  " << from_expr(ns, "", step.pc->guard) << "\n";
+          out << "  " << from_expr(ns, step.pc->function, step.pc->guard)
+              << '\n';
 
         out << "\n";
       }
@@ -354,7 +356,7 @@ void show_goto_trace(
         {
           if(l_it!=step.io_args.begin())
             out << ";";
-          out << " " << from_expr(ns, "", *l_it);
+          out << " " << from_expr(ns, step.pc->function, *l_it);
 
           // the binary representation
           out << " (" << trace_value_binary(*l_it, ns) << ")";
@@ -375,7 +377,7 @@ void show_goto_trace(
       {
         if(l_it!=step.io_args.begin())
           out << ";";
-        out << " " << from_expr(ns, "", *l_it);
+        out << " " << from_expr(ns, step.pc->function, *l_it);
 
         // the binary representation
         out << " (" << trace_value_binary(*l_it, ns) << ")";
diff --git a/src/goto-programs/graphml_witness.cpp b/src/goto-programs/graphml_witness.cpp
index 0a089fc30c5..ccae6ad7e55 100644
--- a/src/goto-programs/graphml_witness.cpp
+++ b/src/goto-programs/graphml_witness.cpp
@@ -302,9 +302,10 @@ void graphml_witnesst::operator()(const goto_tracet &goto_trace)
         {
           xmlt &val=edge.new_element("data");
           val.set_attribute("key", "sourcecode");
-          const std::string cond=from_expr(ns, "", it->cond_expr);
+          const std::string cond =
+            from_expr(ns, it->pc->function, it->cond_expr);
           const std::string neg_cond=
-            from_expr(ns, "", not_exprt(it->cond_expr));
+            from_expr(ns, it->pc->function, not_exprt(it->cond_expr));
           val.data="["+(it->cond_value ? cond : neg_cond)+"]";
 
           #if 0
@@ -485,8 +486,8 @@ void graphml_witnesst::operator()(const symex_target_equationt &equation)
         {
           xmlt &val=edge.new_element("data");
           val.set_attribute("key", "sourcecode");
-          const std::string cond=from_expr(ns, "", it->cond_expr);
-            from_expr(ns, "", not_exprt(it->cond_expr));
+          const std::string cond =
+            from_expr(ns, it->source.pc->function, it->cond_expr);
           val.data="["+cond+"]";
         }
 
diff --git a/src/goto-programs/xml_goto_trace.cpp b/src/goto-programs/xml_goto_trace.cpp
index dca2c704a2b..08a12d1e82e 100644
--- a/src/goto-programs/xml_goto_trace.cpp
+++ b/src/goto-programs/xml_goto_trace.cpp
@@ -147,7 +147,8 @@ void convert(
 
         for(const auto &arg : step.io_args)
         {
-          xml_output.new_element("value").data=from_expr(ns, "", arg);
+          xml_output.new_element("value").data =
+            from_expr(ns, step.pc->function, arg);
           xml_output.new_element("value_expression").
             new_element(xml(arg, ns));
         }
@@ -165,7 +166,8 @@ void convert(
 
         for(const auto &arg : step.io_args)
         {
-          xml_input.new_element("value").data=from_expr(ns, "", arg);
+          xml_input.new_element("value").data =
+            from_expr(ns, step.pc->function, arg);
           xml_input.new_element("value_expression").
             new_element(xml(arg, ns));
         }
diff --git a/src/goto-symex/slice_by_trace.cpp b/src/goto-symex/slice_by_trace.cpp
index 828b457caa0..5218870e96f 100644
--- a/src/goto-symex/slice_by_trace.cpp
+++ b/src/goto-symex/slice_by_trace.cpp
@@ -21,8 +21,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/arith_tools.h>
 #include <util/std_expr.h>
 #include <util/guard.h>
-
-#include <langapi/language_util.h>
+#include <util/format_expr.h>
 
 void symex_slice_by_tracet::slice_by_trace(
   std::string trace_files,
@@ -258,10 +257,10 @@ void symex_slice_by_tracet::compute_ts_back(
 
 #if 0
       std::cout << "EVENT:  " << event << '\n';
-      std::cout << "GUARD:  " << from_expr(ns, "", guard) << '\n';
+      std::cout << "GUARD:  " << format(guard) << '\n';
       for(size_t j=0; j < t.size(); j++)
       {
-        std::cout << "t[" << j << "]=" << from_expr(ns, "", t[j]) <<
+        std::cout << "t[" << j << "]=" << format(t[j]) <<
           '\n';
       }
 #endif
diff --git a/src/goto-symex/symex_dereference.cpp b/src/goto-symex/symex_dereference.cpp
index 82bb1073db7..95b8866865e 100644
--- a/src/goto-symex/symex_dereference.cpp
+++ b/src/goto-symex/symex_dereference.cpp
@@ -19,7 +19,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <pointer-analysis/value_set_dereference.h>
 #include <pointer-analysis/rewrite_index.h>
-#include <langapi/language_util.h>
 
 #include <util/c_types.h>
 
@@ -251,7 +250,7 @@ void goto_symext::dereference_rec(
     value_set_dereferencet dereference(
       ns, state.symbol_table, options, symex_dereference_state, language_mode);
 
-    // std::cout << "**** " << from_expr(ns, "", tmp1) << '\n';
+    // std::cout << "**** " << format(tmp1) << '\n';
     exprt tmp2=
       dereference.dereference(
         tmp1,
@@ -259,7 +258,7 @@ void goto_symext::dereference_rec(
         write?
           value_set_dereferencet::modet::WRITE:
           value_set_dereferencet::modet::READ);
-    // std::cout << "**** " << from_expr(ns, "", tmp2) << '\n';
+    // std::cout << "**** " << format(tmp2) << '\n';
 
     expr.swap(tmp2);
 
diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp
index 66731b82d55..8c33d25541d 100644
--- a/src/goto-symex/symex_main.cpp
+++ b/src/goto-symex/symex_main.cpp
@@ -297,8 +297,8 @@ void goto_symext::symex_step(
   #if 0
   std::cout << "\ninstruction type is " << state.source.pc->type << '\n';
   std::cout << "Location: " << state.source.pc->source_location << '\n';
-  std::cout << "Guard: " << from_expr(ns, "", state.guard.as_expr()) << '\n';
-  std::cout << "Code: " << from_expr(ns, "", state.source.pc->code) << '\n';
+  std::cout << "Guard: " << format(state.guard.as_expr()) << '\n';
+  std::cout << "Code: " << format(state.source.pc->code) << '\n';
   #endif
 
   PRECONDITION(!state.threads.empty());
diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp
index 9ec1adc4efe..27be83608f1 100644
--- a/src/goto-symex/symex_target_equation.cpp
+++ b/src/goto-symex/symex_target_equation.cpp
@@ -618,9 +618,11 @@ void symex_target_equationt::SSA_stept::output(
   switch(type)
   {
   case goto_trace_stept::typet::ASSERT:
-    out << "ASSERT " << from_expr(ns, "", cond_expr) << '\n'; break;
+    out << "ASSERT " << from_expr(ns, source.pc->function, cond_expr) << '\n';
+    break;
   case goto_trace_stept::typet::ASSUME:
-    out << "ASSUME " << from_expr(ns, "", cond_expr) << '\n'; break;
+    out << "ASSUME " << from_expr(ns, source.pc->function, cond_expr) << '\n';
+    break;
   case goto_trace_stept::typet::LOCATION:
     out << "LOCATION" << '\n'; break;
   case goto_trace_stept::typet::INPUT:
@@ -630,7 +632,7 @@ void symex_target_equationt::SSA_stept::output(
 
   case goto_trace_stept::typet::DECL:
     out << "DECL" << '\n';
-    out << from_expr(ns, "", ssa_lhs) << '\n';
+    out << from_expr(ns, source.pc->function, ssa_lhs) << '\n';
     break;
 
   case goto_trace_stept::typet::ASSIGNMENT:
@@ -684,19 +686,20 @@ void symex_target_equationt::SSA_stept::output(
   case goto_trace_stept::typet::MEMORY_BARRIER:
     out << "MEMORY_BARRIER\n"; break;
   case goto_trace_stept::typet::GOTO:
-    out << "IF " << from_expr(ns, "", cond_expr) << " GOTO\n"; break;
+    out << "IF " << from_expr(ns, source.pc->function, cond_expr) << " GOTO\n";
+    break;
 
   default: UNREACHABLE;
   }
 
   if(is_assert() || is_assume() || is_assignment() || is_constraint())
-    out << from_expr(ns, "", cond_expr) << '\n';
+    out << from_expr(ns, source.pc->function, cond_expr) << '\n';
 
   if(is_assert() || is_constraint())
     out << comment << '\n';
 
   if(is_shared_read() || is_shared_write())
-    out << from_expr(ns, "", ssa_lhs) << '\n';
+    out << from_expr(ns, source.pc->function, ssa_lhs) << '\n';
 
-  out << "Guard: " << from_expr(ns, "", guard) << '\n';
+  out << "Guard: " << from_expr(ns, source.pc->function, guard) << '\n';
 }
diff --git a/src/pointer-analysis/dereference.cpp b/src/pointer-analysis/dereference.cpp
index f7ba400ef78..863c44cffb7 100644
--- a/src/pointer-analysis/dereference.cpp
+++ b/src/pointer-analysis/dereference.cpp
@@ -13,7 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #ifdef DEBUG
 #include <iostream>
-#include <langapi/language_util.h>
+#include <util/format_expr.h>
 #endif
 
 #include <util/std_expr.h>
@@ -37,7 +37,7 @@ exprt dereferencet::operator()(const exprt &pointer)
   const typet &type=pointer.type().subtype();
 
   #ifdef DEBUG
-  std::cout << "DEREF: " << from_expr(ns, "", pointer) << '\n';
+  std::cout << "DEREF: " << format(pointer) << '\n';
   #endif
 
   return dereference_rec(
diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp
index c9858d251cb..0e528f5760b 100644
--- a/src/pointer-analysis/value_set.cpp
+++ b/src/pointer-analysis/value_set.cpp
@@ -30,6 +30,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #ifdef DEBUG
 #include <iostream>
+#include <util/format_expr.h>
+#include <util/format_type.h>
 #endif
 
 #include "add_failed_symbols.h"
@@ -331,7 +333,7 @@ void value_sett::get_value_set(
   #if 0
   for(value_setst::valuest::const_iterator it=dest.begin();
       it!=dest.end(); it++)
-    std::cout << "GET_VALUE_SET: " << from_expr(ns, "", *it) << '\n';
+    std::cout << "GET_VALUE_SET: " << format(*it) << '\n';
   #endif
 }
 
@@ -356,7 +358,7 @@ void value_sett::get_value_set_rec(
   const namespacet &ns) const
 {
   #if 0
-  std::cout << "GET_VALUE_SET_REC EXPR: " << from_expr(ns, "", expr) << "\n";
+  std::cout << "GET_VALUE_SET_REC EXPR: " << format(expr) << "\n";
   std::cout << "GET_VALUE_SET_REC SUFFIX: " << suffix << '\n';
   #endif
 
@@ -888,7 +890,7 @@ void value_sett::get_value_set_rec(
   for(const auto &obj : dest.read())
   {
     const exprt &e=to_expr(obj);
-    std::cout << "  " << from_expr(ns, "", e) << "\n";
+    std::cout << "  " << format(e) << "\n";
   }
   std::cout << "\n";
   #endif
@@ -933,7 +935,7 @@ void value_sett::get_reference_set_rec(
   const namespacet &ns) const
 {
   #if 0
-  std::cout << "GET_REFERENCE_SET_REC EXPR: " << from_expr(ns, "", expr)
+  std::cout << "GET_REFERENCE_SET_REC EXPR: " << format(expr)
             << '\n';
   #endif
 
@@ -960,7 +962,7 @@ void value_sett::get_reference_set_rec(
     #if 0
     for(expr_sett::const_iterator it=value_set.begin();
         it!=value_set.end(); it++)
-      std::cout << "VALUE_SET: " << from_expr(ns, "", *it) << '\n';
+      std::cout << "VALUE_SET: " << format(*it) << '\n';
     #endif
 
     return;
@@ -1097,10 +1099,10 @@ void value_sett::assign(
   bool add_to_sets)
 {
 #if 0
-  std::cout << "ASSIGN LHS: " << from_expr(ns, "", lhs) << " : "
-            << from_type(ns, "", lhs.type()) << '\n';
-  std::cout << "ASSIGN RHS: " << from_expr(ns, "", rhs) << " : "
-            << from_type(ns, "", rhs.type()) << '\n';
+  std::cout << "ASSIGN LHS: " << format(lhs) << " : "
+            << format(lhs.type()) << '\n';
+  std::cout << "ASSIGN RHS: " << format(rhs) << " : "
+            << format(rhs.type()) << '\n';
   std::cout << "--------------------------------------------\n";
   output(ns, std::cout);
 #endif
@@ -1305,7 +1307,7 @@ void value_sett::assign_rec(
   bool add_to_sets)
 {
   #if 0
-  std::cout << "ASSIGN_REC LHS: " << from_expr(ns, "", lhs) << '\n';
+  std::cout << "ASSIGN_REC LHS: " << format(lhs) << '\n';
   std::cout << "ASSIGN_REC LHS ID: " << lhs.id() << '\n';
   std::cout << "ASSIGN_REC SUFFIX: " << suffix << '\n';
 
@@ -1313,7 +1315,7 @@ void value_sett::assign_rec(
       it!=values_rhs.read().end();
       it++)
     std::cout << "ASSIGN_REC RHS: " <<
-      from_expr(ns, "", object_numbering[it->first]) << '\n';
+      format(object_numbering[it->first]) << '\n';
   std::cout << '\n';
   #endif
 
diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp
index 542bbdaf989..59a62f31cd6 100644
--- a/src/pointer-analysis/value_set_dereference.cpp
+++ b/src/pointer-analysis/value_set_dereference.cpp
@@ -13,10 +13,13 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #ifdef DEBUG
 #include <iostream>
+#include <util/format_expr.h>
 #endif
 
 #include <cassert>
+#include <sstream>
 
+#include <util/format_type.h>
 #include <util/invariant.h>
 #include <util/string2int.h>
 #include <util/expr_util.h>
@@ -40,8 +43,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <pointer-analysis/value_set.h>
 
-#include <langapi/language_util.h>
-
 #include "pointer_offset_sum.h"
 
 // global data, horrible
@@ -88,7 +89,7 @@ exprt value_set_dereferencet::dereference(
   const typet &type=pointer.type().subtype();
 
   #if 0
-  std::cout << "DEREF: " << from_expr(ns, "", pointer) << '\n';
+  std::cout << "DEREF: " << format(pointer) << '\n';
   #endif
 
   // collect objects the pointer may point to
@@ -101,7 +102,7 @@ exprt value_set_dereferencet::dereference(
       it=points_to_set.begin();
       it!=points_to_set.end();
       it++)
-    std::cout << "P: " << from_expr(ns, "", *it) << '\n';
+    std::cout << "P: " << format(*it) << '\n';
   #endif
 
   // get the values of these
@@ -116,8 +117,8 @@ exprt value_set_dereferencet::dereference(
     valuet value=build_reference_to(*it, mode, pointer, guard);
 
     #if 0
-    std::cout << "V: " << from_expr(ns, "", value.pointer_guard) << " --> ";
-    std::cout << from_expr(ns, "", value.value) << '\n';
+    std::cout << "V: " << format(value.pointer_guard) << " --> ";
+    std::cout << format(value.value) << '\n';
     #endif
 
     values.push_back(value);
@@ -201,7 +202,7 @@ exprt value_set_dereferencet::dereference(
   }
 
   #if 0
-  std::cout << "R: " << from_expr(ns, "", value) << "\n\n";
+  std::cout << "R: " << format(value) << "\n\n";
   #endif
 
   return value;
@@ -291,7 +292,7 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
   const exprt &object=o.object();
 
   #if 0
-  std::cout << "O: " << from_expr(ns, "", root_object) << '\n';
+  std::cout << "O: " << format(root_object) << '\n';
   #endif
 
   valuet result;
@@ -569,15 +570,13 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
       {
         if(options.get_bool_option("pointer-check"))
         {
-          std::string msg="memory model not applicable (got `";
-          msg+=from_type(ns, "", result.value.type());
-          msg+="', expected `";
-          msg+=from_type(ns, "", dereference_type);
-          msg+="')";
+          std::ostringstream msg;
+          msg << "memory model not applicable (got `"
+              << format(result.value.type()) << "', expected `"
+              << format(dereference_type) << "')";
 
           dereference_callback.dereference_failure(
-            "pointer dereference",
-            msg, tmp_guard);
+            "pointer dereference", msg.str(), tmp_guard);
         }
 
         return valuet(); // give up, no way that this is ok
diff --git a/src/pointer-analysis/value_set_fi.cpp b/src/pointer-analysis/value_set_fi.cpp
index 0f8179787c7..d72e7fdda19 100644
--- a/src/pointer-analysis/value_set_fi.cpp
+++ b/src/pointer-analysis/value_set_fi.cpp
@@ -350,7 +350,7 @@ void value_set_fit::get_value_set(
 
   #if 0
   for(expr_sett::const_iterator it=value_set.begin(); it!=value_set.end(); it++)
-    std::cout << "GET_VALUE_SET: " << from_expr(ns, "", *it) << '\n';
+    std::cout << "GET_VALUE_SET: " << format(*it) << '\n';
   #endif
 }
 
@@ -375,7 +375,7 @@ void value_set_fit::get_value_set_rec(
   gvs_recursion_sett &recursion_set) const
 {
   #if 0
-  std::cout << "GET_VALUE_SET_REC EXPR: " << from_expr(ns, "", expr)
+  std::cout << "GET_VALUE_SET_REC EXPR: " << format(expr)
             << '\n';
   std::cout << "GET_VALUE_SET_REC SUFFIX: " << suffix << '\n';
   std::cout << '\n';
@@ -768,7 +768,7 @@ void value_set_fit::get_reference_set_sharing_rec(
   const namespacet &ns) const
 {
   #if 0
-  std::cout << "GET_REFERENCE_SET_REC EXPR: " << from_expr(ns, "", expr)
+  std::cout << "GET_REFERENCE_SET_REC EXPR: " << format(expr)
             << '\n';
   #endif
 
@@ -843,7 +843,7 @@ void value_set_fit::get_reference_set_sharing_rec(
     for(expr_sett::const_iterator it=value_set.begin();
         it!=value_set.end();
         it++)
-      std::cout << "VALUE_SET: " << from_expr(ns, "", *it) << '\n';
+      std::cout << "VALUE_SET: " << format(*it) << '\n';
     #endif
 
     return;
@@ -960,8 +960,8 @@ void value_set_fit::assign(
   const namespacet &ns)
 {
   #if 0
-  std::cout << "ASSIGN LHS: " << from_expr(ns, "", lhs) << '\n';
-  std::cout << "ASSIGN RHS: " << from_expr(ns, "", rhs) << '\n';
+  std::cout << "ASSIGN LHS: " << format(lhs) << '\n';
+  std::cout << "ASSIGN RHS: " << format(rhs) << '\n';
   #endif
 
   if(rhs.id()==ID_if)
@@ -1200,7 +1200,7 @@ void value_set_fit::assign_rec(
   assign_recursion_sett &recursion_set)
 {
   #if 0
-  std::cout << "ASSIGN_REC LHS: " << from_expr(ns, "", lhs) << '\n';
+  std::cout << "ASSIGN_REC LHS: " << format(lhs) << '\n';
   std::cout << "ASSIGN_REC SUFFIX: " << suffix << '\n';
 
   for(object_map_dt::const_iterator it=values_rhs.read().begin();
diff --git a/src/pointer-analysis/value_set_fivr.cpp b/src/pointer-analysis/value_set_fivr.cpp
index 8d0ad73e99c..080100829a8 100644
--- a/src/pointer-analysis/value_set_fivr.cpp
+++ b/src/pointer-analysis/value_set_fivr.cpp
@@ -464,7 +464,7 @@ void value_set_fivrt::get_value_set(
   for(std::list<exprt>::const_iterator it=value_set.begin();
       it!=value_set.end();
       it++)
-    std::cout << "GET_VALUE_SET: " << from_expr(ns, "", *it) << '\n';
+    std::cout << "GET_VALUE_SET: " << format(*it) << '\n';
   #endif
 }
 
@@ -881,8 +881,7 @@ void value_set_fivrt::get_reference_set_sharing_rec(
   const namespacet &ns) const
 {
   #if 0
-  std::cout << "GET_REFERENCE_SET_REC EXPR: " << from_expr(ns, "", expr)
-            << '\n';
+  std::cout << "GET_REFERENCE_SET_REC EXPR: " << format(expr) << '\n';
   #endif
 
   if(expr.type().id()=="#REF#")
@@ -956,7 +955,7 @@ void value_set_fivrt::get_reference_set_sharing_rec(
     for(expr_sett::const_iterator it=value_set.begin();
         it!=value_set.end();
         it++)
-      std::cout << "VALUE_SET: " << from_expr(ns, "", *it) << '\n';
+      std::cout << "VALUE_SET: " << format(*it) << '\n';
     #endif
 
     return;
@@ -1077,8 +1076,8 @@ void value_set_fivrt::assign(
 {
   #if 0
   std::cout << "ASSIGN LHS: " << lhs << '\n';
-  std::cout << "ASSIGN LTYPE: " << ns.follow(lhs.type()) << '\n';
-  std::cout << "ASSIGN RHS: " << from_expr(ns, "", rhs) << '\n';
+  std::cout << "ASSIGN LTYPE: " << format(ns.follow(lhs.type())) << '\n';
+  std::cout << "ASSIGN RHS: " << format(rhs) << '\n';
   #endif
 
   if(rhs.id()==ID_if)
diff --git a/src/pointer-analysis/value_set_fivrns.cpp b/src/pointer-analysis/value_set_fivrns.cpp
index c88b352f825..e031f6b0d42 100644
--- a/src/pointer-analysis/value_set_fivrns.cpp
+++ b/src/pointer-analysis/value_set_fivrns.cpp
@@ -277,7 +277,7 @@ void value_set_fivrnst::get_value_set(
   #if 0
   for(std::list<exprt>::const_iterator it=value_set.begin();
       it!=value_set.end(); it++)
-    std::cout << "GET_VALUE_SET: " << from_expr(ns, "", *it) << '\n';
+    std::cout << "GET_VALUE_SET: " << format(*it) << '\n';
   #endif
 }
 
@@ -622,8 +622,7 @@ void value_set_fivrnst::get_reference_set_rec(
   const namespacet &ns) const
 {
   #if 0
-  std::cout << "GET_REFERENCE_SET_REC EXPR: " << from_expr(ns, "", expr)
-            << '\n';
+  std::cout << "GET_REFERENCE_SET_REC EXPR: " << format(expr) << '\n';
   #endif
 
   if(expr.id()==ID_symbol ||
@@ -648,7 +647,7 @@ void value_set_fivrnst::get_reference_set_rec(
     #if 0
     for(expr_sett::const_iterator it=value_set.begin();
         it!=value_set.end(); it++)
-      std::cout << "VALUE_SET: " << from_expr(ns, "", *it) << '\n';
+      std::cout << "VALUE_SET: " << format(*it) << '\n';
     #endif
 
     return;
@@ -769,8 +768,8 @@ void value_set_fivrnst::assign(
 {
   #if 0
   std::cout << "ASSIGN LHS: " << lhs << '\n';
-  std::cout << "ASSIGN LTYPE: " << ns.follow(lhs.type()) << '\n';
-  std::cout << "ASSIGN RHS: " << from_expr(ns, "", rhs) << '\n';
+  std::cout << "ASSIGN LTYPE: " << format(ns.follow(lhs.type())) << '\n';
+  std::cout << "ASSIGN RHS: " << format(rhs) << '\n';
   #endif
 
   if(rhs.id()==ID_if)
diff --git a/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp b/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp
index efba76b4fe0..31071dace29 100644
--- a/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp
+++ b/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp
@@ -59,7 +59,7 @@ SCENARIO(
         const std::regex numbers("\\$[0-9]*");
         for(auto op : code.operands())
         {
-          const std::string line = from_expr(ns, "", op);
+          const std::string line = from_expr(ns, "arg", op);
           code_string.push_back(
             std::regex_replace(
               std::regex_replace(line, spaces, " "), numbers, ""));
diff --git a/unit/java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp b/unit/java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp
index e9eca838d9c..b292e445ae2 100644
--- a/unit/java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp
+++ b/unit/java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp
@@ -62,7 +62,7 @@ TEST_CASE("Convert exprt to string exprt")
         const std::regex numbers("\\$[0-9]*");
         for(auto op : code.operands())
         {
-          const std::string line = from_expr(ns, "", op);
+          const std::string line = from_expr(ns, "a", op);
           code_string.push_back(
             std::regex_replace(
               std::regex_replace(line, spaces, " "), numbers, ""));
diff --git a/unit/miniBDD.cpp b/unit/miniBDD.cpp
index d0eba414184..bd1eb77eec2 100644
--- a/unit/miniBDD.cpp
+++ b/unit/miniBDD.cpp
@@ -9,6 +9,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <iostream>
 
+#include <util/format_expr.h>
+
 #include <solvers/miniBDD/miniBDD.h>
 
 void test1()
@@ -71,8 +73,6 @@ void test3()
 
 void test4()
 {
-  register_language(new_ansi_c_language);
-
   symbol_exprt a("a", bool_typet());
   symbol_exprt b("b", bool_typet());
 
@@ -81,12 +81,12 @@ void test4()
   symbol_tablet symbol_table;
   namespacet ns(symbol_table);
 
-  std::cout << from_expr(ns, "", o) << std::endl;
+  std::cout << format(o) << std::endl;
 
   bdd_exprt t(ns);
   t.from_expr(o);
 
-  std::cout << from_expr(ns, "", t.as_expr()) << std::endl;
+  std::cout << format(t.as_expr()) << std::endl;
 }
 
 int main()
diff --git a/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp b/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp
index 128f5b0a04f..3556cc26915 100644
--- a/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp
+++ b/unit/solvers/refinement/string_constraint_instantiation/instantiate_not_contains.cpp
@@ -135,7 +135,9 @@ std::string create_info(std::vector<exprt> &lemmas, const namespacet &ns)
   for(auto &lemma : lemmas)
   {
     simplify(lemma, ns);
-    new_lemmas+=from_expr(ns, "", lemma)+"\n\n";
+    std::string lemma_string;
+    get_language_from_mode(ID_java)->from_expr(lemma, lemma_string, ns);
+    new_lemmas += lemma_string + "\n\n";
   }
   return "Instantiated lemmas:\n"+new_lemmas;
 }
@@ -163,6 +165,7 @@ SCENARIO("instantiate_not_contains",
 {
   // For printing expression
   register_language(new_java_bytecode_language);
+  std::unique_ptr<languaget> java_lang = get_language_from_mode(ID_java);
   symbol_tablet symtbl;
   const namespacet ns(symtbl);
 
@@ -205,7 +208,9 @@ SCENARIO("instantiate_not_contains",
       axioms,
       [&](const std::string &accu, string_constraintt sc) { // NOLINT
         simplify(sc, ns);
-        return accu + from_expr(ns, "", sc) + "\n\n";
+        std::string s;
+        java_lang->from_expr(sc, s, ns);
+        return accu + s + "\n\n";
       });
 
     const auto nc_contraints = generator.get_not_contains_constraints();
@@ -218,7 +223,9 @@ SCENARIO("instantiate_not_contains",
         simplify(sc, ns);
         generator.witness[sc] = generator.fresh_symbol("w", t.witness_type());
         nc_axioms.push_back(sc);
-        return accu + from_expr(ns, "", sc) + "\n\n";
+        std::string s;
+        java_lang->from_expr(sc, s, ns);
+        return accu + s + "\n\n";
       });
 
     const auto lemmas = generator.get_lemmas();
@@ -228,7 +235,9 @@ SCENARIO("instantiate_not_contains",
       axioms,
       [&](const std::string &accu, exprt axiom) { // NOLINT
         simplify(axiom, ns);
-        return accu + from_expr(ns, "", axiom) + "\n\n";
+        std::string s;
+        java_lang->from_expr(axiom, s, ns);
+        return accu + s + "\n\n";
       });
 
     INFO("Original axioms:\n");
@@ -294,7 +303,9 @@ SCENARIO("instantiate_not_contains",
       generator.fresh_symbol("w", t.witness_type());
 
     INFO("Original axiom:\n");
-    INFO(from_expr(ns, "", vacuous)+"\n\n");
+    std::string s;
+    java_lang->from_expr(vacuous, s, ns);
+    INFO(s + "\n\n");
 
     WHEN("we instantiate and simplify")
     {
@@ -348,7 +359,9 @@ SCENARIO("instantiate_not_contains",
       generator.fresh_symbol("w", t.witness_type());
 
     INFO("Original axiom:\n");
-    INFO(from_expr(ns, "", trivial)+"\n\n");
+    std::string s;
+    java_lang->from_expr(trivial, s, ns);
+    INFO(s + "\n\n");
 
     WHEN("we instantiate and simplify")
     {
@@ -403,7 +416,9 @@ SCENARIO("instantiate_not_contains",
       generator.fresh_symbol("w", t.witness_type());
 
     INFO("Original axiom:\n");
-    INFO(from_expr(ns, "", trivial)+"\n\n");
+    std::string s;
+    java_lang->from_expr(trivial, s, ns);
+    INFO(s + "\n\n");
 
     WHEN("we instantiate and simplify")
     {
@@ -461,7 +476,9 @@ SCENARIO("instantiate_not_contains",
       generator.fresh_symbol("w", t.witness_type());
 
     INFO("Original axiom:\n");
-    INFO(from_expr(ns, "", trivial)+"\n\n");
+    std::string s;
+    java_lang->from_expr(trivial, s, ns);
+    INFO(s + "\n\n");
 
     WHEN("we instantiate and simplify")
     {
@@ -516,7 +533,9 @@ SCENARIO("instantiate_not_contains",
       generator.fresh_symbol("w", t.witness_type());
 
     INFO("Original axiom:\n");
-    INFO(from_expr(ns, "", trivial)+"\n\n");
+    std::string s;
+    java_lang->from_expr(trivial, s, ns);
+    INFO(s + "\n\n");
 
     WHEN("we instantiate and simplify")
     {