bug.lus

node integ(x : int) returns (sum : int);
let
  sum = x + (0 -> pre sum);
tel;

node main(x : int; y : int) returns (z : int);
var
  history : bool;
  prop : bool;
let
  z = integ(x);

  history = x > 0 and (true -> pre history);
  prop = history => z > 0;
  --%PROPERTY prop;
tel;