Undo bad merge.

27 files changed, 0 insertions, 1349 deletions

diff --git a/Test/VSComp2010/AnswerNoRuntimeChecking b/Test/VSComp2010/AnswerNoRuntimeChecking
deleted file mode 100644
index d0492caf..00000000
--- a/Test/VSComp2010/AnswerNoRuntimeChecking
+++ /dev/null
@@ -1,15 +0,0 @@
-

--------------------- Problem1-SumMax --------------------

-Compiled assembly into Problem1-SumMax.exe

-

--------------------- Problem2-Invert --------------------

-Compiled assembly into Problem2-Invert.exe

-

--------------------- Problem3-FindZero --------------------

-Compiled assembly into Problem3-FindZero.exe

-

--------------------- Problem4-Queens --------------------

-Compiled assembly into Problem4-Queens.exe

-

--------------------- Problem5-DoubleEndedQueue --------------------

-Compiled assembly into Problem5-DoubleEndedQueue.dll

diff --git a/Test/VSComp2010/AnswerRuntimeChecking b/Test/VSComp2010/AnswerRuntimeChecking
deleted file mode 100644
index 858b6370..00000000
--- a/Test/VSComp2010/AnswerRuntimeChecking
+++ /dev/null
@@ -1,4 +0,0 @@
-

--------------------- Problem1-SumMax --------------------

-Compiled assembly into Problem1-SumMax.exe

-Rewrote assembly into Problem1-SumMax.exe

diff --git a/Test/VSComp2010/runtestNoRuntimeChecking.bat b/Test/VSComp2010/runtestNoRuntimeChecking.bat
deleted file mode 100644
index 4efd244a..00000000
--- a/Test/VSComp2010/runtestNoRuntimeChecking.bat
+++ /dev/null
@@ -1,28 +0,0 @@
-@echo off

-setlocal

-

-set BOOGIEDIR=..\..\Binaries

-set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe

-set BPLEXE=%BOOGIEDIR%\Boogie.exe

-

-for %%f in (Problem1-SumMax Problem2-Invert Problem3-FindZero

-            Problem4-Queens Problem5-DoubleEndedQueue) do (

-  echo.

-  echo -------------------- %%f --------------------

-  %DAFNY_EXE% /nologo /errorTrace:0 /verification:0 /runtimeChecking:0 /compile:2 %* %%f.dfy

-  if exist %%f.cs. (

-    del %%f.cs

-  )

-  if exist %%f.exe. (

-    del %%f.exe

-  )

-  if exist %%f.dll. (

-    del %%f.dll

-  )

-  if exist %%f.pdb. (

-    del %%f.pdb

-  )

-  if exist %%f.pdb.original. (

-    del %%f.pdb.original

-  )

-)

diff --git a/Test/VSComp2010/runtestRuntimeChecking.bat b/Test/VSComp2010/runtestRuntimeChecking.bat
deleted file mode 100644
index d3b8a733..00000000
--- a/Test/VSComp2010/runtestRuntimeChecking.bat
+++ /dev/null
@@ -1,33 +0,0 @@
-@echo off

-setlocal

-

-set BOOGIEDIR=..\..\Binaries

-set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe

-set BPLEXE=%BOOGIEDIR%\Boogie.exe

-

-REM to implement:

-REM Problem2-Invert          : quantifiers

-REM Problem3-FindZero        : ghost state

-REM Problem4-Queens          : quantifiers

-REM Problem5-DoubleEndedQueue: ghost state

-

-for %%f in (Problem1-SumMax) do (

-  echo.

-  echo -------------------- %%f --------------------

-  %DAFNY_EXE% /nologo /errorTrace:0 /verification:0 /runtimeChecking:1 /compile:2 %* %%f.dfy

-  if exist %%f.cs. (

-    del %%f.cs

-  )

-  if exist %%f.exe. (

-    del %%f.exe

-  )

-  if exist %%f.dll. (

-    del %%f.dll

-  )

-  if exist %%f.pdb. (

-    del %%f.pdb

-  )

-  if exist %%f.pdb.original. (

-    del %%f.pdb.original

-  )

-)

diff --git a/Test/VSI-Benchmarks/AnswerNoRuntimeChecking b/Test/VSI-Benchmarks/AnswerNoRuntimeChecking
deleted file mode 100644
index 81ac67ef..00000000
--- a/Test/VSI-Benchmarks/AnswerNoRuntimeChecking
+++ /dev/null
@@ -1,32 +0,0 @@
-

--------------------- b1 --------------------

-Compiled assembly into b1.exe

-

--------------------- b2 --------------------

-Compiled assembly into b2.exe

-

--------------------- b3 --------------------

-Compilation error: Method _default.Queue.Init has no body

-Compilation error: Method _default.Queue.Enqueue has no body

-Compilation error: Method _default.Queue.Dequeue has no body

-

--------------------- b4 --------------------

-Compiled assembly into b4.dll

-

--------------------- b5 --------------------

-Compiled assembly into b5.dll

-

--------------------- b6 --------------------

-Compiled assembly into b6.exe

-

--------------------- b7 --------------------

-Compilation error: Method _default.Queue.Init has no body

-Compilation error: Method _default.Queue.Enqueue has no body

-Compilation error: Method _default.Queue.Dequeue has no body

-Compilation error: Method _default.Client.Sort has no body

-

--------------------- b8 --------------------

-Compilation error: Method _default.Queue.Init has no body

-Compilation error: Method _default.Queue.Enqueue has no body

-Compilation error: Method _default.Queue.Dequeue has no body

-Compilation error: Method _default.Glossary.Sort has no body

diff --git a/Test/VSI-Benchmarks/AnswerRuntimeChecking b/Test/VSI-Benchmarks/AnswerRuntimeChecking
deleted file mode 100644
index 49a440db..00000000
--- a/Test/VSI-Benchmarks/AnswerRuntimeChecking
+++ /dev/null
@@ -1,21 +0,0 @@
-

--------------------- b1 --------------------

-Compiled assembly into b1.exe

-Rewrote assembly into b1.exe

-

--------------------- b3 --------------------

-Compilation error: Method _default.Queue.Init has no body

-Compilation error: Method _default.Queue.Enqueue has no body

-Compilation error: Method _default.Queue.Dequeue has no body

-

--------------------- b7 --------------------

-Compilation error: Method _default.Queue.Init has no body

-Compilation error: Method _default.Queue.Enqueue has no body

-Compilation error: Method _default.Queue.Dequeue has no body

-Compilation error: Method _default.Client.Sort has no body

-

--------------------- b8 --------------------

-Compilation error: Method _default.Queue.Init has no body

-Compilation error: Method _default.Queue.Enqueue has no body

-Compilation error: Method _default.Queue.Dequeue has no body

-Compilation error: Method _default.Glossary.Sort has no body

diff --git a/Test/VSI-Benchmarks/runtestNoRuntimeChecking.bat b/Test/VSI-Benchmarks/runtestNoRuntimeChecking.bat
deleted file mode 100644
index c85b7606..00000000
--- a/Test/VSI-Benchmarks/runtestNoRuntimeChecking.bat
+++ /dev/null
@@ -1,27 +0,0 @@
-@echo off

-setlocal

-

-set BOOGIEDIR=..\..\Binaries

-set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe

-set BPLEXE=%BOOGIEDIR%\Boogie.exe

-

-for %%f in (b1 b2 b3 b4 b5 b6 b7 b8) do (

-  echo.

-  echo -------------------- %%f --------------------

-  %DAFNY_EXE% /nologo /errorTrace:0 /verification:0 /runtimeChecking:0 /compile:2 %* %%f.dfy

-  if exist %%f.cs. (

-    del %%f.cs

-  )

-  if exist %%f.exe. (

-    del %%f.exe

-  )

-  if exist %%f.dll. (

-    del %%f.dll

-  )

-  if exist %%f.pdb. (

-    del %%f.pdb

-  )

-  if exist %%f.pdb.original. (

-    del %%f.pdb.original

-  )

-)

diff --git a/Test/VSI-Benchmarks/runtestRuntimeChecking.bat b/Test/VSI-Benchmarks/runtestRuntimeChecking.bat
deleted file mode 100644
index 27df70a3..00000000
--- a/Test/VSI-Benchmarks/runtestRuntimeChecking.bat
+++ /dev/null
@@ -1,33 +0,0 @@
-@echo off

-setlocal

-

-set BOOGIEDIR=..\..\Binaries

-set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe

-set BPLEXE=%BOOGIEDIR%\Boogie.exe

-

-REM to implement:

-REM b2: quantifiers

-REM b4: old expressions

-REM b5: parallel statements

-REM b6: functions

-

-for %%f in (b1 b3 b7 b8) do (

-  echo.

-  echo -------------------- %%f --------------------

-  %DAFNY_EXE% /nologo /errorTrace:0 /verification:0 /runtimeChecking:1 /compile:2 %* %%f.dfy

-  if exist %%f.cs. (

-    del %%f.cs

-  )

-  if exist %%f.exe. (

-    del %%f.exe

-  )

-  if exist %%f.dll. (

-    del %%f.dll

-  )

-  if exist %%f.pdb. (

-    del %%f.pdb

-  )

-  if exist %%f.pdb.original. (

-    del %%f.pdb.original

-  )

-)

diff --git a/Test/dafny0/AnswerNoRuntimeChecking b/Test/dafny0/AnswerNoRuntimeChecking
deleted file mode 100644
index 04ece8ae..00000000
--- a/Test/dafny0/AnswerNoRuntimeChecking
+++ /dev/null
@@ -1,328 +0,0 @@
-

--------------------- Simple --------------------

-Compilation error: compilation of set<object> is not supported; consider introducing a ghost

-

--------------------- TypeTests --------------------

-TypeTests.dfy(89,9): Error: sorry, cannot instantiate collection type with a subrange type

-TypeTests.dfy(4,13): Error: incorrect type of function argument 0 (expected C, got D)

-TypeTests.dfy(4,13): Error: incorrect type of function argument 1 (expected D, got C)

-TypeTests.dfy(5,13): Error: incorrect type of function argument 0 (expected C, got int)

-TypeTests.dfy(5,13): Error: incorrect type of function argument 1 (expected D, got int)

-TypeTests.dfy(11,15): Error: incorrect type of method in-parameter 0 (expected int, got bool)

-TypeTests.dfy(12,11): Error: incorrect type of method out-parameter 0 (expected int, got C)

-TypeTests.dfy(12,11): Error: incorrect type of method out-parameter 1 (expected C, got int)

-TypeTests.dfy(44,9): Error: Assignment to array element is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)

-TypeTests.dfy(53,6): Error: Duplicate local-variable name: z

-TypeTests.dfy(55,6): Error: Duplicate local-variable name: x

-TypeTests.dfy(58,8): Error: Duplicate local-variable name: x

-TypeTests.dfy(61,6): Error: Duplicate local-variable name: y

-TypeTests.dfy(68,17): Error: member F in type C does not refer to a method

-TypeTests.dfy(69,17): Error: a method called as an initialization method must not have any result arguments

-TypeTests.dfy(78,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)

-TypeTests.dfy(78,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)

-TypeTests.dfy(79,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)

-TypeTests.dfy(79,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)

-TypeTests.dfy(80,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)

-TypeTests.dfy(80,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)

-TypeTests.dfy(82,2): Error: LHS of array assignment must denote an array element (found seq<C>)

-TypeTests.dfy(82,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)

-TypeTests.dfy(82,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)

-TypeTests.dfy(83,2): Error: LHS of array assignment must denote an array element (found seq<C>)

-TypeTests.dfy(83,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)

-TypeTests.dfy(83,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)

-TypeTests.dfy(84,2): Error: LHS of array assignment must denote an array element (found seq<C>)

-TypeTests.dfy(84,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)

-TypeTests.dfy(84,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)

-TypeTests.dfy(90,9): Error: sorry, cannot instantiate type parameter with a subrange type

-TypeTests.dfy(91,8): Error: sorry, cannot instantiate 'array' type with a subrange type

-TypeTests.dfy(92,8): Error: sorry, cannot instantiate 'array' type with a subrange type

-TypeTests.dfy(18,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NeverendingList' can be constructed

-34 resolution/type errors detected in TypeTests.dfy

-

--------------------- NatTypes --------------------

-Compilation error: compilation does not support type 'object' as a type parameter; consider introducing a ghost

-Compilation error: compilation does not support type 'object' as a type parameter; consider introducing a ghost

-Compilation error: compilation does not support type 'object' as a type parameter; consider introducing a ghost

-Compilation error: compilation does not support type 'object' as a type parameter; consider introducing a ghost

-Compilation error: compilation does not support type 'object' as a type parameter; consider introducing a ghost

-Compilation error: compilation does not support type 'object' as a type parameter; consider introducing a ghost

-

--------------------- SmallTests --------------------

-Compilation error: an assume statement cannot be compiled (line 13)

-Compilation error: compilation of seq<object> is not supported; consider introducing a ghost

-Compilation error: compilation of seq<object> is not supported; consider introducing a ghost

-Compilation error: compilation of seq<object> is not supported; consider introducing a ghost

-Compilation error: an assume statement cannot be compiled (line 545)

-Compilation error: an assume statement cannot be compiled (line 554)

-Compilation error: an assume statement cannot be compiled (line 556)

-Compilation error: an assume statement cannot be compiled (line 559)

-Compilation error: an assume statement cannot be compiled (line 571)

-Compilation error: an assume statement cannot be compiled (line 574)

-Compilation error: an assume statement cannot be compiled (line 575)

-Compilation error: an assume statement cannot be compiled (line 577)

-Compilation error: an assume statement cannot be compiled (line 584)

-Compilation error: an assume statement cannot be compiled (line 590)

-Compilation error: an assume statement cannot be compiled (line 596)

-Compilation error: an assume statement cannot be compiled (line 603)

-

--------------------- Definedness --------------------

-Compilation error: an assume statement cannot be compiled (line 93)

-

--------------------- FunctionSpecifications --------------------

-Compiled assembly into FunctionSpecifications.dll

-

--------------------- ResolutionErrors --------------------

-ResolutionErrors.dfy(48,13): Error: 'this' is not allowed in a 'static' context

-ResolutionErrors.dfy(109,9): Error: ghost variables are allowed only in specification contexts

-ResolutionErrors.dfy(110,9): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')

-ResolutionErrors.dfy(114,11): Error: ghost variables are allowed only in specification contexts

-ResolutionErrors.dfy(115,9): Error: actual out-parameter 0 is required to be a ghost variable

-ResolutionErrors.dfy(122,15): Error: ghost variables are allowed only in specification contexts

-ResolutionErrors.dfy(126,23): Error: ghost variables are allowed only in specification contexts

-ResolutionErrors.dfy(133,4): Error: ghost variables are allowed only in specification contexts

-ResolutionErrors.dfy(137,21): Error: ghost variables are allowed only in specification contexts

-ResolutionErrors.dfy(138,35): Error: ghost variables are allowed only in specification contexts

-ResolutionErrors.dfy(147,9): Error: only ghost methods can be called from this context

-ResolutionErrors.dfy(153,16): Error: 'decreases *' is not allowed on ghost loops

-ResolutionErrors.dfy(194,27): Error: ghost-context break statement is not allowed to break out of non-ghost structure

-ResolutionErrors.dfy(217,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop

-ResolutionErrors.dfy(229,12): Error: trying to break out of more loop levels than there are enclosing loops

-ResolutionErrors.dfy(233,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop

-ResolutionErrors.dfy(238,8): Error: return statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)

-ResolutionErrors.dfy(10,16): Error: 'decreases *' is not allowed on ghost loops

-ResolutionErrors.dfy(22,11): Error: array selection requires an array2 (got array3<T>)

-ResolutionErrors.dfy(23,12): Error: sequence/array/map selection requires a sequence, array or map (got array3<T>)

-ResolutionErrors.dfy(24,11): Error: array selection requires an array4 (got array<T>)

-ResolutionErrors.dfy(54,14): Error: a field must be selected via an object, not just a class name

-ResolutionErrors.dfy(55,7): Error: unresolved identifier: F

-ResolutionErrors.dfy(56,14): Error: an instance function must be selected via an object, not just a class name

-ResolutionErrors.dfy(56,7): Error: call to instance function requires an instance

-ResolutionErrors.dfy(57,7): Error: unresolved identifier: G

-ResolutionErrors.dfy(59,7): Error: unresolved identifier: M

-ResolutionErrors.dfy(60,7): Error: call to instance method requires an instance

-ResolutionErrors.dfy(61,7): Error: unresolved identifier: N

-ResolutionErrors.dfy(64,8): Error: non-function expression is called with parameters

-ResolutionErrors.dfy(65,14): Error: member z does not exist in class Global

-ResolutionErrors.dfy(84,12): Error: the name 'Benny' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.Benny')

-ResolutionErrors.dfy(89,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')

-ResolutionErrors.dfy(90,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')

-ResolutionErrors.dfy(92,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')

-ResolutionErrors.dfy(94,12): Error: wrong number of arguments to datatype constructor Abc (found 2, expected 1)

-ResolutionErrors.dfy(256,4): Error: label shadows an enclosing label

-ResolutionErrors.dfy(261,2): Error: duplicate label

-ResolutionErrors.dfy(287,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called

-ResolutionErrors.dfy(288,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called

-ResolutionErrors.dfy(290,4): Error: a constructor is only allowed to be called when an object is being allocated

-ResolutionErrors.dfy(304,16): Error: arguments must have the same type (got int and DTD_List)

-ResolutionErrors.dfy(305,16): Error: arguments must have the same type (got DTD_List and int)

-ResolutionErrors.dfy(306,25): Error: arguments must have the same type (got bool and int)

-ResolutionErrors.dfy(309,18): Error: ghost fields are allowed only in specification contexts

-ResolutionErrors.dfy(318,15): Error: ghost variables are allowed only in specification contexts

-ResolutionErrors.dfy(343,2): Error: incorrect type of method in-parameter 1 (expected GenericClass<int>, got GenericClass<bool>)

-ResolutionErrors.dfy(355,18): Error: incorrect type of datatype constructor argument (found GList<_T0>, expected GList<int>)

-48 resolution/type errors detected in ResolutionErrors.dfy

-

--------------------- ParseErrors --------------------

-ParseErrors.dfy(4,19): error: a chain cannot have more than one != operator

-ParseErrors.dfy(6,37): error: this operator chain cannot continue with a descending operator

-ParseErrors.dfy(7,38): error: this operator chain cannot continue with an ascending operator

-ParseErrors.dfy(12,24): error: this operator chain cannot continue with a descending operator

-ParseErrors.dfy(15,18): error: this operator cannot be part of a chain

-ParseErrors.dfy(16,19): error: this operator cannot be part of a chain

-ParseErrors.dfy(17,18): error: this operator cannot be part of a chain

-ParseErrors.dfy(18,18): error: chaining not allowed from the previous operator

-8 parse errors detected in ParseErrors.dfy

-

--------------------- Array --------------------

-Compilation error: Arbitrary type ('B') cannot be compiled

-

--------------------- MultiDimArray --------------------

-Compiled assembly into MultiDimArray.dll

-

--------------------- NonGhostQuantifiers --------------------

-NonGhostQuantifiers.dfy(146,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'

-NonGhostQuantifiers.dfy(150,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'

-NonGhostQuantifiers.dfy(155,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'

-NonGhostQuantifiers.dfy(160,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'

-NonGhostQuantifiers.dfy(164,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'

-NonGhostQuantifiers.dfy(168,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'

-NonGhostQuantifiers.dfy(173,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'

-NonGhostQuantifiers.dfy(178,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'

-NonGhostQuantifiers.dfy(183,13): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'c'

-NonGhostQuantifiers.dfy(13,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'n'

-NonGhostQuantifiers.dfy(42,4): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'n'

-NonGhostQuantifiers.dfy(46,4): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'd'

-NonGhostQuantifiers.dfy(50,4): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'n'

-NonGhostQuantifiers.dfy(74,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'i'

-NonGhostQuantifiers.dfy(78,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j'

-NonGhostQuantifiers.dfy(88,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j'

-NonGhostQuantifiers.dfy(103,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j'

-NonGhostQuantifiers.dfy(111,10): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'y'

-NonGhostQuantifiers.dfy(120,8): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'x'

-NonGhostQuantifiers.dfy(137,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)

-20 resolution/type errors detected in NonGhostQuantifiers.dfy

-

--------------------- AdvancedLHS --------------------

-Compiled assembly into AdvancedLHS.dll

-

--------------------- ModulesCycle --------------------

-ModulesCycle.dfy(12,7): Error: module T named among imports does not exist

-ModulesCycle.dfy(23,7): Error: import graph contains a cycle: H -> I -> J -> G

-2 resolution/type errors detected in ModulesCycle.dfy

-

--------------------- Modules0 --------------------

-Modules0.dfy(5,8): Error: Duplicate name of top-level declaration: WazzupA

-Modules0.dfy(6,11): Error: Duplicate name of top-level declaration: WazzupA

-Modules0.dfy(7,7): Error: Duplicate name of top-level declaration: WazzupA

-Modules0.dfy(10,7): Error: Duplicate name of top-level declaration: WazzupB

-Modules0.dfy(11,8): Error: Duplicate name of top-level declaration: WazzupB

-Modules0.dfy(12,11): Error: Duplicate name of top-level declaration: WazzupB

-Modules0.dfy(42,11): Error: The name T ambiguously refers to a type in one of the modules N, M

-Modules0.dfy(43,18): Error: The name T ambiguously refers to a type in one of the modules N, M

-Modules0.dfy(44,15): Error: The name T ambiguously refers to a type in one of the modules N, M

-Modules0.dfy(46,16): Error: The name T ambiguously refers to a type in one of the modules N, M

-Modules0.dfy(47,18): Error: The name T ambiguously refers to a type in one of the modules N, M

-Modules0.dfy(43,13): Error: Function body type mismatch (expected T, got T)

-Modules0.dfy(48,19): Error: The name T ambiguously refers to a type in one of the modules N, M

-Modules0.dfy(48,12): Error: new can be applied only to reference types (got T)

-Modules0.dfy(54,12): Error: Undeclared top-level type or type parameter: T (did you forget a module import?)

-Modules0.dfy(70,18): Error: Undeclared top-level type or type parameter: MyClass1 (did you forget a module import?)

-Modules0.dfy(71,18): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget a module import?)

-Modules0.dfy(81,18): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget a module import?)

-Modules0.dfy(105,16): Error: Undeclared top-level type or type parameter: ClassG (did you forget a module import?)

-Modules0.dfy(244,11): Error: Undeclared top-level type or type parameter: X (did you forget a module import?)

-Modules0.dfy(250,15): Error: unresolved identifier: X

-Modules0.dfy(251,17): Error: member DoesNotExist does not exist in class X

-Modules0.dfy(294,16): Error: member R does not exist in class B

-Modules0.dfy(294,6): Error: expected method call, found expression

-Modules0.dfy(140,11): Error: ghost variables are allowed only in specification contexts

-Modules0.dfy(154,11): Error: old expressions are allowed only in specification and ghost contexts

-Modules0.dfy(155,11): Error: fresh expressions are allowed only in specification and ghost contexts

-Modules0.dfy(156,11): Error: allocated expressions are allowed only in specification and ghost contexts

-Modules0.dfy(172,10): Error: match source expression 'tree' has already been used as a match source expression in this context

-Modules0.dfy(211,12): Error: match source expression 'l' has already been used as a match source expression in this context

-30 resolution/type errors detected in Modules0.dfy

-

--------------------- BadFunction --------------------

-Compiled assembly into BadFunction.dll

-

--------------------- Comprehensions --------------------

-Compiled assembly into Comprehensions.exe

-

--------------------- Basics --------------------

-Compilation error: an assume statement cannot be compiled (line 22)

-

--------------------- ControlStructures --------------------

-Compiled assembly into ControlStructures.dll

-

--------------------- DTypes --------------------

-Compilation error: compilation does not support type 'object' as a type parameter; consider introducing a ghost

-Compilation error: compilation of set<object> is not supported; consider introducing a ghost

-Compilation error: compilation of set<object> is not supported; consider introducing a ghost

-Compilation error: compilation of set<object> is not supported; consider introducing a ghost

-Compilation error: compilation of set<object> is not supported; consider introducing a ghost

-Compilation error: compilation of set<object> is not supported; consider introducing a ghost

-Compilation error: compilation of set<object> is not supported; consider introducing a ghost

-Compilation error: compilation does not support type 'object' as a type parameter; consider introducing a ghost

-Compilation error: compilation does not support type 'object' as a type parameter; consider introducing a ghost

-Compilation error: compilation does not support type 'object' as a type parameter; consider introducing a ghost

-

--------------------- ParallelResolveErrors --------------------

-ParallelResolveErrors.dfy(7,9): Error: Assignment to non-ghost field is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)

-ParallelResolveErrors.dfy(17,6): Error: LHS of assignment must denote a mutable variable or field

-ParallelResolveErrors.dfy(22,6): Error: body of parallel statement is attempting to update a variable declared outside the parallel statement

-ParallelResolveErrors.dfy(40,6): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)

-ParallelResolveErrors.dfy(52,13): Error: set choose operator not supported inside the enclosing parallel statement

-ParallelResolveErrors.dfy(57,13): Error: new allocation not supported in parallel statements

-ParallelResolveErrors.dfy(67,6): Error: the body of the enclosing parallel statement is not allowed to call non-ghost methods

-ParallelResolveErrors.dfy(74,19): Error: trying to break out of more loop levels than there are enclosing loops

-ParallelResolveErrors.dfy(78,18): Error: return statement is not allowed inside a parallel statement

-ParallelResolveErrors.dfy(85,21): Error: trying to break out of more loop levels than there are enclosing loops

-ParallelResolveErrors.dfy(86,20): Error: trying to break out of more loop levels than there are enclosing loops

-ParallelResolveErrors.dfy(87,20): Error: break label is undefined or not in scope: OutsideLoop

-ParallelResolveErrors.dfy(96,24): Error: trying to break out of more loop levels than there are enclosing loops

-ParallelResolveErrors.dfy(97,24): Error: break label is undefined or not in scope: OutsideLoop

-ParallelResolveErrors.dfy(105,2): Warning: the conclusion of the body of this parallel statement will not be known outside the parallel statement; consider using an 'ensures' clause

-ParallelResolveErrors.dfy(106,9): Error: the body of the enclosing parallel statement is not allowed to update heap locations

-15 resolution/type errors detected in ParallelResolveErrors.dfy

-

--------------------- Parallel --------------------

-Compilation error: compilation of set<object> is not supported; consider introducing a ghost

-Compilation error: compilation of set<object> is not supported; consider introducing a ghost

-Compilation error: compilation of set<object> is not supported; consider introducing a ghost

-Compilation error: an assume statement cannot be compiled (line 47)

-

--------------------- TypeParameters --------------------

-Compiled assembly into TypeParameters.exe

-

--------------------- Coinductive --------------------

-Coinductive.dfy(10,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'Rec_Forever' can be constructed

-Coinductive.dfy(13,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'D' can be constructed

-Coinductive.dfy(35,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'K' can be constructed

-Coinductive.dfy(61,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NotFiniteEnough_Dt' can be constructed

-4 resolution/type errors detected in Coinductive.dfy

-

--------------------- Corecursion --------------------

-Compiled assembly into Corecursion.dll

-

--------------------- TypeAntecedents --------------------

-Compiled assembly into TypeAntecedents.exe

-

--------------------- SplitExpr --------------------

-Compiled assembly into SplitExpr.dll

-

--------------------- LoopModifies --------------------

-Compiled assembly into LoopModifies.dll

-

--------------------- Refinement --------------------

-Compilation error: Method BodyFree._default.M has no body

-Compilation error: an assume statement cannot be compiled (line 128)

-

--------------------- RefinementErrors --------------------

-RefinementErrors.dfy(27,17): Error: a refining method is not allowed to add preconditions

-RefinementErrors.dfy(28,15): Error: a refining method is not allowed to extend the modifies clause

-RefinementErrors.dfy(31,14): Error: a predicate declaration (abc) can only refine a predicate

-RefinementErrors.dfy(32,8): Error: a field declaration (xyz) in a refining class (C) is not allowed replace an existing declaration in the refinement base

-RefinementErrors.dfy(34,13): Error: a function method cannot be changed into a (ghost) function in a refining module: F

-RefinementErrors.dfy(35,9): Error: type parameters are not allowed to be renamed from the names given in the function in the module being refined (expected 'A', found 'C')

-RefinementErrors.dfy(35,11): Error: type parameters are not allowed to be renamed from the names given in the function in the module being refined (expected 'B', found 'A')

-RefinementErrors.dfy(35,13): Error: type parameters are not allowed to be renamed from the names given in the function in the module being refined (expected 'C', found 'B')

-RefinementErrors.dfy(36,23): Error: the type of parameter 'z' is different from the type of the same parameter in the corresponding function in the module it refines ('seq<C>' instead of 'set<C>')

-RefinementErrors.dfy(37,9): Error: there is a difference in name of parameter 3 ('k' versus 'b') of function F compared to corresponding function in the module it refines

-RefinementErrors.dfy(54,20): Error: a function can be changed into a function method in a refining module only if the function has not yet been given a body: G

-11 resolution/type errors detected in RefinementErrors.dfy

-

--------------------- ReturnErrors --------------------

-ReturnErrors.dfy(30,10): Error: cannot have method call in return statement.

-ReturnErrors.dfy(36,10): Error: cannot have effectful parameter in multi-return statement.

-ReturnErrors.dfy(41,10): Error: can only have initialization methods which modify at most 'this'.

-3 resolution/type errors detected in ReturnErrors.dfy

-

--------------------- ChainingDisjointTests --------------------

-Compiled assembly into ChainingDisjointTests.dll

-

--------------------- CallStmtTests --------------------

-CallStmtTests.dfy(4,3): Error: LHS of assignment must denote a mutable variable

-CallStmtTests.dfy(15,8): Error: actual out-parameter 0 is required to be a ghost variable

-2 resolution/type errors detected in CallStmtTests.dfy

-

--------------------- MultiSets --------------------

-Compiled assembly into MultiSets.dll

-

--------------------- PredExpr --------------------

-Compiled assembly into PredExpr.dll

-

--------------------- LetExpr --------------------

-Compilation error: an assume statement cannot be compiled (line 31)

-Compilation error: an assume statement cannot be compiled (line 33)

-Compilation error: an assume statement cannot be compiled (line 34)

-

--------------------- Skeletons --------------------

-Compilation error: an assume statement cannot be compiled (line 5)

-Compilation error: an assume statement cannot be compiled (line 7)

-

--------------------- Maps --------------------

-Compiled assembly into Maps.exe

-

--------------------- Compilation --------------------

-Compiled assembly into Compilation.exe

diff --git a/Test/dafny0/AnswerRuntimeChecking b/Test/dafny0/AnswerRuntimeChecking
deleted file mode 100644
index e3970b78..00000000
--- a/Test/dafny0/AnswerRuntimeChecking
+++ /dev/null
@@ -1,272 +0,0 @@
-

--------------------- Simple --------------------

-Compilation error: compilation of set<object> is not supported; consider introducing a ghost

-

--------------------- TypeTests --------------------

-TypeTests.dfy(89,9): Error: sorry, cannot instantiate collection type with a subrange type

-TypeTests.dfy(4,13): Error: incorrect type of function argument 0 (expected C, got D)

-TypeTests.dfy(4,13): Error: incorrect type of function argument 1 (expected D, got C)

-TypeTests.dfy(5,13): Error: incorrect type of function argument 0 (expected C, got int)

-TypeTests.dfy(5,13): Error: incorrect type of function argument 1 (expected D, got int)

-TypeTests.dfy(11,15): Error: incorrect type of method in-parameter 0 (expected int, got bool)

-TypeTests.dfy(12,11): Error: incorrect type of method out-parameter 0 (expected int, got C)

-TypeTests.dfy(12,11): Error: incorrect type of method out-parameter 1 (expected C, got int)

-TypeTests.dfy(44,9): Error: Assignment to array element is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)

-TypeTests.dfy(53,6): Error: Duplicate local-variable name: z

-TypeTests.dfy(55,6): Error: Duplicate local-variable name: x

-TypeTests.dfy(58,8): Error: Duplicate local-variable name: x

-TypeTests.dfy(61,6): Error: Duplicate local-variable name: y

-TypeTests.dfy(68,17): Error: member F in type C does not refer to a method

-TypeTests.dfy(69,17): Error: a method called as an initialization method must not have any result arguments

-TypeTests.dfy(78,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)

-TypeTests.dfy(78,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)

-TypeTests.dfy(79,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)

-TypeTests.dfy(79,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)

-TypeTests.dfy(80,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)

-TypeTests.dfy(80,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)

-TypeTests.dfy(82,2): Error: LHS of array assignment must denote an array element (found seq<C>)

-TypeTests.dfy(82,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)

-TypeTests.dfy(82,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)

-TypeTests.dfy(83,2): Error: LHS of array assignment must denote an array element (found seq<C>)

-TypeTests.dfy(83,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)

-TypeTests.dfy(83,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)

-TypeTests.dfy(84,2): Error: LHS of array assignment must denote an array element (found seq<C>)

-TypeTests.dfy(84,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)

-TypeTests.dfy(84,10): Error: cannot assign to a range of array elements (try the 'parallel' statement)

-TypeTests.dfy(90,9): Error: sorry, cannot instantiate type parameter with a subrange type

-TypeTests.dfy(91,8): Error: sorry, cannot instantiate 'array' type with a subrange type

-TypeTests.dfy(92,8): Error: sorry, cannot instantiate 'array' type with a subrange type

-TypeTests.dfy(18,9): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NeverendingList' can be constructed

-34 resolution/type errors detected in TypeTests.dfy

-

--------------------- NatTypes --------------------

-Compilation error: compilation does not support type 'object' as a type parameter; consider introducing a ghost

-Compilation error: compilation does not support type 'object' as a type parameter; consider introducing a ghost

-Compilation error: compilation does not support type 'object' as a type parameter; consider introducing a ghost

-Compilation error: compilation does not support type 'object' as a type parameter; consider introducing a ghost

-Compilation error: compilation does not support type 'object' as a type parameter; consider introducing a ghost

-Compilation error: compilation does not support type 'object' as a type parameter; consider introducing a ghost

-

--------------------- Definedness --------------------

-Compiled assembly into Definedness.dll

-Rewrote assembly into Definedness.dll

-

--------------------- FunctionSpecifications --------------------

-Compiled assembly into FunctionSpecifications.dll

-Rewrote assembly into FunctionSpecifications.dll

-

--------------------- ResolutionErrors --------------------

-ResolutionErrors.dfy(48,13): Error: 'this' is not allowed in a 'static' context

-ResolutionErrors.dfy(109,9): Error: ghost variables are allowed only in specification contexts

-ResolutionErrors.dfy(110,9): Error: function calls are allowed only in specification contexts (consider declaring the function a 'function method')

-ResolutionErrors.dfy(114,11): Error: ghost variables are allowed only in specification contexts

-ResolutionErrors.dfy(115,9): Error: actual out-parameter 0 is required to be a ghost variable

-ResolutionErrors.dfy(122,15): Error: ghost variables are allowed only in specification contexts

-ResolutionErrors.dfy(126,23): Error: ghost variables are allowed only in specification contexts

-ResolutionErrors.dfy(133,4): Error: ghost variables are allowed only in specification contexts

-ResolutionErrors.dfy(137,21): Error: ghost variables are allowed only in specification contexts

-ResolutionErrors.dfy(138,35): Error: ghost variables are allowed only in specification contexts

-ResolutionErrors.dfy(147,9): Error: only ghost methods can be called from this context

-ResolutionErrors.dfy(153,16): Error: 'decreases *' is not allowed on ghost loops

-ResolutionErrors.dfy(194,27): Error: ghost-context break statement is not allowed to break out of non-ghost structure

-ResolutionErrors.dfy(217,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop

-ResolutionErrors.dfy(229,12): Error: trying to break out of more loop levels than there are enclosing loops

-ResolutionErrors.dfy(233,12): Error: ghost-context break statement is not allowed to break out of non-ghost loop

-ResolutionErrors.dfy(238,8): Error: return statement is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)

-ResolutionErrors.dfy(10,16): Error: 'decreases *' is not allowed on ghost loops

-ResolutionErrors.dfy(22,11): Error: array selection requires an array2 (got array3<T>)

-ResolutionErrors.dfy(23,12): Error: sequence/array/map selection requires a sequence, array or map (got array3<T>)

-ResolutionErrors.dfy(24,11): Error: array selection requires an array4 (got array<T>)

-ResolutionErrors.dfy(54,14): Error: a field must be selected via an object, not just a class name

-ResolutionErrors.dfy(55,7): Error: unresolved identifier: F

-ResolutionErrors.dfy(56,14): Error: an instance function must be selected via an object, not just a class name

-ResolutionErrors.dfy(56,7): Error: call to instance function requires an instance

-ResolutionErrors.dfy(57,7): Error: unresolved identifier: G

-ResolutionErrors.dfy(59,7): Error: unresolved identifier: M

-ResolutionErrors.dfy(60,7): Error: call to instance method requires an instance

-ResolutionErrors.dfy(61,7): Error: unresolved identifier: N

-ResolutionErrors.dfy(64,8): Error: non-function expression is called with parameters

-ResolutionErrors.dfy(65,14): Error: member z does not exist in class Global

-ResolutionErrors.dfy(84,12): Error: the name 'Benny' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.Benny')

-ResolutionErrors.dfy(89,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')

-ResolutionErrors.dfy(90,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')

-ResolutionErrors.dfy(92,12): Error: the name 'David' denotes a datatype constructor, but does not do so uniquely; add an explicit qualification (for example, 'Abc.David')

-ResolutionErrors.dfy(94,12): Error: wrong number of arguments to datatype constructor Abc (found 2, expected 1)

-ResolutionErrors.dfy(256,4): Error: label shadows an enclosing label

-ResolutionErrors.dfy(261,2): Error: duplicate label

-ResolutionErrors.dfy(287,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called

-ResolutionErrors.dfy(288,4): Error: when allocating an object of type 'ClassWithConstructor', one of its constructor methods must be called

-ResolutionErrors.dfy(290,4): Error: a constructor is only allowed to be called when an object is being allocated

-ResolutionErrors.dfy(304,16): Error: arguments must have the same type (got int and DTD_List)

-ResolutionErrors.dfy(305,16): Error: arguments must have the same type (got DTD_List and int)

-ResolutionErrors.dfy(306,25): Error: arguments must have the same type (got bool and int)

-ResolutionErrors.dfy(309,18): Error: ghost fields are allowed only in specification contexts

-ResolutionErrors.dfy(318,15): Error: ghost variables are allowed only in specification contexts

-ResolutionErrors.dfy(343,2): Error: incorrect type of method in-parameter 1 (expected GenericClass<int>, got GenericClass<bool>)

-ResolutionErrors.dfy(355,18): Error: incorrect type of datatype constructor argument (found GList<_T0>, expected GList<int>)

-48 resolution/type errors detected in ResolutionErrors.dfy

-

--------------------- ParseErrors --------------------

-ParseErrors.dfy(4,19): error: a chain cannot have more than one != operator

-ParseErrors.dfy(6,37): error: this operator chain cannot continue with a descending operator

-ParseErrors.dfy(7,38): error: this operator chain cannot continue with an ascending operator

-ParseErrors.dfy(12,24): error: this operator chain cannot continue with a descending operator

-ParseErrors.dfy(15,18): error: this operator cannot be part of a chain

-ParseErrors.dfy(16,19): error: this operator cannot be part of a chain

-ParseErrors.dfy(17,18): error: this operator cannot be part of a chain

-ParseErrors.dfy(18,18): error: chaining not allowed from the previous operator

-8 parse errors detected in ParseErrors.dfy

-

--------------------- Array --------------------

-Compilation error: Arbitrary type ('B') cannot be compiled

-

--------------------- MultiDimArray --------------------

-Compiled assembly into MultiDimArray.dll

-Rewrote assembly into MultiDimArray.dll

-

--------------------- NonGhostQuantifiers --------------------

-NonGhostQuantifiers.dfy(146,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'

-NonGhostQuantifiers.dfy(150,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'

-NonGhostQuantifiers.dfy(155,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'

-NonGhostQuantifiers.dfy(160,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'

-NonGhostQuantifiers.dfy(164,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'

-NonGhostQuantifiers.dfy(168,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'

-NonGhostQuantifiers.dfy(173,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'

-NonGhostQuantifiers.dfy(178,4): Error: a quantifier involved in a function definition is not allowed to depend on the set of allocated references; Dafny's heuristics can't figure out a bound for the values of 'c'

-NonGhostQuantifiers.dfy(183,13): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'c'

-NonGhostQuantifiers.dfy(13,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'n'

-NonGhostQuantifiers.dfy(42,4): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'n'

-NonGhostQuantifiers.dfy(46,4): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'd'

-NonGhostQuantifiers.dfy(50,4): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'n'

-NonGhostQuantifiers.dfy(74,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'i'

-NonGhostQuantifiers.dfy(78,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j'

-NonGhostQuantifiers.dfy(88,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j'

-NonGhostQuantifiers.dfy(103,5): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'j'

-NonGhostQuantifiers.dfy(111,10): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'y'

-NonGhostQuantifiers.dfy(120,8): Error: quantifiers in non-ghost contexts must be compilable, but Dafny's heuristics can't figure out how to produce a bounded set of values for 'x'

-NonGhostQuantifiers.dfy(137,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)

-20 resolution/type errors detected in NonGhostQuantifiers.dfy

-

--------------------- ModulesCycle --------------------

-ModulesCycle.dfy(12,7): Error: module T named among imports does not exist

-ModulesCycle.dfy(23,7): Error: import graph contains a cycle: H -> I -> J -> G

-2 resolution/type errors detected in ModulesCycle.dfy

-

--------------------- Modules0 --------------------

-Modules0.dfy(5,8): Error: Duplicate name of top-level declaration: WazzupA

-Modules0.dfy(6,11): Error: Duplicate name of top-level declaration: WazzupA

-Modules0.dfy(7,7): Error: Duplicate name of top-level declaration: WazzupA

-Modules0.dfy(10,7): Error: Duplicate name of top-level declaration: WazzupB

-Modules0.dfy(11,8): Error: Duplicate name of top-level declaration: WazzupB

-Modules0.dfy(12,11): Error: Duplicate name of top-level declaration: WazzupB

-Modules0.dfy(42,11): Error: The name T ambiguously refers to a type in one of the modules N, M

-Modules0.dfy(43,18): Error: The name T ambiguously refers to a type in one of the modules N, M

-Modules0.dfy(44,15): Error: The name T ambiguously refers to a type in one of the modules N, M

-Modules0.dfy(46,16): Error: The name T ambiguously refers to a type in one of the modules N, M

-Modules0.dfy(47,18): Error: The name T ambiguously refers to a type in one of the modules N, M

-Modules0.dfy(43,13): Error: Function body type mismatch (expected T, got T)

-Modules0.dfy(48,19): Error: The name T ambiguously refers to a type in one of the modules N, M

-Modules0.dfy(48,12): Error: new can be applied only to reference types (got T)

-Modules0.dfy(54,12): Error: Undeclared top-level type or type parameter: T (did you forget a module import?)

-Modules0.dfy(70,18): Error: Undeclared top-level type or type parameter: MyClass1 (did you forget a module import?)

-Modules0.dfy(71,18): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget a module import?)

-Modules0.dfy(81,18): Error: Undeclared top-level type or type parameter: MyClass2 (did you forget a module import?)

-Modules0.dfy(105,16): Error: Undeclared top-level type or type parameter: ClassG (did you forget a module import?)

-Modules0.dfy(244,11): Error: Undeclared top-level type or type parameter: X (did you forget a module import?)

-Modules0.dfy(250,15): Error: unresolved identifier: X

-Modules0.dfy(251,17): Error: member DoesNotExist does not exist in class X

-Modules0.dfy(294,16): Error: member R does not exist in class B

-Modules0.dfy(294,6): Error: expected method call, found expression

-Modules0.dfy(140,11): Error: ghost variables are allowed only in specification contexts

-Modules0.dfy(154,11): Error: old expressions are allowed only in specification and ghost contexts

-Modules0.dfy(155,11): Error: fresh expressions are allowed only in specification and ghost contexts

-Modules0.dfy(156,11): Error: allocated expressions are allowed only in specification and ghost contexts

-Modules0.dfy(172,10): Error: match source expression 'tree' has already been used as a match source expression in this context

-Modules0.dfy(211,12): Error: match source expression 'l' has already been used as a match source expression in this context

-30 resolution/type errors detected in Modules0.dfy

-

--------------------- Comprehensions --------------------

-Compiled assembly into Comprehensions.exe

-Rewrote assembly into Comprehensions.exe

-

--------------------- ControlStructures --------------------

-Compiled assembly into ControlStructures.dll

-Rewrote assembly into ControlStructures.dll

-

--------------------- ParallelResolveErrors --------------------

-ParallelResolveErrors.dfy(7,9): Error: Assignment to non-ghost field is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)

-ParallelResolveErrors.dfy(17,6): Error: LHS of assignment must denote a mutable variable or field

-ParallelResolveErrors.dfy(22,6): Error: body of parallel statement is attempting to update a variable declared outside the parallel statement

-ParallelResolveErrors.dfy(40,6): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression)

-ParallelResolveErrors.dfy(52,13): Error: set choose operator not supported inside the enclosing parallel statement

-ParallelResolveErrors.dfy(57,13): Error: new allocation not supported in parallel statements

-ParallelResolveErrors.dfy(67,6): Error: the body of the enclosing parallel statement is not allowed to call non-ghost methods

-ParallelResolveErrors.dfy(74,19): Error: trying to break out of more loop levels than there are enclosing loops

-ParallelResolveErrors.dfy(78,18): Error: return statement is not allowed inside a parallel statement

-ParallelResolveErrors.dfy(85,21): Error: trying to break out of more loop levels than there are enclosing loops

-ParallelResolveErrors.dfy(86,20): Error: trying to break out of more loop levels than there are enclosing loops

-ParallelResolveErrors.dfy(87,20): Error: break label is undefined or not in scope: OutsideLoop

-ParallelResolveErrors.dfy(96,24): Error: trying to break out of more loop levels than there are enclosing loops

-ParallelResolveErrors.dfy(97,24): Error: break label is undefined or not in scope: OutsideLoop

-ParallelResolveErrors.dfy(105,2): Warning: the conclusion of the body of this parallel statement will not be known outside the parallel statement; consider using an 'ensures' clause

-ParallelResolveErrors.dfy(106,9): Error: the body of the enclosing parallel statement is not allowed to update heap locations

-15 resolution/type errors detected in ParallelResolveErrors.dfy

-

--------------------- Coinductive --------------------

-Coinductive.dfy(10,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'Rec_Forever' can be constructed

-Coinductive.dfy(13,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'D' can be constructed

-Coinductive.dfy(35,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'K' can be constructed

-Coinductive.dfy(61,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NotFiniteEnough_Dt' can be constructed

-4 resolution/type errors detected in Coinductive.dfy

-

--------------------- Corecursion --------------------

-Compiled assembly into Corecursion.dll

-Rewrote assembly into Corecursion.dll

-

--------------------- LoopModifies --------------------

-Compiled assembly into LoopModifies.dll

-Rewrote assembly into LoopModifies.dll

-

--------------------- Refinement --------------------

-Compilation error: Method BodyFree._default.M has no body

-

--------------------- RefinementErrors --------------------

-RefinementErrors.dfy(27,17): Error: a refining method is not allowed to add preconditions

-RefinementErrors.dfy(28,15): Error: a refining method is not allowed to extend the modifies clause

-RefinementErrors.dfy(31,14): Error: a predicate declaration (abc) can only refine a predicate

-RefinementErrors.dfy(32,8): Error: a field declaration (xyz) in a refining class (C) is not allowed replace an existing declaration in the refinement base

-RefinementErrors.dfy(34,13): Error: a function method cannot be changed into a (ghost) function in a refining module: F

-RefinementErrors.dfy(35,9): Error: type parameters are not allowed to be renamed from the names given in the function in the module being refined (expected 'A', found 'C')

-RefinementErrors.dfy(35,11): Error: type parameters are not allowed to be renamed from the names given in the function in the module being refined (expected 'B', found 'A')

-RefinementErrors.dfy(35,13): Error: type parameters are not allowed to be renamed from the names given in the function in the module being refined (expected 'C', found 'B')

-RefinementErrors.dfy(36,23): Error: the type of parameter 'z' is different from the type of the same parameter in the corresponding function in the module it refines ('seq<C>' instead of 'set<C>')

-RefinementErrors.dfy(37,9): Error: there is a difference in name of parameter 3 ('k' versus 'b') of function F compared to corresponding function in the module it refines

-RefinementErrors.dfy(54,20): Error: a function can be changed into a function method in a refining module only if the function has not yet been given a body: G

-11 resolution/type errors detected in RefinementErrors.dfy

-

--------------------- ReturnErrors --------------------

-ReturnErrors.dfy(30,10): Error: cannot have method call in return statement.

-ReturnErrors.dfy(36,10): Error: cannot have effectful parameter in multi-return statement.

-ReturnErrors.dfy(41,10): Error: can only have initialization methods which modify at most 'this'.

-3 resolution/type errors detected in ReturnErrors.dfy

-

--------------------- ChainingDisjointTests --------------------

-Compiled assembly into ChainingDisjointTests.dll

-Rewrote assembly into ChainingDisjointTests.dll

-

--------------------- CallStmtTests --------------------

-CallStmtTests.dfy(4,3): Error: LHS of assignment must denote a mutable variable

-CallStmtTests.dfy(15,8): Error: actual out-parameter 0 is required to be a ghost variable

-2 resolution/type errors detected in CallStmtTests.dfy

-

--------------------- PredExpr --------------------

-Compiled assembly into PredExpr.dll

-Rewrote assembly into PredExpr.dll

-

--------------------- Skeletons --------------------

-Compiled assembly into Skeletons.dll

-Rewrote assembly into Skeletons.dll

-

--------------------- Compilation --------------------

-Compiled assembly into Compilation.exe

-Rewrote assembly into Compilation.exe

diff --git a/Test/dafny0/runtestNoRuntimeChecking.bat b/Test/dafny0/runtestNoRuntimeChecking.bat
deleted file mode 100644
index c90930d5..00000000
--- a/Test/dafny0/runtestNoRuntimeChecking.bat
+++ /dev/null
@@ -1,44 +0,0 @@
-@echo off

-setlocal

-

-set BOOGIEDIR=..\..\Binaries

-set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe

-set BPLEXE=%BOOGIEDIR%\Boogie.exe

-

-REM bugs:

-REM Modules1

-REM Termination

-REM Datatypes

-REM NoTypeArgs

-REM ReturnTests

-REM Predicates

-

-for %%f in (Simple TypeTests NatTypes SmallTests Definedness

-            FunctionSpecifications ResolutionErrors ParseErrors

-            Array MultiDimArray NonGhostQuantifiers AdvancedLHS

-            ModulesCycle Modules0 BadFunction Comprehensions

-            Basics ControlStructures DTypes ParallelResolveErrors

-            Parallel TypeParameters Coinductive Corecursion

-            TypeAntecedents SplitExpr LoopModifies Refinement

-            RefinementErrors ReturnErrors ChainingDisjointTests

-            CallStmtTests MultiSets PredExpr LetExpr Skeletons

-            Maps Compilation) do (

-  echo.

-  echo -------------------- %%f --------------------

-  %DAFNY_EXE% /nologo /errorTrace:0 /verification:0 /runtimeChecking:0 /compile:2 %* %%f.dfy

-  if exist %%f.cs. (

-    del %%f.cs

-  )

-  if exist %%f.exe. (

-    del %%f.exe

-  )

-  if exist %%f.dll. (

-    del %%f.dll

-  )

-  if exist %%f.pdb. (

-    del %%f.pdb

-  )

-  if exist %%f.pdb.original. (

-    del %%f.pdb.original

-  )

-)

diff --git a/Test/dafny0/runtestRuntimeChecking.bat b/Test/dafny0/runtestRuntimeChecking.bat
deleted file mode 100644
index 42d21010..00000000
--- a/Test/dafny0/runtestRuntimeChecking.bat
+++ /dev/null
@@ -1,55 +0,0 @@
-@echo off

-setlocal

-

-set BOOGIEDIR=..\..\Binaries

-set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe

-set BPLEXE=%BOOGIEDIR%\Boogie.exe

-

-REM bugs:

-REM Modules1

-REM Termination

-REM Datatypes

-REM NoTypeArgs

-REM ReturnTests

-REM Predicates

-

-REM to implement:

-REM SmallTests     : unexpected expressions

-REM AdvancedLHS    : fresh expressions

-REM BadFunction    : ghost state

-REM Basics         : ghost state

-REM DTypes         : quantifiers

-REM Parallel       : quantifiers

-REM TypeParameters : ghost state

-REM TypeAntecedents: quantifiers

-REM SplitExpr      : ghost state

-REM MultiSets      : quantifiers

-REM LetExpr        : old expressions

-REM Maps           : quantifiers

-

-for %%f in (Simple TypeTests NatTypes Definedness

-            FunctionSpecifications ResolutionErrors ParseErrors

-            Array MultiDimArray NonGhostQuantifiers ModulesCycle

-            Modules0 Comprehensions ControlStructures ParallelResolveErrors

-            Coinductive Corecursion LoopModifies Refinement

-            RefinementErrors ReturnErrors ChainingDisjointTests

-            CallStmtTests PredExpr Skeletons Compilation) do (

-  echo.

-  echo -------------------- %%f --------------------

-  %DAFNY_EXE% /nologo /errorTrace:0 /verification:0 /runtimeChecking:1 /compile:2 %* %%f.dfy

-  if exist %%f.cs. (

-    del %%f.cs

-  )

-  if exist %%f.exe. (

-    del %%f.exe

-  )

-  if exist %%f.dll. (

-    del %%f.dll

-  )

-  if exist %%f.pdb. (

-    del %%f.pdb

-  )

-  if exist %%f.pdb.original. (

-    del %%f.pdb.original

-  )

-)

diff --git a/Test/dafny1/AnswerNoRuntimeChecking b/Test/dafny1/AnswerNoRuntimeChecking
deleted file mode 100644
index 5472ec14..00000000
--- a/Test/dafny1/AnswerNoRuntimeChecking
+++ /dev/null
@@ -1,76 +0,0 @@
-

--------------------- Queue --------------------

-Compiled assembly into Queue.dll

-

--------------------- PriorityQueue --------------------

-Compiled assembly into PriorityQueue.dll

-

--------------------- ExtensibleArray --------------------

-Compiled assembly into ExtensibleArray.exe

-

--------------------- ExtensibleArrayAuto --------------------

-Compiled assembly into ExtensibleArrayAuto.exe

-

--------------------- BinaryTree --------------------

-Compiled assembly into BinaryTree.dll

-

--------------------- UnboundedStack --------------------

-Compiled assembly into UnboundedStack.dll

-

--------------------- ListCopy --------------------

-Compilation error: an assume statement cannot be compiled (line 14)

-Compilation error: an assume statement cannot be compiled (line 15)

-

--------------------- ListReverse --------------------

-Compiled assembly into ListReverse.dll

-

--------------------- ListContents --------------------

-Compiled assembly into ListContents.dll

-

--------------------- MatrixFun --------------------

-Compiled assembly into MatrixFun.exe

-

--------------------- pow2 --------------------

-Compiled assembly into pow2.dll

-

--------------------- SchorrWaite --------------------

-Compiled assembly into SchorrWaite.dll

-

--------------------- Cubes --------------------

-Compiled assembly into Cubes.dll

-

--------------------- SumOfCubes --------------------

-Compiled assembly into SumOfCubes.dll

-

--------------------- FindZero --------------------

-Compiled assembly into FindZero.dll

-

--------------------- TerminationDemos --------------------

-Compiled assembly into TerminationDemos.dll

-

--------------------- Substitution --------------------

-Compiled assembly into Substitution.dll

-

--------------------- KatzManna --------------------

-Compilation error: an assume statement cannot be compiled (line 66)

-

--------------------- Induction --------------------

-Compiled assembly into Induction.dll

-

--------------------- Rippling --------------------

-Compilation error: Arbitrary type ('FunctionValue') cannot be compiled

-

--------------------- Celebrity --------------------

-Compilation error: Function _default._default.Knows has no body

-Compilation error: an assume statement cannot be compiled (line 16)

-

--------------------- BDD --------------------

-Compiled assembly into BDD.dll

-

--------------------- UltraFilter --------------------

-Compilation error: Method _default.UltraFilter.H has no body

-Compilation error: an assume statement cannot be compiled (line 42)

-Compilation error: an assume statement cannot be compiled (line 45)

-Compilation error: an assume statement cannot be compiled (line 76)

-Compilation error: an assume statement cannot be compiled (line 97)

-Compilation error: an assume statement cannot be compiled (line 98)

diff --git a/Test/dafny1/AnswerRuntimeChecking b/Test/dafny1/AnswerRuntimeChecking
deleted file mode 100644
index 1ade5aeb..00000000
--- a/Test/dafny1/AnswerRuntimeChecking
+++ /dev/null
@@ -1,27 +0,0 @@
-

--------------------- ListReverse --------------------

-Compiled assembly into ListReverse.dll

-Rewrote assembly into ListReverse.dll

-

--------------------- MatrixFun --------------------

-Compiled assembly into MatrixFun.exe

-Rewrote assembly into MatrixFun.exe

-

--------------------- pow2 --------------------

-Compiled assembly into pow2.dll

-Rewrote assembly into pow2.dll

-

--------------------- Cubes --------------------

-Compiled assembly into Cubes.dll

-Rewrote assembly into Cubes.dll

-

--------------------- Substitution --------------------

-Compiled assembly into Substitution.dll

-Rewrote assembly into Substitution.dll

-

--------------------- KatzManna --------------------

-Compiled assembly into KatzManna.dll

-Rewrote assembly into KatzManna.dll

-

--------------------- Rippling --------------------

-Compilation error: Arbitrary type ('FunctionValue') cannot be compiled

diff --git a/Test/dafny1/runtestNoRuntimeChecking.bat b/Test/dafny1/runtestNoRuntimeChecking.bat
deleted file mode 100644
index a4989fa1..00000000
--- a/Test/dafny1/runtestNoRuntimeChecking.bat
+++ /dev/null
@@ -1,36 +0,0 @@
-@echo off

-setlocal

-

-set BOOGIEDIR=..\..\Binaries

-set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe

-set BPLEXE=%BOOGIEDIR%\Boogie.exe

-

-REM bugs:

-REM SeparationLogicList

-REM TreeDatatype

-REM MoreInduction

-

-for %%f in (Queue PriorityQueue ExtensibleArray ExtensibleArrayAuto

-            BinaryTree UnboundedStack ListCopy ListReverse ListContents

-            MatrixFun pow2 SchorrWaite Cubes SumOfCubes FindZero

-            TerminationDemos Substitution KatzManna Induction Rippling

-            Celebrity BDD UltraFilter) do (

-  echo.

-  echo -------------------- %%f --------------------

-  %DAFNY_EXE% /nologo /errorTrace:0 /verification:0 /runtimeChecking:0 /compile:2 %* %%f.dfy

-  if exist %%f.cs. (

-    del %%f.cs

-  )

-  if exist %%f.exe. (

-    del %%f.exe

-  )

-  if exist %%f.dll. (

-    del %%f.dll

-  )

-  if exist %%f.pdb. (

-    del %%f.pdb

-  )

-  if exist %%f.pdb.original. (

-    del %%f.pdb.original

-  )

-)

diff --git a/Test/dafny1/runtestRuntimeChecking.bat b/Test/dafny1/runtestRuntimeChecking.bat
deleted file mode 100644
index fc32fbf4..00000000
--- a/Test/dafny1/runtestRuntimeChecking.bat
+++ /dev/null
@@ -1,51 +0,0 @@
-@echo off

-setlocal

-

-set BOOGIEDIR=..\..\Binaries

-set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe

-set BPLEXE=%BOOGIEDIR%\Boogie.exe

-

-REM bugs:

-REM SeparationLogicList

-REM TreeDatatype

-REM MoreInduction

-

-REM to implement:

-REM Queue              : parallel statements

-REM PriorityQueue      : ghost state

-REM ExtensibleArray    : ghost state

-REM ExtensibleArrayAuto: ghost state

-REM BinaryTree         : old expressions

-REM UnboundedStack     : ghost state

-REM ListCopy           : fresh expressions

-REM ListContents       : old expressions

-REM SchorrWaite        : ghost state

-REM SumOfCubes         : ghost state

-REM FindZero           : ghost state

-REM TerminationDemos   : ghost state

-REM Induction          : quantifiers

-REM Celebrity          : quantifiers

-REM BDD                : ghost state

-REM UltraFilter        : quantifiers

-

-for %%f in (ListReverse MatrixFun pow2 Cubes Substitution KatzManna

-            Rippling) do (

-  echo.

-  echo -------------------- %%f --------------------

-  %DAFNY_EXE% /nologo /errorTrace:0 /verification:0 /runtimeChecking:1 /compile:2 %* %%f.dfy

-  if exist %%f.cs. (

-    del %%f.cs

-  )

-  if exist %%f.exe. (

-    del %%f.exe

-  )

-  if exist %%f.dll. (

-    del %%f.dll

-  )

-  if exist %%f.pdb. (

-    del %%f.pdb

-  )

-  if exist %%f.pdb.original. (

-    del %%f.pdb.original

-  )

-)

diff --git a/Test/dafny2/AnswerNoRuntimeChecking b/Test/dafny2/AnswerNoRuntimeChecking
deleted file mode 100644
index f04bb934..00000000
--- a/Test/dafny2/AnswerNoRuntimeChecking
+++ /dev/null
@@ -1,30 +0,0 @@
-

--------------------- Classics --------------------

-Compiled assembly into Classics.dll

-

--------------------- TreeBarrier --------------------

-Compilation error: an assume statement cannot be compiled (line 90)

-Compilation error: an assume statement cannot be compiled (line 102)

-Compilation error: an assume statement cannot be compiled (line 128)

-

--------------------- COST-verif-comp-2011-1-MaxArray --------------------

-Compiled assembly into COST-verif-comp-2011-1-MaxArray.dll

-

--------------------- COST-verif-comp-2011-2-MaxTree-class --------------------

-Compiled assembly into COST-verif-comp-2011-2-MaxTree-class.dll

-

--------------------- COST-verif-comp-2011-2-MaxTree-datatype --------------------

-Compiled assembly into COST-verif-comp-2011-2-MaxTree-datatype.dll

-

--------------------- COST-verif-comp-2011-3-TwoDuplicates --------------------

-Compiled assembly into COST-verif-comp-2011-3-TwoDuplicates.dll

-

--------------------- COST-verif-comp-2011-4-FloydCycleDetect --------------------

-Compiled assembly into COST-verif-comp-2011-4-FloydCycleDetect.dll

-

--------------------- Intervals --------------------

-Compiled assembly into Intervals.dll

-

--------------------- StoreAndRetrieve --------------------

-Compilation error: an assume statement cannot be compiled (line 21)

-Compilation error: Function Library.Function.Apply has no body

diff --git a/Test/dafny2/AnswerRuntimeChecking b/Test/dafny2/AnswerRuntimeChecking
deleted file mode 100644
index 32b61bb1..00000000
--- a/Test/dafny2/AnswerRuntimeChecking
+++ /dev/null
@@ -1,7 +0,0 @@
-

--------------------- COST-verif-comp-2011-2-MaxTree-datatype --------------------

-Compiled assembly into COST-verif-comp-2011-2-MaxTree-datatype.dll

-Rewrote assembly into COST-verif-comp-2011-2-MaxTree-datatype.dll

-

--------------------- StoreAndRetrieve --------------------

-Compilation error: Function Library.Function.Apply has no body

diff --git a/Test/dafny2/runtestNoRuntimeChecking.bat b/Test/dafny2/runtestNoRuntimeChecking.bat
deleted file mode 100644
index b60fd69c..00000000
--- a/Test/dafny2/runtestNoRuntimeChecking.bat
+++ /dev/null
@@ -1,34 +0,0 @@
-@echo off

-setlocal

-

-set BOOGIEDIR=..\..\Binaries

-set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe

-set BPLEXE=%BOOGIEDIR%\Boogie.exe

-

-REM soon again: SnapshotableTrees.dfy

-

-for %%f in (Classics TreeBarrier COST-verif-comp-2011-1-MaxArray

-            COST-verif-comp-2011-2-MaxTree-class

-            COST-verif-comp-2011-2-MaxTree-datatype

-            COST-verif-comp-2011-3-TwoDuplicates

-            COST-verif-comp-2011-4-FloydCycleDetect

-            Intervals StoreAndRetrieve) do (

-  echo.

-  echo -------------------- %%f --------------------

-  %DAFNY_EXE% /nologo /errorTrace:0 /verification:0 /runtimeChecking:0 /compile:2 %* %%f.dfy

-  if exist %%f.cs. (

-    del %%f.cs

-  )

-  if exist %%f.exe. (

-    del %%f.exe

-  )

-  if exist %%f.dll. (

-    del %%f.dll

-  )

-  if exist %%f.pdb. (

-    del %%f.pdb

-  )

-  if exist %%f.pdb.original. (

-    del %%f.pdb.original

-  )

-)

diff --git a/Test/dafny2/runtestRuntimeChecking.bat b/Test/dafny2/runtestRuntimeChecking.bat
deleted file mode 100644
index 4ba447a7..00000000
--- a/Test/dafny2/runtestRuntimeChecking.bat
+++ /dev/null
@@ -1,39 +0,0 @@
-@echo off

-setlocal

-

-set BOOGIEDIR=..\..\Binaries

-set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe

-set BPLEXE=%BOOGIEDIR%\Boogie.exe

-

-REM soon again: SnapshotableTrees.dfy

-

-REM to implement:

-REM Classics                               : ghost state

-REM TreeBarrier                            : ghost state

-REM COST-verif-comp-2011-1-MaxArray        : ghost state

-REM COST-verif-comp-2011-2-MaxTree-class   : ghost state

-REM COST-verif-comp-2011-3-TwoDuplicates   : quantifiers

-REM COST-verif-comp-2011-4-FloydCycleDetect: quantifiers

-REM Intervals                              : ghost state

-

-for %%f in (COST-verif-comp-2011-2-MaxTree-datatype

-            StoreAndRetrieve) do (

-  echo.

-  echo -------------------- %%f --------------------

-  %DAFNY_EXE% /nologo /errorTrace:0 /verification:0 /runtimeChecking:1 /compile:2 %* %%f.dfy

-  if exist %%f.cs. (

-    del %%f.cs

-  )

-  if exist %%f.exe. (

-    del %%f.exe

-  )

-  if exist %%f.dll. (

-    del %%f.dll

-  )

-  if exist %%f.pdb. (

-    del %%f.pdb

-  )

-  if exist %%f.pdb.original. (

-    del %%f.pdb.original

-  )

-)

diff --git a/Test/vacid0/AnswerNoRuntimeChecking b/Test/vacid0/AnswerNoRuntimeChecking
deleted file mode 100644
index a1f7f57b..00000000
--- a/Test/vacid0/AnswerNoRuntimeChecking
+++ /dev/null
@@ -1,9 +0,0 @@
-

--------------------- LazyInitArray --------------------

-Compiled assembly into LazyInitArray.dll

-

--------------------- SparseArray --------------------

-Compiled assembly into SparseArray.dll

-

--------------------- Composite --------------------

-Compiled assembly into Composite.exe

diff --git a/Test/vacid0/runtestNoRuntimeChecking.bat b/Test/vacid0/runtestNoRuntimeChecking.bat
deleted file mode 100644
index 3a7befa2..00000000
--- a/Test/vacid0/runtestNoRuntimeChecking.bat
+++ /dev/null
@@ -1,27 +0,0 @@
-@echo off

-setlocal

-

-set BOOGIEDIR=..\..\Binaries

-set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe

-set BPLEXE=%BOOGIEDIR%\Boogie.exe

-

-for %%f in (LazyInitArray SparseArray Composite) do (

-  echo.

-  echo -------------------- %%f --------------------

-  %DAFNY_EXE% /nologo /errorTrace:0 /verification:0 /runtimeChecking:0 /compile:2 %* %%f.dfy

-  if exist %%f.cs. (

-    del %%f.cs

-  )

-  if exist %%f.exe. (

-    del %%f.exe

-  )

-  if exist %%f.dll. (

-    del %%f.dll

-  )

-  if exist %%f.pdb. (

-    del %%f.pdb

-  )

-  if exist %%f.pdb.original. (

-    del %%f.pdb.original

-  )

-)

diff --git a/Test/vacid0/runtestRuntimeChecking.bat b/Test/vacid0/runtestRuntimeChecking.bat
deleted file mode 100644
index 077c1002..00000000
--- a/Test/vacid0/runtestRuntimeChecking.bat
+++ /dev/null
@@ -1,32 +0,0 @@
-@echo off

-setlocal

-

-set BOOGIEDIR=..\..\Binaries

-set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe

-set BPLEXE=%BOOGIEDIR%\Boogie.exe

-

-REM to implement:

-REM LazyInitArray: ghost state

-REM SparseArray  : ghost state

-REM Composite    : ghost state

-

-for %%f in () do (

-  echo.

-  echo -------------------- %%f --------------------

-  %DAFNY_EXE% /nologo /errorTrace:0 /verification:0 /runtimeChecking:1 /compile:2 %* %%f.dfy

-  if exist %%f.cs. (

-    del %%f.cs

-  )

-  if exist %%f.exe. (

-    del %%f.exe

-  )

-  if exist %%f.dll. (

-    del %%f.dll

-  )

-  if exist %%f.pdb. (

-    del %%f.pdb

-  )

-  if exist %%f.pdb.original. (

-    del %%f.pdb.original

-  )

-)

diff --git a/Test/vstte2012/AnswerNoRuntimeChecking b/Test/vstte2012/AnswerNoRuntimeChecking
deleted file mode 100644
index c5508749..00000000
--- a/Test/vstte2012/AnswerNoRuntimeChecking
+++ /dev/null
@@ -1,18 +0,0 @@
-

--------------------- Two-Way-Sort --------------------

-Compiled assembly into Two-Way-Sort.dll

-

--------------------- Combinators --------------------

-Compiled assembly into Combinators.dll

-

--------------------- RingBuffer --------------------

-Compiled assembly into RingBuffer.dll

-

--------------------- RingBufferAuto --------------------

-Compiled assembly into RingBufferAuto.dll

-

--------------------- Tree --------------------

-Compiled assembly into Tree.dll

-

--------------------- BreadthFirstSearch --------------------

-Compilation error: Function _default.BreadthFirstSearch.Succ has no body

diff --git a/Test/vstte2012/AnswerRuntimeChecking b/Test/vstte2012/AnswerRuntimeChecking
deleted file mode 100644
index 5c703cc7..00000000
--- a/Test/vstte2012/AnswerRuntimeChecking
+++ /dev/null
@@ -1,11 +0,0 @@
-

--------------------- Two-Way-Sort --------------------

-Compiled assembly into Two-Way-Sort.dll

-Rewrote assembly into Two-Way-Sort.dll

-

--------------------- Tree --------------------

-Compiled assembly into Tree.dll

-Rewrote assembly into Tree.dll

-

--------------------- BreadthFirstSearch --------------------

-Compilation error: Function _default.BreadthFirstSearch.Succ has no body

diff --git a/Test/vstte2012/runtestNoRuntimeChecking.bat b/Test/vstte2012/runtestNoRuntimeChecking.bat
deleted file mode 100644
index e572ed2f..00000000
--- a/Test/vstte2012/runtestNoRuntimeChecking.bat
+++ /dev/null
@@ -1,28 +0,0 @@
-@echo off

-setlocal

-

-set BOOGIEDIR=..\..\Binaries

-set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe

-set BPLEXE=%BOOGIEDIR%\Boogie.exe

-

-for %%f in (Two-Way-Sort Combinators RingBuffer RingBufferAuto

-            Tree BreadthFirstSearch) do (

-  echo.

-  echo -------------------- %%f --------------------

-  %DAFNY_EXE% /nologo /errorTrace:0 /verification:0 /runtimeChecking:0 /compile:2 %* %%f.dfy

-  if exist %%f.cs. (

-    del %%f.cs

-  )

-  if exist %%f.exe. (

-    del %%f.exe

-  )

-  if exist %%f.dll. (

-    del %%f.dll

-  )

-  if exist %%f.pdb. (

-    del %%f.pdb

-  )

-  if exist %%f.pdb.original. (

-    del %%f.pdb.original

-  )

-)

diff --git a/Test/vstte2012/runtestRuntimeChecking.bat b/Test/vstte2012/runtestRuntimeChecking.bat
deleted file mode 100644
index 042efe96..00000000
--- a/Test/vstte2012/runtestRuntimeChecking.bat
+++ /dev/null
@@ -1,32 +0,0 @@
-@echo off

-setlocal

-

-set BOOGIEDIR=..\..\Binaries

-set DAFNY_EXE=%BOOGIEDIR%\Dafny.exe

-set BPLEXE=%BOOGIEDIR%\Boogie.exe

-

-REM to implement:

-REM Combinators   : ghost state

-REM RingBuffer    : ghost state

-REM RingBufferAuto: ghost state

-

-for %%f in (Two-Way-Sort Tree BreadthFirstSearch) do (

-  echo.

-  echo -------------------- %%f --------------------

-  %DAFNY_EXE% /nologo /errorTrace:0 /verification:0 /runtimeChecking:1 /compile:2 %* %%f.dfy

-  if exist %%f.cs. (

-    del %%f.cs

-  )

-  if exist %%f.exe. (

-    del %%f.exe

-  )

-  if exist %%f.dll. (

-    del %%f.dll

-  )

-  if exist %%f.pdb. (

-    del %%f.pdb

-  )

-  if exist %%f.pdb.original. (

-    del %%f.pdb.original

-  )

-)