summaryrefslogtreecommitdiff
path: root/Test/dafny2
diff options
context:
space:
mode:
authorGravatar leino <unknown>2014-10-21 01:23:06 -0700
committerGravatar leino <unknown>2014-10-21 01:23:06 -0700
commit5de2cc263ce26929baf03ca32c4d6738813db002 (patch)
treebb10567e46087f54245cd17857400055bb7889aa /Test/dafny2
parentbf6de3d13197e1635a4d9fe807b3f4b45113ae6a (diff)
Added VC Splitting switch to dafny2/SnapshotableTrees.dfy to try to avoid some brittleness
Diffstat (limited to 'Test/dafny2')
-rw-r--r--Test/dafny2/SnapshotableTrees.dfy2
1 files changed, 1 insertions, 1 deletions
diff --git a/Test/dafny2/SnapshotableTrees.dfy b/Test/dafny2/SnapshotableTrees.dfy
index f71cf5d3..96d3707f 100644
--- a/Test/dafny2/SnapshotableTrees.dfy
+++ b/Test/dafny2/SnapshotableTrees.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" /vcsMaxKeepGoingSplits:10 "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
// Rustan Leino, September 2011.