diff --git a/regression/contracts/github_6168_infinite_unwinding_bug/test.desc b/regression/contracts/github_6168_infinite_unwinding_bug/test.desc
index b8c6488def9..4714105d895 100644
--- a/regression/contracts/github_6168_infinite_unwinding_bug/test.desc
+++ b/regression/contracts/github_6168_infinite_unwinding_bug/test.desc
@@ -4,8 +4,8 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
-^\[main.1\] line \d+ Check loop invariant before entry: SUCCESS$
-^\[main.2\] line \d+ Check that loop invariant is preserved: SUCCESS$
+^\[main.\d+\] line \d+ Check loop invariant before entry: SUCCESS$
+^\[main.\d+\] line \d+ Check that loop invariant is preserved: SUCCESS$
 --
 --
 This is guarding against an issue described in https://github.com/diffblue/cbmc/issues/6168.
diff --git a/regression/contracts/invar_check_break_fail/test.desc b/regression/contracts/invar_check_break_fail/test.desc
index 705739ed7aa..b473182ddc8 100644
--- a/regression/contracts/invar_check_break_fail/test.desc
+++ b/regression/contracts/invar_check_break_fail/test.desc
@@ -3,9 +3,10 @@ main.c
 --apply-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.1\] .* Check loop invariant before entry: SUCCESS$
-^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
-^\[main.assertion.1\] .* assertion r == 0: FAILURE$
+^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main\.\d+\] .* Check that r is assignable: SUCCESS$
+^\[main\.assertion\.\d+\] .* assertion r == 0: FAILURE$
 ^VERIFICATION FAILED$
 --
 This test is expected to fail along the code path where r is an even integer
diff --git a/regression/contracts/invar_check_break_pass/test.desc b/regression/contracts/invar_check_break_pass/test.desc
index 272f26256f3..afdd776fe65 100644
--- a/regression/contracts/invar_check_break_pass/test.desc
+++ b/regression/contracts/invar_check_break_pass/test.desc
@@ -3,9 +3,10 @@ main.c
 --apply-loop-contracts
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.1\] .* Check loop invariant before entry: SUCCESS$
-^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
-^\[main.assertion.1\] .* assertion r == 0 || r == 1: SUCCESS$
+^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main\.\d+\] .* Check that r is assignable: SUCCESS$
+^\[main\.assertion\.\d+\] .* assertion r == 0 || r == 1: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 This test checks that conditionals and `break` are correctly handled.
diff --git a/regression/contracts/invar_check_continue/test.desc b/regression/contracts/invar_check_continue/test.desc
index f29ca70fd67..a3b77498072 100644
--- a/regression/contracts/invar_check_continue/test.desc
+++ b/regression/contracts/invar_check_continue/test.desc
@@ -3,9 +3,10 @@ main.c
 --apply-loop-contracts
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.1\] .* Check loop invariant before entry: SUCCESS$
-^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
-^\[main.assertion.1\] .* assertion r == 0: SUCCESS$
+^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main\.\d+\] .* Check that r is assignable: SUCCESS$
+^\[main\.assertion\.\d+\] .* assertion r == 0: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 This test checks that conditionals and `continue` are correctly handled.
diff --git a/regression/contracts/invar_check_multiple_loops/test.desc b/regression/contracts/invar_check_multiple_loops/test.desc
index 95405e44617..625c7889df7 100644
--- a/regression/contracts/invar_check_multiple_loops/test.desc
+++ b/regression/contracts/invar_check_multiple_loops/test.desc
@@ -3,13 +3,17 @@ main.c
 --apply-loop-contracts
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.1\] .* Check loop invariant before entry: SUCCESS$
-^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
-^\[main.3\] .* Check decreases clause on loop iteration: SUCCESS$
-^\[main.4\] .* Check loop invariant before entry: SUCCESS$
-^\[main.5\] .* Check that loop invariant is preserved: SUCCESS$
-^\[main.6\] .* Check decreases clause on loop iteration: SUCCESS$
-^\[main.assertion.1\] .* assertion x == y \+ 2 \* n: SUCCESS$
+^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main\.\d+\] .* Check decreases clause on loop iteration: SUCCESS$
+^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main\.\d+\] .* Check decreases clause on loop iteration: SUCCESS$
+^\[main\.assertion\.\d+\] .* assertion x == y \+ 2 \* n: SUCCESS$
+^\[main\.\d+\] line 8 Check that r is assignable: SUCCESS$
+^\[main\.\d+\] line 15 Check that x is assignable: SUCCESS$
+^\[main\.\d+\] line 23 Check that y is assignable: SUCCESS$
+^\[main\.\d+\] line 24 Check that r is assignable: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 This test checks that multiple loops and `for` loops are correctly handled.
diff --git a/regression/contracts/invar_check_nested_loops/test.desc b/regression/contracts/invar_check_nested_loops/test.desc
index 56cce65d6c0..93b26c1ce39 100644
--- a/regression/contracts/invar_check_nested_loops/test.desc
+++ b/regression/contracts/invar_check_nested_loops/test.desc
@@ -3,13 +3,16 @@ main.c
 --apply-loop-contracts
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.1\] .* Check loop invariant before entry: SUCCESS$
-^\[main.5\] .* Check that loop invariant is preserved: SUCCESS$
-^\[main.6\] .* Check decreases clause on loop iteration: SUCCESS$
-^\[main.2\] .* Check loop invariant before entry: SUCCESS$
-^\[main.3\] .* Check that loop invariant is preserved: SUCCESS$
-^\[main.4\] .* Check decreases clause on loop iteration: SUCCESS$
-^\[main.assertion.1\] .* assertion s == n: SUCCESS$
+^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main\.\d+\] .* Check decreases clause on loop iteration: SUCCESS$
+^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main\.\d+\] .* Check decreases clause on loop iteration: SUCCESS$
+^\[main\.\d+] line 23 Check that s is assignable: SUCCESS$
+^\[main\.\d+] line 24 Check that a is assignable: SUCCESS$
+^\[main\.\d+] line 27 Check that s is assignable: SUCCESS$
+^\[main\.assertion.\d+\] .* assertion s == n: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 This test checks that nested loops, `for` loops,
diff --git a/regression/contracts/invar_check_pointer_modifies-01/test.desc b/regression/contracts/invar_check_pointer_modifies-01/test.desc
index f9be5027db7..3a97638f638 100644
--- a/regression/contracts/invar_check_pointer_modifies-01/test.desc
+++ b/regression/contracts/invar_check_pointer_modifies-01/test.desc
@@ -3,9 +3,11 @@ main.c
 --apply-loop-contracts --pointer-check
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.1\] .* Check loop invariant before entry: SUCCESS$
-^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
-^\[main.assertion.1\] .* assertion \*data = 42: SUCCESS$
+^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main\.\d+] .* Check that \*data is assignable: SUCCESS$
+^\[main\.\d+] .* Check that i is assignable: SUCCESS$
+^\[main\.assertion\.\d+\] .* assertion \*data = 42: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 ^\[main.pointer_dereference.*\] line .* dereference failure: pointer NULL in \*data: FAILURE
diff --git a/regression/contracts/invar_check_pointer_modifies-02/test.desc b/regression/contracts/invar_check_pointer_modifies-02/test.desc
index d96eca605ae..6dee673c6f9 100644
--- a/regression/contracts/invar_check_pointer_modifies-02/test.desc
+++ b/regression/contracts/invar_check_pointer_modifies-02/test.desc
@@ -3,10 +3,12 @@ main.c
 --apply-loop-contracts --pointer-check
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.1\] .* Check loop invariant before entry: SUCCESS$
-^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
-^\[main.assertion.1\] .* assertion data == copy: SUCCESS$
-^\[main.assertion.2\] .* assertion \*copy = 42: SUCCESS$
+^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main\.\d+\] .* Check that \*data is assignable: SUCCESS$
+^\[main\.\d+\] .* Check that i is assignable: SUCCESS$
+^\[main\.assertion\.\d+\] .* assertion data == copy: SUCCESS$
+^\[main\.assertion\.\d+\] .* assertion \*copy = 42: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 ^\[main.pointer_dereference.*\] line .* dereference failure: pointer NULL in \*data: FAILURE
diff --git a/regression/contracts/invar_check_sufficiency/test.desc b/regression/contracts/invar_check_sufficiency/test.desc
index 3c7c3b3bc33..3381482ec83 100644
--- a/regression/contracts/invar_check_sufficiency/test.desc
+++ b/regression/contracts/invar_check_sufficiency/test.desc
@@ -3,9 +3,10 @@ main.c
 --apply-loop-contracts
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.1\] .* Check loop invariant before entry: SUCCESS$
-^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
-^\[main.assertion.1\] .* assertion r == 0: SUCCESS$
+^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main\.\d+\] .* Check that r is assignable: SUCCESS$
+^\[main\.assertion\.1\] .* assertion r == 0: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 This test checks that a loop invariant can be proven to be inductive,
diff --git a/regression/contracts/invar_dynamic_struct_member/test.desc b/regression/contracts/invar_dynamic_struct_member/test.desc
index f312b930d1b..763072ccff7 100644
--- a/regression/contracts/invar_dynamic_struct_member/test.desc
+++ b/regression/contracts/invar_dynamic_struct_member/test.desc
@@ -3,8 +3,11 @@ main.c
 --apply-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.1\] .* Check loop invariant before entry: SUCCESS$
-^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main\.\d+\] .* Check that i is assignable: SUCCESS$
+^\[main\.\d+\] line 22 Check that t->x is assignable: SUCCESS$
+^\[main\.\d+\] line 25 Check that t->x is assignable: SUCCESS$
 ^\[main.assertion.1\] .* assertion .*: FAILURE$
 ^VERIFICATION FAILED$
 --
diff --git a/regression/contracts/invar_havoc_dynamic_array/main.c b/regression/contracts/invar_havoc_dynamic_array/main.c
index f6538f67727..e69388b3673 100644
--- a/regression/contracts/invar_havoc_dynamic_array/main.c
+++ b/regression/contracts/invar_havoc_dynamic_array/main.c
@@ -9,7 +9,10 @@ void main()
   data[5] = 0;
 
   for(unsigned i = 0; i < SIZE; i++)
+    // clang-format off
+    __CPROVER_assigns(i, __CPROVER_POINTER_OBJECT(data))
     __CPROVER_loop_invariant(i <= SIZE)
+    // clang-format on
     {
       data[i] = 1;
     }
diff --git a/regression/contracts/invar_havoc_dynamic_array/test.desc b/regression/contracts/invar_havoc_dynamic_array/test.desc
index b86d0b35c5c..0676aa4b6da 100644
--- a/regression/contracts/invar_havoc_dynamic_array/test.desc
+++ b/regression/contracts/invar_havoc_dynamic_array/test.desc
@@ -3,10 +3,12 @@ main.c
 --apply-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.1\] .* Check loop invariant before entry: SUCCESS$
-^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
-^\[main.assertion.1\] .* assertion data\[5\] == 0: FAILURE$
-^\[main.assertion.2\] .* assertion data\[5\] == 1: FAILURE$
+^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main\.\d+\] .* Check that i is assignable: SUCCESS$
+^\[main\.\d+\] .* Check that data\[\(signed long (long )?int\)i\] is assignable: SUCCESS$
+^\[main\.assertion\.\d+\] .* assertion data\[5\] == 0: FAILURE$
+^\[main\.assertion\.\d+\] .* assertion data\[5\] == 1: FAILURE$
 ^VERIFICATION FAILED$
 --
 --
diff --git a/regression/contracts/invar_havoc_dynamic_array_const_idx/test.desc b/regression/contracts/invar_havoc_dynamic_array_const_idx/test.desc
index 3c3fcb5f8e9..27ca897e8bb 100644
--- a/regression/contracts/invar_havoc_dynamic_array_const_idx/test.desc
+++ b/regression/contracts/invar_havoc_dynamic_array_const_idx/test.desc
@@ -3,10 +3,12 @@ main.c
 --apply-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.1\] .* Check loop invariant before entry: SUCCESS$
-^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
-^\[main.assertion.1\] .* assertion data\[1\] == 0 \|\| data\[1\] == 1: FAILURE$
-^\[main.assertion.2\] .* assertion data\[4\] == 0: SUCCESS$
+^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main\.\d+\] .* Check that i is assignable: SUCCESS$
+^\[main\.\d+\] .* Check that data\[\(signed long (long )?int\)1\] is assignable: SUCCESS$
+^\[main\.assertion\.\d+\] .* assertion data\[1\] == 0 \|\| data\[1\] == 1: FAILURE$
+^\[main\.assertion\.\d+\] .* assertion data\[4\] == 0: SUCCESS$
 ^VERIFICATION FAILED$
 --
 --
diff --git a/regression/contracts/invar_havoc_static_array/main.c b/regression/contracts/invar_havoc_static_array/main.c
index b62c8b8f207..8d4be0cc55a 100644
--- a/regression/contracts/invar_havoc_static_array/main.c
+++ b/regression/contracts/invar_havoc_static_array/main.c
@@ -9,7 +9,10 @@ void main()
   data[5] = 0;
 
   for(unsigned i = 0; i < SIZE; i++)
+    // clang-format off
+    __CPROVER_assigns(i, __CPROVER_POINTER_OBJECT(data))
     __CPROVER_loop_invariant(i <= SIZE)
+    // clang-format on
     {
       data[i] = 1;
     }
diff --git a/regression/contracts/invar_havoc_static_array/test.desc b/regression/contracts/invar_havoc_static_array/test.desc
index 3c37f31945c..efc72383f7d 100644
--- a/regression/contracts/invar_havoc_static_array/test.desc
+++ b/regression/contracts/invar_havoc_static_array/test.desc
@@ -3,10 +3,12 @@ main.c
 --apply-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.1\] .* Check loop invariant before entry: SUCCESS$
-^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
-^\[main.assertion.1\] .* assertion data\[5\] == 0: FAILURE$
-^\[main.assertion.2\] .* assertion data\[5\] == 1: FAILURE$
+^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main\.\d+\] .* Check that i is assignable: SUCCESS$
+^\[main\.\d+\] .* Check that data\[\(signed long (long )?int\)i\] is assignable: SUCCESS$
+^\[main\.assertion\.\d+\] .* assertion data\[5\] == 0: FAILURE$
+^\[main\.assertion\.\d+\] .* assertion data\[5\] == 1: FAILURE$
 ^VERIFICATION FAILED$
 --
 --
diff --git a/regression/contracts/invar_havoc_static_array_const_idx/test.desc b/regression/contracts/invar_havoc_static_array_const_idx/test.desc
index 7004c2b0d0d..3ca63dfe501 100644
--- a/regression/contracts/invar_havoc_static_array_const_idx/test.desc
+++ b/regression/contracts/invar_havoc_static_array_const_idx/test.desc
@@ -3,10 +3,12 @@ main.c
 --apply-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.1\] .* Check loop invariant before entry: SUCCESS$
-^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
-^\[main.assertion.1\] .* assertion data\[1\] == 0 \|\| data\[1\] == 1: FAILURE$
-^\[main.assertion.2\] .* assertion data\[4\] == 0: SUCCESS$
+^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main\.\d+\] .* Check that i is assignable: SUCCESS$
+^\[main\.\d+\] .* Check that data\[\(signed long (long )?int\)1\] is assignable: SUCCESS$
+^\[main\.assertion\.\d+\] .* assertion data\[1\] == 0 \|\| data\[1\] == 1: FAILURE$
+^\[main\.assertion\.\d+\] .* assertion data\[4\] == 0: SUCCESS$
 ^VERIFICATION FAILED$
 --
 --
diff --git a/regression/contracts/invar_havoc_static_multi-dim_array/test.desc b/regression/contracts/invar_havoc_static_multi-dim_array/test.desc
index b1b8b58c5e5..9fc74c3694d 100644
--- a/regression/contracts/invar_havoc_static_multi-dim_array/test.desc
+++ b/regression/contracts/invar_havoc_static_multi-dim_array/test.desc
@@ -3,10 +3,10 @@ main.c
 --apply-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.1\] .* Check loop invariant before entry: SUCCESS$
-^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
-^\[main.assertion.1\] .* assertion __CPROVER_same_object\(old_data123, &\(data\[1\]\[2\]\[3\]\)\): SUCCESS$
-^\[main.assertion.2\] .* assertion data\[1\]\[2\]\[3\] == 0: FAILURE$
+^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main\.assertion\.\d+\] .* assertion __CPROVER_same_object\(old_data123, &\(data\[1\]\[2\]\[3\]\)\): SUCCESS$
+^\[main\.assertion\.\d+\] .* assertion data\[1\]\[2\]\[3\] == 0: FAILURE$
 ^VERIFICATION FAILED$
 --
 --
diff --git a/regression/contracts/invar_havoc_static_multi-dim_array_all_const_idx/test.desc b/regression/contracts/invar_havoc_static_multi-dim_array_all_const_idx/test.desc
index 7a315d41510..052762e9b2f 100644
--- a/regression/contracts/invar_havoc_static_multi-dim_array_all_const_idx/test.desc
+++ b/regression/contracts/invar_havoc_static_multi-dim_array_all_const_idx/test.desc
@@ -3,10 +3,11 @@ main.c
 --apply-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.1\] .* Check loop invariant before entry: SUCCESS$
-^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
-^\[main.assertion.1\] .* assertion data\[4\]\[5\]\[6\] == 0: FAILURE$
-^\[main.assertion.2\] .* assertion data\[1\]\[2\]\[3\] == 0: SUCCESS$
+^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main\.\d+\] .* Check that data\[\(signed long (long )?int\)4\]\[\(signed long (long )?int\)5\]\[\(signed long (long )?int\)6\] is assignable: SUCCESS$
+^\[main\.assertion\.\d+\] .* assertion data\[4\]\[5\]\[6\] == 0: FAILURE$
+^\[main\.assertion\.\d+\] .* assertion data\[1\]\[2\]\[3\] == 0: SUCCESS$
 ^VERIFICATION FAILED$
 --
 --
diff --git a/regression/contracts/invar_havoc_static_multi-dim_array_partial_const_idx/main.c b/regression/contracts/invar_havoc_static_multi-dim_array_partial_const_idx/main.c
index dc1ecafd686..ad95ac3048e 100644
--- a/regression/contracts/invar_havoc_static_multi-dim_array_partial_const_idx/main.c
+++ b/regression/contracts/invar_havoc_static_multi-dim_array_partial_const_idx/main.c
@@ -11,7 +11,8 @@ void main()
   data[4][5][6] = 0;
 
   for(unsigned i = 0; i < SIZE; i++)
-    __CPROVER_loop_invariant(i <= SIZE)
+    __CPROVER_assigns(i, __CPROVER_POINTER_OBJECT(data))
+      __CPROVER_loop_invariant(i <= SIZE)
     {
       data[4][i][6] = 1;
     }
diff --git a/regression/contracts/invar_havoc_static_multi-dim_array_partial_const_idx/test.desc b/regression/contracts/invar_havoc_static_multi-dim_array_partial_const_idx/test.desc
index 1c0ebbdea38..910c438d54f 100644
--- a/regression/contracts/invar_havoc_static_multi-dim_array_partial_const_idx/test.desc
+++ b/regression/contracts/invar_havoc_static_multi-dim_array_partial_const_idx/test.desc
@@ -3,10 +3,12 @@ main.c
 --apply-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.1\] .* Check loop invariant before entry: SUCCESS$
-^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
-^\[main.assertion.1\] .* assertion data\[1\]\[2\]\[3\] == 0: FAILURE$
-^\[main.assertion.2\] .* assertion data\[4\]\[5\]\[6\] == 0: FAILURE$
+^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main\.\d+\] .* Check that i is assignable: SUCCESS$
+^\[main\.\d+\] .* Check that data\[\(signed long (long )?int\)4\]\[\(signed long (long )?int\)i\]\[\(signed long (long )?int\)6\] is assignable: SUCCESS$
+^\[main\.assertion\.\d+\] .* assertion data\[1\]\[2\]\[3\] == 0: FAILURE$
+^\[main\.assertion\.\d+\] .* assertion data\[4\]\[5\]\[6\] == 0: FAILURE$
 ^VERIFICATION FAILED$
 --
 --
diff --git a/regression/contracts/invar_loop-entry_check/test.desc b/regression/contracts/invar_loop-entry_check/test.desc
index 8278230c49e..37f389403dd 100644
--- a/regression/contracts/invar_loop-entry_check/test.desc
+++ b/regression/contracts/invar_loop-entry_check/test.desc
@@ -3,15 +3,24 @@ main.c
 --apply-loop-contracts _ --pointer-primitive-check
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.1\] .* Check loop invariant before entry: SUCCESS$
-^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
-^\[main.assertion.1\] .* assertion \*x1 == z1: SUCCESS$
-^\[main.3\] .* Check loop invariant before entry: SUCCESS$
-^\[main.4\] .* Check that loop invariant is preserved: SUCCESS$
-^\[main.assertion.2\] .* assertion x2 == z2: SUCCESS$
-^\[main.5\] .* Check loop invariant before entry: SUCCESS$
-^\[main.6\] .* Check that loop invariant is preserved: SUCCESS$
-^\[main.assertion.3\] .* assertion \*\(s1\.n\) == \*\(s2->n\): SUCCESS$
+^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main\.assertion\.\d+\] .* assertion \*x1 == z1: SUCCESS$
+^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main\.assertion\.\d+\] .* assertion x2 == z2: SUCCESS$
+^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main\.\d+\] .* Check that y1 is assignable: SUCCESS$
+^\[main\.\d+\] line 18 Check that \*x1 is assignable: SUCCESS$
+^\[main\.\d+\] line 19 Check that \*x1 is assignable: SUCCESS$
+^\[main\.\d+\] .* Check that y2 is assignable: SUCCESS$
+^\[main\.\d+\] line 30 Check that x2 is assignable: SUCCESS$
+^\[main\.\d+\] line 31 Check that x2 is assignable: SUCCESS$
+^\[main\.\d+\] .* Check that y3 is assignable: SUCCESS$
+^\[main\.\d+\] .* Check that s0\.n is assignable: SUCCESS$
+^\[main\.\d+\] .* Check that s2->n is assignable: SUCCESS$
+^\[main\.assertion\.\d+\] .* assertion \*\(s1\.n\) == \*\(s2->n\): SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 --
diff --git a/regression/contracts/invar_loop-entry_fail/test.desc b/regression/contracts/invar_loop-entry_fail/test.desc
index 1bfb43d60b7..c5a1d71b0b4 100644
--- a/regression/contracts/invar_loop-entry_fail/test.desc
+++ b/regression/contracts/invar_loop-entry_fail/test.desc
@@ -3,8 +3,11 @@ main.c
 --apply-loop-contracts
 ^EXIT=(10|6)$
 ^SIGNAL=0$
-^\[main.1\] .* Check loop invariant before entry: SUCCESS$
-^\[main.2\] .* Check that loop invariant is preserved: FAILURE$
+^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] .* Check that loop invariant is preserved: FAILURE$
+^\[main\.\d+\] line 11 Check that y is assignable: SUCCESS$
+^\[main\.\d+\] line 12 Check that x is assignable: SUCCESS$
+^\[main\.\d+\] line 13 Check that x is assignable: SUCCESS$
 ^VERIFICATION FAILED$
 --
 --
diff --git a/regression/contracts/invar_loop_constant_fail/test.desc b/regression/contracts/invar_loop_constant_fail/test.desc
index 3f1753aba33..5ffac813b1d 100644
--- a/regression/contracts/invar_loop_constant_fail/test.desc
+++ b/regression/contracts/invar_loop_constant_fail/test.desc
@@ -3,10 +3,12 @@ main.c
 --apply-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.1\] .* Check loop invariant before entry: SUCCESS$
-^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
-^\[main.assertion.1\] .* assertion r == 0: SUCCESS$
-^\[main.assertion.2\] .* assertion s == 1: FAILURE$
+^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main\.\d+\] .* Check that s is assignable: SUCCESS$
+^\[main\.\d+\] .* Check that r is assignable: SUCCESS$
+^\[main\.assertion\.\d+\] .* assertion r == 0: SUCCESS$
+^\[main\.assertion\.\d+\] .* assertion s == 1: FAILURE$
 ^VERIFICATION FAILED$
 --
 This test is expected to fail because it modifies a variable within a loop,
diff --git a/regression/contracts/invar_loop_constant_no_modify/test.desc b/regression/contracts/invar_loop_constant_no_modify/test.desc
index d169ad4403b..2cd7e168998 100644
--- a/regression/contracts/invar_loop_constant_no_modify/test.desc
+++ b/regression/contracts/invar_loop_constant_no_modify/test.desc
@@ -3,10 +3,11 @@ main.c
 --apply-loop-contracts
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.1\] .* Check loop invariant before entry: SUCCESS$
-^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
-^\[main.assertion.1\] .* assertion r == 0: SUCCESS$
-^\[main.assertion.2\] .* assertion s == 1: SUCCESS$
+^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main\.\d+\] .* Check that r is assignable: SUCCESS$
+^\[main\.assertion\.\d+\] .* assertion r == 0: SUCCESS$
+^\[main\.assertion\.\d+\] .* assertion s == 1: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 This test checks that variables that are not modified within the loop
diff --git a/regression/contracts/invar_loop_constant_pass/test.desc b/regression/contracts/invar_loop_constant_pass/test.desc
index e0538966c1d..56cefb66d88 100644
--- a/regression/contracts/invar_loop_constant_pass/test.desc
+++ b/regression/contracts/invar_loop_constant_pass/test.desc
@@ -3,10 +3,12 @@ main.c
 --apply-loop-contracts
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.1\] .* Check loop invariant before entry: SUCCESS$
-^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
-^\[main.assertion.1\] .* assertion r == 0: SUCCESS$
-^\[main.assertion.2\] .* assertion s == 1: SUCCESS$
+^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main\.\d+\] .* Check that s is assignable: SUCCESS$
+^\[main\.\d+\] .* Check that r is assignable: SUCCESS$
+^\[main\.assertion\.\d+\] .* assertion r == 0: SUCCESS$
+^\[main\.assertion\.\d+\] .* assertion s == 1: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 This test checks that the invariant is correctly used to satisfy
diff --git a/regression/contracts/invar_struct_member/test.desc b/regression/contracts/invar_struct_member/test.desc
index c969cfcc6cb..1c93bf225d8 100644
--- a/regression/contracts/invar_struct_member/test.desc
+++ b/regression/contracts/invar_struct_member/test.desc
@@ -3,9 +3,10 @@ main.c
 --apply-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.1\] .* Check loop invariant before entry: SUCCESS$
-^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
-^\[main.assertion.1\] .* assertion t.x == 0 || t.x == 2: FAILURE$
+^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main\.\d+\] .* Check that t\.x is assignable: SUCCESS$
+^\[main\.assertion\.\d+\] .* assertion t.x == 0 || t.x == 2: FAILURE$
 ^VERIFICATION FAILED$
 --
 --
diff --git a/regression/contracts/invariant_side_effects/test.desc b/regression/contracts/invariant_side_effects/test.desc
index 3e6caba882f..dcc839d15e2 100644
--- a/regression/contracts/invariant_side_effects/test.desc
+++ b/regression/contracts/invariant_side_effects/test.desc
@@ -3,9 +3,10 @@ main.c
 --apply-loop-contracts
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.1\] .* Check loop invariant before entry: SUCCESS$
-^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
-^\[main.assertion.1\] .* assertion \*a == N: SUCCESS$
+^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main\.\d+\] .* Check that \*a is assignable: SUCCESS$
+^\[main\.assertion\.\d+\] .* assertion \*a == N: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 This test checks that C expressions are correctly converted to logic
diff --git a/regression/contracts/loop_contracts_binary_search/test.desc b/regression/contracts/loop_contracts_binary_search/test.desc
index 57b27eb77c5..d95106cc389 100644
--- a/regression/contracts/loop_contracts_binary_search/test.desc
+++ b/regression/contracts/loop_contracts_binary_search/test.desc
@@ -3,10 +3,13 @@ main.c
 --apply-loop-contracts _ --pointer-check --bounds-check --signed-overflow-check
 ^EXIT=0$
 ^SIGNAL=0$
-^\[binary_search.1\] .* Check loop invariant before entry: SUCCESS$
-^\[binary_search.2\] .* Check that loop invariant is preserved: SUCCESS$
-^\[binary_search.3\] .* Check decreases clause on loop iteration: SUCCESS$
-^\[main.assertion.1\] .* assertion buf\[idx\] == val: SUCCESS$
+^\[binary_search\.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[binary_search\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[binary_search\.\d+\] .* Check decreases clause on loop iteration: SUCCESS$
+^\[binary_search\.2\] .* Check that lb is assignable: SUCCESS$
+^\[binary_search\.3\] .* Check that ub is assignable: SUCCESS$
+^\[binary_search\.4\] .* Check that mid is assignable: SUCCESS$
+^\[main\.assertion\.\d+\] .* assertion buf\[idx\] == val: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 --
diff --git a/regression/contracts/quantifiers-loop-01/main.c b/regression/contracts/quantifiers-loop-01/main.c
index e02067afe5f..4a75dec55d1 100644
--- a/regression/contracts/quantifiers-loop-01/main.c
+++ b/regression/contracts/quantifiers-loop-01/main.c
@@ -9,6 +9,7 @@ void main()
 
   for(int i = 0; i < N; ++i)
     // clang-format off
+    __CPROVER_assigns(i, __CPROVER_POINTER_OBJECT(a))
     __CPROVER_loop_invariant(
       (0 <= i) && (i <= N) &&
       __CPROVER_forall {
diff --git a/regression/contracts/quantifiers-loop-01/test.desc b/regression/contracts/quantifiers-loop-01/test.desc
index ebe5becbfa6..36add00c985 100644
--- a/regression/contracts/quantifiers-loop-01/test.desc
+++ b/regression/contracts/quantifiers-loop-01/test.desc
@@ -3,9 +3,11 @@ main.c
 --apply-loop-contracts
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.1\] line .* Check loop invariant before entry: SUCCESS
-^\[main.2\] line .* Check that loop invariant is preserved: SUCCESS
-^\[main.assertion.1\] line .* assertion a\[10\] == 1: SUCCESS
+^\[main\.\d+\] line .* Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] line .* Check that loop invariant is preserved: SUCCESS$
+^\[main\.\d+\] line .* Check that i is assignable: SUCCESS$
+^\[main\.\d+\] line .* Check that a\[\(signed long (long )?int\)i\] is assignable: SUCCESS$
+^\[main\.assertion\.\d+\] line .* assertion a\[10\] == 1: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
diff --git a/regression/contracts/quantifiers-loop-02/main.c b/regression/contracts/quantifiers-loop-02/main.c
index d4b57e7e7f9..0e58dd6a5cc 100644
--- a/regression/contracts/quantifiers-loop-02/main.c
+++ b/regression/contracts/quantifiers-loop-02/main.c
@@ -1,12 +1,14 @@
 #include <assert.h>
 
+#define MAX_ARRAY_SIZE 3
 void main()
 {
-  int N, a[64];
-  __CPROVER_assume(0 <= N && N < 64);
+  int N, a[MAX_ARRAY_SIZE];
+  __CPROVER_assume(0 <= N && N < MAX_ARRAY_SIZE);
 
   for(int i = 0; i < N; ++i)
     // clang-format off
+    __CPROVER_assigns(i, __CPROVER_POINTER_OBJECT(a))
     __CPROVER_loop_invariant(
       (0 <= i) && (i <= N) &&
       __CPROVER_forall {
diff --git a/regression/contracts/quantifiers-loop-02/test.desc b/regression/contracts/quantifiers-loop-02/test.desc
index 49cba1964f2..c84fbd9fe58 100644
--- a/regression/contracts/quantifiers-loop-02/test.desc
+++ b/regression/contracts/quantifiers-loop-02/test.desc
@@ -1,11 +1,13 @@
-CORE smt-backend broken-cprover-smt-backend
+CORE smt-backend broken-cprover-smt-backend thorough-smt-backend
 main.c
 --apply-loop-contracts _ --z3
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.\d+\] line .* Check loop invariant before entry: SUCCESS
-^\[main.\d+\] line .* Check that loop invariant is preserved: SUCCESS
-^\[main.assertion.\d+\] line .* assertion .*: SUCCESS
+^\[main.\d+\] line .* Check loop invariant before entry: SUCCESS$
+^\[main.\d+\] line .* Check that loop invariant is preserved: SUCCESS$
+^\[main\.\d+\] line .* Check that i is assignable: SUCCESS$
+^\[main\.\d+\] line .* Check that a\[\(signed long (long )?int\)i\] is assignable: SUCCESS$
+^\[main.assertion.\d+\] line .* assertion .*: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
diff --git a/regression/contracts/quantifiers-loop-03/main.c b/regression/contracts/quantifiers-loop-03/main.c
index ca45553db6e..4a9cecd5769 100644
--- a/regression/contracts/quantifiers-loop-03/main.c
+++ b/regression/contracts/quantifiers-loop-03/main.c
@@ -6,12 +6,13 @@
 void main()
 {
   unsigned N;
-  __CPROVER_assume(N <= MAX_SIZE);
+  __CPROVER_assume(0 < N && N <= MAX_SIZE);
 
   int *a = malloc(N * sizeof(int));
 
   for(int i = 0; i < N; ++i)
     // clang-format off
+    __CPROVER_assigns(i, __CPROVER_POINTER_OBJECT(a))
     __CPROVER_loop_invariant(
       (0 <= i) && (i <= N) &&
       (i != 0 ==> __CPROVER_exists {
diff --git a/regression/contracts/quantifiers-loop-03/test.desc b/regression/contracts/quantifiers-loop-03/test.desc
index 9c3f9f7b76c..8acc26e8542 100644
--- a/regression/contracts/quantifiers-loop-03/test.desc
+++ b/regression/contracts/quantifiers-loop-03/test.desc
@@ -3,9 +3,11 @@ main.c
 --apply-loop-contracts
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.1\] line .* Check loop invariant before entry: SUCCESS
-^\[main.2\] line .* Check that loop invariant is preserved: SUCCESS
-^\[main.assertion.1\] line .* assertion .*: SUCCESS
+^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main\.\d+\] .* Check that i is assignable: SUCCESS$
+^\[main\.\d+\] .* Check that a\[\(signed long (long )?int\)i\] is assignable: SUCCESS$
+^\[main\.assertion\.\d+\] line .* assertion .*: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
diff --git a/regression/contracts/variant_init_inside_loop/test.desc b/regression/contracts/variant_init_inside_loop/test.desc
index 08e6b348593..877d1d22045 100644
--- a/regression/contracts/variant_init_inside_loop/test.desc
+++ b/regression/contracts/variant_init_inside_loop/test.desc
@@ -1,12 +1,13 @@
 CORE
 main.c
 --apply-loop-contracts _ --unsigned-overflow-check
-^\[main.1\] .* Check loop invariant before entry: SUCCESS$
-^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
-^\[main.3\] .* Check decreases clause on loop iteration: SUCCESS$
-^\[main.overflow.1\] .* arithmetic overflow on unsigned - in max - i: SUCCESS$
-^\[main.overflow.3\] .* arithmetic overflow on unsigned - in max - i: SUCCESS$
-^\[main.overflow.2\] .* arithmetic overflow on unsigned \+ in i \+ 1u: SUCCESS$
+^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main\.\d+\] .* Check decreases clause on loop iteration: SUCCESS$
+^\[main\.2\] .* Check that i is assignable: SUCCESS$
+^\[main\.overflow\.1\] .* arithmetic overflow on unsigned - in max - i: SUCCESS$
+^\[main\.overflow\.3\] .* arithmetic overflow on unsigned - in max - i: SUCCESS$
+^\[main\.overflow\.2\] .* arithmetic overflow on unsigned \+ in i \+ 1u: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/regression/contracts/variant_missing_invariant_warning/test.desc b/regression/contracts/variant_missing_invariant_warning/test.desc
index 4af9a7823c3..80ca306f3c4 100644
--- a/regression/contracts/variant_missing_invariant_warning/test.desc
+++ b/regression/contracts/variant_missing_invariant_warning/test.desc
@@ -3,9 +3,10 @@ main.c
 --apply-loop-contracts
 activate-multi-line-match
 ^The loop at file main.c line 4 function main does not have an invariant.*.\nHence, a default invariant \('true'\) is being used to prove those.$
-^\[main.1\].*Check loop invariant before entry: SUCCESS$
-^\[main.2\].*Check that loop invariant is preserved: SUCCESS$
-^\[main.3\].*Check decreases clause on loop iteration: SUCCESS$
+^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main\.\d+\] .* Check decreases clause on loop iteration: SUCCESS$
+^\[main\.\d+\] .* Check that i is assignable: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/regression/contracts/variant_multidimensional_ackermann/test.desc b/regression/contracts/variant_multidimensional_ackermann/test.desc
index 9481899296e..a8e8dd2a786 100644
--- a/regression/contracts/variant_multidimensional_ackermann/test.desc
+++ b/regression/contracts/variant_multidimensional_ackermann/test.desc
@@ -1,11 +1,15 @@
 CORE
 main.c
 --apply-loop-contracts --replace-call-with-contract ackermann
-^\[precondition.1\] .* Check requires clause: SUCCESS$
-^\[precondition.2\] .* Check requires clause: SUCCESS$
-^\[ackermann.1\] .* Check loop invariant before entry: SUCCESS$
-^\[ackermann.2\] .* Check that loop invariant is preserved: SUCCESS$
-^\[ackermann.3\] .* Check decreases clause on loop iteration: SUCCESS$
+^\[precondition\.\d+\] .* line 17 Check requires clause: SUCCESS$
+^\[precondition\.\d+\] .* line 17 Check requires clause: SUCCESS$
+^\[ackermann\.\d+\] line 21 Check loop invariant before entry: SUCCESS$
+^\[ackermann\.\d+\] line 21 Check that loop invariant is preserved: SUCCESS$
+^\[ackermann\.\d+\] line 21 Check decreases clause on loop iteration: SUCCESS$
+^\[ackermann\.\d+\] line 29 Check that m is assignable: SUCCESS$
+^\[ackermann\.\d+\] line 30 Check that n is assignable: SUCCESS$
+^\[ackermann\.\d+\] line 34 Check that n is assignable: SUCCESS$
+^\[ackermann\.\d+\] line 35 Check that m is assignable: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/regression/contracts/variant_multidimensional_not_decreasing_fail1/test.desc b/regression/contracts/variant_multidimensional_not_decreasing_fail1/test.desc
index 8a5f22d5745..22c4a7531d4 100644
--- a/regression/contracts/variant_multidimensional_not_decreasing_fail1/test.desc
+++ b/regression/contracts/variant_multidimensional_not_decreasing_fail1/test.desc
@@ -1,9 +1,12 @@
 CORE
 main.c
 --apply-loop-contracts
-^\[main.1\] .* Check loop invariant before entry: SUCCESS$
-^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
-^\[main.3\] .* Check decreases clause on loop iteration: FAILURE$
+^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main\.\d+\] .* Check decreases clause on loop iteration: FAILURE$
+^\[main\.\d+\] line 14 Check that j is assignable: SUCCESS$
+^\[main\.\d+\] line 18 Check that i is assignable: SUCCESS$
+^\[main\.\d+\] line 19 Check that j is assignable: SUCCESS$
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$
diff --git a/regression/contracts/variant_multidimensional_not_decreasing_fail2/test.desc b/regression/contracts/variant_multidimensional_not_decreasing_fail2/test.desc
index 755888da300..fb7d3607739 100644
--- a/regression/contracts/variant_multidimensional_not_decreasing_fail2/test.desc
+++ b/regression/contracts/variant_multidimensional_not_decreasing_fail2/test.desc
@@ -1,9 +1,12 @@
 CORE
 main.c
 --apply-loop-contracts
-^\[main.1\] .* Check loop invariant before entry: SUCCESS$
-^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
-^\[main.3\] .* Check decreases clause on loop iteration: FAILURE$
+^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main\.\d+\] .* Check decreases clause on loop iteration: FAILURE$
+^\[main\.\d+\] line 14 Check that j is assignable: SUCCESS$
+^\[main\.\d+\] line 18 Check that i is assignable: SUCCESS$
+^\[main\.\d+\] line 19 Check that j is assignable: SUCCESS$
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$
diff --git a/regression/contracts/variant_multidimensional_two_index_variables/test.desc b/regression/contracts/variant_multidimensional_two_index_variables/test.desc
index 7f1172c952f..8a88e25eb86 100644
--- a/regression/contracts/variant_multidimensional_two_index_variables/test.desc
+++ b/regression/contracts/variant_multidimensional_two_index_variables/test.desc
@@ -1,9 +1,12 @@
 CORE
 main.c
 --apply-loop-contracts
-^\[main.1\] .* Check loop invariant before entry: SUCCESS$
-^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
-^\[main.3\] .* Check decreases clause on loop iteration: SUCCESS$
+^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main\.\d+\] .* Check decreases clause on loop iteration: SUCCESS$
+^\[main\.\d+\] line 14 Check that j is assignable: SUCCESS$
+^\[main\.\d+\] line 18 Check that i is assignable: SUCCESS$
+^\[main\.\d+\] line 19 Check that j is assignable: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/regression/contracts/variant_not_decreasing_fail/test.desc b/regression/contracts/variant_not_decreasing_fail/test.desc
index fe019a58bfb..1d3207e55f8 100644
--- a/regression/contracts/variant_not_decreasing_fail/test.desc
+++ b/regression/contracts/variant_not_decreasing_fail/test.desc
@@ -1,9 +1,10 @@
 CORE
 main.c
 --apply-loop-contracts
-^\[main.1\] .* Check loop invariant before entry: SUCCESS$
-^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
-^\[main.3\] .* Check decreases clause on loop iteration: FAILURE$
+^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main\.\d+\] .* Check decreases clause on loop iteration: FAILURE$
+^\[main\.\d+] .* Check that i is assignable: SUCCESS$
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$
diff --git a/regression/contracts/variant_weak_invariant_fail/test.desc b/regression/contracts/variant_weak_invariant_fail/test.desc
index 34be8a10621..cbb416b5bb5 100644
--- a/regression/contracts/variant_weak_invariant_fail/test.desc
+++ b/regression/contracts/variant_weak_invariant_fail/test.desc
@@ -1,9 +1,10 @@
 CORE
 main.c
 --apply-loop-contracts
-^\[main.1\] .* Check loop invariant before entry: SUCCESS$
-^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
-^\[main.3\] .* Check decreases clause on loop iteration: FAILURE$
+^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main\.\d+\] .* Check decreases clause on loop iteration: FAILURE$
+^\[main\.\d+\] .* Check that i is assignable: SUCCESS$
 ^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$
diff --git a/regression/contracts/variant_while_true_pass/test.desc b/regression/contracts/variant_while_true_pass/test.desc
index a960e9d006e..14c961f051b 100644
--- a/regression/contracts/variant_while_true_pass/test.desc
+++ b/regression/contracts/variant_while_true_pass/test.desc
@@ -1,9 +1,10 @@
 CORE
 main.c
 --apply-loop-contracts
-^\[main.1\] .* Check loop invariant before entry: SUCCESS$
-^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
-^\[main.3\] .* Check decreases clause on loop iteration: SUCCESS$
+^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main\.\d+\] .* Check decreases clause on loop iteration: SUCCESS$
+^\[main\.\d+\] .* Check that i is assignable: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp
index ad2f38f0624..325ed89226a 100644
--- a/src/goto-instrument/contracts/contracts.cpp
+++ b/src/goto-instrument/contracts/contracts.cpp
@@ -31,6 +31,7 @@ Date: February 2016
 #include <util/c_types.h>
 #include <util/expr_util.h>
 #include <util/find_symbols.h>
+#include <util/format_expr.h>
 #include <util/fresh_symbol.h>
 #include <util/graph.h>
 #include <util/mathematical_expr.h>
@@ -252,13 +253,30 @@ void code_contractst::check_apply_loop_contracts(
     loop_head,
     add_pragma_disable_assigns_check(generated_code));
 
-  // havoc the variables that may be modified
-  assignst assigns;
+  assignst to_havoc;
+
   if(assigns_clause.is_nil())
   {
+    // No assigns clause was specified for this loop.
+    // Infer memory locations assigned by the loop from the loop instructions
+    // and the inferred aliasing relation.
     try
     {
-      get_assigns(local_may_alias, loop, assigns);
+      get_assigns(local_may_alias, loop, to_havoc);
+      log.debug() << "No loop assigns clause provided. Inferred targets {";
+      // Add inferred targets to the loop assigns clause.
+      bool ran_once = false;
+      for(const auto &target : to_havoc)
+      {
+        if(ran_once)
+          log.debug() << ", ";
+        ran_once = true;
+        log.debug() << format(target);
+        loop_assigns.add_to_write_set(target);
+      }
+      log.debug()
+        << "}. Please specify an assigns clause if verification fails."
+        << messaget::eom;
     }
     catch(const analysis_exceptiont &exc)
     {
@@ -271,24 +289,29 @@ void code_contractst::check_apply_loop_contracts(
   }
   else
   {
-    assigns.insert(
+    // An assigns clause was specified for this loop.
+    // Add the targets to the set of expressions to havoc.
+    // TODO: Should we add the automatically detected local static variables
+    // too ? (they are present in loop_assigns but not in assigns_clause, and
+    // they are not necessarily touched by the loop).
+    to_havoc.insert(
       assigns_clause.operands().cbegin(), assigns_clause.operands().cend());
+  }
 
-    // Create snapshots of write set CARs.
-    // This must be done before havocing the write set.
-    for(const auto &car : loop_assigns.get_write_set())
-    {
-      auto snapshot_instructions = car.generate_snapshot_instructions();
-      insert_before_swap_and_advance(
-        goto_function.body, loop_head, snapshot_instructions);
-    };
+  // Create snapshots of write set CARs.
+  // This must be done before havocing the write set.
+  for(const auto &car : loop_assigns.get_write_set())
+  {
+    auto snapshot_instructions = car.generate_snapshot_instructions();
+    insert_before_swap_and_advance(
+      goto_function.body, loop_head, snapshot_instructions);
+  };
 
-    // Perform write set instrumentation on the entire loop.
-    check_frame_conditions(
-      function_name, goto_function.body, loop_head, loop_end, loop_assigns);
-  }
+  // Perform write set instrumentation on the entire loop.
+  check_frame_conditions(
+    function_name, goto_function.body, loop_head, loop_end, loop_assigns);
 
-  havoc_assigns_targetst havoc_gen(assigns, ns);
+  havoc_assigns_targetst havoc_gen(to_havoc, ns);
   havoc_gen.append_full_havoc_code(
     loop_head->source_location(), generated_code);