diff --git a/regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_fail/main.c b/regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_fail/main.c
index 2208c1b74c6..d033d2bf4e1 100644
--- a/regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_fail/main.c
+++ b/regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_fail/main.c
@@ -1,11 +1,11 @@
 void foo()
 {
-  int nondet_var;
-  int __VERIFIER_var;
-  int __CPROVER_var;
+  int nondet_var = nondet_int();
+  int __VERIFIER_var = nondet_int();
+  int __CPROVER_var = nondet_int();
   for(int i = 10; i > 0; i--)
     // clang-format off
-  __CPROVER_assigns(i)
+   __CPROVER_assigns(i)
   __CPROVER_loop_invariant(0 <= i && i <= 10)
   __CPROVER_decreases(i)
     // clang-format on
diff --git a/regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_pass/main.c b/regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_pass/main.c
index fa1b4a5b622..146a02bdb92 100644
--- a/regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_pass/main.c
+++ b/regression/contracts-dfcc/dont_skip_cprover_prefixed_vars_pass/main.c
@@ -1,8 +1,8 @@
 void foo()
 {
-  int nondet_var;
-  int __VERIFIER_var;
-  int __CPROVER_var;
+  int nondet_var = nondet_int();
+  int __VERIFIER_var = nondet_int();
+  int __CPROVER_var = nondet_int();
   for(int i = 10; i > 0; i--)
     // clang-format off
   __CPROVER_assigns(i,nondet_var, __VERIFIER_var, __CPROVER_var)
diff --git a/regression/contracts-dfcc/invar_assigns_opt/main.c b/regression/contracts-dfcc/invar_assigns_opt/main.c
index f58b52a7091..0d05b46b83e 100644
--- a/regression/contracts-dfcc/invar_assigns_opt/main.c
+++ b/regression/contracts-dfcc/invar_assigns_opt/main.c
@@ -17,7 +17,7 @@ int foo()
     }
   assert(r1 == 0);
 
-  int r2, s2 = 1;
+  int r2 = nondet_int(), s2 = 1;
   __CPROVER_assume(r2 >= 0);
   while(r2 > 0)
     __CPROVER_assigns(r2, s2) __CPROVER_loop_invariant(r2 >= 0 && s2 == 1)
diff --git a/regression/contracts-dfcc/invar_check_break_fail/main.c b/regression/contracts-dfcc/invar_check_break_fail/main.c
index 938877b2788..f3d7e980066 100644
--- a/regression/contracts-dfcc/invar_check_break_fail/main.c
+++ b/regression/contracts-dfcc/invar_check_break_fail/main.c
@@ -1,8 +1,6 @@
-#include <assert.h>
-
 int main()
 {
-  int r;
+  int r = nondet_int();
   __CPROVER_assume(r >= 0);
 
   while(r > 0)
diff --git a/regression/contracts-dfcc/invar_check_break_fail/test.desc b/regression/contracts-dfcc/invar_check_break_fail/test.desc
index fc631b16d94..058043e7df3 100644
--- a/regression/contracts-dfcc/invar_check_break_fail/test.desc
+++ b/regression/contracts-dfcc/invar_check_break_fail/test.desc
@@ -3,9 +3,9 @@ main.c
 --dfcc main --apply-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.loop_invariant_base.\d+\] line 8 Check invariant before entry for loop .*: SUCCESS$
-^\[main.loop_invariant_step.\d+\] line 8 Check invariant after step for loop .*: SUCCESS$
-^\[main.loop_step_unwinding.\d+\] line 8 Check step was unwound for loop .*: SUCCESS$
+^\[main.loop_invariant_base.\d+\] line 6 Check invariant before entry for loop .*: SUCCESS$
+^\[main.loop_invariant_step.\d+\] line 6 Check invariant after step for loop .*: SUCCESS$
+^\[main.loop_step_unwinding.\d+\] line 6 Check step was unwound for loop .*: SUCCESS$
 ^\[main.assigns.\d+\] .* Check that r is assignable: SUCCESS$
 ^\[main\.assertion\.\d+\] .* assertion r == 0: FAILURE$
 ^VERIFICATION FAILED$
diff --git a/regression/contracts-dfcc/invar_check_break_pass/main.c b/regression/contracts-dfcc/invar_check_break_pass/main.c
index c8eeb27e513..64962f40bb1 100644
--- a/regression/contracts-dfcc/invar_check_break_pass/main.c
+++ b/regression/contracts-dfcc/invar_check_break_pass/main.c
@@ -1,8 +1,6 @@
-#include <assert.h>
-
 int main()
 {
-  int r;
+  int r = nondet_int();
   __CPROVER_assume(r >= 0);
 
   while(r > 0)
diff --git a/regression/contracts-dfcc/invar_check_break_pass/test.desc b/regression/contracts-dfcc/invar_check_break_pass/test.desc
index 296d3790c62..7bfc153254f 100644
--- a/regression/contracts-dfcc/invar_check_break_pass/test.desc
+++ b/regression/contracts-dfcc/invar_check_break_pass/test.desc
@@ -3,10 +3,10 @@ main.c
 --dfcc main --apply-loop-contracts
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.loop_invariant_base.\d+\] line 8 Check invariant before entry for loop .*: SUCCESS$
-^\[main.loop_invariant_step.\d+\] line 8 Check invariant after step for loop .*: SUCCESS$
-^\[main.loop_step_unwinding.\d+\] line 8 Check step was unwound for loop .*: SUCCESS$
-^\[main.loop_decreases.\d+\] line 8 Check variant decreases after step for loop .*: SUCCESS$
+^\[main.loop_invariant_base.\d+\] line 6 Check invariant before entry for loop .*: SUCCESS$
+^\[main.loop_invariant_step.\d+\] line 6 Check invariant after step for loop .*: SUCCESS$
+^\[main.loop_step_unwinding.\d+\] line 6 Check step was unwound for loop .*: SUCCESS$
+^\[main.loop_decreases.\d+\] line 6 Check variant decreases after step for loop .*: SUCCESS$
 ^\[main.assigns.\d+\] .* Check that r is assignable: SUCCESS$
 ^\[main\.assertion\.\d+\] .* assertion r == 0 || r == 1: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/contracts-dfcc/invar_check_continue/main.c b/regression/contracts-dfcc/invar_check_continue/main.c
index c60b5233082..e743c201697 100644
--- a/regression/contracts-dfcc/invar_check_continue/main.c
+++ b/regression/contracts-dfcc/invar_check_continue/main.c
@@ -1,8 +1,6 @@
-#include <assert.h>
-
 int main()
 {
-  int r;
+  int r = nondet_int();
   __CPROVER_assume(r >= 0);
 
   while(r > 0)
diff --git a/regression/contracts-dfcc/invar_check_continue/test.desc b/regression/contracts-dfcc/invar_check_continue/test.desc
index d001a45151d..e4510785257 100644
--- a/regression/contracts-dfcc/invar_check_continue/test.desc
+++ b/regression/contracts-dfcc/invar_check_continue/test.desc
@@ -3,11 +3,11 @@ main.c
 --dfcc main --apply-loop-contracts
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.loop_assigns.\d+\] line 8 Check assigns clause inclusion for loop .*: SUCCESS$
-^\[main.loop_invariant_base.\d+\] line 8 Check invariant before entry for loop .*: SUCCESS$
-^\[main.loop_invariant_step.\d+\] line 8 Check invariant after step for loop .*: SUCCESS$
-^\[main.loop_step_unwinding.\d+\] line 8 Check step was unwound for loop .*: SUCCESS$
-^\[main.loop_decreases.\d+\] line 8 Check variant decreases after step for loop .*: SUCCESS$
+^\[main.loop_assigns.\d+\] line 6 Check assigns clause inclusion for loop .*: SUCCESS$
+^\[main.loop_invariant_base.\d+\] line 6 Check invariant before entry for loop .*: SUCCESS$
+^\[main.loop_invariant_step.\d+\] line 6 Check invariant after step for loop .*: SUCCESS$
+^\[main.loop_step_unwinding.\d+\] line 6 Check step was unwound for loop .*: SUCCESS$
+^\[main.loop_decreases.\d+\] line 6 Check variant decreases after step for loop .*: SUCCESS$
 ^\[main.assigns.\d+\] .* Check that r is assignable: SUCCESS$
 ^\[main\.assertion\.\d+\] .* assertion r == 0: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/contracts-dfcc/invar_check_multiple_loops/main.c b/regression/contracts-dfcc/invar_check_multiple_loops/main.c
index dea8557dd6e..a9dedee41d5 100644
--- a/regression/contracts-dfcc/invar_check_multiple_loops/main.c
+++ b/regression/contracts-dfcc/invar_check_multiple_loops/main.c
@@ -2,7 +2,7 @@
 
 int main()
 {
-  int r, n, x, y;
+  int r, n, x = nondet_int(), y = nondet_int();
   __CPROVER_assume(n > 0 && x == y);
 
   for(r = 0; r < n; ++r)
diff --git a/regression/contracts-dfcc/invar_check_nested_loops/main.c b/regression/contracts-dfcc/invar_check_nested_loops/main.c
index 8ea27e7bd99..dcd84fbae8b 100644
--- a/regression/contracts-dfcc/invar_check_nested_loops/main.c
+++ b/regression/contracts-dfcc/invar_check_nested_loops/main.c
@@ -2,7 +2,7 @@
 
 int main()
 {
-  int n, s = 0;
+  int n = nondet_int(), s = 0;
   __CPROVER_assume(n >= 0);
 
   for(int i = 0; i < n; ++i)
@@ -11,7 +11,7 @@ int main()
     __CPROVER_decreases(n - i)
     // clang-format on
     {
-      int a, b;
+      int a = nondet_int(), b = nondet_int();
       __CPROVER_assume(b >= 0 && a == b);
 
       while(a > 0)
diff --git a/regression/contracts-dfcc/invar_check_pointer_modifies-01/main.c b/regression/contracts-dfcc/invar_check_pointer_modifies-01/main.c
index c6034daab31..356a052a3bd 100644
--- a/regression/contracts-dfcc/invar_check_pointer_modifies-01/main.c
+++ b/regression/contracts-dfcc/invar_check_pointer_modifies-01/main.c
@@ -6,7 +6,7 @@ void main()
   char *data = malloc(1);
   *data = 42;
 
-  unsigned i;
+  unsigned i = nondet_int();
   while(i > 0)
     // clang-format off
     __CPROVER_loop_invariant(*data == 42)
diff --git a/regression/contracts-dfcc/invar_check_pointer_modifies-02/main.c b/regression/contracts-dfcc/invar_check_pointer_modifies-02/main.c
index 03ae679af71..de9e1fd8978 100644
--- a/regression/contracts-dfcc/invar_check_pointer_modifies-02/main.c
+++ b/regression/contracts-dfcc/invar_check_pointer_modifies-02/main.c
@@ -8,7 +8,7 @@ void main()
   copy = data;
   *data = 42;
 
-  unsigned i;
+  unsigned i = nondet_int();
   while(i > 0)
     // clang-format off
     __CPROVER_loop_invariant(*data == 42)
diff --git a/regression/contracts-dfcc/invar_check_sufficiency/main.c b/regression/contracts-dfcc/invar_check_sufficiency/main.c
index 667d3bdfd9e..2b755b5918f 100644
--- a/regression/contracts-dfcc/invar_check_sufficiency/main.c
+++ b/regression/contracts-dfcc/invar_check_sufficiency/main.c
@@ -2,7 +2,7 @@
 
 int main()
 {
-  int r;
+  int r = nondet_int();
   __CPROVER_assume(r >= 0);
 
   while(r > 0)
diff --git a/regression/contracts-dfcc/invar_loop-entry_check/main.c b/regression/contracts-dfcc/invar_loop-entry_check/main.c
index 5e8b4bb5a00..a9d2b5e3151 100644
--- a/regression/contracts-dfcc/invar_loop-entry_check/main.c
+++ b/regression/contracts-dfcc/invar_loop-entry_check/main.c
@@ -8,7 +8,7 @@ typedef struct
 
 void main()
 {
-  int *x1, y1, z1;
+  int *x1, y1 = nondet_int(), z1;
   x1 = &z1;
 
   while(y1 > 0)
@@ -20,7 +20,7 @@ void main()
     }
   assert(*x1 == z1);
 
-  int x2, y2, z2;
+  int x2, y2 = nondet_int(), z2;
   x2 = z2;
 
   while(y2 > 0)
@@ -32,8 +32,9 @@ void main()
     }
   assert(x2 == z2);
 
-  int y3;
+  int y3 = nondet_int();
   s s0, s1, *s2 = &s0;
+  s0.n = nondet_int();
   s2->n = malloc(sizeof(int));
   s1.n = s2->n;
 
diff --git a/regression/contracts-dfcc/invar_loop-entry_check/test.desc b/regression/contracts-dfcc/invar_loop-entry_check/test.desc
index 22d1c09a32a..635d418e08f 100644
--- a/regression/contracts-dfcc/invar_loop-entry_check/test.desc
+++ b/regression/contracts-dfcc/invar_loop-entry_check/test.desc
@@ -11,10 +11,10 @@ main.c
 ^\[main.loop_invariant_base.\d+] line 26 Check invariant before entry for loop .*: SUCCESS$
 ^\[main.loop_invariant_step.\d+] line 26 Check invariant after step for loop .*: SUCCESS$
 ^\[main.loop_step_unwinding.\d+] line 26 Check step was unwound for loop .*: SUCCESS$
-^\[main.loop_assigns.\d+] line 40 Check assigns clause inclusion for loop .*: SUCCESS$
-^\[main.loop_invariant_base.\d+] line 40 Check invariant before entry for loop .*: SUCCESS$
-^\[main.loop_invariant_step.\d+] line 40 Check invariant after step for loop .*: SUCCESS$
-^\[main.loop_step_unwinding.\d+] line 40 Check step was unwound for loop .*: SUCCESS$
+^\[main.loop_assigns.\d+] line 41 Check assigns clause inclusion for loop .*: SUCCESS$
+^\[main.loop_invariant_base.\d+] line 41 Check invariant before entry for loop .*: SUCCESS$
+^\[main.loop_invariant_step.\d+] line 41 Check invariant after step for loop .*: SUCCESS$
+^\[main.loop_step_unwinding.\d+] line 41 Check step was unwound for loop .*: SUCCESS$
 ^\[main\.assertion\.\d+\] .* assertion \*x1 == z1: SUCCESS$
 ^\[main\.assertion\.\d+\] .* assertion x2 == z2: SUCCESS$
 ^\[main.assigns.\d+\] .* Check that y1 is assignable: SUCCESS$
diff --git a/regression/contracts-dfcc/invar_loop-entry_fail/main.c b/regression/contracts-dfcc/invar_loop-entry_fail/main.c
index e902c8ab841..7e1f8e3baa0 100644
--- a/regression/contracts-dfcc/invar_loop-entry_fail/main.c
+++ b/regression/contracts-dfcc/invar_loop-entry_fail/main.c
@@ -2,7 +2,7 @@
 
 void main()
 {
-  int x, y, z;
+  int x = nondet_int(), y = nondet_int(), z = nondet_int();
   x = z;
 
   while(y > 0)
diff --git a/regression/contracts-dfcc/invar_loop_constant_fail/main.c b/regression/contracts-dfcc/invar_loop_constant_fail/main.c
index c2085486cb6..0891fb013a8 100644
--- a/regression/contracts-dfcc/invar_loop_constant_fail/main.c
+++ b/regression/contracts-dfcc/invar_loop_constant_fail/main.c
@@ -2,7 +2,7 @@
 
 int main()
 {
-  int r;
+  int r = nondet_int();
   int s = 1;
   __CPROVER_assume(r >= 0);
   while(r > 0)
diff --git a/regression/contracts-dfcc/invar_loop_constant_no_modify/main.c b/regression/contracts-dfcc/invar_loop_constant_no_modify/main.c
index 3b03c7777d2..e5acf175624 100644
--- a/regression/contracts-dfcc/invar_loop_constant_no_modify/main.c
+++ b/regression/contracts-dfcc/invar_loop_constant_no_modify/main.c
@@ -2,7 +2,7 @@
 
 int main()
 {
-  int r;
+  int r = nondet_int();
   int s = 1;
   __CPROVER_assume(r >= 0);
   while(r > 0)
diff --git a/regression/contracts-dfcc/invar_loop_constant_pass/main.c b/regression/contracts-dfcc/invar_loop_constant_pass/main.c
index fbb5cb3d88a..26a6c1aa5b3 100644
--- a/regression/contracts-dfcc/invar_loop_constant_pass/main.c
+++ b/regression/contracts-dfcc/invar_loop_constant_pass/main.c
@@ -2,7 +2,7 @@
 
 int main()
 {
-  int r, s = 1;
+  int r = nondet_int(), s = 1;
   __CPROVER_assume(r >= 0);
   while(r > 0)
     // clang-format off
diff --git a/regression/contracts-dfcc/loop_assigns_inference-02/main.c b/regression/contracts-dfcc/loop_assigns_inference-02/main.c
index 063b47929ee..adf6da2dec0 100644
--- a/regression/contracts-dfcc/loop_assigns_inference-02/main.c
+++ b/regression/contracts-dfcc/loop_assigns_inference-02/main.c
@@ -10,11 +10,14 @@ void main()
 void foo()
 {
   int *b = malloc(SIZE * sizeof(int));
+  int *j;
   for(unsigned i = 0; i < SIZE; i++)
     // clang-format off
     __CPROVER_loop_invariant(i <= SIZE)
     // clang-format on
     {
+      j = malloc(SIZE * sizeof(int));
       b[i] = 1;
+      free(j);
     }
 }
diff --git a/regression/contracts-dfcc/loop_assigns_inference-02/test.desc b/regression/contracts-dfcc/loop_assigns_inference-02/test.desc
index 3ac2c189a99..7c6886eef4f 100644
--- a/regression/contracts-dfcc/loop_assigns_inference-02/test.desc
+++ b/regression/contracts-dfcc/loop_assigns_inference-02/test.desc
@@ -3,12 +3,12 @@ main.c
 --no-malloc-may-fail --dfcc main --apply-loop-contracts
 ^EXIT=0$
 ^SIGNAL=0$
-^\[foo.loop_assigns.\d+\] line 13 Check assigns clause inclusion for loop .*: SUCCESS$
-^\[foo.loop_assigns.\d+\] line 13 Check assigns clause inclusion for loop .*: SUCCESS$
-^\[foo.loop_invariant_base.\d+\] line 13 Check invariant before entry for loop .*: SUCCESS$
-^\[foo.loop_invariant_base.\d+\] line 13 Check invariant before entry for loop .*: SUCCESS$
-^\[foo.loop_invariant_step.\d+\] line 13 Check invariant after step for loop .*: SUCCESS$
-^\[foo.loop_step_unwinding.\d+\] line 13 Check step was unwound for loop .*: SUCCESS$
+^\[foo.loop_assigns.\d+\] line 14 Check assigns clause inclusion for loop .*: SUCCESS$
+^\[foo.loop_assigns.\d+\] line 14 Check assigns clause inclusion for loop .*: SUCCESS$
+^\[foo.loop_invariant_base.\d+\] line 14 Check invariant before entry for loop .*: SUCCESS$
+^\[foo.loop_invariant_base.\d+\] line 14 Check invariant before entry for loop .*: SUCCESS$
+^\[foo.loop_invariant_step.\d+\] line 14 Check invariant after step for loop .*: SUCCESS$
+^\[foo.loop_step_unwinding.\d+\] line 14 Check step was unwound for loop .*: SUCCESS$
 ^\[foo.assigns.\d+\] .* Check that i is assignable: SUCCESS$
 ^\[foo.assigns.\d+\] .* Check that b\[(.*)i\] is assignable: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/contracts-dfcc/loop_assigns_inference-03/main.c b/regression/contracts-dfcc/loop_assigns_inference-03/main.c
index c969cde10a0..67f7d35bc00 100644
--- a/regression/contracts-dfcc/loop_assigns_inference-03/main.c
+++ b/regression/contracts-dfcc/loop_assigns_inference-03/main.c
@@ -12,4 +12,5 @@ void main()
     {
       b[i] = 1;
     }
+  assert(b[0] = 1);
 }
diff --git a/regression/contracts-dfcc/loop_assigns_target_base_idents/main.c b/regression/contracts-dfcc/loop_assigns_target_base_idents/main.c
index a785111100b..940eedd38a6 100644
--- a/regression/contracts-dfcc/loop_assigns_target_base_idents/main.c
+++ b/regression/contracts-dfcc/loop_assigns_target_base_idents/main.c
@@ -6,6 +6,9 @@ int foo() __CPROVER_assigns()
   char buf1[SIZE];
   char buf2[SIZE];
   char buf3[SIZE];
+  buf1[0] = 0;
+  buf2[0] = 0;
+  buf3[0] = 0;
   size_t i = 0;
   while(i < SIZE)
     // clang-format off
diff --git a/regression/contracts-dfcc/quantifiers-loop-02/main.c b/regression/contracts-dfcc/quantifiers-loop-02/main.c
index ca7b41d0ec5..c132bb1672e 100644
--- a/regression/contracts-dfcc/quantifiers-loop-02/main.c
+++ b/regression/contracts-dfcc/quantifiers-loop-02/main.c
@@ -4,6 +4,7 @@
 void main()
 {
   int N, a[MAX_ARRAY_SIZE];
+  a[0] = nondet_int();
   __CPROVER_assume(0 <= N && N < MAX_ARRAY_SIZE);
 
   for(int i = 0; i < N; ++i)
diff --git a/regression/contracts-dfcc/quantifiers-loop-02/test.desc b/regression/contracts-dfcc/quantifiers-loop-02/test.desc
index 23c3147f616..1a9501d1784 100644
--- a/regression/contracts-dfcc/quantifiers-loop-02/test.desc
+++ b/regression/contracts-dfcc/quantifiers-loop-02/test.desc
@@ -3,12 +3,12 @@ main.c
 --dfcc main --apply-loop-contracts _ --z3
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.loop_assigns.\d+\] line 9 Check assigns clause inclusion for loop .*: SUCCESS$
-^\[main.loop_assigns.\d+\] line 9 Check assigns clause inclusion for loop .*: SUCCESS$
-^\[main.loop_invariant_base.\d+\] line 9 Check invariant before entry for loop .*: SUCCESS$
-^\[main.loop_invariant_base.\d+\] line 9 Check invariant before entry for loop .*: SUCCESS$
-^\[main.loop_invariant_step.\d+\] line 9 Check invariant after step for loop .*: SUCCESS$
-^\[main.loop_step_unwinding.\d+\] line 9 Check step was unwound for loop .*: SUCCESS$
+^\[main.loop_assigns.\d+\] line 10 Check assigns clause inclusion for loop .*: SUCCESS$
+^\[main.loop_assigns.\d+\] line 10 Check assigns clause inclusion for loop .*: SUCCESS$
+^\[main.loop_invariant_base.\d+\] line 10 Check invariant before entry for loop .*: SUCCESS$
+^\[main.loop_invariant_base.\d+\] line 10 Check invariant before entry for loop .*: SUCCESS$
+^\[main.loop_invariant_step.\d+\] line 10 Check invariant after step for loop .*: SUCCESS$
+^\[main.loop_step_unwinding.\d+\] line 10 Check step was unwound for loop .*: SUCCESS$
 ^\[main.assigns.\d+\] line .* Check that i is assignable: SUCCESS$
 ^\[main.assigns.\d+\] line .* Check that a\[(\(signed (long (long )?)?int\))?i\] is assignable: SUCCESS$
 ^\[main.assertion.\d+\] line .* assertion .*: SUCCESS$
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp
index d20a80dc759..004825bee06 100644
--- a/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp
+++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_cfg_info.cpp
@@ -253,26 +253,6 @@ static bool is_assigned(dirtyt &dirty, const irep_idt &ident, assignst assigns)
   return false;
 }
 
-/// Collect identifiers that are local to this loop only
-/// (excluding nested loop).
-static std::unordered_set<irep_idt> gen_loop_locals_set(
-  const dfcc_loop_nesting_grapht &loop_nesting_graph,
-  const std::size_t loop_id)
-{
-  std::unordered_set<irep_idt> loop_locals;
-  for(const auto &target : loop_nesting_graph[loop_id].instructions)
-  {
-    auto loop_id_opt = dfcc_get_loop_id(target);
-    if(
-      target->is_decl() && loop_id_opt.has_value() &&
-      loop_id_opt.value() == loop_id)
-    {
-      loop_locals.insert(target->decl_symbol().get_identifier());
-    }
-  }
-  return loop_locals;
-}
-
 /// Compute subset of locals that must be tracked in the loop's write set.
 /// A local must be tracked if it is dirty or if it may be assigned by one
 /// of the inner loops.
@@ -329,6 +309,7 @@ static struct contract_clausest default_loop_contract_clauses(
   const dfcc_loop_nesting_grapht &loop_nesting_graph,
   const std::size_t loop_id,
   const irep_idt &function_id,
+  goto_functiont &goto_function,
   local_may_aliast &local_may_alias,
   const bool check_side_effect,
   message_handlert &message_handler,
@@ -381,7 +362,12 @@ static struct contract_clausest default_loop_contract_clauses(
     {
       // infer assigns clause targets if none given
       auto inferred = dfcc_infer_loop_assigns(
-        local_may_alias, loop.instructions, loop.head->source_location(), ns);
+        local_may_alias,
+        goto_function,
+        loop.instructions,
+        loop.head->source_location(),
+        message_handler,
+        ns);
       log.warning() << "No assigns clause provided for loop " << function_id
                     << "." << loop.latch->loop_number << " at "
                     << loop.head->source_location() << ". The inferred set {";
@@ -416,6 +402,7 @@ static dfcc_loop_infot gen_dfcc_loop_info(
   const dfcc_loop_nesting_grapht &loop_nesting_graph,
   const std::size_t loop_id,
   const irep_idt &function_id,
+  goto_functiont &goto_function,
   const std::map<std::size_t, dfcc_loop_infot> &loop_info_map,
   dirtyt &dirty,
   local_may_aliast &local_may_alias,
@@ -424,8 +411,13 @@ static dfcc_loop_infot gen_dfcc_loop_info(
   dfcc_libraryt &library,
   symbol_table_baset &symbol_table)
 {
-  std::unordered_set<irep_idt> loop_locals =
-    gen_loop_locals_set(loop_nesting_graph, loop_id);
+  const namespacet ns(symbol_table);
+  std::unordered_set<irep_idt> loop_locals = gen_loop_locals_set(
+    function_id,
+    goto_function,
+    loop_nesting_graph[loop_id].instructions,
+    message_handler,
+    ns);
 
   std::unordered_set<irep_idt> loop_tracked = gen_tracked_set(
     loop_nesting_graph.get_predecessors(loop_id),
@@ -433,11 +425,11 @@ static dfcc_loop_infot gen_dfcc_loop_info(
     dirty,
     loop_info_map);
 
-  const namespacet ns(symbol_table);
   struct contract_clausest contract_clauses = default_loop_contract_clauses(
     loop_nesting_graph,
     loop_id,
     function_id,
+    goto_function,
     local_may_alias,
     check_side_effect,
     message_handler,
@@ -559,6 +551,7 @@ dfcc_cfg_infot::dfcc_cfg_infot(
          loop_nesting_graph,
          loop_id,
          function_id,
+         goto_function,
          loop_info_map,
          dirty,
          local_may_alias,
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_infer_loop_assigns.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_infer_loop_assigns.cpp
index 611b09ffbc5..cc4025a59a4 100644
--- a/src/goto-instrument/contracts/dynamic-frames/dfcc_infer_loop_assigns.cpp
+++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_infer_loop_assigns.cpp
@@ -13,6 +13,7 @@ Author: Remi Delmas, delmasrd@amazon.com
 #include <util/pointer_expr.h>
 #include <util/std_code.h>
 
+#include <analyses/goto_rw.h>
 #include <goto-instrument/contracts/utils.h>
 #include <goto-instrument/havoc_utils.h>
 
@@ -46,10 +47,82 @@ depends_on(const exprt &expr, std::unordered_set<irep_idt> identifiers)
   return false;
 }
 
+/// Collect identifiers that are local to this loop only
+/// (excluding nested loop).
+/// A target is a loop local if
+/// 1. it is declared inside the loop, or
+/// 2. there is no write or read of it outside the loop.
+std::unordered_set<irep_idt> gen_loop_locals_set(
+  const irep_idt &function_id,
+  goto_functiont &goto_function,
+  const loopt &loop,
+  message_handlert &message_handler,
+  const namespacet &ns)
+{
+  std::unordered_set<irep_idt> loop_locals;
+  std::unordered_set<irep_idt> non_loop_locals;
+  // Ranges of all variables declared outside the loop.
+  rw_range_sett decl_rw_range_set(ns, message_handler);
+  // Ranges of all read/write outside the loop.
+  rw_range_sett non_loop_rw_range_set(ns, message_handler);
+
+  Forall_goto_program_instructions(i_it, goto_function.body)
+  {
+    // All variables declared in loops are loop locals.
+    if(i_it->is_decl() && loop.contains(i_it))
+    {
+      loop_locals.insert(i_it->decl_symbol().get_identifier());
+    }
+    // Record all other declared variables and their ranges.
+    else if(i_it->is_decl())
+    {
+      goto_rw(function_id, i_it, decl_rw_range_set);
+    }
+    // Record all writing/reading outside the loop.
+    else if(
+      (i_it->is_assign() || i_it->is_function_call()) && !loop.contains(i_it))
+    {
+      goto_rw(function_id, i_it, non_loop_rw_range_set);
+    }
+  }
+
+  // Check if declared variables are loop locals.
+  for(const auto &decl_rw : decl_rw_range_set.get_w_set())
+  {
+    bool is_loop_local = true;
+    // No write to the declared variable.
+    for(const auto &writing_rw : non_loop_rw_range_set.get_w_set())
+    {
+      if(decl_rw.first == writing_rw.first)
+      {
+        is_loop_local = false;
+        break;
+      }
+    }
+
+    // No read to the declared variable.
+    for(const auto &writing_rw : non_loop_rw_range_set.get_r_set())
+    {
+      if(decl_rw.first == writing_rw.first)
+      {
+        is_loop_local = false;
+        break;
+      }
+    }
+
+    if(is_loop_local)
+      loop_locals.insert(decl_rw.first);
+  }
+
+  return loop_locals;
+}
+
 assignst dfcc_infer_loop_assigns(
   const local_may_aliast &local_may_alias,
+  goto_functiont &goto_function,
   const loopt &loop_instructions,
   const source_locationt &loop_head_location,
+  message_handlert &message_handler,
   const namespacet &ns)
 {
   // infer
@@ -57,7 +130,8 @@ assignst dfcc_infer_loop_assigns(
   infer_loop_assigns(local_may_alias, loop_instructions, assigns);
 
   // compute locals
-  std::unordered_set<irep_idt> loop_locals;
+  std::unordered_set<irep_idt> loop_locals = gen_loop_locals_set(
+    irep_idt(), goto_function, loop_instructions, message_handler, ns);
   for(const auto &target : loop_instructions)
   {
     if(target->is_decl())
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_infer_loop_assigns.h b/src/goto-instrument/contracts/dynamic-frames/dfcc_infer_loop_assigns.h
index ac773869009..670904bc9e3 100644
--- a/src/goto-instrument/contracts/dynamic-frames/dfcc_infer_loop_assigns.h
+++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_infer_loop_assigns.h
@@ -17,13 +17,25 @@ Author: Remi Delmas, delmasrd@amazon.com
 class source_locationt;
 class messaget;
 class namespacet;
+class message_handlert;
 
 // \brief Infer assigns clause targets for a loop from its instructions and a
 // may alias analysis at the function level.
 assignst dfcc_infer_loop_assigns(
   const local_may_aliast &local_may_alias,
+  goto_functiont &goto_function,
   const loopt &loop_instructions,
   const source_locationt &loop_head_location,
+  message_handlert &message_handler,
+  const namespacet &ns);
+
+/// Collect identifiers that are local to this loop only
+/// (excluding nested loop).
+std::unordered_set<irep_idt> gen_loop_locals_set(
+  const irep_idt &function_id,
+  goto_functiont &goto_function,
+  const loopt &loop,
+  message_handlert &message_handler,
   const namespacet &ns);
 
 #endif
diff --git a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp
index 7f6acd75e7f..4d896a5d0cc 100644
--- a/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp
+++ b/src/goto-instrument/contracts/dynamic-frames/dfcc_instrument_loop.cpp
@@ -298,6 +298,13 @@ dfcc_instrument_loopt::add_prehead_instructions(
     code_function_callt call = library.write_set_create_call(
       addr_of_loop_write_set,
       from_integer(assigns.size(), size_type()),
+      from_integer(0, size_type()),
+      false_exprt(),
+      false_exprt(),
+      false_exprt(),
+      false_exprt(),
+      true_exprt(),
+      true_exprt(),
       loop_head_location);
     pre_loop_head_instrs.add(
       goto_programt::make_function_call(call, loop_head_location));