diff --git a/regression/cbmc/Pointer_Arithmetic12/test.desc b/regression/cbmc/Pointer_Arithmetic12/test.desc
index b3a154d150b..369ec919c3d 100644
--- a/regression/cbmc/Pointer_Arithmetic12/test.desc
+++ b/regression/cbmc/Pointer_Arithmetic12/test.desc
@@ -1,4 +1,4 @@
-CORE
+THOROUGH
 main.i
 --32 --little-endian
 ^EXIT=0$
@@ -6,3 +6,5 @@ main.i
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
+--
+Takes around 2 minutes to run.
diff --git a/regression/cbmc/Pointer_Arithmetic13/test.desc b/regression/cbmc/Pointer_Arithmetic13/test.desc
index 52168c7eba4..9efefbc7362 100644
--- a/regression/cbmc/Pointer_Arithmetic13/test.desc
+++ b/regression/cbmc/Pointer_Arithmetic13/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Pointer_Arithmetic18/main.c b/regression/cbmc/Pointer_Arithmetic18/main.c
new file mode 100644
index 00000000000..90345662392
--- /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;
+  int n = 2;
+  __CPROVER_assert(&((char *)base)[offset] != 0, "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..0098f266ed3
--- /dev/null
+++ b/regression/cbmc/Pointer_Arithmetic18/test.desc
@@ -0,0 +1,8 @@
+CORE
+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..6de79559914
--- /dev/null
+++ b/regression/cbmc/Pointer_comparison1/test.desc
@@ -0,0 +1,8 @@
+CORE
+main.c
+
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
diff --git a/regression/cbmc/address_space_size_limit1/test.c b/regression/cbmc/address_space_size_limit1/test.c
deleted file mode 100644
index a4f9e047262..00000000000
--- a/regression/cbmc/address_space_size_limit1/test.c
+++ /dev/null
@@ -1,16 +0,0 @@
-
-#include <stdlib.h>
-#include <assert.h>
-
-int main(int argc, char** argv)
-{
-
-  int i;
-  char* c;
-  for(i=0; i<300; ++i)
-  {
-    c=(char*)malloc(1);
-    assert(c!=(char*)0);
-  }
-
-}
diff --git a/regression/cbmc/address_space_size_limit1/test.desc b/regression/cbmc/address_space_size_limit1/test.desc
deleted file mode 100644
index 3bc849b0cbf..00000000000
--- a/regression/cbmc/address_space_size_limit1/test.desc
+++ /dev/null
@@ -1,7 +0,0 @@
-CORE thorough-paths broken-smt-backend
-test.c
---no-simplify --unwind 300 --object-bits 8
-too many addressed objects
-^EXIT=6$
-^SIGNAL=0$
---
diff --git a/regression/cbmc/address_space_size_limit3/test.desc b/regression/cbmc/address_space_size_limit3/test.desc
index ac8f72553aa..32244336607 100644
--- a/regression/cbmc/address_space_size_limit3/test.desc
+++ b/regression/cbmc/address_space_size_limit3/test.desc
@@ -1,4 +1,4 @@
-CORE
+THOROUGH
 main.i
 --32 --little-endian --object-bits 25 --pointer-check
 ^EXIT=10$
diff --git a/src/solvers/flattening/boolbv_byte_extract.cpp b/src/solvers/flattening/boolbv_byte_extract.cpp
index 9b78b79ecbd..cce55d6572a 100644
--- a/src/solvers/flattening/boolbv_byte_extract.cpp
+++ b/src/solvers/flattening/boolbv_byte_extract.cpp
@@ -38,8 +38,12 @@ bvt map_bv(const bv_endianness_mapt &map, const bvt &src)
 bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
 {
   // array logic does not handle byte operators, thus lower when operating on
-  // unbounded arrays
-  if(is_unbounded_array(expr.op().type()))
+  // unbounded arrays; similarly, byte extracts over pointers are not to be
+  // handled here
+  if(
+    is_unbounded_array(expr.op().type()) ||
+    has_subtype(expr.type(), ID_pointer, ns) ||
+    has_subtype(expr.op().type(), ID_pointer, ns))
   {
     return convert_bv(lower_byte_extract(expr, ns));
   }
diff --git a/src/solvers/flattening/boolbv_byte_update.cpp b/src/solvers/flattening/boolbv_byte_update.cpp
index 2210fc48cb7..3ee84ad4ca8 100644
--- a/src/solvers/flattening/boolbv_byte_update.cpp
+++ b/src/solvers/flattening/boolbv_byte_update.cpp
@@ -20,10 +20,13 @@ Author: Daniel Kroening, kroening@kroening.com
 bvt boolbvt::convert_byte_update(const byte_update_exprt &expr)
 {
   // if we update (from) an unbounded array, lower the expression as the array
-  // logic does not handle byte operators
+  // logic does not handle byte operators; similarly, data types that contain
+  // pointers must not be handled here
   if(
     is_unbounded_array(expr.op().type()) ||
-    is_unbounded_array(expr.value().type()))
+    is_unbounded_array(expr.value().type()) ||
+    has_subtype(expr.value().type(), ID_pointer, ns) ||
+    has_subtype(expr.op0().type(), ID_pointer, ns))
   {
     return convert_bv(lower_byte_update(expr, ns));
   }
diff --git a/src/solvers/flattening/boolbv_width.cpp b/src/solvers/flattening/boolbv_width.cpp
index 57c5bc3e3cd..991b45da0ed 100644
--- a/src/solvers/flattening/boolbv_width.cpp
+++ b/src/solvers/flattening/boolbv_width.cpp
@@ -11,8 +11,10 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <algorithm>
 
 #include <util/arith_tools.h>
+#include <util/config.h>
 #include <util/exception_utils.h>
 #include <util/invariant.h>
+#include <util/namespace.h>
 #include <util/std_types.h>
 
 boolbv_widtht::boolbv_widtht(const namespacet &_ns):ns(_ns)
@@ -23,6 +25,21 @@ boolbv_widtht::~boolbv_widtht()
 {
 }
 
+std::size_t boolbv_widtht::get_object_width(const pointer_typet &type) const
+{
+  return type.get_width();
+}
+
+std::size_t boolbv_widtht::get_offset_width(const pointer_typet &type) const
+{
+  return type.get_width();
+}
+
+std::size_t boolbv_widtht::get_address_width(const pointer_typet &type) const
+{
+  return type.get_width();
+}
+
 const boolbv_widtht::entryt &boolbv_widtht::get_entry(const typet &type) const
 {
   // check cache first
@@ -182,7 +199,12 @@ const boolbv_widtht::entryt &boolbv_widtht::get_entry(const typet &type) const
     CHECK_RETURN(entry.total_width > 0);
   }
   else if(type_id==ID_pointer)
-    entry.total_width = type_checked_cast<pointer_typet>(type).get_width();
+  {
+    const pointer_typet &t = type_checked_cast<pointer_typet>(type);
+    entry.total_width =
+      get_address_width(t) + get_object_width(t) + get_offset_width(t);
+    DATA_INVARIANT(entry.total_width != 0, "pointer must have width");
+  }
   else if(type_id==ID_struct_tag)
     entry=get_entry(ns.follow_tag(to_struct_tag_type(type)));
   else if(type_id==ID_union_tag)
diff --git a/src/solvers/flattening/boolbv_width.h b/src/solvers/flattening/boolbv_width.h
index d25115b3a83..e29e351b94e 100644
--- a/src/solvers/flattening/boolbv_width.h
+++ b/src/solvers/flattening/boolbv_width.h
@@ -11,7 +11,8 @@ Author: Daniel Kroening, kroening@kroening.com
 #define CPROVER_SOLVERS_FLATTENING_BOOLBV_WIDTH_H
 
 #include <util/std_types.h>
-#include <util/namespace.h>
+
+class namespacet;
 
 class boolbv_widtht
 {
@@ -33,6 +34,10 @@ class boolbv_widtht
     const struct_typet &type,
     const irep_idt &member) const;
 
+  std::size_t get_object_width(const pointer_typet &type) const;
+  std::size_t get_offset_width(const pointer_typet &type) const;
+  std::size_t get_address_width(const pointer_typet &type) const;
+
 protected:
   const namespacet &ns;
 
diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp
index c2becd93654..f2ba6558035 100644
--- a/src/solvers/flattening/bv_pointers.cpp
+++ b/src/solvers/flattening/bv_pointers.cpp
@@ -11,7 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/arith_tools.h>
 #include <util/bitvector_expr.h>
 #include <util/c_types.h>
-#include <util/config.h>
 #include <util/exception_utils.h>
 #include <util/pointer_expr.h>
 #include <util/pointer_offset_size.h>
@@ -34,6 +33,10 @@ literalt bv_pointerst::convert_rest(const exprt &expr)
         bvt invalid_bv;
         encode(pointer_logic.get_invalid_object(), invalid_bv);
 
+        const pointer_typet &type = to_pointer_type(operands[0].type());
+        const std::size_t object_bits = boolbv_width.get_object_width(type);
+        const std::size_t offset_bits = boolbv_width.get_offset_width(type);
+
         bvt equal_invalid_bv;
         equal_invalid_bv.resize(object_bits);
 
@@ -70,8 +73,11 @@ literalt bv_pointerst::convert_rest(const exprt &expr)
        operands[0].type().id()==ID_pointer &&
        operands[1].type().id()==ID_pointer)
     {
-      const bvt &bv0=convert_bv(operands[0]);
-      const bvt &bv1=convert_bv(operands[1]);
+      // comparison over integers
+      bvt bv0 = convert_bv(operands[0]);
+      address_bv(bv0, to_pointer_type(operands[0].type()));
+      bvt bv1 = convert_bv(operands[1]);
+      address_bv(bv1, to_pointer_type(operands[1].type()));
 
       return bv_utils.rel(
         bv0, expr.id(), bv1, bv_utilst::representationt::UNSIGNED);
@@ -87,12 +93,38 @@ bv_pointerst::bv_pointerst(
   message_handlert &message_handler,
   bool get_array_constraints)
   : boolbvt(_ns, _prop, message_handler, get_array_constraints),
-    pointer_logic(_ns)
+    pointer_logic(_ns),
+    need_address_bounds(false)
 {
-  object_bits=config.bv_encoding.object_bits;
-  std::size_t pointer_width = boolbv_width(pointer_type(empty_typet()));
-  offset_bits=pointer_width-object_bits;
-  bits=pointer_width;
+  const pointer_typet type = pointer_type(empty_typet());
+
+  // the address of NULL is zero unless the platform uses a different
+  // configuration, in which case we use a non-deterministic integer
+  // value
+  bvt &null_pointer = pointer_bits[pointer_logic.get_null_object()];
+  null_pointer.resize(
+    boolbv_width.get_address_width(type), const_literal(false));
+  if(!pointer_logic.get_null_is_zero())
+  {
+    for(auto &literal : null_pointer)
+      literal = prop.new_variable();
+  }
+
+  // use the maximum integer as the address of an invalid object,
+  // unless NULL is not zero on this platform (and might thus be this
+  // maximum integer), in which case we use a non-deterministic
+  // integer value
+  bvt &invalid_object = pointer_bits[pointer_logic.get_invalid_object()];
+  invalid_object.resize(
+    boolbv_width.get_address_width(type), const_literal(true));
+  if(!pointer_logic.get_null_is_zero())
+  {
+    for(auto &literal : invalid_object)
+      literal = prop.new_variable();
+
+    // NULL and INVALID are distinct
+    prop.l_set_to_false(bv_utils.equal(null_pointer, invalid_object));
+  }
 }
 
 bool bv_pointerst::convert_address_of_rec(
@@ -121,11 +153,13 @@ bool bv_pointerst::convert_address_of_rec(
     const exprt &index=index_expr.index();
     const typet &array_type = array.type();
 
+    const std::size_t bits = boolbv_width(pointer_type(empty_typet()));
+
     // recursive call
     if(array_type.id()==ID_pointer)
     {
       // this should be gone
-      bv=convert_pointer_type(array);
+      bv = convert_bv(array);
       CHECK_RETURN(bv.size()==bits);
     }
     else if(array_type.id()==ID_array ||
@@ -155,6 +189,7 @@ bool bv_pointerst::convert_address_of_rec(
     if(convert_address_of_rec(byte_extract_expr.op(), bv))
       return true;
 
+    const std::size_t bits = boolbv_width(pointer_type(empty_typet()));
     CHECK_RETURN(bv.size()==bits);
 
     offset_arithmetic(bv, 1, byte_extract_expr.offset());
@@ -223,8 +258,7 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
 {
   PRECONDITION(expr.type().id() == ID_pointer);
 
-  // make sure the config hasn't been changed
-  PRECONDITION(bits==boolbv_width(expr.type()));
+  const std::size_t bits = boolbv_width(expr.type());
 
   if(expr.id()==ID_symbol)
   {
@@ -257,11 +291,55 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
       op_type.id() == ID_c_enum || op_type.id() == ID_c_enum_tag)
     {
       // Cast from a bitvector type to pointer.
-      // We just do a zero extension.
 
-      const bvt &op_bv=convert_bv(op);
+      // Fixed integer address is NULL object plus given offset.
+      if(op.id() == ID_constant)
+      {
+        bvt bv;
+
+        encode(pointer_logic.get_null_object(), bv);
+        offset_arithmetic(bv, 1, op);
+
+        return bv;
+      }
 
-      return bv_utils.zero_extension(op_bv, bits);
+      // For all other cases we postpone until we know the full set of objects.
+      std::size_t width =
+        boolbv_width.get_offset_width(to_pointer_type(expr.type())) +
+        boolbv_width.get_object_width(to_pointer_type(expr.type()));
+
+      bvt bv;
+      bv.resize(width);
+
+      for(std::size_t i = 0; i < width; i++)
+        bv[i] = prop.new_variable();
+
+      bvt op_bv = convert_bv(op);
+      bv_utilst::representationt rep = op_type.id() == ID_signedbv
+                                         ? bv_utilst::representationt::SIGNED
+                                         : bv_utilst::representationt::UNSIGNED;
+
+      DATA_INVARIANT(
+        op_bv.size() <=
+          boolbv_width.get_address_width(to_pointer_type(expr.type())),
+        "integer cast to pointer of smaller size");
+      op_bv = bv_utils.extension(
+        op_bv,
+        boolbv_width.get_address_width(to_pointer_type(expr.type())),
+        rep);
+
+      bv.insert(bv.end(), op_bv.begin(), op_bv.end());
+
+      postponed_list.push_back(postponedt());
+      postponed_list.back().op = op_bv;
+      postponed_list.back().bv = bv;
+      postponed_list.back().expr = expr;
+
+      DATA_INVARIANT(
+        postponed_list.back().bv.size() == bits,
+        "pointer encoding does not have matching width");
+
+      return postponed_list.back().bv;
     }
   }
   else if(expr.id()==ID_if)
@@ -304,7 +382,18 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
     else
     {
       mp_integer i = bvrep2integer(value, bits, false);
-      bv=bv_utils.build_constant(i, bits);
+      bvt bv_offset = bv_utils.build_constant(
+        i, boolbv_width.get_offset_width(to_pointer_type(expr.type())));
+      bvt bv_addr = bv_utils.build_constant(
+        i, boolbv_width.get_address_width(to_pointer_type(expr.type())));
+
+      encode(pointer_logic.get_invalid_object(), bv);
+      object_bv(bv, to_pointer_type(expr.type()));
+      bv.insert(bv.end(), bv_offset.begin(), bv_offset.end());
+      bv.insert(bv.end(), bv_addr.begin(), bv_addr.end());
+
+      DATA_INVARIANT(
+        bv.size() == bits, "pointer encoding does not have matching width");
     }
 
     return bv;
@@ -349,12 +438,15 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
       count == 1,
       "there should be exactly one pointer-type operand in a pointer-type sum");
 
-    bvt sum=bv_utils.build_constant(0, bits);
-
-    forall_operands(it, plus_expr)
+    exprt sum = plus_expr;
+    for(exprt::operandst::iterator it = sum.operands().begin();
+        it != sum.operands().end();) // no ++it
     {
       if(it->type().id()==ID_pointer)
+      {
+        it = sum.operands().erase(it);
         continue;
+      }
 
       if(it->type().id()!=ID_unsignedbv &&
          it->type().id()!=ID_signedbv)
@@ -364,21 +456,14 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
         return failed_bv;
       }
 
-      bv_utilst::representationt rep=
-        it->type().id()==ID_signedbv?bv_utilst::representationt::SIGNED:
-                                     bv_utilst::representationt::UNSIGNED;
-
-      bvt op=convert_bv(*it);
-      CHECK_RETURN(!op.empty());
-
-      // we cut any extra bits off
-
-      if(op.size()>bits)
-        op.resize(bits);
-      else if(op.size()<bits)
-        op=bv_utils.extension(op, bits, rep);
-
-      sum=bv_utils.add(sum, op);
+      sum.type() = it->type();
+      ++it;
+    }
+    CHECK_RETURN(!sum.operands().empty());
+    if(sum.operands().size() == 1)
+    {
+      exprt tmp = sum.operands().front();
+      sum.swap(tmp);
     }
 
     offset_arithmetic(bv, size, sum);
@@ -464,6 +549,10 @@ bvt bv_pointerst::convert_bitvector(const exprt &expr)
     bvt lhs = convert_bv(minus_expr.lhs());
     bvt rhs = convert_bv(minus_expr.rhs());
 
+    // this is address arithmetic, but does consider the type
+    address_bv(lhs, to_pointer_type(minus_expr.lhs().type()));
+    address_bv(rhs, to_pointer_type(minus_expr.rhs().type()));
+
     std::size_t width=boolbv_width(expr.type());
 
     if(width==0)
@@ -504,7 +593,8 @@ bvt bv_pointerst::convert_bitvector(const exprt &expr)
     expr.id() == ID_pointer_offset &&
     to_unary_expr(expr).op().type().id() == ID_pointer)
   {
-    bvt op0 = convert_bv(to_unary_expr(expr).op());
+    const exprt &op0 = to_unary_expr(expr).op();
+    bvt op0_bv = convert_bv(op0);
 
     std::size_t width=boolbv_width(expr.type());
 
@@ -512,10 +602,10 @@ bvt bv_pointerst::convert_bitvector(const exprt &expr)
       return conversion_failed(expr);
 
     // we need to strip off the object part
-    op0.resize(offset_bits);
+    offset_bv(op0_bv, to_pointer_type(op0.type()));
 
     // we do a sign extension to permit negative offsets
-    return bv_utils.sign_extension(op0, width);
+    return bv_utils.sign_extension(op0_bv, width);
   }
   else if(
     expr.id() == ID_object_size &&
@@ -542,33 +632,36 @@ bvt bv_pointerst::convert_bitvector(const exprt &expr)
     expr.id() == ID_pointer_object &&
     to_unary_expr(expr).op().type().id() == ID_pointer)
   {
-    bvt op0 = convert_bv(to_unary_expr(expr).op());
+    const exprt &op0 = to_unary_expr(expr).op();
+    bvt op0_bv = convert_bv(op0);
 
     std::size_t width=boolbv_width(expr.type());
 
     if(width==0)
       return conversion_failed(expr);
 
-    // erase offset bits
+    // erase offset and integer bits
+    object_bv(op0_bv, to_pointer_type(op0.type()));
 
-    op0.erase(op0.begin()+0, op0.begin()+offset_bits);
-
-    return bv_utils.zero_extension(op0, width);
+    return bv_utils.zero_extension(op0_bv, width);
   }
   else if(
     expr.id() == ID_typecast &&
     to_typecast_expr(expr).op().type().id() == ID_pointer)
   {
     // pointer to int
-    bvt op0 = convert_pointer_type(to_typecast_expr(expr).op());
+    bvt op0 = convert_bv(to_typecast_expr(expr).op());
 
-    // squeeze it in!
+    // erase offset and object bits
+    address_bv(op0, to_pointer_type(to_typecast_expr(expr).op().type()));
 
     std::size_t width=boolbv_width(expr.type());
 
     if(width==0)
       return conversion_failed(expr);
 
+    need_address_bounds = true;
+
     return bv_utils.zero_extension(op0, width);
   }
 
@@ -584,9 +677,15 @@ exprt bv_pointerst::bv_get_rec(
   if(type.id()!=ID_pointer)
     return SUB::bv_get_rec(expr, bv, offset, type);
 
-  std::string value_addr, value_offset, value;
+  std::string value, value_offset, value_obj;
 
-  for(std::size_t i=0; i<bits; i++)
+  const std::size_t object_bits =
+    boolbv_width.get_object_width(to_pointer_type(type));
+  const std::size_t offset_bits =
+    boolbv_width.get_offset_width(to_pointer_type(type));
+  const std::size_t address_bits =
+    boolbv_width.get_address_width(to_pointer_type(type));
+  for(std::size_t i = 0; i < object_bits + offset_bits + address_bits; i++)
   {
     char ch=0;
     std::size_t bit_nr=i+offset;
@@ -600,18 +699,18 @@ exprt bv_pointerst::bv_get_rec(
     }
     // clang-format on
 
-    value=ch+value;
-
-    if(i<offset_bits)
-      value_offset=ch+value_offset;
+    if(i < object_bits)
+      value_obj = ch + value_obj;
+    else if(i < object_bits + offset_bits)
+      value_offset = ch + value_offset;
     else
-      value_addr=ch+value_addr;
+      value = ch + value;
   }
 
   // we treat these like bit-vector constants, but with
   // some additional annotation
 
-  const irep_idt bvrep = make_bvrep(bits, [&value](std::size_t i) {
+  const irep_idt bvrep = make_bvrep(address_bits, [&value](std::size_t i) {
     return value[value.size() - 1 - i] == '1';
   });
 
@@ -619,7 +718,7 @@ exprt bv_pointerst::bv_get_rec(
 
   pointer_logict::pointert pointer;
   pointer.object =
-    numeric_cast_v<std::size_t>(binary2integer(value_addr, false));
+    numeric_cast_v<std::size_t>(binary2integer(value_obj, false));
   pointer.offset=binary2integer(value_offset, true);
 
   // we add the elaborated expression as operand
@@ -631,29 +730,69 @@ exprt bv_pointerst::bv_get_rec(
 
 void bv_pointerst::encode(std::size_t addr, bvt &bv)
 {
-  bv.resize(bits);
+  const pointer_typet type = pointer_type(empty_typet());
+  const std::size_t offset_bits = boolbv_width.get_offset_width(type);
+  const std::size_t object_bits = boolbv_width.get_object_width(type);
+  const std::size_t address_bits = boolbv_width.get_object_width(type);
+  const std::size_t bits = offset_bits + object_bits + address_bits;
+  PRECONDITION(boolbv_width(type) == bits);
 
-  // set offset to zero
-  for(std::size_t i=0; i<offset_bits; i++)
-    bv[i]=const_literal(false);
+  bv.clear();
+  bv.reserve(bits);
 
   // set variable part
   for(std::size_t i=0; i<object_bits; i++)
-    bv[offset_bits+i]=const_literal((addr&(std::size_t(1)<<i))!=0);
+    bv.push_back(const_literal((addr & (std::size_t(1) << i)) != 0));
+
+  // set offset to zero
+  for(std::size_t i = 0; i < offset_bits; i++)
+    bv.push_back(const_literal(false));
+
+  // add integer value
+  auto entry = pointer_bits.insert({addr, bvt()});
+  if(entry.second)
+  {
+    entry.first->second.reserve(address_bits);
+    for(unsigned i = 0; i < address_bits; ++i)
+      entry.first->second.push_back(prop.new_variable());
+  }
+
+  bv.insert(bv.end(), entry.first->second.begin(), entry.first->second.end());
+
+  DATA_INVARIANT(
+    bv.size() == bits, "pointer encoding does not have matching width");
 }
 
 void bv_pointerst::offset_arithmetic(bvt &bv, const mp_integer &x)
 {
+  const pointer_typet type = pointer_type(empty_typet());
+  const std::size_t offset_bits = boolbv_width.get_offset_width(type);
+  const std::size_t object_bits = boolbv_width.get_object_width(type);
+  const std::size_t address_bits = boolbv_width.get_object_width(type);
+
+  // add to offset_bits
   bvt bv1=bv;
-  bv1.resize(offset_bits); // strip down
+  offset_bv(bv1, type);
 
   bvt bv2=bv_utils.build_constant(x, offset_bits);
 
   bvt tmp=bv_utils.add(bv1, bv2);
 
-  // copy offset bits
+  // update offset bits
   for(std::size_t i=0; i<offset_bits; i++)
-    bv[i]=tmp[i];
+    bv[object_bits + i] = tmp[i];
+
+  // add to pointer value
+  bvt bv3 = bv;
+  address_bv(bv3, type);
+
+  bvt bv4 = bv_utils.build_constant(x, address_bits);
+
+  bvt tmp2 = bv_utils.add(bv3, bv4);
+
+  // update pointer value by offset
+  for(std::size_t i = 0; i < address_bits; i++)
+    bv[object_bits + offset_bits + i] = tmp2[i];
 }
 
 void bv_pointerst::offset_arithmetic(
@@ -661,62 +800,85 @@ void bv_pointerst::offset_arithmetic(
   const mp_integer &factor,
   const exprt &index)
 {
+  const pointer_typet type = pointer_type(empty_typet());
+  const std::size_t offset_bits = boolbv_width.get_offset_width(type);
+  const std::size_t object_bits = boolbv_width.get_object_width(type);
+  const std::size_t address_bits = boolbv_width.get_object_width(type);
+
   bvt bv_index=convert_bv(index);
 
   bv_utilst::representationt rep=
     index.type().id()==ID_signedbv?bv_utilst::representationt::SIGNED:
                                    bv_utilst::representationt::UNSIGNED;
 
+  DATA_INVARIANT(
+    bv_index.size() <= offset_bits,
+    "pointer arithmetic does not have matching width");
   bv_index=bv_utils.extension(bv_index, offset_bits, rep);
 
-  offset_arithmetic(bv, factor, bv_index);
-}
-
-void bv_pointerst::offset_arithmetic(
-  bvt &bv,
-  const mp_integer &factor,
-  const bvt &index)
-{
-  bvt bv_index;
-
-  if(factor==1)
-    bv_index=index;
-  else
+  if(factor != 1)
   {
-    bvt bv_factor=bv_utils.build_constant(factor, index.size());
-    bv_index=bv_utils.unsigned_multiplier(index, bv_factor);
+    bvt bv_factor = bv_utils.build_constant(factor, offset_bits);
+    bv_index = bv_utils.signed_multiplier(bv_index, bv_factor);
   }
 
-  bv_index=bv_utils.zero_extension(bv_index, bv.size());
+  // add to offset_bits
+  bvt bv1 = bv;
+  offset_bv(bv1, type);
 
-  bvt bv_tmp=bv_utils.add(bv, bv_index);
+  bvt bv_tmp = bv_utils.add(bv1, bv_index);
 
-  // copy lower parts of result
+  // update offset bits
   for(std::size_t i=0; i<offset_bits; i++)
-    bv[i]=bv_tmp[i];
+    bv[object_bits + i] = bv_tmp[i];
+
+  // add to pointer value
+  bvt bv2 = bv;
+  address_bv(bv2, type);
+
+  bv_index = bv_utils.zero_extension(bv_index, address_bits);
+
+  bvt tmp2 = bv_utils.add(bv2, bv_index);
+
+  // update pointer value by offset
+  for(std::size_t i = 0; i < address_bits; i++)
+    bv[object_bits + offset_bits + i] = tmp2[i];
 }
 
 void bv_pointerst::add_addr(const exprt &expr, bvt &bv)
 {
   std::size_t a=pointer_logic.add_object(expr);
 
+  const pointer_typet type = pointer_type(expr.type());
+  const std::size_t object_bits = boolbv_width.get_object_width(type);
   const std::size_t max_objects=std::size_t(1)<<object_bits;
 
   if(a==max_objects)
     throw analysis_exceptiont(
       "too many addressed objects: maximum number of objects is set to 2^n=" +
-      std::to_string(max_objects) + " (with n=" + std::to_string(object_bits) +
-      "); " +
+      std::to_string(max_objects) + " (with n=" +
+      std::to_string(boolbv_width.get_object_width(type)) + "); " +
       "use the `--object-bits n` option to increase the maximum number");
 
+  auto entry = pointer_bits.insert({a, bvt()});
+  if(entry.second)
+  {
+    std::size_t address_bits = boolbv_width.get_address_width(type);
+
+    entry.first->second.reserve(address_bits);
+    for(unsigned i = 0; i < address_bits; ++i)
+      entry.first->second.push_back(prop.new_variable());
+  }
+
   encode(a, bv);
 }
 
-void bv_pointerst::do_postponed(
-  const postponedt &postponed)
+void bv_pointerst::do_postponed_non_typecast(const postponedt &postponed)
 {
   if(postponed.expr.id() == ID_is_dynamic_object)
   {
+    const auto &type =
+      to_pointer_type(to_unary_expr(postponed.expr).op().type());
     const auto &objects = pointer_logic.objects;
     std::size_t number=0;
 
@@ -729,11 +891,10 @@ void bv_pointerst::do_postponed(
       // only compare object part
       bvt bv;
       encode(number, bv);
-
-      bv.erase(bv.begin(), bv.begin()+offset_bits);
+      object_bv(bv, type);
 
       bvt saved_bv=postponed.op;
-      saved_bv.erase(saved_bv.begin(), saved_bv.begin()+offset_bits);
+      object_bv(saved_bv, type);
 
       POSTCONDITION(bv.size()==saved_bv.size());
       PRECONDITION(postponed.bv.size()==1);
@@ -749,6 +910,8 @@ void bv_pointerst::do_postponed(
   }
   else if(postponed.expr.id()==ID_object_size)
   {
+    const auto &type =
+      to_pointer_type(to_unary_expr(postponed.expr).op().type());
     const auto &objects = pointer_logic.objects;
     std::size_t number=0;
 
@@ -770,11 +933,10 @@ void bv_pointerst::do_postponed(
       // only compare object part
       bvt bv;
       encode(number, bv);
-
-      bv.erase(bv.begin(), bv.begin()+offset_bits);
+      object_bv(bv, type);
 
       bvt saved_bv=postponed.op;
-      saved_bv.erase(saved_bv.begin(), saved_bv.begin()+offset_bits);
+      object_bv(saved_bv, type);
 
       bvt size_bv = convert_bv(object_size);
 
@@ -783,15 +945,195 @@ void bv_pointerst::do_postponed(
       PRECONDITION(size_bv.size() == postponed.bv.size());
 
       literalt l1=bv_utils.equal(bv, saved_bv);
+
       literalt l2=bv_utils.equal(postponed.bv, size_bv);
 
       prop.l_set_to_true(prop.limplies(l1, l2));
     }
   }
+  else if(postponed.expr.id() == ID_typecast)
+  {
+    // defer until phase 2 as the other postponed expressions may
+    // yield additional entries in pointer_bits
+    need_address_bounds = true;
+  }
   else
     UNREACHABLE;
 }
 
+void bv_pointerst::encode_object_bounds(bounds_mapt &dest)
+{
+  const auto &objects = pointer_logic.objects;
+  std::size_t number = 0;
+
+  const bvt null_pointer = pointer_bits.at(pointer_logic.get_null_object());
+  const bvt &invalid_object =
+    pointer_bits.at(pointer_logic.get_invalid_object());
+
+  bvt conj;
+  conj.reserve(objects.size());
+
+  for(const exprt &expr : objects)
+  {
+    const auto size_expr = size_of_expr(expr.type(), ns);
+
+    if(!size_expr.has_value())
+    {
+      ++number;
+      continue;
+    }
+
+    bvt size_bv = convert_bv(*size_expr);
+
+    // NULL, INVALID have no size
+    DATA_INVARIANT(
+      number != pointer_logic.get_null_object(),
+      "NULL object cannot have a size");
+    DATA_INVARIANT(
+      number != pointer_logic.get_invalid_object(),
+      "INVALID object cannot have a size");
+
+    bvt object_bv;
+    encode(number, object_bv);
+
+    // prepare comparison over integers
+    bvt bv = object_bv;
+    address_bv(bv, pointer_type(expr.type()));
+    DATA_INVARIANT(
+      bv.size() == null_pointer.size(),
+      "NULL pointer encoding does not have matching width");
+    DATA_INVARIANT(
+      bv.size() == invalid_object.size(),
+      "INVALID pointer encoding does not have matching width");
+    DATA_INVARIANT(
+      size_bv.size() == bv.size(),
+      "pointer encoding does not have matching width");
+
+    // NULL, INVALID must not be within object bounds
+    literalt null_lower_bound = bv_utils.rel(
+      null_pointer, ID_lt, bv, bv_utilst::representationt::UNSIGNED);
+
+    literalt inv_obj_lower_bound = bv_utils.rel(
+      invalid_object, ID_lt, bv, bv_utilst::representationt::UNSIGNED);
+
+    // compute the upper bound with the side effect of enforcing the
+    // object addresses not to wrap around/overflow
+    bvt obj_upper_bound = bv_utils.add_sub_no_overflow(
+      bv, size_bv, false, bv_utilst::representationt::UNSIGNED);
+
+    literalt null_upper_bound = bv_utils.rel(
+      null_pointer,
+      ID_ge,
+      obj_upper_bound,
+      bv_utilst::representationt::UNSIGNED);
+
+    literalt inv_obj_upper_bound = bv_utils.rel(
+      invalid_object,
+      ID_ge,
+      obj_upper_bound,
+      bv_utilst::representationt::UNSIGNED);
+
+    // store bounds for re-use
+    dest.insert({number, {bv, obj_upper_bound}});
+
+    conj.push_back(prop.lor(null_lower_bound, null_upper_bound));
+    conj.push_back(prop.lor(inv_obj_lower_bound, inv_obj_upper_bound));
+
+    ++number;
+  }
+
+  if(!conj.empty())
+    prop.l_set_to_true(prop.land(conj));
+}
+
+void bv_pointerst::do_postponed_typecast(
+  const postponedt &postponed,
+  const bounds_mapt &bounds)
+{
+  if(postponed.expr.id() != ID_typecast)
+    return;
+
+  const pointer_typet &type = to_pointer_type(postponed.expr.type());
+  const std::size_t bits = boolbv_width.get_offset_width(type) +
+                           boolbv_width.get_object_width(type) +
+                           boolbv_width.get_address_width(type);
+
+  // given an integer (possibly representing an address) postponed.op,
+  // compute the object and offset that it may refer to
+  bvt saved_bv = postponed.op;
+
+  bvt conj, oob_conj;
+  conj.reserve(bounds.size() + 3);
+  oob_conj.reserve(bounds.size());
+
+  for(const auto &bounds_entry : bounds)
+  {
+    std::size_t number = bounds_entry.first;
+
+    // pointer must be within object bounds
+    const bvt &lb = bounds_entry.second.first;
+    const bvt &ub = bounds_entry.second.second;
+
+    literalt lower_bound =
+      bv_utils.rel(saved_bv, ID_ge, lb, bv_utilst::representationt::UNSIGNED);
+
+    literalt upper_bound =
+      bv_utils.rel(saved_bv, ID_lt, ub, bv_utilst::representationt::UNSIGNED);
+
+    // compute the offset within the object, and the corresponding
+    // pointer bv
+    bvt offset = bv_utils.sub(saved_bv, lb);
+
+    bvt bv;
+    encode(number, bv);
+    object_bv(bv, type);
+    DATA_INVARIANT(
+      offset.size() == boolbv_width.get_offset_width(type),
+      "pointer encoding does not have matching width");
+    bv.insert(bv.end(), offset.begin(), offset.end());
+    bv.insert(bv.end(), saved_bv.begin(), saved_bv.end());
+    DATA_INVARIANT(
+      bv.size() == bits, "pointer encoding does not have matching width");
+
+    // if the integer address is within the object bounds, return an
+    // adjusted offset
+    literalt in_bounds = prop.land(lower_bound, upper_bound);
+    conj.push_back(prop.limplies(in_bounds, bv_utils.equal(bv, postponed.bv)));
+    oob_conj.push_back(!in_bounds);
+  }
+
+  // append integer address as both offset and address
+  bvt invalid_bv, null_bv;
+  encode(pointer_logic.get_invalid_object(), invalid_bv);
+  object_bv(invalid_bv, type);
+  invalid_bv.insert(invalid_bv.end(), saved_bv.begin(), saved_bv.end());
+  invalid_bv.insert(invalid_bv.end(), saved_bv.begin(), saved_bv.end());
+  encode(pointer_logic.get_null_object(), null_bv);
+  object_bv(null_bv, type);
+  null_bv.insert(null_bv.end(), saved_bv.begin(), saved_bv.end());
+  null_bv.insert(null_bv.end(), saved_bv.begin(), saved_bv.end());
+
+  // NULL is always NULL
+  conj.push_back(prop.limplies(
+    bv_utils.equal(saved_bv, pointer_bits.at(pointer_logic.get_null_object())),
+    bv_utils.equal(null_bv, postponed.bv)));
+
+  // INVALID is always INVALID
+  conj.push_back(prop.limplies(
+    bv_utils.equal(
+      saved_bv, pointer_bits.at(pointer_logic.get_invalid_object())),
+    bv_utils.equal(invalid_bv, postponed.bv)));
+
+  // one of the objects or NULL or INVALID with an offset
+  conj.push_back(prop.limplies(
+    prop.land(oob_conj),
+    prop.lor(
+      bv_utils.equal(null_bv, postponed.bv),
+      bv_utils.equal(invalid_bv, postponed.bv))));
+
+  prop.l_set_to_true(prop.land(conj));
+}
+
 void bv_pointerst::post_process()
 {
   // post-processing arrays may yield further objects, do this first
@@ -801,7 +1143,19 @@ void bv_pointerst::post_process()
       it=postponed_list.begin();
       it!=postponed_list.end();
       it++)
-    do_postponed(*it);
+    do_postponed_non_typecast(*it);
+
+  if(need_address_bounds)
+  {
+    // make sure NULL and INVALID are unique addresses
+    bounds_mapt bounds;
+    encode_object_bounds(bounds);
+
+    for(postponed_listt::const_iterator it = postponed_list.begin();
+        it != postponed_list.end();
+        it++)
+      do_postponed_typecast(*it, bounds);
+  }
 
   // Clear the list to avoid re-doing in case of incremental usage.
   postponed_list.clear();
diff --git a/src/solvers/flattening/bv_pointers.h b/src/solvers/flattening/bv_pointers.h
index 0c6c01cfb2f..509770823a7 100644
--- a/src/solvers/flattening/bv_pointers.h
+++ b/src/solvers/flattening/bv_pointers.h
@@ -10,7 +10,6 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_SOLVERS_FLATTENING_BV_POINTERS_H
 #define CPROVER_SOLVERS_FLATTENING_BV_POINTERS_H
 
-
 #include "boolbv.h"
 #include "pointer_logic.h"
 
@@ -31,7 +30,9 @@ class bv_pointerst:public boolbvt
   // NOLINTNEXTLINE(readability/identifiers)
   typedef boolbvt SUB;
 
-  unsigned object_bits, offset_bits, bits;
+  typedef std::map<std::size_t, bvt> pointer_bitst;
+  pointer_bitst pointer_bits;
+  bool need_address_bounds;
 
   void encode(std::size_t object, bvt &bv);
 
@@ -55,8 +56,6 @@ class bv_pointerst:public boolbvt
 
   void offset_arithmetic(bvt &bv, const mp_integer &x);
   void offset_arithmetic(bvt &bv, const mp_integer &factor, const exprt &index);
-  void offset_arithmetic(
-    bvt &bv, const mp_integer &factor, const bvt &index_bv);
 
   struct postponedt
   {
@@ -67,7 +66,30 @@ class bv_pointerst:public boolbvt
   typedef std::list<postponedt> postponed_listt;
   postponed_listt postponed_list;
 
-  void do_postponed(const postponedt &postponed);
+  void do_postponed_non_typecast(const postponedt &postponed);
+  typedef std::map<std::size_t, std::pair<bvt, bvt>> bounds_mapt;
+  void encode_object_bounds(bounds_mapt &dest);
+  void
+  do_postponed_typecast(const postponedt &postponed, const bounds_mapt &bounds);
+
+  void object_bv(bvt &bv, const pointer_typet &type) const
+  {
+    bv.resize(boolbv_width.get_object_width(type));
+  }
+
+  void offset_bv(bvt &bv, const pointer_typet &type) const
+  {
+    bv.erase(bv.begin(), bv.begin() + boolbv_width.get_object_width(type));
+    bv.resize(boolbv_width.get_offset_width(type));
+  }
+
+  void address_bv(bvt &bv, const pointer_typet &type) const
+  {
+    bv.erase(
+      bv.begin(),
+      bv.begin() + boolbv_width.get_object_width(type) +
+        boolbv_width.get_offset_width(type));
+  }
 };
 
 #endif // CPROVER_SOLVERS_FLATTENING_BV_POINTERS_H
diff --git a/src/solvers/flattening/pointer_logic.cpp b/src/solvers/flattening/pointer_logic.cpp
index f96921d3a48..ba37c9b5403 100644
--- a/src/solvers/flattening/pointer_logic.cpp
+++ b/src/solvers/flattening/pointer_logic.cpp
@@ -14,6 +14,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/arith_tools.h>
 #include <util/byte_operators.h>
 #include <util/c_types.h>
+#include <util/config.h>
 #include <util/invariant.h>
 #include <util/pointer_expr.h>
 #include <util/pointer_offset_size.h>
@@ -159,6 +160,8 @@ pointer_logict::pointer_logict(const namespacet &_ns):ns(_ns)
 
   // add INVALID
   invalid_object=objects.number(exprt("INVALID"));
+
+  null_is_zero_address = config.ansi_c.NULL_is_zero;
 }
 
 pointer_logict::~pointer_logict()
diff --git a/src/solvers/flattening/pointer_logic.h b/src/solvers/flattening/pointer_logic.h
index 8736c4ae28c..a572f71437e 100644
--- a/src/solvers/flattening/pointer_logic.h
+++ b/src/solvers/flattening/pointer_logic.h
@@ -70,9 +70,15 @@ class pointer_logict
 
   void get_dynamic_objects(std::vector<std::size_t> &objects) const;
 
+  bool get_null_is_zero() const
+  {
+    return null_is_zero_address;
+  }
+
 protected:
   const namespacet &ns;
   std::size_t null_object, invalid_object;
+  bool null_is_zero_address;
 };
 
 #endif // CPROVER_SOLVERS_FLATTENING_POINTER_LOGIC_H
diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
index c4c562226f0..196c22f10c0 100644
--- a/src/solvers/smt2/smt2_conv.cpp
+++ b/src/solvers/smt2/smt2_conv.cpp
@@ -210,10 +210,9 @@ void smt2_convt::define_object_size(
   PRECONDITION(expr.id() == ID_object_size);
   const exprt &ptr = to_unary_expr(expr).op();
   std::size_t size_width = boolbv_width(expr.type());
-  std::size_t pointer_width = boolbv_width(ptr.type());
   std::size_t number = 0;
-  std::size_t h=pointer_width-1;
-  std::size_t l=pointer_width-config.bv_encoding.object_bits;
+  std::size_t object_bits =
+    boolbv_width.get_object_width(to_pointer_type(ptr.type()));
 
   for(const auto &o : pointer_logic.objects)
   {
@@ -230,12 +229,12 @@ void smt2_convt::define_object_size(
       continue;
     }
 
-    out << "(assert (implies (= " <<
-      "((_ extract " << h << " " << l << ") ";
+    out << "(assert (implies (= "
+        << "((_ extract " << object_bits - 1 << " 0) ";
     convert_expr(ptr);
-    out << ") (_ bv" << number << " " << config.bv_encoding.object_bits << "))"
-        << "(= " << id << " (_ bv" << *object_size << " " << size_width
-        << "))))\n";
+    out << ") (_ bv" << number << " " << object_bits << "))"
+        << "(= " << id << " (_ bv" << object_size->to_ulong() << " "
+        << size_width << "))))\n";
 
     ++number;
   }
@@ -568,10 +567,14 @@ exprt smt2_convt::parse_rec(const irept &src, const typet &type)
     mp_integer v = numeric_cast_v<mp_integer>(bv_expr);
 
     // split into object and offset
-    mp_integer pow=power(2, width-config.bv_encoding.object_bits);
+    std::size_t object_bits =
+      boolbv_width.get_object_width(to_pointer_type(type));
+    std::size_t offset_bits =
+      boolbv_width.get_offset_width(to_pointer_type(type));
+    mp_integer pow = power(2, object_bits);
     pointer_logict::pointert ptr;
-    ptr.object = numeric_cast_v<std::size_t>(v / pow);
-    ptr.offset=v%pow;
+    ptr.object = numeric_cast_v<std::size_t>(v % pow);
+    ptr.offset = (v % power(2, object_bits + offset_bits)) / pow;
     return pointer_logic.pointer_expr(ptr, to_pointer_type(type));
   }
   else if(type.id()==ID_struct)
@@ -614,12 +617,18 @@ void smt2_convt::convert_address_of_rec(
      expr.id()==ID_string_constant ||
      expr.id()==ID_label)
   {
-    out
-      << "(concat (_ bv"
-      << pointer_logic.add_object(expr) << " "
-      << config.bv_encoding.object_bits << ")"
-      << " (_ bv0 "
-      << boolbv_width(result_type)-config.bv_encoding.object_bits << "))";
+    std::string addr =
+      expr.id() == ID_symbol
+        ? expr.get_string(ID_identifier) + "$address"
+        : "(_ bv0 " +
+            std::to_string(boolbv_width.get_address_width(result_type)) + ")";
+
+    out << "(concat "
+        << "(concat "
+        << "(_ bv" << pointer_logic.add_object(expr) << " "
+        << boolbv_width.get_object_width(result_type) << ") "
+        << "(_ bv0 " << boolbv_width.get_offset_width(result_type) << ")) "
+        << addr << ")";
   }
   else if(expr.id()==ID_index)
   {
@@ -1424,23 +1433,21 @@ void smt2_convt::convert_expr(const exprt &expr)
       op.type().id() == ID_pointer,
       "operand of pointer offset expression shall be of pointer type");
 
+    std::size_t object_bits =
+      boolbv_width.get_object_width(to_pointer_type(op.type()));
     std::size_t offset_bits =
-      boolbv_width(op.type()) - config.bv_encoding.object_bits;
-    std::size_t result_width=boolbv_width(expr.type());
+      boolbv_width.get_offset_width(to_pointer_type(op.type()));
+    std::size_t ext = boolbv_width(expr.type()) - offset_bits;
 
-    // max extract width
-    if(offset_bits>result_width)
-      offset_bits=result_width;
-
-    // too few bits?
-    if(result_width>offset_bits)
-      out << "((_ zero_extend " << result_width-offset_bits << ") ";
+    if(ext > 0)
+      out << "((_ zero_extend " << ext << ") ";
 
-    out << "((_ extract " << offset_bits-1 << " 0) ";
+    out << "((_ extract " << object_bits + offset_bits - 1 << " " << object_bits
+        << ") ";
     convert_expr(op);
     out << ")";
 
-    if(result_width>offset_bits)
+    if(ext > 0)
       out << ")"; // zero_extend
   }
   else if(expr.id()==ID_pointer_object)
@@ -1451,15 +1458,14 @@ void smt2_convt::convert_expr(const exprt &expr)
       op.type().id() == ID_pointer,
       "pointer object expressions should be of pointer type");
 
-    std::size_t ext=boolbv_width(expr.type())-config.bv_encoding.object_bits;
-    std::size_t pointer_width = boolbv_width(op.type());
+    std::size_t object_bits =
+      boolbv_width.get_object_width(to_pointer_type(op.type()));
+    std::size_t ext = boolbv_width(expr.type()) - object_bits;
 
     if(ext>0)
       out << "((_ zero_extend " << ext << ") ";
 
-    out << "((_ extract "
-        << pointer_width-1 << " "
-        << pointer_width-config.bv_encoding.object_bits << ") ";
+    out << "((_ extract " << object_bits - 1 << " 0) ";
     convert_expr(op);
     out << ")";
 
@@ -1472,14 +1478,13 @@ void smt2_convt::convert_expr(const exprt &expr)
   }
   else if(expr.id() == ID_is_invalid_pointer)
   {
-    const auto &op = to_unary_expr(expr).op();
-    std::size_t pointer_width = boolbv_width(op.type());
-    out << "(= ((_ extract "
-        << pointer_width-1 << " "
-        << pointer_width-config.bv_encoding.object_bits << ") ";
-    convert_expr(op);
-    out << ") (_ bv" << pointer_logic.get_invalid_object()
-        << " " << config.bv_encoding.object_bits << "))";
+    std::size_t object_bits = boolbv_width.get_object_width(
+      to_pointer_type(to_unary_expr(expr).op().type()));
+
+    out << "(= ((_ extract " << object_bits - 1 << " 0) ";
+    convert_expr(to_unary_expr(expr).op());
+    out << ") (_ bv" << pointer_logic.get_invalid_object() << " " << object_bits
+        << "))";
   }
   else if(expr.id()==ID_string_constant)
   {
@@ -2956,30 +2961,28 @@ void smt2_convt::convert_is_dynamic_object(const unary_exprt &expr)
   std::vector<std::size_t> dynamic_objects;
   pointer_logic.get_dynamic_objects(dynamic_objects);
 
+  std::size_t object_bits =
+    boolbv_width.get_object_width(to_pointer_type(expr.op().type()));
+
   if(dynamic_objects.empty())
     out << "false";
   else
   {
-    std::size_t pointer_width = boolbv_width(expr.op().type());
-
-    out << "(let ((?obj ((_ extract "
-        << pointer_width-1 << " "
-        << pointer_width-config.bv_encoding.object_bits << ") ";
+    out << "(let ((?obj ((_ extract " << object_bits << " 0) ";
     convert_expr(expr.op());
     out << "))) ";
 
     if(dynamic_objects.size()==1)
     {
-      out << "(= (_ bv" << dynamic_objects.front()
-          << " " << config.bv_encoding.object_bits << ") ?obj)";
+      out << "(= (_ bv" << dynamic_objects.front() << " " << object_bits
+          << ") ?obj)";
     }
     else
     {
       out << "(or";
 
       for(const auto &object : dynamic_objects)
-        out << " (= (_ bv" << object
-            << " " << config.bv_encoding.object_bits << ") ?obj)";
+        out << " (= (_ bv" << object << " " << object_bits << ") ?obj)";
 
       out << ")"; // or
     }