test.lus

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

node main(x : int; y : int; r : real) returns (z : int);
var
  history : bool;
  prop1 : bool;
  prop2 : bool;
let
  z = integ(x);

  history = x > 0 and (true -> pre history);
  prop1 = history => z > 0;

  --%PROPERTY prop1;

  prop2 = integ(x) + integ(y) = integ(x + y) -> pre(integ(x) + integ(y) = integ(x + y) -> not(0.0 < r and r < 1.0));
  --%PROPERTY prop2;
tel;