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')

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