Remove "no-overflow-mult" expression

Author: danpoe

src/solvers/flattening/boolbv.cpp

@@ -224,9 +224,8 @@ bvt boolbvt::convert_bitvector(const exprt &expr)
           expr.id()=="no-overflow-plus" ||
           expr.id()=="no-overflow-minus")
     return convert_add_sub(expr);
-  else if(expr.id()==ID_mult ||
-          expr.id()=="no-overflow-mult")
-    return convert_mult(expr);
+  else if(expr.id() == ID_mult)
+    return convert_mult(to_mult_expr(expr));
   else if(expr.id()==ID_div)
     return convert_div(to_div_expr(expr));
   else if(expr.id()==ID_mod)

src/solvers/flattening/boolbv.h

@@ -152,7 +152,7 @@ class boolbvt:public arrayst
   virtual bvt convert_union(const union_exprt &expr);
   virtual bvt convert_bv_typecast(const typecast_exprt &expr);
   virtual bvt convert_add_sub(const exprt &expr);
-  virtual bvt convert_mult(const exprt &expr);
+  virtual bvt convert_mult(const mult_exprt &expr);
   virtual bvt convert_div(const div_exprt &expr);
   virtual bvt convert_mod(const mod_exprt &expr);
   virtual bvt convert_floatbv_op(const exprt &expr);

src/solvers/flattening/boolbv_mult.cpp

@@ -10,10 +10,8 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/std_types.h>
 
-bvt boolbvt::convert_mult(const exprt &expr)
+bvt boolbvt::convert_mult(const mult_exprt &expr)
 {
-  PRECONDITION(expr.id() == ID_mult || expr.id() == "no-overflow-mult");
-
   std::size_t width=boolbv_width(expr.type());
 
   if(width==0)
@@ -27,8 +25,6 @@ bvt boolbvt::convert_mult(const exprt &expr)
 
   const exprt &op0=expr.op0();
 
-  bool no_overflow=expr.id()=="no-overflow-mult";
-
   DATA_INVARIANT(
     op0.type() == expr.type(),
     "multiplication operands should have same type as expression");
@@ -80,10 +76,7 @@ bvt boolbvt::convert_mult(const exprt &expr)
 
       const bvt &op = convert_bv(*it, width);
 
-      if(no_overflow)
-        bv=bv_utils.multiplier_no_overflow(bv, op, rep);
-      else
-        bv=bv_utils.multiplier(bv, op, rep);
+      bv = bv_utils.multiplier(bv, op, rep);
     }
 
     return bv;

src/solvers/refinement/bv_refinement.h

@@ -51,7 +51,7 @@ class bv_refinementt:public bv_pointerst
   void post_process_arrays() override;
 
   // Refine arithmetic
-  bvt convert_mult(const exprt &expr) override;
+  bvt convert_mult(const mult_exprt &expr) override;
   bvt convert_div(const div_exprt &expr) override;
   bvt convert_mod(const mod_exprt &expr) override;
   bvt convert_floatbv_op(const exprt &expr) override;

src/solvers/refinement/refine_arithmetic.cpp

@@ -50,7 +50,7 @@ bvt bv_refinementt::convert_floatbv_op(const exprt &expr)
   return bv;
 }
 
-bvt bv_refinementt::convert_mult(const exprt &expr)
+bvt bv_refinementt::convert_mult(const mult_exprt &expr)
 {
   if(!config_.refine_arithmetic || expr.type().id()==ID_fixedbv)
     return SUB::convert_mult(expr);
@@ -65,7 +65,7 @@ bvt bv_refinementt::convert_mult(const exprt &expr)
   PRECONDITION(operands.size()>=2);
 
   if(operands.size()>2)
-    return convert_mult(make_binary(expr)); // make binary
+    return convert_mult(to_mult_expr(make_binary(expr))); // make binary
 
   // we keep multiplication by a constant for integers
   if(type.id()!=ID_floatbv)