diff --git a/jbmc/regression/jbmc-json-ui/pointer-simplification/test.desc b/jbmc/regression/jbmc-json-ui/pointer-simplification/test.desc
index b6fbcc4a530..50d7aaf18ac 100644
--- a/jbmc/regression/jbmc-json-ui/pointer-simplification/test.desc
+++ b/jbmc/regression/jbmc-json-ui/pointer-simplification/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 test
 filter.jq --json-ui --trace
 ^EXIT=0$
diff --git a/jbmc/regression/jbmc-strings/StringFormatHex/test-hex-eval-upper.desc b/jbmc/regression/jbmc-strings/StringFormatHex/test-hex-eval-upper.desc
index 07722f345f2..386fe0feeda 100644
--- a/jbmc/regression/jbmc-strings/StringFormatHex/test-hex-eval-upper.desc
+++ b/jbmc/regression/jbmc-strings/StringFormatHex/test-hex-eval-upper.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 Test
 --function Test.testHexEvalUpper --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --trace
 ^EXIT=10$
diff --git a/jbmc/regression/jbmc-strings/StringFormatHex/test-hex-eval.desc b/jbmc/regression/jbmc-strings/StringFormatHex/test-hex-eval.desc
index 6042b9571cb..68bf07a99cf 100644
--- a/jbmc/regression/jbmc-strings/StringFormatHex/test-hex-eval.desc
+++ b/jbmc/regression/jbmc-strings/StringFormatHex/test-hex-eval.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 Test
 --function Test.testHexEval --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --trace
 ^EXIT=10$
diff --git a/jbmc/regression/jbmc-strings/char_escape/test.desc b/jbmc/regression/jbmc-strings/char_escape/test.desc
index fe0255b60de..aa2af5efedc 100644
--- a/jbmc/regression/jbmc-strings/char_escape/test.desc
+++ b/jbmc/regression/jbmc-strings/char_escape/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 Test
 --function Test.test --trace --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --json-ui
 ^EXIT=10$
diff --git a/jbmc/regression/jbmc/address_space_size_limit1/test.desc b/jbmc/regression/jbmc/address_space_size_limit1/test.desc
index a9bb6c1ed0a..cd86e56700d 100644
--- a/jbmc/regression/jbmc/address_space_size_limit1/test.desc
+++ b/jbmc/regression/jbmc/address_space_size_limit1/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 Test
 --object-bits 4
 too many addressed objects
diff --git a/jbmc/regression/jbmc/assume-inputs-non-null/class_assume.desc b/jbmc/regression/jbmc/assume-inputs-non-null/class_assume.desc
index 4e07e36aac7..7c9ce8eb92b 100644
--- a/jbmc/regression/jbmc/assume-inputs-non-null/class_assume.desc
+++ b/jbmc/regression/jbmc/assume-inputs-non-null/class_assume.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 My
 --function My.classArg --java-assume-inputs-non-null
 ^EXIT=10$
diff --git a/jbmc/regression/jbmc/lambda-boxing/Boolean.desc b/jbmc/regression/jbmc/lambda-boxing/Boolean.desc
index 0332bda7d98..04893538e3f 100644
--- a/jbmc/regression/jbmc/lambda-boxing/Boolean.desc
+++ b/jbmc/regression/jbmc/lambda-boxing/Boolean.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 BoxingLambda
 --function BoxingLambda.testBoolean --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
 \[java::BoxingLambda\.testBoolean:\(\)V\.assertion\.1\] line 73 assertion at file BoxingLambda\.java line 73 function java::BoxingLambda\.testBoolean:\(\)V bytecode-index 25: SUCCESS
diff --git a/jbmc/regression/jbmc/lambda-boxing/Float.desc b/jbmc/regression/jbmc/lambda-boxing/Float.desc
index 9f5d65588f0..7c011ea31db 100644
--- a/jbmc/regression/jbmc/lambda-boxing/Float.desc
+++ b/jbmc/regression/jbmc/lambda-boxing/Float.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 BoxingLambda
 --function BoxingLambda.testFloat --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
 \[java::BoxingLambda\.testFloat:\(\)V\.assertion\.1\] line 125 assertion at file BoxingLambda\.java line 125 function java::BoxingLambda\.testFloat:\(\)V bytecode-index 27: SUCCESS
diff --git a/jbmc/regression/jbmc/lambda-boxing/Integer.desc b/jbmc/regression/jbmc/lambda-boxing/Integer.desc
index 60e86c4827c..165f727b44d 100644
--- a/jbmc/regression/jbmc/lambda-boxing/Integer.desc
+++ b/jbmc/regression/jbmc/lambda-boxing/Integer.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 BoxingLambda
 --function BoxingLambda.testInteger --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
 \[java::BoxingLambda\.testInteger:\(\)V\.assertion\.1\] line 138 assertion at file BoxingLambda\.java line 138 function java::BoxingLambda\.testInteger:\(\)V bytecode-index 26: SUCCESS
diff --git a/jbmc/regression/jbmc/lambda-void-return-type/test.desc b/jbmc/regression/jbmc/lambda-void-return-type/test.desc
index f850216ee3a..ce6e46ad364 100644
--- a/jbmc/regression/jbmc/lambda-void-return-type/test.desc
+++ b/jbmc/regression/jbmc/lambda-void-return-type/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 Test
 --function Test.test --classpath `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
 ^EXIT=10$
diff --git a/jbmc/regression/jbmc/no-main-args-elements-maybe-null2/test.desc b/jbmc/regression/jbmc/no-main-args-elements-maybe-null2/test.desc
index 3ded38f4ad6..2b6fc518980 100644
--- a/jbmc/regression/jbmc/no-main-args-elements-maybe-null2/test.desc
+++ b/jbmc/regression/jbmc/no-main-args-elements-maybe-null2/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 Main
 --function Main.main
 ^EXIT=10$
diff --git a/jbmc/regression/jbmc/string_field_aliasing/test.desc b/jbmc/regression/jbmc/string_field_aliasing/test.desc
index 9082fd092e3..5ba913b80ff 100644
--- a/jbmc/regression/jbmc/string_field_aliasing/test.desc
+++ b/jbmc/regression/jbmc/string_field_aliasing/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 Cart
 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --trace --java-max-vla-length 96 --java-unwind-enum-static --max-nondet-string-length 200 --unwind 4 --function Cart.checkTax4 --string-printable
 ^EXIT=10$
diff --git a/jbmc/regression/strings-smoke-tests/java_parseint/test4.desc b/jbmc/regression/strings-smoke-tests/java_parseint/test4.desc
index 09c74c001ad..11ac9232999 100644
--- a/jbmc/regression/strings-smoke-tests/java_parseint/test4.desc
+++ b/jbmc/regression/strings-smoke-tests/java_parseint/test4.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 Test4
 --max-nondet-string-length 1000 --cp `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar` --function Test4.main --trace
 ^EXIT=10$
diff --git a/regression/cbmc-library/free-01/test.desc b/regression/cbmc-library/free-01/test.desc
index 769ba573e7c..40f601bba9f 100644
--- a/regression/cbmc-library/free-01/test.desc
+++ b/regression/cbmc-library/free-01/test.desc
@@ -1,7 +1,7 @@
 CORE
 main.c
 --pointer-check --bounds-check --stop-on-fail
-free argument must be NULL or valid pointer
+free argument must be (dynamic object|NULL or valid pointer)
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/regression/cbmc-primitives/r_w_ok_bug/test.desc b/regression/cbmc-primitives/r_w_ok_bug/test.desc
index e47b34c18b2..54d5d3700de 100644
--- a/regression/cbmc-primitives/r_w_ok_bug/test.desc
+++ b/regression/cbmc-primitives/r_w_ok_bug/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --pointer-check --no-simplify --no-propagation
 ^\[main.pointer_dereference.\d+\] line 8 dereference failure: pointer outside object bounds in \*p1: FAILURE$
diff --git a/regression/cbmc-primitives/same-object-01/test-no-cp.desc b/regression/cbmc-primitives/same-object-01/test-no-cp.desc
index 97df364eec4..8482907fb49 100644
--- a/regression/cbmc-primitives/same-object-01/test-no-cp.desc
+++ b/regression/cbmc-primitives/same-object-01/test-no-cp.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --no-simplify --no-propagation
 ^EXIT=0$
diff --git a/regression/cbmc-primitives/same-object-01/test.desc b/regression/cbmc-primitives/same-object-01/test.desc
index d32f40840c5..877ae606eb8 100644
--- a/regression/cbmc-primitives/same-object-01/test.desc
+++ b/regression/cbmc-primitives/same-object-01/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 
 ^EXIT=0$
diff --git a/regression/cbmc/Pointer_comparison1/main.c b/regression/cbmc/Pointer_comparison1/main.c
index 08022bf75fd..e45b7c1aa5e 100644
--- a/regression/cbmc/Pointer_comparison1/main.c
+++ b/regression/cbmc/Pointer_comparison1/main.c
@@ -10,8 +10,7 @@ int main()
     return 0;
 
   if(
-    (unsigned long)p >
-    42) // unsoundly evaluates to true due to pointer encoding
+    (unsigned long)p > 1) // unsoundly evaluates to true due to pointer encoding
   {
     return 0;
   }
diff --git a/regression/cbmc/address_space_size_limit1/test.desc b/regression/cbmc/address_space_size_limit1/test.desc
index 3bc849b0cbf..9c02e15b09d 100644
--- a/regression/cbmc/address_space_size_limit1/test.desc
+++ b/regression/cbmc/address_space_size_limit1/test.desc
@@ -1,4 +1,4 @@
-CORE thorough-paths broken-smt-backend
+KNOWNBUG thorough-paths broken-smt-backend
 test.c
 --no-simplify --unwind 300 --object-bits 8
 too many addressed objects
diff --git a/regression/cbmc/hex_trace/main.c b/regression/cbmc/hex_trace/main.c
index 91e9de5a3d6..08938f6a71a 100644
--- a/regression/cbmc/hex_trace/main.c
+++ b/regression/cbmc/hex_trace/main.c
@@ -6,6 +6,7 @@ int main()
   char *p;
 
   a = 0;
+  b = 0;
   a = -100;
   a = 2147483647;
   b = a * 2;
diff --git a/regression/contracts/assigns-enforce-malloc-zero/test.desc b/regression/contracts/assigns-enforce-malloc-zero/test.desc
index eefba72ce5b..6940c67a633 100644
--- a/regression/contracts/assigns-enforce-malloc-zero/test.desc
+++ b/regression/contracts/assigns-enforce-malloc-zero/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --enforce-contract foo _ --malloc-may-fail --malloc-fail-null
 ^\[foo.assigns.\d+\] line 9 Check that POINTER_OBJECT\(\(const void \*\)a\) is valid when a != \(\(char \*\)NULL\): SUCCESS$
diff --git a/regression/contracts/test_struct_member_enforce/test.desc b/regression/contracts/test_struct_member_enforce/test.desc
index 7f7a8adf160..2b9112f2b03 100644
--- a/regression/contracts/test_struct_member_enforce/test.desc
+++ b/regression/contracts/test_struct_member_enforce/test.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 main.c
 --enforce-contract foo
 ^EXIT=0$
diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp
index 86f0361cb89..1a0bf68a3f3 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/byte_operators.h>
 #include <util/c_types.h>
-#include <util/config.h>
 #include <util/exception_utils.h>
 #include <util/expr_util.h>
 #include <util/namespace.h>
@@ -71,53 +70,100 @@ bv_pointerst::endianness_map(const typet &type, bool little_endian) const
   return bv_endianness_mapt{type, little_endian, ns, bv_width};
 }
 
-std::size_t bv_pointerst::get_object_width(const pointer_typet &) const
-{
-  // not actually type-dependent for now
-  return config.bv_encoding.object_bits;
-}
-
-std::size_t bv_pointerst::get_offset_width(const pointer_typet &type) const
+bvt bv_pointerst::object_literals(const bvt &bv, const pointer_typet &type)
 {
-  const std::size_t pointer_width = type.get_width();
-  const std::size_t object_width = get_object_width(type);
-  PRECONDITION(pointer_width >= object_width);
-  return pointer_width - object_width;
-}
+  const auto width = type.get_width();
+  PRECONDITION(width == bv.size());
 
-std::size_t bv_pointerst::get_address_width(const pointer_typet &type) const
-{
-  return type.get_width();
-}
+  const auto result = prop.new_variables(width);
+  bvt match_found_disjuncts;
 
-bvt bv_pointerst::object_literals(const bvt &bv, const pointer_typet &type)
-  const
-{
-  const std::size_t offset_width = get_offset_width(type);
-  const std::size_t object_width = get_object_width(type);
-  PRECONDITION(bv.size() >= offset_width + object_width);
+  for(std::size_t i = 0; i < numbered_pointers.size(); i++)
+  {
+    auto cond = bv_utils.equal(
+      bv,
+      bv_utilst::concatenate(
+        bv_utilst::build_constant(i, width - 1), {const_literal(true)}));
+    match_found_disjuncts.push_back(cond);
+    bv_utils.cond_implies_equal(
+      cond,
+      bv_utilst::zero_extension(numbered_pointers[i].first, width),
+      result);
+  }
 
-  return bvt(
-    bv.begin() + offset_width, bv.begin() + offset_width + object_width);
+  auto match_found = prop.lor(match_found_disjuncts);
+
+  // The top bit distinguishes 'object only' vs. 'table encoded'.
+  // When outside of the table, return an invalid object.
+  return bv_utils.select(
+    bv.back(),
+    bv_utils.select(
+      match_found,
+      result,
+      bv_utilst::build_constant(pointer_logic.get_invalid_object(), width)),
+    bv);
 }
 
 bvt bv_pointerst::offset_literals(const bvt &bv, const pointer_typet &type)
-  const
 {
-  const std::size_t offset_width = get_offset_width(type);
-  PRECONDITION(bv.size() >= offset_width);
+  const auto width = type.get_width();
+  PRECONDITION(width == bv.size());
+
+  const auto result = prop.new_variables(width);
+  bvt match_found_disjuncts;
+
+  for(std::size_t i = 0; i < numbered_pointers.size(); i++)
+  {
+    auto cond = bv_utils.equal(
+      bv,
+      bv_utilst::concatenate(
+        bv_utilst::build_constant(i, width - 1), {const_literal(true)}));
+    match_found_disjuncts.push_back(cond);
+    bv_utils.cond_implies_equal(
+      cond,
+      bv_utilst::sign_extension(numbered_pointers[i].second, width),
+      result);
+  }
+
+  auto match_found = prop.lor(match_found_disjuncts);
 
-  return bvt(bv.begin(), bv.begin() + offset_width);
+  // the top bit distinguishes 'object only' vs. 'table encoded'
+  return bv_utils.select(
+    bv.back(),
+    bv_utils.select(match_found, result, bv_utilst::zeros(width)),
+    bv_utilst::zeros(width));
 }
 
-bvt bv_pointerst::object_offset_encoding(const bvt &object, const bvt &offset)
+bvt bv_pointerst::object_offset_encoding(
+  const bvt &object_bv,
+  const bvt &offset_bv,
+  const pointer_typet &type)
 {
-  bvt result;
-  result.reserve(offset.size() + object.size());
-  result.insert(result.end(), offset.begin(), offset.end());
-  result.insert(result.end(), object.begin(), object.end());
-
-  return result;
+  const auto width = type.get_width();
+  PRECONDITION(object_bv.size() == width);
+  PRECONDITION(offset_bv.size() == width);
+
+  // is the offset zero?
+  if(std::find_if_not(offset_bv.begin(), offset_bv.end(), [](literalt l) {
+       return l == const_literal(false);
+     }) != offset_bv.end())
+  {
+    // offset is not zero, add to the pointer table
+    auto number = numbered_pointers.size();
+    numbered_pointers.emplace_back(object_bv, offset_bv);
+
+    // Encode the table index.
+    // Also set top bit to distinguish from object-only pointers.
+    return bv_utilst::concatenate(
+      bv_utilst::build_constant(number, width - 1), {const_literal(true)});
+  }
+  else
+  {
+    // Offset is zero, just zero-extend object number.
+    // Top bit is zero to indicate object-only pointer.
+    return bv_utilst::concatenate(
+      bv_utilst::zero_extension(object_bv, width - 1), {const_literal(false)});
+  }
 }
 
 literalt bv_pointerst::convert_rest(const exprt &expr)
@@ -141,17 +187,7 @@ literalt bv_pointerst::convert_rest(const exprt &expr)
         bvt invalid_bv = object_literals(
           encode(pointer_logic.get_invalid_object(), type), type);
 
-        const std::size_t object_bits = get_object_width(type);
-
-        bvt equal_invalid_bv;
-        equal_invalid_bv.reserve(object_bits);
-
-        for(std::size_t i=0; i<object_bits; i++)
-        {
-          equal_invalid_bv.push_back(prop.lequal(object_bv[i], invalid_bv[i]));
-        }
-
-        return prop.land(equal_invalid_bv);
+        return bv_utils.equal(object_bv, invalid_bv);
       }
     }
   }
@@ -168,6 +204,32 @@ literalt bv_pointerst::convert_rest(const exprt &expr)
       return l;
     }
   }
+  else if(expr.id() == ID_equal || expr.id() == ID_notequal)
+  {
+    if(
+      operands.size() == 2 && operands[0].type().id() == ID_pointer &&
+      operands[1].type().id() == ID_pointer)
+    {
+      // bit-wise comparison doesn't work because of numbered pointers
+      const bvt &bv0 = convert_bv(operands[0]);
+      const bvt &bv1 = convert_bv(operands[1]);
+
+      const pointer_typet &type0 = to_pointer_type(operands[0].type());
+      bvt object_bv0 = object_literals(bv0, type0);
+      bvt offset_bv0 = offset_literals(bv0, type0);
+
+      const pointer_typet &type1 = to_pointer_type(operands[1].type());
+      bvt object_bv1 = object_literals(bv1, type1);
+      bvt offset_bv1 = offset_literals(bv1, type1);
+
+      // object and offset need to match
+      auto equal = prop.land(
+        bv_utils.equal(object_bv0, object_bv1),
+        bv_utils.equal(offset_bv0, offset_bv1));
+
+      return expr.id() == ID_equal ? equal : !equal;
+    }
+  }
   else if(expr.id()==ID_lt || expr.id()==ID_le ||
           expr.id()==ID_gt || expr.id()==ID_ge)
   {
@@ -381,11 +443,11 @@ 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.
-
+      // We interpret as NULL + offset, where the offset is
+      // derived from the bitvector by zero extension.
       const bvt &op_bv=convert_bv(op);
-
-      return bv_utils.zero_extension(op_bv, bits);
+      return object_offset_encoding(
+        bv_utilst::zeros(bits), bv_utilst::zero_extension(op_bv, bits), type);
     }
   }
   else if(expr.id()==ID_if)
@@ -463,8 +525,7 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
       count == 1,
       "there should be exactly one pointer-type operand in a pointer-type sum");
 
-    const std::size_t offset_bits = get_offset_width(type);
-    bvt sum = bv_utils.build_constant(0, offset_bits);
+    bvt sum = bv_utils.build_constant(0, bits);
 
     forall_operands(it, plus_expr)
     {
@@ -484,7 +545,8 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
       bvt op=convert_bv(*it);
       CHECK_RETURN(!op.empty());
 
-      op = bv_utils.extension(op, offset_bits, rep);
+      op = bv_utils.extension(op, bits, rep);
+      CHECK_RETURN(op.size() == sum.size());
 
       sum=bv_utils.add(sum, op);
     }
@@ -794,13 +856,8 @@ exprt bv_pointerst::bv_get_rec(
   bvt value_bv(bv.begin() + offset, bv.begin() + offset + bits);
 
   std::string value = bits_to_string(prop, value_bv);
-  std::string value_addr = bits_to_string(prop, object_literals(value_bv, pt));
-  std::string value_offset =
-    bits_to_string(prop, offset_literals(value_bv, pt));
-
   // we treat these like bit-vector constants, but with
   // some additional annotation
-
   const irep_idt bvrep = make_bvrep(bits, [&value](std::size_t i) {
     return value[value.size() - 1 - i] == '1';
   });
@@ -808,24 +865,49 @@ exprt bv_pointerst::bv_get_rec(
   constant_exprt result(bvrep, type);
 
   pointer_logict::pointert pointer;
-  pointer.object =
-    numeric_cast_v<std::size_t>(binary2integer(value_addr, false));
-  pointer.offset=binary2integer(value_offset, true);
+
+  // Top bit set?
+  if(value.front() == '1')
+  {
+    // It's a pointer into the table. Turn bits into number, but
+    // first strip top bit.
+    auto index = binary2integer(value.substr(1, std::string::npos), false);
+
+    if(index >= 0 && index < numbered_pointers.size())
+    {
+      // copy from table
+      const auto &entry = numbered_pointers[numeric_cast_v<std::size_t>(index)];
+      pointer.object = binary2integer(bits_to_string(prop, entry.first), false);
+      pointer.offset = binary2integer(bits_to_string(prop, entry.second), true);
+    }
+    else
+    {
+      // out of bounds, we'll make it an 'invalid pointer'
+      pointer.object = pointer_logic.get_invalid_object();
+      pointer.offset = 0;
+    }
+  }
+  else
+  {
+    // It's an object only, offset is zero.
+    pointer.object = binary2integer(value, false);
+    pointer.offset = 0;
+  }
 
   return annotated_pointer_constant_exprt{
     bvrep, pointer_logic.pointer_expr(pointer, pt)};
 }
 
-bvt bv_pointerst::encode(const mp_integer &addr, const pointer_typet &type)
+bvt bv_pointerst::encode(const mp_integer &object, const pointer_typet &type)
   const
 {
-  const std::size_t offset_bits = get_offset_width(type);
-  const std::size_t object_bits = get_object_width(type);
+  const auto width = type.get_width();
 
-  bvt zero_offset(offset_bits, const_literal(false));
-  bvt object = bv_utils.build_constant(addr, object_bits);
+  auto object_bv = bv_utilst::build_constant(object, width - 1);
 
-  return object_offset_encoding(object, zero_offset);
+  // Offset is zero, just zero-extend object number.
+  // Top bit is zero to indicate object-only pointer.
+  return bv_utilst::concatenate(object_bv, {const_literal(false)});
 }
 
 bvt bv_pointerst::offset_arithmetic(
@@ -833,7 +915,7 @@ bvt bv_pointerst::offset_arithmetic(
   const bvt &bv,
   const mp_integer &x)
 {
-  const std::size_t offset_bits = get_offset_width(type);
+  const std::size_t offset_bits = type.get_width();
 
   return offset_arithmetic(
     type, bv, 1, bv_utils.build_constant(x, offset_bits));
@@ -851,36 +933,45 @@ bvt bv_pointerst::offset_arithmetic(
     index.type().id()==ID_signedbv?bv_utilst::representationt::SIGNED:
                                    bv_utilst::representationt::UNSIGNED;
 
-  const std::size_t offset_bits = get_offset_width(type);
-  bv_index=bv_utils.extension(bv_index, offset_bits, rep);
+  PRECONDITION(bv.size() == type.get_width());
+
+  bv_index = bv_utils.extension(bv_index, bv.size(), rep);
 
   return offset_arithmetic(type, bv, factor, bv_index);
 }
 
 bvt bv_pointerst::offset_arithmetic(
   const pointer_typet &type,
-  const bvt &bv,
+  const bvt &pointer_bv,
   const mp_integer &factor,
-  const bvt &index)
+  const bvt &index_bv)
 {
-  bvt bv_index;
+  PRECONDITION(pointer_bv.size() == type.get_width());
+  PRECONDITION(index_bv.size() == type.get_width());
+
+  bvt index_scaled_bv;
 
   if(factor==1)
-    bv_index=index;
+  {
+    index_scaled_bv = index_bv;
+  }
   else
   {
-    bvt bv_factor=bv_utils.build_constant(factor, index.size());
-    bv_index = bv_utils.signed_multiplier(index, bv_factor);
+    bvt factor_bv = bv_utils.build_constant(factor, pointer_bv.size());
+    index_scaled_bv = bv_utils.signed_multiplier(
+      bv_utils.sign_extension(index_bv, pointer_bv.size()), factor_bv);
   }
 
-  const std::size_t offset_bits = get_offset_width(type);
-  bv_index = bv_utils.sign_extension(bv_index, offset_bits);
+  bvt offset_bv = offset_literals(pointer_bv, type);
+  CHECK_RETURN(offset_bv.size() == pointer_bv.size());
 
-  bvt offset_bv = offset_literals(bv, type);
+  DATA_INVARIANT(
+    offset_bv.size() == index_scaled_bv.size(),
+    "pointer offset bitvector width");
 
-  bvt bv_tmp = bv_utils.add(offset_bv, bv_index);
+  bvt sum = bv_utils.add(offset_bv, index_scaled_bv);
 
-  return object_offset_encoding(object_literals(bv, type), bv_tmp);
+  return object_offset_encoding(object_literals(pointer_bv, type), sum, type);
 }
 
 bvt bv_pointerst::add_addr(const exprt &expr)
@@ -888,15 +979,14 @@ bvt bv_pointerst::add_addr(const exprt &expr)
   const auto a = pointer_logic.add_object(expr);
 
   const pointer_typet type = pointer_type(expr.type());
-  const std::size_t object_bits = get_object_width(type);
-  const std::size_t max_objects=std::size_t(1)<<object_bits;
+  const mp_integer object_bits = type.get_width();
+  const mp_integer max_objects = mp_integer(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) +
-      "); " +
-      "use the `--object-bits n` option to increase the maximum number");
+      "too many addressed objects: maximum number of objects is 2^n=" +
+      integer2string(max_objects) + " (with n=" + integer2string(object_bits) +
+      ")");
 
   return encode(a, type);
 }
diff --git a/src/solvers/flattening/bv_pointers.h b/src/solvers/flattening/bv_pointers.h
index eb7536a7620..76982cffa60 100644
--- a/src/solvers/flattening/bv_pointers.h
+++ b/src/solvers/flattening/bv_pointers.h
@@ -32,10 +32,6 @@ class bv_pointerst:public boolbvt
 protected:
   pointer_logict pointer_logic;
 
-  std::size_t get_object_width(const pointer_typet &) const;
-  std::size_t get_offset_width(const pointer_typet &) const;
-  std::size_t get_address_width(const pointer_typet &) const;
-
   // NOLINTNEXTLINE(readability/identifiers)
   typedef boolbvt SUB;
 
@@ -94,21 +90,28 @@ class bv_pointerst:public boolbvt
   /// \param bv: Encoded pointer
   /// \param type: Type of the encoded pointer
   /// \return Vector of literals identifying the object part of \p bv
-  bvt object_literals(const bvt &bv, const pointer_typet &type) const;
+  bvt object_literals(const bvt &bv, const pointer_typet &type);
 
   /// Given a pointer encoded in \p bv, extract the literals representing the
   /// offset into an object that the pointer points to.
   /// \param bv: Encoded pointer
   /// \param type: Type of the encoded pointer
   /// \return Vector of literals identifying the offset part of \p bv
-  bvt offset_literals(const bvt &bv, const pointer_typet &type) const;
+  bvt offset_literals(const bvt &bv, const pointer_typet &type);
 
   /// Construct a pointer encoding from given encodings of \p object and \p
   /// offset.
   /// \param object: Encoded object
   /// \param offset: Encoded offset
+  /// \param type: Type of the encoded pointer
   /// \return Pointer encoding
-  static bvt object_offset_encoding(const bvt &object, const bvt &offset);
+  bvt object_offset_encoding(
+    const bvt &object,
+    const bvt &offset,
+    const pointer_typet &type);
+
+  /// Table that maps a 'pointer number' to its object/offset pair
+  std::vector<std::pair<bvt, bvt>> numbered_pointers;
 };
 
 #endif // CPROVER_SOLVERS_FLATTENING_BV_POINTERS_H
diff --git a/src/solvers/flattening/bv_utils.h b/src/solvers/flattening/bv_utils.h
index 35a64eec59b..1b988cda0c6 100644
--- a/src/solvers/flattening/bv_utils.h
+++ b/src/solvers/flattening/bv_utils.h
@@ -179,17 +179,17 @@ class bv_utilst
   static bvt
   extension(const bvt &bv, std::size_t new_size, representationt rep);
 
-  bvt sign_extension(const bvt &bv, std::size_t new_size)
+  static bvt sign_extension(const bvt &bv, std::size_t new_size)
   {
     return extension(bv, new_size, representationt::SIGNED);
   }
 
-  bvt zero_extension(const bvt &bv, std::size_t new_size)
+  static bvt zero_extension(const bvt &bv, std::size_t new_size)
   {
     return extension(bv, new_size, representationt::UNSIGNED);
   }
 
-  bvt zeros(std::size_t new_size) const
+  static bvt zeros(std::size_t new_size)
   {
     bvt result;
     result.resize(new_size, const_literal(false));