Merge pull request #3043 from hannes-steffenhagen-diffblue/feature-invariant_cleanup-flattening-if

Use expected_width parameter in flattening/boolbv_if to simplify error handling

Author: NlightNFotis

src/solvers/flattening/boolbv_if.cpp

@@ -18,11 +18,8 @@ bvt boolbvt::convert_if(const if_exprt &expr)
 
   literalt cond=convert(expr.cond());
 
-  const bvt &op1_bv=convert_bv(expr.true_case());
-  const bvt &op2_bv=convert_bv(expr.false_case());
+  const bvt &true_case_bv = convert_bv(expr.true_case(), width);
+  const bvt &false_case_bv = convert_bv(expr.false_case(), width);
 
-  if(op1_bv.size()!=width || op2_bv.size()!=width)
-    throw "operand size mismatch for if "+expr.pretty();
-
-  return bv_utils.select(cond, op1_bv, op2_bv);
+  return bv_utils.select(cond, true_case_bv, false_case_bv);
 }