The following program verifies but should not, since variable ``a`` is read but not always defined. ``` from nagini_contracts.contracts import * @Pure def oops(i: int) -> int: if i > 0: a = 5 b = a return 5 oops(-2) ```