Remove "no-overflow-unary-minus" expressions

Author: danpoe

src/solvers/flattening/boolbv.cpp

@@ -251,9 +251,8 @@ bvt boolbvt::convert_bitvector(const exprt &expr)
           expr.id()==ID_bitxnor || expr.id()==ID_bitnor ||
           expr.id()==ID_bitnand)
     return convert_bitwise(expr);
-  else if(expr.id()==ID_unary_minus ||
-          expr.id()=="no-overflow-unary-minus")
-    return convert_unary_minus(to_unary_expr(expr));
+  else if(expr.id() == ID_unary_minus)
+    return convert_unary_minus(to_unary_minus_expr(expr));
   else if(expr.id()==ID_unary_plus)
   {
     return convert_bitvector(to_unary_plus_expr(expr).op());

src/solvers/flattening/boolbv.h

@@ -164,7 +164,7 @@ class boolbvt:public arrayst
   virtual bvt convert_cond(const exprt &expr);
   virtual bvt convert_shift(const binary_exprt &expr);
   virtual bvt convert_bitwise(const exprt &expr);
-  virtual bvt convert_unary_minus(const unary_exprt &expr);
+  virtual bvt convert_unary_minus(const unary_minus_exprt &expr);
   virtual bvt convert_abs(const abs_exprt &expr);
   virtual bvt convert_concatenation(const exprt &expr);
   virtual bvt convert_replication(const replication_exprt &expr);

src/solvers/flattening/boolbv_unary_minus.cpp

@@ -17,7 +17,7 @@ Author: Daniel Kroening, [email protected]
 
 #include "boolbv_type.h"
 
-bvt boolbvt::convert_unary_minus(const unary_exprt &expr)
+bvt boolbvt::convert_unary_minus(const unary_minus_exprt &expr)
 {
   const typet &type=ns.follow(expr.type());
 
@@ -33,8 +33,6 @@ bvt boolbvt::convert_unary_minus(const unary_exprt &expr)
   bvtypet bvtype=get_bvtype(type);
   bvtypet op_bvtype = get_bvtype(op.type());
 
-  bool no_overflow=(expr.id()=="no-overflow-unary-minus");
-
   if(bvtype==bvtypet::IS_UNKNOWN &&
      (type.id()==ID_vector || type.id()==ID_complex))
   {
@@ -79,27 +77,17 @@ bvt boolbvt::convert_unary_minus(const unary_exprt &expr)
   }
   else if(bvtype==bvtypet::IS_FIXED && op_bvtype==bvtypet::IS_FIXED)
   {
-    if(no_overflow)
-      return bv_utils.negate_no_overflow(op_bv);
-    else
-      return bv_utils.negate(op_bv);
+    return bv_utils.negate(op_bv);
   }
   else if(bvtype==bvtypet::IS_FLOAT && op_bvtype==bvtypet::IS_FLOAT)
   {
-    INVARIANT(!no_overflow, "");
     float_utilst float_utils(prop, to_floatbv_type(expr.type()));
     return float_utils.negate(op_bv);
   }
   else if((op_bvtype==bvtypet::IS_SIGNED || op_bvtype==bvtypet::IS_UNSIGNED) &&
           (bvtype==bvtypet::IS_SIGNED || bvtype==bvtypet::IS_UNSIGNED))
   {
-    if(no_overflow)
-      prop.l_set_to(bv_utils.overflow_negate(op_bv), false);
-
-    if(no_overflow)
-      return bv_utils.negate_no_overflow(op_bv);
-    else
-      return bv_utils.negate(op_bv);
+    return bv_utils.negate(op_bv);
   }
 
   return conversion_failed(expr);