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, 2 insertions, 2 deletions

diff --git a/Test/vstte2012/BreadthFirstSearch.dfy b/Test/vstte2012/BreadthFirstSearch.dfy
index e1a93730..ac070ac6 100644
--- a/Test/vstte2012/BreadthFirstSearch.dfy
+++ b/Test/vstte2012/BreadthFirstSearch.dfy
@@ -80,7 +80,7 @@ class BreadthFirstSearch<Vertex(==)>
       decreases AllVertices - Processed;

     {

       // remove a vertex "v" from "C"

-      var v := choose C;

+      var v :| v in C;

       C, Processed := C - {v}, Processed + {v};

       ghost var pathToV := Find(source, v, paths);

     

@@ -264,7 +264,7 @@ class BreadthFirstSearch<Vertex(==)>
     if (vSuccs == {}) {

       newPaths := paths;

     } else {

-      var succ := choose vSuccs;

+      var succ :| succ in vSuccs;

       newPaths := Maplet(Domain(paths) + {succ}, succ, pathToV + [v], paths);

       newPaths := UpdatePaths(vSuccs - {succ}, source, newPaths, v, pathToV);

     }