summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar leino <unknown>2015-06-12 15:59:17 -0700
committerGravatar leino <unknown>2015-06-12 15:59:17 -0700
commit19176cf2d4ae511bcfb32ea2d417dae83861728a (patch)
tree9f23b751813e36ed0178157e65ecae1858ffefb9
parentee342d75f0237336a4f5624557707ce663b25e59 (diff)
Added /vcs... cop-out to test case to make it go through
-rw-r--r--Test/dafny4/NumberRepresentations.dfy2
1 files changed, 1 insertions, 1 deletions
diff --git a/Test/dafny4/NumberRepresentations.dfy b/Test/dafny4/NumberRepresentations.dfy
index 1ebdf64c..8a94505c 100644
--- a/Test/dafny4/NumberRepresentations.dfy
+++ b/Test/dafny4/NumberRepresentations.dfy
@@ -1,4 +1,4 @@
-// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
+// RUN: %dafny /compile:0 /vcsMaxKeepGoingSplits:5 /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
// We consider a number representation that consists of a sequence of digits. The least