format_expr: show quantified symbol in forall/exists

This makes the output closer to usual mathematical convention.

Author: Daniel Kroening

src/util/format_expr.cpp

@@ -219,13 +219,13 @@ 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)
-    return os << id << u8" \u2200 : "
-              << format(to_quantifier_expr(expr).symbol().type()) << " . "
-              << format(to_quantifier_expr(expr).where());
+    return os << u8"\u2200 " << format(to_quantifier_expr(expr).symbol())
+              << " : " << 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());
+    return os << u8"\u2203 " << format(to_quantifier_expr(expr).symbol())
+              << " : " << format(to_quantifier_expr(expr).symbol().type())
+              << " . " << format(to_quantifier_expr(expr).where());
   else if(id == ID_let)
     return os << "LET " << format(to_let_expr(expr).symbol()) << " = "
               << format(to_let_expr(expr).value()) << " IN "