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);
     }