Replace throw with invariant in boolbv_if

Author: hannes-steffenhagen-diffblue

src/solvers/flattening/boolbv_if.cpp

@@ -21,8 +21,11 @@ bvt boolbvt::convert_if(const if_exprt &expr)
   const bvt &true_case_bv = convert_bv(expr.true_case());
   const bvt &false_case_bv = convert_bv(expr.false_case());
 
-  if(true_case_bv.size() != width || false_case_bv.size() != width)
-    throw "operand size mismatch for if "+expr.pretty();
+  DATA_INVARIANT_WITH_DIAGNOSTICS(
+    true_case_bv.size() == width && false_case_bv.size() == width,
+    "both branches of an if statement have to return bit vectors of the same "
+    "width",
+    irep_pretty_diagnosticst{expr});
 
   return bv_utils.select(cond, true_case_bv, false_case_bv);
 }