Merge pull request #5891 from tautschnig/fix-simplify-bitor

Simplify bitor/bitxor with ID_bv-typed zero operand

Author: kroening

src/util/simplify_expr_int.cpp

@@ -715,6 +715,14 @@ simplify_exprt::simplify_bitwise(const multi_ary_exprt &expr)
         it = new_expr.operands().erase(it);
         no_change = false;
       }
+      else if(
+        it->is_constant() && it->type().id() == ID_bv &&
+        to_constant_expr(*it).value_is_zero_string() &&
+        new_expr.operands().size() > 1)
+      {
+        it = new_expr.operands().erase(it);
+        no_change = false;
+      }
       else
         it++;
     }

unit/util/simplify_expr.cpp

@@ -501,3 +501,18 @@ TEST_CASE("Simplifying cast expressions", "[core][util]")
     REQUIRE(simplified_expr == expr);
   }
 }
+
+TEST_CASE("Simplify bitor", "[core][util]")
+{
+  const symbol_tablet symbol_table;
+  const namespacet ns(symbol_table);
+
+  SECTION("Simplification for raw bitvector")
+  {
+    bv_typet bv{4};
+    constant_exprt zero = from_integer(0, bv);
+    symbol_exprt b{"B", bv};
+
+    REQUIRE(simplify_expr(bitor_exprt{b, zero}, ns) == b);
+  }
+}