predicate status(var int: stat);@\Vlabel{line:6:status}@
function var STATUS: status() =
  let {
    var STATUS: stat;
    constraint status(stat);
  } in stat;