format_expr: +, -, *, / bind stronger than ==, !=, <, <=, >, >=

Author: Daniel Kroening

regression/cbmc/show-vcc/main_prec.c

@@ -0,0 +1,8 @@
+int main()
+{
+  __CPROVER_bool a, b, c;
+  int x, y, z;
+  x = y + z;
+  a = (b == c);
+  __CPROVER_assert(0, "some property");
+}

regression/cbmc/show-vcc/main_prec.desc

@@ -0,0 +1,9 @@
+CORE
+main_prec.c
+--show-vcc
+^EXIT=0$
+^SIGNAL=0$
+^some property$
+^\{-.*\} main::1::x!0@1#2 = main::1::y!0@1#1 \+ main::1::z!0@1#1$
+^\{-.*\} main::1::a!0@1#2 ⇔ \(main::1::b!0@1#1 ⇔ main::1::c!0@1#1\)$
+--

src/util/format_expr.cpp

@@ -77,6 +77,16 @@ static bool bracket_subexpression(const exprt &sub_expr, const exprt &expr)
     (expr.id() == ID_and || expr.id() == ID_or))
     return false;
 
+  // +, -, *, / bind stronger than ==, !=, <, <=, >, >=
+  if(
+    (sub_expr.id() == ID_plus || sub_expr.id() == ID_minus ||
+     sub_expr.id() == ID_mult || sub_expr.id() == ID_div) &&
+    (expr.id() == ID_equal || expr.id() == ID_notequal || expr.id() == ID_lt ||
+     expr.id() == ID_gt || expr.id() == ID_le || expr.id() == ID_ge))
+  {
+    return false;
+  }
+
   return true;
 }