// Purpose: test that functions should not be allowed the same names as LTL operators
// Description: One module. The module has a boolean state variable, x, which is initialised as true and remains unchanged in the next block. The module declares an uninterpreted function called G. The module has an LTL property which says that globally, the uninterpreted function should return true when applid to the state var x.
// Expectation: assertions should fail, or UCLID should throw an error about clashing names of LTL operators and functions
// Validation: this currently is a bug? Adding a check to the LTL operator rewriter pass would validate the test


module main
{
  var x : boolean;

  function G(b: boolean) : boolean;

  init {
    x=true;
  }
  next {
    x' = x;
  }

  property[LTL] p1 : G(G(x));

  control {
    // print_module;
    vobj = bmc(3);
    check;
    print_results;
  }
}
