Replace throws with invariants in boolbv_equality

Author: hannes-steffenhagen-diffblue

src/solvers/flattening/boolbv_equality.cpp

@@ -19,13 +19,11 @@ literalt boolbvt::convert_equality(const equal_exprt &expr)
 {
   const bool is_base_type_eq =
     base_type_eq(expr.lhs().type(), expr.rhs().type(), ns);
-  if(!is_base_type_eq)
-  {
-    const std::string error_msg =
-      std::string("equality without matching types:\n") + "######### lhs: " +
-      expr.lhs().pretty() + '\n' + "######### rhs: " + expr.rhs().pretty();
-    throw bitvector_conversion_exceptiont(error_msg, expr);
-  }
+  DATA_INVARIANT_WITH_DIAGNOSTICS(
+    is_base_type_eq,
+    "types of expressions on each side of equality should match",
+    irep_pretty_diagnosticst{expr.lhs()},
+    irep_pretty_diagnosticst{expr.rhs()});
 
   // see if it is an unbounded array
   if(is_unbounded_array(expr.lhs().type()))
@@ -44,12 +42,13 @@ literalt boolbvt::convert_equality(const equal_exprt &expr)
   const bvt &lhs_bv = convert_bv(expr.lhs());
   const bvt &rhs_bv = convert_bv(expr.rhs());
 
-  DATA_INVARIANT(
+  DATA_INVARIANT_WITH_DIAGNOSTICS(
     lhs_bv.size() == rhs_bv.size(),
-    std::string("unexpected size mismatch on equality:\n") +
-      "lhs: " + expr.lhs().pretty() + '\n' + "lhs size: " +
-      std::to_string(lhs_bv.size()) + '\n' + "rhs: " + expr.rhs().pretty() +
-      '\n' + "rhs size: " + std::to_string(rhs_bv.size()));
+    "sizes of lhs and rhs bitvectors should match",
+    irep_pretty_diagnosticst{expr.lhs()},
+    "lhs size: " + std::to_string(lhs_bv.size()),
+    irep_pretty_diagnosticst{expr.rhs()},
+    "rhs size: " + std::to_string(rhs_bv.size()));
 
   if(lhs_bv.empty())
   {
@@ -69,21 +68,22 @@ literalt boolbvt::convert_verilog_case_equality(
 
   const bool is_base_type_eq =
     base_type_eq(expr.lhs().type(), expr.rhs().type(), ns);
-  DATA_INVARIANT(
+  DATA_INVARIANT_WITH_DIAGNOSTICS(
     is_base_type_eq,
-    std::string("verilog_case_equality without matching types:\n") +
-      "######### lhs: " + expr.lhs().pretty() + '\n' +
-      "######### rhs: " + expr.rhs().pretty());
+    "lhs and rhs types should match in verilog_case_equality",
+    irep_pretty_diagnosticst{expr.lhs()},
+    irep_pretty_diagnosticst{expr.rhs()});
 
   const bvt &lhs_bv = convert_bv(expr.lhs());
   const bvt &rhs_bv = convert_bv(expr.rhs());
 
-  DATA_INVARIANT(
+  DATA_INVARIANT_WITH_DIAGNOSTICS(
     lhs_bv.size() == rhs_bv.size(),
-    std::string("unexpected size mismatch on verilog_case_equality:\n") +
-      "lhs: " + expr.lhs().pretty() + '\n' + "lhs size: " +
-      std::to_string(lhs_bv.size()) + '\n' + "rhs: " + expr.rhs().pretty() +
-      '\n' + "rhs size: " + std::to_string(rhs_bv.size()));
+    "bitvector arguments to verilog_case_equality should have the same size",
+    irep_pretty_diagnosticst{expr.lhs()},
+    "lhs size: " + std::to_string(lhs_bv.size()),
+    irep_pretty_diagnosticst{expr.rhs()},
+    "rhs size: " + std::to_string(rhs_bv.size()));
 
   if(expr.id()==ID_verilog_case_inequality)
     return !bv_utils.equal(lhs_bv, rhs_bv);