Simplifier: in pointer-typed (a + b) + c the pointer may be c

The rewrite tries to combine the integer-typed operands; if c is the pointer,
then (a + b) is already of the right form and no changes are needed.

Author: tautschnig

regression/cbmc/Pointer_Arithmetic15/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 
 ^EXIT=10$
@@ -7,5 +7,5 @@ main.c
 --
 ^warning: ignoring
 --
-Symbolic execution currently messes up the typing in "p = a + b + p;" making the
+The simplifier previously messed up the typing in "p = a + b + p;" making the
 right-hand side signed long rather than a pointer.

src/util/simplify_expr_int.cpp

@@ -479,6 +479,7 @@ bool simplify_exprt::simplify_plus(exprt &expr)
     if(expr.type().id()==ID_pointer &&
        expr.operands().size()==2 &&
        expr.op0().id()==ID_plus &&
+       expr.op0().type().id() == ID_pointer &&
        expr.op0().operands().size()==2)
     {
       exprt op0=expr.op0();