1 files changed, 48 insertions, 0 deletions
diff --git a/Test/triggers/some-proofs-only-work-without-autoTriggers.dfy b/Test/triggers/some-proofs-only-work-without-autoTriggers.dfy
new file mode 100644
index 00000000..bc2e0934
--- /dev/null
+++ b/Test/triggers/some-proofs-only-work-without-autoTriggers.dfy
@@ -0,0 +1,48 @@
+// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 /printTooltips "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// The examples below work nicely with /autoTriggers:0, but break when we use
+// /autoTriggers.
+
+// The issue is that the axioms for sequences are missing a number of facts,
+// which was not a problem before /autoTriggers and /stricterTriggers, but has
+// become one. Here are examples of things that Dafny won’t prove with
+// /autoTriggers (I would expect it wouldn’t with stricterTriggers either,
+// though the second example is trickier than the first):
+
+method M(a: seq<int>) {
+  if * {
+    // This fails; it needs the following axiom:
+    //   axiom (forall<T> s: Seq T ::
+    //    { Seq#Take(s, Seq#Length(s)) }
+    //    Seq#Take(s, Seq#Length(s)) == s);
+    assume forall x :: x in a ==> x > 0;
+    assert forall x :: x in a[..|a|] ==> x > 0;
+  } else if * {
+    // This fails; it needs the following axiom:
+    //   axiom (forall<T> s: Seq T, i: int ::
+    //    { Seq#Index(s, i) }
+    //    0 <= i && i < Seq#Length(s) ==>
+    //    Seq#Contains(s, Seq#Index(s, i)));
+    assume forall x :: x in a ==> x > 0;
+    assert forall i | 0 <= i < |a| ::  a[i] > 0;
+  } else if * {
+    assume |a| > 3;
+    assume forall x | x in a[..3] :: x > 1;
+    // This fails, but here it's a lot harder to know what a good axiom would be.
+    assert forall x | x in a[..2] :: x > 1;
+  }
+}
+
+
+// In the first case, the Boogie version is
+//
+//   Seq#Contains(Seq#Take(a#0, Seq#Length(a#0)), $Box(x#0_1)) ⟹ x#0_1 > 0
+//
+// And of course Z3 picks $Box(x#0_1). The third case is similar.
+//
+// The problem is of course that knowing that x ∈ a[..2] doesn’t magically give
+// you a term that matches x ∈ a[..3]. One could imagine introducing an extra
+// symbol in the translation to put x and a together for triggering purposes,
+// but that would have the same sort of issues as adding symbols for arithmetic
+// operators.