diff --git a/src/cbmc/show_vcc.cpp b/src/cbmc/show_vcc.cpp
index 6a5b051cff9..b50eb3df2f6 100644
--- a/src/cbmc/show_vcc.cpp
+++ b/src/cbmc/show_vcc.cpp
@@ -22,9 +22,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 void bmct::show_vcc_plain(std::ostream &out)
 {
-  out << "\n" << "VERIFICATION CONDITIONS:" << "\n" << "\n";
-
   bool has_threads=equation.has_threads();
+  bool first=true;
 
   for(symex_target_equationt::SSA_stepst::iterator
       s_it=equation.SSA_steps.begin();
@@ -34,6 +33,11 @@ void bmct::show_vcc_plain(std::ostream &out)
     if(!s_it->is_assert())
       continue;
 
+    if(first)
+      first=false;
+    else
+      out << '\n';
+
     if(s_it->source.pc->source_location.is_not_nil())
       out << s_it->source.pc->source_location << "\n";
 
@@ -66,13 +70,14 @@ void bmct::show_vcc_plain(std::ostream &out)
         }
       }
 
-    out << "|--------------------------" << "\n";
+    // Unicode equivalent of "|--------------------------"
+    out << u8"\u251c";
+    for(unsigned i=0; i<26; i++) out << u8"\u2500";
+    out << '\n';
 
     std::string string_value=
       from_expr(ns, s_it->source.pc->function, s_it->cond_expr);
     out << "{" << 1 << "} " << string_value << "\n";
-
-    out << "\n";
   }
 }
 
@@ -159,7 +164,14 @@ void bmct::show_vcc()
     break;
 
   case ui_message_handlert::uit::PLAIN:
-    show_vcc_plain(out);
+    status() << "VERIFICATION CONDITIONS:\n" << eom;
+    if(have_file)
+      show_vcc_plain(out);
+    else
+    {
+      show_vcc_plain(status());
+      status() << eom;
+    }
     break;
   }
 
diff --git a/src/util/format_expr.cpp b/src/util/format_expr.cpp
index 0007306c264..7b087990324 100644
--- a/src/util/format_expr.cpp
+++ b/src/util/format_expr.cpp
@@ -62,6 +62,27 @@ static std::ostream &format_rec(std::ostream &os, const multi_ary_exprt &src)
 {
   bool first = true;
 
+  std::string operator_str;
+
+  if(src.id() == ID_and)
+    operator_str = u8"\u2227"; // wedge, U+2227
+  else if(src.id() == ID_or)
+    operator_str = u8"\u2228"; // vee, U+2228
+  else if(src.id() == ID_xor)
+    operator_str = u8"\u2295"; // + in circle, U+2295
+  else if(src.id() == ID_le)
+    operator_str = u8"\u2264"; // <=, U+2264
+  else if(src.id() == ID_ge)
+    operator_str = u8"\u2265"; // >=, U+2265
+  else if(src.id() == ID_notequal)
+    operator_str = u8"\u2260"; // /=, U+2260
+  else if(src.id() == ID_implies)
+    operator_str = u8"\u21d2"; // =>, U+21D2
+  else if(src.id() == ID_iff)
+    operator_str = u8"\u21d4"; // <=>, U+21D4
+  else
+    operator_str = id2string(src.id());
+
   for(const auto &op : src.operands())
   {
     if(first)
@@ -95,7 +116,7 @@ static std::ostream &format_rec(std::ostream &os, const binary_exprt &src)
 static std::ostream &format_rec(std::ostream &os, const unary_exprt &src)
 {
   if(src.id() == ID_not)
-    os << '!';
+    os << u8"\u00ac"; // neg, U+00AC
   else if(src.id() == ID_unary_minus)
     os << '-';
   else
@@ -197,8 +218,12 @@ std::ostream &format_rec(std::ostream &os, const exprt &expr)
   }
   else if(id == ID_type)
     return format_rec(os, expr.type());
-  else if(id == ID_forall || id == ID_exists)
-    return os << id << ' ' << format(to_quantifier_expr(expr).symbol()) << " : "
+  else if(id == ID_forall)
+    return os << id << u8" \u2200 : "
+              << format(to_quantifier_expr(expr).symbol().type()) << " . "
+              << format(to_quantifier_expr(expr).where());
+  else if(id == ID_exists)
+    return os << id << u8" \u2203 : "
               << format(to_quantifier_expr(expr).symbol().type()) << " . "
               << format(to_quantifier_expr(expr).where());
   else if(id == ID_let)