diff --git a/doc/cprover-manual/goto-cc.md b/doc/cprover-manual/goto-cc.md
index 723cf676e0d..ea36701e2e5 100644
--- a/doc/cprover-manual/goto-cc.md
+++ b/doc/cprover-manual/goto-cc.md
@@ -132,9 +132,6 @@ most important architectural parameters are:
     `sizeof(long int)` on various machines.
 -   The width of pointers; for example, compare the value of `sizeof(int *)` on
     various machines.
--   The number of bits in a pointer which are used to differentiate between
-    different objects. The remaining bits of a pointer are used for offsets
-    within objects.
 -   The [endianness](http://en.wikipedia.org/wiki/Endianness) of
     the architecture.
 
@@ -152,8 +149,6 @@ following command-line arguments can be passed to the CPROVER tools:
 -   The word-width can be set with `--16`, `--32`, `--64`.
 -   The endianness can be defined with `--little-endian` and
     `--big-endian`.
--   The number of bits in a pointer used to differentiate between different
-    objects can be set using `--object-bits x`. Where `x` is the number of bits.
 
 When using a goto binary, CBMC and the other tools read the
 configuration from the binary. The setting when running goto-cc is
diff --git a/doc/man/goto-cc.1 b/doc/man/goto-cc.1
index 66f951902ae..8d06cdcf067 100644
--- a/doc/man/goto-cc.1
+++ b/doc/man/goto-cc.1
@@ -96,9 +96,10 @@ files.
 .TP
 \fB\-\-print\-rejected\-preprocessed\-source\fR \fIfile\fR
 Copy failing (preprocessed) source to \fIfile\fR.
-.TP
-\fB\-\-object\-bits\fR \fIN\fR
-Configure the number of bits used for object numbering in CBMC's pointer encoding.
+.SH BACKWARD COMPATIBILITY
+.B goto\-cc
+will warn and ignore the use of \fB\-\-object\-bits\fR, which previous versions
+processed. This option now instead needs to be passed to \fBcbmc\fR(1).
 .SH ENVIRONMENT
 All tools honor the TMPDIR environment variable when generating temporary
 files and directories.
diff --git a/regression/CMakeLists.txt b/regression/CMakeLists.txt
index f243fd2087c..ea9c02a753d 100644
--- a/regression/CMakeLists.txt
+++ b/regression/CMakeLists.txt
@@ -63,7 +63,6 @@ else()
   add_subdirectory(goto-cl)
 endif()
 add_subdirectory(goto-cc-cbmc)
-add_subdirectory(goto-cc-cbmc-shared-options)
 add_subdirectory(cbmc-cpp)
 add_subdirectory(goto-cc-goto-analyzer)
 add_subdirectory(goto-analyzer-simplify)
diff --git a/regression/Makefile b/regression/Makefile
index c29abf01af7..7206f57bf21 100644
--- a/regression/Makefile
+++ b/regression/Makefile
@@ -36,7 +36,6 @@ DIRS = cbmc-shadow-memory \
        goto-gcc \
        goto-cl \
        goto-cc-cbmc \
-       goto-cc-cbmc-shared-options \
        cbmc-cpp \
        goto-cc-goto-analyzer \
        goto-analyzer-simplify \
diff --git a/regression/cbmc/simplify_singleton_interval_7690/singleton_interval_in_assume_7690.c b/regression/cbmc/simplify_singleton_interval_7690/singleton_interval_in_assume_7690.c
index f382fe03dfb..736b9513e0d 100644
--- a/regression/cbmc/simplify_singleton_interval_7690/singleton_interval_in_assume_7690.c
+++ b/regression/cbmc/simplify_singleton_interval_7690/singleton_interval_in_assume_7690.c
@@ -5,8 +5,6 @@
 #include <stdlib.h>
 #include <stdint.h>
 
-extern size_t __CPROVER_max_malloc_size;
-
 #if defined(_WIN32) && defined(_M_X64)
 int __builtin_clzll(unsigned long long);
 #define __nof_symex_objects                                                    \
diff --git a/regression/contracts-dfcc/memory-predicates-pointer-in-range-requires/test.desc b/regression/contracts-dfcc/memory-predicates-pointer-in-range-requires/test.desc
index 52123718dcc..93a74386fc2 100644
--- a/regression/contracts-dfcc/memory-predicates-pointer-in-range-requires/test.desc
+++ b/regression/contracts-dfcc/memory-predicates-pointer-in-range-requires/test.desc
@@ -1,4 +1,4 @@
-CORE dfcc-only
+THOROUGH dfcc-only
 main.c
 --malloc-may-fail --malloc-fail-null --dfcc main --enforce-contract foo _ --pointer-check --pointer-primitive-check
 ^EXIT=0$
diff --git a/regression/goto-cc-cbmc-shared-options/CMakeLists.txt b/regression/goto-cc-cbmc-shared-options/CMakeLists.txt
deleted file mode 100644
index b29f1a50349..00000000000
--- a/regression/goto-cc-cbmc-shared-options/CMakeLists.txt
+++ /dev/null
@@ -1,11 +0,0 @@
-if(WIN32)
-    set(is_windows true)
-    set(exclude_broken_windows_tests -X winbug)
-else()
-    set(is_windows false)
-    set(exclude_broken_windows_tests "")
-endif()
-
-add_test_pl_tests(
-    "${CMAKE_CURRENT_SOURCE_DIR}/chain.sh $<TARGET_FILE:goto-cc> $<TARGET_FILE:cbmc> ${is_windows}" ${exclude_broken_windows_tests}
-)
diff --git a/regression/goto-cc-cbmc-shared-options/Makefile b/regression/goto-cc-cbmc-shared-options/Makefile
deleted file mode 100644
index 0ac48438476..00000000000
--- a/regression/goto-cc-cbmc-shared-options/Makefile
+++ /dev/null
@@ -1,30 +0,0 @@
-default: tests.log
-
-include ../../src/config.inc
-include ../../src/common
-
-ifeq ($(BUILD_ENV_),MSVC)
-	exe=../../../src/goto-cc/goto-cl
-	is_windows=true
-	exclude_broken_windows_tests=-X winbug
-else
-	exe=../../../src/goto-cc/goto-cc
-	is_windows=false
-	exclude_broken_windows_tests=
-endif
-
-test:
-	@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/cbmc/cbmc $(is_windows)' $(exclude_broken_windows_tests)
-
-tests.log:
-	@../test.pl -e -p -c '../chain.sh $(exe) ../../../src/cbmc/cbmc $(is_windows)' $(exclude_broken_windows_tests)
-
-clean:
-	@for dir in *; do \
-		$(RM) tests.log; \
-		if [ -d "$$dir" ]; then \
-			cd "$$dir"; \
-			$(RM) *.out *.gb; \
-			cd ..; \
-		fi \
-	done
diff --git a/regression/goto-cc-cbmc-shared-options/README.md b/regression/goto-cc-cbmc-shared-options/README.md
deleted file mode 100644
index ed104e3d6ab..00000000000
--- a/regression/goto-cc-cbmc-shared-options/README.md
+++ /dev/null
@@ -1,4 +0,0 @@
-This directory is for tests where we -
- 1) Run `goto-cc` on the specified input file, with the specified options.
- 2) Run `cbmc` on the goto binary produced in step 1. Using the same options
-    from the `.desc` file as were specified in step 1.
diff --git a/regression/goto-cc-cbmc-shared-options/chain.sh b/regression/goto-cc-cbmc-shared-options/chain.sh
deleted file mode 100755
index 1adc624a11b..00000000000
--- a/regression/goto-cc-cbmc-shared-options/chain.sh
+++ /dev/null
@@ -1,20 +0,0 @@
-#!/usr/bin/env bash
-
-set -e
-
-goto_cc=$1
-cbmc=$2
-is_windows=$3
-
-options=${*:4:$#-4}
-name=${*:$#}
-base_name=${name%.c}
-base_name=${base_name%.cpp}
-
-if [[ "${is_windows}" == "true" ]]; then
-  "${goto_cc}" "${name}" ${options} "/Fe${base_name}.gb"
-else
-  "${goto_cc}" "${name}" -o "${base_name}.gb" ${options}
-fi
-
-"${cbmc}" "${base_name}.gb" ${options}
diff --git a/regression/goto-cc-cbmc-shared-options/object-bits/default_bits.desc b/regression/goto-cc-cbmc/object-bits/default_bits.desc
similarity index 100%
rename from regression/goto-cc-cbmc-shared-options/object-bits/default_bits.desc
rename to regression/goto-cc-cbmc/object-bits/default_bits.desc
diff --git a/regression/goto-cc-cbmc-shared-options/object-bits/fewer_bits.desc b/regression/goto-cc-cbmc/object-bits/fewer_bits.desc
similarity index 96%
rename from regression/goto-cc-cbmc-shared-options/object-bits/fewer_bits.desc
rename to regression/goto-cc-cbmc/object-bits/fewer_bits.desc
index 32723acdbbb..ed34ce893c4 100644
--- a/regression/goto-cc-cbmc-shared-options/object-bits/fewer_bits.desc
+++ b/regression/goto-cc-cbmc/object-bits/fewer_bits.desc
@@ -1,4 +1,4 @@
-CORE winbug
+CORE
 test.c
 --function main --object-bits 6
 ^EXIT=10$
diff --git a/regression/goto-cc-cbmc-shared-options/object-bits/more_bits.desc b/regression/goto-cc-cbmc/object-bits/more_bits.desc
similarity index 96%
rename from regression/goto-cc-cbmc-shared-options/object-bits/more_bits.desc
rename to regression/goto-cc-cbmc/object-bits/more_bits.desc
index a0f25c0b4aa..cabc3e744d2 100644
--- a/regression/goto-cc-cbmc-shared-options/object-bits/more_bits.desc
+++ b/regression/goto-cc-cbmc/object-bits/more_bits.desc
@@ -1,4 +1,4 @@
-CORE winbug
+CORE
 test.c
 --function main --object-bits 10
 ^EXIT=10$
diff --git a/regression/goto-cc-cbmc-shared-options/object-bits/test.c b/regression/goto-cc-cbmc/object-bits/test.c
similarity index 100%
rename from regression/goto-cc-cbmc-shared-options/object-bits/test.c
rename to regression/goto-cc-cbmc/object-bits/test.c
diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/src/ansi-c/ansi_c_internal_additions.cpp
index 9273f40cfc3..7f2eb517393 100644
--- a/src/ansi-c/ansi_c_internal_additions.cpp
+++ b/src/ansi-c/ansi_c_internal_additions.cpp
@@ -124,34 +124,6 @@ static std::string architecture_string(T value, const char *s)
          std::string(s) + "=" + std::to_string(value) + ";\n";
 }
 
-/// The maximum allocation size is determined by the number of bits that
-/// are left in the pointer of width \p pointer_width.
-///
-/// The allocation size cannot exceed the number represented by the (signed)
-/// offset, otherwise it would not be possible to store a pointer into a
-/// valid bit of memory. Therefore, the max allocation size is
-/// 2^(offset_bits - 1), where the offset bits is the number of bits left in the
-/// pointer after the object bits.
-///
-/// The offset must be signed, as a pointer can point to the end of the memory
-/// block, and needs to be able to point back to the start.
-/// \param pointer_width: The width of the pointer
-/// \param object_bits : The number of bits used to represent the ID
-/// \return The size in bytes of the maximum allocation supported.
-static mp_integer
-max_malloc_size(std::size_t pointer_width, std::size_t object_bits)
-{
-  PRECONDITION(pointer_width >= 1);
-  PRECONDITION(object_bits < pointer_width);
-  PRECONDITION(object_bits >= 1);
-  const auto offset_bits = pointer_width - object_bits;
-  // We require the offset to be able to express upto allocation_size - 1,
-  // but also down to -allocation_size, therefore the size is allowable
-  // is number of bits, less the signed bit.
-  const auto bits_for_positive_offset = offset_bits - 1;
-  return ((mp_integer)1) << (mp_integer)bits_for_positive_offset;
-}
-
 void ansi_c_internal_additions(std::string &code, bool support_float16_type)
 {
   // clang-format off
@@ -175,9 +147,9 @@ void ansi_c_internal_additions(std::string &code, bool support_float16_type)
       CPROVER_PREFIX "size_t size, " CPROVER_PREFIX "bool zero);\n"
     "void " CPROVER_PREFIX "deallocate(void *);\n"
 
-    CPROVER_PREFIX "size_t " CPROVER_PREFIX "max_malloc_size="+
-    integer2string(max_malloc_size(config.ansi_c.pointer_width, config
-    .bv_encoding.object_bits));
+    CPROVER_PREFIX "thread_local " CPROVER_PREFIX "size_t "
+      CPROVER_PREFIX "max_malloc_size="+
+      integer2string(config.max_malloc_size());
   if(config.ansi_c.pointer_width==config.ansi_c.long_int_width)
     code += "UL;\n";
   else if(config.ansi_c.pointer_width==config.ansi_c.long_long_int_width)
diff --git a/src/ansi-c/cprover_library.h b/src/ansi-c/cprover_library.h
index 33c67d980ad..8b760bf2f4f 100644
--- a/src/ansi-c/cprover_library.h
+++ b/src/ansi-c/cprover_library.h
@@ -52,4 +52,5 @@ void cprover_c_library_factory_force_load(
   const std::set<irep_idt> &functions,
   symbol_table_baset &symbol_table,
   message_handlert &message_handler);
+
 #endif // CPROVER_ANSI_C_CPROVER_LIBRARY_H
diff --git a/src/ansi-c/library/cprover.h b/src/ansi-c/library/cprover.h
index 0b0baa23b1b..7e3b5693d25 100644
--- a/src/ansi-c/library/cprover.h
+++ b/src/ansi-c/library/cprover.h
@@ -26,8 +26,11 @@ extern const void *__CPROVER_deallocated;
 extern const void *__CPROVER_memory_leak;
 
 extern int __CPROVER_malloc_failure_mode;
-extern __CPROVER_size_t __CPROVER_max_malloc_size;
 extern __CPROVER_bool __CPROVER_malloc_may_fail;
+// The maximum size of an object that we can handle under the object:offset
+// pointer encoding. Marked thread-local as it is a per-analysis constant that
+// can safely be constant-propagated even in concurrent execution.
+extern __CPROVER_thread_local __CPROVER_size_t __CPROVER_max_malloc_size;
 
 // malloc failure modes
 extern int __CPROVER_malloc_failure_mode_return_null;
diff --git a/src/ansi-c/library/cprover_contracts.c b/src/ansi-c/library/cprover_contracts.c
index 37c5e476093..6f7d10fca87 100644
--- a/src/ansi-c/library/cprover_contracts.c
+++ b/src/ansi-c/library/cprover_contracts.c
@@ -7,7 +7,6 @@
 #define __CPROVER_contracts_library_defined
 
 // external dependencies
-extern __CPROVER_size_t __CPROVER_max_malloc_size;
 const void *__CPROVER_alloca_object = 0;
 extern const void *__CPROVER_deallocated;
 const void *__CPROVER_new_object = 0;
diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index ae9c2876c9d..6ab22b4411e 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -808,6 +808,8 @@ int cbmc_parse_optionst::get_goto_program(
 
   goto_model = initialize_goto_model(cmdline.args, ui_message_handler, options);
 
+  update_max_malloc_size(goto_model, ui_message_handler);
+
   if(cmdline.isset("show-symbol-table"))
   {
     show_symbol_table(goto_model, ui_message_handler);
diff --git a/src/goto-cc/gcc_cmdline.cpp b/src/goto-cc/gcc_cmdline.cpp
index e2b72ad0f89..46f8fbae0b9 100644
--- a/src/goto-cc/gcc_cmdline.cpp
+++ b/src/goto-cc/gcc_cmdline.cpp
@@ -29,7 +29,6 @@ const char *goto_cc_options_with_separated_argument[]=
   "--native-linker",
   "--print-rejected-preprocessed-source",
   "--mangle-suffix",
-  "--object-bits",
   nullptr
 };
 
diff --git a/src/goto-cc/goto_cc_mode.cpp b/src/goto-cc/goto_cc_mode.cpp
index df0c9733f19..fb0583e3a0c 100644
--- a/src/goto-cc/goto_cc_mode.cpp
+++ b/src/goto-cc/goto_cc_mode.cpp
@@ -74,7 +74,6 @@ void goto_cc_modet::help()
     "symbols\n"
     " {y--print-rejected-preprocessed-source} {ufile} \t "
     "copy failing (preprocessed) source to file\n"
-    " {y--object-bits} {N} \t number of bits used for object addresses\n"
     "\n");
 }
 
diff --git a/src/goto-instrument/nondet_static.cpp b/src/goto-instrument/nondet_static.cpp
index e968a346dba..7c7e7170ec8 100644
--- a/src/goto-instrument/nondet_static.cpp
+++ b/src/goto-instrument/nondet_static.cpp
@@ -77,16 +77,17 @@ bool is_nondet_initializable_static(
 /// assigned to nondet-initializable static variables with nondeterministic
 /// values.
 /// \param ns: Namespace for resolving type information.
-/// \param [out] goto_functions: Existing goto-functions to be updated.
+/// \param [inout] goto_model: Existing goto-functions and symbol table to
+///   be updated.
 /// \param fct_name: Name of the goto-function to be updated.
 static void nondet_static(
   const namespacet &ns,
-  goto_functionst &goto_functions,
+  goto_modelt &goto_model,
   const irep_idt &fct_name)
 {
   goto_functionst::function_mapt::iterator fct_entry =
-    goto_functions.function_map.find(fct_name);
-  CHECK_RETURN(fct_entry != goto_functions.function_map.end());
+    goto_model.goto_functions.function_map.find(fct_name);
+  CHECK_RETURN(fct_entry != goto_model.goto_functions.function_map.end());
 
   goto_programt &init = fct_entry->second.body;
 
@@ -99,11 +100,11 @@ static void nondet_static(
 
       if(is_nondet_initializable_static(sym, ns))
       {
-        const auto source_location = instruction.source_location();
-        instruction = goto_programt::make_assignment(
-          code_assignt(
-            sym, side_effect_expr_nondett(sym.type(), source_location)),
-          source_location);
+        side_effect_expr_nondett nondet{
+          sym.type(), instruction.source_location()};
+        instruction.assign_rhs_nonconst() = nondet;
+        goto_model.symbol_table.get_writeable_ref(sym.get_identifier()).value =
+          nondet;
       }
     }
     else if(instruction.is_function_call())
@@ -113,33 +114,24 @@ static void nondet_static(
       // see cpp/cpp_typecheck.cpp, which creates initialization functions
       if(fsym.get_identifier().starts_with("#cpp_dynamic_initialization#"))
       {
-        nondet_static(ns, goto_functions, fsym.get_identifier());
+        nondet_static(ns, goto_model, fsym.get_identifier());
       }
     }
   }
 
   // update counters etc.
-  goto_functions.update();
-}
-
-/// Nondeterministically initializes global scope variables in
-/// CPROVER_initialize function.
-/// \param ns: Namespace for resolving type information.
-/// \param [out] goto_functions: Existing goto-functions to be updated.
-void nondet_static(const namespacet &ns, goto_functionst &goto_functions)
-{
-  nondet_static(ns, goto_functions, INITIALIZE_FUNCTION);
+  goto_model.goto_functions.update();
 }
 
 /// First main entry point of the module. Nondeterministically initializes
 /// global scope variables, except for constants (such as string literals, final
 /// fields) and internal variables (such as CPROVER and symex variables,
 /// language specific internal variables).
-/// \param [out] goto_model: Existing goto-model to be updated.
+/// \param [inout] goto_model: Existing goto-model to be updated.
 void nondet_static(goto_modelt &goto_model)
 {
   const namespacet ns(goto_model.symbol_table);
-  nondet_static(ns, goto_model.goto_functions);
+  nondet_static(ns, goto_model, INITIALIZE_FUNCTION);
 }
 
 /// Second main entry point of the module. Nondeterministically initializes
@@ -199,7 +191,7 @@ void nondet_static(
     }
   }
 
-  nondet_static(ns, goto_model.goto_functions, INITIALIZE_FUNCTION);
+  nondet_static(ns, goto_model, INITIALIZE_FUNCTION);
 }
 
 /// Nondeterministically initializes global scope variables that
@@ -227,5 +219,5 @@ void nondet_static_matching(goto_modelt &goto_model, const std::string &regex)
   }
 
   const namespacet ns(goto_model.symbol_table);
-  nondet_static(ns, goto_model.goto_functions, INITIALIZE_FUNCTION);
+  nondet_static(ns, goto_model, INITIALIZE_FUNCTION);
 }
diff --git a/src/goto-instrument/nondet_static.h b/src/goto-instrument/nondet_static.h
index 94353d9d253..a3f8a9816da 100644
--- a/src/goto-instrument/nondet_static.h
+++ b/src/goto-instrument/nondet_static.h
@@ -32,10 +32,6 @@ bool is_nondet_initializable_static(
   const symbol_exprt &symbol_expr,
   const namespacet &ns);
 
-void nondet_static(
-  const namespacet &ns,
-  goto_functionst &goto_functions);
-
 void nondet_static(goto_modelt &);
 
 void nondet_static(goto_modelt &, const std::set<std::string> &);
diff --git a/src/goto-programs/initialize_goto_model.cpp b/src/goto-programs/initialize_goto_model.cpp
index 11c0870f1f7..43ac5304aa9 100644
--- a/src/goto-programs/initialize_goto_model.cpp
+++ b/src/goto-programs/initialize_goto_model.cpp
@@ -11,6 +11,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "initialize_goto_model.h"
 
+#include <util/arith_tools.h>
+#include <util/c_types.h>
 #include <util/config.h>
 #include <util/exception_utils.h>
 #include <util/message.h>
@@ -22,6 +24,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <langapi/language.h>
 #include <langapi/language_file.h>
 #include <langapi/mode.h>
+#include <linking/static_lifetime_init.h>
 
 #include "goto_convert_functions.h"
 #include "read_goto_binary.h"
@@ -236,3 +239,29 @@ goto_modelt initialize_goto_model(
 
   return goto_model;
 }
+
+void update_max_malloc_size(
+  goto_modelt &goto_model,
+  message_handlert &message_handler)
+{
+  if(!goto_model.symbol_table.has_symbol(CPROVER_PREFIX "max_malloc_size"))
+    return;
+
+  const auto previous_max_malloc_size_value = numeric_cast<mp_integer>(
+    goto_model.symbol_table.lookup_ref(CPROVER_PREFIX "max_malloc_size").value);
+  const mp_integer current_max_malloc_size = config.max_malloc_size();
+
+  if(
+    !previous_max_malloc_size_value.has_value() ||
+    *previous_max_malloc_size_value != current_max_malloc_size)
+  {
+    symbolt &max_malloc_size_sym = goto_model.symbol_table.get_writeable_ref(
+      CPROVER_PREFIX "max_malloc_size");
+    max_malloc_size_sym.value =
+      from_integer(current_max_malloc_size, size_type());
+    max_malloc_size_sym.value.set(ID_C_no_nondet_initialization, true);
+
+    if(goto_model.can_produce_function(INITIALIZE_FUNCTION))
+      recreate_initialize_function(goto_model, message_handler);
+  }
+}
diff --git a/src/goto-programs/initialize_goto_model.h b/src/goto-programs/initialize_goto_model.h
index 6925a10e3f5..88849fe71ea 100644
--- a/src/goto-programs/initialize_goto_model.h
+++ b/src/goto-programs/initialize_goto_model.h
@@ -56,4 +56,8 @@ void set_up_custom_entry_point(
   bool try_mode_lookup,
   message_handlert &message_handler);
 
+/// Update the initial value of `__CPROVER_max_malloc_size` in case the number
+/// of object bits has changed.
+void update_max_malloc_size(goto_modelt &, message_handlert &);
+
 #endif // CPROVER_GOTO_PROGRAMS_INITIALIZE_GOTO_MODEL_H
diff --git a/src/goto-synthesizer/goto_synthesizer_parse_options.cpp b/src/goto-synthesizer/goto_synthesizer_parse_options.cpp
index 61e2a71c403..3e4f3fe4dbc 100644
--- a/src/goto-synthesizer/goto_synthesizer_parse_options.cpp
+++ b/src/goto-synthesizer/goto_synthesizer_parse_options.cpp
@@ -13,6 +13,7 @@ Author: Qinheping Hu
 #include <util/unicode.h>
 #include <util/version.h>
 
+#include <goto-programs/initialize_goto_model.h>
 #include <goto-programs/read_goto_binary.h>
 #include <goto-programs/set_properties.h>
 #include <goto-programs/show_goto_functions.h>
@@ -73,6 +74,8 @@ int goto_synthesizer_parse_optionst::doit()
     configure_gcc(gcc_version);
   }
 
+  update_max_malloc_size(goto_model, ui_message_handler);
+
   // Get options for the backend verifier and preprocess `goto_model`.
   const auto &options = get_options();
 
diff --git a/src/util/config.cpp b/src/util/config.cpp
index 63ac91d8943..7033b771a42 100644
--- a/src/util/config.cpp
+++ b/src/util/config.cpp
@@ -1482,3 +1482,28 @@ irep_idt configt::this_operating_system()
 
   return this_os;
 }
+
+/// The maximum allocation size is determined by the number of bits that
+/// are left in the pointer of width `ansi_c.pointer_width`.
+///
+/// The allocation size cannot exceed the number represented by the (signed)
+/// offset, otherwise it would not be possible to store a pointer into a
+/// valid bit of memory. Therefore, the max allocation size is
+/// 2^(offset_bits - 1), where the offset bits is the number of bits left in the
+/// pointer after the object bits.
+///
+/// The offset must be signed, as a pointer can point to the end of the memory
+/// block, and needs to be able to point back to the start.
+/// \return The size in bytes of the maximum allocation supported.
+mp_integer configt::max_malloc_size() const
+{
+  PRECONDITION(ansi_c.pointer_width >= 1);
+  PRECONDITION(bv_encoding.object_bits < ansi_c.pointer_width);
+  PRECONDITION(bv_encoding.object_bits >= 1);
+  const auto offset_bits = ansi_c.pointer_width - bv_encoding.object_bits;
+  // We require the offset to be able to express upto allocation_size - 1,
+  // but also down to -allocation_size, therefore the size is allowable
+  // is number of bits, less the signed bit.
+  const auto bits_for_positive_offset = offset_bits - 1;
+  return ((mp_integer)1) << (mp_integer)bits_for_positive_offset;
+}
diff --git a/src/util/config.h b/src/util/config.h
index 288b244621a..f97aa531e19 100644
--- a/src/util/config.h
+++ b/src/util/config.h
@@ -363,6 +363,7 @@ class configt
 
   void set_object_bits_from_symbol_table(const symbol_table_baset &);
   std::string object_bits_info();
+  mp_integer max_malloc_size() const;
 
   static irep_idt this_architecture();
   static irep_idt this_operating_system();
diff --git a/src/util/simplify_expr_pointer.cpp b/src/util/simplify_expr_pointer.cpp
index f089d274962..1511717dd94 100644
--- a/src/util/simplify_expr_pointer.cpp
+++ b/src/util/simplify_expr_pointer.cpp
@@ -10,7 +10,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "arith_tools.h"
 #include "c_types.h"
-#include "config.h"
 #include "expr_util.h"
 #include "namespace.h"
 #include "pointer_expr.h"
@@ -403,23 +402,6 @@ simplify_exprt::simplify_pointer_offset(const pointer_offset_exprt &expr)
     {
       return from_integer(0, expr.type());
     }
-    else
-    {
-      // this is a pointer, we can't use to_integer
-      const auto width = to_pointer_type(ptr.type()).get_width();
-      mp_integer number = bvrep2integer(c_ptr.get_value(), width, false);
-      // a null pointer would have been caught above, return value 0
-      // will indicate that conversion failed
-      if(number==0)
-        return unchanged(expr);
-
-      // The constant address consists of OBJECT-ID || OFFSET.
-      mp_integer offset_bits =
-        *pointer_offset_bits(ptr.type(), ns) - config.bv_encoding.object_bits;
-      number%=power(2, offset_bits);
-
-      return from_integer(number, expr.type());
-    }
   }
 
   return unchanged(expr);
diff --git a/unit/Makefile b/unit/Makefile
index b29f8c56ee1..1870b890517 100644
--- a/unit/Makefile
+++ b/unit/Makefile
@@ -49,7 +49,6 @@ SRC += analyses/ai/ai.cpp \
        analyses/variable-sensitivity/variable_sensitivity_domain/to_predicate.cpp \
        analyses/variable-sensitivity/variable_sensitivity_test_helpers.cpp \
        ansi-c/expr2c.cpp \
-       ansi-c/max_malloc_size.cpp \
        ansi-c/type2name.cpp \
        ansi-c/c_typecheck_base.cpp \
        big-int/big-int.cpp \
@@ -168,6 +167,7 @@ SRC += analyses/ai/ai.cpp \
        util/json_object.cpp \
        util/lazy.cpp \
        util/lower_byte_operators.cpp \
+       util/max_malloc_size.cpp \
        util/memory_info.cpp \
        util/message.cpp \
        util/optional_utils.cpp \
diff --git a/unit/ansi-c/max_malloc_size.cpp b/unit/ansi-c/max_malloc_size.cpp
deleted file mode 100644
index e7bd73089d7..00000000000
--- a/unit/ansi-c/max_malloc_size.cpp
+++ /dev/null
@@ -1,46 +0,0 @@
-/*******************************************************************\
-
-Module: Unit test for max_malloc_size
-
-Author: Thomas Kiley
-
-\*******************************************************************/
-
-#include <ansi-c/ansi_c_internal_additions.cpp>
-#include <testing-utils/use_catch.h>
-
-TEST_CASE(
-  "max_malloc_size",
-  "[core][ansi-c][ansi_c_internal_additions][max_malloc_size]")
-{
-  cbmc_invariants_should_throwt throw_invariants;
-
-  SECTION("Too many bits for pointer ID")
-  {
-    REQUIRE_THROWS_AS(max_malloc_size(4, 4), invariant_failedt);
-    REQUIRE_THROWS_AS(max_malloc_size(4, 5), invariant_failedt);
-  }
-
-  SECTION("Not enough bits for pointer ID")
-  {
-    REQUIRE_THROWS_AS(max_malloc_size(4, 0), invariant_failedt);
-  }
-
-  SECTION("Not enough bits in the pointer")
-  {
-    REQUIRE_THROWS_AS(max_malloc_size(0, 0), invariant_failedt);
-  }
-
-  SECTION("Valid allocation size configurations")
-  {
-    // The one bit offset can be used to store 0, or -1, so we can allocate
-    // a single bit
-    REQUIRE(max_malloc_size(4, 3) == 1);
-    // Here we use 4 bits for the object ID, leaving 3 for the offset
-    REQUIRE(max_malloc_size(8, 4) == 8);
-    REQUIRE(max_malloc_size(128, 64) == 9223372036854775808ull /*2^63*/);
-    REQUIRE(
-      max_malloc_size(128, 63) == string2integer("18446744073709551616"
-                                                 /*2^64*/));
-  }
-}
diff --git a/unit/util/max_malloc_size.cpp b/unit/util/max_malloc_size.cpp
new file mode 100644
index 00000000000..b2ffefb5a99
--- /dev/null
+++ b/unit/util/max_malloc_size.cpp
@@ -0,0 +1,63 @@
+/*******************************************************************\
+
+Module: Unit test for max_malloc_size
+
+Author: Thomas Kiley
+
+\*******************************************************************/
+
+#include <util/config.h>
+
+#include <testing-utils/use_catch.h>
+
+TEST_CASE("max_malloc_size", "[core][util][config][max_malloc_size]")
+{
+  cbmc_invariants_should_throwt throw_invariants;
+
+  configt config_backup = config;
+
+  SECTION("Too many bits for pointer ID")
+  {
+    config.ansi_c.pointer_width = 4;
+    config.bv_encoding.object_bits = 4;
+    REQUIRE_THROWS_AS(config.max_malloc_size(), invariant_failedt);
+    config.bv_encoding.object_bits = 5;
+    REQUIRE_THROWS_AS(config.max_malloc_size(), invariant_failedt);
+  }
+
+  SECTION("Not enough bits for pointer ID")
+  {
+    config.ansi_c.pointer_width = 4;
+    config.bv_encoding.object_bits = 0;
+    REQUIRE_THROWS_AS(config.max_malloc_size(), invariant_failedt);
+  }
+
+  SECTION("Not enough bits in the pointer")
+  {
+    config.ansi_c.pointer_width = 0;
+    config.bv_encoding.object_bits = 0;
+    REQUIRE_THROWS_AS(config.max_malloc_size(), invariant_failedt);
+  }
+
+  SECTION("Valid allocation size configurations")
+  {
+    // The one bit offset can be used to store 0, or -1, so we can allocate
+    // a single bit
+    config.ansi_c.pointer_width = 4;
+    config.bv_encoding.object_bits = 3;
+    REQUIRE(config.max_malloc_size() == 1);
+    // Here we use 4 bits for the object ID, leaving 3 for the offset
+    config.ansi_c.pointer_width = 8;
+    config.bv_encoding.object_bits = 4;
+    REQUIRE(config.max_malloc_size() == 8);
+    config.ansi_c.pointer_width = 128;
+    config.bv_encoding.object_bits = 64;
+    REQUIRE(config.max_malloc_size() == 9223372036854775808ull /*2^63*/);
+    config.bv_encoding.object_bits = 63;
+    REQUIRE(
+      config.max_malloc_size() == string2integer("18446744073709551616"
+                                                 /*2^64*/));
+  }
+
+  std::swap(config_backup, config);
+}
diff --git a/unit/util/simplify_expr.cpp b/unit/util/simplify_expr.cpp
index 756666240a6..8219df4f45f 100644
--- a/unit/util/simplify_expr.cpp
+++ b/unit/util/simplify_expr.cpp
@@ -44,27 +44,6 @@ TEST_CASE("Simplify pointer_offset(address of array index)", "[core][util]")
   REQUIRE(offset_value==1);
 }
 
-TEST_CASE("Simplify const pointer offset", "[core][util]")
-{
-  config.set_arch("none");
-
-  symbol_tablet symbol_table;
-  namespacet ns(symbol_table);
-
-  // build a numeric constant of some pointer type
-  constant_exprt number=from_integer(1234, size_type());
-  number.type()=pointer_type(char_type());
-
-  exprt p_o=pointer_offset(number);
-
-  exprt simp=simplify_expr(p_o, ns);
-
-  REQUIRE(simp.is_constant());
-  const mp_integer offset_value =
-    numeric_cast_v<mp_integer>(to_constant_expr(simp));
-  REQUIRE(offset_value==1234);
-}
-
 TEST_CASE("Simplify byte extract", "[core][util]")
 {
   // this test does require a proper architecture to be set so that byte extract