[Eva] The automatic loop unrolling supports nested loop exit conditions.
This is required to automatically unroll loops with conditions such as `nondet && x < 100`, as this is converted by the Frama-C kernel as two nested conditional statements, where only the second one can be used to unroll the loop.
Loading
Please register or sign in to comment