Dafny: support assign-such-that in var declarations in refinements

1 files changed, 2 insertions, 2 deletions

diff --git a/Test/dafny2/StoreAndRetrieve.dfy b/Test/dafny2/StoreAndRetrieve.dfy
index 1357b65c..ea26a234 100644
--- a/Test/dafny2/StoreAndRetrieve.dfy
+++ b/Test/dafny2/StoreAndRetrieve.dfy
@@ -18,7 +18,7 @@ module A imports Library {
       ensures Contents == old(Contents);

       ensures thing in Contents && Function.Apply(matchCriterion, thing);

     {

-      var k;  assume k in Contents && Function.Apply(matchCriterion, k);

+      var k :| k in Contents && Function.Apply(matchCriterion, k);

       thing := k;

     }

   }

@@ -49,7 +49,7 @@ module B refines A {
         if (Function.Apply(matchCriterion, arr[i])) { break; }

         i := i + 1;

       }

-      var k := arr[i];  assert ...;

+      var k := arr[i];

     }

   }

 }