Pointer subtraction was fixed in 3acdb52

The invariant failure was caused by a bug in handling pointer
subtraction, which was fixed in 3acdb52. The test also wrongly assumed
verification would succeed, which is not correct for `*p`, which is out
of bounds.

Fixes: #5328

Author: tautschnig

regression/cbmc-primitives/r_w_ok_bug/test.desc

@@ -1,9 +1,11 @@
-KNOWNBUG
+CORE
 main.c
 --pointer-check --no-simplify --no-propagation
-^EXIT=0$
+^\[main.pointer_dereference.\d+\] line 8 dereference failure: pointer outside dynamic object bounds in \*p: FAILURE$
+^\[main.pointer_dereference.\d+\] line 8 dereference failure: pointer outside object bounds in \*p: FAILURE$
+^\*\* 2 of \d+ failed
+^VERIFICATION FAILED$
+^EXIT=10$
 ^SIGNAL=0$
 --
 ^warning: ignoring
---
-Crashes during the flattening, issue #5328