Add a simple test for the conversion of pointer arithmetic/subtraction.

This works without any changes to our conversion of `minus_exprt`s because
there's a transformation between the frontend and the backend that converts
a (*a - 3) to (*a + (-3)).

Author: NlightNFotis

regression/cbmc-incr-smt2/pointer_arithmetic/subtraction_simple.c

@@ -0,0 +1,12 @@
+#define NULL (void *)0
+
+int main()
+{
+  int *x;
+  int *y = x - 2;
+  __CPROVER_assume(x != NULL);
+  __CPROVER_assume(y != NULL);
+
+  __CPROVER_assert(y == x, "expected failure after pointer manipulation");
+  __CPROVER_assert(y != x, "expected successful after pointer manipulation");
+}

regression/cbmc-incr-smt2/pointer_arithmetic/subtraction_simple.desc

@@ -0,0 +1,11 @@
+CORE
+subtraction_simple.c
+--trace
+\[main\.assertion\.1\] line \d+ expected failure after pointer manipulation: FAILURE
+\[main\.assertion\.2\] line \d+ expected successful after pointer manipulation: SUCCESS
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+This test is similar to the one in `addition_simple.desc`, but testing end-to-end
+the conversion of a subtraction case of pointer arithmetic.