Refactor simplify_minus

* Use to_minus_expr instead of asserting the expression id
* Rename the local variables for easier readability

Author: hannes-steffenhagen-diffblue

src/util/simplify_expr_int.cpp

@@ -604,43 +604,42 @@ bool simplify_exprt::simplify_plus(exprt &expr)
 
 bool simplify_exprt::simplify_minus(exprt &expr)
 {
+  auto const &minus_expr = to_minus_expr(expr);
   if(!is_number(expr.type()) &&
      expr.type().id()!=ID_pointer)
     return true;
 
-  exprt::operandst &operands=expr.operands();
-
-  assert(expr.id()==ID_minus);
+  const exprt::operandst &operands = minus_expr.operands();
 
   if(operands.size()!=2)
     return true;
 
-  if(is_number(expr.type()) &&
-     is_number(operands[0].type()) &&
-     is_number(operands[1].type()))
+  if(
+    is_number(minus_expr.type()) && is_number(operands[0].type()) &&
+    is_number(operands[1].type()))
   {
     // rewrite "a-b" to "a+(-b)"
-    unary_minus_exprt tmp2(operands[1]);
-    simplify_unary_minus(tmp2);
+    unary_minus_exprt rhs_negated(operands[1]);
+    simplify_unary_minus(rhs_negated);
 
-    plus_exprt tmp(operands[0], tmp2);
-    simplify_node(tmp);
+    plus_exprt plus_expr(operands[0], rhs_negated);
+    simplify_node(plus_expr);
 
-    expr.swap(tmp);
+    expr.swap(plus_expr);
     return false;
   }
   else if(expr.type().id()==ID_pointer &&
           operands[0].type().id()==ID_pointer &&
           is_number(operands[1].type()))
   {
     // pointer arithmetic: rewrite "p-i" to "p+(-i)"
-    unary_minus_exprt tmp2(operands[1]);
-    simplify_unary_minus(tmp2);
+    unary_minus_exprt negated_pointer_offset(operands[1]);
+    simplify_unary_minus(negated_pointer_offset);
 
-    plus_exprt tmp(operands[0], tmp2);
-    simplify_plus(tmp);
+    plus_exprt pointer_offset_expr(operands[0], negated_pointer_offset);
+    simplify_plus(pointer_offset_expr);
 
-    expr.swap(tmp);
+    expr.swap(pointer_offset_expr);
     return false;
   }
   else if(is_number(expr.type()) &&