diff --git a/regression/cbmc/Pointer_Arithmetic18/main.c b/regression/cbmc/Pointer_Arithmetic18/main.c
new file mode 100644
index 00000000000..4297e96c282
--- /dev/null
+++ b/regression/cbmc/Pointer_Arithmetic18/main.c
@@ -0,0 +1,11 @@
+#define MB 0x00100000
+#define BASE (15 * MB)
+#define OFFSET (1 * MB)
+
+main()
+{
+  char *base = BASE;
+  int offset = OFFSET;
+  __CPROVER_assert(
+    &((char *)base)[offset] >= BASE + OFFSET, "no wrap-around expected");
+}
diff --git a/regression/cbmc/Pointer_Arithmetic18/test.desc b/regression/cbmc/Pointer_Arithmetic18/test.desc
new file mode 100644
index 00000000000..94d7221330d
--- /dev/null
+++ b/regression/cbmc/Pointer_Arithmetic18/test.desc
@@ -0,0 +1,8 @@
+KNOWNBUG
+main.c
+--32
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring
diff --git a/regression/cbmc/Pointer_comparison1/main.c b/regression/cbmc/Pointer_comparison1/main.c
new file mode 100644
index 00000000000..08022bf75fd
--- /dev/null
+++ b/regression/cbmc/Pointer_comparison1/main.c
@@ -0,0 +1,22 @@
+#include <stdlib.h>
+
+int main()
+{
+  if(sizeof(void *) != 8)
+    return 0;
+
+  char *p = malloc(1);
+  if(p == 0)
+    return 0;
+
+  if(
+    (unsigned long)p >
+    42) // unsoundly evaluates to true due to pointer encoding
+  {
+    return 0;
+  }
+
+  __CPROVER_assert(0, "");
+
+  return 0;
+}
diff --git a/regression/cbmc/Pointer_comparison1/test.desc b/regression/cbmc/Pointer_comparison1/test.desc
new file mode 100644
index 00000000000..6b765c70f48
--- /dev/null
+++ b/regression/cbmc/Pointer_comparison1/test.desc
@@ -0,0 +1,8 @@
+KNOWNBUG
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring