3 files changed, 7 insertions, 11 deletions
diff --git a/Test/dafny1/ExtensibleArray.dfy b/Test/dafny1/ExtensibleArray.dfy
index b790eea5..4ceca552 100644
--- a/Test/dafny1/ExtensibleArray.dfy
+++ b/Test/dafny1/ExtensibleArray.dfy
@@ -39,7 +39,7 @@ class ExtensibleArray<T> {
     ensures Valid() && fresh(Repr - {this});
     ensures Contents == [];
   {
-    var arr := new T[256];  elements := arr;
+    elements := new T[256];
     more := null;
     length := 0;
     M := 0;
@@ -90,15 +90,14 @@ class ExtensibleArray<T> {
       elements[length - M] := t;
     } else {
       if (more == null) {
-        var mr := new ExtensibleArray<array<T>>.Init();
-        more := mr;
-        Repr := Repr + {mr} + mr.Repr;
+        more := new ExtensibleArray<array<T>>.Init();
+        Repr := Repr + {more} + more.Repr;
       }
       // "elements" is full, so move it into "more" and allocate a new array
       call more.Append(elements);
       Repr := Repr + more.Repr;
       M := M + 256;
-      var arr := new T[256];  elements := arr;
+      elements := new T[256];
       Repr := Repr + {elements};
       elements[0] := t;
     }
diff --git a/Test/dafny1/PriorityQueue.dfy b/Test/dafny1/PriorityQueue.dfy
index 957eb7cb..db1c60fa 100644
--- a/Test/dafny1/PriorityQueue.dfy
+++ b/Test/dafny1/PriorityQueue.dfy
@@ -27,8 +27,7 @@ class PriorityQueue {
     ensures N == capacity;
   {
     N := capacity;
-    var arr := new int[N+1];
-    a := arr;
+    a := new int[N+1];
     n := 0;
     Repr := {this};
     Repr := Repr + {a};
@@ -143,8 +142,7 @@ class PriorityQueue_Alternative {
     ensures N == capacity;
   {
     N := capacity;
-    var arr := new int[N+1];
-    a := arr;
+    a := new int[N+1];
     n := 0;
     Repr := {this};
     Repr := Repr + {a};
diff --git a/Test/dafny1/UnboundedStack.dfy b/Test/dafny1/UnboundedStack.dfy
index 940e1a0a..dfc10327 100644
--- a/Test/dafny1/UnboundedStack.dfy
+++ b/Test/dafny1/UnboundedStack.dfy
@@ -31,8 +31,7 @@ class UnboundedStack<T> {
     ensures IsUnboundedStack();
     ensures content == [val] + old(content);
   {
-    var tmp := new Node<T>.InitNode(val,top);
-    top := tmp;
+    top := new Node<T>.InitNode(val,top);
     representation := representation + top.footprint;
     content := [val] + content;
   }