From 5296b17758c3e27bf551e9a322323a37983d7abb Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Wed, 27 Mar 2013 13:51:16 -0700
Subject: 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;

---
 Test/vstte2012/BreadthFirstSearch.dfy | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'Test/vstte2012')

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);
     }
-- 
cgit v1.2.3