node test() returns(x, y, probe z: int; a, b: bool)
var px, py: int;
let
  a = false -> pre b;
  b = true -> not pre a;

  px = pre x;
  py = pre y;

  x = 0 -> (if a = b then px + 1 else px);
  y = 0 -> (if a = b then py else py + 1);

  z = x - y;

  guarantee g1: x >= y;
tel