format_expr: equality on booleans is now shown as 'iff'

This makes the output closer to usual mathematical convention.

Author: Daniel Kroening

src/util/format_expr.cpp

@@ -78,6 +78,13 @@ static std::ostream &format_rec(std::ostream &os, const multi_ary_exprt &src)
     operator_str = u8"\u2260"; // /=, U+2260
   else if(src.id() == ID_implies)
     operator_str = u8"\u21d2"; // =>, U+21D2
+  else if(src.id() == ID_equal)
+  {
+    if(!src.operands().empty() && src.op0().type().id() == ID_bool)
+      operator_str = u8"\u21d4"; // <=>, U+21D4
+    else
+      operator_str = "=";
+  }
   else
     operator_str = id2string(src.id());