blob: e3257cc02924e95c956b243d5a7c3ca50175ba24 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
|
function test(probe i: int) returns(probe a, b, c: int; exit: bool)
let
assume i_bounded : i >= -10 and i <= 10;
a = i;
guarantee a_eq_i : a = i;
b = 0;
c = 0;
exit = i >= 5;
tel
|