Fully simplify (in)equalities over constants+if

The case of constant-on-lhs together with an if-expression on the
right-hand side previously required multiple simplification passes as
the constant-on-both-sides case was not considered for this case.

Author: tautschnig

src/util/simplify_expr_int.cpp

@@ -1550,10 +1550,10 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality_rhs_is_constant(
   if(expr.op0().id()==ID_if && expr.op0().operands().size()==3)
   {
     if_exprt if_expr=lift_if(expr, 0);
-    if_expr.true_case() = simplify_inequality_rhs_is_constant(
-      to_binary_relation_expr(if_expr.true_case()));
-    if_expr.false_case() = simplify_inequality_rhs_is_constant(
-      to_binary_relation_expr(if_expr.false_case()));
+    if_expr.true_case() =
+      simplify_inequality(to_binary_relation_expr(if_expr.true_case()));
+    if_expr.false_case() =
+      simplify_inequality(to_binary_relation_expr(if_expr.false_case()));
     return changed(simplify_if(if_expr));
   }
 

unit/util/simplify_expr.cpp

@@ -516,3 +516,27 @@ TEST_CASE("Simplify bitor", "[core][util]")
     REQUIRE(simplify_expr(bitor_exprt{b, zero}, ns) == b);
   }
 }
+
+TEST_CASE("Simplify inequality", "[core][util]")
+{
+  symbol_tablet symbol_table;
+  namespacet ns(symbol_table);
+
+  {
+    // This checks that 3 < (B ? 4 : 5) simplifies to true, just like (B ? 4 :
+    // 5) > 3 simplifies to true.
+    signedbv_typet sbv{4};
+    symbol_exprt b{"B", bool_typet{}};
+    if_exprt if_b{b, from_integer(4, sbv), from_integer(5, sbv)};
+
+    binary_relation_exprt comparison_gt{if_b, ID_gt, from_integer(3, sbv)};
+    exprt simp = simplify_expr(comparison_gt, ns);
+
+    REQUIRE(simp == true_exprt{});
+
+    binary_relation_exprt comparison_lt{from_integer(3, sbv), ID_lt, if_b};
+    simp = simplify_expr(comparison_lt, ns);
+
+    REQUIRE(simp == true_exprt{});
+  }
+}