Check inferred loop assigns clauses instead of blindly trusting them

regression/contracts/github_6168_infinite_unwinding_bug/test.desc

@@ -4,8 +4,8 @@ main.c
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$
-^\[main.1\] line \d+ Check loop invariant before entry: SUCCESS$
-^\[main.2\] line \d+ Check that loop invariant is preserved: SUCCESS$
+^\[main.\d+\] line \d+ Check loop invariant before entry: SUCCESS$
+^\[main.\d+\] line \d+ Check that loop invariant is preserved: SUCCESS$
 --
 --
 This is guarding against an issue described in https://github.com/diffblue/cbmc/issues/6168.

regression/contracts/invar_check_break_fail/test.desc

@@ -3,9 +3,10 @@ main.c
 --apply-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.1\] .* Check loop invariant before entry: SUCCESS$
-^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
-^\[main.assertion.1\] .* assertion r == 0: FAILURE$
+^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main\.\d+\] .* Check that r is assignable: SUCCESS$
+^\[main\.assertion\.\d+\] .* assertion r == 0: FAILURE$
 ^VERIFICATION FAILED$
 --
 This test is expected to fail along the code path where r is an even integer

regression/contracts/invar_check_break_pass/test.desc

@@ -3,9 +3,10 @@ main.c
 --apply-loop-contracts
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.1\] .* Check loop invariant before entry: SUCCESS$
-^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
-^\[main.assertion.1\] .* assertion r == 0 || r == 1: SUCCESS$
+^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main\.\d+\] .* Check that r is assignable: SUCCESS$
+^\[main\.assertion\.\d+\] .* assertion r == 0 || r == 1: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 This test checks that conditionals and `break` are correctly handled.

regression/contracts/invar_check_continue/test.desc

@@ -3,9 +3,10 @@ main.c
 --apply-loop-contracts
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.1\] .* Check loop invariant before entry: SUCCESS$
-^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
-^\[main.assertion.1\] .* assertion r == 0: SUCCESS$
+^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main\.\d+\] .* Check that r is assignable: SUCCESS$
+^\[main\.assertion\.\d+\] .* assertion r == 0: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 This test checks that conditionals and `continue` are correctly handled.

regression/contracts/invar_check_multiple_loops/test.desc

@@ -3,13 +3,17 @@ main.c
 --apply-loop-contracts
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.1\] .* Check loop invariant before entry: SUCCESS$
-^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
-^\[main.3\] .* Check decreases clause on loop iteration: SUCCESS$
-^\[main.4\] .* Check loop invariant before entry: SUCCESS$
-^\[main.5\] .* Check that loop invariant is preserved: SUCCESS$
-^\[main.6\] .* Check decreases clause on loop iteration: SUCCESS$
-^\[main.assertion.1\] .* assertion x == y \+ 2 \* n: SUCCESS$
+^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main\.\d+\] .* Check decreases clause on loop iteration: SUCCESS$
+^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main\.\d+\] .* Check decreases clause on loop iteration: SUCCESS$
+^\[main\.assertion\.\d+\] .* assertion x == y \+ 2 \* n: SUCCESS$
+^\[main\.\d+\] line 8 Check that r is assignable: SUCCESS$
+^\[main\.\d+\] line 15 Check that x is assignable: SUCCESS$
+^\[main\.\d+\] line 23 Check that y is assignable: SUCCESS$
+^\[main\.\d+\] line 24 Check that r is assignable: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 This test checks that multiple loops and `for` loops are correctly handled.

regression/contracts/invar_check_nested_loops/test.desc

@@ -3,13 +3,16 @@ main.c
 --apply-loop-contracts
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.1\] .* Check loop invariant before entry: SUCCESS$
-^\[main.5\] .* Check that loop invariant is preserved: SUCCESS$
-^\[main.6\] .* Check decreases clause on loop iteration: SUCCESS$
-^\[main.2\] .* Check loop invariant before entry: SUCCESS$
-^\[main.3\] .* Check that loop invariant is preserved: SUCCESS$
-^\[main.4\] .* Check decreases clause on loop iteration: SUCCESS$
-^\[main.assertion.1\] .* assertion s == n: SUCCESS$
+^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main\.\d+\] .* Check decreases clause on loop iteration: SUCCESS$
+^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main\.\d+\] .* Check decreases clause on loop iteration: SUCCESS$
+^\[main\.\d+] line 23 Check that s is assignable: SUCCESS$
+^\[main\.\d+] line 24 Check that a is assignable: SUCCESS$
+^\[main\.\d+] line 27 Check that s is assignable: SUCCESS$
+^\[main\.assertion.\d+\] .* assertion s == n: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 This test checks that nested loops, `for` loops,

regression/contracts/invar_check_pointer_modifies-01/test.desc

@@ -3,9 +3,11 @@ main.c
 --apply-loop-contracts --pointer-check
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.1\] .* Check loop invariant before entry: SUCCESS$
-^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
-^\[main.assertion.1\] .* assertion \*data = 42: SUCCESS$
+^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main\.\d+] .* Check that \*data is assignable: SUCCESS$
+^\[main\.\d+] .* Check that i is assignable: SUCCESS$
+^\[main\.assertion\.\d+\] .* assertion \*data = 42: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 ^\[main.pointer_dereference.*\] line .* dereference failure: pointer NULL in \*data: FAILURE

regression/contracts/invar_check_pointer_modifies-02/test.desc

@@ -3,10 +3,12 @@ main.c
 --apply-loop-contracts --pointer-check
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.1\] .* Check loop invariant before entry: SUCCESS$
-^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
-^\[main.assertion.1\] .* assertion data == copy: SUCCESS$
-^\[main.assertion.2\] .* assertion \*copy = 42: SUCCESS$
+^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main\.\d+\] .* Check that \*data is assignable: SUCCESS$
+^\[main\.\d+\] .* Check that i is assignable: SUCCESS$
+^\[main\.assertion\.\d+\] .* assertion data == copy: SUCCESS$
+^\[main\.assertion\.\d+\] .* assertion \*copy = 42: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 ^\[main.pointer_dereference.*\] line .* dereference failure: pointer NULL in \*data: FAILURE

regression/contracts/invar_check_sufficiency/test.desc

@@ -3,9 +3,10 @@ main.c
 --apply-loop-contracts
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.1\] .* Check loop invariant before entry: SUCCESS$
-^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
-^\[main.assertion.1\] .* assertion r == 0: SUCCESS$
+^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main\.\d+\] .* Check that r is assignable: SUCCESS$
+^\[main\.assertion\.1\] .* assertion r == 0: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 This test checks that a loop invariant can be proven to be inductive,

regression/contracts/invar_dynamic_struct_member/test.desc

@@ -3,8 +3,11 @@ main.c
 --apply-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.1\] .* Check loop invariant before entry: SUCCESS$
-^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main\.\d+\] .* Check that i is assignable: SUCCESS$
+^\[main\.\d+\] line 22 Check that t->x is assignable: SUCCESS$
+^\[main\.\d+\] line 25 Check that t->x is assignable: SUCCESS$
 ^\[main.assertion.1\] .* assertion .*: FAILURE$
 ^VERIFICATION FAILED$
 --

regression/contracts/invar_havoc_dynamic_array/main.c

@@ -9,7 +9,10 @@ void main()
   data[5] = 0;
 
   for(unsigned i = 0; i < SIZE; i++)
+    // clang-format off
+    __CPROVER_assigns(i, __CPROVER_POINTER_OBJECT(data))
     __CPROVER_loop_invariant(i <= SIZE)
+    // clang-format on
     {
       data[i] = 1;
     }

regression/contracts/invar_havoc_dynamic_array/test.desc

@@ -3,10 +3,12 @@ main.c
 --apply-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.1\] .* Check loop invariant before entry: SUCCESS$
-^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
-^\[main.assertion.1\] .* assertion data\[5\] == 0: FAILURE$
-^\[main.assertion.2\] .* assertion data\[5\] == 1: FAILURE$
+^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main\.\d+\] .* Check that i is assignable: SUCCESS$
+^\[main\.\d+\] .* Check that data\[\(signed long (long )?int\)i\] is assignable: SUCCESS$
+^\[main\.assertion\.\d+\] .* assertion data\[5\] == 0: FAILURE$
+^\[main\.assertion\.\d+\] .* assertion data\[5\] == 1: FAILURE$
 ^VERIFICATION FAILED$
 --
 --

regression/contracts/invar_havoc_dynamic_array_const_idx/test.desc

@@ -3,10 +3,12 @@ main.c
 --apply-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.1\] .* Check loop invariant before entry: SUCCESS$
-^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
-^\[main.assertion.1\] .* assertion data\[1\] == 0 \|\| data\[1\] == 1: FAILURE$
-^\[main.assertion.2\] .* assertion data\[4\] == 0: SUCCESS$
+^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main\.\d+\] .* Check that i is assignable: SUCCESS$
+^\[main\.\d+\] .* Check that data\[\(signed long (long )?int\)1\] is assignable: SUCCESS$
+^\[main\.assertion\.\d+\] .* assertion data\[1\] == 0 \|\| data\[1\] == 1: FAILURE$
+^\[main\.assertion\.\d+\] .* assertion data\[4\] == 0: SUCCESS$
 ^VERIFICATION FAILED$
 --
 --

regression/contracts/invar_havoc_static_array/main.c

@@ -9,7 +9,10 @@ void main()
   data[5] = 0;
 
   for(unsigned i = 0; i < SIZE; i++)
+    // clang-format off
+    __CPROVER_assigns(i, __CPROVER_POINTER_OBJECT(data))
     __CPROVER_loop_invariant(i <= SIZE)
+    // clang-format on
     {
       data[i] = 1;
     }

regression/contracts/invar_havoc_static_array/test.desc

@@ -3,10 +3,12 @@ main.c
 --apply-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.1\] .* Check loop invariant before entry: SUCCESS$
-^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
-^\[main.assertion.1\] .* assertion data\[5\] == 0: FAILURE$
-^\[main.assertion.2\] .* assertion data\[5\] == 1: FAILURE$
+^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main\.\d+\] .* Check that i is assignable: SUCCESS$
+^\[main\.\d+\] .* Check that data\[\(signed long (long )?int\)i\] is assignable: SUCCESS$
+^\[main\.assertion\.\d+\] .* assertion data\[5\] == 0: FAILURE$
+^\[main\.assertion\.\d+\] .* assertion data\[5\] == 1: FAILURE$
 ^VERIFICATION FAILED$
 --
 --

regression/contracts/invar_havoc_static_array_const_idx/test.desc

@@ -3,10 +3,12 @@ main.c
 --apply-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.1\] .* Check loop invariant before entry: SUCCESS$
-^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
-^\[main.assertion.1\] .* assertion data\[1\] == 0 \|\| data\[1\] == 1: FAILURE$
-^\[main.assertion.2\] .* assertion data\[4\] == 0: SUCCESS$
+^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main\.\d+\] .* Check that i is assignable: SUCCESS$
+^\[main\.\d+\] .* Check that data\[\(signed long (long )?int\)1\] is assignable: SUCCESS$
+^\[main\.assertion\.\d+\] .* assertion data\[1\] == 0 \|\| data\[1\] == 1: FAILURE$
+^\[main\.assertion\.\d+\] .* assertion data\[4\] == 0: SUCCESS$
 ^VERIFICATION FAILED$
 --
 --

regression/contracts/invar_havoc_static_multi-dim_array/test.desc

@@ -3,10 +3,10 @@ main.c
 --apply-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.1\] .* Check loop invariant before entry: SUCCESS$
-^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
-^\[main.assertion.1\] .* assertion __CPROVER_same_object\(old_data123, &\(data\[1\]\[2\]\[3\]\)\): SUCCESS$
-^\[main.assertion.2\] .* assertion data\[1\]\[2\]\[3\] == 0: FAILURE$
+^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main\.assertion\.\d+\] .* assertion __CPROVER_same_object\(old_data123, &\(data\[1\]\[2\]\[3\]\)\): SUCCESS$
+^\[main\.assertion\.\d+\] .* assertion data\[1\]\[2\]\[3\] == 0: FAILURE$
 ^VERIFICATION FAILED$
 --
 --

regression/contracts/invar_havoc_static_multi-dim_array_all_const_idx/test.desc

@@ -3,10 +3,11 @@ main.c
 --apply-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.1\] .* Check loop invariant before entry: SUCCESS$
-^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
-^\[main.assertion.1\] .* assertion data\[4\]\[5\]\[6\] == 0: FAILURE$
-^\[main.assertion.2\] .* assertion data\[1\]\[2\]\[3\] == 0: SUCCESS$
+^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main\.\d+\] .* Check that data\[\(signed long (long )?int\)4\]\[\(signed long (long )?int\)5\]\[\(signed long (long )?int\)6\] is assignable: SUCCESS$
+^\[main\.assertion\.\d+\] .* assertion data\[4\]\[5\]\[6\] == 0: FAILURE$
+^\[main\.assertion\.\d+\] .* assertion data\[1\]\[2\]\[3\] == 0: SUCCESS$
 ^VERIFICATION FAILED$
 --
 --

regression/contracts/invar_havoc_static_multi-dim_array_partial_const_idx/main.c

@@ -11,7 +11,8 @@ void main()
   data[4][5][6] = 0;
 
   for(unsigned i = 0; i < SIZE; i++)
-    __CPROVER_loop_invariant(i <= SIZE)
+    __CPROVER_assigns(i, __CPROVER_POINTER_OBJECT(data))
+      __CPROVER_loop_invariant(i <= SIZE)
     {
       data[4][i][6] = 1;
     }

regression/contracts/invar_havoc_static_multi-dim_array_partial_const_idx/test.desc

@@ -3,10 +3,12 @@ main.c
 --apply-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.1\] .* Check loop invariant before entry: SUCCESS$
-^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
-^\[main.assertion.1\] .* assertion data\[1\]\[2\]\[3\] == 0: FAILURE$
-^\[main.assertion.2\] .* assertion data\[4\]\[5\]\[6\] == 0: FAILURE$
+^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main\.\d+\] .* Check that i is assignable: SUCCESS$
+^\[main\.\d+\] .* Check that data\[\(signed long (long )?int\)4\]\[\(signed long (long )?int\)i\]\[\(signed long (long )?int\)6\] is assignable: SUCCESS$
+^\[main\.assertion\.\d+\] .* assertion data\[1\]\[2\]\[3\] == 0: FAILURE$
+^\[main\.assertion\.\d+\] .* assertion data\[4\]\[5\]\[6\] == 0: FAILURE$
 ^VERIFICATION FAILED$
 --
 --

regression/contracts/invar_loop-entry_check/test.desc

@@ -3,15 +3,24 @@ main.c
 --apply-loop-contracts _ --pointer-primitive-check
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.1\] .* Check loop invariant before entry: SUCCESS$
-^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
-^\[main.assertion.1\] .* assertion \*x1 == z1: SUCCESS$
-^\[main.3\] .* Check loop invariant before entry: SUCCESS$
-^\[main.4\] .* Check that loop invariant is preserved: SUCCESS$
-^\[main.assertion.2\] .* assertion x2 == z2: SUCCESS$
-^\[main.5\] .* Check loop invariant before entry: SUCCESS$
-^\[main.6\] .* Check that loop invariant is preserved: SUCCESS$
-^\[main.assertion.3\] .* assertion \*\(s1\.n\) == \*\(s2->n\): SUCCESS$
+^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main\.assertion\.\d+\] .* assertion \*x1 == z1: SUCCESS$
+^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main\.assertion\.\d+\] .* assertion x2 == z2: SUCCESS$
+^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main\.\d+\] .* Check that y1 is assignable: SUCCESS$
+^\[main\.\d+\] line 18 Check that \*x1 is assignable: SUCCESS$
+^\[main\.\d+\] line 19 Check that \*x1 is assignable: SUCCESS$
+^\[main\.\d+\] .* Check that y2 is assignable: SUCCESS$
+^\[main\.\d+\] line 30 Check that x2 is assignable: SUCCESS$
+^\[main\.\d+\] line 31 Check that x2 is assignable: SUCCESS$
+^\[main\.\d+\] .* Check that y3 is assignable: SUCCESS$
+^\[main\.\d+\] .* Check that s0\.n is assignable: SUCCESS$
+^\[main\.\d+\] .* Check that s2->n is assignable: SUCCESS$
+^\[main\.assertion\.\d+\] .* assertion \*\(s1\.n\) == \*\(s2->n\): SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 --

regression/contracts/invar_loop-entry_fail/test.desc

@@ -3,8 +3,11 @@ main.c
 --apply-loop-contracts
 ^EXIT=(10|6)$
 ^SIGNAL=0$
-^\[main.1\] .* Check loop invariant before entry: SUCCESS$
-^\[main.2\] .* Check that loop invariant is preserved: FAILURE$
+^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] .* Check that loop invariant is preserved: FAILURE$
+^\[main\.\d+\] line 11 Check that y is assignable: SUCCESS$
+^\[main\.\d+\] line 12 Check that x is assignable: SUCCESS$
+^\[main\.\d+\] line 13 Check that x is assignable: SUCCESS$
 ^VERIFICATION FAILED$
 --
 --

regression/contracts/invar_loop_constant_fail/test.desc

@@ -3,10 +3,12 @@ main.c
 --apply-loop-contracts
 ^EXIT=10$
 ^SIGNAL=0$
-^\[main.1\] .* Check loop invariant before entry: SUCCESS$
-^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
-^\[main.assertion.1\] .* assertion r == 0: SUCCESS$
-^\[main.assertion.2\] .* assertion s == 1: FAILURE$
+^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main\.\d+\] .* Check that s is assignable: SUCCESS$
+^\[main\.\d+\] .* Check that r is assignable: SUCCESS$
+^\[main\.assertion\.\d+\] .* assertion r == 0: SUCCESS$
+^\[main\.assertion\.\d+\] .* assertion s == 1: FAILURE$
 ^VERIFICATION FAILED$
 --
 This test is expected to fail because it modifies a variable within a loop,

regression/contracts/invar_loop_constant_no_modify/test.desc

@@ -3,10 +3,11 @@ main.c
 --apply-loop-contracts
 ^EXIT=0$
 ^SIGNAL=0$
-^\[main.1\] .* Check loop invariant before entry: SUCCESS$
-^\[main.2\] .* Check that loop invariant is preserved: SUCCESS$
-^\[main.assertion.1\] .* assertion r == 0: SUCCESS$
-^\[main.assertion.2\] .* assertion s == 1: SUCCESS$
+^\[main\.\d+\] .* Check loop invariant before entry: SUCCESS$
+^\[main\.\d+\] .* Check that loop invariant is preserved: SUCCESS$
+^\[main\.\d+\] .* Check that r is assignable: SUCCESS$
+^\[main\.assertion\.\d+\] .* assertion r == 0: SUCCESS$
+^\[main\.assertion\.\d+\] .* assertion s == 1: SUCCESS$
 ^VERIFICATION SUCCESSFUL$
 --
 This test checks that variables that are not modified within the loop