The Dafny call statement now automatically declares left-hand sides as local variables, if they were not already local variables.

1 files changed, 0 insertions, 3 deletions

diff --git a/Test/VSI-Benchmarks/b7.dfy b/Test/VSI-Benchmarks/b7.dfy
index 95267823..f7d51058 100644
--- a/Test/VSI-Benchmarks/b7.dfy
+++ b/Test/VSI-Benchmarks/b7.dfy
@@ -129,12 +129,10 @@ class Client {
 		call rd.Open();

 		

 		var q:= new Queue<int>;	

-		var ch;

 		while (true)

 		 invariant rd.Valid() && fresh(rd.footprint) && fresh(q);

 		 decreases |rd.stream|;

 		{

-				var eos:bool;

 				call eos := rd.AtEndOfStream();

 				if (eos) 

 				{

@@ -146,7 +144,6 @@ class Client {
 	    }

 	    

 	    call rd.Close();

-	    var perm;

 	    call q,perm := Sort(q);

 	    

 	    var wr:= new Stream;