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