make_and simplifies trivial expressions

This is to avoid generating expressions like TRUE && TRUE

Author: romainbrenguier

src/util/expr_util.cpp

@@ -292,6 +292,19 @@ constant_exprt make_boolean_expr(bool value)
 
 exprt make_and(exprt a, exprt b)
 {
+  PRECONDITION(a.type().id() == ID_bool && b.type().id() == ID_bool);
+  if(b.is_constant())
+  {
+    if(b.get(ID_value) == ID_false)
+      return false_exprt{};
+    return a;
+  }
+  if(a.is_constant())
+  {
+    if(a.get(ID_value) == ID_false)
+      return false_exprt{};
+    return b;
+  }
   if(b.id() == ID_and)
   {
     b.add_to_operands(std::move(a));

src/util/expr_util.h

@@ -101,7 +101,8 @@ class is_constantt
 constant_exprt make_boolean_expr(bool);
 
 /// Conjunction of two expressions. If the second is already an `and_exprt`
-/// add to its operands instead of creating a new expression.
+/// add to its operands instead of creating a new expression. If one is `true`,
+/// return the other expression. If one is `false` returns `false`.
 exprt make_and(exprt a, exprt b);
 
 #endif // CPROVER_UTIL_EXPR_UTIL_H