node test(i: int) returns (probe a, probe b, probe c: int; exit: bool)
var
  la, lb: int;
  half: bool;
let
  exit = i >= 20;

  half = true -> not pre half;

  la = 0 -> pre a;
  lb = 0 -> pre b;
  activate
    if half then
      let
        a = la + 1;
        b = lb;
      tel
    else
      let
        a = la;
        b = lb + 1;
      tel
  returns a, b;

  c = a - b;

  guarantee c_bounded: c >= 0 and c <= 1;
  guarantee link_c_half: (half and c = 1) or ((not half) and c = 0);
tel