Use unary_minus_overflow_exprt

Author: thomasspriggs

src/ansi-c/c_typecheck_expr.cpp

@@ -3161,7 +3161,7 @@ exprt c_typecheck_baset::do_special_functions(
 
     typecheck_expr_unary_arithmetic(tmp);
 
-    unary_overflow_exprt overflow{ID_unary_minus, tmp.operands().front()};
+    unary_minus_overflow_exprt overflow{tmp.operands().front()};
     overflow.add_source_location() = tmp.source_location();
     return std::move(overflow);
   }

src/ansi-c/expr2c.cpp

@@ -3921,7 +3921,7 @@ std::string expr2ct::convert_with_precedence(
     return convert_cond(src, precedence);
 
   else if(
-    src.id() == ID_overflow_unary_minus ||
+    can_cast_expr<unary_minus_overflow_exprt>(src) ||
     can_cast_expr<binary_overflow_exprt>(src))
   {
     return convert_overflow(src, precedence);

src/ansi-c/goto_check_c.cpp

@@ -1052,7 +1052,7 @@ void goto_check_ct::integer_overflow_check(
     std::string kind = type.id() == ID_unsignedbv ? "unsigned" : "signed";
 
     add_guarded_property(
-      not_exprt{unary_overflow_exprt{expr.id(), to_unary_expr(expr).op()}},
+      not_exprt{unary_minus_overflow_exprt{to_unary_expr(expr).op()}},
       "arithmetic overflow on " + kind + " " + expr.id_string(),
       "overflow",
       expr.find_source_location(),

src/solvers/flattening/boolbv.cpp

@@ -418,7 +418,7 @@ literalt boolbvt::convert_rest(const exprt &expr)
     return convert_onehot(to_unary_expr(expr));
   else if(
     can_cast_expr<binary_overflow_exprt>(expr) ||
-    expr.id() == ID_overflow_unary_minus)
+    can_cast_expr<unary_minus_overflow_exprt>(expr))
   {
     return convert_overflow(expr);
   }

src/solvers/flattening/boolbv_overflow.cpp

@@ -161,11 +161,11 @@ literalt boolbvt::convert_overflow(const exprt &expr)
     return
       prop.land(!neg_shift, prop.lselect(undef, prop.lor(bv0), overflow));
   }
-  else if(expr.id()==ID_overflow_unary_minus)
+  else if(
+    const auto unary_minus_overflow =
+      expr_try_dynamic_cast<unary_minus_overflow_exprt>(expr))
   {
-    const auto &overflow_expr = to_unary_expr(expr);
-
-    const bvt &bv = convert_bv(overflow_expr.op());
+    const bvt &bv = convert_bv(unary_minus_overflow->op());
 
     return bv_utils.overflow_negate(bv);
   }

src/util/simplify_expr.cpp

@@ -2278,7 +2278,7 @@ simplify_exprt::simplify_overflow_unary(const unary_overflow_exprt &expr)
     return unchanged(expr);
 
   mp_integer no_overflow_result;
-  if(expr.id() == ID_overflow_unary_minus)
+  if(can_cast_expr<unary_minus_overflow_exprt>(expr))
     no_overflow_result = -*op_value;
   else
     UNREACHABLE;
@@ -2552,9 +2552,11 @@ simplify_exprt::resultt<> simplify_exprt::simplify_node(exprt node)
   {
     r = simplify_overflow_binary(*binary_overflow);
   }
-  else if(expr.id() == ID_overflow_unary_minus)
+  else if(
+    const auto unary_overflow =
+      expr_try_dynamic_cast<unary_overflow_exprt>(expr))
   {
-    r = simplify_overflow_unary(to_unary_overflow_expr(expr));
+    r = simplify_overflow_unary(*unary_overflow);
   }
   else if(expr.id() == ID_bitreverse)
   {