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 | |
| parent | 871e9be2f1f7cf654151a39ee7ced2cf1f862d1e (diff) | |
Dafny tests: Disabled SnapshotableTrees.dfy for now while performance issues are being investigated
| -rw-r--r-- | Test/dafny2/Answer | 4 | ||||
| -rw-r--r-- | Test/dafny2/SnapshotableTrees.dfy | 3 | ||||
| -rw-r--r-- | Test/dafny2/runtest.bat | 3 |
3 files changed, 3 insertions, 7 deletions
diff --git a/Test/dafny2/Answer b/Test/dafny2/Answer index eed3eaa0..9cb94f69 100644 --- a/Test/dafny2/Answer +++ b/Test/dafny2/Answer @@ -3,10 +3,6 @@ Dafny program verifier finished with 5 verified, 0 errors
--------------------- SnapshotableTrees.dfy --------------------
-
-Dafny program verifier finished with 36 verified, 0 errors
-
-------------------- TreeBarrier.dfy --------------------
Dafny program verifier finished with 8 verified, 0 errors
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;
diff --git a/Test/dafny2/runtest.bat b/Test/dafny2/runtest.bat index 6c723ea5..d7c0dc79 100644 --- a/Test/dafny2/runtest.bat +++ b/Test/dafny2/runtest.bat @@ -5,9 +5,10 @@ set BOOGIEDIR=..\..\Binaries set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe
set CSC=c:/Windows/Microsoft.NET/Framework/v4.0.30319/csc.exe
+REM soon again: SnapshotableTrees.dfy
for %%f in (
Classics.dfy
- SnapshotableTrees.dfy TreeBarrier.dfy
+ TreeBarrier.dfy
COST-verif-comp-2011-1-MaxArray.dfy
COST-verif-comp-2011-2-MaxTree-class.dfy
COST-verif-comp-2011-2-MaxTree-datatype.dfy
|