diff --git a/infer/src/topl/ToplAst.ml b/infer/src/topl/ToplAst.ml
index a9a9d8868..9bf8136a7 100644
--- a/infer/src/topl/ToplAst.ml
+++ b/infer/src/topl/ToplAst.ml
@@ -42,4 +42,8 @@ type vertex = string [@@deriving compare, hash, sexp]
 type transition = {source: vertex; target: vertex; label: label}
 
 type t =
-  {name: property_name; message: string option; prefixes: string list; transitions: transition list}
+  { name: property_name
+  ; message: string option
+  ; prefixes: string list
+  ; nondet: string list
+  ; transitions: transition list }
diff --git a/infer/src/topl/ToplAutomaton.ml b/infer/src/topl/ToplAutomaton.ml
index 0fdad01f6..e569f089d 100644
--- a/infer/src/topl/ToplAutomaton.ml
+++ b/infer/src/topl/ToplAutomaton.ml
@@ -6,6 +6,7 @@
  *)
 
 open! IStd
+module L = Logging
 
 let tt = ToplUtils.debug
 
@@ -26,25 +27,39 @@ type tindex = int
 
 type transition = {source: vindex; target: vindex; label: ToplAst.label}
 
-(** - INV1: Array.length states = Array.length outgoing
+(** - INV1: Array.length states = Array.length outgoing = Array.length nondets
     - INV2: Array.length transitions = Array.length skips
     - INV3: each index of [transitions] occurs exactly once in one of [outgoing]'s lists
-    - INV4: max_args is the maximum length of the arguments list in a label on a transition The
-      fields marked as redundant are computed from the others (when the automaton is built), and are
-      cached for speed. *)
+    - INV4: max_args is the maximum length of the arguments list in a label on a transition
+
+    The fields marked as redundant are computed from the others (when the automaton is built), and
+    are cached for speed. *)
 type t =
   { states: vname array
+  ; nondets: bool array (* redundant *)
   ; transitions: transition array
   ; skips: bool array (* redundant *)
   ; outgoing: tindex list array
   ; vindex: vname -> vindex
-  ; max_args: int (* redundant; cached for speed *) }
+  ; max_args: int (* redundant *) }
 
-(** [index_in H a x] is the (last) index of [x] in array [a]. *)
-let index_in (type k) (module H : Hashtbl_intf.S with type key = k) (a : k array) : k -> int =
+(** [index_in H a] returns a pair of functions [(opt, err)] that lookup the (last) index of an
+    element in [a]. The difference is that [opt x] returns an option, while [err msg x] makes Infer
+    die, mentioning [msg].*)
+let index_in (type k) (module H : Hashtbl_intf.S with type key = k) (a : k array) :
+    (k -> int option) * (string -> k -> int) =
   let h = H.create ~size:(2 * Array.length a) () in
   let f i x = H.set h ~key:x ~data:i in
-  Array.iteri ~f a ; H.find_exn h
+  Array.iteri ~f a ;
+  let opt = H.find h in
+  let err msg x =
+    match opt x with
+    | Some x ->
+        x
+    | None ->
+        L.die InternalError "ToplAutomaton.index_in out of bounds (%s)" msg
+  in
+  (opt, err)
 
 
 let make properties =
@@ -57,7 +72,8 @@ let make properties =
     Array.of_list (List.dedup_and_sort ~compare:Vname.compare (List.concat_map ~f properties))
   in
   Array.iteri ~f:(fun i (p, v) -> tt "state[%d]=(%s,%s)@\n" i p v) states ;
-  let vindex = index_in (module Vname.Table) states in
+  let vindex_opt, vindex = index_in (module Vname.Table) states in
+  let vindex = vindex "vertex" in
   let transitions : transition array =
     let f p =
       let prefix_pname pname =
@@ -92,6 +108,23 @@ let make properties =
     in
     Array.fold ~init:0 ~f transitions
   in
+  let nondets : bool array =
+    let vcount = Array.length states in
+    let a = Array.create ~len:vcount false in
+    let f ToplAst.{nondet; name; _} =
+      let set_nondet state =
+        match vindex_opt (name, state) with
+        | Some i ->
+            a.(i) <- true
+        | None ->
+            L.user_warning
+              "TOPL: %s declared as nondet, but it appears in no transition of property %s" state
+              name
+      in
+      List.iter ~f:set_nondet nondet
+    in
+    List.iter ~f properties ; a
+  in
   let skips : bool array =
     let is_skip {source; target; label} =
       let r = Int.equal source target in
@@ -104,13 +137,15 @@ let make properties =
     in
     Array.map ~f:is_skip transitions
   in
-  {states; transitions; skips; outgoing; vindex; max_args}
+  {states; nondets; transitions; skips; outgoing; vindex; max_args}
 
 
 let outgoing a i = a.outgoing.(i)
 
 let vname a i = a.states.(i)
 
+let is_nondet a i = a.nondets.(i)
+
 let vcount a = Array.length a.states
 
 let transition a i = a.transitions.(i)
diff --git a/infer/src/topl/ToplAutomaton.mli b/infer/src/topl/ToplAutomaton.mli
index 7961b8974..4d87817de 100644
--- a/infer/src/topl/ToplAutomaton.mli
+++ b/infer/src/topl/ToplAutomaton.mli
@@ -37,6 +37,8 @@ val outgoing : t -> vindex -> tindex list
 
 val vname : t -> vindex -> vname
 
+val is_nondet : t -> vindex -> bool
+
 val vcount : t -> int
 
 val transition : t -> tindex -> transition
diff --git a/infer/src/topl/ToplLexer.mll b/infer/src/topl/ToplLexer.mll
index bc1cf1335..efcd54dfc 100644
--- a/infer/src/topl/ToplLexer.mll
+++ b/infer/src/topl/ToplLexer.mll
@@ -54,6 +54,7 @@ rule raw_token = parse
   | "prefix" { PREFIX }
   | "property" { PROPERTY }
   | "message" { MESSAGE }
+  | "nondet" { NONDET }
   | ['a'-'z'] id_tail as id { LID id }
   | ['A'-'Z'] id_tail as id { UID id }
   | eof { EOF }
diff --git a/infer/src/topl/ToplMonitor.ml b/infer/src/topl/ToplMonitor.ml
index f57f3f721..1572b2ffd 100644
--- a/infer/src/topl/ToplMonitor.ml
+++ b/infer/src/topl/ToplMonitor.ml
@@ -341,7 +341,9 @@ let generate_execute_state automaton proc_name =
     in
     let transitions = ToplAutomaton.outgoing automaton state in
     let fold f init = List.fold_right ~init ~f transitions in
-    fold check_transition_maybe (fold check_transition skip)
+    let detbranches = fold check_transition skip in
+    if ToplAutomaton.is_nondet automaton state then fold check_transition_maybe detbranches
+    else detbranches
   in
   let body =
     gen_if
diff --git a/infer/src/topl/ToplParser.mly b/infer/src/topl/ToplParser.mly
index 7ee1bdc50..aa4fcab8f 100644
--- a/infer/src/topl/ToplParser.mly
+++ b/infer/src/topl/ToplParser.mly
@@ -29,6 +29,7 @@
 %token LT
 %token MESSAGE
 %token NE
+%token NONDET
 %token PREFIX
 %token PROPERTY
 %token RC
@@ -42,17 +43,22 @@
 properties: ps=one_property* EOF { ps }
 
 one_property:
-    PROPERTY name=identifier LC message=message? prefixes=prefix* transitions=transition* RC
-    { ToplAst.{name; message; prefixes; transitions} }
+    PROPERTY name=identifier LC message=message? prefixes=prefix* nondet=nondet
+      transitions=transition* RC
+    { ToplAst.{name; message; prefixes; nondet; transitions} }
 
 message: MESSAGE s=STRING { s }
 
 prefix: PREFIX s=STRING { s }
 
+nondet: NONDET LP ns=state* RP { ns }
+
 transition:
-    source=identifier ARROW target=identifier COLON label=label
+    source=state ARROW target=state COLON label=label
     { ToplAst.{source; target; label} }
 
+state: i=identifier { i }
+
 label:
     return=value_pattern ASGN cp=call_pattern condition=condition?
     { let procedure_name, arguments = cp in
diff --git a/infer/tests/codetoanalyze/java/topl/SkipAfterRemove.topl b/infer/tests/codetoanalyze/java/topl/SkipAfterRemove.topl
index 57ab29b1b..fb77d5d48 100644
--- a/infer/tests/codetoanalyze/java/topl/SkipAfterRemove.topl
+++ b/infer/tests/codetoanalyze/java/topl/SkipAfterRemove.topl
@@ -1,5 +1,6 @@
 property SkipAfterRemove
   prefix "ArrayList"
+  nondet (start)
   start -> start: *
   start -> removed: remove(Collection, Index)
   removed -> ok:    get(collection, index)
diff --git a/infer/tests/codetoanalyze/java/topl/hasnext.topl b/infer/tests/codetoanalyze/java/topl/hasnext.topl
index 8a08339c5..c9a598ed3 100644
--- a/infer/tests/codetoanalyze/java/topl/hasnext.topl
+++ b/infer/tests/codetoanalyze/java/topl/hasnext.topl
@@ -2,6 +2,7 @@ property HasNext
   prefix "Iterator"
   prefix "List"
   prefix "Scanner"
+  nondet (start)
   start -> start: *
   start -> invalid: I = iterator(*)
   start -> invalid: Scanner(I, *)  // For constructors, biabduction has "this" as first argument
diff --git a/infer/tests/codetoanalyze/java/topl/issues.exp b/infer/tests/codetoanalyze/java/topl/issues.exp
index 984715fd6..29d13a156 100644
--- a/infer/tests/codetoanalyze/java/topl/issues.exp
+++ b/infer/tests/codetoanalyze/java/topl/issues.exp
@@ -1,8 +1,8 @@
-codetoanalyze/java/topl/IndexSkip.java, IndexSkip.foo(java.util.ArrayList):void, 2, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure foo(...),Taking true branch,Skipping get(...): unknown method,start of procedure saveArgs(...),return from a call to void Property.saveArgs(Object,ArrayList,Object),start of procedure execute(),start of procedure execute_state_0(),Taking false branch,return from a call to void Property.execute_state_0(),start of procedure execute_state_1(),Taking true branch,start of procedure maybe(),return from a call to void Property.maybe(),Taking false branch,start of procedure maybe(),return from a call to void Property.maybe(),Taking false branch,Taking false branch,Taking false branch,return from a call to void Property.execute_state_1(),start of procedure execute_state_2(),Taking false branch,return from a call to void Property.execute_state_2(),start of procedure execute_state_3(),Taking false branch,return from a call to void Property.execute_state_3(),start of procedure execute_state_4(),Taking false branch,return from a call to void Property.execute_state_4(),start of procedure execute_state_5(),Taking false branch,return from a call to void Property.execute_state_5(),start of procedure execute_state_6(),Taking false branch,return from a call to void Property.execute_state_6(),start of procedure execute_state_7(),Taking false branch,return from a call to void Property.execute_state_7(),return from a call to void Property.execute()]
+codetoanalyze/java/topl/IndexSkip.java, IndexSkip.foo(java.util.ArrayList):void, 2, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure foo(...),Taking true branch,Skipping get(...): unknown method,start of procedure saveArgs(...),return from a call to void Property.saveArgs(Object,ArrayList,Object),start of procedure execute(),start of procedure execute_state_0(),Taking false branch,return from a call to void Property.execute_state_0(),start of procedure execute_state_1(),Taking true branch,Taking false branch,Taking false branch,return from a call to void Property.execute_state_1(),start of procedure execute_state_2(),Taking false branch,return from a call to void Property.execute_state_2(),start of procedure execute_state_3(),Taking false branch,return from a call to void Property.execute_state_3(),start of procedure execute_state_4(),Taking false branch,return from a call to void Property.execute_state_4(),start of procedure execute_state_5(),Taking false branch,return from a call to void Property.execute_state_5(),start of procedure execute_state_6(),Taking false branch,return from a call to void Property.execute_state_6(),start of procedure execute_state_7(),Taking false branch,return from a call to void Property.execute_state_7(),return from a call to void Property.execute()]
 codetoanalyze/java/topl/Iterators.java, Iterators.hasNextBad(java.util.List):void, 0, TOPL_ERROR, no_bucket, ERROR, []
-codetoanalyze/java/topl/Iterators.java, Iterators.hasNextBad(java.util.List):void, 2, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure hasNextBad(...),Skipping iterator(): unknown method,start of procedure saveArgs(...),return from a call to void Property.saveArgs(Object,List),start of procedure execute(),start of procedure execute_state_0(),Taking false branch,return from a call to void Property.execute_state_0(),start of procedure execute_state_1(),Taking true branch,start of procedure maybe(),return from a call to void Property.maybe(),Taking false branch,start of procedure maybe(),return from a call to void Property.maybe(),Taking false branch,Taking false branch,Taking false branch,return from a call to void Property.execute_state_1(),start of procedure execute_state_2(),Taking false branch,return from a call to void Property.execute_state_2(),start of procedure execute_state_3(),Taking false branch,return from a call to void Property.execute_state_3(),start of procedure execute_state_4(),Taking false branch,return from a call to void Property.execute_state_4(),start of procedure execute_state_5(),Taking false branch,return from a call to void Property.execute_state_5(),start of procedure execute_state_6(),Taking false branch,return from a call to void Property.execute_state_6(),start of procedure execute_state_7(),Taking false branch,return from a call to void Property.execute_state_7(),return from a call to void Property.execute()]
+codetoanalyze/java/topl/Iterators.java, Iterators.hasNextBad(java.util.List):void, 2, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure hasNextBad(...),Skipping iterator(): unknown method,start of procedure saveArgs(...),return from a call to void Property.saveArgs(Object,List),start of procedure execute(),start of procedure execute_state_0(),Taking false branch,return from a call to void Property.execute_state_0(),start of procedure execute_state_1(),Taking true branch,Taking false branch,Taking false branch,return from a call to void Property.execute_state_1(),start of procedure execute_state_2(),Taking false branch,return from a call to void Property.execute_state_2(),start of procedure execute_state_3(),Taking false branch,return from a call to void Property.execute_state_3(),start of procedure execute_state_4(),Taking false branch,return from a call to void Property.execute_state_4(),start of procedure execute_state_5(),Taking false branch,return from a call to void Property.execute_state_5(),start of procedure execute_state_6(),Taking false branch,return from a call to void Property.execute_state_6(),start of procedure execute_state_7(),Taking false branch,return from a call to void Property.execute_state_7(),return from a call to void Property.execute()]
 codetoanalyze/java/topl/Iterators.java, Iterators.hasNextInterproceduralBad(java.util.List):void, 0, TOPL_ERROR, no_bucket, ERROR, []
-codetoanalyze/java/topl/Iterators.java, Iterators.hasNextInterproceduralBad(java.util.List):void, 1, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure hasNextInterproceduralBad(...),Skipping iterator(): unknown method,start of procedure saveArgs(...),return from a call to void Property.saveArgs(Object,List),start of procedure execute(),start of procedure execute_state_0(),Taking false branch,return from a call to void Property.execute_state_0(),start of procedure execute_state_1(),Taking true branch,start of procedure maybe(),return from a call to void Property.maybe(),Taking false branch,start of procedure maybe(),return from a call to void Property.maybe(),Taking false branch,Taking false branch,Taking false branch,return from a call to void Property.execute_state_1(),start of procedure execute_state_2(),Taking false branch,return from a call to void Property.execute_state_2(),start of procedure execute_state_3(),Taking false branch,return from a call to void Property.execute_state_3(),start of procedure execute_state_4(),Taking false branch,return from a call to void Property.execute_state_4(),start of procedure execute_state_5(),Taking false branch,return from a call to void Property.execute_state_5(),start of procedure execute_state_6(),Taking false branch,return from a call to void Property.execute_state_6(),start of procedure execute_state_7(),Taking false branch,return from a call to void Property.execute_state_7(),return from a call to void Property.execute(),start of procedure getSingleElementOk(...),Skipping next(): unknown method]
-codetoanalyze/java/topl/Iterators.java, Iterators.hasNextInterproceduralOk(java.util.List):void, 2, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure hasNextInterproceduralOk(...),Skipping iterator(): unknown method,start of procedure saveArgs(...),return from a call to void Property.saveArgs(Object,List),start of procedure execute(),start of procedure execute_state_0(),Taking false branch,return from a call to void Property.execute_state_0(),start of procedure execute_state_1(),Taking true branch,start of procedure maybe(),return from a call to void Property.maybe(),Taking false branch,start of procedure maybe(),return from a call to void Property.maybe(),Taking false branch,Taking false branch,Taking false branch,return from a call to void Property.execute_state_1(),start of procedure execute_state_2(),Taking false branch,return from a call to void Property.execute_state_2(),start of procedure execute_state_3(),Taking false branch,return from a call to void Property.execute_state_3(),start of procedure execute_state_4(),Taking false branch,return from a call to void Property.execute_state_4(),start of procedure execute_state_5(),Taking false branch,return from a call to void Property.execute_state_5(),start of procedure execute_state_6(),Taking false branch,return from a call to void Property.execute_state_6(),start of procedure execute_state_7(),Taking false branch,return from a call to void Property.execute_state_7(),return from a call to void Property.execute()]
-codetoanalyze/java/topl/Iterators.java, Iterators.hasNextOk(java.util.List):void, 2, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure hasNextOk(...),Skipping iterator(): unknown method,start of procedure saveArgs(...),return from a call to void Property.saveArgs(Object,List),start of procedure execute(),start of procedure execute_state_0(),Taking false branch,return from a call to void Property.execute_state_0(),start of procedure execute_state_1(),Taking true branch,start of procedure maybe(),return from a call to void Property.maybe(),Taking false branch,start of procedure maybe(),return from a call to void Property.maybe(),Taking false branch,Taking false branch,Taking false branch,return from a call to void Property.execute_state_1(),start of procedure execute_state_2(),Taking false branch,return from a call to void Property.execute_state_2(),start of procedure execute_state_3(),Taking false branch,return from a call to void Property.execute_state_3(),start of procedure execute_state_4(),Taking false branch,return from a call to void Property.execute_state_4(),start of procedure execute_state_5(),Taking false branch,return from a call to void Property.execute_state_5(),start of procedure execute_state_6(),Taking false branch,return from a call to void Property.execute_state_6(),start of procedure execute_state_7(),Taking false branch,return from a call to void Property.execute_state_7(),return from a call to void Property.execute()]
+codetoanalyze/java/topl/Iterators.java, Iterators.hasNextInterproceduralBad(java.util.List):void, 1, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure hasNextInterproceduralBad(...),Skipping iterator(): unknown method,start of procedure saveArgs(...),return from a call to void Property.saveArgs(Object,List),start of procedure execute(),start of procedure execute_state_0(),Taking false branch,return from a call to void Property.execute_state_0(),start of procedure execute_state_1(),Taking true branch,Taking false branch,Taking false branch,return from a call to void Property.execute_state_1(),start of procedure execute_state_2(),Taking false branch,return from a call to void Property.execute_state_2(),start of procedure execute_state_3(),Taking false branch,return from a call to void Property.execute_state_3(),start of procedure execute_state_4(),Taking false branch,return from a call to void Property.execute_state_4(),start of procedure execute_state_5(),Taking false branch,return from a call to void Property.execute_state_5(),start of procedure execute_state_6(),Taking false branch,return from a call to void Property.execute_state_6(),start of procedure execute_state_7(),Taking false branch,return from a call to void Property.execute_state_7(),return from a call to void Property.execute(),start of procedure getSingleElementOk(...),Skipping next(): unknown method]
+codetoanalyze/java/topl/Iterators.java, Iterators.hasNextInterproceduralOk(java.util.List):void, 2, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure hasNextInterproceduralOk(...),Skipping iterator(): unknown method,start of procedure saveArgs(...),return from a call to void Property.saveArgs(Object,List),start of procedure execute(),start of procedure execute_state_0(),Taking false branch,return from a call to void Property.execute_state_0(),start of procedure execute_state_1(),Taking true branch,Taking false branch,Taking false branch,return from a call to void Property.execute_state_1(),start of procedure execute_state_2(),Taking false branch,return from a call to void Property.execute_state_2(),start of procedure execute_state_3(),Taking false branch,return from a call to void Property.execute_state_3(),start of procedure execute_state_4(),Taking false branch,return from a call to void Property.execute_state_4(),start of procedure execute_state_5(),Taking false branch,return from a call to void Property.execute_state_5(),start of procedure execute_state_6(),Taking false branch,return from a call to void Property.execute_state_6(),start of procedure execute_state_7(),Taking false branch,return from a call to void Property.execute_state_7(),return from a call to void Property.execute()]
+codetoanalyze/java/topl/Iterators.java, Iterators.hasNextOk(java.util.List):void, 2, NULL_DEREFERENCE, no_bucket, ERROR, [start of procedure hasNextOk(...),Skipping iterator(): unknown method,start of procedure saveArgs(...),return from a call to void Property.saveArgs(Object,List),start of procedure execute(),start of procedure execute_state_0(),Taking false branch,return from a call to void Property.execute_state_0(),start of procedure execute_state_1(),Taking true branch,Taking false branch,Taking false branch,return from a call to void Property.execute_state_1(),start of procedure execute_state_2(),Taking false branch,return from a call to void Property.execute_state_2(),start of procedure execute_state_3(),Taking false branch,return from a call to void Property.execute_state_3(),start of procedure execute_state_4(),Taking false branch,return from a call to void Property.execute_state_4(),start of procedure execute_state_5(),Taking false branch,return from a call to void Property.execute_state_5(),start of procedure execute_state_6(),Taking false branch,return from a call to void Property.execute_state_6(),start of procedure execute_state_7(),Taking false branch,return from a call to void Property.execute_state_7(),return from a call to void Property.execute()]
 codetoanalyze/java/topl/ScannerFail.java, ScannerFail.readBad():void, 0, TOPL_ERROR, no_bucket, ERROR, []
diff --git a/infer/tests/codetoanalyze/java/topl/iterators.topl b/infer/tests/codetoanalyze/java/topl/iterators.topl
index 4ffad0d1b..34d37da30 100644
--- a/infer/tests/codetoanalyze/java/topl/iterators.topl
+++ b/infer/tests/codetoanalyze/java/topl/iterators.topl
@@ -1,6 +1,7 @@
 property HasNext
   prefix "Iterator"
   prefix "List"
+  nondet (start)
   start -> start: *
   start -> invalid: I = iterator(*)
   invalid -> valid: <true> = hasNext(i) // treat as shorthand for <B> = hasNext if (b)
@@ -10,12 +11,15 @@ property HasNext
 property UnsafeIterator
   prefix "Collection"
   prefix "Iterator"
+  nondet (start)
+  start -> start: *
   start -> iterating: I = iterator(C)
   iterating -> modified: remove(c, *)
   iterating -> modified: add(c, *)
   modified -> error: next(i)
 
 property UnsafeMapIterator
+  nondet (start)
   start -> start: *
   start -> gotView: View = keySet(M)
   start -> gotView: View = values(M)
@@ -25,7 +29,8 @@ property UnsafeMapIterator
 
 property SkipIndexAfterRemove
   prefix "ArrayList"
+  nondet (start)
   start -> start: *
   start -> removed: remove(Collection, Index)
   removed -> ok:    get(collection, index)
-  removed -> error: get(collection, J) // TODO: if (j!=index)
+  removed -> error: get(collection, J) if J != index
diff --git a/infer/tests/codetoanalyze/java/topl/tomcat.topl b/infer/tests/codetoanalyze/java/topl/tomcat.topl
index b7d3e4413..d259bda25 100644
--- a/infer/tests/codetoanalyze/java/topl/tomcat.topl
+++ b/infer/tests/codetoanalyze/java/topl/tomcat.topl
@@ -4,12 +4,13 @@ property ForwardUncommitted
   prefix "javax.servlet"
   prefix "javax.servlet.{ServletOutputStream,ServletResponse}"
   prefix "java.io.PrintWriter"
+  nondet (start)
   start -> start: *
   start -> tracking: R = "ServletResponse.\<init\>"
   tracking -> ok: flushBuffer(r)
   tracking -> gotWriter: W = getWriter(r)
   gotWriter -> ok: flush(w)
-  gotWrite -> ok: flushBuffer(r)
+  gotWriter -> ok: flushBuffer(r)
   tracking -> gotStream: S = getOutputStream(r)
   gotStream -> ok: flush(s)
   gotStream -> ok: flushBuffer(r)
@@ -24,6 +25,7 @@ property ForwardUncommitted
 property InterleavedResponse1
   message "A ServletResponse was asked for both a writer and a stream."
   prefix "javax.servlet.ServletResponse"
+  nondet (start)
   start -> start: *
   start -> gotWriter: W = getWriter(R)
   start -> gotStream: S = getOutputStream(R)
@@ -34,6 +36,7 @@ property InterleavedResponse2
   // vertex names: w = got writer; W = used writer; similarly for s, S
   message "Incompatible methods for putting data into a response were used."
   prefix "javax.servlet.ServletResponse"
+  nondet (start)
   start -> start: *
   start -> w: W = getWriter(R)
   start -> s: S = getOutputStream(R)