diff options
| author |  Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-07-17 11:49:37 -0700 |
|---|---|---|
| committer | Clément Pit--Claudel <clement.pitclaudel@live.com> | 2015-07-17 11:49:37 -0700 |
| commit | d9e4d4e4979ecb10f18583f51cd94e71a4dca9a4 (patch) | |
| tree | 2ef326f66aad4f3cac93dca3c547e9e4a3327e4f /Test/dafny0/SeqFromArray.dfy | |
| parent | fde628b5153b86f187f353c6f79113932c309abe (diff) | |
Enable autoTriggers in LitTriggers and SeqFromArray
Diffstat (limited to 'Test/dafny0/SeqFromArray.dfy')
| -rw-r--r-- | Test/dafny0/SeqFromArray.dfy | 8 |
1 files changed, 7 insertions, 1 deletions
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:
|