diff --git a/doc/architectural/memory-bounds-checking.md b/doc/architectural/memory-bounds-checking.md
index a02f816d99c..73933e27f27 100644
--- a/doc/architectural/memory-bounds-checking.md
+++ b/doc/architectural/memory-bounds-checking.md
@@ -30,19 +30,10 @@ inline void *malloc(__CPROVER_size_t malloc_size)
 {
   void *malloc_res;
   malloc_res = __CPROVER_allocate(malloc_size, 0);
-
-  __CPROVER_bool record_malloc = __VERIFIER_nondet___CPROVER_bool();
-  __CPROVER_malloc_object = record_malloc ? malloc_res : __CPROVER_malloc_object;
-
   return malloc_res;
 }
 ```
 
-The internal variable `__CPROVER_malloc_object`
-is initialized to 0 in the `__CPROVER_initialize()` function of a goto program.
-The nondeterministic switch controls whether the address of the memory
-block allocated in this particular invocation of `malloc()` is recorded.
-
 When the option `--pointer-check` is used, cbmc generates the following
 verification condition for each pointer dereference expression (e.g.,
 `*pointer`):
@@ -73,8 +64,7 @@ int main()
 ```
 
 Here the verification condition generated for the pointer dereference should
-fail. In the approach outlined above it indeed can, as one can choose true for
-`__VERIFIER_nondet___CPROVER_bool()` in the first call
-to `malloc()`, and false for `__VERIFIER_nondet___CPROVER_bool()` in the second
-call to `malloc()`. Thus, the object address of the first call to
-`malloc()` is recorded in `__CPROVER_malloc_object`.
+fail: for `p1` in `*p1`, `__CPROVER_POINTER_OFFSET` will evaluate to 1 (owing to
+the increment `p1++`, and `__CPROVER_OBJECT_SIZE` will also evaluate to 1.
+Consequently, the less-than comparison in the verification condition evaluates
+to false.
diff --git a/jbmc/src/java_bytecode/java_bytecode_internal_additions.cpp b/jbmc/src/java_bytecode/java_bytecode_internal_additions.cpp
index cd90096e577..c30152ea932 100644
--- a/jbmc/src/java_bytecode/java_bytecode_internal_additions.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_internal_additions.cpp
@@ -36,20 +36,6 @@ void java_internal_additions(symbol_table_baset &dest)
     dest.add(symbol);
   }
 
-  // add __CPROVER_malloc_object
-
-  {
-    symbolt symbol;
-    symbol.base_name = CPROVER_PREFIX "malloc_object";
-    symbol.name=CPROVER_PREFIX "malloc_object";
-    symbol.type = pointer_type(java_void_type());
-    symbol.mode=ID_C;
-    symbol.is_lvalue=true;
-    symbol.is_state_var=true;
-    symbol.is_thread_local=true;
-    dest.add(symbol);
-  }
-
   {
     auxiliary_symbolt symbol;
     symbol.base_name = INFLIGHT_EXCEPTION_VARIABLE_BASENAME;
diff --git a/regression/goto-analyzer/constant_propagation_01/test-vsd.desc b/regression/goto-analyzer/constant_propagation_01/test-vsd.desc
index 9c4ca23bf15..37aba4c1a6c 100644
--- a/regression/goto-analyzer/constant_propagation_01/test-vsd.desc
+++ b/regression/goto-analyzer/constant_propagation_01/test-vsd.desc
@@ -3,7 +3,7 @@ main.c
 --variable-sensitivity --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$
 ^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 16, function calls: 2$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_01/test.desc b/regression/goto-analyzer/constant_propagation_01/test.desc
index ff1046eea1f..cae4e9e0e4b 100644
--- a/regression/goto-analyzer/constant_propagation_01/test.desc
+++ b/regression/goto-analyzer/constant_propagation_01/test.desc
@@ -3,7 +3,7 @@ main.c
 --constants --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$
 ^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 16, function calls: 2$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_02/test-vsd.desc b/regression/goto-analyzer/constant_propagation_02/test-vsd.desc
index f04aa76fd55..7ed72ea96d6 100644
--- a/regression/goto-analyzer/constant_propagation_02/test-vsd.desc
+++ b/regression/goto-analyzer/constant_propagation_02/test-vsd.desc
@@ -3,7 +3,7 @@ main.c
 --variable-sensitivity --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$
 ^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 15, function calls: 2$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_02/test.desc b/regression/goto-analyzer/constant_propagation_02/test.desc
index 157122e6f02..f2b6df6334f 100644
--- a/regression/goto-analyzer/constant_propagation_02/test.desc
+++ b/regression/goto-analyzer/constant_propagation_02/test.desc
@@ -3,7 +3,7 @@ main.c
 --constants --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$
 ^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 15, function calls: 2$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_03/test-vsd.desc b/regression/goto-analyzer/constant_propagation_03/test-vsd.desc
index f04aa76fd55..7ed72ea96d6 100644
--- a/regression/goto-analyzer/constant_propagation_03/test-vsd.desc
+++ b/regression/goto-analyzer/constant_propagation_03/test-vsd.desc
@@ -3,7 +3,7 @@ main.c
 --variable-sensitivity --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$
 ^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 15, function calls: 2$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_03/test.desc b/regression/goto-analyzer/constant_propagation_03/test.desc
index 157122e6f02..f2b6df6334f 100644
--- a/regression/goto-analyzer/constant_propagation_03/test.desc
+++ b/regression/goto-analyzer/constant_propagation_03/test.desc
@@ -3,7 +3,7 @@ main.c
 --constants --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$
 ^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 15, function calls: 2$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_04/test-vsd.desc b/regression/goto-analyzer/constant_propagation_04/test-vsd.desc
index f04aa76fd55..7ed72ea96d6 100644
--- a/regression/goto-analyzer/constant_propagation_04/test-vsd.desc
+++ b/regression/goto-analyzer/constant_propagation_04/test-vsd.desc
@@ -3,7 +3,7 @@ main.c
 --variable-sensitivity --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$
 ^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 15, function calls: 2$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_04/test.desc b/regression/goto-analyzer/constant_propagation_04/test.desc
index 157122e6f02..f2b6df6334f 100644
--- a/regression/goto-analyzer/constant_propagation_04/test.desc
+++ b/regression/goto-analyzer/constant_propagation_04/test.desc
@@ -3,7 +3,7 @@ main.c
 --constants --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$
 ^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 15, function calls: 2$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_07/test-vsd.desc b/regression/goto-analyzer/constant_propagation_07/test-vsd.desc
index a08ad0585de..eb062c1d12d 100644
--- a/regression/goto-analyzer/constant_propagation_07/test-vsd.desc
+++ b/regression/goto-analyzer/constant_propagation_07/test-vsd.desc
@@ -3,7 +3,7 @@ main.c
 --variable-sensitivity --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^Simplified:  assert: 1, assume: 0, goto: 3, assigns: 9, function calls: 0$
+^Simplified:  assert: 1, assume: 0, goto: 3, assigns: 8, function calls: 0$
 ^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 17, function calls: 2$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_07/test.desc b/regression/goto-analyzer/constant_propagation_07/test.desc
index 8cbddd545a5..864e92aefa2 100644
--- a/regression/goto-analyzer/constant_propagation_07/test.desc
+++ b/regression/goto-analyzer/constant_propagation_07/test.desc
@@ -3,7 +3,7 @@ main.c
 --constants --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^Simplified:  assert: 1, assume: 0, goto: 3, assigns: 9, function calls: 0$
+^Simplified:  assert: 1, assume: 0, goto: 3, assigns: 8, function calls: 0$
 ^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 17, function calls: 2$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_08/test-vsd.desc b/regression/goto-analyzer/constant_propagation_08/test-vsd.desc
index 9f688397164..3439120d10e 100644
--- a/regression/goto-analyzer/constant_propagation_08/test-vsd.desc
+++ b/regression/goto-analyzer/constant_propagation_08/test-vsd.desc
@@ -3,7 +3,7 @@ main.c
 --variable-sensitivity --vsd-arrays every-element --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^Simplified:  assert: 1, assume: 0, goto: 2, assigns: 8, function calls: 0$
+^Simplified:  assert: 1, assume: 0, goto: 2, assigns: 7, function calls: 0$
 ^Unmodified:  assert: 0, assume: 0, goto: 3, assigns: 16, function calls: 2$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_11/test-vsd.desc b/regression/goto-analyzer/constant_propagation_11/test-vsd.desc
index 678780d953a..914e9437146 100644
--- a/regression/goto-analyzer/constant_propagation_11/test-vsd.desc
+++ b/regression/goto-analyzer/constant_propagation_11/test-vsd.desc
@@ -3,7 +3,7 @@ main.c
 --variable-sensitivity --vsd-arrays every-element --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$
 ^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 13, function calls: 2$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_11/test.desc b/regression/goto-analyzer/constant_propagation_11/test.desc
index f24b6403cbc..91dbe25d0c9 100644
--- a/regression/goto-analyzer/constant_propagation_11/test.desc
+++ b/regression/goto-analyzer/constant_propagation_11/test.desc
@@ -3,7 +3,7 @@ main.c
 --constants --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 8, function calls: 0$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$
 ^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 13, function calls: 2$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_12/test-vsd.desc b/regression/goto-analyzer/constant_propagation_12/test-vsd.desc
index 8744444c5e7..e5e6d43b1ee 100644
--- a/regression/goto-analyzer/constant_propagation_12/test-vsd.desc
+++ b/regression/goto-analyzer/constant_propagation_12/test-vsd.desc
@@ -3,7 +3,7 @@ main.c
 --variable-sensitivity --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$
 ^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 14, function calls: 2$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/constant_propagation_12/test.desc b/regression/goto-analyzer/constant_propagation_12/test.desc
index b58cb411abb..cec2574b7c1 100644
--- a/regression/goto-analyzer/constant_propagation_12/test.desc
+++ b/regression/goto-analyzer/constant_propagation_12/test.desc
@@ -3,7 +3,7 @@ main.c
 --constants --simplify out.gb
 ^EXIT=0$
 ^SIGNAL=0$
-^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 7, function calls: 0$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 6, function calls: 0$
 ^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 14, function calls: 2$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/sensitivity-last-written-locations-arrays/test.desc b/regression/goto-analyzer/sensitivity-last-written-locations-arrays/test.desc
index cb3a0f92f47..4143c80414c 100644
--- a/regression/goto-analyzer/sensitivity-last-written-locations-arrays/test.desc
+++ b/regression/goto-analyzer/sensitivity-last-written-locations-arrays/test.desc
@@ -8,30 +8,29 @@ activate-multi-line-match
 main#return_value \(\) -> TOP @ \[1\]
 __CPROVER_dead_object \(\) -> TOP @ \[5\]
 __CPROVER_deallocated \(\) -> TOP @ \[6\]
-__CPROVER_malloc_is_new_array \(\) -> FALSE @ \[9\]
-__CPROVER_malloc_object \(\) -> TOP @ \[10\]
-__CPROVER_memory_leak \(\) -> TOP @ \[12\]
-__CPROVER_next_thread_key \(\) -> 0ul @ \[14\]
-__CPROVER_pipe_count \(\) -> 0u @ \[15\]
-__CPROVER_rounding_mode \(\) -> 0 @ \[16\]
-__CPROVER_thread_id \(\) -> 0ul @ \[17\]
-__CPROVER_threads_exited \(\) -> TOP @ \[20\]
-do_arrays::1::bool_ \(\) -> TOP @ \[22\]
-do_arrays::1::bool_1 \(\) -> TOP @ \[23\]
-do_arrays::1::bool_2 \(\) -> TOP @ \[24\]
-do_arrays::1::x \(\) -> \{\[0\] = 10 @ \[26\]\n\} @ \[26\]
-do_arrays::1::x \(\) -> \{\[0\] = 10 @ \[26\]\n\[1\] = 20 @ \[27\]\n\} @ \[27\]
-do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[28\]\n\[1\] = 20 @ \[27\]\n\} @ \[28\]
-do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[28\]\n\[1\] = 40 @ \[29\]\n\} @ \[29\]
-do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[28\]\n\[1\] = 30 @ \[30\]\n\} @ \[30\]
-do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[31\]\n\[1\] = 30 @ \[30\]\n\} @ \[31\]
-do_arrays::1::x \(\) -> \{\[0\] = 5 @ \[32\]\n\[1\] = 30 @ \[30\]\n\} @ \[32\]
-do_arrays::1::x \(\) -> \{\[0\] = 15 @ \[33\]\n\[1\] = 30 @ \[30\]\n\} @ \[33\]
-do_arrays::1::x \(\) -> \{\[0\] = 15 @ \[33\]\n\[1\] = 10 @ \[34\]\n\} @ \[34\]
-do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[36\]\n\[1\] = 10 @ \[34\]\n\} @ \[36\]
-do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[36\, 38\]\n\[1\] = 10 @ \[34\]\n\} @ \[36\, 38\]
-do_arrays::1::x \(\) -> \{\[0\] = 0 @ \[40]\n\[1\] = 10 @ \[34\]\n\} @ \[40\]
-do_arrays::1::x \(\) -> \{\[0\] = 3 @ \[42]\n\[1\] = 10 @ \[34\]\n\} @ \[42\]
-do_arrays::1::x \(\) -> \{\[0\] = TOP @ \[42\, 44]\n\[1\] = 10 @ \[34\]\n\} @ \[42\, 44\]
-do_arrays::1::x \(\) -> \{\[0\] = TOP @ \[42\, 44\, 47]\n\[1\] = 10 @ \[49\]\n\} @ \[49\]
-do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[50]\n\[1\] = 10 @ \[49\]\n\} @ \[50\]
+__CPROVER_memory_leak \(\) -> TOP @ \[10\]
+__CPROVER_new_object \(\) -> TOP @ \[11\]
+__CPROVER_next_thread_key \(\) -> 0ul @ \[13\]
+__CPROVER_pipe_count \(\) -> 0u @ \[14\]
+__CPROVER_rounding_mode \(\) -> 0 @ \[15\]
+__CPROVER_thread_id \(\) -> 0ul @ \[16\]
+__CPROVER_threads_exited \(\) -> TOP @ \[19\]
+do_arrays::1::bool_ \(\) -> TOP @ \[21\]
+do_arrays::1::bool_1 \(\) -> TOP @ \[22\]
+do_arrays::1::bool_2 \(\) -> TOP @ \[23\]
+do_arrays::1::x \(\) -> \{\[0\] = 10 @ \[25\]\n\} @ \[25\]
+do_arrays::1::x \(\) -> \{\[0\] = 10 @ \[25\]\n\[1\] = 20 @ \[26\]\n\} @ \[26\]
+do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[27\]\n\[1\] = 20 @ \[26\]\n\} @ \[27\]
+do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[27\]\n\[1\] = 40 @ \[28\]\n\} @ \[28\]
+do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[27\]\n\[1\] = 30 @ \[29\]\n\} @ \[29\]
+do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[30\]\n\[1\] = 30 @ \[29\]\n\} @ \[30\]
+do_arrays::1::x \(\) -> \{\[0\] = 5 @ \[31\]\n\[1\] = 30 @ \[29\]\n\} @ \[31\]
+do_arrays::1::x \(\) -> \{\[0\] = 15 @ \[32\]\n\[1\] = 30 @ \[29\]\n\} @ \[32\]
+do_arrays::1::x \(\) -> \{\[0\] = 15 @ \[32\]\n\[1\] = 10 @ \[33\]\n\} @ \[33\]
+do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[35\]\n\[1\] = 10 @ \[33\]\n\} @ \[35\]
+do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[35\, 37\]\n\[1\] = 10 @ \[33\]\n\} @ \[35\, 37\]
+do_arrays::1::x \(\) -> \{\[0\] = 0 @ \[39]\n\[1\] = 10 @ \[33\]\n\} @ \[39\]
+do_arrays::1::x \(\) -> \{\[0\] = 3 @ \[41]\n\[1\] = 10 @ \[33\]\n\} @ \[41\]
+do_arrays::1::x \(\) -> \{\[0\] = TOP @ \[41\, 43]\n\[1\] = 10 @ \[33\]\n\} @ \[41\, 43\]
+do_arrays::1::x \(\) -> \{\[0\] = TOP @ \[41\, 43\, 46]\n\[1\] = 10 @ \[48\]\n\} @ \[48\]
+do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[49]\n\[1\] = 10 @ \[48\]\n\} @ \[49\]
diff --git a/regression/goto-analyzer/sensitivity-last-written-locations-pointers/test.desc b/regression/goto-analyzer/sensitivity-last-written-locations-pointers/test.desc
index e9c20ba4c03..54cf4a3de1b 100644
--- a/regression/goto-analyzer/sensitivity-last-written-locations-pointers/test.desc
+++ b/regression/goto-analyzer/sensitivity-last-written-locations-pointers/test.desc
@@ -8,29 +8,28 @@ activate-multi-line-match
 main#return_value \(\) -> TOP @ \[1\]
 __CPROVER_dead_object \(\) -> TOP @ \[5\]
 __CPROVER_deallocated \(\) -> TOP @ \[6\]
-__CPROVER_malloc_is_new_array \(\) -> FALSE @ \[9\]
-__CPROVER_malloc_object \(\) -> TOP @ \[10\]
-__CPROVER_memory_leak \(\) -> TOP @ \[12\]
-__CPROVER_next_thread_key \(\) -> 0ul @ \[14\]
-__CPROVER_pipe_count \(\) -> 0u @ \[15\]
-__CPROVER_rounding_mode \(\) -> 0 @ \[16\]
-__CPROVER_thread_id \(\) -> 0ul @ \[17\]
-__CPROVER_threads_exited \(\) -> TOP @ \[20\]
-do_pointers::1::bool_ \(\) -> TOP @ \[22\]
-do_pointers::1::bool_1 \(\) -> TOP @ \[23\]
-do_pointers::1::bool_2 \(\) -> TOP @ \[24\]
-do_pointers::1::x \(\) -> TOP @ \[25\]
-do_pointers::1::x \(\) -> 10 @ \[26\]
-do_pointers::1::x_p \(\) -> TOP @ \[27\]
-do_pointers::1::y \(\) -> TOP @ \[28\]
-do_pointers::1::y \(\) -> 20 @ \[29\]
-do_pointers::1::y_p \(\) -> TOP @ \[30\]
-do_pointers::1::x_p \(\) -> ptr ->\(do_pointers::1::x\) @ \[31\]
-do_pointers::1::x \(\) -> 30 @ \[32\]
-do_pointers::1::x \(\) -> 40 @ \[33\]
-do_pointers::1::x \(\) -> TOP @ \[34\]
-do_pointers::1::x \(\) -> 50 @ \[35\]
-do_pointers::1::y_p \(\) -> ptr ->\(do_pointers::1::x\) @ \[36\]
-do_pointers::1::x \(\) -> 60 @ \[37\]
-do_pointers::1::j \(\) -> TOP @ \[38\]
-do_pointers::1::j \(\) -> 60 @ \[39\]
+__CPROVER_new_object \(\) -> TOP @ \[11\]
+__CPROVER_memory_leak \(\) -> TOP @ \[10\]
+__CPROVER_next_thread_id \(\) -> 0ul @ \[12\]
+__CPROVER_pipe_count \(\) -> 0u @ \[14\]
+__CPROVER_rounding_mode \(\) -> 0 @ \[15\]
+__CPROVER_thread_id \(\) -> 0ul @ \[16\]
+__CPROVER_threads_exited \(\) -> TOP @ \[19\]
+do_pointers::1::bool_ \(\) -> TOP @ \[21\]
+do_pointers::1::bool_1 \(\) -> TOP @ \[22\]
+do_pointers::1::bool_2 \(\) -> TOP @ \[23\]
+do_pointers::1::x \(\) -> TOP @ \[24\]
+do_pointers::1::x \(\) -> 10 @ \[25\]
+do_pointers::1::x_p \(\) -> TOP @ \[26\]
+do_pointers::1::y \(\) -> TOP @ \[27\]
+do_pointers::1::y \(\) -> 20 @ \[28\]
+do_pointers::1::y_p \(\) -> TOP @ \[29\]
+do_pointers::1::x_p \(\) -> ptr ->\(do_pointers::1::x\) @ \[30\]
+do_pointers::1::x \(\) -> 30 @ \[31\]
+do_pointers::1::x \(\) -> 40 @ \[32\]
+do_pointers::1::x \(\) -> TOP @ \[33\]
+do_pointers::1::x \(\) -> 50 @ \[34\]
+do_pointers::1::y_p \(\) -> ptr ->\(do_pointers::1::x\) @ \[35\]
+do_pointers::1::x \(\) -> 60 @ \[36\]
+do_pointers::1::j \(\) -> TOP @ \[37\]
+do_pointers::1::j \(\) -> 60 @ \[38\]
diff --git a/regression/goto-analyzer/sensitivity-last-written-locations-structs/test.desc b/regression/goto-analyzer/sensitivity-last-written-locations-structs/test.desc
index 9553229dc2a..722f45da250 100644
--- a/regression/goto-analyzer/sensitivity-last-written-locations-structs/test.desc
+++ b/regression/goto-analyzer/sensitivity-last-written-locations-structs/test.desc
@@ -8,35 +8,34 @@ activate-multi-line-match
 main#return_value \(\) -> TOP @ \[1\]
 __CPROVER_dead_object \(\) -> TOP @ \[5\]
 __CPROVER_deallocated \(\) -> TOP @ \[6\]
-__CPROVER_malloc_is_new_array \(\) -> FALSE @ \[9\]
-__CPROVER_malloc_object \(\) -> TOP @ \[10\]
-__CPROVER_memory_leak \(\) -> TOP @ \[12\]
-__CPROVER_next_thread_key \(\) -> 0ul @ \[14\]
-__CPROVER_pipe_count \(\) -> 0u @ \[15\]
-__CPROVER_rounding_mode \(\) -> 0 @ \[16\]
-__CPROVER_thread_id \(\) -> 0ul @ \[17\]
-__CPROVER_threads_exited \(\) -> TOP @ \[20\]
-do_structs::1::bool_ \(\) -> TOP @ \[22\]
-do_structs::1::bool_1 \(\) -> TOP @ \[23\]
-do_structs::1::bool_2 \(\) -> TOP @ \[24\]
-do_structs::1::st \(\) -> \{\} @ \[25\]
-do_structs::1::st \(\) -> \{.x=10 @ \[26\]\} @ \[26\]
-do_structs::1::st \(\) -> \{.x=10 @ \[26\]\, .y=20 @ \[27\]\} @ \[27\]
-do_structs::1::st \(\) -> \{.x=30 @ \[28\]\, .y=20 @ \[27\]\} @ \[28\]
-do_structs::1::st \(\) -> \{.x=30 @ \[28\]\, .y=40 @ \[29\]\} @ \[29\]
-do_structs::1::st \(\) -> \{.x=30 @ \[28\]\, .y=30 @ \[30\]\} @ \[30\]
-do_structs::1::st \(\) -> \{.x=30 @ \[31\]\, .y=30 @ \[30\]\} @ \[31\]
-do_structs::1::st \(\) -> \{.x=5 @ \[32\]\, .y=30 @ \[30\]\} @ \[32\]
-do_structs::1::st \(\) -> \{.x=15 @ \[33\]\, .y=30 @ \[30\]\} @ \[33\]
-do_structs::1::st \(\) -> \{.x=15 @ \[33\]\, .y=10 @ \[34\]\} @ \[34\]
-do_structs::1::st \(\) -> \{.x=20 @ \[36\]\, .y=10 @ \[34\]\} @ \[36\]
-do_structs::1::st \(\) -> \{.x=20 @ \[36\, 38\]\, .y=10 @ \[34\]\} @ \[36\, 38\]
-do_structs::1::st \(\) -> \{.x=0 @ \[40\]\, .y=10 @ \[34\]\} @ \[40\]
-do_structs::1::st \(\) -> \{.x=3 @ \[42\]\, .y=10 @ \[34\]\} @ \[42\]
-do_structs::1::st \(\) -> \{.x=TOP @ \[42\, 44\]\, .y=10 @ \[34\]\} @ \[42\, 44\]
-do_structs::1::st \(\) -> \{.x=TOP @ \[42\, 44\, 47\]\, .y=10 @ \[34\]\} @ \[42\, 44\, 47\]
-do_structs::1::st \(\) -> \{.x=TOP @ \[42\, 44\, 47\]\, .y=10 @ \[49\]\} @ \[49\]
-do_structs::1::st \(\) -> \{.x=20 @ \[50\]\, .y=10 @ \[49\]\} @ \[50\]
-do_structs::1::new_age \(\) -> \{\} @ \[51\]
-do_structs::1::new_age \(\) -> \{.x=20 @ \[52\]\, .y=10 @ \[52\]\} @ \[52\]
+__CPROVER_new_object \(\) -> TOP @ \[11\]
+__CPROVER_memory_leak \(\) -> TOP @ \[10\]
+__CPROVER_next_thread_id \(\) -> 0ul @ \[12\]
+__CPROVER_pipe_count \(\) -> 0u @ \[14\]
+__CPROVER_rounding_mode \(\) -> 0 @ \[15\]
+__CPROVER_thread_id \(\) -> 0ul @ \[16\]
+__CPROVER_threads_exited \(\) -> TOP @ \[19\]
+do_structs::1::bool_ \(\) -> TOP @ \[21\]
+do_structs::1::bool_1 \(\) -> TOP @ \[22\]
+do_structs::1::bool_2 \(\) -> TOP @ \[23\]
+do_structs::1::st \(\) -> \{\} @ \[24\]
+do_structs::1::st \(\) -> \{.x=10 @ \[25\]\} @ \[25\]
+do_structs::1::st \(\) -> \{.x=10 @ \[25\]\, .y=20 @ \[26\]\} @ \[26\]
+do_structs::1::st \(\) -> \{.x=30 @ \[27\]\, .y=20 @ \[26\]\} @ \[27\]
+do_structs::1::st \(\) -> \{.x=30 @ \[27\]\, .y=40 @ \[28\]\} @ \[28\]
+do_structs::1::st \(\) -> \{.x=30 @ \[27\]\, .y=30 @ \[29\]\} @ \[29\]
+do_structs::1::st \(\) -> \{.x=30 @ \[30\]\, .y=30 @ \[29\]\} @ \[30\]
+do_structs::1::st \(\) -> \{.x=5 @ \[31\]\, .y=30 @ \[29\]\} @ \[31\]
+do_structs::1::st \(\) -> \{.x=15 @ \[32\]\, .y=30 @ \[29\]\} @ \[32\]
+do_structs::1::st \(\) -> \{.x=15 @ \[32\]\, .y=10 @ \[33\]\} @ \[33\]
+do_structs::1::st \(\) -> \{.x=20 @ \[35\]\, .y=10 @ \[33\]\} @ \[35\]
+do_structs::1::st \(\) -> \{.x=20 @ \[35\, 37\]\, .y=10 @ \[33\]\} @ \[35\, 37\]
+do_structs::1::st \(\) -> \{.x=0 @ \[39\]\, .y=10 @ \[33\]\} @ \[39\]
+do_structs::1::st \(\) -> \{.x=3 @ \[41\]\, .y=10 @ \[33\]\} @ \[41\]
+do_structs::1::st \(\) -> \{.x=TOP @ \[41\, 43\]\, .y=10 @ \[33\]\} @ \[41\, 43\]
+do_structs::1::st \(\) -> \{.x=TOP @ \[41\, 43\, 46\]\, .y=10 @ \[33\]\} @ \[41\, 43\, 46\]
+do_structs::1::st \(\) -> \{.x=TOP @ \[41\, 43\, 46\]\, .y=10 @ \[48\]\} @ \[48\]
+do_structs::1::st \(\) -> \{.x=20 @ \[49\]\, .y=10 @ \[48\]\} @ \[49\]
+do_structs::1::new_age \(\) -> \{\} @ \[50\]
+do_structs::1::new_age \(\) -> \{.x=20 @ \[51\]\, .y=10 @ \[51\]\} @ \[51\]
 --
diff --git a/regression/goto-analyzer/sensitivity-last-written-locations-variables/test.desc b/regression/goto-analyzer/sensitivity-last-written-locations-variables/test.desc
index f7c95538c9b..d19b03bcb20 100644
--- a/regression/goto-analyzer/sensitivity-last-written-locations-variables/test.desc
+++ b/regression/goto-analyzer/sensitivity-last-written-locations-variables/test.desc
@@ -7,39 +7,41 @@ main#return_value \(\) -> TOP @ \[1\]
 __CPROVER_alloca_object \(\) -> TOP @ \[4\]
 __CPROVER_dead_object \(\) -> TOP @ \[5\]
 __CPROVER_deallocated \(\) -> TOP @ \[6\]
-__CPROVER_malloc_is_new_array \(\) -> FALSE @ \[9\]
-__CPROVER_malloc_object \(\) -> TOP @ \[10\]
-__CPROVER_memory_leak \(\) -> TOP @ \[12\]
-__CPROVER_next_thread_key \(\) -> 0ul @ \[14\]
-__CPROVER_pipe_count \(\) -> 0u @ \[15\]
-__CPROVER_rounding_mode \(\) -> 0 @ \[16\]
-__CPROVER_thread_id \(\) -> 0ul @ \[17\]
-__CPROVER_threads_exited \(\) -> TOP @ \[20\]
-global_x \(\) -> 0 @ \[21\]
-do_variables::1::bool_ \(\) -> TOP @ \[23\]
-do_variables::1::bool_1 \(\) -> TOP @ \[24\]
-do_variables::1::bool_2 \(\) -> TOP @ \[25\]
-global_x \(\) -> 5 @ \[26\]
-do_variables::1::x \(\) -> TOP @ \[27\]
-do_variables::1::x \(\) -> 10 @ \[28\]
-do_variables::1::y \(\) -> TOP @ \[29\]
-do_variables::1::y \(\) -> 20 @ \[30\]
-do_variables::1::x \(\) -> 30 @ \[31\]
-do_variables::1::y \(\) -> 40 @ \[32\]
-do_variables::1::y \(\) -> 30 @ \[33\]
-do_variables::1::x \(\) -> 30 @ \[34\]
-do_variables::1::x \(\) -> 5 @ \[35\]
-do_variables::1::x \(\) -> 15 @ \[36\]
-do_variables::1::y \(\) -> 10 @ \[37\]
-do_variables::1::x \(\) -> 20 @ \[39\]
-do_variables::1::x \(\) -> 20 @ \[39\, 41\]
-do_variables::1::x \(\) -> 50 @ \[43\]
-do_variables::1::x \(\) -> 20 @ \[45\]
-do_variables::1::x \(\) -> TOP @ \[45\, 47\]
-do_variables::1::x \(\) -> 0 @ \[49\]
-do_variables::1::x \(\) -> 3 @ \[51\]
-do_variables::1::x \(\) -> TOP @ \[51\, 53\]
-do_variables::1::x \(\) -> TOP @ \[51\, 53\, 56\]
-do_variables::1::y \(\) -> 10 @ \[58\]
-do_variables::1::x \(\) -> 20 @ \[59\]
+__CPROVER_new_object \(\) -> TOP @ \[11\]
+__CPROVER_memory_leak \(\) -> TOP @ \[10\]
+__CPROVER_next_thread_id \(\) -> 0ul @ \[12\]
+__CPROVER_next_thread_key \(\) -> 0ul @ \[13\]
+__CPROVER_pipe_count \(\) -> 0u @ \[14\]
+__CPROVER_rounding_mode \(\) -> 0 @ \[15\]
+__CPROVER_thread_id \(\) -> 0ul @ \[16\]
+__CPROVER_thread_key_dtors \(\) -> TOP @ \[17\]
+__CPROVER_thread_keys \(\) -> TOP @ \[18\]
+__CPROVER_threads_exited \(\) -> TOP @ \[19\]
+global_x \(\) -> 0 @ \[20\]
+do_variables::1::bool_ \(\) -> TOP @ \[22\]
+do_variables::1::bool_1 \(\) -> TOP @ \[23\]
+do_variables::1::bool_2 \(\) -> TOP @ \[24\]
+global_x \(\) -> 5 @ \[25\]
+do_variables::1::x \(\) -> TOP @ \[26\]
+do_variables::1::x \(\) -> 10 @ \[27\]
+do_variables::1::y \(\) -> TOP @ \[28\]
+do_variables::1::y \(\) -> 20 @ \[29\]
+do_variables::1::x \(\) -> 30 @ \[30\]
+do_variables::1::y \(\) -> 40 @ \[31\]
+do_variables::1::y \(\) -> 30 @ \[32\]
+do_variables::1::x \(\) -> 30 @ \[33\]
+do_variables::1::x \(\) -> 5 @ \[34\]
+do_variables::1::x \(\) -> 15 @ \[35\]
+do_variables::1::y \(\) -> 10 @ \[36\]
+do_variables::1::x \(\) -> 20 @ \[38\]
+do_variables::1::x \(\) -> 20 @ \[38\, 40\]
+do_variables::1::x \(\) -> 50 @ \[42\]
+do_variables::1::x \(\) -> 20 @ \[44\]
+do_variables::1::x \(\) -> TOP @ \[44\, 46\]
+do_variables::1::x \(\) -> 0 @ \[48\]
+do_variables::1::x \(\) -> 3 @ \[50\]
+do_variables::1::x \(\) -> TOP @ \[50\, 52\]
+do_variables::1::x \(\) -> TOP @ \[50\, 52\, 55\]
+do_variables::1::y \(\) -> 10 @ \[57\]
+do_variables::1::x \(\) -> 20 @ \[58\]
 --
diff --git a/regression/goto-analyzer/sensitivity-test-data-dependency-context/test.desc b/regression/goto-analyzer/sensitivity-test-data-dependency-context/test.desc
index 7af6e45f9c3..6e9a2906657 100644
--- a/regression/goto-analyzer/sensitivity-test-data-dependency-context/test.desc
+++ b/regression/goto-analyzer/sensitivity-test-data-dependency-context/test.desc
@@ -5,8 +5,8 @@ data-dependency-context.c
 activate-multi-line-match
 ^EXIT=0$
 ^SIGNAL=0$
-st \(\) -> \{.a=.* @ \[2, 54\]\[Data dependencies: 54, 2\]\[Data dominators: \], .b=.* @ \[5, 54\]\[Data dependencies: 54, 5\]\[Data dominators: \]\} @ \[2, 5, 54\]\[Data dependencies: 54, 5, 2\]\[Data dominators: 54\]
-ar \(\) -> \{\[0\] = TOP @ \[11\, 48\]\[Data dependencies: 48\, 11\]\[Data dominators: \]\n\[1\] = TOP @ \[14\, 48\]\[Data dependencies: 48\, 14\]\[Data dominators: \]\n\} @ \[11\, 14\, 48\]\[Data dependencies: 48\, 14\, 11\]\[Data dominators: 48\]
-arr \(\) -> \{\[0\] = 1 @ \[19\]\[Data dependencies: 19\]\[Data dominators: 19\]\n\[1\] = 2 @ \[20\]\[Data dependencies: 20\]\[Data dominators: 20\]\n\[2\] = TOP @ \[21, 23\]\[Data dependencies: 23, 21\]\[Data dominators: \]\n\} @ \[21, 23\]\[Data dependencies: 23, 21\]\[Data dominators: 49\]
+st \(\) -> \{.a=.* @ \[2, 53\]\[Data dependencies: 53, 2\]\[Data dominators: \], .b=.* @ \[5, 53\]\[Data dependencies: 53, 5\]\[Data dominators: \]\} @ \[2, 5, 53\]\[Data dependencies: 53, 5, 2\]\[Data dominators: 53\]
+ar \(\) -> \{\[0\] = TOP @ \[11\, 47\]\[Data dependencies: 47\, 11\]\[Data dominators: \]\n\[1\] = TOP @ \[14\, 47\]\[Data dependencies: 47\, 14\]\[Data dominators: \]\n\} @ \[11\, 14\, 47\]\[Data dependencies: 47\, 14\, 11\]\[Data dominators: 47\]
+arr \(\) -> \{\[0\] = 1 @ \[19\]\[Data dependencies: 19\]\[Data dominators: 19\]\n\[1\] = 2 @ \[20\]\[Data dependencies: 20\]\[Data dominators: 20\]\n\[2\] = TOP @ \[21, 23\]\[Data dependencies: 23, 21\]\[Data dominators: \]\n\} @ \[21, 23\]\[Data dependencies: 23, 21\]\[Data dominators: 48\]
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/variable-sensitivity-dependence-graph-toyota/test.desc b/regression/goto-analyzer/variable-sensitivity-dependence-graph-toyota/test.desc
index 14b69051c4e..e74548e5815 100644
--- a/regression/goto-analyzer/variable-sensitivity-dependence-graph-toyota/test.desc
+++ b/regression/goto-analyzer/variable-sensitivity-dependence-graph-toyota/test.desc
@@ -3,35 +3,35 @@ main.c
 file1.c file2.c --dependence-graph-vs --vsd-structs every-field --vsd-arrays every-element --show
 ^EXIT=0$
 ^SIGNAL=0$
-^Data dependencies: 60 \[st.a\]$
-^Data dependencies: 60 \[st.b\]$
-^Data dependencies: 1 \[st.a\], 60 \[st.a\]$
-^Data dependencies: 4 \[st.b\], 60 \[st.b\]$
-^Data dependencies: 1 \[st.a\], 4 \[st.b\], 60 \[st.a, st.b\]$
-^Data dependencies: 54 \[ar\[\([^)]*\)0\]\]$
-^Data dependencies: 54 \[ar\[\([^)]*\)1\]\]$
-^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 54 \[ar\[\([^)]*\)0\]\]$
-^Data dependencies: 13 \[ar\[\([^)]*\)1\]\], 54 \[ar\[\([^)]*\)1\]\]$
-^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 13 \[ar\[\([^)]*\)1\]\], 54 \[ar\[\([^)]*\)0\], ar\[\([^)]*\)1\]\]$
+^Data dependencies: 59 \[st.a\]$
+^Data dependencies: 59 \[st.b\]$
+^Data dependencies: 1 \[st.a\], 59 \[st.a\]$
+^Data dependencies: 4 \[st.b\], 59 \[st.b\]$
+^Data dependencies: 1 \[st.a\], 4 \[st.b\], 59 \[st.a, st.b\]$
+^Data dependencies: 53 \[ar\[\([^)]*\)0\]\]$
+^Data dependencies: 53 \[ar\[\([^)]*\)1\]\]$
+^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 53 \[ar\[\([^)]*\)0\]\]$
+^Data dependencies: 13 \[ar\[\([^)]*\)1\]\], 53 \[ar\[\([^)]*\)1\]\]$
+^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 13 \[ar\[\([^)]*\)1\]\], 53 \[ar\[\([^)]*\)0\], ar\[\([^)]*\)1\]\]$
 ^Data dependencies: 19 \[arr\[\([^)]*\)1\]\]$
 ^Data dependencies: 18 \[arr\[\([^)]*\)0\]\]$
 ^Data dependencies: 19 \[arr\[\([^)]*\)1\]\]$
 ^Data dependencies: 20 \[arr\[\([^)]*\)2\]\], 22 \[arr\[\([^)]*\)2\]\]$
-^Data dependencies: 1 \[st.a\], 60 \[st.a\], 64 \[st.a\]$
-^Data dependencies: 4 \[st.b\], 60 \[st.b\], 67 \[st.b\]$
-^Data dependencies: 1 \[st.a\], 4 \[st.b\], 60 \[st.a, st.b\], 64 \[st.a\], 67 \[st.b\]$
-^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 54 \[ar\[\([^)]*\)0\]\], 75 \[ar\[\([^)]*\)0\]\]$
-^Data dependencies: 13 \[ar\[\([^)]*\)1\]\], 54 \[ar\[\([^)]*\)1\]\], 78 \[ar\[\([^)]*\)1\]\]$
-^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 13 \[ar\[\([^)]*\)1\]\], 54 \[ar\[\([^)]*\)0\], ar\[\([^)]*\)1\]\], 75 \[ar\[\([^)]*\)0\]\], 78 \[ar\[\([^)]*\)1\]\]$
-^Data dependencies: 1 \[st.a\], 60 \[st.a\]$
-^Data dependencies: 4 \[st.b\], 60 \[st.b\]$
-^Data dependencies: 1 \[st.a\], 60 \[st.a\], 64 \[st.a\]$
-^Data dependencies: 4 \[st.b\], 60 \[st.b\], 67 \[st.b\]$
-^Data dependencies: 1 \[st.a\], 4 \[st.b\], 60 \[st.a, st.b\], 64 \[st.a\], 67 \[st.b\]$
-^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 54 \[ar\[\([^)]*\)0\]\]$
-^Data dependencies: 13 \[ar\[\([^)]*\)1\]\], 54 \[ar\[\([^)]*\)1\]\]$
-^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 54 \[ar\[\([^)]*\)0\]\], 75 \[ar\[\([^)]*\)0\]\]$
-^Data dependencies: 13 \[ar\[\([^)]*\)1\]\], 54 \[ar\[\([^)]*\)1\]\], 78 \[ar\[\([^)]*\)1\]\]$
-^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 13 \[ar\[\([^)]*\)1\]\], 54 \[ar\[\([^)]*\)0\], ar\[\([^)]*\)1\]\], 75 \[ar\[\([^)]*\)0\]\], 78 \[ar\[\([^)]*\)1\]\]$
+^Data dependencies: 1 \[st.a\], 59 \[st.a\], 63 \[st.a\]$
+^Data dependencies: 4 \[st.b\], 59 \[st.b\], 66 \[st.b\]$
+^Data dependencies: 1 \[st.a\], 4 \[st.b\], 59 \[st.a, st.b\], 63 \[st.a\], 66 \[st.b\]$
+^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 53 \[ar\[\([^)]*\)0\]\], 74 \[ar\[\([^)]*\)0\]\]$
+^Data dependencies: 13 \[ar\[\([^)]*\)1\]\], 53 \[ar\[\([^)]*\)1\]\], 77 \[ar\[\([^)]*\)1\]\]$
+^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 13 \[ar\[\([^)]*\)1\]\], 53 \[ar\[\([^)]*\)0\], ar\[\([^)]*\)1\]\], 74 \[ar\[\([^)]*\)0\]\], 77 \[ar\[\([^)]*\)1\]\]$
+^Data dependencies: 1 \[st.a\], 59 \[st.a\]$
+^Data dependencies: 4 \[st.b\], 59 \[st.b\]$
+^Data dependencies: 1 \[st.a\], 59 \[st.a\], 63 \[st.a\]$
+^Data dependencies: 4 \[st.b\], 59 \[st.b\], 66 \[st.b\]$
+^Data dependencies: 1 \[st.a\], 4 \[st.b\], 59 \[st.a, st.b\], 63 \[st.a\], 66 \[st.b\]$
+^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 53 \[ar\[\([^)]*\)0\]\]$
+^Data dependencies: 13 \[ar\[\([^)]*\)1\]\], 53 \[ar\[\([^)]*\)1\]\]$
+^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 53 \[ar\[\([^)]*\)0\]\], 74 \[ar\[\([^)]*\)0\]\]$
+^Data dependencies: 13 \[ar\[\([^)]*\)1\]\], 53 \[ar\[\([^)]*\)1\]\], 77 \[ar\[\([^)]*\)1\]\]$
+^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 13 \[ar\[\([^)]*\)1\]\], 53 \[ar\[\([^)]*\)0\], ar\[\([^)]*\)1\]\], 74 \[ar\[\([^)]*\)0\]\], 77 \[ar\[\([^)]*\)1\]\]$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/variable-sensitivity-dependence-graph/test.desc b/regression/goto-analyzer/variable-sensitivity-dependence-graph/test.desc
index 181577f7052..2c643b4b78d 100644
--- a/regression/goto-analyzer/variable-sensitivity-dependence-graph/test.desc
+++ b/regression/goto-analyzer/variable-sensitivity-dependence-graph/test.desc
@@ -3,36 +3,36 @@ main.c
 file1.c file2.c --dependence-graph-vs --vsd-structs every-field --vsd-arrays every-element --show
 ^EXIT=0$
 ^SIGNAL=0$
-^Data dependencies: 60 \[st.a\]$
-^Data dependencies: 60 \[st.b\]$
-^Data dependencies: 1 \[st.a\], 60 \[st.a\]$
-^Data dependencies: 4 \[st.b\], 60 \[st.b\]$
-^Data dependencies: 1 \[st.a\], 4 \[st.b\], 60 \[st.a, st.b\]$
-^Data dependencies: 54 \[ar\[\([^)]*\)0\]\]$
+^Data dependencies: 59 \[st.a\]$
+^Data dependencies: 59 \[st.b\]$
+^Data dependencies: 1 \[st.a\], 59 \[st.a\]$
+^Data dependencies: 4 \[st.b\], 59 \[st.b\]$
+^Data dependencies: 1 \[st.a\], 4 \[st.b\], 59 \[st.a, st.b\]$
+^Data dependencies: 53 \[ar\[\([^)]*\)0\]\]$
 ^Data dependencies: 6 \[out1\]$
-^Data dependencies: 54 \[ar\[\([^)]*\)1\]\]$
-^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 54 \[ar\[\([^)]*\)0\]\]$
-^Data dependencies: 13 \[ar\[\([^)]*\)1\]\], 54 \[ar\[\([^)]*\)1\]\]$
-^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 13 \[ar\[\([^)]*\)1\]\], 54 \[ar\[\([^)]*\)0\], ar\[\([^)]*\)1\]\]$
+^Data dependencies: 53 \[ar\[\([^)]*\)1\]\]$
+^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 53 \[ar\[\([^)]*\)0\]\]$
+^Data dependencies: 13 \[ar\[\([^)]*\)1\]\], 53 \[ar\[\([^)]*\)1\]\]$
+^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 13 \[ar\[\([^)]*\)1\]\], 53 \[ar\[\([^)]*\)0\], ar\[\([^)]*\)1\]\]$
 ^Data dependencies: 19 \[arr\[\([^)]*\)1\]\]$
 ^Data dependencies: 18 \[arr\[\([^)]*\)0\]\]$
 ^Data dependencies: 19 \[arr\[\([^)]*\)1\]\]$
 ^Data dependencies: 20 \[arr\[\([^)]*\)2\]\], 22 \[arr\[\([^)]*\)2\]\]$
-^Data dependencies: 1 \[st.a\], 60 \[st.a\], 64 \[st.a\]$
-^Data dependencies: 4 \[st.b\], 60 \[st.b\], 67 \[st.b\]$
-^Data dependencies: 1 \[st.a\], 4 \[st.b\], 60 \[st.a, st.b\], 64 \[st.a\], 67 \[st.b\]$
-^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 54 \[ar\[\([^)]*\)0\]\], 75 \[ar\[\([^)]*\)0\]\]$
-^Data dependencies: 13 \[ar\[\([^)]*\)1\]\], 54 \[ar\[\([^)]*\)1\]\], 78 \[ar\[\([^)]*\)1\]\]$
-^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 13 \[ar\[\([^)]*\)1\]\], 54 \[ar\[\([^)]*\)0\], ar\[\([^)]*\)1\]\], 75 \[ar\[\([^)]*\)0\]\], 78 \[ar\[\([^)]*\)1\]\]$
-^Data dependencies: 1 \[st.a\], 60 \[st.a\]$
-^Data dependencies: 4 \[st.b\], 60 \[st.b\]$
-^Data dependencies: 1 \[st.a\], 60 \[st.a\], 64 \[st.a\]$
-^Data dependencies: 4 \[st.b\], 60 \[st.b\], 67 \[st.b\]$
-^Data dependencies: 1 \[st.a\], 4 \[st.b\], 60 \[st.a, st.b\], 64 \[st.a\], 67 \[st.b\]$
-^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 54 \[ar\[\([^)]*\)0\]\]$
-^Data dependencies: 13 \[ar\[\([^)]*\)1\]\], 54 \[ar\[\([^)]*\)1\]\]$
-^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 54 \[ar\[\([^)]*\)0\]\], 75 \[ar\[\([^)]*\)0\]\]$
-^Data dependencies: 13 \[ar\[\([^)]*\)1\]\], 54 \[ar\[\([^)]*\)1\]\], 78 \[ar\[\([^)]*\)1\]\]$
-^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 13 \[ar\[\([^)]*\)1\]\], 54 \[ar\[\([^)]*\)0\], ar\[\([^)]*\)1\]\], 75 \[ar\[\([^)]*\)0\]\], 78 \[ar\[\([^)]*\)1\]\]$
+^Data dependencies: 1 \[st.a\], 59 \[st.a\], 63 \[st.a\]$
+^Data dependencies: 4 \[st.b\], 59 \[st.b\], 66 \[st.b\]$
+^Data dependencies: 1 \[st.a\], 4 \[st.b\], 59 \[st.a, st.b\], 63 \[st.a\], 66 \[st.b\]$
+^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 53 \[ar\[\([^)]*\)0\]\], 74 \[ar\[\([^)]*\)0\]\]$
+^Data dependencies: 13 \[ar\[\([^)]*\)1\]\], 53 \[ar\[\([^)]*\)1\]\], 77 \[ar\[\([^)]*\)1\]\]$
+^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 13 \[ar\[\([^)]*\)1\]\], 53 \[ar\[\([^)]*\)0\], ar\[\([^)]*\)1\]\], 74 \[ar\[\([^)]*\)0\]\], 77 \[ar\[\([^)]*\)1\]\]$
+^Data dependencies: 1 \[st.a\], 59 \[st.a\]$
+^Data dependencies: 4 \[st.b\], 59 \[st.b\]$
+^Data dependencies: 1 \[st.a\], 59 \[st.a\], 63 \[st.a\]$
+^Data dependencies: 4 \[st.b\], 59 \[st.b\], 66 \[st.b\]$
+^Data dependencies: 1 \[st.a\], 4 \[st.b\], 59 \[st.a, st.b\], 63 \[st.a\], 66 \[st.b\]$
+^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 53 \[ar\[\([^)]*\)0\]\]$
+^Data dependencies: 13 \[ar\[\([^)]*\)1\]\], 53 \[ar\[\([^)]*\)1\]\]$
+^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 53 \[ar\[\([^)]*\)0\]\], 74 \[ar\[\([^)]*\)0\]\]$
+^Data dependencies: 13 \[ar\[\([^)]*\)1\]\], 53 \[ar\[\([^)]*\)1\]\], 77 \[ar\[\([^)]*\)1\]\]$
+^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 13 \[ar\[\([^)]*\)1\]\], 53 \[ar\[\([^)]*\)0\], ar\[\([^)]*\)1\]\], 74 \[ar\[\([^)]*\)0\]\], 77 \[ar\[\([^)]*\)1\]\]$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/variable-sensitivity-dependence-graph17/test.desc b/regression/goto-analyzer/variable-sensitivity-dependence-graph17/test.desc
index f75c010051c..9b1e9200e7c 100644
--- a/regression/goto-analyzer/variable-sensitivity-dependence-graph17/test.desc
+++ b/regression/goto-analyzer/variable-sensitivity-dependence-graph17/test.desc
@@ -4,5 +4,5 @@ main.c
 activate-multi-line-match
 ^EXIT=0$
 ^SIGNAL=0$
-\*\*\*\* 9 file .*main\.c line 22 function main\nControl dependencies: 36 \[UNCONDITIONAL\]\nData dependencies: 1 \[g_a\[\([^)]*\)i\]\], 2 \[g_a\[\([^)]*\)i\]\], 3 \[g_a\[\([^)]*\)i\]\], 7 \[g_a\[\([^)]*\)i\]\]
+\*\*\*\* 9 file .*main\.c line 22 function main\nControl dependencies: 35 \[UNCONDITIONAL\]\nData dependencies: 1 \[g_a\[\([^)]*\)i\]\], 2 \[g_a\[\([^)]*\)i\]\], 3 \[g_a\[\([^)]*\)i\]\], 7 \[g_a\[\([^)]*\)i\]\]
 --
diff --git a/src/analyses/escape_analysis.cpp b/src/analyses/escape_analysis.cpp
index 5fdb9a2d1c6..94ae7556d24 100644
--- a/src/analyses/escape_analysis.cpp
+++ b/src/analyses/escape_analysis.cpp
@@ -19,7 +19,6 @@ bool escape_domaint::is_tracked(const symbol_exprt &symbol)
   const irep_idt &identifier=symbol.get_identifier();
   if(
     identifier == CPROVER_PREFIX "memory_leak" ||
-    identifier == CPROVER_PREFIX "malloc_object" ||
     identifier == CPROVER_PREFIX "dead_object" ||
     identifier == CPROVER_PREFIX "deallocated")
   {
diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/src/ansi-c/ansi_c_internal_additions.cpp
index 4e20690d04c..fba813cd03a 100644
--- a/src/ansi-c/ansi_c_internal_additions.cpp
+++ b/src/ansi-c/ansi_c_internal_additions.cpp
@@ -178,8 +178,7 @@ void ansi_c_internal_additions(std::string &code)
     // malloc
     "const void *" CPROVER_PREFIX "deallocated=0;\n"
     "const void *" CPROVER_PREFIX "dead_object=0;\n"
-    "const void *" CPROVER_PREFIX "malloc_object=0;\n"
-    CPROVER_PREFIX "bool " CPROVER_PREFIX "malloc_is_new_array=0;\n" // for C++
+    "const void *" CPROVER_PREFIX "new_object=0;\n" // for C++
     "const void *" CPROVER_PREFIX "memory_leak=0;\n"
     "void *" CPROVER_PREFIX "allocate("
       CPROVER_PREFIX "size_t size, " CPROVER_PREFIX "bool zero);\n"
diff --git a/src/ansi-c/library/cprover.h b/src/ansi-c/library/cprover.h
index 6eb1776fda0..a60ae2ecb4b 100644
--- a/src/ansi-c/library/cprover.h
+++ b/src/ansi-c/library/cprover.h
@@ -12,8 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com
 typedef __typeof__(sizeof(int)) __CPROVER_size_t;
 void *__CPROVER_allocate(__CPROVER_size_t size, __CPROVER_bool zero);
 extern const void *__CPROVER_deallocated;
-extern const void *__CPROVER_malloc_object;
-extern _Bool __CPROVER_malloc_is_new_array;
+extern const void *__CPROVER_new_object;
 extern const void *__CPROVER_memory_leak;
 
 extern int __CPROVER_malloc_failure_mode;
diff --git a/src/ansi-c/library/stdlib.c b/src/ansi-c/library/stdlib.c
index 378e2fd0997..f5ae4c99aba 100644
--- a/src/ansi-c/library/stdlib.c
+++ b/src/ansi-c/library/stdlib.c
@@ -109,13 +109,6 @@ __CPROVER_HIDE:;
   __CPROVER_deallocated =
     (malloc_res == __CPROVER_deallocated) ? 0 : __CPROVER_deallocated;
 
-  // record the object size for non-determistic bounds checking
-  __CPROVER_bool record_malloc = __VERIFIER_nondet___CPROVER_bool();
-  __CPROVER_malloc_object =
-    record_malloc ? malloc_res : __CPROVER_malloc_object;
-  __CPROVER_malloc_is_new_array =
-    record_malloc ? 0 : __CPROVER_malloc_is_new_array;
-
   // detect memory leaks
   __CPROVER_bool record_may_leak = __VERIFIER_nondet___CPROVER_bool();
   __CPROVER_memory_leak = record_may_leak ? malloc_res : __CPROVER_memory_leak;
@@ -173,13 +166,6 @@ __CPROVER_HIDE:;
   __CPROVER_deallocated =
     (malloc_res == __CPROVER_deallocated) ? 0 : __CPROVER_deallocated;
 
-  // record the object size for non-determistic bounds checking
-  __CPROVER_bool record_malloc = __VERIFIER_nondet___CPROVER_bool();
-  __CPROVER_malloc_object =
-    record_malloc ? malloc_res : __CPROVER_malloc_object;
-  __CPROVER_malloc_is_new_array =
-    record_malloc ? 0 : __CPROVER_malloc_is_new_array;
-
   // detect memory leaks
   __CPROVER_bool record_may_leak = __VERIFIER_nondet___CPROVER_bool();
   __CPROVER_memory_leak = record_may_leak ? malloc_res : __CPROVER_memory_leak;
@@ -205,11 +191,6 @@ inline void *__builtin_alloca(__CPROVER_size_t alloca_size)
   // make sure it's not recorded as deallocated
   __CPROVER_deallocated=(res==__CPROVER_deallocated)?0:__CPROVER_deallocated;
 
-  // record the object size for non-determistic bounds checking
-  __CPROVER_bool record_malloc=__VERIFIER_nondet___CPROVER_bool();
-  __CPROVER_malloc_object=record_malloc?res:__CPROVER_malloc_object;
-  __CPROVER_malloc_is_new_array=record_malloc?0:__CPROVER_malloc_is_new_array;
-
   // record alloca to detect invalid free
   __CPROVER_bool record_alloca = __VERIFIER_nondet___CPROVER_bool();
   __CPROVER_alloca_object = record_alloca ? res : __CPROVER_alloca_object;
@@ -238,6 +219,7 @@ __CPROVER_HIDE:;
 #undef free
 
 __CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
+__CPROVER_bool __CPROVER_uninterpreted_is_new_array(const void *);
 extern void *__CPROVER_alloca_object;
 
 inline void free(void *ptr)
@@ -258,10 +240,10 @@ inline void free(void *ptr)
 
   // catch people who try to use free(...) for stuff
   // allocated with new[]
-  __CPROVER_precondition(ptr==0 ||
-                         __CPROVER_malloc_object!=ptr ||
-                         !__CPROVER_malloc_is_new_array,
-                         "free called for new[] object");
+  __CPROVER_precondition(
+    ptr == 0 || __CPROVER_new_object != ptr ||
+      !__CPROVER_uninterpreted_is_new_array(ptr),
+    "free called for new[] object");
 
   // catch people who try to use free(...) with alloca
   __CPROVER_precondition(
diff --git a/src/cpp/cpp_internal_additions.cpp b/src/cpp/cpp_internal_additions.cpp
index 3d5afe2955c..e07c2637f52 100644
--- a/src/cpp/cpp_internal_additions.cpp
+++ b/src/cpp/cpp_internal_additions.cpp
@@ -90,9 +90,7 @@ void cpp_internal_additions(std::ostream &out)
   // malloc
   out << "const void *" CPROVER_PREFIX "deallocated = 0;" << '\n';
   out << "const void *" CPROVER_PREFIX "dead_object = 0;" << '\n';
-  out << "const void *" CPROVER_PREFIX "malloc_object = 0;" << '\n';
-  out << "" CPROVER_PREFIX "bool " CPROVER_PREFIX "malloc_is_new_array = 0;"
-      << '\n';
+  out << "const void *" CPROVER_PREFIX "new_object = 0;" << '\n';
   out << "const void *" CPROVER_PREFIX "memory_leak = 0;" << '\n';
   out << "void *" CPROVER_PREFIX "allocate("
       << CPROVER_PREFIX "size_t size, " CPROVER_PREFIX "bool zero);" << '\n';
diff --git a/src/cpp/library/cprover.h b/src/cpp/library/cprover.h
index a89f8152337..83c61849e72 100644
--- a/src/cpp/library/cprover.h
+++ b/src/cpp/library/cprover.h
@@ -13,8 +13,7 @@ Author: Daniel Kroening, kroening@kroening.com
 typedef __typeof__(sizeof(int)) __CPROVER_size_t;
 void *__CPROVER_allocate(__CPROVER_size_t size, __CPROVER_bool zero);
 extern const void *__CPROVER_deallocated;
-extern const void *__CPROVER_malloc_object;
-extern _Bool __CPROVER_malloc_is_new_array;
+extern const void *__CPROVER_new_object;
 extern const void *__CPROVER_memory_leak;
 
 void __CPROVER_assume(__CPROVER_bool assumption) __attribute__((__noreturn__));
diff --git a/src/cpp/library/new.c b/src/cpp/library/new.c
index afae65b44c7..977361c17b7 100644
--- a/src/cpp/library/new.c
+++ b/src/cpp/library/new.c
@@ -1,6 +1,7 @@
 /* FUNCTION: __new */
 
 __CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
+__CPROVER_bool __CPROVER_uninterpreted_is_new_array(const void *);
 
 inline void *__new(__typeof__(sizeof(int)) malloc_size)
 {
@@ -13,10 +14,10 @@ inline void *__new(__typeof__(sizeof(int)) malloc_size)
   // ensure it's not recorded as deallocated
   __CPROVER_deallocated=(res==__CPROVER_deallocated)?0:__CPROVER_deallocated;
 
-  // non-derministically record the object size for bounds checking
+  // non-deterministically record the object for delete/delete[] checking
   __CPROVER_bool record_malloc=__VERIFIER_nondet___CPROVER_bool();
-  __CPROVER_malloc_object=record_malloc?res:__CPROVER_malloc_object;
-  __CPROVER_malloc_is_new_array=record_malloc?0:__CPROVER_malloc_is_new_array;
+  __CPROVER_new_object = record_malloc ? res : __CPROVER_new_object;
+  __CPROVER_assume(!__CPROVER_uninterpreted_is_new_array(res));
 
   // detect memory leaks
   __CPROVER_bool record_may_leak=__VERIFIER_nondet___CPROVER_bool();
@@ -28,6 +29,7 @@ inline void *__new(__typeof__(sizeof(int)) malloc_size)
 /* FUNCTION: __new_array */
 
 __CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
+__CPROVER_bool __CPROVER_uninterpreted_is_new_array(const void *);
 
 inline void *__new_array(__CPROVER_size_t count, __CPROVER_size_t size)
 {
@@ -40,10 +42,10 @@ inline void *__new_array(__CPROVER_size_t count, __CPROVER_size_t size)
   // ensure it's not recorded as deallocated
   __CPROVER_deallocated=(res==__CPROVER_deallocated)?0:__CPROVER_deallocated;
 
-  // non-deterministically record the object size for bounds checking
+  // non-deterministically record the object for delete/delete[] checking
   __CPROVER_bool record_malloc=__VERIFIER_nondet___CPROVER_bool();
-  __CPROVER_malloc_object=record_malloc?res:__CPROVER_malloc_object;
-  __CPROVER_malloc_is_new_array=record_malloc?1:__CPROVER_malloc_is_new_array;
+  __CPROVER_new_object = record_malloc ? res : __CPROVER_new_object;
+  __CPROVER_assume(__CPROVER_uninterpreted_is_new_array(res));
 
   // detect memory leaks
   __CPROVER_bool record_may_leak=__VERIFIER_nondet___CPROVER_bool();
@@ -66,6 +68,7 @@ inline void *__placement_new(__typeof__(sizeof(int)) malloc_size, void *p)
 /* FUNCTION: __delete */
 
 __CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
+__CPROVER_bool __CPROVER_uninterpreted_is_new_array(const void *);
 
 inline void __delete(void *ptr)
 {
@@ -80,10 +83,10 @@ inline void __delete(void *ptr)
   __CPROVER_precondition(ptr==0 || __CPROVER_deallocated!=ptr, "double delete");
 
   // catch people who call delete for objects allocated with new[]
-  __CPROVER_precondition(ptr==0 ||
-                         __CPROVER_malloc_object!=ptr ||
-                         !__CPROVER_malloc_is_new_array,
-                         "delete of array object");
+  __CPROVER_precondition(
+    ptr == 0 || __CPROVER_new_object != ptr ||
+      !__CPROVER_uninterpreted_is_new_array(ptr),
+    "delete of array object");
 
   // If ptr is NULL, no operation is performed.
   // This is a requirement by the standard, not generosity!
@@ -102,6 +105,7 @@ inline void __delete(void *ptr)
 /* FUNCTION: __delete_array */
 
 __CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
+__CPROVER_bool __CPROVER_uninterpreted_is_new_array(const void *);
 
 inline void __delete_array(void *ptr)
 {
@@ -120,10 +124,10 @@ inline void __delete_array(void *ptr)
                          "double delete");
 
   // catch people who call delete[] for objects allocated with new
-  __CPROVER_precondition(ptr==0 ||
-                         __CPROVER_malloc_object!=ptr ||
-                         __CPROVER_malloc_is_new_array,
-                         "delete[] of non-array object");
+  __CPROVER_precondition(
+    ptr == 0 || __CPROVER_new_object != ptr ||
+      __CPROVER_uninterpreted_is_new_array(ptr),
+    "delete[] of non-array object");
 
   if(ptr!=0)
   {
diff --git a/src/jsil/jsil_internal_additions.cpp b/src/jsil/jsil_internal_additions.cpp
index 636baf018a8..2583361d128 100644
--- a/src/jsil/jsil_internal_additions.cpp
+++ b/src/jsil/jsil_internal_additions.cpp
@@ -39,22 +39,6 @@ void jsil_internal_additions(symbol_tablet &dest)
     dest.add(symbol);
   }
 
-  // add __CPROVER_malloc_object
-
-  {
-    symbolt symbol;
-    symbol.base_name = CPROVER_PREFIX "malloc_object";
-    symbol.name=CPROVER_PREFIX "malloc_object";
-    symbol.type=pointer_type(empty_typet());
-    symbol.mode=ID_C;
-    symbol.is_lvalue=true;
-    symbol.is_state_var=true;
-    symbol.is_thread_local=true;
-    // mark as already typechecked
-    symbol.is_extern=true;
-    dest.add(symbol);
-  }
-
   // add eval
 
   {
diff --git a/src/util/pointer_predicates.cpp b/src/util/pointer_predicates.cpp
index e4c61a4dadf..4c0eb969b29 100644
--- a/src/util/pointer_predicates.cpp
+++ b/src/util/pointer_predicates.cpp
@@ -40,14 +40,6 @@ exprt pointer_offset(const exprt &pointer)
   return unary_exprt(ID_pointer_offset, pointer, signed_size_type());
 }
 
-exprt malloc_object(const exprt &pointer, const namespacet &ns)
-{
-  // we check __CPROVER_malloc_object!
-  const symbolt &malloc_object_symbol=ns.lookup(CPROVER_PREFIX "malloc_object");
-
-  return same_object(pointer, malloc_object_symbol.symbol_expr());
-}
-
 exprt deallocated(const exprt &pointer, const namespacet &ns)
 {
   // we check __CPROVER_deallocated!
diff --git a/src/util/pointer_predicates.h b/src/util/pointer_predicates.h
index 7a8d2a6f1a0..891a91cb8c6 100644
--- a/src/util/pointer_predicates.h
+++ b/src/util/pointer_predicates.h
@@ -22,8 +22,6 @@ exprt deallocated(const exprt &pointer, const namespacet &);
 exprt dead_object(const exprt &pointer, const namespacet &);
 exprt pointer_offset(const exprt &pointer);
 exprt pointer_object(const exprt &pointer);
-DEPRECATED(SINCE(2021, 5, 6, "Unnecessary, remove any use"))
-exprt malloc_object(const exprt &pointer, const namespacet &);
 exprt object_size(const exprt &pointer);
 DEPRECATED(SINCE(2021, 5, 6, "Use is_dynamic_object_exprt instead"))
 exprt dynamic_object(const exprt &pointer);