diff --git a/regression/cbmc/byte_extract1/main.c b/regression/cbmc/byte_extract1/main.c
new file mode 100644
index 00000000000..90c04de94cb
--- /dev/null
+++ b/regression/cbmc/byte_extract1/main.c
@@ -0,0 +1,11 @@
+#include <assert.h>
+#include <string.h>
+
+int main()
+{
+  int x;
+  int *p = (char *)&x - 2;
+  int y;
+  memcpy(&y, p, sizeof(int));
+  assert(0);
+}
diff --git a/regression/cbmc/byte_extract1/test.desc b/regression/cbmc/byte_extract1/test.desc
new file mode 100644
index 00000000000..d80821ffede
--- /dev/null
+++ b/regression/cbmc/byte_extract1/test.desc
@@ -0,0 +1,11 @@
+CORE
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+Invariant check failed
+--
+This example previously failed the invariant "mp_integer should be convertible
+to target integral type".
diff --git a/src/solvers/flattening/boolbv_byte_extract.cpp b/src/solvers/flattening/boolbv_byte_extract.cpp
index 97314f76cb2..9b78b79ecbd 100644
--- a/src/solvers/flattening/boolbv_byte_extract.cpp
+++ b/src/solvers/flattening/boolbv_byte_extract.cpp
@@ -121,7 +121,7 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
       if(offset + i < 0 || offset + i >= op_bv.size())
         bv[i]=prop.new_variable();
       else
-        bv[i] = op_bv[numeric_cast_v<std::size_t>(offset) + i];
+        bv[i] = op_bv[numeric_cast_v<std::size_t>(offset + i)];
   }
   else
   {