team-worthwhile/worthwhile — Issue #69: Variables in loops are not bound to function preconditions
Author: jspam
Created: 2012-02-18 23:44:36+00:00
State: open
Labels: prover

Try to prove the following program:

```
function Integer test(Integer i)
_requires i % 2 = 0
{
Integer murks := 0

while (murks = 0)
{
_assert i % 2 = 0
murks := 1
}

return i
}
```

The proof fails with the following counterexample:

```
(model
(define-fun i!2 () Int
(- 1))
(define-fun i!0 () Int
0)
(define-fun murks!1 () Int
0)
)
```

The value for ```i!2``` should not appear in the counterexample because ```i``` is an even number by precondition.

When the ```while``` loop is removed (i.e. the ```_assert``` is placed directly in the function's body), the program is correctly verified.