// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"
// RUN: %diff "%s.expect" "%t"

// This test checks for tricky cases of redundancy suppression when building
// triggers.

predicate P(x: int, y: int)
predicate Q(x: int)
predicate R(x: int)

method M() {
  // For this term, it is enough to order the terms by number of variables
  assert forall x, y :: true || P(x, y) || Q(y) || R(x);
  assert forall x, y :: true || Q(y) || P(x, y) || R(x);
  assert forall x, y :: true || Q(y) || R(x) || P(x, y);
}

predicate PP(x: int, y: int, z: int)
predicate QQ(x: int, y: int)
predicate RR(x: int, y: int)
predicate SS(x: int, y: int)

method MM() {
  // Not for this one, though
  assert forall x, y, z, u, v, w :: true || PP(x, y, z) || QQ(x, u) || RR(y, v) || SS(z, w);
  assert forall x, y, z, u, v, w :: true || QQ(x, u) || PP(x, y, z) || RR(y, v) || SS(z, w);
  assert forall x, y, z, u, v, w :: true || QQ(x, u) || RR(y, v) || PP(x, y, z) || SS(z, w);
  assert forall x, y, z, u, v, w :: true || QQ(x, u) || RR(y, v) || SS(z, w) || PP(x, y, z);
}