diff options
| -rw-r--r-- | Test/dafny0/LitTriggers.dfy | 6 | ||||
| -rw-r--r-- | Test/dafny0/SeqFromArray.dfy | 8 | ||||
| -rw-r--r-- | Test/dafny4/NumberRepresentations.dfy | 4 |
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:
|