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