cbmc-incr-smt2 tests: remove misguided assertion

There is no reason an integer couldn't have the same value as a pointer
(when converted to an integer type). This assertion might accidentally
hold on platforms where sizeof(int) != sizeof(int *) given our current
pointer model, but this is an implementation detail that we must not
rely on. The assertion certainly doesn't hold when sizeof(int) ==
sizeof(int *).

Author: tautschnig

regression/cbmc-incr-smt2/pointers-relational-operators/pointers_assume.c

@@ -16,7 +16,6 @@ int main()
   }
 
   __CPROVER_assume(y >= z);
-  __CPROVER_assert(x != y, "x != y: expected successful");
   __CPROVER_assert(x == y, "x == y: expected failure");
 
   __CPROVER_assume(z >= x);

regression/cbmc-incr-smt2/pointers-relational-operators/pointers_assume.desc

@@ -1,11 +1,10 @@
 CORE
 pointers_assume.c
 --trace
-\[main\.assertion\.1\] line \d+ x != y: expected successful: SUCCESS
-\[main\.assertion\.2\] line \d+ x == y: expected failure: FAILURE
-\[main\.assertion\.3\] line \d+ z >= x: expected successful: SUCCESS
-\[main\.assertion\.4\] line \d+ z <= y: expected successful: SUCCESS
-\[main\.assertion\.5\] line \d+ z <= x: expected failure: FAILURE
+\[main\.assertion\.1\] line \d+ x == y: expected failure: FAILURE
+\[main\.assertion\.2\] line \d+ z >= x: expected successful: SUCCESS
+\[main\.assertion\.3\] line \d+ z <= y: expected successful: SUCCESS
+\[main\.assertion\.4\] line \d+ z <= x: expected failure: FAILURE
 ^EXIT=10$
 ^SIGNAL=0$
 --