associativity of plus

Author: kroening

regression/cbmc/Associativity1/main.c

@@ -0,0 +1,11 @@
+#include <assert.h>
+
+int main (void) {
+	int x;
+
+	while ((x + 1) -x != 1) {
+		assert(0);
+	}
+
+	return 0;
+}

regression/cbmc/Associativity1/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring

src/util/simplify_expr_int.cpp

@@ -527,7 +527,7 @@ bool simplify_exprt::simplify_minus(exprt &expr)
     simplify_unary_minus(tmp2);
 
     plus_exprt tmp(operands[0], tmp2);
-    simplify_plus(tmp);
+    simplify_node(tmp);
 
     expr.swap(tmp);
     return false;