diff --git a/regression/contracts-dfcc/test_is_fresh_enforce_requires_disjunction_fail/test.desc b/regression/contracts-dfcc/test_is_fresh_enforce_requires_disjunction_fail/test.desc
index e121dadff07..bffd72b375d 100644
--- a/regression/contracts-dfcc/test_is_fresh_enforce_requires_disjunction_fail/test.desc
+++ b/regression/contracts-dfcc/test_is_fresh_enforce_requires_disjunction_fail/test.desc
@@ -5,13 +5,13 @@ main.c
 ^\[__CPROVER_contracts_car_set_insert.assertion.\d+\] line \d+ no offset bits overflow on CAR upper bound computation: FAILURE$
 ^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ ptr NULL or writable up to size: FAILURE$
 ^\[__CPROVER_contracts_write_set_check_assignment.assertion.\d+\] line \d+ no offset bits overflow on CAR upper bound computation: FAILURE$
-^\[foo.assigns.\d+\] line 11 Check that *x is assignable: FAILURE$
-^\[foo.pointer_dereference.\d+\] line 11 dereference failure: pointer NULL in \*x: FAILURE$
-^\[foo.pointer_dereference.\d+\] line 11 dereference failure: pointer invalid in \*x: FAILURE$
-^\[foo.pointer_dereference.\d+\] line 11 dereference failure: deallocated dynamic object in \*x: FAILURE$
-^\[foo.pointer_dereference.\d+\] line 11 dereference failure: dead object in \*x: FAILURE$
-^\[foo.pointer_dereference.\d+\] line 11 dereference failure: pointer outside object bounds in \*x: FAILURE$
-^\[foo.pointer_dereference.\d+\] line 11 dereference failure: invalid integer address in \*x: FAILURE$
+^\[foo.assigns.\d+\] line \d+ Check that \*x is assignable: FAILURE$
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer NULL in \*x: FAILURE$
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer invalid in \*x: FAILURE$
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: deallocated dynamic object in \*x: FAILURE$
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: dead object in \*x: FAILURE$
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: pointer outside object bounds in \*x: FAILURE$
+^\[foo.pointer_dereference.\d+\] line \d+ dereference failure: invalid integer address in \*x: FAILURE$
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/regression/contracts-dfcc/test_is_fresh_enforce_requires_disjunction_pass/test.desc b/regression/contracts-dfcc/test_is_fresh_enforce_requires_disjunction_pass/test.desc
index 8f6cf7c92fc..f5d0da4c552 100644
--- a/regression/contracts-dfcc/test_is_fresh_enforce_requires_disjunction_pass/test.desc
+++ b/regression/contracts-dfcc/test_is_fresh_enforce_requires_disjunction_pass/test.desc
@@ -1,23 +1,23 @@
 CORE dfcc-only
 main.c
 --dfcc main --enforce-contract foo
-^\[foo.assertion.\d+\] line 13 assertion 0: FAILURE$
-^\[foo.assigns.\d+\] line 14 Check that \*x is assignable: SUCCESS$
-^\[foo.pointer_dereference.\d+\] line 14 dereference failure: pointer NULL in \*x: SUCCESS$
-^\[foo.pointer_dereference.\d+\] line 14 dereference failure: pointer invalid in \*x: SUCCESS$
-^\[foo.pointer_dereference.\d+\] line 14 dereference failure: deallocated dynamic object in \*x: SUCCESS$
-^\[foo.pointer_dereference.\d+\] line 14 dereference failure: dead object in \*x: SUCCESS$
-^\[foo.pointer_dereference.\d+\] line 14 dereference failure: pointer outside object bounds in \*x: SUCCESS$
-^\[foo.pointer_dereference.\d+\] line 14 dereference failure: invalid integer address in \*x: SUCCESS$
-^\[foo.assertion.\d+\] line 16 assertion 0: FAILURE$
-^\[foo.assertion.\d+\] line 17 assertion x == \(\(.*\)NULL\): SUCCESS$
-^\[foo.assigns.\d+\] line 18 Check that \*y is assignable: SUCCESS$
-^\[foo.pointer_dereference.\d+\] line 18 dereference failure: pointer NULL in \*y: SUCCESS$
-^\[foo.pointer_dereference.\d+\] line 18 dereference failure: pointer invalid in \*y: SUCCESS$
-^\[foo.pointer_dereference.\d+\] line 18 dereference failure: deallocated dynamic object in \*y: SUCCESS$
-^\[foo.pointer_dereference.\d+\] line 18 dereference failure: dead object in \*y: SUCCESS$
-^\[foo.pointer_dereference.\d+\] line 18 dereference failure: pointer outside object bounds in \*y: SUCCESS$
-^\[foo.pointer_dereference.\d+\] line 18 dereference failure: invalid integer address in \*y: SUCCESS$
+^\[foo.assertion.\d+\] line 14 assertion 0: FAILURE$
+^\[foo.assigns.\d+\] line 15 Check that \*x is assignable: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line 15 dereference failure: pointer NULL in \*x: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line 15 dereference failure: pointer invalid in \*x: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line 15 dereference failure: deallocated dynamic object in \*x: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line 15 dereference failure: dead object in \*x: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line 15 dereference failure: pointer outside object bounds in \*x: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line 15 dereference failure: invalid integer address in \*x: SUCCESS$
+^\[foo.assertion.\d+\] line 19 assertion 0: FAILURE$
+^\[foo.assertion.\d+\] line 20 assertion x == \(\(.*\)NULL\): SUCCESS$
+^\[foo.assigns.\d+\] line 21 Check that \*y is assignable: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line 21 dereference failure: pointer NULL in \*y: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line 21 dereference failure: pointer invalid in \*y: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line 21 dereference failure: deallocated dynamic object in \*y: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line 21 dereference failure: dead object in \*y: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line 21 dereference failure: pointer outside object bounds in \*y: SUCCESS$
+^\[foo.pointer_dereference.\d+\] line 21 dereference failure: invalid integer address in \*y: SUCCESS$
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
diff --git a/regression/contracts-dfcc/test_is_fresh_replace_ensures_disjunction_pass/test.desc b/regression/contracts-dfcc/test_is_fresh_replace_ensures_disjunction_pass/test.desc
index 483223a7922..295434501f9 100644
--- a/regression/contracts-dfcc/test_is_fresh_replace_ensures_disjunction_pass/test.desc
+++ b/regression/contracts-dfcc/test_is_fresh_replace_ensures_disjunction_pass/test.desc
@@ -1,23 +1,23 @@
 CORE dfcc-only
 main.c
 --dfcc main --replace-call-with-contract foo
-^\[bar.assertion.\d+\] line 25 assertion 0: FAILURE$
-^\[bar.assigns.\d+\] line 26 Check that \*x is assignable: SUCCESS$
-^\[bar.pointer_dereference.\d+\] line 26 dereference failure: pointer NULL in \*x: SUCCESS$
-^\[bar.pointer_dereference.\d+\] line 26 dereference failure: pointer invalid in \*x: SUCCESS$
-^\[bar.pointer_dereference.\d+\] line 26 dereference failure: deallocated dynamic object in \*x: SUCCESS$
-^\[bar.pointer_dereference.\d+\] line 26 dereference failure: dead object in \*x: SUCCESS$
-^\[bar.pointer_dereference.\d+\] line 26 dereference failure: pointer outside object bounds in \*x: SUCCESS$
-^\[bar.pointer_dereference.\d+\] line 26 dereference failure: invalid integer address in \*x: SUCCESS$
-^\[bar.assertion.\d+\] line 28 assertion 0: FAILURE$
-^\[bar.assertion.\d+\] line 29 assertion x == \(\(.*\)NULL\): SUCCESS$
-^\[bar.assigns.\d+\] line 30 Check that \*y is assignable: SUCCESS$
-^\[bar.pointer_dereference.\d+\] line 30 dereference failure: pointer NULL in \*y: SUCCESS$
-^\[bar.pointer_dereference.\d+\] line 30 dereference failure: pointer invalid in \*y: SUCCESS$
-^\[bar.pointer_dereference.\d+\] line 30 dereference failure: deallocated dynamic object in \*y: SUCCESS$
-^\[bar.pointer_dereference.\d+\] line 30 dereference failure: dead object in \*y: SUCCESS$
-^\[bar.pointer_dereference.\d+\] line 30 dereference failure: pointer outside object bounds in \*y: SUCCESS$
-^\[bar.pointer_dereference.\d+\] line 30 dereference failure: invalid integer address in \*y: SUCCESS$
+^\[bar.assertion.\d+\] line 27 assertion 0: FAILURE$
+^\[bar.assigns.\d+\] line 28 Check that \*x is assignable: SUCCESS$
+^\[bar.pointer_dereference.\d+\] line 28 dereference failure: pointer NULL in \*x: SUCCESS$
+^\[bar.pointer_dereference.\d+\] line 28 dereference failure: pointer invalid in \*x: SUCCESS$
+^\[bar.pointer_dereference.\d+\] line 28 dereference failure: deallocated dynamic object in \*x: SUCCESS$
+^\[bar.pointer_dereference.\d+\] line 28 dereference failure: dead object in \*x: SUCCESS$
+^\[bar.pointer_dereference.\d+\] line 28 dereference failure: pointer outside object bounds in \*x: SUCCESS$
+^\[bar.pointer_dereference.\d+\] line 28 dereference failure: invalid integer address in \*x: SUCCESS$
+^\[bar.assertion.\d+\] line 32 assertion 0: FAILURE$
+^\[bar.assertion.\d+\] line 33 assertion x == \(\(.*\)NULL\): SUCCESS$
+^\[bar.assigns.\d+\] line 34 Check that \*y is assignable: SUCCESS$
+^\[bar.pointer_dereference.\d+\] line 34 dereference failure: pointer NULL in \*y: SUCCESS$
+^\[bar.pointer_dereference.\d+\] line 34 dereference failure: pointer invalid in \*y: SUCCESS$
+^\[bar.pointer_dereference.\d+\] line 34 dereference failure: deallocated dynamic object in \*y: SUCCESS$
+^\[bar.pointer_dereference.\d+\] line 34 dereference failure: dead object in \*y: SUCCESS$
+^\[bar.pointer_dereference.\d+\] line 34 dereference failure: pointer outside object bounds in \*y: SUCCESS$
+^\[bar.pointer_dereference.\d+\] line 34 dereference failure: invalid integer address in \*y: SUCCESS$
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$