const bound: int = 128;

node limiter(x: int; d: int) returns (probe y: int)
    var s, r: int;
    let
        assume in_bounded: x >= -bound and x <= bound;
        assume d_bounded: d = 16;
        guarantee out_bounded: y >= -bound and y <= bound;
        s = 0 -> pre y;
        r = x - s;
        activate
          if r <= -d then
            let y = s - d; tel
          else if r >= d then
            let y = s + d; tel
          else 
            let y = x; tel
        returns y;
    tel

node test(i: int) returns(a, b, c: int; exit: bool)
    let
        exit = i >= 30;
        a = (i * 21 + 122) mod (2 * bound + 1) - bound;  -- not really random
        b = 16;
        c = limiter(a, b);
    tel