Set up the same test infrastructure as in Boogie.

55 files changed, 158 insertions, 10 deletions

diff --git a/Test/dafny1/Answer b/Test/dafny1/Answer
index 06cac03b..e60451c2 100644
--- a/Test/dafny1/Answer
+++ b/Test/dafny1/Answer
@@ -92,20 +92,20 @@ Dafny program verifier finished with 33 verified, 0 errors
 Dafny program verifier finished with 141 verified, 0 errors

 

 -------------------- MoreInduction.dfy --------------------

-MoreInduction.dfy(75,1): Error BP5003: A postcondition might not hold on this return path.

-MoreInduction.dfy(74,11): Related location: This is the postcondition that might not hold.

+MoreInduction.dfy(78,1): Error BP5003: A postcondition might not hold on this return path.

+MoreInduction.dfy(77,11): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon0

-MoreInduction.dfy(80,1): Error BP5003: A postcondition might not hold on this return path.

-MoreInduction.dfy(79,21): Related location: This is the postcondition that might not hold.

+MoreInduction.dfy(83,1): Error BP5003: A postcondition might not hold on this return path.

+MoreInduction.dfy(82,21): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon0

-MoreInduction.dfy(85,1): Error BP5003: A postcondition might not hold on this return path.

-MoreInduction.dfy(84,11): Related location: This is the postcondition that might not hold.

+MoreInduction.dfy(88,1): Error BP5003: A postcondition might not hold on this return path.

+MoreInduction.dfy(87,11): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon0

-MoreInduction.dfy(90,1): Error BP5003: A postcondition might not hold on this return path.

-MoreInduction.dfy(89,22): Related location: This is the postcondition that might not hold.

+MoreInduction.dfy(93,1): Error BP5003: A postcondition might not hold on this return path.

+MoreInduction.dfy(92,22): Related location: This is the postcondition that might not hold.

 Execution trace:

     (0,0): anon0

 

diff --git a/Test/dafny1/BDD.dfy b/Test/dafny1/BDD.dfy
index 3b6e478c..252164db 100644
--- a/Test/dafny1/BDD.dfy
+++ b/Test/dafny1/BDD.dfy
@@ -1,4 +1,5 @@
-

+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

 

 module SimpleBDD

 {

@@ -57,4 +58,4 @@ module SimpleBDD
 	   b := node.b;

 	 }

    }

-}
\ No newline at end of file
+}

diff --git a/Test/dafny1/BDD.dfy.expect b/Test/dafny1/BDD.dfy.expect
new file mode 100644
index 00000000..790f6509
--- /dev/null
+++ b/Test/dafny1/BDD.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 5 verified, 0 errors

diff --git a/Test/dafny1/BinaryTree.dfy b/Test/dafny1/BinaryTree.dfy
index ea915f69..edacd931 100644
--- a/Test/dafny1/BinaryTree.dfy
+++ b/Test/dafny1/BinaryTree.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

 class IntSet {

   ghost var Contents: set<int>;

   ghost var Repr: set<object>;

diff --git a/Test/dafny1/BinaryTree.dfy.expect b/Test/dafny1/BinaryTree.dfy.expect
new file mode 100644
index 00000000..acae4413
--- /dev/null
+++ b/Test/dafny1/BinaryTree.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 24 verified, 0 errors

diff --git a/Test/dafny1/Celebrity.dfy b/Test/dafny1/Celebrity.dfy
index a4043f4d..7e5ab205 100644
--- a/Test/dafny1/Celebrity.dfy
+++ b/Test/dafny1/Celebrity.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

 // Celebrity example, inspired by the Rodin tutorial

 

 static function method Knows<Person>(a: Person, b: Person): bool

diff --git a/Test/dafny1/Celebrity.dfy.expect b/Test/dafny1/Celebrity.dfy.expect
new file mode 100644
index 00000000..c87e2af2
--- /dev/null
+++ b/Test/dafny1/Celebrity.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 10 verified, 0 errors

diff --git a/Test/dafny1/Cubes.dfy b/Test/dafny1/Cubes.dfy
index 1ada79fa..ecf26676 100644
--- a/Test/dafny1/Cubes.dfy
+++ b/Test/dafny1/Cubes.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

 method Cubes(a: array<int>)

   requires a != null;

   modifies a;

diff --git a/Test/dafny1/Cubes.dfy.expect b/Test/dafny1/Cubes.dfy.expect
new file mode 100644
index 00000000..069e7767
--- /dev/null
+++ b/Test/dafny1/Cubes.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 2 verified, 0 errors

diff --git a/Test/dafny1/ExtensibleArray.dfy b/Test/dafny1/ExtensibleArray.dfy
index 57ac69c7..cb48e02b 100644
--- a/Test/dafny1/ExtensibleArray.dfy
+++ b/Test/dafny1/ExtensibleArray.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

 class ExtensibleArray<T> {

   ghost var Contents: seq<T>;

   ghost var Repr: set<object>;

diff --git a/Test/dafny1/ExtensibleArray.dfy.expect b/Test/dafny1/ExtensibleArray.dfy.expect
new file mode 100644
index 00000000..f3a9c95f
--- /dev/null
+++ b/Test/dafny1/ExtensibleArray.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 11 verified, 0 errors

diff --git a/Test/dafny1/ExtensibleArrayAuto.dfy b/Test/dafny1/ExtensibleArrayAuto.dfy
index b05af9f9..b2e5ecc4 100644
--- a/Test/dafny1/ExtensibleArrayAuto.dfy
+++ b/Test/dafny1/ExtensibleArrayAuto.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

 class {:autocontracts} ExtensibleArray<T> {

   ghost var Contents: seq<T>;

 

diff --git a/Test/dafny1/ExtensibleArrayAuto.dfy.expect b/Test/dafny1/ExtensibleArrayAuto.dfy.expect
new file mode 100644
index 00000000..f3a9c95f
--- /dev/null
+++ b/Test/dafny1/ExtensibleArrayAuto.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 11 verified, 0 errors

diff --git a/Test/dafny1/FindZero.dfy b/Test/dafny1/FindZero.dfy
index c92dd065..f0eb6a60 100644
--- a/Test/dafny1/FindZero.dfy
+++ b/Test/dafny1/FindZero.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

 method FindZero(a: array<int>) returns (r: int)

   requires a != null && forall i :: 0 <= i < a.Length ==> 0 <= a[i];

   requires forall i :: 0 <= i && i+1 < a.Length ==> a[i]-1 <= a[i+1];

diff --git a/Test/dafny1/FindZero.dfy.expect b/Test/dafny1/FindZero.dfy.expect
new file mode 100644
index 00000000..42fd56a5
--- /dev/null
+++ b/Test/dafny1/FindZero.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 8 verified, 0 errors

diff --git a/Test/dafny1/Induction.dfy b/Test/dafny1/Induction.dfy
index 3585dde6..5dc398f3 100644
--- a/Test/dafny1/Induction.dfy
+++ b/Test/dafny1/Induction.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

 class IntegerInduction {

   // This class considers different ways of proving, for any natural n:

   //   (SUM i in [0, n] :: i^3) == (SUM i in [0, n] :: i)^2

diff --git a/Test/dafny1/Induction.dfy.expect b/Test/dafny1/Induction.dfy.expect
new file mode 100644
index 00000000..0d7d6532
--- /dev/null
+++ b/Test/dafny1/Induction.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 33 verified, 0 errors

diff --git a/Test/dafny1/KatzManna.dfy b/Test/dafny1/KatzManna.dfy
index 60b70c1a..5987a82b 100644
--- a/Test/dafny1/KatzManna.dfy
+++ b/Test/dafny1/KatzManna.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

 method NinetyOne(x: int, ghost proveFunctionalPostcondition: bool) returns (z: int)

   ensures proveFunctionalPostcondition ==> z == if x > 101 then x-10 else 91;

 {

diff --git a/Test/dafny1/KatzManna.dfy.expect b/Test/dafny1/KatzManna.dfy.expect
new file mode 100644
index 00000000..4ef2de53
--- /dev/null
+++ b/Test/dafny1/KatzManna.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 6 verified, 0 errors

diff --git a/Test/dafny1/ListContents.dfy b/Test/dafny1/ListContents.dfy
index a8b4861d..b79d3308 100644
--- a/Test/dafny1/ListContents.dfy
+++ b/Test/dafny1/ListContents.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

 class Node<T> {

   var list: seq<T>;

   var footprint: set<Node<T>>;

diff --git a/Test/dafny1/ListContents.dfy.expect b/Test/dafny1/ListContents.dfy.expect
new file mode 100644
index 00000000..249e77e5
--- /dev/null
+++ b/Test/dafny1/ListContents.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 9 verified, 0 errors

diff --git a/Test/dafny1/ListCopy.dfy b/Test/dafny1/ListCopy.dfy
index d5febfe0..4bffd51b 100644
--- a/Test/dafny1/ListCopy.dfy
+++ b/Test/dafny1/ListCopy.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

 class Node {

   var nxt: Node;

 

diff --git a/Test/dafny1/ListCopy.dfy.expect b/Test/dafny1/ListCopy.dfy.expect
new file mode 100644
index 00000000..73ba063c
--- /dev/null
+++ b/Test/dafny1/ListCopy.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 4 verified, 0 errors

diff --git a/Test/dafny1/ListReverse.dfy b/Test/dafny1/ListReverse.dfy
index ef029b88..0837dd91 100644
--- a/Test/dafny1/ListReverse.dfy
+++ b/Test/dafny1/ListReverse.dfy
@@ -1,3 +1,5 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

 

 class Node {

   var nxt: Node;

diff --git a/Test/dafny1/ListReverse.dfy.expect b/Test/dafny1/ListReverse.dfy.expect
new file mode 100644
index 00000000..069e7767
--- /dev/null
+++ b/Test/dafny1/ListReverse.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 2 verified, 0 errors

diff --git a/Test/dafny1/MatrixFun.dfy b/Test/dafny1/MatrixFun.dfy
index 8f9d87ed..08c82132 100644
--- a/Test/dafny1/MatrixFun.dfy
+++ b/Test/dafny1/MatrixFun.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

 method MirrorImage<T>(m: array2<T>)

   requires m != null;

   modifies m;

diff --git a/Test/dafny1/MatrixFun.dfy.expect b/Test/dafny1/MatrixFun.dfy.expect
new file mode 100644
index 00000000..42fd56a5
--- /dev/null
+++ b/Test/dafny1/MatrixFun.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 8 verified, 0 errors

diff --git a/Test/dafny1/MoreInduction.dfy b/Test/dafny1/MoreInduction.dfy
index 84c32fb3..d71c735f 100644
--- a/Test/dafny1/MoreInduction.dfy
+++ b/Test/dafny1/MoreInduction.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

 datatype List<X> = Nil | Cons(Node<X>, List<X>);

 datatype Node<X> = Element(X) | Nary(List<X>);

 

diff --git a/Test/dafny1/MoreInduction.dfy.expect b/Test/dafny1/MoreInduction.dfy.expect
new file mode 100644
index 00000000..c8785e56
--- /dev/null
+++ b/Test/dafny1/MoreInduction.dfy.expect
@@ -0,0 +1,18 @@
+MoreInduction.dfy(78,1): Error BP5003: A postcondition might not hold on this return path.

+MoreInduction.dfy(77,11): Related location: This is the postcondition that might not hold.

+Execution trace:

+    (0,0): anon0

+MoreInduction.dfy(83,1): Error BP5003: A postcondition might not hold on this return path.

+MoreInduction.dfy(82,21): Related location: This is the postcondition that might not hold.

+Execution trace:

+    (0,0): anon0

+MoreInduction.dfy(88,1): Error BP5003: A postcondition might not hold on this return path.

+MoreInduction.dfy(87,11): Related location: This is the postcondition that might not hold.

+Execution trace:

+    (0,0): anon0

+MoreInduction.dfy(93,1): Error BP5003: A postcondition might not hold on this return path.

+MoreInduction.dfy(92,22): Related location: This is the postcondition that might not hold.

+Execution trace:

+    (0,0): anon0

+

+Dafny program verifier finished with 15 verified, 4 errors

diff --git a/Test/dafny1/PriorityQueue.dfy b/Test/dafny1/PriorityQueue.dfy
index 0343cb07..4b2b2283 100644
--- a/Test/dafny1/PriorityQueue.dfy
+++ b/Test/dafny1/PriorityQueue.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

 class PriorityQueue {

   var N: int;  // capacity

   var n: int;  // current size

diff --git a/Test/dafny1/PriorityQueue.dfy.expect b/Test/dafny1/PriorityQueue.dfy.expect
new file mode 100644
index 00000000..acae4413
--- /dev/null
+++ b/Test/dafny1/PriorityQueue.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 24 verified, 0 errors

diff --git a/Test/dafny1/Queue.dfy b/Test/dafny1/Queue.dfy
index 8396ec5c..c7892df6 100644
--- a/Test/dafny1/Queue.dfy
+++ b/Test/dafny1/Queue.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

 // Queue.dfy

 // Dafny version of Queue.bpl

 // Rustan Leino, 2008

diff --git a/Test/dafny1/Queue.dfy.expect b/Test/dafny1/Queue.dfy.expect
new file mode 100644
index 00000000..39123c41
--- /dev/null
+++ b/Test/dafny1/Queue.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 22 verified, 0 errors

diff --git a/Test/dafny1/Rippling.dfy b/Test/dafny1/Rippling.dfy
index 4aaa9a38..0f32d529 100644
--- a/Test/dafny1/Rippling.dfy
+++ b/Test/dafny1/Rippling.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

 // Datatypes

 

 datatype Bool = False | True;

diff --git a/Test/dafny1/Rippling.dfy.expect b/Test/dafny1/Rippling.dfy.expect
new file mode 100644
index 00000000..5bec7f90
--- /dev/null
+++ b/Test/dafny1/Rippling.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 141 verified, 0 errors

diff --git a/Test/dafny1/SchorrWaite-stages.dfy b/Test/dafny1/SchorrWaite-stages.dfy
index 63c55506..7b2e7eda 100644
--- a/Test/dafny1/SchorrWaite-stages.dfy
+++ b/Test/dafny1/SchorrWaite-stages.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

 // Schorr-Waite algorithms, written and verified in Dafny.

 // Rustan Leino

 // Original version:  7 November 2008

diff --git a/Test/dafny1/SchorrWaite-stages.dfy.expect b/Test/dafny1/SchorrWaite-stages.dfy.expect
new file mode 100644
index 00000000..d903c7c5
--- /dev/null
+++ b/Test/dafny1/SchorrWaite-stages.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 16 verified, 0 errors

diff --git a/Test/dafny1/SchorrWaite.dfy b/Test/dafny1/SchorrWaite.dfy
index 18adf491..de07fdcc 100644
--- a/Test/dafny1/SchorrWaite.dfy
+++ b/Test/dafny1/SchorrWaite.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

 // Rustan Leino

 // 7 November 2008

 // Schorr-Waite and other marking algorithms, written and verified in Dafny.

diff --git a/Test/dafny1/SchorrWaite.dfy.expect b/Test/dafny1/SchorrWaite.dfy.expect
new file mode 100644
index 00000000..c87e2af2
--- /dev/null
+++ b/Test/dafny1/SchorrWaite.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 10 verified, 0 errors

diff --git a/Test/dafny1/SeparationLogicList.dfy b/Test/dafny1/SeparationLogicList.dfy
index 0b803afc..5a4d967f 100644
--- a/Test/dafny1/SeparationLogicList.dfy
+++ b/Test/dafny1/SeparationLogicList.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

 // This file contains three variations of the separation-logic lseg linked-list example.

 

 // In this first variation, the auxiliary information about the contents represented by a linked list

diff --git a/Test/dafny1/SeparationLogicList.dfy.expect b/Test/dafny1/SeparationLogicList.dfy.expect
new file mode 100644
index 00000000..d903c7c5
--- /dev/null
+++ b/Test/dafny1/SeparationLogicList.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 16 verified, 0 errors

diff --git a/Test/dafny1/Substitution.dfy b/Test/dafny1/Substitution.dfy
index ad39e3f2..10b70e09 100644
--- a/Test/dafny1/Substitution.dfy
+++ b/Test/dafny1/Substitution.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

 datatype List = Nil | Cons(Expr, List);

 

 datatype Expr =

diff --git a/Test/dafny1/Substitution.dfy.expect b/Test/dafny1/Substitution.dfy.expect
new file mode 100644
index 00000000..b9a9bc89
--- /dev/null
+++ b/Test/dafny1/Substitution.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 12 verified, 0 errors

diff --git a/Test/dafny1/SumOfCubes.dfy b/Test/dafny1/SumOfCubes.dfy
index 7ed7ce9b..f1bcf6c7 100644
--- a/Test/dafny1/SumOfCubes.dfy
+++ b/Test/dafny1/SumOfCubes.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

 class SumOfCubes {

   static function SumEmUp(n: int, m: int): int

     requires 0 <= n && n <= m;

diff --git a/Test/dafny1/SumOfCubes.dfy.expect b/Test/dafny1/SumOfCubes.dfy.expect
new file mode 100644
index 00000000..5f41963f
--- /dev/null
+++ b/Test/dafny1/SumOfCubes.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 17 verified, 0 errors

diff --git a/Test/dafny1/TerminationDemos.dfy b/Test/dafny1/TerminationDemos.dfy
index 0aa36a10..f8fd2953 100644
--- a/Test/dafny1/TerminationDemos.dfy
+++ b/Test/dafny1/TerminationDemos.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

 class Example {

   method M(n: int)

   {

diff --git a/Test/dafny1/TerminationDemos.dfy.expect b/Test/dafny1/TerminationDemos.dfy.expect
new file mode 100644
index 00000000..f5019f3b
--- /dev/null
+++ b/Test/dafny1/TerminationDemos.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 14 verified, 0 errors

diff --git a/Test/dafny1/TreeDatatype.dfy b/Test/dafny1/TreeDatatype.dfy
index a94283e6..763cef1b 100644
--- a/Test/dafny1/TreeDatatype.dfy
+++ b/Test/dafny1/TreeDatatype.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

 // ------------------ generic list, non-generic tree

 

 datatype List<T> = Nil | Cons(T, List<T>);

diff --git a/Test/dafny1/TreeDatatype.dfy.expect b/Test/dafny1/TreeDatatype.dfy.expect
new file mode 100644
index 00000000..c87e2af2
--- /dev/null
+++ b/Test/dafny1/TreeDatatype.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 10 verified, 0 errors

diff --git a/Test/dafny1/UltraFilter.dfy b/Test/dafny1/UltraFilter.dfy
index c78d5e81..a32e6e0b 100644
--- a/Test/dafny1/UltraFilter.dfy
+++ b/Test/dafny1/UltraFilter.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

 // ultra filter

 

 class UltraFilter<G(==)> {

diff --git a/Test/dafny1/UltraFilter.dfy.expect b/Test/dafny1/UltraFilter.dfy.expect
new file mode 100644
index 00000000..74590090
--- /dev/null
+++ b/Test/dafny1/UltraFilter.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 19 verified, 0 errors

diff --git a/Test/dafny1/UnboundedStack.dfy b/Test/dafny1/UnboundedStack.dfy
index dfc10327..58351ebb 100644
--- a/Test/dafny1/UnboundedStack.dfy
+++ b/Test/dafny1/UnboundedStack.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

 class UnboundedStack<T> {

   ghost var representation: set<object>;

   ghost var content: seq<T>;

diff --git a/Test/dafny1/UnboundedStack.dfy.expect b/Test/dafny1/UnboundedStack.dfy.expect
new file mode 100644
index 00000000..b9a9bc89
--- /dev/null
+++ b/Test/dafny1/UnboundedStack.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 12 verified, 0 errors

diff --git a/Test/dafny1/pow2.dfy b/Test/dafny1/pow2.dfy
index bc23fb0b..ad6a9737 100644
--- a/Test/dafny1/pow2.dfy
+++ b/Test/dafny1/pow2.dfy
@@ -1,3 +1,6 @@
+// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"

+// RUN: %diff "%s.expect" "%t"

+

 // This is a Dafny adaptation of a Coq program by David Pichardie.

 

 function IsEven(n: int): bool

diff --git a/Test/dafny1/pow2.dfy.expect b/Test/dafny1/pow2.dfy.expect
new file mode 100644
index 00000000..42fd56a5
--- /dev/null
+++ b/Test/dafny1/pow2.dfy.expect
@@ -0,0 +1,2 @@
+

+Dafny program verifier finished with 8 verified, 0 errors