diff --git a/regression/contracts/assigns_enforce_04/test.desc b/regression/contracts/assigns_enforce_04/test.desc
index b1a24463b4d..2e1caa26893 100644
--- a/regression/contracts/assigns_enforce_04/test.desc
+++ b/regression/contracts/assigns_enforce_04/test.desc
@@ -3,12 +3,6 @@ main.c
 --enforce-contract f1
 ^EXIT=0$
 ^SIGNAL=0$
-^\[f1.\d+\] line \d+ Check that x2 is assignable: SUCCESS$
-^\[f1.\d+\] line \d+ Check that y2 is assignable: SUCCESS$
-^\[f1.\d+\] line \d+ Check that z2 is assignable: SUCCESS$
-^\[f2.\d+\] line \d+ Check that x3 is assignable: SUCCESS$
-^\[f2.\d+\] line \d+ Check that y3 is assignable: SUCCESS$
-^\[f2.\d+\] line \d+ Check that z3 is assignable: SUCCESS$
 ^\[f3.\d+\] line \d+ Check that \*x3 is assignable: SUCCESS$
 ^\[f3.\d+\] line \d+ Check that \*y3 is assignable: SUCCESS$
 ^\[f3.\d+\] line \d+ Check that \*z3 is assignable: SUCCESS$
diff --git a/regression/contracts/assigns_enforce_05/test.desc b/regression/contracts/assigns_enforce_05/test.desc
index 6c7363f88d0..97352a948f2 100644
--- a/regression/contracts/assigns_enforce_05/test.desc
+++ b/regression/contracts/assigns_enforce_05/test.desc
@@ -3,7 +3,6 @@ main.c
 --enforce-contract f1 --enforce-contract f2 --enforce-contract f3
 ^EXIT=0$
 ^SIGNAL=0$
-^\[f1.1\] line \d+ .*: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 --
diff --git a/regression/contracts/assigns_enforce_18/test.desc b/regression/contracts/assigns_enforce_18/test.desc
index 011006f19c6..74c8ac7a49b 100644
--- a/regression/contracts/assigns_enforce_18/test.desc
+++ b/regression/contracts/assigns_enforce_18/test.desc
@@ -7,9 +7,6 @@ main.c
 ^\[bar.\d+\] line \d+ Check that \*b is assignable: SUCCESS$
 ^\[baz.\d+\] line \d+ Check that POINTER_OBJECT\(\(void \*\)c\) is assignable: FAILURE$
 ^\[baz.\d+\] line \d+ Check that \*a is assignable: SUCCESS$
-^\[foo.\d+\] line \d+ Check that a is assignable: SUCCESS$
-^\[foo.\d+\] line \d+ Check that yp is assignable: SUCCESS$
-^\[foo.\d+\] line \d+ Check that z is assignable: SUCCESS$
 ^\[foo.\d+\] line \d+ Check that \*xp is assignable: SUCCESS$
 ^\[foo.\d+\] line \d+ Check that y is assignable: FAILURE$
 ^\[foo.\d+\] line \d+ Check that POINTER_OBJECT\(\(void \*\)yp\) is assignable: SUCCESS$
diff --git a/regression/contracts/assigns_enforce_21/test.desc b/regression/contracts/assigns_enforce_21/test.desc
index 7b629e00d6f..7e2b828b342 100644
--- a/regression/contracts/assigns_enforce_21/test.desc
+++ b/regression/contracts/assigns_enforce_21/test.desc
@@ -6,9 +6,6 @@ main.c
 main.c function bar
 ^\[bar.\d+\] line \d+ Check that \*y is assignable: SUCCESS$
 ^\[bar.\d+\] line \d+ Check that x is assignable: FAILURE$
-^\[baz.\d+\] line \d+ Check that w is assignable: SUCCESS$
-^\[foo.\d+\] line \d+ Check that w is assignable: SUCCESS$
-^\[foo.\d+\] line \d+ Check that z is assignable: SUCCESS$
 ^VERIFICATION FAILED$
 --
 --
diff --git a/regression/contracts/assigns_enforce_arrays_01/main.c b/regression/contracts/assigns_enforce_arrays_01/main.c
index bf793de2da6..ee8405c3ce4 100644
--- a/regression/contracts/assigns_enforce_arrays_01/main.c
+++ b/regression/contracts/assigns_enforce_arrays_01/main.c
@@ -1,4 +1,4 @@
-void f1(int a[], int len) __CPROVER_assigns(a)
+void f1(int a[], int len) __CPROVER_assigns()
 {
   int b[10];
   a = b;
diff --git a/regression/contracts/assigns_enforce_arrays_03/main.c b/regression/contracts/assigns_enforce_arrays_03/main.c
index 9a51b358f75..2511fbe4103 100644
--- a/regression/contracts/assigns_enforce_arrays_03/main.c
+++ b/regression/contracts/assigns_enforce_arrays_03/main.c
@@ -1,4 +1,4 @@
-void assign_out_under(int a[], int len) __CPROVER_assigns(a)
+void assign_out_under(int a[], int len) __CPROVER_assigns()
 {
   a[1] = 5;
 }
diff --git a/regression/contracts/assigns_enforce_arrays_03/test.desc b/regression/contracts/assigns_enforce_arrays_03/test.desc
index f8f7fe4b375..f6e98f0b4aa 100644
--- a/regression/contracts/assigns_enforce_arrays_03/test.desc
+++ b/regression/contracts/assigns_enforce_arrays_03/test.desc
@@ -6,5 +6,6 @@ main.c
 ^VERIFICATION FAILED$
 --
 --
-Checks whether verification fails when an assigns clause contains pointer,
-but function only modifies its content.
+Checks whether verification fails when a function has an array 
+as parameter, an empty assigns clause and attempts to modify the object
+pointed to by the pointer.
diff --git a/regression/contracts/assigns_enforce_arrays_04/main.c b/regression/contracts/assigns_enforce_arrays_04/main.c
index 6e51934a449..bf4d22fa028 100644
--- a/regression/contracts/assigns_enforce_arrays_04/main.c
+++ b/regression/contracts/assigns_enforce_arrays_04/main.c
@@ -1,21 +1,20 @@
-void assigns_single(int a[], int len) __CPROVER_assigns(a)
+void assigns_single(int a[], int len)
 {
+  int i;
+  __CPROVER_assume(0 <= i && i < len);
+  a[i] = 0;
 }
 
-void assigns_range(int a[], int len) __CPROVER_assigns(a)
-{
-}
-
-void assigns_big_range(int a[], int len) __CPROVER_assigns(a)
+void uses_assigns(int a[], int len)
+  __CPROVER_assigns(__CPROVER_POINTER_OBJECT(a))
 {
   assigns_single(a, len);
-  assigns_range(a, len);
 }
 
 int main()
 {
   int arr[10];
-  assigns_big_range(arr, 10);
+  uses_assigns(arr, 10);
 
   return 0;
 }
diff --git a/regression/contracts/assigns_enforce_arrays_04/test.desc b/regression/contracts/assigns_enforce_arrays_04/test.desc
index e59988d65d7..e2dd274fa7d 100644
--- a/regression/contracts/assigns_enforce_arrays_04/test.desc
+++ b/regression/contracts/assigns_enforce_arrays_04/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-contract assigns_single --enforce-contract assigns_range --enforce-contract assigns_big_range
+--enforce-contract uses_assigns
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/contracts/assigns_enforce_arrays_05/main.c b/regression/contracts/assigns_enforce_arrays_05/main.c
index 4eade02f201..01ec9cf6b98 100644
--- a/regression/contracts/assigns_enforce_arrays_05/main.c
+++ b/regression/contracts/assigns_enforce_arrays_05/main.c
@@ -1,18 +1,23 @@
-void assigns_ptr(int *x) __CPROVER_assigns(*x)
+void assigns_ptr(int *x)
 {
   *x = 200;
 }
 
-void assigns_range(int a[], int len) __CPROVER_assigns(a)
+void uses_assigns(int a[], int i, int len)
+  // clang-format off
+ __CPROVER_requires(0 <= i && i < len)
+  __CPROVER_assigns(*(&a[i]))
+// clang-format on
 {
-  int *ptr = &(a[7]);
+  int *ptr = &(a[i]);
   assigns_ptr(ptr);
 }
 
 int main()
 {
   int arr[10];
-  assigns_range(arr, 10);
-
+  int i;
+  __CPROVER_assume(0 <= i && i < 10);
+  uses_assigns(arr, i, 10);
   return 0;
 }
diff --git a/regression/contracts/assigns_enforce_arrays_05/test.desc b/regression/contracts/assigns_enforce_arrays_05/test.desc
index 4fe133f4914..019d4770188 100644
--- a/regression/contracts/assigns_enforce_arrays_05/test.desc
+++ b/regression/contracts/assigns_enforce_arrays_05/test.desc
@@ -1,11 +1,10 @@
 CORE
 main.c
---enforce-contract assigns_range
-^EXIT=10$
+--enforce-contract uses_assigns
+^EXIT=0$
 ^SIGNAL=0$
-^VERIFICATION FAILED$
+^\[assigns_ptr\.\d+\] line \d+ Check that \*x is assignable: SUCCESS$
+^VERIFICATION SUCCESSFUL$
 --
 --
-Checks whether verification fails when an assigns clause of a function
-indicates the pointer might change, but one of its internal function only
-modified its content.
+Checks whether verification succeeds for array elements at a symbolic index. 
diff --git a/regression/contracts/assigns_enforce_detect_local_statics/test.desc b/regression/contracts/assigns_enforce_detect_local_statics/test.desc
index 9b0ea3f8b69..e0309d9fc9d 100644
--- a/regression/contracts/assigns_enforce_detect_local_statics/test.desc
+++ b/regression/contracts/assigns_enforce_detect_local_statics/test.desc
@@ -1,13 +1,12 @@
 CORE
 main.c
 --enforce-contract bar
+^\[foo.\d+\] line 14 Check that foo\$\$1\$\$x is assignable: SUCCESS
+^\[foo.\d+\] line 17 Check that \*y is assignable: SUCCESS
+^\[foo.\d+\] line 20 Check that \*yy is assignable: FAILURE
+^VERIFICATION FAILED$
 ^EXIT=10$
 ^SIGNAL=0$
-^\[foo.\d+\] line \d+ Check that y is assignable: SUCCESS$
-^\[foo.\d+\] line \d+ Check that foo\$\$1\$\$x is assignable: SUCCESS$
-^\[foo.\d+\] line \d+ Check that \*y is assignable: SUCCESS$
-^\[foo.\d+\] line \d+ Check that \*yy is assignable: FAILURE$
-^VERIFICATION FAILED$
 --
 --
 Checks whether static local and global variables are correctly tracked
diff --git a/regression/contracts/assigns_enforce_free_dead/test.desc b/regression/contracts/assigns_enforce_free_dead/test.desc
index 616e2b670ab..b4cee3c92a3 100644
--- a/regression/contracts/assigns_enforce_free_dead/test.desc
+++ b/regression/contracts/assigns_enforce_free_dead/test.desc
@@ -7,12 +7,6 @@ main.c
 ^\[foo.\d+\] line \d+ Check that \*q is assignable: SUCCESS$
 ^\[foo.\d+\] line \d+ Check that \*w is assignable: SUCCESS$
 ^\[foo.\d+\] line \d+ Check that \*x is assignable: SUCCESS$
-^\[foo.\d+\] line \d+ Check that a is assignable: SUCCESS$
-^\[foo.\d+\] line \d+ Check that q is assignable: SUCCESS$
-^\[foo.\d+\] line \d+ Check that w is assignable: SUCCESS$
-^\[foo.\d+\] line \d+ Check that x is assignable: SUCCESS$
-^\[foo.\d+\] line \d+ Check that y is assignable: SUCCESS$
-^\[foo.\d+\] line \d+ Check that z is assignable: SUCCESS$
 ^\[foo.\d+\] line \d+ Check that POINTER_OBJECT\(\(void \*\)z\) is assignable: SUCCESS$
 ^EXIT=10$
 ^SIGNAL=0$
@@ -22,16 +16,7 @@ main.c
 ^\[foo.\d+\] line \d+ Check that \*q is assignable: FAILURE$
 ^\[foo.\d+\] line \d+ Check that \*w is assignable: FAILURE$
 ^\[foo.\d+\] line \d+ Check that \*x is assignable: FAILURE$
-^\[foo.\d+\] line \d+ Check that a is assignable: FAILURE$
-^\[foo.\d+\] line \d+ Check that q is assignable: FAILURE$
-^\[foo.\d+\] line \d+ Check that w is assignable: FAILURE$
-^\[foo.\d+\] line \d+ Check that x is assignable: FAILURE$
-^\[foo.\d+\] line \d+ Check that y is assignable: FAILURE$
-^\[foo.\d+\] line \d+ Check that z is assignable: FAILURE$
 ^\[foo.\d+\] line \d+ Check that POINTER_OBJECT\(\(void \*\)z\) is assignable: FAILURE$
-^.*__car_valid.*: FAILURE$
-^.*__car_lb.*: FAILURE$
-^.*__car_ub.*: FAILURE$
 --
 Checks that invalidated CARs are correctly tracked on `free` and `DEAD`.
 
@@ -40,6 +25,3 @@ we rule out all failures using the negative regex matches above.
 
 We also check (using positive regex matches above) that
 `**p` should be assignable in one case and should not be assignable in the other.
-
-Finally, we check that there should be no "internal" assertion failures
-on `__car_valid`, `__car_ub`, `__car_lb` variables used to track CARs.
diff --git a/regression/contracts/assigns_enforce_malloc_01/main.c b/regression/contracts/assigns_enforce_malloc_01/main.c
index c02eca20a2a..7896a93b158 100644
--- a/regression/contracts/assigns_enforce_malloc_01/main.c
+++ b/regression/contracts/assigns_enforce_malloc_01/main.c
@@ -1,16 +1,15 @@
 #include <stdlib.h>
 
-int f1(int *a, int *b) __CPROVER_assigns(*a, b)
+int f(int *a) __CPROVER_assigns()
 {
-  b = (int *)malloc(sizeof(int));
-  *b = 5;
+  a = (int *)malloc(sizeof(int));
+  *a = 5;
 }
 
 int main()
 {
   int m = 4;
-  int n = 3;
-  f1(&m, &n);
+  f(&m);
 
   return 0;
 }
diff --git a/regression/contracts/assigns_enforce_malloc_01/test.desc b/regression/contracts/assigns_enforce_malloc_01/test.desc
index 7b71dc6b088..0ee889a7b2b 100644
--- a/regression/contracts/assigns_enforce_malloc_01/test.desc
+++ b/regression/contracts/assigns_enforce_malloc_01/test.desc
@@ -1,9 +1,12 @@
 CORE
 main.c
---enforce-contract f1
+--enforce-contract f
 ^EXIT=0$
 ^SIGNAL=0$
+^\[f\.\d+\] line \d+ Check that \*a is assignable: SUCCESS
 ^VERIFICATION SUCCESSFUL$
 --
 --
-This test checks that verification succeeds when a formal parameter pointer outside of the assigns clause is instead pointed as freshly allocated memory before being assigned.
+This test checks that verification succeeds when a formal parameter
+with a pointer type is first updated to point to a locally malloc'd object
+before being assigned to.
diff --git a/regression/contracts/assigns_enforce_malloc_02/test.desc b/regression/contracts/assigns_enforce_malloc_02/test.desc
index 5cf7b48e5a7..49f5f99a59d 100644
--- a/regression/contracts/assigns_enforce_malloc_02/test.desc
+++ b/regression/contracts/assigns_enforce_malloc_02/test.desc
@@ -1,9 +1,11 @@
 CORE
 main.c
 --enforce-contract f1
-^EXIT=6$
+^Invariant check failed$
+^Condition: is_loop_free
+^Reason: Loops remain in function 'f1', assigns clause checking instrumentation cannot be applied\.
+^EXIT=(127|134)$
 ^SIGNAL=0$
-Unable to complete instrumentation, as this malloc may be in a loop.$
 --
 --
 This test checks that an error is thrown when malloc is called within a loop.
diff --git a/regression/contracts/assigns_enforce_multi_file_02/header.h b/regression/contracts/assigns_enforce_multi_file_02/header.h
index e07691ac68a..267565a2ed5 100644
--- a/regression/contracts/assigns_enforce_multi_file_02/header.h
+++ b/regression/contracts/assigns_enforce_multi_file_02/header.h
@@ -14,7 +14,7 @@ struct pair_of_pairs
 
 int f1(int *a, struct pair *b);
 
-int f1(int *a, struct pair *b) __CPROVER_assigns(*a, b)
+int f1(int *a, struct pair *b) __CPROVER_assigns(*a)
 {
   struct pair_of_pairs *pop =
     (struct pair_of_pairs *)malloc(sizeof(struct pair_of_pairs));
diff --git a/regression/contracts/assigns_enforce_multi_file_02/test.desc b/regression/contracts/assigns_enforce_multi_file_02/test.desc
index 6020c479abb..dd02559f652 100644
--- a/regression/contracts/assigns_enforce_multi_file_02/test.desc
+++ b/regression/contracts/assigns_enforce_multi_file_02/test.desc
@@ -3,6 +3,7 @@ main.c
 --enforce-contract f1
 ^EXIT=0$
 ^SIGNAL=0$
+^\[f1\.\d+\] line \d+ Check that b->y is assignable: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 --
diff --git a/regression/contracts/assigns_enforce_statics/test.desc b/regression/contracts/assigns_enforce_statics/test.desc
index 269b088542b..fee67eaefaa 100644
--- a/regression/contracts/assigns_enforce_statics/test.desc
+++ b/regression/contracts/assigns_enforce_statics/test.desc
@@ -3,7 +3,6 @@ main.c
 --enforce-contract foo _ --pointer-primitive-check
 ^EXIT=0$
 ^SIGNAL=0$
-^\[foo.\d+\] line \d+ Check that y is assignable: SUCCESS$
 ^\[foo.\d+\] line \d+ Check that foo\$\$1\$\$x is assignable: SUCCESS$
 ^\[foo.\d+\] line \d+ Check that \*y is assignable: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/contracts/assigns_enforce_structs_01/main.c b/regression/contracts/assigns_enforce_structs_01/main.c
index c44f786ef44..ee4a59c2b1f 100644
--- a/regression/contracts/assigns_enforce_structs_01/main.c
+++ b/regression/contracts/assigns_enforce_structs_01/main.c
@@ -6,18 +6,17 @@ struct pair
   int y;
 };
 
-int f1(int *a, int *b) __CPROVER_assigns(*a, b)
+int f(int *a) __CPROVER_assigns()
 {
   struct pair *p = (struct pair *)malloc(sizeof(struct pair));
-  b = &(p->y);
-  *b = 5;
+  a = &(p->y);
+  *a = 5;
 }
 
 int main()
 {
   int m = 4;
-  int n = 3;
-  f1(&m, &n);
+  f(&m);
 
   return 0;
 }
diff --git a/regression/contracts/assigns_enforce_structs_01/test.desc b/regression/contracts/assigns_enforce_structs_01/test.desc
index 00a255be860..0d77a423c99 100644
--- a/regression/contracts/assigns_enforce_structs_01/test.desc
+++ b/regression/contracts/assigns_enforce_structs_01/test.desc
@@ -1,11 +1,12 @@
 CORE
 main.c
---enforce-contract f1
+--enforce-contract f
 ^EXIT=0$
 ^SIGNAL=0$
+^\[f\.\d+\] line \d+ Check that \*a is assignable: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 --
-Checks whether verification succeeds when a formal parameter pointer outside
-of the assigns clause is instead pointed at the location of a member of a
-freshly allocated struct before being assigned.
+Checks whether verification succeeds when a pointer deref that is not
+specified in the assigns clause is first pointed at a member of a
+locally malloc'd struct before being assigned.
diff --git a/regression/contracts/assigns_enforce_structs_02/main.c b/regression/contracts/assigns_enforce_structs_02/main.c
index 4d909f19131..fd544aa9148 100644
--- a/regression/contracts/assigns_enforce_structs_02/main.c
+++ b/regression/contracts/assigns_enforce_structs_02/main.c
@@ -12,19 +12,18 @@ struct pair_of_pairs
   struct pair p2;
 };
 
-int f1(int *a, int *b) __CPROVER_assigns(*a, b)
+int f(int *a) __CPROVER_assigns()
 {
   struct pair_of_pairs *pop =
     (struct pair_of_pairs *)malloc(sizeof(struct pair_of_pairs));
-  b = &(pop->p2.x);
-  *b = 5;
+  a = &(pop->p2.x);
+  *a = 5;
 }
 
 int main()
 {
   int m = 4;
-  int n = 3;
-  f1(&m, &n);
+  f(&m);
 
   return 0;
 }
diff --git a/regression/contracts/assigns_enforce_structs_02/test.desc b/regression/contracts/assigns_enforce_structs_02/test.desc
index 5d72b1c2f13..fc0948b1676 100644
--- a/regression/contracts/assigns_enforce_structs_02/test.desc
+++ b/regression/contracts/assigns_enforce_structs_02/test.desc
@@ -1,13 +1,12 @@
 CORE
 main.c
---enforce-contract f1
+--enforce-contract f
 ^EXIT=0$
 ^SIGNAL=0$
+^\[f\.\d+\] line \d+ Check that \*a is assignable: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 --
-Checks whether verification succeeds when a formal parameter pointer outside
-of the assigns clause is assigned after being pointed at the location of a
-member of a sub-struct of a freshly allocated struct before being assigned.
-This is meant to show that all contained members (and their contained members)
-of assignable structs are valid to assign.
+Checks whether verification succeeds when a pointer deref that is not
+specified in the assigns clause is first pointed at a member of a locally
+malloc'd struct before being assigned (with extra nesting).
diff --git a/regression/contracts/assigns_enforce_structs_03/main.c b/regression/contracts/assigns_enforce_structs_03/main.c
index 2ecfd58997d..a4d282edc25 100644
--- a/regression/contracts/assigns_enforce_structs_03/main.c
+++ b/regression/contracts/assigns_enforce_structs_03/main.c
@@ -12,19 +12,18 @@ struct pair_of_pairs
   struct pair p2;
 };
 
-int f1(int *a, struct pair *b) __CPROVER_assigns(*a, b)
+int f(struct pair *a) __CPROVER_assigns()
 {
   struct pair_of_pairs *pop =
     (struct pair_of_pairs *)malloc(sizeof(struct pair_of_pairs));
-  b = &(pop->p2);
-  b->y = 5;
+  a = &(pop->p2);
+  a->y = 5;
 }
 
 int main()
 {
-  int m = 4;
-  struct pair n;
-  f1(&m, &n);
+  struct pair m;
+  f(&m);
 
   return 0;
 }
diff --git a/regression/contracts/assigns_enforce_structs_03/test.desc b/regression/contracts/assigns_enforce_structs_03/test.desc
index f8ab3d39c45..0d57241131b 100644
--- a/regression/contracts/assigns_enforce_structs_03/test.desc
+++ b/regression/contracts/assigns_enforce_structs_03/test.desc
@@ -1,6 +1,6 @@
 CORE
 main.c
---enforce-contract f1
+--enforce-contract f
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
diff --git a/regression/contracts/assigns_enforce_structs_04/test.desc b/regression/contracts/assigns_enforce_structs_04/test.desc
index 24300267705..3de0bffb9ca 100644
--- a/regression/contracts/assigns_enforce_structs_04/test.desc
+++ b/regression/contracts/assigns_enforce_structs_04/test.desc
@@ -6,7 +6,6 @@ main.c
 ^\[f1.\d+\] line \d+ Check that p->y is assignable: FAILURE$
 ^\[f2.\d+\] line \d+ Check that p->x is assignable: FAILURE$
 ^\[f3.\d+\] line \d+ Check that p->y is assignable: SUCCESS$
-^\[f4.\d+\] line \d+ Check that p is assignable: SUCCESS$
 ^VERIFICATION FAILED$
 --
 --
diff --git a/regression/contracts/assigns_enforce_subfunction_calls/test.desc b/regression/contracts/assigns_enforce_subfunction_calls/test.desc
index c4ffcabe76d..9411d1e4536 100644
--- a/regression/contracts/assigns_enforce_subfunction_calls/test.desc
+++ b/regression/contracts/assigns_enforce_subfunction_calls/test.desc
@@ -3,28 +3,15 @@ main.c
 --enforce-contract foo
 ^EXIT=10$
 ^SIGNAL=0$
-^main.c function bar$
-^\[bar.1\] line \d+ Check that x is assignable: SUCCESS$
-^\[bar.2\] line \d+ Check that y is assignable: SUCCESS$
-^\[bar.3\] line \d+ Check that x is assignable: SUCCESS$
-^\[bar.4\] line \d+ Check that y is assignable: SUCCESS$
 ^main.c function baz$
 ^\[baz.1\] line \d+ Check that \*x is assignable: SUCCESS$
 ^\[baz.2\] line \d+ Check that \*x is assignable: SUCCESS$
 ^\[baz.3\] line \d+ Check that \*x is assignable: FAILURE$
 ^\[baz.4\] line \d+ Check that \*x is assignable: FAILURE$
 ^main.c function foo$
-^\[foo.1\] line \d+ Check that x is assignable: SUCCESS$
-^\[foo.2\] line \d+ Check that y is assignable: SUCCESS$
 ^\[foo.assertion.1\] line \d+ foo.x.set: SUCCESS$
-^\[foo.3\] line \d+ Check that x is assignable: SUCCESS$
-^\[foo.4\] line \d+ Check that y is assignable: SUCCESS$
 ^\[foo.assertion.2\] line \d+ foo.local.set: SUCCESS$
-^\[foo.5\] line \d+ Check that x is assignable: SUCCESS$
-^\[foo.6\] line \d+ Check that y is assignable: SUCCESS$
 ^\[foo.assertion.3\] line \d+ foo.y.set: SUCCESS$
-^\[foo.7\] line \d+ Check that x is assignable: SUCCESS$
-^\[foo.8\] line \d+ Check that y is assignable: SUCCESS$
 ^\[foo.assertion.4\] line \d+ foo.z.set: SUCCESS$
 ^VERIFICATION FAILED$
 --
diff --git a/regression/contracts/assigns_function_pointer/main.c b/regression/contracts/assigns_function_pointer/main.c
index 26bb484468a..f3d27e97713 100644
--- a/regression/contracts/assigns_function_pointer/main.c
+++ b/regression/contracts/assigns_function_pointer/main.c
@@ -3,22 +3,36 @@
 
 int x = 0;
 
+struct fptr_t
+{
+  void (*f)();
+};
+
 void foo()
 {
   x = 1;
 }
 
-void bar(void (*fun_ptr)()) __CPROVER_assigns(fun_ptr)
+void foofoo()
+{
+  x = 2;
+}
+
+void bar(struct fptr_t *s, void (**f)()) __CPROVER_assigns(s->f, *f)
 {
-  fun_ptr = &foo;
+  s->f = &foo;
+  *f = &foofoo;
 }
 
 int main()
 {
   assert(x == 0);
-  void (*fun_ptr)() = NULL;
-  bar(fun_ptr);
-  fun_ptr();
+  struct fptr_t s;
+  void (*f)();
+  bar(&s, &f);
+  s.f();
   assert(x == 1);
+  f();
+  assert(x == 2);
   return 0;
 }
diff --git a/regression/contracts/assigns_function_pointer/test.desc b/regression/contracts/assigns_function_pointer/test.desc
index 4795e9d620b..f5d4a7d36b8 100644
--- a/regression/contracts/assigns_function_pointer/test.desc
+++ b/regression/contracts/assigns_function_pointer/test.desc
@@ -3,9 +3,12 @@ main.c
 --enforce-contract bar
 ^EXIT=0$
 ^SIGNAL=0$
-^\[bar.1\] line \d+ Check that fun\_ptr is assignable: SUCCESS$
 ^\[main.assertion.\d+\] line \d+ assertion x \=\= 0: SUCCESS$
+^\[bar\.\d+\] line \d+ Check that s->f is assignable: SUCCESS$
+^\[bar\.\d+\] line \d+ Check that \*f is assignable: SUCCESS$
 ^\[main.assertion.\d+\] line \d+ assertion x \=\= 1: SUCCESS$
+^\[main.assertion.\d+\] line \d+ assertion x \=\= 2: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
-Checks whether assigns clause accepts function pointers.
+Checks whether assigns clause accepts function pointers
+and pointers to function pointers.
diff --git a/regression/contracts/assigns_type_checking_valid_cases/main.c b/regression/contracts/assigns_type_checking_valid_cases/main.c
index 69062b90dc4..f1381d555e4 100644
--- a/regression/contracts/assigns_type_checking_valid_cases/main.c
+++ b/regression/contracts/assigns_type_checking_valid_cases/main.c
@@ -14,17 +14,17 @@ struct buf
   struct blob aux;
 };
 
-void foo1(int a) __CPROVER_assigns(a)
+void foo1(int a) __CPROVER_assigns()
 {
   a = 0;
 }
 
-void foo2(int *b) __CPROVER_assigns(b)
+void foo2(int *b) __CPROVER_assigns()
 {
   b = NULL;
 }
 
-void foo3(int a, int *b) __CPROVER_assigns(b, x, y)
+void foo3(int a, int *b) __CPROVER_assigns(x, y)
 {
   b = NULL;
   x = malloc(sizeof(*x));
@@ -32,14 +32,14 @@ void foo3(int a, int *b) __CPROVER_assigns(b, x, y)
 }
 
 void foo4(int a, int *b, int *c) __CPROVER_requires(c != NULL)
-  __CPROVER_requires(x != NULL) __CPROVER_assigns(b, *c, *x)
+  __CPROVER_requires(x != NULL) __CPROVER_assigns(*c, *x)
 {
   b = NULL;
   *c = 0;
   *x = 0;
 }
 
-void foo5(struct buf buffer) __CPROVER_assigns(buffer)
+void foo5(struct buf buffer) __CPROVER_assigns()
 {
   buffer.data = NULL;
   buffer.len = 0;
@@ -73,7 +73,7 @@ void foo8(int array[]) __CPROVER_assigns(__CPROVER_POINTER_OBJECT(array))
   array[9] = 1;
 }
 
-void foo9(int array[]) __CPROVER_assigns(array)
+void foo9(int array[]) __CPROVER_assigns()
 {
   int *new_array = NULL;
   array = new_array;
diff --git a/regression/contracts/assigns_type_checking_valid_cases/test.desc b/regression/contracts/assigns_type_checking_valid_cases/test.desc
index e7c22c65b59..1592a4973c2 100644
--- a/regression/contracts/assigns_type_checking_valid_cases/test.desc
+++ b/regression/contracts/assigns_type_checking_valid_cases/test.desc
@@ -3,13 +3,9 @@ main.c
 --enforce-contract foo1 --enforce-contract foo2 --enforce-contract foo3 --enforce-contract foo4 --enforce-contract foo5 --enforce-contract foo6 --enforce-contract foo7 --enforce-contract foo8 --enforce-contract foo9 --enforce-contract foo10 _ --pointer-primitive-check
 ^EXIT=0$
 ^SIGNAL=0$
-^\[foo1.\d+\] line \d+ Check that a is assignable: SUCCESS$
 ^\[foo10.\d+\] line \d+ Check that buffer->len is assignable: SUCCESS$
 ^\[foo10.\d+\] line \d+ Check that buffer->aux\.allocated is assignable: SUCCESS$
-^\[foo2.\d+\] line \d+ Check that b is assignable: SUCCESS$
-^\[foo3.\d+\] line \d+ Check that b is assignable: SUCCESS$
 ^\[foo3.\d+\] line \d+ Check that y is assignable: SUCCESS$
-^\[foo4.\d+\] line \d+ Check that b is assignable: SUCCESS$
 ^\[foo4.\d+\] line \d+ Check that \*c is assignable: SUCCESS$
 ^\[foo4.\d+\] line \d+ Check that \*x is assignable: SUCCESS$
 ^\[foo5.\d+\] line \d+ Check that buffer.data is assignable: SUCCESS$
@@ -28,7 +24,6 @@ main.c
 ^\[foo8.\d+\] line \d+ Check that array\[\(.* int\)7\] is assignable: SUCCESS$
 ^\[foo8.\d+\] line \d+ Check that array\[\(.* int\)8\] is assignable: SUCCESS$
 ^\[foo8.\d+\] line \d+ Check that array\[\(.* int\)9\] is assignable: SUCCESS$
-^\[foo9.\d+\] line \d+ Check that array is assignable: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 Checks whether CBMC parses correctly all standard cases for assigns clauses.
diff --git a/regression/contracts/assigns_validity_pointer_01/test.desc b/regression/contracts/assigns_validity_pointer_01/test.desc
index 149013fd7a7..905c8e2e27a 100644
--- a/regression/contracts/assigns_validity_pointer_01/test.desc
+++ b/regression/contracts/assigns_validity_pointer_01/test.desc
@@ -8,7 +8,6 @@ SUCCESS
 // bar
 ASSERT \*foo::x > 0
 IF ¬\(\*foo::x = 3\) THEN GOTO \d
-IF ¬\(.*0.* = NULL\) THEN GOTO \d
 ASSIGN .*::tmp_if_expr := \(\*\(.*0.*\) = 5 \? true : false\)
 ASSIGN .*::tmp_if_expr\$\d := .*::tmp_if_expr \? true : false
 ASSUME .*::tmp_if_expr\$\d
diff --git a/regression/contracts/assigns_validity_pointer_02/test.desc b/regression/contracts/assigns_validity_pointer_02/test.desc
index c8730036836..4035fc12118 100644
--- a/regression/contracts/assigns_validity_pointer_02/test.desc
+++ b/regression/contracts/assigns_validity_pointer_02/test.desc
@@ -7,8 +7,6 @@ main.c
 ^\[bar.\d+\] line \d+ Check that \*x is assignable: SUCCESS$
 ^\[bar.\d+\] line \d+ Check that \*y is assignable: SUCCESS$
 ^\[baz.\d+\] line \d+ Check that \*z is assignable: SUCCESS$
-^\[foo.\d+\] line \d+ Check that x is assignable: SUCCESS$
-^\[foo.\d+\] line \d+ Check that y is assignable: SUCCESS$
 ^\[foo.\d+\] line \d+ Check that \*x is assignable: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
diff --git a/regression/contracts/function_check_02/main.c b/regression/contracts/function_check_02/main.c
index 7960696b6d1..18be2525d8e 100644
--- a/regression/contracts/function_check_02/main.c
+++ b/regression/contracts/function_check_02/main.c
@@ -15,10 +15,16 @@ int initialize(int *arr)
   )
 // clang-format on
 {
-  for(int i = 0; i < 10; i++)
-  {
-    arr[i] = i;
-  }
+  arr[0] = 0;
+  arr[1] = 1;
+  arr[2] = 2;
+  arr[3] = 3;
+  arr[4] = 4;
+  arr[5] = 5;
+  arr[6] = 6;
+  arr[7] = 7;
+  arr[8] = 8;
+  arr[9] = 9;
 
   return 0;
 }
diff --git a/regression/contracts/history-pointer-enforce-10/main.c b/regression/contracts/history-pointer-enforce-10/main.c
index 5421773d9bb..475bc47b411 100644
--- a/regression/contracts/history-pointer-enforce-10/main.c
+++ b/regression/contracts/history-pointer-enforce-10/main.c
@@ -23,7 +23,7 @@ void bar(struct pair *p) __CPROVER_assigns(p->y)
   p->y = (p->y + 5);
 }
 
-void baz(struct pair p) __CPROVER_assigns(p)
+void baz(struct pair p) __CPROVER_assigns()
   __CPROVER_ensures(p == __CPROVER_old(p))
 {
   struct pair pp = p;
diff --git a/regression/contracts/history-pointer-enforce-10/test.desc b/regression/contracts/history-pointer-enforce-10/test.desc
index a3ad4b4cb9c..e8359a34c9e 100644
--- a/regression/contracts/history-pointer-enforce-10/test.desc
+++ b/regression/contracts/history-pointer-enforce-10/test.desc
@@ -7,8 +7,6 @@ main.c
 ^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$
 ^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$
 ^\[bar.\d+\] line \d+ Check that p->y is assignable: SUCCESS$
-^\[baz.\d+\] line \d+ Check that p is assignable: SUCCESS$
-^\[baz.\d+\] line \d+ Check that p is assignable: SUCCESS$
 ^\[foo.\d+\] line \d+ Check that \*p->y is assignable: SUCCESS$
 ^\[foo.\d+\] line \d+ Check that z is assignable: SUCCESS$
 ^\[main.assertion.\d+\] line \d+ assertion \*\(p->y\) == 7: SUCCESS$
@@ -19,3 +17,5 @@ main.c
 This test checks that history variables are supported for structs, symbols, and
 struct members. By using the --enforce-contract flag, the postcondition
 (with history variable) is asserted. In this case, this assertion should pass.
+Note: A function is always authorized to assign the variables that store
+its arguments, there is no need to mention them in the assigns clause.
diff --git a/regression/contracts/loop-freeness-check/main.c b/regression/contracts/loop-freeness-check/main.c
new file mode 100644
index 00000000000..3840c6dcaec
--- /dev/null
+++ b/regression/contracts/loop-freeness-check/main.c
@@ -0,0 +1,16 @@
+int foo(int *arr)
+  // clang-format off
+  __CPROVER_assigns(__CPROVER_POINTER_OBJECT(arr))
+// clang-format off
+{
+  for(int i = 0; i < 10; i++)
+    arr[i] = i;
+
+  return 0;
+}
+
+int main()
+{
+  int arr[10];
+  foo(arr);
+}
diff --git a/regression/contracts/loop-freeness-check/test.desc b/regression/contracts/loop-freeness-check/test.desc
new file mode 100644
index 00000000000..a1dc7477d0c
--- /dev/null
+++ b/regression/contracts/loop-freeness-check/test.desc
@@ -0,0 +1,13 @@
+CORE
+main.c
+--enforce-contract foo
+^--- begin invariant violation report ---$
+^Invariant check failed$
+^Condition: is_loop_free\(.*\)
+^Reason: Loops remain in function 'foo', assigns clause checking instrumentation cannot be applied\.$
+^EXIT=(127|134)$
+^SIGNAL=0$
+--
+--
+This test checks that loops that remain in the program when attempting to 
+instrument assigns clauses are detected and trigger an INVARIANT.
diff --git a/regression/contracts/quantifiers-exists-ensures-enforce/main.c b/regression/contracts/quantifiers-exists-ensures-enforce/main.c
index 1194c2968de..bfdc2e43d77 100644
--- a/regression/contracts/quantifiers-exists-ensures-enforce/main.c
+++ b/regression/contracts/quantifiers-exists-ensures-enforce/main.c
@@ -7,10 +7,16 @@ int f1(int *arr)
   })
 // clang-format on
 {
-  for(int i = 0; i < 10; i++)
-  {
-    arr[i] = i;
-  }
+  arr[0] = 0;
+  arr[1] = 1;
+  arr[2] = 2;
+  arr[3] = 3;
+  arr[4] = 4;
+  arr[5] = 5;
+  arr[6] = 6;
+  arr[7] = 7;
+  arr[8] = 8;
+  arr[9] = 9;
 
   return 0;
 }
@@ -24,10 +30,16 @@ int f2(int *arr)
   })
 // clang-format on
 {
-  for(int i = 0; i < 10; i++)
-  {
-    arr[i] = 0;
-  }
+  arr[0] = 0;
+  arr[1] = 1;
+  arr[2] = 2;
+  arr[3] = 3;
+  arr[4] = 4;
+  arr[5] = 5;
+  arr[6] = 6;
+  arr[7] = 7;
+  arr[8] = 8;
+  arr[9] = 9;
 
   return 0;
 }
diff --git a/regression/contracts/quantifiers-exists-requires-enforce/main.c b/regression/contracts/quantifiers-exists-requires-enforce/main.c
index 7985f57de3b..c74bbfbb009 100644
--- a/regression/contracts/quantifiers-exists-requires-enforce/main.c
+++ b/regression/contracts/quantifiers-exists-requires-enforce/main.c
@@ -1,7 +1,7 @@
 #include <stdbool.h>
 #include <stdlib.h>
 
-#define MAX_LEN 64
+#define MAX_LEN 10
 
 // clang-format off
 bool f1(int *arr, int len)
@@ -18,11 +18,27 @@ bool f1(int *arr, int len)
 // clang-format on
 {
   bool found_four = false;
-  for(int i = 0; i <= MAX_LEN; i++)
-  {
-    if(i < len)
-      found_four |= (arr[i] == 4);
-  }
+  if(0 < len)
+    found_four |= (arr[0] == 4);
+  if(1 < len)
+    found_four |= (arr[1] == 4);
+  if(2 < len)
+    found_four |= (arr[2] == 4);
+  if(3 < len)
+    found_four |= (arr[3] == 4);
+  if(4 < len)
+    found_four |= (arr[4] == 4);
+  if(5 < len)
+    found_four |= (arr[5] == 4);
+  if(6 < len)
+    found_four |= (arr[6] == 4);
+  if(7 < len)
+    found_four |= (arr[7] == 4);
+  if(8 < len)
+    found_four |= (arr[8] == 4);
+
+  if(9 < len)
+    found_four |= (arr[9] == 4);
 
   // clang-format off
   return (len > 0 ==> found_four);
diff --git a/regression/contracts/quantifiers-forall-ensures-enforce/main.c b/regression/contracts/quantifiers-forall-ensures-enforce/main.c
index cceba46be58..3e6335ab1f3 100644
--- a/regression/contracts/quantifiers-forall-ensures-enforce/main.c
+++ b/regression/contracts/quantifiers-forall-ensures-enforce/main.c
@@ -1,6 +1,6 @@
 #include <stdlib.h>
 
-#define MAX_LEN 16
+#define MAX_LEN 10
 
 // clang-format off
 int f1(int *arr, int len)
@@ -12,11 +12,27 @@ int f1(int *arr, int len)
   })
 // clang-format on
 {
-  for(int i = 0; i < MAX_LEN; i++)
-  {
-    if(i < len)
-      arr[i] = 0;
-  }
+  if(0 < len)
+    arr[0] = 0;
+  if(1 < len)
+    arr[1] = 0;
+  if(2 < len)
+    arr[2] = 0;
+  if(3 < len)
+    arr[3] = 0;
+  if(4 < len)
+    arr[4] = 0;
+  if(5 < len)
+    arr[5] = 0;
+  if(6 < len)
+    arr[6] = 0;
+  if(7 < len)
+    arr[7] = 0;
+  if(8 < len)
+    arr[8] = 0;
+  if(9 < len)
+    arr[9] = 0;
+
   return 0;
 }
 
diff --git a/regression/contracts/quantifiers-forall-ensures-enforce/test.desc b/regression/contracts/quantifiers-forall-ensures-enforce/test.desc
index 87a1b4d333e..b5a17935c58 100644
--- a/regression/contracts/quantifiers-forall-ensures-enforce/test.desc
+++ b/regression/contracts/quantifiers-forall-ensures-enforce/test.desc
@@ -4,10 +4,11 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^\[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS$
-^\[f1.\d+\] line \d+ Check that arr\[\(.*\)i\] is assignable: SUCCESS$
+^\[f1.\d+\] line \d+ Check that arr\[\(.*\)\d\] is assignable: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 ^warning: ignoring
+^\[f1.\d+\] line \d+ Check that arr\[\(.*\)\d\] is assignable: FAILURE$
 --
 The purpose of this test is to ensure that we can safely use __CPROVER_forall
 within positive contexts (enforced ENSURES clauses).
diff --git a/regression/contracts/quantifiers-forall-requires-enforce/main.c b/regression/contracts/quantifiers-forall-requires-enforce/main.c
index fe0da19e0ca..2040549f0f4 100644
--- a/regression/contracts/quantifiers-forall-requires-enforce/main.c
+++ b/regression/contracts/quantifiers-forall-requires-enforce/main.c
@@ -12,8 +12,16 @@ bool f1(int *arr)
 // clang-format on
 {
   bool is_identity = true;
-  for(int i = 0; i < 10; ++i)
-    is_identity &= (arr[i] == i);
+  is_identity &= (arr[0] == 0);
+  is_identity &= (arr[1] == 1);
+  is_identity &= (arr[2] == 2);
+  is_identity &= (arr[3] == 3);
+  is_identity &= (arr[4] == 4);
+  is_identity &= (arr[5] == 5);
+  is_identity &= (arr[6] == 6);
+  is_identity &= (arr[7] == 7);
+  is_identity &= (arr[8] == 8);
+  is_identity &= (arr[9] == 9);
   return is_identity;
 }
 
diff --git a/regression/contracts/quantifiers-nested-01/main.c b/regression/contracts/quantifiers-nested-01/main.c
index 2e1d0667115..f44da69dd13 100644
--- a/regression/contracts/quantifiers-nested-01/main.c
+++ b/regression/contracts/quantifiers-nested-01/main.c
@@ -11,10 +11,16 @@ int f1(int *arr)
   })
 // clang-format on
 {
-  for(int i = 0; i < 10; i++)
-  {
-    arr[i] = i;
-  }
+  arr[0] = 0;
+  arr[1] = 1;
+  arr[2] = 2;
+  arr[3] = 3;
+  arr[4] = 4;
+  arr[5] = 5;
+  arr[6] = 6;
+  arr[7] = 7;
+  arr[8] = 8;
+  arr[9] = 9;
 
   return 0;
 }
diff --git a/regression/contracts/quantifiers-nested-03/main.c b/regression/contracts/quantifiers-nested-03/main.c
index e7bf048ddcf..ca586ae9f3e 100644
--- a/regression/contracts/quantifiers-nested-03/main.c
+++ b/regression/contracts/quantifiers-nested-03/main.c
@@ -10,10 +10,16 @@ __CPROVER_assigns(__CPROVER_POINTER_OBJECT(arr))
   )
 // clang-format on
 {
-  for(int i = 0; i < 10; i++)
-  {
-    arr[i] = i;
-  }
+  arr[0] = 0;
+  arr[1] = 1;
+  arr[2] = 2;
+  arr[3] = 3;
+  arr[4] = 4;
+  arr[5] = 5;
+  arr[6] = 6;
+  arr[7] = 7;
+  arr[8] = 8;
+  arr[9] = 9;
 
   return 0;
 }
diff --git a/regression/contracts/test_aliasing_ensure/main.c b/regression/contracts/test_aliasing_ensure/main.c
index 3c4f94e863d..f68c823dc5a 100644
--- a/regression/contracts/test_aliasing_ensure/main.c
+++ b/regression/contracts/test_aliasing_ensure/main.c
@@ -6,7 +6,7 @@ int z;
 
 // clang-format off
 int foo(int *x, int *y)
-  __CPROVER_assigns(z, *x, y)
+  __CPROVER_assigns(z, *x)
   __CPROVER_requires(
     __CPROVER_is_fresh(x, sizeof(int)) &&
     *x > 0 &&
diff --git a/regression/contracts/test_aliasing_ensure_indirect/main.c b/regression/contracts/test_aliasing_ensure_indirect/main.c
index bac705ee9e3..125da5a16ac 100644
--- a/regression/contracts/test_aliasing_ensure_indirect/main.c
+++ b/regression/contracts/test_aliasing_ensure_indirect/main.c
@@ -2,7 +2,7 @@
 #include <stdbool.h>
 #include <stdlib.h>
 
-void bar(int *z) __CPROVER_assigns(z)
+void bar(int *z) __CPROVER_assigns()
   __CPROVER_ensures(__CPROVER_is_fresh(z, sizeof(int)))
 {
   z = malloc(sizeof(*z));
@@ -11,7 +11,7 @@ void bar(int *z) __CPROVER_assigns(z)
 
 // clang-format off
 int foo(int *x, int *y)
-  __CPROVER_assigns(*x, y)
+  __CPROVER_assigns(*x)
   __CPROVER_requires(
     __CPROVER_is_fresh(x, sizeof(int)) &&
     *x > 0 &&
diff --git a/regression/contracts/test_aliasing_ensure_indirect/test.desc b/regression/contracts/test_aliasing_ensure_indirect/test.desc
index 69df6b6065c..4c9575dddb9 100644
--- a/regression/contracts/test_aliasing_ensure_indirect/test.desc
+++ b/regression/contracts/test_aliasing_ensure_indirect/test.desc
@@ -4,7 +4,6 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 \[postcondition.\d+\] file main.c line \d+ Check ensures clause: SUCCESS
-\[bar.\d+\] line \d+ Check that z is assignable: SUCCESS
 \[foo.\d+\] line \d+ Check that \*x is assignable: SUCCESS
 \[main.assertion.\d+\] line \d+ assertion \!\(n \< 4\): SUCCESS
 ^VERIFICATION SUCCESSFUL$
diff --git a/src/goto-instrument/contracts/assigns.cpp b/src/goto-instrument/contracts/assigns.cpp
index bd612a25ff1..6e17935a63e 100644
--- a/src/goto-instrument/contracts/assigns.cpp
+++ b/src/goto-instrument/contracts/assigns.cpp
@@ -159,6 +159,15 @@ assigns_clauset::conditional_address_ranget::generate_unsafe_inclusion_check(
                               pointer_offset(upper_bound_address_var)}});
 }
 
+bool assigns_clauset::conditional_address_ranget::maybe_alive(
+  cfg_infot &cfg_info) const
+{
+  if(can_cast_expr<symbol_exprt>(source_expr))
+    return cfg_info.is_maybe_alive(to_symbol_expr(source_expr));
+
+  return true;
+}
+
 assigns_clauset::assigns_clauset(
   const exprt::operandst &assigns,
   const messaget &log,
@@ -192,14 +201,26 @@ void assigns_clauset::remove_from_write_set(const exprt &target_expr)
 }
 
 exprt assigns_clauset::generate_inclusion_check(
-  const conditional_address_ranget &lhs) const
+  const conditional_address_ranget &lhs,
+  optionalt<cfg_infot> &cfg_info_opt) const
 {
   if(write_set.empty())
     return not_exprt{lhs.validity_condition_var};
 
   exprt::operandst conditions{not_exprt{lhs.validity_condition_var}};
-  for(const auto &target : write_set)
-    conditions.push_back(target.generate_unsafe_inclusion_check(lhs));
+
+  if(cfg_info_opt.has_value())
+  {
+    auto &cfg_info = cfg_info_opt.value();
+    for(const auto &target : write_set)
+      if(target.maybe_alive(cfg_info))
+        conditions.push_back(target.generate_unsafe_inclusion_check(lhs));
+  }
+  else
+  {
+    for(const auto &target : write_set)
+      conditions.push_back(target.generate_unsafe_inclusion_check(lhs));
+  }
 
   return disjunction(conditions);
 }
diff --git a/src/goto-instrument/contracts/assigns.h b/src/goto-instrument/contracts/assigns.h
index 3059c9e882c..f43251347de 100644
--- a/src/goto-instrument/contracts/assigns.h
+++ b/src/goto-instrument/contracts/assigns.h
@@ -47,6 +47,11 @@ class assigns_clauset
       }
     };
 
+    /// Returns true whenever this CAR's `source_expr` and associated address
+    /// range may be alive at the instruction currently pointed to by
+    /// `cfg_info.target`.
+    bool maybe_alive(cfg_infot &cfg_info) const;
+
     const exprt source_expr;
     const source_locationt &location;
     const assigns_clauset &parent;
@@ -82,7 +87,9 @@ class assigns_clauset
   write_sett::const_iterator add_to_write_set(const exprt &);
   void remove_from_write_set(const exprt &);
 
-  exprt generate_inclusion_check(const conditional_address_ranget &) const;
+  exprt generate_inclusion_check(
+    const conditional_address_ranget &lhs,
+    optionalt<cfg_infot> &cfg_info_opt) const;
 
   const write_sett &get_write_set() const
   {
diff --git a/src/goto-instrument/contracts/contracts.cpp b/src/goto-instrument/contracts/contracts.cpp
index 325ed89226a..6c74c51d0c5 100644
--- a/src/goto-instrument/contracts/contracts.cpp
+++ b/src/goto-instrument/contracts/contracts.cpp
@@ -16,6 +16,7 @@ Date: February 2016
 #include <algorithm>
 #include <map>
 
+#include <analyses/local_bitvector_analysis.h>
 #include <analyses/local_may_alias.h>
 
 #include <ansi-c/c_expr.h>
@@ -307,9 +308,19 @@ void code_contractst::check_apply_loop_contracts(
       goto_function.body, loop_head, snapshot_instructions);
   };
 
+  optionalt<cfg_infot> cfg_empty_info;
+
   // Perform write set instrumentation on the entire loop.
   check_frame_conditions(
-    function_name, goto_function.body, loop_head, loop_end, loop_assigns);
+    function_name,
+    goto_function.body,
+    loop_head,
+    loop_end,
+    loop_assigns,
+    // do not skip checks on function parameter assignments
+    skipt::DontSkip,
+    // do not use CFG info for now
+    cfg_empty_info);
 
   havoc_assigns_targetst havoc_gen(to_havoc, ns);
   havoc_gen.append_full_havoc_code(
@@ -908,23 +919,25 @@ goto_functionst &code_contractst::get_goto_functions()
 }
 
 void code_contractst::instrument_assign_statement(
-  goto_programt::instructionst::iterator &instruction_it,
+  goto_programt::targett &instruction_it,
   goto_programt &program,
-  assigns_clauset &assigns_clause)
+  assigns_clauset &assigns_clause,
+  optionalt<cfg_infot> &cfg_info_opt)
 {
-  INVARIANT(
-    instruction_it->is_assign(),
-    "The first instruction of instrument_assign_statement should always be"
-    " an assignment");
   add_inclusion_check(
-    program, assigns_clause, instruction_it, instruction_it->assign_lhs());
+    program,
+    assigns_clause,
+    instruction_it,
+    instruction_it->assign_lhs(),
+    cfg_info_opt);
 }
 
 void code_contractst::instrument_call_statement(
-  goto_programt::instructionst::iterator &instruction_it,
+  goto_programt::targett &instruction_it,
   const irep_idt &function,
   goto_programt &body,
-  assigns_clauset &assigns)
+  assigns_clauset &assigns,
+  optionalt<cfg_infot> &cfg_info_opt)
 {
   INVARIANT(
     instruction_it->is_function_call(),
@@ -962,7 +975,8 @@ void code_contractst::instrument_call_statement(
       body,
       assigns,
       instruction_it,
-      pointer_object(instruction_it->call_arguments().front()));
+      pointer_object(instruction_it->call_arguments().front()),
+      cfg_info_opt);
 
     // skip all invalidation business if we're freeing invalid memory
     goto_programt alias_checking_instructions, skip_program;
@@ -1122,10 +1136,8 @@ bool code_contractst::check_frame_conditions_function(const irep_idt &function)
     return true;
   }
 
-  if(check_for_looped_mallocs(function_obj->second.body))
-  {
-    return true;
-  }
+  const auto &goto_function = function_obj->second;
+  auto &function_body = function_obj->second.body;
 
   // Get assigns clause for function
   const symbolt &target = ns.lookup(function);
@@ -1136,21 +1148,9 @@ bool code_contractst::check_frame_conditions_function(const irep_idt &function)
     function,
     symbol_table);
 
-  // detect and add static local variables
+  // Detect and add static local variables
   assigns.add_static_locals_to_write_set(goto_functions, function);
 
-  // Add formal parameters to write set
-  for(const auto &param : to_code_type(target.type).parameters())
-    assigns.add_to_write_set(ns.lookup(param.get_identifier()).symbol_expr());
-
-  auto instruction_it = function_obj->second.body.instructions.begin();
-  for(const auto &car : assigns.get_write_set())
-  {
-    auto snapshot_instructions = car.generate_snapshot_instructions();
-    insert_before_swap_and_advance(
-      function_obj->second.body, instruction_it, snapshot_instructions);
-  };
-
   // Full inlining of the function body
   // Inlining is performed so that function calls to a same function
   // occurring under different write sets get instrumented specifically
@@ -1162,38 +1162,147 @@ bool code_contractst::check_frame_conditions_function(const irep_idt &function)
     decorated.get_recursive_function_warnings_count() == 0,
     "Recursive functions found during inlining");
 
-  // restore internal invariants
+  // Clean up possible fake loops that are due to `IF 0!=0 GOTO i` instructions
+  simplify_gotos(function_body, ns);
+
+  // Restore internal coherence in the programs
+  goto_functions.update();
+
+  INVARIANT(
+    is_loop_free(function_body, ns, log),
+    "Loops remain in function '" + id2string(function) +
+      "', assigns clause checking instrumentation cannot be applied.");
+
+  // Create a deep copy of the original goto_function object
+  // and compute static control flow graph information on it
+  goto_functiont goto_function_orig;
+  goto_function_orig.copy_from(goto_function);
+  cfg_infot cfg_info(ns, goto_function_orig);
+  optionalt<cfg_infot> cfg_info_opt{cfg_info};
+
+  // Add formal parameters to write set
+  for(const auto &param : to_code_type(target.type).parameters())
+    assigns.add_to_write_set(ns.lookup(param.get_identifier()).symbol_expr());
+
+  auto instruction_it = function_body.instructions.begin();
+  for(const auto &car : assigns.get_write_set())
+  {
+    auto snapshot_instructions = car.generate_snapshot_instructions();
+    insert_before_swap_and_advance(
+      function_body, instruction_it, snapshot_instructions);
+  };
+
+  // Restore internal coherence in the programs
   goto_functions.update();
 
   // Insert write set inclusion checks.
   check_frame_conditions(
-    function_obj->first,
-    function_obj->second.body,
+    function,
+    function_body,
     instruction_it,
-    function_obj->second.body.instructions.end(),
-    assigns);
+    function_body.instructions.end(),
+    assigns,
+    // skip checks on function parameter assignments
+    skipt::Skip,
+    cfg_info_opt);
 
   return false;
 }
 
+/// Returns true iff the target instruction is tagged with a
+/// 'CONTRACT_PRAGMA_DISABLE_ASSIGNS_CHECK' pragma.
+bool has_disable_assigns_check_pragma(
+  const goto_programt::const_targett &target)
+{
+  const auto &pragmas = target->source_location().get_pragmas();
+  return pragmas.find(CONTRACT_PRAGMA_DISABLE_ASSIGNS_CHECK) != pragmas.end();
+}
+
+/// Returns true iff an `ASSIGN lhs := rhs` instruction must be instrumented.
+bool must_check_assign(
+  const goto_programt::const_targett &target,
+  code_contractst::skipt skip_parameter_assigns,
+  const namespacet ns,
+  const optionalt<cfg_infot> cfg_info_opt)
+{
+  if(
+    const auto &symbol_expr =
+      expr_try_dynamic_cast<symbol_exprt>(target->assign_lhs()))
+  {
+    if(
+      skip_parameter_assigns == code_contractst::skipt::DontSkip &&
+      ns.lookup(symbol_expr->get_identifier()).is_parameter)
+      return true;
+
+    if(cfg_info_opt.has_value())
+      return !cfg_info_opt.value().is_local(symbol_expr->get_identifier());
+  }
+
+  return true;
+}
+
+/// Returns true iff a `DECL x` must be added to the local write set.
+///
+/// A variable is called 'dirty' if its address gets taken at some point in
+/// the program.
+///
+/// Assuming the goto program is obtained from a structured C program that
+/// passed C compiler checks, non-dirty variables can only be assigned to
+/// directly by name, cannot escape their lexical scope, and are always safe
+/// to assign. Hence, we only track dirty variables in the write set.
+bool must_track_decl(
+  const goto_programt::const_targett &target,
+  const optionalt<cfg_infot> &cfg_info_opt)
+{
+  if(cfg_info_opt.has_value())
+    return cfg_info_opt.value().is_not_local_or_dirty_local(
+      target->decl_symbol().get_identifier());
+
+  // Unless proved non-dirty by the CFG analysis we assume it is dirty.
+  return true;
+}
+
+/// Returns true iff a `DEAD x` must be processed to upate the local write set.
+/// The conditions are the same than for tracking a `DECL x` instruction.
+bool must_track_dead(
+  const goto_programt::const_targett &target,
+  const optionalt<cfg_infot> &cfg_info_opt)
+{
+  // Unless proved non-dirty by the CFG analysis we assume it is dirty.
+  if(!cfg_info_opt.has_value())
+    return true;
+
+  return cfg_info_opt.value().is_not_local_or_dirty_local(
+    target->dead_symbol().get_identifier());
+}
+
 void code_contractst::check_frame_conditions(
   const irep_idt &function,
   goto_programt &body,
   goto_programt::targett instruction_it,
   const goto_programt::targett &instruction_end,
-  assigns_clauset &assigns)
+  assigns_clauset &assigns,
+  skipt skip_parameter_assigns,
+  optionalt<cfg_infot> &cfg_info_opt)
 {
-  for(; instruction_it != instruction_end; ++instruction_it)
+  while(instruction_it != instruction_end)
   {
-    const auto &pragmas = instruction_it->source_location().get_pragmas();
-    if(pragmas.find(CONTRACT_PRAGMA_DISABLE_ASSIGNS_CHECK) != pragmas.end())
+    // Skip instructions marked as disabled for assigns clause checking
+    if(has_disable_assigns_check_pragma(instruction_it))
+    {
+      instruction_it++;
+      if(cfg_info_opt.has_value())
+        cfg_info_opt.value().step();
       continue;
+    }
 
     // Do not instrument this instruction again in the future,
     // since we are going to instrument it now below.
     add_pragma_disable_assigns_check(*instruction_it);
 
-    if(instruction_it->is_decl())
+    if(
+      instruction_it->is_decl() &&
+      must_track_decl(instruction_it, cfg_info_opt))
     {
       // grab the declared symbol
       const auto &decl_symbol = instruction_it->decl_symbol();
@@ -1205,18 +1314,24 @@ void code_contractst::check_frame_conditions(
         body, instruction_it, snapshot_instructions);
       // since CAR was inserted *after* the DECL instruction,
       // move the instruction pointer backward,
-      // because the `for` loop takes care of the increment
+      // because the loop step takes care of the increment
       instruction_it--;
     }
-    else if(instruction_it->is_assign())
+    else if(
+      instruction_it->is_assign() &&
+      must_check_assign(
+        instruction_it, skip_parameter_assigns, ns, cfg_info_opt))
     {
-      instrument_assign_statement(instruction_it, body, assigns);
+      instrument_assign_statement(instruction_it, body, assigns, cfg_info_opt);
     }
     else if(instruction_it->is_function_call())
     {
-      instrument_call_statement(instruction_it, function, body, assigns);
+      instrument_call_statement(
+        instruction_it, function, body, assigns, cfg_info_opt);
     }
-    else if(instruction_it->is_dead())
+    else if(
+      instruction_it->is_dead() &&
+      must_track_dead(instruction_it, cfg_info_opt))
     {
       const auto &symbol = instruction_it->dead_symbol();
       source_locationt location_no_checks = instruction_it->source_location();
@@ -1232,10 +1347,10 @@ void code_contractst::check_frame_conditions(
           symbol_car->validity_condition_var,
           false_exprt{},
           instruction_it->source_location());
-        // note that the CAR must be invalidated _after_ the DEAD instruction
-        body.insert_after(
+        body.insert_before_swap(
           instruction_it,
           add_pragma_disable_assigns_check(invalidation_assignment));
+        instruction_it++;
       }
       else
       {
@@ -1257,8 +1372,14 @@ void code_contractst::check_frame_conditions(
     {
       const auto havoc_argument =
         pointer_object(instruction_it->get_other().operands().front());
-      add_inclusion_check(body, assigns, instruction_it, havoc_argument);
+      add_inclusion_check(
+        body, assigns, instruction_it, havoc_argument, cfg_info_opt);
     }
+
+    // Move to the next instruction
+    instruction_it++;
+    if(cfg_info_opt.has_value())
+      cfg_info_opt.value().step();
   }
 }
 
@@ -1266,10 +1387,11 @@ const assigns_clauset::conditional_address_ranget
 code_contractst::add_inclusion_check(
   goto_programt &program,
   const assigns_clauset &assigns,
-  goto_programt::instructionst::iterator &instruction_it,
-  const exprt &expr)
+  goto_programt::targett &instruction_it,
+  const exprt &lhs,
+  optionalt<cfg_infot> &cfg_info_opt)
 {
-  const assigns_clauset::conditional_address_ranget car{assigns, expr};
+  const assigns_clauset::conditional_address_ranget car{assigns, lhs};
   auto snapshot_instructions = car.generate_snapshot_instructions();
   insert_before_swap_and_advance(
     program, instruction_it, snapshot_instructions);
@@ -1279,9 +1401,9 @@ code_contractst::add_inclusion_check(
     instruction_it->source_location_nonconst();
   disable_pointer_checks(location_no_checks);
   location_no_checks.set_comment(
-    "Check that " + from_expr(ns, expr.id(), expr) + " is assignable");
+    "Check that " + from_expr(ns, lhs.id(), lhs) + " is assignable");
   assertion.add(goto_programt::make_assertion(
-    assigns.generate_inclusion_check(car), location_no_checks));
+    assigns.generate_inclusion_check(car, cfg_info_opt), location_no_checks));
   insert_before_swap_and_advance(program, instruction_it, assertion);
 
   return car;
diff --git a/src/goto-instrument/contracts/contracts.h b/src/goto-instrument/contracts/contracts.h
index 6514aada79e..bc0313c9595 100644
--- a/src/goto-instrument/contracts/contracts.h
+++ b/src/goto-instrument/contracts/contracts.h
@@ -28,6 +28,7 @@ Date: February 2016
 
 #include <util/message.h>
 #include <util/namespace.h>
+#include <util/optional.h>
 #include <util/pointer_expr.h>
 
 #include "assigns.h"
@@ -110,6 +111,13 @@ class code_contractst
 
   namespacet ns;
 
+  /// Tells wether to skip or not skip an action
+  enum class skipt
+  {
+    DontSkip,
+    Skip
+  };
+
 protected:
   symbol_tablet &symbol_table;
   goto_functionst &goto_functions;
@@ -125,22 +133,38 @@ class code_contractst
   /// Instrument functions to check frame conditions.
   bool check_frame_conditions_function(const irep_idt &function);
 
-  /// Insert assertion statements into the goto program to ensure that
+  ///  \brief Insert assertion statements into the goto program to ensure that
   /// assigned memory is within the assignable memory frame.
+  ///
+  /// \param function Name of the function getting instrumented.
+  /// \param body Body of the function getting instrumented.
+  /// \param instruction_it Iterator to the instruction from which to start
+  /// instrumentation (inclusive).
+  /// \param instruction_end Iterator to the instruction at which to stop
+  /// instrumentation (exclusive).
+  /// \param assigns Assigns clause of the function (its write set attribute
+  /// gets extended during the instrumentation).
+  /// \param skip_parameter_assigns If true, will cause assignments to symbol
+  /// marked as is_parameter to not be instrumented.
+  /// \param cfg_info_opt Control flow graph information can will be used
+  /// for write set optimisation if available.
   void check_frame_conditions(
-    const irep_idt &,
-    goto_programt &,
-    goto_programt::targett,
-    const goto_programt::targett &,
-    assigns_clauset &);
+    const irep_idt &function,
+    goto_programt &body,
+    goto_programt::targett instruction_it,
+    const goto_programt::targett &instruction_end,
+    assigns_clauset &assigns,
+    skipt skip_parameter_assigns,
+    optionalt<cfg_infot> &cfg_info_opt);
 
   /// Inserts an assertion into the goto program to ensure that
   /// an expression is within the assignable memory frame.
   const assigns_clauset::conditional_address_ranget add_inclusion_check(
-    goto_programt &,
-    const assigns_clauset &,
-    goto_programt::instructionst::iterator &,
-    const exprt &);
+    goto_programt &program,
+    const assigns_clauset &assigns,
+    goto_programt::targett &instruction_it,
+    const exprt &lhs,
+    optionalt<cfg_infot> &cfg_info_opt);
 
   /// Check if there are any malloc statements which may be repeated because of
   /// a goto statement that jumps back.
@@ -150,18 +174,20 @@ class code_contractst
   /// instruction_it, to ensure that the left-hand-side of the assignment
   /// is "included" in the (conditional address ranges in the) write set.
   void instrument_assign_statement(
-    goto_programt::instructionst::iterator &,
-    goto_programt &,
-    assigns_clauset &);
+    goto_programt::targett &instruction_it,
+    goto_programt &program,
+    assigns_clauset &assigns_clause,
+    optionalt<cfg_infot> &cfg_info_opt);
 
   /// Inserts an assertion into program immediately before the function call at
   /// instruction_it, to ensure that all memory locations written to by the
   // callee are "included" in the (conditional address ranges in the) write set.
   void instrument_call_statement(
-    goto_programt::instructionst::iterator &,
-    const irep_idt &,
-    goto_programt &,
-    assigns_clauset &);
+    goto_programt::targett &instruction_it,
+    const irep_idt &function,
+    goto_programt &body,
+    assigns_clauset &assigns,
+    optionalt<cfg_infot> &cfg_info_opt);
 
   /// Apply loop contracts, whenever available, to all loops in `function`.
   /// Loop invariants, loop variants, and loop assigns clauses.
@@ -173,10 +199,10 @@ class code_contractst
   /// non-deterministic assignments for the write set, and assumptions
   /// based on ensures clauses.
   bool apply_function_contract(
-    const irep_idt &,
-    const source_locationt &,
-    goto_programt &,
-    goto_programt::targett &);
+    const irep_idt &function,
+    const source_locationt &location,
+    goto_programt &function_body,
+    goto_programt::targett &target);
 
   /// Instruments `wrapper_function` adding assumptions based on requires
   /// clauses and assertions based on ensures clauses.
diff --git a/src/goto-instrument/contracts/utils.cpp b/src/goto-instrument/contracts/utils.cpp
index 95185dd4dd1..607038d9e87 100644
--- a/src/goto-instrument/contracts/utils.cpp
+++ b/src/goto-instrument/contracts/utils.cpp
@@ -10,9 +10,13 @@ Date: September 2021
 
 #include "utils.h"
 
+#include <goto-programs/cfg.h>
 #include <util/fresh_symbol.h>
+#include <util/graph.h>
+#include <util/message.h>
 #include <util/pointer_expr.h>
 #include <util/pointer_predicates.h>
+#include <util/simplify_expr.h>
 
 goto_programt::instructiont &
 add_pragma_disable_assigns_check(goto_programt::instructiont &instr)
@@ -163,3 +167,64 @@ void disable_pointer_checks(source_locationt &source_location)
   source_location.add_pragma("disable:pointer-primitive-check");
   source_location.add_pragma("disable:pointer-overflow-check");
 }
+
+void simplify_gotos(goto_programt &goto_program, namespacet &ns)
+{
+  for(auto &instruction : goto_program.instructions)
+  {
+    if(
+      instruction.is_goto() &&
+      simplify_expr(instruction.get_condition(), ns).is_false())
+      instruction.turn_into_skip();
+  }
+}
+
+bool is_loop_free(
+  const goto_programt &goto_program,
+  namespacet &ns,
+  messaget &log)
+{
+  // create cfg from instruction list
+  cfg_baset<empty_cfg_nodet> cfg;
+  cfg(goto_program);
+
+  // check that all nodes are there
+  INVARIANT(
+    goto_program.instructions.size() == cfg.size(),
+    "Instruction list vs CFG size mismatch.");
+
+  // compute SCCs
+  using idxt = graph_nodet<empty_cfg_nodet>::node_indext;
+  std::vector<idxt> node_to_scc(cfg.size(), -1);
+  auto nof_sccs = cfg.SCCs(node_to_scc);
+
+  // compute size of each SCC
+  std::vector<int> scc_size(nof_sccs, 0);
+  for(auto scc : node_to_scc)
+  {
+    INVARIANT(
+      0 <= scc && scc < nof_sccs, "Could not determine SCC for instruction");
+    scc_size[scc]++;
+  }
+
+  // check they are all of size 1
+  for(size_t scc_id = 0; scc_id < nof_sccs; scc_id++)
+  {
+    auto size = scc_size[scc_id];
+    if(size > 1)
+    {
+      log.error() << "Found CFG SCC with size " << size << messaget::eom;
+      for(const auto &node_id : node_to_scc)
+      {
+        if(node_to_scc[node_id] == scc_id)
+        {
+          const auto &pc = cfg[node_id].PC;
+          goto_program.output_instruction(ns, "", log.error(), *pc);
+          log.error() << messaget::eom;
+        }
+      }
+      return false;
+    }
+  }
+  return true;
+}
diff --git a/src/goto-instrument/contracts/utils.h b/src/goto-instrument/contracts/utils.h
index 1614ce023a3..3ff656953a9 100644
--- a/src/goto-instrument/contracts/utils.h
+++ b/src/goto-instrument/contracts/utils.h
@@ -13,10 +13,16 @@ Date: September 2021
 
 #include <vector>
 
+#include <analyses/dirty.h>
+#include <analyses/locals.h>
+
 #include <goto-instrument/havoc_utils.h>
 
 #include <goto-programs/goto_model.h>
 
+#include <util/expr_cast.h>
+#include <util/message.h>
+
 #define CONTRACT_PRAGMA_DISABLE_ASSIGNS_CHECK "contracts:disable:assigns-check"
 
 /// \brief A class that overrides the low-level havocing functions in the base
@@ -112,7 +118,7 @@ void insert_before_swap_and_advance(
 /// \param mode: The mode for the new symbol, e.g. ID_C, ID_java.
 /// \param symtab: The symbol table to which the new symbol is to be added.
 /// \param suffix: Suffix to use to generate the unique name
-/// \param is_auxiliary: Do not print symbol in traces if true (default = false)
+/// \param is_auxiliary: Do not print symbol in traces if true (default = true)
 /// \return The new symbolt object.
 const symbolt &new_tmp_symbol(
   const typet &type,
@@ -120,9 +126,84 @@ const symbolt &new_tmp_symbol(
   const irep_idt &mode,
   symbol_table_baset &symtab,
   std::string suffix = "tmp_cc",
-  bool is_auxiliary = false);
+  bool is_auxiliary = true);
 
 /// Add disable pragmas for all pointer checks on the given location
 void disable_pointer_checks(source_locationt &source_location);
 
+/// Turns goto instructions `IF cond GOTO label` where the condition
+/// statically simplifies to `false` into SKIP instructions.
+void simplify_gotos(goto_programt &goto_program, namespacet &ns);
+
+/// Returns true iff the given program is loop-free,
+/// i.e. if each SCC of its CFG contains a single element.
+bool is_loop_free(
+  const goto_programt &goto_program,
+  namespacet &ns,
+  messaget &log);
+
+/// Stores information about a goto function computed from its CFG,
+/// together with a `target` iterator into the instructions of the function.
+///
+/// The methods of this class provide information about identifiers at
+/// the current `target` instruction to allow simplifying assigns
+/// clause checking assertions.
+class cfg_infot
+{
+public:
+  cfg_infot(const namespacet &_ns, goto_functiont &_goto_function)
+    : ns(_ns),
+      goto_function(_goto_function),
+      target(goto_function.body.instructions.begin()),
+      dirty_analysis(goto_function),
+      locals(goto_function)
+  {
+  }
+
+  /// Steps the `target` iterator forward.
+  void step()
+  {
+    target++;
+  }
+
+  /// Returns true iff the given `ident` is either not a `goto_function` local
+  /// or is a local that is dirty.
+  bool is_not_local_or_dirty_local(irep_idt ident) const
+  {
+    if(is_local(ident))
+      return dirty_analysis.get_dirty_ids().find(ident) !=
+             dirty_analysis.get_dirty_ids().end();
+    else
+      return true;
+  }
+
+  /// Returns true whenever the given `symbol_expr` might be alive
+  /// at the current `target` instruction.
+  bool is_maybe_alive(const symbol_exprt &symbol_expr)
+  {
+    // TODO query the static analysis when available
+    return true;
+  }
+
+  /// Returns true iff `ident` is a local (or parameter) of `goto_function`.
+  bool is_local(irep_idt ident) const
+  {
+    const auto &symbol = ns.lookup(ident);
+    return locals.is_local(ident) || symbol.is_parameter;
+  }
+
+  /// returns the current target instruction
+  const goto_programt::targett &get_current_target() const
+  {
+    return target;
+  }
+
+private:
+  const namespacet &ns;
+  goto_functiont &goto_function;
+  goto_programt::targett target;
+  const dirtyt dirty_analysis;
+  const localst locals;
+};
+
 #endif // CPROVER_GOTO_INSTRUMENT_CONTRACTS_UTILS_H