diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-12-07 00:23:08 -0800 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-12-07 00:23:08 -0800 |
| commit | 714f99d776c21d8a1b50e0020eb678414a0cf67d (patch) | |
| tree | c030d98b2d38f6457af5ddc86a9bbbe937718c2b /Test/dafny2/SnapshotableTrees.dfy | |
| parent | 871e9be2f1f7cf654151a39ee7ced2cf1f862d1e (diff) | |
Dafny tests: Disabled SnapshotableTrees.dfy for now while performance issues are being investigated
Diffstat (limited to 'Test/dafny2/SnapshotableTrees.dfy')
| -rw-r--r-- | Test/dafny2/SnapshotableTrees.dfy | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/Test/dafny2/SnapshotableTrees.dfy b/Test/dafny2/SnapshotableTrees.dfy index f711e758..2c7a91df 100644 --- a/Test/dafny2/SnapshotableTrees.dfy +++ b/Test/dafny2/SnapshotableTrees.dfy @@ -250,7 +250,6 @@ class Node 0 <= pos < |r.Contents| == |n.Contents| + 1 &&
r.Contents == n.Contents[..pos] + [x] + n.Contents[pos..];
decreases if n == null then {} else n.Repr;
-/* Commented out while performance issues with the prover and going into SMTLib2 mode are being investigated.
{
if (n == null) {
r := new Node.Init(x);
@@ -287,7 +286,7 @@ class Node r, pos := n, -1;
}
}
-*/
+
method MutatingInsert(x: int) returns (ghost pos: int)
requires Valid();
modifies Repr;
|