// Purpose: test that macros 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 defines a macro called G, which takes a boolean input and returns false. The module has an LTL property which says that globally, the macro G(x) should return true.
// 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;

  define G(b: boolean) : boolean = false;

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

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

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