The "choose" statement, hacky and specialized as it was, is now gone. Use the assign-such-that statement instead. For example: x :| x in S;

1 files changed, 1 insertions, 1 deletions

diff --git a/Test/dafny0/LoopModifies.dfy b/Test/dafny0/LoopModifies.dfy
index c9d87f86..1757836f 100644
--- a/Test/dafny0/LoopModifies.dfy
+++ b/Test/dafny0/LoopModifies.dfy
@@ -307,7 +307,7 @@ method Testing12(a: Elem, b: Elem, c: Elem)
       modifies S;

       decreases S;

    {

-      var j := choose S;

+      var j :| j in S;

       // these still good, even though S shrinks to not include them.

       a.i := i;

       b.i := i;