From 9f8cb23ad0662cea28f681872236277c2af2432e Mon Sep 17 00:00:00 2001
From: Clément Pit--Claudel <clement.pitclaudel@live.com>
Date: Thu, 16 Jul 2015 14:27:28 -0700
Subject: Strip literals from triggers

---
 Test/dafny0/LitTriggers.dfy | 35 +++++++++++++++++++++++++++++++++++
 1 file changed, 35 insertions(+)
 create mode 100644 Test/dafny0/LitTriggers.dfy

(limited to 'Test/dafny0/LitTriggers.dfy')

diff --git a/Test/dafny0/LitTriggers.dfy b/Test/dafny0/LitTriggers.dfy
new file mode 100644
index 00000000..14880d68
--- /dev/null
+++ b/Test/dafny0/LitTriggers.dfy
@@ -0,0 +1,35 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// Imported from bug 76. LitInt would be triggered on, causing matching failures.
+
+predicate P(x:int, y:int)
+
+lemma L1(x:int, y:int)
+    requires y == 2;
+    requires forall i :: P(i, 3);
+{
+    assert P(x, y + 1);
+}
+
+lemma L2(x:int, y:int)
+    requires y == 2;
+    requires forall i {:trigger P(i, 3)} :: P(i, 3);
+{
+    assert P(x, y + 1);
+}
+
+lemma L3(x:int, y:int)
+    requires y == 2;
+    requires forall i :: P(i, 3);
+{
+    var dummy := 3;
+    assert P(x, y + 1);
+}
+
+lemma L4(x:int, y:int)
+    requires y == 2;
+    requires forall i, j :: j == 3 ==> P(i, j);
+{
+    assert P(x, y + 1);
+}
-- 
cgit v1.2.3


From d9e4d4e4979ecb10f18583f51cd94e71a4dca9a4 Mon Sep 17 00:00:00 2001
From: Clément Pit--Claudel <clement.pitclaudel@live.com>
Date: Fri, 17 Jul 2015 11:49:37 -0700
Subject: Enable autoTriggers in LitTriggers and SeqFromArray

---
 Test/dafny0/LitTriggers.dfy           | 6 +++++-
 Test/dafny0/SeqFromArray.dfy          | 8 +++++++-
 Test/dafny4/NumberRepresentations.dfy | 4 ++++
 3 files changed, 16 insertions(+), 2 deletions(-)

(limited to 'Test/dafny0/LitTriggers.dfy')

diff --git a/Test/dafny0/LitTriggers.dfy b/Test/dafny0/LitTriggers.dfy
index 14880d68..93e65643 100644
--- a/Test/dafny0/LitTriggers.dfy
+++ b/Test/dafny0/LitTriggers.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 // Imported from bug 76. LitInt would be triggered on, causing matching failures.
@@ -33,3 +33,7 @@ lemma L4(x:int, y:int)
 {
     assert P(x, y + 1);
 }
+
+// Local Variables:
+// dafny-prover-local-args: ("/autoTriggers:1")
+// End:
diff --git a/Test/dafny0/SeqFromArray.dfy b/Test/dafny0/SeqFromArray.dfy
index 3a8760ba..629c5045 100644
--- a/Test/dafny0/SeqFromArray.dfy
+++ b/Test/dafny0/SeqFromArray.dfy
@@ -1,6 +1,8 @@
-// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %dafny /compile:3 /print:"%t.print" /dprint:"%t.dprint" /autoTriggers:1 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
+// /autoTriggers:1 added to suppress instabilities
+
 method Main() { }
 
 method H(a: array<int>, c: array<int>, n: nat, j: nat)
@@ -88,3 +90,7 @@ method M(a: array<int>, c: array<int>, m: nat, n: nat, k: nat, l: nat)
       assert a[k..k+m] == c[l+k..l+k+m];
   }
 }
+
+// Local Variables:
+// dafny-prover-local-args: ("/autoTriggers:1")
+// End:
diff --git a/Test/dafny4/NumberRepresentations.dfy b/Test/dafny4/NumberRepresentations.dfy
index 8a94505c..f51ae924 100644
--- a/Test/dafny4/NumberRepresentations.dfy
+++ b/Test/dafny4/NumberRepresentations.dfy
@@ -293,3 +293,7 @@ lemma MulInverse(x: int, a: int, b: int, y: int)
   ensures a == b;
 {
 }
+
+// Local Variables:
+// dafny-prover-local-args: ("/vcsMaxKeepGoingSplits:5")
+// End:
-- 
cgit v1.2.3