diff --git a/regression/cbmc/pointer-overflow1/main.c b/regression/cbmc/pointer-overflow1/main.c
index eecb5222a40..062a1819ec5 100644
--- a/regression/cbmc/pointer-overflow1/main.c
+++ b/regression/cbmc/pointer-overflow1/main.c
@@ -11,8 +11,8 @@ int main()
   p2 = p - other1;
   p2 = p - other2 - other1;
 
-  p2 = p + sizeof(int);
-  p2 = p + sizeof(int) + sizeof(int);
+  p2 = (char *)p + sizeof(int);
+  p2 = (char *)p + sizeof(int) + sizeof(int);
 
   return 0;
 }
diff --git a/regression/cbmc/pointer-overflow1/test.desc b/regression/cbmc/pointer-overflow1/test.desc
index c0f0033f690..fedee95fa1a 100644
--- a/regression/cbmc/pointer-overflow1/test.desc
+++ b/regression/cbmc/pointer-overflow1/test.desc
@@ -3,9 +3,12 @@ main.c
 --pointer-overflow-check --unsigned-overflow-check
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main\.overflow\.\d+\] line \d+ (pointer )?arithmetic overflow on .*sizeof\(signed int\) .* : SUCCESS
+^\[main\.overflow\.\d+\] line 8 (pointer )?arithmetic overflow on .*: FAILURE
+^\[main\.overflow\.\d+\] line 9 (pointer )?arithmetic overflow on .*: FAILURE
+^\[main\.overflow\.\d+\] line 10 (pointer )?arithmetic overflow on .*: FAILURE
+^\[main\.overflow\.\d+\] line 11 (pointer )?arithmetic overflow on .*: FAILURE
+^\[main\.overflow\.\d+\] line 12 (pointer )?arithmetic overflow on .*: FAILURE
 ^VERIFICATION FAILED$
-^\*\* 8 of 13 failed
 --
-^\[main\.overflow\.\d+\] line \d+ (pointer )?arithmetic overflow on .*sizeof\(signed int\) .* : FAILURE
+^\[main\.overflow\.\d+\] line 1[45] (pointer )?arithmetic overflow on .*sizeof\(signed int\) .* : FAILURE
 ^warning: ignoring
diff --git a/regression/cbmc/pointer-overflow2/main.c b/regression/cbmc/pointer-overflow2/main.c
index e73ba1eb115..442e002ae79 100644
--- a/regression/cbmc/pointer-overflow2/main.c
+++ b/regression/cbmc/pointer-overflow2/main.c
@@ -2,9 +2,10 @@
 
 void main()
 {
+  __CPROVER_allocated_memory(9, sizeof(char));
   char *p = (char *)10;
   p -= 1;
   p += 1;
-  p += -1; // spurious pointer overflow report
-  p -= -1; // spurious pointer overflow report
+  p += -1; // previously: spurious pointer overflow report
+  p -= -1; // previously: spurious pointer overflow report
 }
diff --git a/regression/cbmc/pointer-overflow3/main.c b/regression/cbmc/pointer-overflow3/main.c
new file mode 100644
index 00000000000..a3a8c803f69
--- /dev/null
+++ b/regression/cbmc/pointer-overflow3/main.c
@@ -0,0 +1,13 @@
+#include <stdlib.h>
+
+int main()
+{
+  int *p = malloc(sizeof(int) * 5);
+  int *p2 = p + 10; // undefined behavior for indexing out of bounds
+  int *p3 = p - 10; // undefined behavior for indexing out of bounds
+
+  int arr[5];
+  int *p4 = arr + 10; // undefined behavior for indexing out of bounds
+  int *p5 = arr - 10; // undefined behavior for indexing out of bounds
+  return 0;
+}
diff --git a/regression/cbmc/pointer-overflow3/test.desc b/regression/cbmc/pointer-overflow3/test.desc
new file mode 100644
index 00000000000..7a98821d501
--- /dev/null
+++ b/regression/cbmc/pointer-overflow3/test.desc
@@ -0,0 +1,16 @@
+CORE broken-smt-backend
+main.c
+--pointer-overflow-check --no-simplify
+^\[main.pointer_arithmetic.\d+\] line 6 pointer arithmetic: pointer outside dynamic object bounds in p \+ \(signed (long (long )?)?int\)10: FAILURE
+^\[main.pointer_arithmetic.\d+\] line 7 pointer arithmetic: pointer outside dynamic object bounds in p - \(signed (long (long )?)?int\)10: FAILURE
+^\[main.pointer_arithmetic.\d+\] line 10 pointer arithmetic: pointer outside object bounds in arr \+ \(signed (long (long )?)?int\)10: FAILURE
+^\[main.pointer_arithmetic.\d+\] line 11 pointer arithmetic: pointer outside object bounds in arr - \(signed (long (long )?)?int\)10: FAILURE
+^\*\* 4 of \d+ failed
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+Invariant check failed
+--
+Uses --no-simplify to avoid removing repeated ASSERT FALSE statements.
diff --git a/src/analyses/goto_check.cpp b/src/analyses/goto_check.cpp
index 594fab39fc6..76ffb0505f1 100644
--- a/src/analyses/goto_check.cpp
+++ b/src/analyses/goto_check.cpp
@@ -286,8 +286,12 @@ class goto_checkt
 void goto_checkt::collect_allocations(
   const goto_functionst &goto_functions)
 {
-  if(!enable_pointer_check && !enable_bounds_check)
+  if(
+    !enable_pointer_check && !enable_bounds_check &&
+    !enable_pointer_overflow_check)
+  {
     return;
+  }
 
   for(const auto &gf_entry : goto_functions.function_map)
   {
@@ -1172,6 +1176,21 @@ void goto_checkt::pointer_overflow_check(
     expr.find_source_location(),
     expr,
     guard);
+
+  // the result must be within object bounds or one past the end
+  const auto size = from_integer(0, size_type());
+  auto conditions = get_pointer_dereferenceable_conditions(expr, size);
+
+  for(const auto &c : conditions)
+  {
+    add_guarded_property(
+      c.assertion,
+      "pointer arithmetic: " + c.description,
+      "pointer arithmetic",
+      expr.find_source_location(),
+      expr,
+      guard);
+  }
 }
 
 void goto_checkt::pointer_validity_check(
diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp
index a841f026004..368d4e20c9f 100644
--- a/src/solvers/flattening/bv_pointers.cpp
+++ b/src/solvers/flattening/bv_pointers.cpp
@@ -506,7 +506,7 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
 
     const bvt &bv = convert_bv(minus_expr.lhs());
 
-    typet pointer_sub_type = minus_expr.rhs().type().subtype();
+    typet pointer_sub_type = minus_expr.lhs().type().subtype();
     mp_integer element_size;
 
     if(pointer_sub_type.id()==ID_empty)