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/LitTriggers.dfy | |
| parent | fde628b5153b86f187f353c6f79113932c309abe (diff) | |
Enable autoTriggers in LitTriggers and SeqFromArray
Diffstat (limited to 'Test/dafny0/LitTriggers.dfy')
| -rw-r--r-- | Test/dafny0/LitTriggers.dfy | 6 |
1 files changed, 5 insertions, 1 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:
|