Enable autoTriggers in LitTriggers and SeqFromArray

3 files changed, 16 insertions, 2 deletions

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: