Add relational operators in assume context regression tests

Author: NlightNFotis

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

@@ -0,0 +1,27 @@
+#include <stdlib.h>
+
+int main()
+{
+  int x;
+  int *y = &x;
+  int *z = &x;
+
+  if(x)
+  {
+    y++;
+  }
+  else
+  {
+    z++;
+  }
+
+  __CPROVER_assume(y >= z);
+  __CPROVER_assert(x != y, "x != y: expected successful");
+  __CPROVER_assert(x == y, "x == y: expected failure");
+
+  __CPROVER_assume(z >= x);
+
+  __CPROVER_assert(z >= x, "z >= x: expected successful");
+  __CPROVER_assert(z <= y, "z <= y: expected successful");
+  __CPROVER_assert(z <= x, "z <= x: expected failure");
+}

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

@@ -0,0 +1,14 @@
+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
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+This is testing basic pointer relational operator support for three objects
+defined in the function's stack frame.