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.

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

@@ -472,7 +472,9 @@ bool simplify_exprt::simplify_plus(exprt &expr)
     // ((T*)p+a)+b -> (T*)p+(a+b)
     if(
       plus_expr.type().id() == ID_pointer && plus_expr.operands().size() == 2 &&
-      plus_expr.op0().id() == ID_plus && plus_expr.op0().operands().size() == 2)
+      plus_expr.op0().id() == ID_plus &&
+      plus_expr.op0().type().id() == ID_pointer &&
+      plus_expr.op0().operands().size() == 2)
     {
       exprt op0 = plus_expr.op0();