Bug: Loop invariants in correctness witnesses produced by UAutomizer refer to out-of-bound variables

[Po-Chun-Chien]

Basic Info

• Version: 0e0057cc (downloaded from tool archive of SV-COMP 2024)
• Input file: cal57.c with property unreach-call.prp

Description

The loop invariant in a correctness witness generated by UAutomizer might contain out-of-bound program variables, making the invariant syntactically incorrect.

Here's an example witness obtained by running the following command:

./Ultimate.py --spec ../unreach-call.prp --file ../cal57.c --full-output --architecture 64bit

This is the invariant generated for the loop at line 42 of the program:

<node id="N29">
<data key="invariant">((((((((((1 == mask_SORT_1) &amp;&amp; (7 == mask_SORT_5)) &amp;&amp; (1 == var_31)) &amp;&amp; (0 == state_12)) &amp;&amp; (0 == state_18)) &amp;&amp; (var_15 == 0)) &amp;&amp; (1 == var_21)) &amp;&amp; (var_11 == 0)) || (((((((((1 == mask_SORT_1) &amp;&amp; (1 == state_12)) &amp;&amp; (1 == state_18)) &amp;&amp; (7 == mask_SORT_5)) &amp;&amp; (1 == var_31)) &amp;&amp; ((!((var_25 == 1)) &amp;&amp; !((var_20 == 1))) || ((var_20 == 1) &amp;&amp; (var_25 == 1)))) &amp;&amp; (var_15 == 0)) &amp;&amp; (1 == var_21)) &amp;&amp; (var_11 == 0))) || ((((((((1 == mask_SORT_1) &amp;&amp; (1 == state_12)) &amp;&amp; (7 == mask_SORT_5)) &amp;&amp; (1 == var_31)) &amp;&amp; (0 == state_18)) &amp;&amp; (var_15 == 0)) &amp;&amp; (1 == var_21)) &amp;&amp; (var_11 == 0)))</data>

The invariant refer to variables var_20 and var_25, which are declared inside the loop at line 68 and 75, respectively. Therefore, the invariant is syntactically wrong.

[schuessf]

Thank you for your report! I just fixed this problem, we did not handle the scope of for-loops fully correct, as a for-loop has usually two scopes: the initializer and the body.