diff --git a/regression/cbmc-concurrency/thread_chain_cbmc1/main.c b/regression/cbmc-concurrency/thread_chain_cbmc1/main.c
index f9e0ab46b64..ed0471a5b18 100644
--- a/regression/cbmc-concurrency/thread_chain_cbmc1/main.c
+++ b/regression/cbmc-concurrency/thread_chain_cbmc1/main.c
@@ -18,7 +18,7 @@
 typedef unsigned long thread_id_t;
 
 // Internal unbounded array indexed by local thread identifiers
-extern __CPROVER_bool __CPROVER_threads_exited[];
+__CPROVER_bool __CPROVER_threads_exited[__CPROVER_constant_infinity_uint];
 
 // A thread_chain is like a chain of threads `f, g, ...` where `f`
 // must terminate before `g` can start to run, and so forth.
diff --git a/regression/cbmc-concurrency/thread_chain_cbmc2/main.c b/regression/cbmc-concurrency/thread_chain_cbmc2/main.c
index f9e0ab46b64..ed0471a5b18 100644
--- a/regression/cbmc-concurrency/thread_chain_cbmc2/main.c
+++ b/regression/cbmc-concurrency/thread_chain_cbmc2/main.c
@@ -18,7 +18,7 @@
 typedef unsigned long thread_id_t;
 
 // Internal unbounded array indexed by local thread identifiers
-extern __CPROVER_bool __CPROVER_threads_exited[];
+__CPROVER_bool __CPROVER_threads_exited[__CPROVER_constant_infinity_uint];
 
 // A thread_chain is like a chain of threads `f, g, ...` where `f`
 // must terminate before `g` can start to run, and so forth.
diff --git a/regression/cbmc-library/__atomic_always_lock_free-01/main.c b/regression/cbmc-library/__atomic_always_lock_free-01/main.c
index cfb762868e4..5b88bd587df 100644
--- a/regression/cbmc-library/__atomic_always_lock_free-01/main.c
+++ b/regression/cbmc-library/__atomic_always_lock_free-01/main.c
@@ -1,5 +1,9 @@
 #include <assert.h>
 
+#ifndef __GNUC__
+_Bool __atomic_always_lock_free(__CPROVER_size_t, void *);
+#endif
+
 int main()
 {
   assert(__atomic_always_lock_free(sizeof(int), 0));
diff --git a/regression/cbmc-library/__atomic_clear-01/main.c b/regression/cbmc-library/__atomic_clear-01/main.c
index 94a759177c5..57bf57abbc2 100644
--- a/regression/cbmc-library/__atomic_clear-01/main.c
+++ b/regression/cbmc-library/__atomic_clear-01/main.c
@@ -1,5 +1,9 @@
 #include <assert.h>
 
+#ifndef __GNUC__
+void __atomic_clear(_Bool *, int);
+#endif
+
 int main()
 {
   _Bool n;
diff --git a/regression/cbmc-library/__atomic_is_lock_free-01/main.c b/regression/cbmc-library/__atomic_is_lock_free-01/main.c
index 514abeaac5d..3ac747b7976 100644
--- a/regression/cbmc-library/__atomic_is_lock_free-01/main.c
+++ b/regression/cbmc-library/__atomic_is_lock_free-01/main.c
@@ -1,5 +1,9 @@
 #include <assert.h>
 
+#ifndef __GNUC__
+_Bool __atomic_is_lock_free(__CPROVER_size_t, void *);
+#endif
+
 int main()
 {
   assert(__atomic_is_lock_free(sizeof(int), 0));
diff --git a/regression/cbmc-library/__atomic_signal_fence-01/main.c b/regression/cbmc-library/__atomic_signal_fence-01/main.c
index 3a809cf651f..539a54287e5 100644
--- a/regression/cbmc-library/__atomic_signal_fence-01/main.c
+++ b/regression/cbmc-library/__atomic_signal_fence-01/main.c
@@ -1,5 +1,9 @@
 #include <assert.h>
 
+#ifndef __GNUC__
+void __atomic_signal_fence(int);
+#endif
+
 int main()
 {
   __atomic_signal_fence(0);
diff --git a/regression/cbmc-library/__atomic_test_and_set-01/main.c b/regression/cbmc-library/__atomic_test_and_set-01/main.c
index 9a9150b3766..4fdcf0ffb68 100644
--- a/regression/cbmc-library/__atomic_test_and_set-01/main.c
+++ b/regression/cbmc-library/__atomic_test_and_set-01/main.c
@@ -1,5 +1,9 @@
 #include <assert.h>
 
+#ifndef __GNUC__
+_Bool __atomic_test_and_set(void *, int);
+#endif
+
 int main()
 {
   char c = 0;
diff --git a/regression/cbmc-library/__atomic_thread_fence-01/main.c b/regression/cbmc-library/__atomic_thread_fence-01/main.c
index b9001b81810..dd08b8e1801 100644
--- a/regression/cbmc-library/__atomic_thread_fence-01/main.c
+++ b/regression/cbmc-library/__atomic_thread_fence-01/main.c
@@ -1,5 +1,9 @@
 #include <assert.h>
 
+#ifndef __GNUC__
+void __atomic_thread_fence(int);
+#endif
+
 int main()
 {
   __atomic_thread_fence(0);
diff --git a/regression/cbmc-library/__errno_location-01/main.c b/regression/cbmc-library/__errno_location-01/main.c
index 24329d09ff5..c32d17bf73b 100644
--- a/regression/cbmc-library/__errno_location-01/main.c
+++ b/regression/cbmc-library/__errno_location-01/main.c
@@ -1,9 +1,9 @@
 #include <assert.h>
 #include <errno.h>
 
-int main()
+int main(int arc, char *argv[])
 {
-  __errno_location();
-  assert(0);
+  // errno expands to use of __errno_location() with glibc
+  assert(errno == 0);
   return 0;
 }
diff --git a/regression/cbmc-library/__errno_location-01/test.desc b/regression/cbmc-library/__errno_location-01/test.desc
index 9542d988e8d..96c9b4bcd7b 100644
--- a/regression/cbmc-library/__errno_location-01/test.desc
+++ b/regression/cbmc-library/__errno_location-01/test.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 main.c
 --pointer-check --bounds-check
 ^EXIT=0$
diff --git a/regression/cbmc-library/_longjmp-01/main.c b/regression/cbmc-library/_longjmp-01/main.c
index cdac71afdc5..5be8777c4ed 100644
--- a/regression/cbmc-library/_longjmp-01/main.c
+++ b/regression/cbmc-library/_longjmp-01/main.c
@@ -1,5 +1,9 @@
 #include <setjmp.h>
 
+#ifndef __GNUC__
+#  define _longjmp(a, b) longjmp(a, b)
+#endif
+
 static jmp_buf env;
 
 int main()
diff --git a/regression/cbmc-library/_longjmp-01/test.desc b/regression/cbmc-library/_longjmp-01/test.desc
index c07910fc69d..b7d7e2001ce 100644
--- a/regression/cbmc-library/_longjmp-01/test.desc
+++ b/regression/cbmc-library/_longjmp-01/test.desc
@@ -1,8 +1,8 @@
 CORE
 main.c
 --pointer-check --bounds-check
-^\[_longjmp.assertion.1\] line 12 _longjmp requires instrumentation: FAILURE$
-^\[main.assertion.1\] line 8 unreachable: SUCCESS$
+^\[_?longjmp.assertion.1\] line 12 _?longjmp requires instrumentation: FAILURE$
+^\[main.assertion.1\] line 12 unreachable: SUCCESS$
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$
diff --git a/regression/cbmc-library/alloca-02/main.c b/regression/cbmc-library/alloca-02/main.c
index 27dd244c4ad..d23244d6a88 100644
--- a/regression/cbmc-library/alloca-02/main.c
+++ b/regression/cbmc-library/alloca-02/main.c
@@ -4,9 +4,14 @@
 void *alloca(size_t alloca_size);
 #endif
 
+// intentionally type conflicting: the built-in library uses const void*; this
+// is to check that object type updates are performed
+extern const char *__CPROVER_alloca_object;
+
 int *foo()
 {
   int *foo_ptr = alloca(sizeof(int));
+  __CPROVER_assert(foo_ptr == __CPROVER_alloca_object, "may fail");
   return foo_ptr;
 }
 
diff --git a/regression/cbmc-library/alloca-02/test.desc b/regression/cbmc-library/alloca-02/test.desc
index 3c2405a8436..273ea7118de 100644
--- a/regression/cbmc-library/alloca-02/test.desc
+++ b/regression/cbmc-library/alloca-02/test.desc
@@ -2,7 +2,7 @@ CORE
 main.c
 --pointer-check
 dereference failure: dead object in \*from_foo: FAILURE$
-^\*\* 1 of 6 failed
+^\*\* 2 of 7 failed
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$
diff --git a/regression/cbmc-library/memcpy-07/main.c b/regression/cbmc-library/memcpy-07/main.c
index 06ad39e2b74..971509901fc 100644
--- a/regression/cbmc-library/memcpy-07/main.c
+++ b/regression/cbmc-library/memcpy-07/main.c
@@ -1,4 +1,5 @@
 // #include <string.h> intentionally omitted
+void *memcpy();
 
 struct c
 {
diff --git a/regression/cbmc/String_Abstraction17/strcpy-no-decl.c b/regression/cbmc/String_Abstraction17/strcpy-no-decl.c
index 0e7a93df5e6..17c80a7a2d5 100644
--- a/regression/cbmc/String_Abstraction17/strcpy-no-decl.c
+++ b/regression/cbmc/String_Abstraction17/strcpy-no-decl.c
@@ -1,4 +1,5 @@
-void *malloc(unsigned);
+#include <stdlib.h>
+// string.h intentionally omitted
 
 char *make_str()
 {
diff --git a/regression/cbmc/String_Abstraction17/test.desc b/regression/cbmc/String_Abstraction17/test.desc
index ea2896bae68..ad0106474bd 100644
--- a/regression/cbmc/String_Abstraction17/test.desc
+++ b/regression/cbmc/String_Abstraction17/test.desc
@@ -1,11 +1,13 @@
 CORE
 strcpy-no-decl.c
 --string-abstraction --validate-goto-model
-Condition: strlen type inconsistency
-^EXIT=(127|134)$
+^EXIT=10$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-While this test currently passes when omitting --validate-goto-model, we should
-expect a report of type inconsistencies as no forward declarations are present.
+The linker is able to fix up type inconsistencies of the missing function
+declarations, but the absence of a declaration of strlen results in not picking
+up the library model. Consequently the assumption does not work as intended, and
+verification fails. Adding #include <string.h> makes verification pass as
+expected.
diff --git a/regression/cbmc/array_of_bool_as_bitvec/main.c b/regression/cbmc/array_of_bool_as_bitvec/main.c
index 19888bb1a45..07106dde3d2 100644
--- a/regression/cbmc/array_of_bool_as_bitvec/main.c
+++ b/regression/cbmc/array_of_bool_as_bitvec/main.c
@@ -3,6 +3,7 @@
 #include <stdlib.h>
 
 __CPROVER_bool w[8];
+__CPROVER_bool v[__CPROVER_constant_infinity_uint];
 
 void main()
 {
diff --git a/regression/cbmc/array_of_bool_as_bitvec/test-smt2-outfile.desc b/regression/cbmc/array_of_bool_as_bitvec/test-smt2-outfile.desc
index ae228a04e44..a7ede3fc945 100644
--- a/regression/cbmc/array_of_bool_as_bitvec/test-smt2-outfile.desc
+++ b/regression/cbmc/array_of_bool_as_bitvec/test-smt2-outfile.desc
@@ -1,15 +1,15 @@
 CORE broken-smt-backend
 main.c
 --smt2 --outfile -
-\(= \(select array_of\.2 i\) \(ite false #b1 #b0\)\)
-\(= \(select array\.3 \(\(_ zero_extend 32\) \|main::1::idx!0@1#1\|\)\) #b1\)
-\(= \(select array\.3 \(_ bv\d+ 64\)\) \(ite false #b1 #b0\)\)
+\(= \(select array_of\.0 i\) \(ite false #b1 #b0\)\)
+\(= \(select array\.1 \(\(_ zero_extend 32\) \|main::1::idx!0@1#1\|\)\) #b1\)
+\(= \(select array\.1 \(_ bv\d+ 64\)\) \(ite false #b1 #b0\)\)
 ^EXIT=0$
 ^SIGNAL=0$
 --
-\(= \(select array_of\.2 i\) false\)
-\(= \(select array\.3 \(\(_ zero_extend 32\) \|main::1::idx!0@1#1\|\)\) #b1 #b0\)
-\(= \(select array\.3 \(_ bv\d+ 64\)\) false\)
+\(= \(select array_of\.0 i\) false\)
+\(= \(select array\.1 \(\(_ zero_extend 32\) \|main::1::idx!0@1#1\|\)\) #b1 #b0\)
+\(= \(select array\.1 \(_ bv\d+ 64\)\) false\)
 --
 This test checks for correctness of BitVec-array encoding of Boolean arrays.
 
diff --git a/regression/cbmc/enum-trace1/main.c b/regression/cbmc/enum-trace1/main.c
index b4e8ce48d74..2256efc27c1 100644
--- a/regression/cbmc/enum-trace1/main.c
+++ b/regression/cbmc/enum-trace1/main.c
@@ -16,6 +16,9 @@ typedef enum ENUMT
 
 void test(enum ENUM e, enum_t t)
 {
+  // ensure sane input values
+  __CPROVER_assume(__CPROVER_enum_is_in_range(e));
+  __CPROVER_assume(__CPROVER_enum_is_in_range(t));
   enum ENUM ee = e;
   enum_t tt = t;
 
diff --git a/regression/cbmc/xml-escaping/debug_output.desc b/regression/cbmc/xml-escaping/debug_output.desc
index ddfb415c818..af4f42c9fa8 100644
--- a/regression/cbmc/xml-escaping/debug_output.desc
+++ b/regression/cbmc/xml-escaping/debug_output.desc
@@ -4,7 +4,6 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 VERIFICATION FAILED
-⇔ false
 \¬main\:\:1\:\:x\!0\@1\#1
 --
 XML does not support escaping non-printable character
diff --git a/regression/cbmc/xml-trace/test.desc b/regression/cbmc/xml-trace/test.desc
index 5ed215d69a5..999afcec05a 100644
--- a/regression/cbmc/xml-trace/test.desc
+++ b/regression/cbmc/xml-trace/test.desc
@@ -7,7 +7,7 @@ activate-multi-line-match
 VERIFICATION FAILED
 <assignment assignment_type="actual_parameter" base_name="u" display_name="test::u" hidden="false" identifier="test::u" mode="C" step_nr="\d+" thread="0">\n\s*<location file=".*" line="\d+" working-directory=".*"/>\n\s*<full_lhs_type>union myunion</full_lhs_type>\n\s*<full_lhs>u</full_lhs>
 <value>\{ \.i=\d+ll? \}</value>\n\s*<value_expression>\n\s*<union>\n\s*<member member_name="i">\n\s*<integer binary="\d+" c_type=".*int.*" width="\d+">\d+</integer>\n\s*</member>\n\s*</union>\n\s*</value_expression>
-<assignment assignment_type="state" base_name="u" display_name="test::u" hidden="false" identifier="test::u" mode="C" step_nr="\d+" thread="0">\n\s*<location file=".*" function="test" line="\d+" working-directory=".*"/>\n\s*<full_lhs_type>signed long( long)? int</full_lhs_type>\n\s*<full_lhs>u\.i</full_lhs>\n\s*<full_lhs_value binary="[01]+">\d+ll?</full_lhs_value>\n\s*</assignment>
+<assignment assignment_type="state" base_name="u" display_name="test::u" hidden="false" identifier="test::u" mode="C" step_nr="\d+" thread="0">\n\s*<location file=".*" function="test" line="\d+" working-directory=".*"/>\n\s*<full_lhs_type>(signed long( long)? int|int64_t)</full_lhs_type>\n\s*<full_lhs>u\.i</full_lhs>\n\s*<full_lhs_value binary="[01]+">\d+ll?</full_lhs_value>\n\s*</assignment>
 --
 ^warning: ignoring
 --
diff --git a/regression/cprover/arrays/array1.desc b/regression/cprover/arrays/array1.desc
index 896115d8009..37b1ff5a824 100644
--- a/regression/cprover/arrays/array1.desc
+++ b/regression/cprover/arrays/array1.desc
@@ -3,11 +3,11 @@ array1.c
 --text --solve --inline --no-safety
 ^EXIT=10$
 ^SIGNAL=0$
-^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[element_address\(❝array❞, .*1.*\):=10\]\)$
-^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[element_address\(❝array❞, .*2.*\):=20\]\)$
-^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(element_address\(❝array❞, .*1.*\)\) = 10\)$
-^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ \(ς\(element_address\(❝array❞, .*2.*\)\) = 20\)$
-^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(element_address\(❝array❞, .*2.*\)\) = 30\)$
+^\(\d+\) ∀ ς : state \. S10\(ς\) ⇒ S11\(ς\[element_address\(❝array❞, .*1.*\):=10\]\)$
+^\(\d+\) ∀ ς : state \. S11\(ς\) ⇒ S12\(ς\[element_address\(❝array❞, .*2.*\):=20\]\)$
+^\(\d+\) ∀ ς : state \. S12\(ς\) ⇒ \(ς\(element_address\(❝array❞, .*1.*\)\) = 10\)$
+^\(\d+\) ∀ ς : state \. S13\(ς\) ⇒ \(ς\(element_address\(❝array❞, .*2.*\)\) = 20\)$
+^\(\d+\) ∀ ς : state \. S14\(ς\) ⇒ \(ς\(element_address\(❝array❞, .*2.*\)\) = 30\)$
 ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
 ^\[main\.assertion\.2\] line \d+ property 2: SUCCESS$
 ^\[main\.assertion\.3\] line \d+ property 3: REFUTED$
diff --git a/regression/cprover/arrays/array2.desc b/regression/cprover/arrays/array2.desc
index 75f86008155..c9d515beef2 100644
--- a/regression/cprover/arrays/array2.desc
+++ b/regression/cprover/arrays/array2.desc
@@ -3,9 +3,9 @@ array2.c
 --text --solve --inline --no-safety
 ^EXIT=10$
 ^SIGNAL=0$
-^\(\d+\) ∀ ς : state \. \(S23\(ς\) ∧ ς\(❝main::1::i❞\) = ς\(❝main::1::j❞\)\) ⇒ S24\(ς\)$
-^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(element_address\(❝main::1::array❞, cast\(ς\(❝main::1::i❞\), signedbv\[64\]\)\)\) = ς\(element_address\(❝main::1::array❞, cast\(ς\(❝main::1::j❞\), signedbv\[64\]\)\)\)\)$
-^\(\d+\) ∀ ς : state \. S25\(ς\) ⇒ \(ς\(element_address\(❝main::1::array❞, cast\(ς\(❝main::1::i❞\), signedbv\[64\]\)\)\) = ς\(element_address\(❝main::1::array❞, cast\(ς\(❝main::1::k❞\), signedbv\[64\]\)\)\)\)$
+^\(\d+\) ∀ ς : state \. \(S13\(ς\) ∧ ς\(❝main::1::i❞\) = ς\(❝main::1::j❞\)\) ⇒ S14\(ς\)$
+^\(\d+\) ∀ ς : state \. S14\(ς\) ⇒ \(ς\(element_address\(❝main::1::array❞, cast\(ς\(❝main::1::i❞\), signedbv\[64\]\)\)\) = ς\(element_address\(❝main::1::array❞, cast\(ς\(❝main::1::j❞\), signedbv\[64\]\)\)\)\)$
+^\(\d+\) ∀ ς : state \. S15\(ς\) ⇒ \(ς\(element_address\(❝main::1::array❞, cast\(ς\(❝main::1::i❞\), signedbv\[64\]\)\)\) = ς\(element_address\(❝main::1::array❞, cast\(ς\(❝main::1::k❞\), signedbv\[64\]\)\)\)\)$
 ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
 ^\[main\.assertion\.2\] line \d+ property 2: REFUTED$
 --
diff --git a/regression/cprover/basic/assume1.desc b/regression/cprover/basic/assume1.desc
index 9ce490abc7c..80e691c1dfd 100644
--- a/regression/cprover/basic/assume1.desc
+++ b/regression/cprover/basic/assume1.desc
@@ -6,9 +6,9 @@ assume1.c
 ^ \(\d+\) ∀ ς : state \. initial_state\(ς\) ⇒ SInitial\(ς\)$
 ^ \(\d+\) S0 = SInitial$
 ^ \(\d+\) S1 = S0$
-^\(\d+\) ∀ ς : state \. \(S20\(ς\) ∧ ς\(❝main::1::x❞\) ≥ 10\) ⇒ S21\(ς\)$
-^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ \(ς\(❝main::1::x❞\) ≥ 5\)$
-^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(❝main::1::x❞\) ≥ 15\)$
+^\(\d+\) ∀ ς : state \. \(S10\(ς\) ∧ ς\(❝main::1::x❞\) ≥ 10\) ⇒ S11\(ς\)$
+^\(\d+\) ∀ ς : state \. S11\(ς\) ⇒ \(ς\(❝main::1::x❞\) ≥ 5\)$
+^\(\d+\) ∀ ς : state \. S12\(ς\) ⇒ \(ς\(❝main::1::x❞\) ≥ 15\)$
 ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
 ^\[main\.assertion\.2\] line \d+ property 2: REFUTED$
 --
diff --git a/regression/cprover/basic/basic1.desc b/regression/cprover/basic/basic1.desc
index 11a7b0ad24c..a8de994b8a6 100644
--- a/regression/cprover/basic/basic1.desc
+++ b/regression/cprover/basic/basic1.desc
@@ -5,8 +5,8 @@ basic1.c
 ^SIGNAL=0$
 ^ \(\d+\) ∀ ς : state \. initial_state\(ς\) ⇒ SInitial\(ς\)$
 ^ \(\d+\) S0 = SInitial$
-^\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[❝x❞:=0\]\)$
-^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝x❞:=1\]\)$
-^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ \(ς\(❝x❞\) = 1\)$
+^\(\d+\) ∀ ς : state \. S7\(ς\) ⇒ S8\(ς\[❝x❞:=0\]\)$
+^\(\d+\) ∀ ς : state \. S10\(ς\) ⇒ S11\(ς\[❝x❞:=1\]\)$
+^\(\d+\) ∀ ς : state \. S11\(ς\) ⇒ \(ς\(❝x❞\) = 1\)$
 ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
 --
diff --git a/regression/cprover/basic/basic2.desc b/regression/cprover/basic/basic2.desc
index 297a94c2fc5..ecbef615ff7 100644
--- a/regression/cprover/basic/basic2.desc
+++ b/regression/cprover/basic/basic2.desc
@@ -3,11 +3,11 @@ basic2.c
 --text --solve --inline
 ^EXIT=0$
 ^SIGNAL=0$
-^\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[❝x❞:=0\]\)$
-^\(\d+\) S19 = S18$
-^\(\d+\) S20 = S19$
-^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝x❞:=1\]\)$
-^\(\d+\) S22 = S21$
-^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(❝x❞\) = 1\)$
+^\(\d+\) ∀ ς : state \. S7\(ς\) ⇒ S8\(ς\[❝x❞:=0\]\)$
+^\(\d+\) S9 = S8$
+^\(\d+\) S10 = S9$
+^\(\d+\) ∀ ς : state \. S10\(ς\) ⇒ S11\(ς\[❝x❞:=1\]\)$
+^\(\d+\) S12 = S11$
+^\(\d+\) ∀ ς : state \. S12\(ς\) ⇒ \(ς\(❝x❞\) = 1\)$
 ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
 --
diff --git a/regression/cprover/basic/basic3.desc b/regression/cprover/basic/basic3.desc
index eb2127fbc7b..a8631aef078 100644
--- a/regression/cprover/basic/basic3.desc
+++ b/regression/cprover/basic/basic3.desc
@@ -3,10 +3,10 @@ basic3.c
 --text --solve --inline
 ^EXIT=0$
 ^SIGNAL=0$
-\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[❝x❞:=0\]\)
-\(\d+\) ∀ ς : state \. S18\(ς\) ⇒ S19\(ς\[❝y❞:=0\]\)
-\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝x❞:=1\]\)
-\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝y❞:=2\]\)
-\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ \(ς\(❝x❞\) = 1\)
+\(\d+\) ∀ ς : state \. S7\(ς\) ⇒ S8\(ς\[❝x❞:=0\]\)
+\(\d+\) ∀ ς : state \. S8\(ς\) ⇒ S9\(ς\[❝y❞:=0\]\)
+\(\d+\) ∀ ς : state \. S11\(ς\) ⇒ S12\(ς\[❝x❞:=1\]\)
+\(\d+\) ∀ ς : state \. S12\(ς\) ⇒ S13\(ς\[❝y❞:=2\]\)
+\(\d+\) ∀ ς : state \. S13\(ς\) ⇒ \(ς\(❝x❞\) = 1\)
 ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
 --
diff --git a/regression/cprover/basic/basic4.desc b/regression/cprover/basic/basic4.desc
index 1aaf8f0de0e..bca24eb3a18 100644
--- a/regression/cprover/basic/basic4.desc
+++ b/regression/cprover/basic/basic4.desc
@@ -3,9 +3,9 @@ basic4.c
 --text --solve --inline
 ^EXIT=10$
 ^SIGNAL=0$
-^\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[❝x❞:=0\]\)$
-^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝x❞:=1\]\)$
-^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝x❞:=2\]\)$
-^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(❝x❞\) = 1\)$
+^\(\d+\) ∀ ς : state \. S7\(ς\) ⇒ S8\(ς\[❝x❞:=0\]\)$
+^\(\d+\) ∀ ς : state \. S10\(ς\) ⇒ S11\(ς\[❝x❞:=1\]\)$
+^\(\d+\) ∀ ς : state \. S11\(ς\) ⇒ S12\(ς\[❝x❞:=2\]\)$
+^\(\d+\) ∀ ς : state \. S12\(ς\) ⇒ \(ς\(❝x❞\) = 1\)$
 ^\[main\.assertion\.1\] line \d+ property 1: REFUTED$
 --
diff --git a/regression/cprover/basic/basic5.desc b/regression/cprover/basic/basic5.desc
index d0f62ff8464..2ac5fe52cba 100644
--- a/regression/cprover/basic/basic5.desc
+++ b/regression/cprover/basic/basic5.desc
@@ -3,12 +3,12 @@ basic5.c
 --text --solve --inline
 ^EXIT=10$
 ^SIGNAL=0$
-^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝main::1::c1❞:=ς\(❝main::1::x❞\) ≥ 10\]\)$
-^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S23\(enter_scope_state\(ς, ❝main::1::c2❞\)\)$
-^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ S24\(ς\[❝main::1::c2❞:=ς\(❝main::1::x❞\) ≥ 5\]\)$
-^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(❝main::1::c1❞\) ⇒ ς\(❝main::1::c2❞\)\)$
-^\(\d+\) S25 = S24$
-^\(\d+\) ∀ ς : state \. S25\(ς\) ⇒ \(ς\(❝main::1::c2❞\) ⇒ ς\(❝main::1::c1❞\)\)$
+^\(\d+\) ∀ ς : state \. S11\(ς\) ⇒ S12\(ς\[❝main::1::c1❞:=ς\(❝main::1::x❞\) ≥ 10\]\)$
+^\(\d+\) ∀ ς : state \. S12\(ς\) ⇒ S13\(enter_scope_state\(ς, ❝main::1::c2❞\)\)$
+^\(\d+\) ∀ ς : state \. S13\(ς\) ⇒ S14\(ς\[❝main::1::c2❞:=ς\(❝main::1::x❞\) ≥ 5\]\)$
+^\(\d+\) ∀ ς : state \. S14\(ς\) ⇒ \(ς\(❝main::1::c1❞\) ⇒ ς\(❝main::1::c2❞\)\)$
+^\(\d+\) S15 = S14$
+^\(\d+\) ∀ ς : state \. S15\(ς\) ⇒ \(ς\(❝main::1::c2❞\) ⇒ ς\(❝main::1::c1❞\)\)$
 ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
 ^\[main\.assertion\.2\] line \d+ property 2: REFUTED$
 --
diff --git a/regression/cprover/basic/basic6.desc b/regression/cprover/basic/basic6.desc
index 7bbc6dd7c54..be02c9414c6 100644
--- a/regression/cprover/basic/basic6.desc
+++ b/regression/cprover/basic/basic6.desc
@@ -3,11 +3,11 @@ basic6.c
 --text --solve --inline
 ^EXIT=0$
 ^SIGNAL=0$
-^\(23\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝x❞:=1\]\)$
-^\(24\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝x❞:=ς\(❝x❞\) \+ 1\]\)$
-^\(25\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝x❞:=ς\(❝x❞\) \+ 1\]\)$
-^\(26\) ∀ ς : state \. S23\(ς\) ⇒ S24\(ς\[❝x❞:=ς\(❝x❞\) \+ 1\]\)$
-^\(27\) ∀ ς : state \. S24\(ς\) ⇒ S25\(ς\[❝x❞:=ς\(❝x❞\) \+ 1\]\)$
-^\(28\) ∀ ς : state \. S25\(ς\) ⇒ \(ς\(❝x❞\) = 5\)$
+^\(13\) ∀ ς : state \. S10\(ς\) ⇒ S11\(ς\[❝x❞:=1\]\)$
+^\(14\) ∀ ς : state \. S11\(ς\) ⇒ S12\(ς\[❝x❞:=ς\(❝x❞\) \+ 1\]\)$
+^\(15\) ∀ ς : state \. S12\(ς\) ⇒ S13\(ς\[❝x❞:=ς\(❝x❞\) \+ 1\]\)$
+^\(16\) ∀ ς : state \. S13\(ς\) ⇒ S14\(ς\[❝x❞:=ς\(❝x❞\) \+ 1\]\)$
+^\(17\) ∀ ς : state \. S14\(ς\) ⇒ S15\(ς\[❝x❞:=ς\(❝x❞\) \+ 1\]\)$
+^\(18\) ∀ ς : state \. S15\(ς\) ⇒ \(ς\(❝x❞\) = 5\)$
 ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
 --
diff --git a/regression/cprover/basic/nondet1.desc b/regression/cprover/basic/nondet1.desc
index f902da15fbd..31a0da25664 100644
--- a/regression/cprover/basic/nondet1.desc
+++ b/regression/cprover/basic/nondet1.desc
@@ -3,13 +3,13 @@ nondet1.c
 --text --solve --inline
 ^EXIT=10$
 ^SIGNAL=0$
-^\(\d+\) ∀ ς : state, nondet::S22-0 : signedbv\[32\] \. S21\(ς\) ⇒ S22\(ς\[❝main::1::x❞:=nondet::S22-0\]\)$
-^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(❝main::1::x❞\) = 20\)$
-^\(\d+\) S23 = S22$
-^\(\d+\) ∀ ς : state, nondet::S24-0 : signedbv\[32\] \. S23\(ς\) ⇒ S24\(ς\[❝main::1::y❞:=nondet::S24-0\]\)$
-^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(❝main::1::x❞\) = ς\(❝main::1::y❞\)\)$
-^\(\d+\) S25 = S24$
-^\(\d+\) ∀ ς : state \. S25\(ς\) ⇒ S26\(ς\[❝return'❞:=0\]\)$
+^\(\d+\) ∀ ς : state, nondet::S12-0 : signedbv\[32\] \. S11\(ς\) ⇒ S12\(ς\[❝main::1::x❞:=nondet::S12-0\]\)$
+^\(\d+\) ∀ ς : state \. S12\(ς\) ⇒ \(ς\(❝main::1::x❞\) = 20\)$
+^\(\d+\) S13 = S12$
+^\(\d+\) ∀ ς : state, nondet::S14-0 : signedbv\[32\] \. S13\(ς\) ⇒ S14\(ς\[❝main::1::y❞:=nondet::S14-0\]\)$
+^\(\d+\) ∀ ς : state \. S14\(ς\) ⇒ \(ς\(❝main::1::x❞\) = ς\(❝main::1::y❞\)\)$
+^\(\d+\) S15 = S14$
+^\(\d+\) ∀ ς : state \. S15\(ς\) ⇒ S16\(ς\[❝return'❞:=0\]\)$
 ^\[main\.assertion\.1\] line \d+ property 1: REFUTED$
 ^\[main\.assertion\.2\] line \d+ property 2: REFUTED$
 --
diff --git a/regression/cprover/branching/branching1.desc b/regression/cprover/branching/branching1.desc
index ff64a86eb44..21517818990 100644
--- a/regression/cprover/branching/branching1.desc
+++ b/regression/cprover/branching/branching1.desc
@@ -3,20 +3,20 @@ branching1.c
 --text --solve --inline
 ^EXIT=10$
 ^SIGNAL=0$
-^\(\d+\) ∀ ς : state \. \(S20\(ς\) ∧ ¬\(ς\(❝main::1::x❞\) ≥ 5\)\) ⇒ S21T\(\ς\)$
-^\(\d+\) ∀ ς : state \. \(S20\(ς\) ∧ ς\(❝main::1::x❞\) ≥ 5\) ⇒ S21\(ς\)$
-^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ \(ς\(❝main::1::x❞\) ≥ 5\)$
-^\(\d+\) S22 = S21$
-^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(0 ≠ 0\)$
-^\(\d+\) S23 = S22$
-^\(\d+\) S24 = S23$
-^\(\d+\) ∀ ς : state \. S21T\(ς\) ⇒ \(ς\(❝main::1::x❞\) < 5\)$
-^\(\d+\) S25 = S21T$
-^\(\d+\) ∀ ς : state \. S25\(ς\) ⇒ \(0 ≠ 0\)$
-^\(\d+\) S26 = S25$
-^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ S27in\(ς\)$
-^\(\d+\) ∀ ς : state \. S26\(ς\) ⇒ S27in\(ς\)$
-^\(\d+\) S27 = S27in$
+^\(\d+\) ∀ ς : state \. \(S10\(ς\) ∧ ¬\(ς\(❝main::1::x❞\) ≥ 5\)\) ⇒ S11T\(\ς\)$
+^\(\d+\) ∀ ς : state \. \(S10\(ς\) ∧ ς\(❝main::1::x❞\) ≥ 5\) ⇒ S11\(ς\)$
+^\(\d+\) ∀ ς : state \. S11\(ς\) ⇒ \(ς\(❝main::1::x❞\) ≥ 5\)$
+^\(\d+\) S12 = S11$
+^\(\d+\) ∀ ς : state \. S12\(ς\) ⇒ \(0 ≠ 0\)$
+^\(\d+\) S13 = S12$
+^\(\d+\) S14 = S13$
+^\(\d+\) ∀ ς : state \. S11T\(ς\) ⇒ \(ς\(❝main::1::x❞\) < 5\)$
+^\(\d+\) S15 = S11T$
+^\(\d+\) ∀ ς : state \. S15\(ς\) ⇒ \(0 ≠ 0\)$
+^\(\d+\) S16 = S15$
+^\(\d+\) ∀ ς : state \. S14\(ς\) ⇒ S17in\(ς\)$
+^\(\d+\) ∀ ς : state \. S16\(ς\) ⇒ S17in\(ς\)$
+^\(\d+\) S17 = S17in$
 ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
 ^\[main\.assertion\.2\] line \d+ property 2: REFUTED$
 ^\[main\.assertion\.3\] line \d+ property 3: SUCCESS$
diff --git a/regression/cprover/branching/branching2.desc b/regression/cprover/branching/branching2.desc
index 53d98c6674a..286cb86aa81 100644
--- a/regression/cprover/branching/branching2.desc
+++ b/regression/cprover/branching/branching2.desc
@@ -3,14 +3,14 @@ branching2.c
 --text --solve --inline
 ^EXIT=10$
 ^SIGNAL=0$
-^\(\d+\) ∀ ς : state \. \(S21\(ς\) ∧ ¬\(ς\(❝main::1::a❞\) ≥ 5\)\) ⇒ S22T\(ς\)$
-^\(\d+\) ∀ ς : state \. \(S21\(ς\) ∧ ς\(❝main::1::a❞\) ≥ 5\) ⇒ S22\(ς\)$
-^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝main::1::b❞:=1\]\)$
-^\(\d+\) S24 = S23$
-^\(\d+\) ∀ ς : state \. S22T\(ς\) ⇒ S25\(ς\[❝main::1::b❞:=0\]\)$
-^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ S26in\(ς\)$
-^\(\d+\) ∀ ς : state \. S25\(ς\) ⇒ S26in\(ς\)$
-^\(\d+\) S26 = S26in$
+^\(\d+\) ∀ ς : state \. \(S11\(ς\) ∧ ¬\(ς\(❝main::1::a❞\) ≥ 5\)\) ⇒ S12T\(ς\)$
+^\(\d+\) ∀ ς : state \. \(S11\(ς\) ∧ ς\(❝main::1::a❞\) ≥ 5\) ⇒ S12\(ς\)$
+^\(\d+\) ∀ ς : state \. S12\(ς\) ⇒ S13\(ς\[❝main::1::b❞:=1\]\)$
+^\(\d+\) S14 = S13$
+^\(\d+\) ∀ ς : state \. S12T\(ς\) ⇒ S15\(ς\[❝main::1::b❞:=0\]\)$
+^\(\d+\) ∀ ς : state \. S14\(ς\) ⇒ S16in\(ς\)$
+^\(\d+\) ∀ ς : state \. S15\(ς\) ⇒ S16in\(ς\)$
+^\(\d+\) S16 = S16in$
 ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
 ^\[main\.assertion\.2\] line \d+ property 2: REFUTED$
 --
diff --git a/regression/cprover/float/basic-float1.desc b/regression/cprover/float/basic-float1.desc
index f166c3d1380..e9d78c81ddc 100644
--- a/regression/cprover/float/basic-float1.desc
+++ b/regression/cprover/float/basic-float1.desc
@@ -3,7 +3,7 @@ basic-float1.c
 --text --solve --inline
 ^EXIT=0$
 ^SIGNAL=0$
-^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝main::1::f❞:=floatbv_typecast\(1, floatbv\[32\], ς\(❝__CPROVER_rounding_mode❞\)\)\]\)$
-^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ ieee_float_equal\(floatbv_plus\(ς\(❝main::1::f❞\), 0\.5, ς\(❝__CPROVER_rounding_mode❞\)\), 1\.5\)$
+^\(\d+\) ∀ ς : state \. S10\(ς\) ⇒ S11\(ς\[❝main::1::f❞:=floatbv_typecast\(1, floatbv\[32\], ς\(❝__CPROVER_rounding_mode❞\)\)\]\)$
+^\(\d+\) ∀ ς : state \. S11\(ς\) ⇒ ieee_float_equal\(floatbv_plus\(ς\(❝main::1::f❞\), 0\.5, ς\(❝__CPROVER_rounding_mode❞\)\), 1\.5\)$
 ^\[main\.assertion\.1\] line \d+ addition: SUCCESS$
 --
diff --git a/regression/cprover/function_calls/call_no_body1.desc b/regression/cprover/function_calls/call_no_body1.desc
index fe1c8685695..dc99c1876ad 100644
--- a/regression/cprover/function_calls/call_no_body1.desc
+++ b/regression/cprover/function_calls/call_no_body1.desc
@@ -4,6 +4,6 @@ call_no_body1.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^\*\*\*\* WARNING: no body for function function_without_body$
-^\(\d+\) ∀ ς : state, nondet::S28\.2-0 : signedbv\[32\] \. S28\.1\(ς\) ⇒ S28\.2\(ς\[❝main::\$tmp::return_value_function_without_body❞:=nondet::S28\.2-0\]\)$
-^\(\d+\) ∀ ς : state \. S28\.2\(ς\) ⇒ S28\.3\(ς\[❝main::1::x❞:=ς\(❝main::\$tmp::return_value_function_without_body❞\)\]\)$
+^\(\d+\) ∀ ς : state, nondet::S18\.2-0 : signedbv\[32\] \. S18\.1\(ς\) ⇒ S18\.2\(ς\[❝main::\$tmp::return_value_function_without_body❞:=nondet::S18\.2-0\]\)$
+^\(\d+\) ∀ ς : state \. S18\.2\(ς\) ⇒ S18\.3\(ς\[❝main::1::x❞:=ς\(❝main::\$tmp::return_value_function_without_body❞\)\]\)$
 --
diff --git a/regression/cprover/function_calls/call_no_body2.desc b/regression/cprover/function_calls/call_no_body2.desc
index 05093778b48..9615edec2f8 100644
--- a/regression/cprover/function_calls/call_no_body2.desc
+++ b/regression/cprover/function_calls/call_no_body2.desc
@@ -3,5 +3,5 @@ call_no_body2.c
 --text
 ^EXIT=0$
 ^SIGNAL=0$
-^\(\d+\) ∀ ς : state, nondet::S28\.2-0 : signedbv\[32\] \. S28\.1\(ς\) ⇒ S28\.2\(ς\[❝main::\$tmp::return_value_function_without_body❞\.❝x❞:=nondet::S28\.2-0\]\)$
+^\(\d+\) ∀ ς : state, nondet::S18\.2-0 : signedbv\[32\] \. S18\.1\(ς\) ⇒ S18\.2\(ς\[❝main::\$tmp::return_value_function_without_body❞\.❝x❞:=nondet::S18\.2-0\]\)$
 --
diff --git a/regression/cprover/loops/do_while1.desc b/regression/cprover/loops/do_while1.desc
index fa38eb3a586..a9c0d5d99e8 100644
--- a/regression/cprover/loops/do_while1.desc
+++ b/regression/cprover/loops/do_while1.desc
@@ -3,12 +3,12 @@ do_while1.c
 --text --solve --inline
 ^EXIT=0$
 ^SIGNAL=0$
-^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝x❞:=10\]\)$
-^\(\d+\) ∀ ς : state \. S23T\(ς\) ⇒ S22in\(ς\)$
-^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22in\(ς\)$
-^\(\d+\) ∀ ς : state \. S22in\(ς\) ⇒ S22\(ς\[❝x❞:=20\]\)$
-^\(\d+\) ∀ ς : state . \(S22\(ς\) ∧ ς\(❝x❞\) ≠ 20\) ⇒ S23T\(ς\)$
-^\(\d+\) ∀ ς : state . \(S22\(ς\) ∧ ¬\(ς\(❝x❞\) ≠ 20\)\) ⇒ S23\(ς\)$
+^\(\d+\) ∀ ς : state \. S10\(ς\) ⇒ S11\(ς\[❝x❞:=10\]\)$
+^\(\d+\) ∀ ς : state \. S13T\(ς\) ⇒ S12in\(ς\)$
+^\(\d+\) ∀ ς : state \. S11\(ς\) ⇒ S12in\(ς\)$
+^\(\d+\) ∀ ς : state \. S12in\(ς\) ⇒ S12\(ς\[❝x❞:=20\]\)$
+^\(\d+\) ∀ ς : state . \(S12\(ς\) ∧ ς\(❝x❞\) ≠ 20\) ⇒ S13T\(ς\)$
+^\(\d+\) ∀ ς : state . \(S12\(ς\) ∧ ¬\(ς\(❝x❞\) ≠ 20\)\) ⇒ S13\(ς\)$
 ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
 --
 --
diff --git a/regression/cprover/loops/for1.desc b/regression/cprover/loops/for1.desc
index c9e443cfc46..4fbec274ddd 100644
--- a/regression/cprover/loops/for1.desc
+++ b/regression/cprover/loops/for1.desc
@@ -3,14 +3,14 @@ for1.c
 --text --solve --inline
 ^EXIT=0$
 ^SIGNAL=0$
-^\(\d+\) ∀ ς : state \. S25\(ς\) ⇒ S22in\(ς\)$
-^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22in\(ς\)$
-^\(\d+\) ∀ ς : state \. \(S22in\(ς\) ∧ ¬\(ς\(❝main::1::i❞\) < 10\)\) ⇒ S22T\(ς\)$
-^\(\d+\) ∀ ς : state \. \(S22in\(ς\) ∧ ς\(❝main::1::i❞\) < 10\) ⇒ S22\(ς\)$
-^\(\d+\) S23 = S22$
-^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ S24\(ς\[❝main::1::i❞:=ς\(❝main::1::i❞\) \+ 1\]\)$
-^\(\d+\) S25 = S24$
-^\(\d+\) S26 = S22T$
+^\(\d+\) ∀ ς : state \. S15\(ς\) ⇒ S12in\(ς\)$
+^\(\d+\) ∀ ς : state \. S11\(ς\) ⇒ S12in\(ς\)$
+^\(\d+\) ∀ ς : state \. \(S12in\(ς\) ∧ ¬\(ς\(❝main::1::i❞\) < 10\)\) ⇒ S12T\(ς\)$
+^\(\d+\) ∀ ς : state \. \(S12in\(ς\) ∧ ς\(❝main::1::i❞\) < 10\) ⇒ S12\(ς\)$
+^\(\d+\) S13 = S12$
+^\(\d+\) ∀ ς : state \. S13\(ς\) ⇒ S14\(ς\[❝main::1::i❞:=ς\(❝main::1::i❞\) \+ 1\]\)$
+^\(\d+\) S15 = S14$
+^\(\d+\) S16 = S12T$
 ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
 --
 --
diff --git a/regression/cprover/loops/for2.desc b/regression/cprover/loops/for2.desc
index 8b0f17e74ff..12e48bd31b7 100644
--- a/regression/cprover/loops/for2.desc
+++ b/regression/cprover/loops/for2.desc
@@ -3,12 +3,12 @@ for2.c
 --text --solve --unwind 10 --inline
 ^EXIT=10$
 ^SIGNAL=0$
-^\(\d+\) ∀ ς : state \. S25\(ς\) ⇒ S22in\(ς\)$
-^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22in\(ς\)$
-^\(\d+\) ∀ ς : state \. \(S22in\(ς\) ∧ ¬\(ς\(❝main::1::1::x❞\) ≠ 10\)\) ⇒ S22T\(ς\)$
-^\(\d+\) ∀ ς : state \. \(S22in\(ς\) ∧ ς\(❝main::1::1::x❞\) ≠ 10\) ⇒ S22\(ς\)$
-^\(\d+\) S23 = S22$
-^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ S24\(ς\[❝main::1::1::x❞:=ς\(❝main::1::1::x❞\) \+ 1\]\)$
+^\(\d+\) ∀ ς : state \. S15\(ς\) ⇒ S12in\(ς\)$
+^\(\d+\) ∀ ς : state \. S11\(ς\) ⇒ S12in\(ς\)$
+^\(\d+\) ∀ ς : state \. \(S12in\(ς\) ∧ ¬\(ς\(❝main::1::1::x❞\) ≠ 10\)\) ⇒ S12T\(ς\)$
+^\(\d+\) ∀ ς : state \. \(S12in\(ς\) ∧ ς\(❝main::1::1::x❞\) ≠ 10\) ⇒ S12\(ς\)$
+^\(\d+\) S13 = S12$
+^\(\d+\) ∀ ς : state \. S13\(ς\) ⇒ S14\(ς\[❝main::1::1::x❞:=ς\(❝main::1::1::x❞\) \+ 1\]\)$
 ^\[main\.assertion\.1\] line \d+ property 1: REFUTED$
 --
 --
diff --git a/regression/cprover/loops/while-break1.desc b/regression/cprover/loops/while-break1.desc
index 6b8f4c5c8de..1f65f79fdb4 100644
--- a/regression/cprover/loops/while-break1.desc
+++ b/regression/cprover/loops/while-break1.desc
@@ -3,15 +3,15 @@ while-break1.c
 --text --solve --inline
 ^EXIT=0$
 ^SIGNAL=0$
-^\(\d+\) ∀ ς : state \. S28\(ς\) ⇒ S22in\(ς\)$
-^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22in\(ς\)$
-^\(\d+\) ∀ ς : state \. \(S22in\(ς\) ∧ ¬\(1 ≠ 0\)\) ⇒ S22T\(ς\)$
-^\(\d+\) ∀ ς : state \. \(S22in\(ς\) ∧ 1 ≠ 0\) ⇒ S22\(ς\)$
-^\(\d+\) ∀ ς : state \. \(S22\(ς\) ∧ ¬\(ς\(❝main::1::x❞\) = 0\)\) ⇒ S23T\(ς\)$
-^\(\d+\) ∀ ς : state \. \(S22\(ς\) ∧ ς\(❝main::1::x❞\) = 0\) ⇒ S23\(ς\)$
-^\(\d+\) ∀ ς : state \. S22T\(ς\) ⇒ S29in\(ς\)$
-^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ S29in\(ς\)$
-^\(\d+\) ∀ ς : state \. S26\(ς\) ⇒ S29in\(ς\)$
+^\(\d+\) ∀ ς : state \. S18\(ς\) ⇒ S12in\(ς\)$
+^\(\d+\) ∀ ς : state \. S11\(ς\) ⇒ S12in\(ς\)$
+^\(\d+\) ∀ ς : state \. \(S12in\(ς\) ∧ ¬\(1 ≠ 0\)\) ⇒ S12T\(ς\)$
+^\(\d+\) ∀ ς : state \. \(S12in\(ς\) ∧ 1 ≠ 0\) ⇒ S12\(ς\)$
+^\(\d+\) ∀ ς : state \. \(S12\(ς\) ∧ ¬\(ς\(❝main::1::x❞\) = 0\)\) ⇒ S13T\(ς\)$
+^\(\d+\) ∀ ς : state \. \(S12\(ς\) ∧ ς\(❝main::1::x❞\) = 0\) ⇒ S13\(ς\)$
+^\(\d+\) ∀ ς : state \. S12T\(ς\) ⇒ S19in\(ς\)$
+^\(\d+\) ∀ ς : state \. S14\(ς\) ⇒ S19in\(ς\)$
+^\(\d+\) ∀ ς : state \. S16\(ς\) ⇒ S19in\(ς\)$
 ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
 --
 --
diff --git a/regression/cprover/pointers/malloc1.desc b/regression/cprover/pointers/malloc1.desc
index 775ddcbbaf9..b592ec6376d 100644
--- a/regression/cprover/pointers/malloc1.desc
+++ b/regression/cprover/pointers/malloc1.desc
@@ -3,6 +3,6 @@ malloc1.c
 --text --solve --inline
 ^EXIT=0$
 ^SIGNAL=0$
-^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝main::\$tmp::return_value_malloc❞:=allocate\(ς, 4 \* cast\(10, unsignedbv\[64\]\)\)\]\)$
+^\(\d+\) ∀ ς : state \. S11\(ς\) ⇒ S12\(ς\[❝main::\$tmp::return_value_malloc❞:=allocate\(ς, 4 \* cast\(10, unsignedbv\[64\]\)\)\]\)$
 ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
 --
diff --git a/regression/cprover/pointers/pointers0.desc b/regression/cprover/pointers/pointers0.desc
index 9ce4f642078..71485440798 100644
--- a/regression/cprover/pointers/pointers0.desc
+++ b/regression/cprover/pointers/pointers0.desc
@@ -3,7 +3,7 @@ pointers0.c
 --text --solve --inline --no-safety
 ^EXIT=0$
 ^SIGNAL=0$
-^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝main::1::p❞:=❝main::1::x❞\]\)$
-^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(ς\(❝main::1::p❞\)\) = ς\(❝main::1::x❞\)\)$
+^\(\d+\) ∀ ς : state \. S11\(ς\) ⇒ S12\(ς\[❝main::1::p❞:=❝main::1::x❞\]\)$
+^\(\d+\) ∀ ς : state \. S12\(ς\) ⇒ \(ς\(ς\(❝main::1::p❞\)\) = ς\(❝main::1::x❞\)\)$
 ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
 --
diff --git a/regression/cprover/pointers/pointers1.desc b/regression/cprover/pointers/pointers1.desc
index 46ccbfe4633..fd69542b9f5 100644
--- a/regression/cprover/pointers/pointers1.desc
+++ b/regression/cprover/pointers/pointers1.desc
@@ -3,9 +3,9 @@ pointers1.c
 --text --solve --inline --no-safety
 ^EXIT=0$
 ^SIGNAL=0$
-^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝x❞:=10\]\)$
-^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ S24\(ς\[❝p❞:=❝x❞\]\)$
-^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ S25\(ς\[❝y❞:=ς\(ς\(❝p❞\)\)\]\)$
-^\(\d+\) ∀ ς : state \. S25\(ς\) ⇒ \(ς\(❝y❞\) = 10\)$
+^\(\d+\) ∀ ς : state \. S12\(ς\) ⇒ S13\(ς\[❝x❞:=10\]\)$
+^\(\d+\) ∀ ς : state \. S13\(ς\) ⇒ S14\(ς\[❝p❞:=❝x❞\]\)$
+^\(\d+\) ∀ ς : state \. S14\(ς\) ⇒ S15\(ς\[❝y❞:=ς\(ς\(❝p❞\)\)\]\)$
+^\(\d+\) ∀ ς : state \. S15\(ς\) ⇒ \(ς\(❝y❞\) = 10\)$
 ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
 --
diff --git a/regression/cprover/pointers/pointers2.desc b/regression/cprover/pointers/pointers2.desc
index b39c93b79b2..94398531679 100644
--- a/regression/cprover/pointers/pointers2.desc
+++ b/regression/cprover/pointers/pointers2.desc
@@ -3,12 +3,12 @@ pointers2.c
 --text --solve --inline --no-safety
 ^EXIT=10$
 ^SIGNAL=0$
-^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝x❞:=10\]\)$
-^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝p❞:=❝x❞\]\)$
-^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ S24\(ς\[ς\(❝p❞\):=20\]\)$
-^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ \(ς\(❝x❞\) = 20\)$
-^\(\d+\) S25 = S24$
-^\(\d+\) ∀ ς : state \. S25\(ς\) ⇒ \(ς\(❝x❞\) = 10\)$
+^\(\d+\) ∀ ς : state \. S11\(ς\) ⇒ S12\(ς\[❝x❞:=10\]\)$
+^\(\d+\) ∀ ς : state \. S12\(ς\) ⇒ S13\(ς\[❝p❞:=❝x❞\]\)$
+^\(\d+\) ∀ ς : state \. S13\(ς\) ⇒ S14\(ς\[ς\(❝p❞\):=20\]\)$
+^\(\d+\) ∀ ς : state \. S14\(ς\) ⇒ \(ς\(❝x❞\) = 20\)$
+^\(\d+\) S15 = S14$
+^\(\d+\) ∀ ς : state \. S15\(ς\) ⇒ \(ς\(❝x❞\) = 10\)$
 ^\[main\.assertion\.1] line \d+ property 1: SUCCESS$
 ^\[main\.assertion\.2] line \d+ property 2: REFUTED$
 --
diff --git a/regression/cprover/pointers/pointers3.desc b/regression/cprover/pointers/pointers3.desc
index b8b51405977..2ba664b3702 100644
--- a/regression/cprover/pointers/pointers3.desc
+++ b/regression/cprover/pointers/pointers3.desc
@@ -3,7 +3,7 @@ pointers3.c
 --text --solve --inline --no-safety
 ^EXIT=0$
 ^SIGNAL=0$
-^\(\d+\) ∀ ς : state \. \(S20\(ς\) ∧ ς\(ς\(❝main::1::p❞\)\) = 10\) ⇒ S21\(ς\)$
-^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ \(ς\(ς\(❝main::1::p❞\)\) = 10\)$
+^\(\d+\) ∀ ς : state \. \(S10\(ς\) ∧ ς\(ς\(❝main::1::p❞\)\) = 10\) ⇒ S11\(ς\)$
+^\(\d+\) ∀ ς : state \. S11\(ς\) ⇒ \(ς\(ς\(❝main::1::p❞\)\) = 10\)$
 ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
 --
diff --git a/regression/cprover/pointers/pointers4.desc b/regression/cprover/pointers/pointers4.desc
index 1569fe88769..72cfaa2cff2 100644
--- a/regression/cprover/pointers/pointers4.desc
+++ b/regression/cprover/pointers/pointers4.desc
@@ -3,9 +3,9 @@ pointers4.c
 --text --solve --inline --no-safety
 ^EXIT=10$
 ^SIGNAL=0$
-^\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[❝x❞:=0\]\)$
-^\(\d+\) ∀ ς : state \. \(S21\(ς\) ∧ ς\(ς\(❝main::1::p❞\)\) = 10\) ⇒ S22\(ς\)$
-^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝main::1::p❞:=❝x❞\]\)$
-^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ \(ς\(ς\(❝main::1::p❞\)\) = 10\)$
+^\(\d+\) ∀ ς : state \. S7\(ς\) ⇒ S8\(ς\[❝x❞:=0\]\)$
+^\(\d+\) ∀ ς : state \. \(S11\(ς\) ∧ ς\(ς\(❝main::1::p❞\)\) = 10\) ⇒ S12\(ς\)$
+^\(\d+\) ∀ ς : state \. S12\(ς\) ⇒ S13\(ς\[❝main::1::p❞:=❝x❞\]\)$
+^\(\d+\) ∀ ς : state \. S13\(ς\) ⇒ \(ς\(ς\(❝main::1::p❞\)\) = 10\)$
 ^\[main\.assertion\.1\] line \d+ property 1: REFUTED$
 --
diff --git a/regression/cprover/pointers/pointers5.desc b/regression/cprover/pointers/pointers5.desc
index 453b44b3ea6..128b13fe12d 100644
--- a/regression/cprover/pointers/pointers5.desc
+++ b/regression/cprover/pointers/pointers5.desc
@@ -3,7 +3,7 @@ pointers5.c
 --text --solve --inline --no-safety
 ^EXIT=0$
 ^SIGNAL=0$
-^\(\d+\) ∀ ς : state \. \(S22\(ς\) ∧ ς\(❝main::1::p❞\) = ς\(❝main::1::q❞\)\) ⇒ S23\(ς\)$
-^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ \(ς\(ς\(❝main::1::p❞\)\) = ς\(ς\(❝main::1::q❞\)\)\)$
+^\(\d+\) ∀ ς : state \. \(S12\(ς\) ∧ ς\(❝main::1::p❞\) = ς\(❝main::1::q❞\)\) ⇒ S13\(ς\)$
+^\(\d+\) ∀ ς : state \. S13\(ς\) ⇒ \(ς\(ς\(❝main::1::p❞\)\) = ς\(ς\(❝main::1::q❞\)\)\)$
 ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
 --
diff --git a/regression/cprover/pointers/pointers6.desc b/regression/cprover/pointers/pointers6.desc
index 35c1dff9a5b..36d9b6e4082 100644
--- a/regression/cprover/pointers/pointers6.desc
+++ b/regression/cprover/pointers/pointers6.desc
@@ -3,9 +3,9 @@ pointers6.c
 --text --solve --inline --no-safety
 ^EXIT=0$
 ^SIGNAL=0$
-^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝main::1::p❞:=❝x❞\]\)$
-^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ S24\(ς\[ς\(❝main::1::p❞\):=10\]\)$
-^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ S25\(ς\[❝main::1::q❞:=❝x❞\]\)$
-^\(\d+\) ∀ ς : state \. S25\(ς\) ⇒ \(ς\(ς\(❝main::1::q❞\)\) = 10\)$
+^\(\d+\) ∀ ς : state \. S12\(ς\) ⇒ S13\(ς\[❝main::1::p❞:=❝x❞\]\)$
+^\(\d+\) ∀ ς : state \. S13\(ς\) ⇒ S14\(ς\[ς\(❝main::1::p❞\):=10\]\)$
+^\(\d+\) ∀ ς : state \. S14\(ς\) ⇒ S15\(ς\[❝main::1::q❞:=❝x❞\]\)$
+^\(\d+\) ∀ ς : state \. S15\(ς\) ⇒ \(ς\(ς\(❝main::1::q❞\)\) = 10\)$
 ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
 --
diff --git a/regression/cprover/pointers/pointers7.desc b/regression/cprover/pointers/pointers7.desc
index 6f18eb76bfb..540d64f133b 100644
--- a/regression/cprover/pointers/pointers7.desc
+++ b/regression/cprover/pointers/pointers7.desc
@@ -3,14 +3,14 @@ pointers7.c
 --text --solve --inline --no-safety
 ^EXIT=0$
 ^SIGNAL=0$
-^\(\d+\) ∀ ς : state \. S17\(ς\) ⇒ S18\(ς\[❝p❞:=NULL\]\)$
-^\(\d+\) ∀ ς : state \. S18\(ς\) ⇒ S19\(ς\[❝x❞:=0\]\)$
-^\(\d+\) ∀ ς : state \. S19\(ς\) ⇒ S20\(ς\[❝y❞:=0\]\)$
-^\(\d+\) S21 = S20$
-^\(\d+\) S22 = S21$
-^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝x❞:=10\]\)$
-^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ S24\(ς\[❝p❞:=❝y❞\]\)$
-^\(\d+\) ∀ ς : state \. S24\(ς\) ⇒ S25\(ς\[ς\(❝p❞\):=20\]\)$
-^\(\d+\) ∀ ς : state \. S25\(ς\) ⇒ \(ς\(❝x❞\) = 10\)$
+^\(\d+\) ∀ ς : state \. S7\(ς\) ⇒ S8\(ς\[❝p❞:=NULL\]\)$
+^\(\d+\) ∀ ς : state \. S8\(ς\) ⇒ S9\(ς\[❝x❞:=0\]\)$
+^\(\d+\) ∀ ς : state \. S9\(ς\) ⇒ S10\(ς\[❝y❞:=0\]\)$
+^\(\d+\) S11 = S10$
+^\(\d+\) S12 = S11$
+^\(\d+\) ∀ ς : state \. S12\(ς\) ⇒ S13\(ς\[❝x❞:=10\]\)$
+^\(\d+\) ∀ ς : state \. S13\(ς\) ⇒ S14\(ς\[❝p❞:=❝y❞\]\)$
+^\(\d+\) ∀ ς : state \. S14\(ς\) ⇒ S15\(ς\[ς\(❝p❞\):=20\]\)$
+^\(\d+\) ∀ ς : state \. S15\(ς\) ⇒ \(ς\(❝x❞\) = 10\)$
 ^\[main\.assertion\.1\] line \d property 1: SUCCESS$
 --
diff --git a/regression/cprover/pointers/pointers8.desc b/regression/cprover/pointers/pointers8.desc
index c56a19d3e73..13588c91baa 100644
--- a/regression/cprover/pointers/pointers8.desc
+++ b/regression/cprover/pointers/pointers8.desc
@@ -3,8 +3,8 @@ pointers8.c
 --text --solve --inline --no-safety
 ^EXIT=0$
 ^SIGNAL=0$
-^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[ς\(❝main::1::p❞\):=123\]\)$
-^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝main::1::p_value❞:=ς\(ς\(❝main::1::p❞\)\)\]\)$
-^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ \(ς\(❝main::1::p_value❞\) = 123\)$
+^\(\d+\) ∀ ς : state \. S10\(ς\) ⇒ S11\(ς\[ς\(❝main::1::p❞\):=123\]\)$
+^\(\d+\) ∀ ς : state \. S12\(ς\) ⇒ S13\(ς\[❝main::1::p_value❞:=ς\(ς\(❝main::1::p❞\)\)\]\)$
+^\(\d+\) ∀ ς : state \. S13\(ς\) ⇒ \(ς\(❝main::1::p_value❞\) = 123\)$
 ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
 --
diff --git a/regression/cprover/pointers/pointers9.desc b/regression/cprover/pointers/pointers9.desc
index aa097d00389..54ee6653588 100644
--- a/regression/cprover/pointers/pointers9.desc
+++ b/regression/cprover/pointers/pointers9.desc
@@ -3,9 +3,9 @@ pointers9.c
 --text --solve --inline --no-safety
 ^EXIT=0$
 ^SIGNAL=0$
-^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝main::1::x❞:=123\]\)$
-^\(\d+\) ∀ ς : state \. \(S22\(ς\) ∧ ¬\(ς\(❝main::1::p❞\) = ❝main::1::x❞\)\) ⇒ S23T\(ς\)$
-^\(\d+\) ∀ ς : state \. \(S22\(ς\) ∧ ς\(❝main::1::p❞\) = ❝main::1::x❞\) ⇒ S23\(ς\)$
-^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ \(ς\(ς\(❝main::1::p❞\)\) = 123\)$
+^\(\d+\) ∀ ς : state \. S11\(ς\) ⇒ S12\(ς\[❝main::1::x❞:=123\]\)$
+^\(\d+\) ∀ ς : state \. \(S12\(ς\) ∧ ¬\(ς\(❝main::1::p❞\) = ❝main::1::x❞\)\) ⇒ S13T\(ς\)$
+^\(\d+\) ∀ ς : state \. \(S12\(ς\) ∧ ς\(❝main::1::p❞\) = ❝main::1::x❞\) ⇒ S13\(ς\)$
+^\(\d+\) ∀ ς : state \. S13\(ς\) ⇒ \(ς\(ς\(❝main::1::p❞\)\) = 123\)$
 ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
 --
diff --git a/regression/cprover/pointers/struct_pointer1.desc b/regression/cprover/pointers/struct_pointer1.desc
index 8582daf8386..f8d09cb004a 100644
--- a/regression/cprover/pointers/struct_pointer1.desc
+++ b/regression/cprover/pointers/struct_pointer1.desc
@@ -3,8 +3,8 @@ struct_pointer1.c
 --text --solve --inline --no-safety
 ^EXIT=0$
 ^SIGNAL=0$
-^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[ς\(❝main::1::my_struct_ptr❞\)\.❝data❞:=123\]\)$
-^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[❝main::1::my_struct_data❞:=ς\(ς\(❝main::1::my_struct_ptr❞\)\.❝data❞\)\]\)$
-^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ \(ς\(❝main::1::my_struct_data❞\) = 123\)$
+^\(\d+\) ∀ ς : state \. S10\(ς\) ⇒ S11\(ς\[ς\(❝main::1::my_struct_ptr❞\)\.❝data❞:=123\]\)$
+^\(\d+\) ∀ ς : state \. S12\(ς\) ⇒ S13\(ς\[❝main::1::my_struct_data❞:=ς\(ς\(❝main::1::my_struct_ptr❞\)\.❝data❞\)\]\)$
+^\(\d+\) ∀ ς : state \. S13\(ς\) ⇒ \(ς\(❝main::1::my_struct_data❞\) = 123\)$
 ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
 --
diff --git a/regression/cprover/pointers/struct_pointer2.desc b/regression/cprover/pointers/struct_pointer2.desc
index 620e0f42d4a..9e6b0d11273 100644
--- a/regression/cprover/pointers/struct_pointer2.desc
+++ b/regression/cprover/pointers/struct_pointer2.desc
@@ -3,8 +3,8 @@ struct_pointer2.c
 --text --solve --inline --no-safety
 ^EXIT=0$
 ^SIGNAL=0$
-^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝main::1::my_struct_ptr❞:=❝main::1::my_struct❞\]\)$
-^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ S23\(ς\[ς\(❝main::1::my_struct_ptr❞\)\.❝data❞:=123\]\)$
-^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ \(ς\(❝main::1::my_struct❞\.❝data❞\) = 123\)$
+^\(\d+\) ∀ ς : state \. S11\(ς\) ⇒ S12\(ς\[❝main::1::my_struct_ptr❞:=❝main::1::my_struct❞\]\)$
+^\(\d+\) ∀ ς : state \. S12\(ς\) ⇒ S13\(ς\[ς\(❝main::1::my_struct_ptr❞\)\.❝data❞:=123\]\)$
+^\(\d+\) ∀ ς : state \. S13\(ς\) ⇒ \(ς\(❝main::1::my_struct❞\.❝data❞\) = 123\)$
 ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
 --
diff --git a/regression/cprover/safety/use_after_free1.desc b/regression/cprover/safety/use_after_free1.desc
index 55f42a70080..a2f4b160356 100644
--- a/regression/cprover/safety/use_after_free1.desc
+++ b/regression/cprover/safety/use_after_free1.desc
@@ -3,6 +3,6 @@ use_after_free1.c
 --text --inline --no-safety
 ^EXIT=0$
 ^SIGNAL=0$
-^\(\d+\) ∀ ς : state . S21\(ς\) ⇒ S22\(ς\[❝main::\$tmp::return_value_malloc❞:=allocate\(ς, 4\)\]\)$
-^\(\d+\) ∀ ς : state . S25\(ς\) ⇒ S26\(deallocate_state\(ς, cast\(ς\(❝main::1::p❞\), empty\*\)\)\)$
+^\(\d+\) ∀ ς : state . S11\(ς\) ⇒ S12\(ς\[❝main::\$tmp::return_value_malloc❞:=allocate\(ς, 4\)\]\)$
+^\(\d+\) ∀ ς : state . S15\(ς\) ⇒ S16\(deallocate_state\(ς, cast\(ς\(❝main::1::p❞\), empty\*\)\)\)$
 --
diff --git a/regression/cprover/structs/nondet_struct1.desc b/regression/cprover/structs/nondet_struct1.desc
index e7c54f6c58e..a8fa2b39dc7 100644
--- a/regression/cprover/structs/nondet_struct1.desc
+++ b/regression/cprover/structs/nondet_struct1.desc
@@ -3,5 +3,5 @@ nondet_struct1.c
 --text --inline
 ^EXIT=0$
 ^SIGNAL=0$
-^\(\d+\) ∀ ς : state, nondet::S21-0 : signedbv\[32\], nondet::S21-1 : signedbv\[32\] \. S20\(ς\) ⇒ S21\(ς\[❝s❞\.❝x❞:=nondet::S21-0\]\[❝s❞\.❝y❞:=nondet::S21-1\]\)$
+^\(\d+\) ∀ ς : state, nondet::S11-0 : signedbv\[32\], nondet::S11-1 : signedbv\[32\] \. S10\(ς\) ⇒ S11\(ς\[❝s❞\.❝x❞:=nondet::S11-0\]\[❝s❞\.❝y❞:=nondet::S11-1\]\)$
 --
diff --git a/regression/cprover/structs/struct1.desc b/regression/cprover/structs/struct1.desc
index 0c58df9e6a3..042328e9bb5 100644
--- a/regression/cprover/structs/struct1.desc
+++ b/regression/cprover/structs/struct1.desc
@@ -3,7 +3,7 @@ struct1.c
 --text --solve --inline
 ^EXIT=0$
 ^SIGNAL=0$
-^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝s❞.❝x❞:=1\]\)$
-^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ \(ς\(❝s❞.❝x❞\) = 1\)$
+^\(\d+\) ∀ ς : state \. S10\(ς\) ⇒ S11\(ς\[❝s❞.❝x❞:=1\]\)$
+^\(\d+\) ∀ ς : state \. S11\(ς\) ⇒ \(ς\(❝s❞.❝x❞\) = 1\)$
 ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
 --
diff --git a/regression/cprover/structs/struct2.desc b/regression/cprover/structs/struct2.desc
index a260597c06e..a470f44c4e5 100644
--- a/regression/cprover/structs/struct2.desc
+++ b/regression/cprover/structs/struct2.desc
@@ -3,10 +3,10 @@ struct2.c
 --text --solve --inline
 ^EXIT=0$
 ^SIGNAL=0$
-^\(\d+\) ∀ ς : state \. S20\(ς\) ⇒ S21\(ς\[❝s❞.❝x❞:=1\]\)$
-^\(\d+\) ∀ ς : state \. S21\(ς\) ⇒ S22\(ς\[❝s❞.❝y❞:=2\]\)$
-^\(\d+\) ∀ ς : state \. S22\(ς\) ⇒ \(ς\(❝s❞.❝x❞\) = 1\)$
-^\(\d+\) ∀ ς : state \. S23\(ς\) ⇒ \(ς\(❝s❞.❝y❞\) = 2\)$
+^\(\d+\) ∀ ς : state \. S10\(ς\) ⇒ S11\(ς\[❝s❞.❝x❞:=1\]\)$
+^\(\d+\) ∀ ς : state \. S11\(ς\) ⇒ S12\(ς\[❝s❞.❝y❞:=2\]\)$
+^\(\d+\) ∀ ς : state \. S12\(ς\) ⇒ \(ς\(❝s❞.❝x❞\) = 1\)$
+^\(\d+\) ∀ ς : state \. S13\(ς\) ⇒ \(ς\(❝s❞.❝y❞\) = 2\)$
 ^\[main\.assertion\.1\] line \d+ property 1: SUCCESS$
 ^\[main\.assertion\.2\] line \d+ property 2: SUCCESS$
 --
diff --git a/regression/goto-analyzer/constant_propagation_01/test-vsd.desc b/regression/goto-analyzer/constant_propagation_01/test-vsd.desc
index 8eb05ff4f8d..741965ab2a5 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$
-^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 14, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 2, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 9, 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 47aea19e28b..e0147b4ce18 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$
-^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 14, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 2, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 9, 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 89bcfe85984..db447649547 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$
-^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 13, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 3, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 8, 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 0cc5f61bb73..f8465991235 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$
-^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 13, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 3, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 8, 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 89bcfe85984..db447649547 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$
-^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 13, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 3, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 8, 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 0cc5f61bb73..f8465991235 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$
-^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 13, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 3, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 8, 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 89bcfe85984..db447649547 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$
-^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 13, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 3, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 8, 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 0cc5f61bb73..f8465991235 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$
-^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 13, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 3, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 0, assigns: 8, 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 d4c16c2278f..14364a509af 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$
-^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 15, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 3, assigns: 4, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 10, 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 22058dcb77e..3b836b8dad2 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$
-^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 15, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 3, assigns: 4, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 10, 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 5ddf203f9b3..b478301d9ee 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: 1, assigns: 8, function calls: 0$
-^Unmodified:  assert: 0, assume: 0, goto: 2, assigns: 12, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 3, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 2, assigns: 7, 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 8d26811ac53..90e1b48f887 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$
-^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 11, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 3, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 6, 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 e63b5b8a837..bba19b94b66 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$
-^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 11, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 3, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 6, 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 bcc8b541c93..e8b6c2d034f 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$
-^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 12, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 2, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 7, 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 79fcdf4a79b..614698c7277 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$
-^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 12, function calls: 2$
+^Simplified:  assert: 1, assume: 0, goto: 1, assigns: 2, function calls: 0$
+^Unmodified:  assert: 0, assume: 0, goto: 1, assigns: 7, function calls: 2$
 --
 ^warning: ignoring
diff --git a/regression/goto-analyzer/liveness-function-call/test-liveness-show.desc b/regression/goto-analyzer/liveness-function-call/test-liveness-show.desc
index 2a8b2b0aa11..c1501370247 100644
--- a/regression/goto-analyzer/liveness-function-call/test-liveness-show.desc
+++ b/regression/goto-analyzer/liveness-function-call/test-liveness-show.desc
@@ -3,8 +3,8 @@ main.c
 --variable-sensitivity --vsd-liveness --show
 ^EXIT=0$
 ^SIGNAL=0$
-globalX .* 0 @ \[25\]
+globalX .* 0 @ \[15\]
 globalX .* 1 @ \[0\]
 globalX .* 2 @ \[3\]
-globalX .* TOP @ \[28\]
+globalX .* TOP @ \[18\]
 --
diff --git a/regression/goto-analyzer/liveness-function-call/test-liveness-three-way-show.desc b/regression/goto-analyzer/liveness-function-call/test-liveness-three-way-show.desc
index dd242a3a3e6..2c13d44ae4b 100644
--- a/regression/goto-analyzer/liveness-function-call/test-liveness-three-way-show.desc
+++ b/regression/goto-analyzer/liveness-function-call/test-liveness-three-way-show.desc
@@ -3,8 +3,8 @@ main.c
 --variable-sensitivity --vsd-liveness --three-way-merge --show
 ^EXIT=0$
 ^SIGNAL=0$
-globalX .* 0 @ \[25\]
+globalX .* 0 @ \[15\]
 globalX .* 1 @ \[0\]
 globalX .* 2 @ \[3\]
-globalX .* TOP @ \[28\]
+globalX .* TOP @ \[18\]
 --
diff --git a/regression/goto-analyzer/liveness-function-call/test-write-location-show.desc b/regression/goto-analyzer/liveness-function-call/test-write-location-show.desc
index 8de3a82a5ef..f3fd23e0665 100644
--- a/regression/goto-analyzer/liveness-function-call/test-write-location-show.desc
+++ b/regression/goto-analyzer/liveness-function-call/test-write-location-show.desc
@@ -3,7 +3,7 @@ main.c
 --variable-sensitivity --show
 ^EXIT=0$
 ^SIGNAL=0$
-globalX .* 0 @ \[25\]
+globalX .* 0 @ \[15\]
 globalX .* 1 @ \[0\]
 globalX .* TOP @ \[0, 3\]
 --
diff --git a/regression/goto-analyzer/liveness-function-call/test-write-location-three-way-show.desc b/regression/goto-analyzer/liveness-function-call/test-write-location-three-way-show.desc
index c8daf2ef143..242a87dda34 100644
--- a/regression/goto-analyzer/liveness-function-call/test-write-location-three-way-show.desc
+++ b/regression/goto-analyzer/liveness-function-call/test-write-location-three-way-show.desc
@@ -3,7 +3,7 @@ main.c
 --variable-sensitivity --three-way-merge --show
 ^EXIT=0$
 ^SIGNAL=0$
-globalX .* 0 @ \[25\]
+globalX .* 0 @ \[15\]
 globalX .* 1 @ \[0\]
 globalX .* 2 @ \[3\]
 --
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 92cff667e02..19398dce8fb 100644
--- a/regression/goto-analyzer/sensitivity-last-written-locations-arrays/test.desc
+++ b/regression/goto-analyzer/sensitivity-last-written-locations-arrays/test.desc
@@ -6,32 +6,26 @@ activate-multi-line-match
 ^EXIT=0$
 ^SIGNAL=0$
 main#return_value \(\) -> TOP @ \[1\]
-__CPROVER_dead_object \(\) -> TOP @ \[5\]
-__CPROVER_deallocated \(\) -> TOP @ \[6\]
-__CPROVER_malloc_is_new_array \(\) -> FALSE @ \[7\]
-__CPROVER_memory_leak \(\) -> TOP @ \[9\]
-__CPROVER_new_object \(\) -> TOP @ \[10\]
-__CPROVER_next_thread_key \(\) -> 0ul @ \[12\]
-__CPROVER_pipe_count \(\) -> 0u @ \[13\]
-__CPROVER_rounding_mode \(\) -> 0 @ \[14\]
-__CPROVER_thread_id \(\) -> 0ul @ \[15\]
-__CPROVER_threads_exited \(\) -> TOP @ \[18\]
-do_arrays::1::bool_ \(\) -> TOP @ \[20\]
-do_arrays::1::bool_1 \(\) -> TOP @ \[21\]
-do_arrays::1::bool_2 \(\) -> TOP @ \[22\]
-do_arrays::1::x \(\) -> \{\[0\] = 10 @ \[24\]\n\} @ \[24\]
-do_arrays::1::x \(\) -> \{\[0\] = 10 @ \[24\]\n\[1\] = 20 @ \[25\]\n\} @ \[25\]
-do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[26\]\n\[1\] = 20 @ \[25\]\n\} @ \[26\]
-do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[26\]\n\[1\] = 40 @ \[27\]\n\} @ \[27\]
-do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[26\]\n\[1\] = 30 @ \[28\]\n\} @ \[28\]
-do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[29\]\n\[1\] = 30 @ \[28\]\n\} @ \[29\]
-do_arrays::1::x \(\) -> \{\[0\] = 5 @ \[30\]\n\[1\] = 30 @ \[28\]\n\} @ \[30\]
-do_arrays::1::x \(\) -> \{\[0\] = 15 @ \[31\]\n\[1\] = 30 @ \[28\]\n\} @ \[31\]
-do_arrays::1::x \(\) -> \{\[0\] = 15 @ \[31\]\n\[1\] = 10 @ \[32\]\n\} @ \[32\]
-do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[34\]\n\[1\] = 10 @ \[32\]\n\} @ \[34\]
-do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[34\, 36\]\n\[1\] = 10 @ \[32\]\n\} @ \[34\, 36\]
-do_arrays::1::x \(\) -> \{\[0\] = 0 @ \[38]\n\[1\] = 10 @ \[32\]\n\} @ \[38\]
-do_arrays::1::x \(\) -> \{\[0\] = 3 @ \[40]\n\[1\] = 10 @ \[32\]\n\} @ \[40\]
-do_arrays::1::x \(\) -> \{\[0\] = TOP @ \[40\, 42]\n\[1\] = 10 @ \[32\]\n\} @ \[40\, 42\]
-do_arrays::1::x \(\) -> \{\[0\] = TOP @ \[40\, 42\, 45]\n\[1\] = 10 @ \[47\]\n\} @ \[47\]
-do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[48]\n\[1\] = 10 @ \[47\]\n\} @ \[48\]
+__CPROVER_dead_object \(\) -> TOP @ \[4\]
+__CPROVER_deallocated \(\) -> TOP @ \[5\]
+__CPROVER_memory_leak \(\) -> TOP @ \[7\]
+__CPROVER_rounding_mode \(\) -> 0 @ \[8\]
+do_arrays::1::bool_ \(\) -> TOP @ \[10\]
+do_arrays::1::bool_1 \(\) -> TOP @ \[11\]
+do_arrays::1::bool_2 \(\) -> TOP @ \[12\]
+do_arrays::1::x \(\) -> \{\[0\] = 10 @ \[14\]\n\} @ \[14\]
+do_arrays::1::x \(\) -> \{\[0\] = 10 @ \[14\]\n\[1\] = 20 @ \[15\]\n\} @ \[15\]
+do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[16\]\n\[1\] = 20 @ \[15\]\n\} @ \[16\]
+do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[16\]\n\[1\] = 40 @ \[17\]\n\} @ \[17\]
+do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[16\]\n\[1\] = 30 @ \[18\]\n\} @ \[18\]
+do_arrays::1::x \(\) -> \{\[0\] = 30 @ \[19\]\n\[1\] = 30 @ \[18\]\n\} @ \[19\]
+do_arrays::1::x \(\) -> \{\[0\] = 5 @ \[20\]\n\[1\] = 30 @ \[18\]\n\} @ \[20\]
+do_arrays::1::x \(\) -> \{\[0\] = 15 @ \[21\]\n\[1\] = 30 @ \[18\]\n\} @ \[21\]
+do_arrays::1::x \(\) -> \{\[0\] = 15 @ \[21\]\n\[1\] = 10 @ \[22\]\n\} @ \[22\]
+do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[24\]\n\[1\] = 10 @ \[22\]\n\} @ \[24\]
+do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[24\, 26\]\n\[1\] = 10 @ \[22\]\n\} @ \[24\, 26\]
+do_arrays::1::x \(\) -> \{\[0\] = 0 @ \[28]\n\[1\] = 10 @ \[22\]\n\} @ \[28\]
+do_arrays::1::x \(\) -> \{\[0\] = 3 @ \[30]\n\[1\] = 10 @ \[22\]\n\} @ \[30\]
+do_arrays::1::x \(\) -> \{\[0\] = TOP @ \[30\, 32]\n\[1\] = 10 @ \[22\]\n\} @ \[30\, 32\]
+do_arrays::1::x \(\) -> \{\[0\] = TOP @ \[30\, 32\, 35]\n\[1\] = 10 @ \[37\]\n\} @ \[37\]
+do_arrays::1::x \(\) -> \{\[0\] = 20 @ \[38]\n\[1\] = 10 @ \[37\]\n\} @ \[38\]
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 bf14f6154f4..94a6ad7e383 100644
--- a/regression/goto-analyzer/sensitivity-last-written-locations-pointers/test.desc
+++ b/regression/goto-analyzer/sensitivity-last-written-locations-pointers/test.desc
@@ -6,31 +6,25 @@ activate-multi-line-match
 ^EXIT=0$
 ^SIGNAL=0$
 main#return_value \(\) -> TOP @ \[1\]
-__CPROVER_dead_object \(\) -> TOP @ \[5\]
-__CPROVER_deallocated \(\) -> TOP @ \[6\]
-__CPROVER_malloc_is_new_array \(\) -> FALSE @ \[7\]
-__CPROVER_memory_leak \(\) -> TOP @ \[9\]
-__CPROVER_new_object \(\) -> TOP @ \[10\]
-__CPROVER_next_thread_key \(\) -> 0ul @ \[12\]
-__CPROVER_pipe_count \(\) -> 0u @ \[13\]
-__CPROVER_rounding_mode \(\) -> 0 @ \[14\]
-__CPROVER_thread_id \(\) -> 0ul @ \[15\]
-__CPROVER_threads_exited \(\) -> TOP @ \[18\]
-do_pointers::1::bool_ \(\) -> TOP @ \[20\]
-do_pointers::1::bool_1 \(\) -> TOP @ \[21\]
-do_pointers::1::bool_2 \(\) -> TOP @ \[22\]
-do_pointers::1::x \(\) -> TOP @ \[23\]
-do_pointers::1::x \(\) -> 10 @ \[24\]
-do_pointers::1::x_p \(\) -> TOP @ \[25\]
-do_pointers::1::y \(\) -> TOP @ \[26\]
-do_pointers::1::y \(\) -> 20 @ \[27\]
-do_pointers::1::y_p \(\) -> TOP @ \[28\]
-do_pointers::1::x_p \(\) -> ptr ->\(do_pointers::1::x\) @ \[29\]
-do_pointers::1::x \(\) -> 30 @ \[30\]
-do_pointers::1::x \(\) -> 40 @ \[31\]
-do_pointers::1::x \(\) -> TOP @ \[32\]
-do_pointers::1::x \(\) -> 50 @ \[33\]
-do_pointers::1::y_p \(\) -> ptr ->\(do_pointers::1::x\) @ \[34\]
-do_pointers::1::x \(\) -> 60 @ \[35\]
-do_pointers::1::j \(\) -> TOP @ \[36\]
-do_pointers::1::j \(\) -> 60 @ \[37\]
+__CPROVER_dead_object \(\) -> TOP @ \[4\]
+__CPROVER_deallocated \(\) -> TOP @ \[5\]
+__CPROVER_memory_leak \(\) -> TOP @ \[7\]
+__CPROVER_rounding_mode \(\) -> 0 @ \[8\]
+do_pointers::1::bool_ \(\) -> TOP @ \[10\]
+do_pointers::1::bool_1 \(\) -> TOP @ \[11\]
+do_pointers::1::bool_2 \(\) -> TOP @ \[12\]
+do_pointers::1::x \(\) -> TOP @ \[13\]
+do_pointers::1::x \(\) -> 10 @ \[14\]
+do_pointers::1::x_p \(\) -> TOP @ \[15\]
+do_pointers::1::y \(\) -> TOP @ \[16\]
+do_pointers::1::y \(\) -> 20 @ \[17\]
+do_pointers::1::y_p \(\) -> TOP @ \[18\]
+do_pointers::1::x_p \(\) -> ptr ->\(do_pointers::1::x\) @ \[19\]
+do_pointers::1::x \(\) -> 30 @ \[20\]
+do_pointers::1::x \(\) -> 40 @ \[21\]
+do_pointers::1::x \(\) -> TOP @ \[22\]
+do_pointers::1::x \(\) -> 50 @ \[23\]
+do_pointers::1::y_p \(\) -> ptr ->\(do_pointers::1::x\) @ \[24\]
+do_pointers::1::x \(\) -> 60 @ \[25\]
+do_pointers::1::j \(\) -> TOP @ \[26\]
+do_pointers::1::j \(\) -> 60 @ \[27\]
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 9b63fdf295e..c74416efa88 100644
--- a/regression/goto-analyzer/sensitivity-last-written-locations-structs/test.desc
+++ b/regression/goto-analyzer/sensitivity-last-written-locations-structs/test.desc
@@ -6,37 +6,31 @@ activate-multi-line-match
 ^EXIT=0$
 ^SIGNAL=0$
 main#return_value \(\) -> TOP @ \[1\]
-__CPROVER_dead_object \(\) -> TOP @ \[5\]
-__CPROVER_deallocated \(\) -> TOP @ \[6\]
-__CPROVER_malloc_is_new_array \(\) -> FALSE @ \[7\]
-__CPROVER_memory_leak \(\) -> TOP @ \[9\]
-__CPROVER_new_object \(\) -> TOP @ \[10\]
-__CPROVER_next_thread_key \(\) -> 0ul @ \[12\]
-__CPROVER_pipe_count \(\) -> 0u @ \[13\]
-__CPROVER_rounding_mode \(\) -> 0 @ \[14\]
-__CPROVER_thread_id \(\) -> 0ul @ \[15\]
-__CPROVER_threads_exited \(\) -> TOP @ \[18\]
-do_structs::1::bool_ \(\) -> TOP @ \[20\]
-do_structs::1::bool_1 \(\) -> TOP @ \[21\]
-do_structs::1::bool_2 \(\) -> TOP @ \[22\]
-do_structs::1::st \(\) -> \{\} @ \[23\]
-do_structs::1::st \(\) -> \{.x=10 @ \[24\]\} @ \[24\]
-do_structs::1::st \(\) -> \{.x=10 @ \[24\]\, .y=20 @ \[25\]\} @ \[25\]
-do_structs::1::st \(\) -> \{.x=30 @ \[26\]\, .y=20 @ \[25\]\} @ \[26\]
-do_structs::1::st \(\) -> \{.x=30 @ \[26\]\, .y=40 @ \[27\]\} @ \[27\]
-do_structs::1::st \(\) -> \{.x=30 @ \[26\]\, .y=30 @ \[28\]\} @ \[28\]
-do_structs::1::st \(\) -> \{.x=30 @ \[29\]\, .y=30 @ \[28\]\} @ \[29\]
-do_structs::1::st \(\) -> \{.x=5 @ \[30\]\, .y=30 @ \[28\]\} @ \[30\]
-do_structs::1::st \(\) -> \{.x=15 @ \[31\]\, .y=30 @ \[28\]\} @ \[31\]
-do_structs::1::st \(\) -> \{.x=15 @ \[31\]\, .y=10 @ \[32\]\} @ \[32\]
-do_structs::1::st \(\) -> \{.x=20 @ \[34\]\, .y=10 @ \[32\]\} @ \[34\]
-do_structs::1::st \(\) -> \{.x=20 @ \[34\, 36\]\, .y=10 @ \[32\]\} @ \[34\, 36\]
-do_structs::1::st \(\) -> \{.x=0 @ \[38\]\, .y=10 @ \[32\]\} @ \[38\]
-do_structs::1::st \(\) -> \{.x=3 @ \[40\]\, .y=10 @ \[32\]\} @ \[40\]
-do_structs::1::st \(\) -> \{.x=TOP @ \[40\, 42\]\, .y=10 @ \[32\]\} @ \[40\, 42\]
-do_structs::1::st \(\) -> \{.x=TOP @ \[40\, 42\, 45\]\, .y=10 @ \[32\]\} @ \[40\, 42\, 45\]
-do_structs::1::st \(\) -> \{.x=TOP @ \[40\, 42\, 45\]\, .y=10 @ \[47\]\} @ \[47\]
-do_structs::1::st \(\) -> \{.x=20 @ \[48\]\, .y=10 @ \[47\]\} @ \[48\]
-do_structs::1::new_age \(\) -> \{\} @ \[49\]
-do_structs::1::new_age \(\) -> \{.x=20 @ \[50\]\, .y=10 @ \[50\]\} @ \[50\]
+__CPROVER_dead_object \(\) -> TOP @ \[4\]
+__CPROVER_deallocated \(\) -> TOP @ \[5\]
+__CPROVER_memory_leak \(\) -> TOP @ \[7\]
+__CPROVER_rounding_mode \(\) -> 0 @ \[8\]
+do_structs::1::bool_ \(\) -> TOP @ \[10\]
+do_structs::1::bool_1 \(\) -> TOP @ \[11\]
+do_structs::1::bool_2 \(\) -> TOP @ \[12\]
+do_structs::1::st \(\) -> \{\} @ \[13\]
+do_structs::1::st \(\) -> \{.x=10 @ \[14\]\} @ \[14\]
+do_structs::1::st \(\) -> \{.x=10 @ \[14\]\, .y=20 @ \[15\]\} @ \[15\]
+do_structs::1::st \(\) -> \{.x=30 @ \[16\]\, .y=20 @ \[15\]\} @ \[16\]
+do_structs::1::st \(\) -> \{.x=30 @ \[16\]\, .y=40 @ \[17\]\} @ \[17\]
+do_structs::1::st \(\) -> \{.x=30 @ \[16\]\, .y=30 @ \[18\]\} @ \[18\]
+do_structs::1::st \(\) -> \{.x=30 @ \[19\]\, .y=30 @ \[18\]\} @ \[19\]
+do_structs::1::st \(\) -> \{.x=5 @ \[20\]\, .y=30 @ \[18\]\} @ \[20\]
+do_structs::1::st \(\) -> \{.x=15 @ \[21\]\, .y=30 @ \[18\]\} @ \[21\]
+do_structs::1::st \(\) -> \{.x=15 @ \[21\]\, .y=10 @ \[22\]\} @ \[22\]
+do_structs::1::st \(\) -> \{.x=20 @ \[24\]\, .y=10 @ \[22\]\} @ \[24\]
+do_structs::1::st \(\) -> \{.x=20 @ \[24\, 26\]\, .y=10 @ \[22\]\} @ \[24\, 26\]
+do_structs::1::st \(\) -> \{.x=0 @ \[28\]\, .y=10 @ \[22\]\} @ \[28\]
+do_structs::1::st \(\) -> \{.x=3 @ \[30\]\, .y=10 @ \[22\]\} @ \[30\]
+do_structs::1::st \(\) -> \{.x=TOP @ \[30\, 32\]\, .y=10 @ \[22\]\} @ \[30\, 32\]
+do_structs::1::st \(\) -> \{.x=TOP @ \[30\, 32\, 35\]\, .y=10 @ \[22\]\} @ \[30\, 32\, 35\]
+do_structs::1::st \(\) -> \{.x=TOP @ \[30\, 32\, 35\]\, .y=10 @ \[37\]\} @ \[37\]
+do_structs::1::st \(\) -> \{.x=20 @ \[38\]\, .y=10 @ \[37\]\} @ \[38\]
+do_structs::1::new_age \(\) -> \{\} @ \[39\]
+do_structs::1::new_age \(\) -> \{.x=20 @ \[40\]\, .y=10 @ \[40\]\} @ \[40\]
 --
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 37eb13074fc..ccb6a2526dc 100644
--- a/regression/goto-analyzer/sensitivity-last-written-locations-variables/test.desc
+++ b/regression/goto-analyzer/sensitivity-last-written-locations-variables/test.desc
@@ -4,42 +4,35 @@ sensitivity_dependency_variables.c
 ^EXIT=0$
 ^SIGNAL=0$
 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 @ \[7\]
-__CPROVER_memory_leak \(\) -> TOP @ \[9\]
-__CPROVER_new_object \(\) -> TOP @ \[10\]
-__CPROVER_next_thread_key \(\) -> 0ul @ \[12\]
-__CPROVER_pipe_count \(\) -> 0u @ \[13\]
-__CPROVER_rounding_mode \(\) -> 0 @ \[14\]
-__CPROVER_thread_id \(\) -> 0ul @ \[15\]
-__CPROVER_threads_exited \(\) -> TOP @ \[18\]
-global_x \(\) -> 0 @ \[19\]
-do_variables::1::bool_ \(\) -> TOP @ \[21\]
-do_variables::1::bool_1 \(\) -> TOP @ \[22\]
-do_variables::1::bool_2 \(\) -> TOP @ \[23\]
-global_x \(\) -> 5 @ \[24\]
-do_variables::1::x \(\) -> TOP @ \[25\]
-do_variables::1::x \(\) -> 10 @ \[26\]
-do_variables::1::y \(\) -> TOP @ \[27\]
-do_variables::1::y \(\) -> 20 @ \[28\]
-do_variables::1::x \(\) -> 30 @ \[29\]
-do_variables::1::y \(\) -> 40 @ \[30\]
-do_variables::1::y \(\) -> 30 @ \[31\]
-do_variables::1::x \(\) -> 30 @ \[32\]
-do_variables::1::x \(\) -> 5 @ \[33\]
-do_variables::1::x \(\) -> 15 @ \[34\]
-do_variables::1::y \(\) -> 10 @ \[35\]
-do_variables::1::x \(\) -> 20 @ \[37\]
-do_variables::1::x \(\) -> 20 @ \[37\, 39\]
-do_variables::1::x \(\) -> 50 @ \[41\]
-do_variables::1::x \(\) -> 20 @ \[43\]
-do_variables::1::x \(\) -> TOP @ \[43\, 45\]
-do_variables::1::x \(\) -> 0 @ \[47\]
-do_variables::1::x \(\) -> 3 @ \[49\]
-do_variables::1::x \(\) -> TOP @ \[49\, 51\]
-do_variables::1::x \(\) -> TOP @ \[49\, 51\, 54\]
-do_variables::1::y \(\) -> 10 @ \[56\]
-do_variables::1::x \(\) -> 20 @ \[57\]
+__CPROVER_dead_object \(\) -> TOP @ \[4\]
+__CPROVER_deallocated \(\) -> TOP @ \[5\]
+__CPROVER_memory_leak \(\) -> TOP @ \[7\]
+__CPROVER_rounding_mode \(\) -> 0 @ \[8\]
+global_x \(\) -> 0 @ \[9\]
+do_variables::1::bool_ \(\) -> TOP @ \[11\]
+do_variables::1::bool_1 \(\) -> TOP @ \[12\]
+do_variables::1::bool_2 \(\) -> TOP @ \[13\]
+global_x \(\) -> 5 @ \[14\]
+do_variables::1::x \(\) -> TOP @ \[15\]
+do_variables::1::x \(\) -> 10 @ \[16\]
+do_variables::1::y \(\) -> TOP @ \[17\]
+do_variables::1::y \(\) -> 20 @ \[18\]
+do_variables::1::x \(\) -> 30 @ \[19\]
+do_variables::1::y \(\) -> 40 @ \[20\]
+do_variables::1::y \(\) -> 30 @ \[21\]
+do_variables::1::x \(\) -> 30 @ \[22\]
+do_variables::1::x \(\) -> 5 @ \[23\]
+do_variables::1::x \(\) -> 15 @ \[24\]
+do_variables::1::y \(\) -> 10 @ \[25\]
+do_variables::1::x \(\) -> 20 @ \[27\]
+do_variables::1::x \(\) -> 20 @ \[27\, 29\]
+do_variables::1::x \(\) -> 50 @ \[31\]
+do_variables::1::x \(\) -> 20 @ \[33\]
+do_variables::1::x \(\) -> TOP @ \[33\, 35\]
+do_variables::1::x \(\) -> 0 @ \[37\]
+do_variables::1::x \(\) -> 3 @ \[39\]
+do_variables::1::x \(\) -> TOP @ \[39\, 41\]
+do_variables::1::x \(\) -> TOP @ \[39\, 41\, 44\]
+do_variables::1::y \(\) -> 10 @ \[46\]
+do_variables::1::x \(\) -> 20 @ \[47\]
 --
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 e070c053f6f..a87879274f8 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, 52\]\[Data dependencies: 52, 2\]\[Data dominators: \], .b=.* @ \[5, 52\]\[Data dependencies: 52, 5\]\[Data dominators: \]\} @ \[2, 5, 52\]\[Data dependencies: 52, 5, 2\]\[Data dominators: 52\]
-ar \(\) -> \{\[0\] = TOP @ \[11\, 46\]\[Data dependencies: 46\, 11\]\[Data dominators: \]\n\[1\] = TOP @ \[14\, 46\]\[Data dependencies: 46\, 14\]\[Data dominators: \]\n\} @ \[11\, 14\, 46\]\[Data dependencies: 46\, 14\, 11\]\[Data dominators: 46\]
-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: 47\]
+st \(\) -> \{.a=.* @ \[2, 42\]\[Data dependencies: 42, 2\]\[Data dominators: \], .b=.* @ \[5, 42\]\[Data dependencies: 42, 5\]\[Data dominators: \]\} @ \[2, 5, 42\]\[Data dependencies: 42, 5, 2\]\[Data dominators: 42\]
+ar \(\) -> \{\[0\] = TOP @ \[11\, 36\]\[Data dependencies: 36\, 11\]\[Data dominators: \]\n\[1\] = TOP @ \[14\, 36\]\[Data dependencies: 36\, 14\]\[Data dominators: \]\n\} @ \[11\, 14\, 36\]\[Data dependencies: 36\, 14\, 11\]\[Data dominators: 36\]
+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: 37\]
 --
 ^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 1bd4f4ec3b5..cd3a57851d6 100644
--- a/regression/goto-analyzer/variable-sensitivity-dependence-graph-toyota/test.desc
+++ b/regression/goto-analyzer/variable-sensitivity-dependence-graph-toyota/test.desc
@@ -3,24 +3,24 @@ main.c
 file1.c file2.c --dependence-graph-vs --vsd-structs every-field --vsd-arrays every-element --show
 ^EXIT=0$
 ^SIGNAL=0$
-^Data dependencies: 58 \[st.a\]$
-^Data dependencies: 58 \[st.b\]$
-^Data dependencies: 1 \[st.a\], 58 \[st.a\]$
-^Data dependencies: 4 \[st.b\], 58 \[st.b\]$
-^Data dependencies: 1 \[st.a\], 4 \[st.b\], 58 \[st.a, st.b\]$
-^Data dependencies: 52 \[ar\[\([^)]*\)0\]\]$
-^Data dependencies: 52 \[ar\[\([^)]*\)1\]\]$
-^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 52 \[ar\[\([^)]*\)0\]\]$
-^Data dependencies: 13 \[ar\[\([^)]*\)1\]\], 52 \[ar\[\([^)]*\)1\]\]$
-^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 13 \[ar\[\([^)]*\)1\]\], 52 \[ar\[\([^)]*\)0\], ar\[\([^)]*\)1\]\]$
+^Data dependencies: 48 \[st.a\]$
+^Data dependencies: 48 \[st.b\]$
+^Data dependencies: 1 \[st.a\], 48 \[st.a\]$
+^Data dependencies: 4 \[st.b\], 48 \[st.b\]$
+^Data dependencies: 1 \[st.a\], 4 \[st.b\], 48 \[st.a, st.b\]$
+^Data dependencies: 42 \[ar\[\([^)]*\)0\]\]$
+^Data dependencies: 42 \[ar\[\([^)]*\)1\]\]$
+^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 42 \[ar\[\([^)]*\)0\]\]$
+^Data dependencies: 13 \[ar\[\([^)]*\)1\]\], 42 \[ar\[\([^)]*\)1\]\]$
+^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 13 \[ar\[\([^)]*\)1\]\], 42 \[ar\[\([^)]*\)0\], ar\[\([^)]*\)1\]\]$
 ^Data dependencies: 19 \[arr\[\([^)]*\)1\]\]$
 ^Data dependencies: 18 \[arr\[\([^)]*\)0\]\]$
 ^Data dependencies: 20 \[arr\[\([^)]*\)2\]\], 22 \[arr\[\([^)]*\)2\]\]$
-^Data dependencies: 1 \[st.a\], 58 \[st.a\], 62 \[st.a\]$
-^Data dependencies: 4 \[st.b\], 58 \[st.b\], 65 \[st.b\]$
-^Data dependencies: 1 \[st.a\], 4 \[st.b\], 58 \[st.a, st.b\], 62 \[st.a\], 65 \[st.b\]$
-^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 52 \[ar\[\([^)]*\)0\]\], 73 \[ar\[\([^)]*\)0\]\]$
-^Data dependencies: 13 \[ar\[\([^)]*\)1\]\], 52 \[ar\[\([^)]*\)1\]\], 76 \[ar\[\([^)]*\)1\]\]$
-^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 13 \[ar\[\([^)]*\)1\]\], 52 \[ar\[\([^)]*\)0\], ar\[\([^)]*\)1\]\], 73 \[ar\[\([^)]*\)0\]\], 76 \[ar\[\([^)]*\)1\]\]$
+^Data dependencies: 1 \[st.a\], 48 \[st.a\], 52 \[st.a\]$
+^Data dependencies: 4 \[st.b\], 48 \[st.b\], 55 \[st.b\]$
+^Data dependencies: 1 \[st.a\], 4 \[st.b\], 48 \[st.a, st.b\], 52 \[st.a\], 55 \[st.b\]$
+^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 42 \[ar\[\([^)]*\)0\]\], 63 \[ar\[\([^)]*\)0\]\]$
+^Data dependencies: 13 \[ar\[\([^)]*\)1\]\], 42 \[ar\[\([^)]*\)1\]\], 66 \[ar\[\([^)]*\)1\]\]$
+^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 13 \[ar\[\([^)]*\)1\]\], 42 \[ar\[\([^)]*\)0\], ar\[\([^)]*\)1\]\], 63 \[ar\[\([^)]*\)0\]\], 66 \[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 a87e2b7a739..8abe0ffdcec 100644
--- a/regression/goto-analyzer/variable-sensitivity-dependence-graph/test.desc
+++ b/regression/goto-analyzer/variable-sensitivity-dependence-graph/test.desc
@@ -3,25 +3,25 @@ main.c
 file1.c file2.c --dependence-graph-vs --vsd-structs every-field --vsd-arrays every-element --show
 ^EXIT=0$
 ^SIGNAL=0$
-^Data dependencies: 58 \[st.a\]$
-^Data dependencies: 58 \[st.b\]$
-^Data dependencies: 1 \[st.a\], 58 \[st.a\]$
-^Data dependencies: 4 \[st.b\], 58 \[st.b\]$
-^Data dependencies: 1 \[st.a\], 4 \[st.b\], 58 \[st.a, st.b\]$
-^Data dependencies: 52 \[ar\[\([^)]*\)0\]\]$
+^Data dependencies: 48 \[st.a\]$
+^Data dependencies: 48 \[st.b\]$
+^Data dependencies: 1 \[st.a\], 48 \[st.a\]$
+^Data dependencies: 4 \[st.b\], 48 \[st.b\]$
+^Data dependencies: 1 \[st.a\], 4 \[st.b\], 48 \[st.a, st.b\]$
+^Data dependencies: 42 \[ar\[\([^)]*\)0\]\]$
 ^Data dependencies: 6 \[out1\]$
-^Data dependencies: 52 \[ar\[\([^)]*\)1\]\]$
-^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 52 \[ar\[\([^)]*\)0\]\]$
-^Data dependencies: 13 \[ar\[\([^)]*\)1\]\], 52 \[ar\[\([^)]*\)1\]\]$
-^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 13 \[ar\[\([^)]*\)1\]\], 52 \[ar\[\([^)]*\)0\], ar\[\([^)]*\)1\]\]$
+^Data dependencies: 42 \[ar\[\([^)]*\)1\]\]$
+^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 42 \[ar\[\([^)]*\)0\]\]$
+^Data dependencies: 13 \[ar\[\([^)]*\)1\]\], 42 \[ar\[\([^)]*\)1\]\]$
+^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 13 \[ar\[\([^)]*\)1\]\], 42 \[ar\[\([^)]*\)0\], ar\[\([^)]*\)1\]\]$
 ^Data dependencies: 19 \[arr\[\([^)]*\)1\]\]$
 ^Data dependencies: 18 \[arr\[\([^)]*\)0\]\]$
 ^Data dependencies: 20 \[arr\[\([^)]*\)2\]\], 22 \[arr\[\([^)]*\)2\]\]$
-^Data dependencies: 1 \[st.a\], 58 \[st.a\], 62 \[st.a\]$
-^Data dependencies: 4 \[st.b\], 58 \[st.b\], 65 \[st.b\]$
-^Data dependencies: 1 \[st.a\], 4 \[st.b\], 58 \[st.a, st.b\], 62 \[st.a\], 65 \[st.b\]$
-^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 52 \[ar\[\([^)]*\)0\]\], 73 \[ar\[\([^)]*\)0\]\]$
-^Data dependencies: 13 \[ar\[\([^)]*\)1\]\], 52 \[ar\[\([^)]*\)1\]\], 76 \[ar\[\([^)]*\)1\]\]$
-^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 13 \[ar\[\([^)]*\)1\]\], 52 \[ar\[\([^)]*\)0\], ar\[\([^)]*\)1\]\], 73 \[ar\[\([^)]*\)0\]\], 76 \[ar\[\([^)]*\)1\]\]$
+^Data dependencies: 1 \[st.a\], 48 \[st.a\], 52 \[st.a\]$
+^Data dependencies: 4 \[st.b\], 48 \[st.b\], 55 \[st.b\]$
+^Data dependencies: 1 \[st.a\], 4 \[st.b\], 48 \[st.a, st.b\], 52 \[st.a\], 55 \[st.b\]$
+^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 42 \[ar\[\([^)]*\)0\]\], 63 \[ar\[\([^)]*\)0\]\]$
+^Data dependencies: 13 \[ar\[\([^)]*\)1\]\], 42 \[ar\[\([^)]*\)1\]\], 66 \[ar\[\([^)]*\)1\]\]$
+^Data dependencies: 10 \[ar\[\([^)]*\)0\]\], 13 \[ar\[\([^)]*\)1\]\], 42 \[ar\[\([^)]*\)0\], ar\[\([^)]*\)1\]\], 63 \[ar\[\([^)]*\)0\]\], 66 \[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 fc1a4eff163..8bae062cd04 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: 34 \[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: 24 \[UNCONDITIONAL\]\nData dependencies: 1 \[g_a\[\([^)]*\)i\]\], 2 \[g_a\[\([^)]*\)i\]\], 3 \[g_a\[\([^)]*\)i\]\], 7 \[g_a\[\([^)]*\)i\]\]
 --
diff --git a/regression/goto-cc-goto-analyzer/instrument_preconditions_locations/s2n_hash_inlined.c b/regression/goto-cc-goto-analyzer/instrument_preconditions_locations/s2n_hash_inlined.c
index 5dc784acc4a..0c4baffd118 100644
--- a/regression/goto-cc-goto-analyzer/instrument_preconditions_locations/s2n_hash_inlined.c
+++ b/regression/goto-cc-goto-analyzer/instrument_preconditions_locations/s2n_hash_inlined.c
@@ -1,3 +1,5 @@
+#include <stdlib.h>
+
 // This file is highly reduced from some open source projects.
 // The following four lines are adapted from the openssl library
 // Full repository here:
diff --git a/src/ansi-c/ansi_c_internal_additions.cpp b/src/ansi-c/ansi_c_internal_additions.cpp
index d5f4911e4f4..901b88cc383 100644
--- a/src/ansi-c/ansi_c_internal_additions.cpp
+++ b/src/ansi-c/ansi_c_internal_additions.cpp
@@ -159,28 +159,15 @@ void ansi_c_internal_additions(std::string &code)
     "const unsigned " CPROVER_PREFIX "constant_infinity_uint;\n"
     "typedef void " CPROVER_PREFIX "integer;\n"
     "typedef void " CPROVER_PREFIX "rational;\n"
-    CPROVER_PREFIX "thread_local unsigned long " CPROVER_PREFIX "thread_id=0;\n"
-    CPROVER_PREFIX "bool " CPROVER_PREFIX "threads_exited["
-      CPROVER_PREFIX "constant_infinity_uint];\n"
-    "unsigned long " CPROVER_PREFIX "next_thread_id=0;\n"
-    CPROVER_PREFIX "thread_local const void* " CPROVER_PREFIX "thread_keys["
-      CPROVER_PREFIX "constant_infinity_uint];\n"
-    CPROVER_PREFIX "thread_local void (*" CPROVER_PREFIX "thread_key_dtors["
-      CPROVER_PREFIX "constant_infinity_uint])(void *);\n"
-    CPROVER_PREFIX "thread_local unsigned long "
-      CPROVER_PREFIX "next_thread_key = 0;\n"
     "extern unsigned char " CPROVER_PREFIX "memory["
       CPROVER_PREFIX "constant_infinity_uint];\n"
 
     // malloc
     "const void *" CPROVER_PREFIX "deallocated=0;\n"
     "const void *" CPROVER_PREFIX "dead_object=0;\n"
-    "const void *" CPROVER_PREFIX "new_object=0;\n" // for C++
-    CPROVER_PREFIX "bool " CPROVER_PREFIX "malloc_is_new_array=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"
-    "const void *" CPROVER_PREFIX "alloca_object = 0;\n"
     "void " CPROVER_PREFIX "deallocate(void *);\n"
 
     CPROVER_PREFIX "size_t " CPROVER_PREFIX "max_malloc_size="+
@@ -209,11 +196,6 @@ void ansi_c_internal_additions(std::string &code)
     "  short next_avail;\n"
     "  short next_unread;\n"
     "};\n"
-    "extern struct " CPROVER_PREFIX "pipet " CPROVER_PREFIX "pipes["
-      CPROVER_PREFIX "constant_infinity_uint];\n"
-    // offset to make sure we don't collide with other fds
-    "extern const int " CPROVER_PREFIX "pipe_offset;\n"
-    "unsigned " CPROVER_PREFIX "pipe_count=0;\n"
     "\n"
     // This function needs to be declared, or otherwise can't be called
     // by the entry-point construction.
diff --git a/src/ansi-c/cprover_library.cpp b/src/ansi-c/cprover_library.cpp
index 6582a491b1e..9966e83e669 100644
--- a/src/ansi-c/cprover_library.cpp
+++ b/src/ansi-c/cprover_library.cpp
@@ -98,7 +98,8 @@ std::string get_cprover_library_text(
 
 void cprover_c_library_factory(
   const std::set<irep_idt> &functions,
-  symbol_table_baset &symbol_table,
+  const symbol_table_baset &symbol_table,
+  symbol_table_baset &dest_symbol_table,
   message_handlert &message_handler)
 {
   if(config.ansi_c.lib==configt::ansi_ct::libt::LIB_NONE)
@@ -107,7 +108,7 @@ void cprover_c_library_factory(
   std::string library_text =
     get_cprover_library_text(functions, symbol_table, false);
 
-  add_library(library_text, symbol_table, message_handler);
+  add_library(library_text, dest_symbol_table, message_handler);
 }
 
 void add_library(
diff --git a/src/ansi-c/cprover_library.h b/src/ansi-c/cprover_library.h
index 80bbfea2608..33c67d980ad 100644
--- a/src/ansi-c/cprover_library.h
+++ b/src/ansi-c/cprover_library.h
@@ -41,6 +41,7 @@ void add_library(
 
 void cprover_c_library_factory(
   const std::set<irep_idt> &functions,
+  const symbol_table_baset &,
   symbol_table_baset &,
   message_handlert &);
 
diff --git a/src/ansi-c/library/cprover.h b/src/ansi-c/library/cprover.h
index 16b17990ea8..67b70f1bac7 100644
--- a/src/ansi-c/library/cprover.h
+++ b/src/ansi-c/library/cprover.h
@@ -18,11 +18,11 @@ typedef __typeof__(sizeof(int)) __CPROVER_size_t;
 // NOLINTNEXTLINE(readability/identifiers)
 typedef signed long long __CPROVER_ssize_t;
 
+#define __CPROVER_constant_infinity_uint 1
+
 void *__CPROVER_allocate(__CPROVER_size_t size, __CPROVER_bool zero);
 void __CPROVER_deallocate(void *);
 extern const void *__CPROVER_deallocated;
-extern const void *__CPROVER_new_object;
-extern __CPROVER_bool __CPROVER_malloc_is_new_array;
 extern const void *__CPROVER_memory_leak;
 
 extern int __CPROVER_malloc_failure_mode;
diff --git a/src/ansi-c/library/pthread_lib.c b/src/ansi-c/library/pthread_lib.c
index 5155a42e6c3..d893d6440a0 100644
--- a/src/ansi-c/library/pthread_lib.c
+++ b/src/ansi-c/library/pthread_lib.c
@@ -291,12 +291,17 @@ int pthread_mutex_destroy(pthread_mutex_t *mutex)
 #define __CPROVER_PTHREAD_H_INCLUDED
 #endif
 
-extern __CPROVER_bool __CPROVER_threads_exited[];
-extern __CPROVER_thread_local unsigned long __CPROVER_thread_id;
-
-extern __CPROVER_thread_local const void *__CPROVER_thread_keys[];
-extern __CPROVER_thread_local void (*__CPROVER_thread_key_dtors[])(void *);
-extern __CPROVER_thread_local unsigned long __CPROVER_next_thread_key;
+__CPROVER_bool __CPROVER_threads_exited[__CPROVER_constant_infinity_uint];
+__CPROVER_thread_local unsigned long __CPROVER_thread_id = 0;
+#if 0
+  // Destructor support is disabled as it is too expensive due to its extensive
+  // use of shared variables.
+__CPROVER_thread_local const void
+  *__CPROVER_thread_keys[__CPROVER_constant_infinity_uint];
+__CPROVER_thread_local void (
+  *__CPROVER_thread_key_dtors[__CPROVER_constant_infinity_uint])(void *);
+__CPROVER_thread_local unsigned long __CPROVER_next_thread_key = 0;
+#endif
 
 void pthread_exit(void *value_ptr)
 {
@@ -332,9 +337,11 @@ void pthread_exit(void *value_ptr)
 #define __CPROVER_ERRNO_H_INCLUDED
 #endif
 
-extern __CPROVER_bool __CPROVER_threads_exited[];
-extern __CPROVER_thread_local unsigned long __CPROVER_thread_id;
-extern unsigned long __CPROVER_next_thread_id;
+__CPROVER_bool __CPROVER_threads_exited[__CPROVER_constant_infinity_uint];
+#ifndef LIBRARY_CHECK
+__CPROVER_thread_local unsigned long __CPROVER_thread_id = 0;
+#endif
+unsigned long __CPROVER_next_thread_id = 0;
 
 int pthread_join(pthread_t thread, void **value_ptr)
 {
@@ -369,9 +376,11 @@ __CPROVER_HIDE:;
 #endif
 
 #ifdef __APPLE__
-extern __CPROVER_bool __CPROVER_threads_exited[];
-extern __CPROVER_thread_local unsigned long __CPROVER_thread_id;
-extern unsigned long __CPROVER_next_thread_id;
+__CPROVER_bool __CPROVER_threads_exited[__CPROVER_constant_infinity_uint];
+#  ifndef LIBRARY_CHECK
+__CPROVER_thread_local unsigned long __CPROVER_thread_id = 0;
+unsigned long __CPROVER_next_thread_id = 0;
+#  endif
 
 int _pthread_join(pthread_t thread, void **value_ptr)
 {
@@ -535,12 +544,19 @@ int pthread_rwlock_wrlock(pthread_rwlock_t *lock)
 
 /* FUNCTION: __spawned_thread */
 
-extern __CPROVER_bool __CPROVER_threads_exited[];
-extern __CPROVER_thread_local unsigned long __CPROVER_thread_id;
-
-extern __CPROVER_thread_local const void *__CPROVER_thread_keys[];
-extern __CPROVER_thread_local void (*__CPROVER_thread_key_dtors[])(void *);
-extern __CPROVER_thread_local unsigned long __CPROVER_next_thread_key;
+__CPROVER_bool __CPROVER_threads_exited[__CPROVER_constant_infinity_uint];
+#ifndef LIBRARY_CHECK
+__CPROVER_thread_local unsigned long __CPROVER_thread_id = 0;
+#endif
+#if 0
+  // Destructor support is disabled as it is too expensive due to its extensive
+  // use of shared variables.
+__CPROVER_thread_local const void
+  *__CPROVER_thread_keys[__CPROVER_constant_infinity_uint];
+__CPROVER_thread_local void (
+  *__CPROVER_thread_key_dtors[__CPROVER_constant_infinity_uint])(void *);
+#endif
+__CPROVER_thread_local unsigned long __CPROVER_next_thread_key = 0;
 
 void __spawned_thread(
   unsigned long this_thread_id,
@@ -598,7 +614,14 @@ __CPROVER_HIDE:;
 #  define __CPROVER_PTHREAD_H_INCLUDED
 #endif
 
-extern unsigned long __CPROVER_next_thread_id;
+#ifndef LIBRARY_CHECK
+unsigned long __CPROVER_next_thread_id = 0;
+#  if 0
+__CPROVER_thread_local void (
+  *__CPROVER_thread_key_dtors[__CPROVER_constant_infinity_uint])(void *);
+#  endif
+__CPROVER_thread_local unsigned long __CPROVER_next_thread_key = 0;
+#endif
 
 void __spawned_thread(
   unsigned long this_thread_id,
@@ -929,9 +952,15 @@ int pthread_barrier_wait(pthread_barrier_t *barrier)
 #define __CPROVER_PTHREAD_H_INCLUDED
 #endif
 
-extern __CPROVER_thread_local const void *__CPROVER_thread_keys[];
-extern __CPROVER_thread_local void (*__CPROVER_thread_key_dtors[])(void *);
-extern __CPROVER_thread_local unsigned long __CPROVER_next_thread_key;
+__CPROVER_thread_local const void
+  *__CPROVER_thread_keys[__CPROVER_constant_infinity_uint];
+#ifndef LIBRARY_CHECK
+#  if 0
+__CPROVER_thread_local void (
+  *__CPROVER_thread_key_dtors[__CPROVER_constant_infinity_uint])(void *);
+#  endif
+__CPROVER_thread_local unsigned long __CPROVER_next_thread_key = 0;
+#endif
 
 int pthread_key_create(pthread_key_t *key, void (*destructor)(void *))
 {
@@ -955,7 +984,8 @@ __CPROVER_HIDE:;
 #define __CPROVER_PTHREAD_H_INCLUDED
 #endif
 
-extern __CPROVER_thread_local const void *__CPROVER_thread_keys[];
+__CPROVER_thread_local const void
+  *__CPROVER_thread_keys[__CPROVER_constant_infinity_uint];
 
 int pthread_key_delete(pthread_key_t key)
 {
@@ -971,7 +1001,8 @@ __CPROVER_HIDE:;
 #define __CPROVER_PTHREAD_H_INCLUDED
 #endif
 
-extern __CPROVER_thread_local const void *__CPROVER_thread_keys[];
+__CPROVER_thread_local const void
+  *__CPROVER_thread_keys[__CPROVER_constant_infinity_uint];
 
 void *pthread_getspecific(pthread_key_t key)
 {
@@ -986,7 +1017,8 @@ __CPROVER_HIDE:;
 #define __CPROVER_PTHREAD_H_INCLUDED
 #endif
 
-extern __CPROVER_thread_local const void *__CPROVER_thread_keys[];
+__CPROVER_thread_local const void
+  *__CPROVER_thread_keys[__CPROVER_constant_infinity_uint];
 
 int pthread_setspecific(pthread_key_t key, const void *value)
 {
diff --git a/src/ansi-c/library/stdlib.c b/src/ansi-c/library/stdlib.c
index 4928d725dcb..327ae44593a 100644
--- a/src/ansi-c/library/stdlib.c
+++ b/src/ansi-c/library/stdlib.c
@@ -108,6 +108,7 @@ __CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
 #ifndef __GNUC__
 _Bool __builtin_mul_overflow();
 #endif
+__CPROVER_bool __CPROVER_malloc_is_new_array = 0;
 
 void *calloc(__CPROVER_size_t nmemb, __CPROVER_size_t size)
 {
@@ -169,6 +170,9 @@ __CPROVER_HIDE:;
 #undef malloc
 
 __CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
+#ifndef LIBRARY_CHECK
+__CPROVER_bool __CPROVER_malloc_is_new_array = 0;
+#endif
 
 // malloc is marked "inline" for the benefit of goto-analyzer. Really,
 // goto-analyzer should take care of inlining as needed.
@@ -225,7 +229,10 @@ __CPROVER_HIDE:;
 /* FUNCTION: __builtin_alloca */
 
 __CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
-extern void *__CPROVER_alloca_object;
+const void *__CPROVER_alloca_object = 0;
+#ifndef LIBRARY_CHECK
+__CPROVER_bool __CPROVER_malloc_is_new_array = 0;
+#endif
 
 void *__builtin_alloca(__CPROVER_size_t alloca_size)
 {
@@ -265,7 +272,13 @@ __CPROVER_HIDE:;
 #undef free
 
 __CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
-extern void *__CPROVER_alloca_object;
+#ifndef LIBRARY_CHECK
+const void *__CPROVER_alloca_object = 0;
+#endif
+const void *__CPROVER_new_object = 0;
+#ifndef LIBRARY_CHECK
+__CPROVER_bool __CPROVER_malloc_is_new_array = 0;
+#endif
 
 void free(void *ptr)
 {
diff --git a/src/ansi-c/library/unistd.c b/src/ansi-c/library/unistd.c
index 333cfc2a045..7fde194e53e 100644
--- a/src/ansi-c/library/unistd.c
+++ b/src/ansi-c/library/unistd.c
@@ -45,10 +45,10 @@ int unlink(const char *s)
 #define __CPROVER_ERRNO_H_INCLUDED
 #endif
 
-extern struct __CPROVER_pipet __CPROVER_pipes[];
+extern struct __CPROVER_pipet __CPROVER_pipes[__CPROVER_constant_infinity_uint];
 // offset to make sure we don't collide with other fds
 extern const int __CPROVER_pipe_offset;
-extern unsigned __CPROVER_pipe_count;
+unsigned __CPROVER_pipe_count = 0;
 
 __CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
 
@@ -97,7 +97,7 @@ __CPROVER_HIDE:;
 
 /* FUNCTION: close */
 
-extern struct __CPROVER_pipet __CPROVER_pipes[];
+extern struct __CPROVER_pipet __CPROVER_pipes[__CPROVER_constant_infinity_uint];
 // offset to make sure we don't collide with other fds
 extern const int __CPROVER_pipe_offset;
 
@@ -151,7 +151,7 @@ int _close(int fildes)
 #define size_type size_t
 #endif
 
-extern struct __CPROVER_pipet __CPROVER_pipes[];
+extern struct __CPROVER_pipet __CPROVER_pipes[__CPROVER_constant_infinity_uint];
 // offset to make sure we don't collide with other fds
 extern const int __CPROVER_pipe_offset;
 
@@ -229,7 +229,7 @@ ret_type _write(int fildes, const void *buf, size_type nbyte)
 #define size_type size_t
 #endif
 
-extern struct __CPROVER_pipet __CPROVER_pipes[];
+extern struct __CPROVER_pipet __CPROVER_pipes[__CPROVER_constant_infinity_uint];
 // offset to make sure we don't collide with other fds
 extern const int __CPROVER_pipe_offset;
 
diff --git a/src/cpp/cpp_internal_additions.cpp b/src/cpp/cpp_internal_additions.cpp
index c1365387c83..aae4a67dbff 100644
--- a/src/cpp/cpp_internal_additions.cpp
+++ b/src/cpp/cpp_internal_additions.cpp
@@ -67,36 +67,13 @@ void cpp_internal_additions(std::ostream &out)
   out << "const unsigned __CPROVER::constant_infinity_uint;" << '\n';
   out << "typedef void " CPROVER_PREFIX "integer;" << '\n';
   out << "typedef void " CPROVER_PREFIX "rational;" << '\n';
-  // TODO: thread_local is still broken
-  // out << "thread_local unsigned long "
-  //     << CPROVER_PREFIX "thread_id = 0;" << '\n';
-  out << CPROVER_PREFIX "bool "
-      << CPROVER_PREFIX "threads_exited[__CPROVER::constant_infinity_uint];"
-      << '\n';
-  out << "unsigned long " CPROVER_PREFIX "next_thread_id = 0;" << '\n';
-  // TODO: thread_local is still broken
-  out << "void* "
-      << CPROVER_PREFIX "thread_keys[__CPROVER::constant_infinity_uint];"
-      << '\n';
-  // TODO: thread_local is still broken
-  out << "void (*"
-      << CPROVER_PREFIX "thread_key_dtors[__CPROVER::constant_infinity_uint])"
-      << "(void *);" << '\n';
-  // TODO: thread_local is still broken
-  out << "unsigned long " CPROVER_PREFIX "next_thread_key = 0;" << '\n';
-  out << "extern unsigned char "
-      << CPROVER_PREFIX "memory[__CPROVER::constant_infinity_uint];" << '\n';
 
   // malloc
   out << "const void *" CPROVER_PREFIX "deallocated = 0;" << '\n';
   out << "const void *" CPROVER_PREFIX "dead_object = 0;" << '\n';
-  out << "const void *" CPROVER_PREFIX "new_object = 0;" << '\n';
-  out << "" CPROVER_PREFIX "bool " CPROVER_PREFIX "malloc_is_new_array = 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';
-  out << "const void *" CPROVER_PREFIX "alloca_object = 0;" << '\n';
 
   // auxiliaries for new/delete
   out << "void *__new(__CPROVER::size_t);" << '\n';
@@ -119,11 +96,6 @@ void cpp_internal_additions(std::ostream &out)
       << "  short next_avail;\n"
       << "  short next_unread;\n"
       << "};\n";
-  out << "extern struct " CPROVER_PREFIX "pipet "
-      << "" CPROVER_PREFIX "pipes[__CPROVER::constant_infinity_uint];" << '\n';
-  // offset to make sure we don't collide with other fds
-  out << "extern const int " CPROVER_PREFIX "pipe_offset;" << '\n';
-  out << "unsigned " CPROVER_PREFIX "pipe_count=0;" << '\n';
 
   // This function needs to be declared, or otherwise can't be called
   // by the entry-point construction.
diff --git a/src/cpp/cprover_library.cpp b/src/cpp/cprover_library.cpp
index e906808b4ec..b79134b37cb 100644
--- a/src/cpp/cprover_library.cpp
+++ b/src/cpp/cprover_library.cpp
@@ -37,7 +37,8 @@ static std::string get_cprover_library_text(
 
 void cprover_cpp_library_factory(
   const std::set<irep_idt> &functions,
-  symbol_table_baset &symbol_table,
+  const symbol_table_baset &symbol_table,
+  symbol_table_baset &dest_symbol_table,
   message_handlert &message_handler)
 {
   if(config.ansi_c.lib == configt::ansi_ct::libt::LIB_NONE)
@@ -46,5 +47,5 @@ void cprover_cpp_library_factory(
   const std::string library_text =
     get_cprover_library_text(functions, symbol_table);
 
-  add_library(library_text, symbol_table, message_handler);
+  add_library(library_text, dest_symbol_table, message_handler);
 }
diff --git a/src/cpp/cprover_library.h b/src/cpp/cprover_library.h
index 54a5661aec5..6000972eb23 100644
--- a/src/cpp/cprover_library.h
+++ b/src/cpp/cprover_library.h
@@ -18,6 +18,7 @@ class symbol_table_baset;
 
 void cprover_cpp_library_factory(
   const std::set<irep_idt> &functions,
+  const symbol_table_baset &,
   symbol_table_baset &,
   message_handlert &);
 
diff --git a/src/cpp/library/cprover.h b/src/cpp/library/cprover.h
index 7870bb31daf..cfbc3a9d4d5 100644
--- a/src/cpp/library/cprover.h
+++ b/src/cpp/library/cprover.h
@@ -13,8 +13,6 @@ 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_new_object;
-extern __CPROVER_bool __CPROVER_malloc_is_new_array;
 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 1f623058581..fd8261e47b4 100644
--- a/src/cpp/library/new.c
+++ b/src/cpp/library/new.c
@@ -1,6 +1,8 @@
 /* FUNCTION: __new */
 
 __CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
+const void *__CPROVER_new_object = 0;
+__CPROVER_bool __CPROVER_malloc_is_new_array = 0;
 
 inline void *__new(__typeof__(sizeof(int)) malloc_size)
 {
@@ -25,6 +27,8 @@ inline void *__new(__typeof__(sizeof(int)) malloc_size)
 /* FUNCTION: __new_array */
 
 __CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
+const void *__CPROVER_new_object = 0;
+__CPROVER_bool __CPROVER_malloc_is_new_array = 0;
 
 inline void *__new_array(__CPROVER_size_t count, __CPROVER_size_t size)
 {
@@ -60,6 +64,8 @@ inline void *__placement_new(__typeof__(sizeof(int)) malloc_size, void *p)
 /* FUNCTION: __delete */
 
 __CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
+const void *__CPROVER_new_object = 0;
+__CPROVER_bool __CPROVER_malloc_is_new_array = 0;
 
 inline void __delete(void *ptr)
 {
@@ -93,6 +99,8 @@ inline void __delete(void *ptr)
 /* FUNCTION: __delete_array */
 
 __CPROVER_bool __VERIFIER_nondet___CPROVER_bool();
+const void *__CPROVER_new_object = 0;
+__CPROVER_bool __CPROVER_malloc_is_new_array = 0;
 
 inline void __delete_array(void *ptr)
 {
diff --git a/src/goto-programs/link_to_library.cpp b/src/goto-programs/link_to_library.cpp
index 48b18553bb5..2e656cf589f 100644
--- a/src/goto-programs/link_to_library.cpp
+++ b/src/goto-programs/link_to_library.cpp
@@ -11,38 +11,100 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "link_to_library.h"
 
+#include <linking/static_lifetime_init.h>
+
 #include "compute_called_functions.h"
 #include "goto_convert_functions.h"
 #include "goto_model.h"
+#include "link_goto_model.h"
+
+/// Try to add \p missing_function from \p library to \p goto_model.
+static optionalt<replace_symbolt::expr_mapt> add_one_function(
+  goto_modelt &goto_model,
+  message_handlert &message_handler,
+  const std::function<void(
+    const std::set<irep_idt> &,
+    const symbol_tablet &,
+    symbol_tablet &,
+    message_handlert &)> &library,
+  const irep_idt &missing_function)
+{
+  goto_modelt library_model;
+  library(
+    {missing_function},
+    goto_model.symbol_table,
+    library_model.symbol_table,
+    message_handler);
+
+  // convert to CFG
+  if(
+    library_model.symbol_table.symbols.find(missing_function) !=
+    library_model.symbol_table.symbols.end())
+  {
+    goto_convert(
+      missing_function,
+      library_model.symbol_table,
+      library_model.goto_functions,
+      message_handler);
+  }
+
+  // check whether additional initialization may be required
+  if(
+    goto_model.goto_functions.function_map.find(INITIALIZE_FUNCTION) !=
+    goto_model.goto_functions.function_map.end())
+  {
+    for(const auto &entry : library_model.symbol_table)
+    {
+      if(
+        entry.second.is_static_lifetime && !entry.second.is_type &&
+        !entry.second.is_macro && entry.second.type.id() != ID_code &&
+        !goto_model.symbol_table.has_symbol(entry.first))
+      {
+        goto_model.unload(INITIALIZE_FUNCTION);
+        break;
+      }
+    }
+  }
+
+  return link_goto_model(goto_model, std::move(library_model), message_handler);
+}
 
 /// Complete missing function definitions using the \p library.
 /// \param goto_model: goto model that may contain function calls and symbols
 ///   with missing function bodies
 /// \param message_handler: message handler to report library processing
 ///   problems
-/// \param library: generator function that produces function definitions for a
-///   given set of symbol names that have no body.
+/// \param library: generator function that produces function definitions (in
+///   the symbol table that is the third parameter) for a given set of symbol
+///   names (first parameter) that have no body in the source symbol table
+///   (second parameter).
 void link_to_library(
   goto_modelt &goto_model,
   message_handlert &message_handler,
-  const std::function<
-    void(const std::set<irep_idt> &, symbol_tablet &, message_handlert &)>
-    &library)
+  const std::function<void(
+    const std::set<irep_idt> &,
+    const symbol_tablet &,
+    symbol_tablet &,
+    message_handlert &)> &library)
 {
   // this needs a fixedpoint, as library functions
   // may depend on other library functions
 
   std::set<irep_idt> added_functions;
+  // Linking in library functions (now seeing full definitions rather than
+  // forward declarations, or perhaps even cases of missing forward
+  // declarations) may result in type changes to objects.
+  replace_symbolt::expr_mapt object_type_updates;
+  const bool had_init =
+    goto_model.goto_functions.function_map.find(INITIALIZE_FUNCTION) !=
+    goto_model.goto_functions.function_map.end();
 
   while(true)
   {
     std::unordered_set<irep_idt> called_functions =
       compute_called_functions(goto_model.goto_functions);
 
-    // eliminate those for which we already have a body
-
-    std::set<irep_idt> missing_functions;
-
+    bool changed = false;
     for(const auto &id : called_functions)
     {
       goto_functionst::function_mapt::const_iterator f_it =
@@ -59,30 +121,44 @@ void link_to_library(
         // already added
       }
       else
-        missing_functions.insert(id);
+      {
+        changed = true;
+        added_functions.insert(id);
+
+        auto updates_opt =
+          add_one_function(goto_model, message_handler, library, id);
+        if(!updates_opt.has_value())
+        {
+          messaget log{message_handler};
+          log.warning() << "Linking library function '" << id << "' failed"
+                        << messaget::eom;
+          continue;
+        }
+        object_type_updates.insert(updates_opt->begin(), updates_opt->end());
+      }
     }
 
     // done?
-    if(missing_functions.empty())
+    if(!changed)
       break;
+  }
 
-    library(missing_functions, goto_model.symbol_table, message_handler);
-
-    // convert to CFG
-    for(const auto &id : missing_functions)
-    {
-      if(
-        goto_model.symbol_table.symbols.find(id) !=
-        goto_model.symbol_table.symbols.end())
-      {
-        goto_convert(
-          id,
-          goto_model.symbol_table,
-          goto_model.goto_functions,
-          message_handler);
-      }
-
-      added_functions.insert(id);
-    }
+  if(
+    had_init &&
+    goto_model.goto_functions.function_map.find(INITIALIZE_FUNCTION) ==
+      goto_model.goto_functions.function_map.end())
+  {
+    static_lifetime_init(
+      goto_model.symbol_table,
+      goto_model.symbol_table.lookup_ref(INITIALIZE_FUNCTION).location);
+    goto_convert(
+      INITIALIZE_FUNCTION,
+      goto_model.symbol_table,
+      goto_model.goto_functions,
+      message_handler);
+    goto_model.goto_functions.update();
   }
+
+  if(!object_type_updates.empty())
+    finalize_linking(goto_model, object_type_updates);
 }
diff --git a/src/goto-programs/link_to_library.h b/src/goto-programs/link_to_library.h
index 8f04f377ddc..8ddf2d3b0b8 100644
--- a/src/goto-programs/link_to_library.h
+++ b/src/goto-programs/link_to_library.h
@@ -24,7 +24,10 @@ class symbol_tablet;
 void link_to_library(
   goto_modelt &,
   message_handlert &,
-  const std::function<
-    void(const std::set<irep_idt> &, symbol_tablet &, message_handlert &)> &);
+  const std::function<void(
+    const std::set<irep_idt> &,
+    const symbol_tablet &,
+    symbol_tablet &,
+    message_handlert &)> &);
 
 #endif // CPROVER_GOTO_PROGRAMS_LINK_TO_LIBRARY_H