team-worthwhile/worthwhile — Issue #19: Worthwhile reports Z3 timeout although Z3 is still running
Author: tbormer
Created: 2012-02-07 17:05:42+00:00
State: open

Steps to reproduce:

```Integer x
Integer y
Integer z := 0
Integer oldX := x
Integer oldY := y

while (y != 0)
_invariant y >= 0 && oldX * oldY = x * y + z
{
if (y / 2 * 2 != y) {
z := x + z
y := y / 2
x := 2 * x
}

if (y / 2 * 2 = y) {
y := y / 2
x := 2 * x
}
}
_assert z = oldX * oldY
```