anchor.diff:      /// </returns>
       let optimiseGraph model optR optA verbose =
           // TODO(CaptainHayashi): Use the model for something.
  -        let f = Utils.optimiseWith optR optA verbose
  -                   [ ("graph-collapse-nops", true, removeIdStep)
  -                     ("graph-collapse-ites", true, removeITENodeStep) ]
  -        liftNodeOptimisation f
  +        onNodes (Utils.optimiseWith optR optA verbose
  +                     [ ("graph-collapse-nops", true, collapseNops)
  +                       ("graph-collapse-ites", true, collapseITEs) ] )
   
       /// <summary>
       ///     Optimises a model over graphs.
  
positive.code:          *)
          if (Seq.isEmpty xs)
          then newGraph
          else liftNodeOptimisation opt newGraph
  
      /// <summary>
      ///     Removes a node if it is an ITE-guarded view.
      ///
      ///     <para>
      ///         An ITE-guarded view is a view with one in-edge,
      ///         two guarded funcs which negate each other, and two
      ///         out-edges, each assuming one of the guards.
      ///     </para>
      /// </summary>
      /// <param name="_arg1">
      ///     A triple of:
      ///     the list of nodes already removed, which is appended to in the
      ///     result;
      ///     the graph to optimise (perhaps);
      ///     an Option containing the name of the node to optimise.
      /// </param>
      /// <returns>
      ///     A triple containing the list of edge names removed, an
      ///     optimised graph, and an Option containing the node name if it was
      ///     not removed.
      /// </returns>
      let removeITENodeStep (removed, g, nNameOpt) =
          // Does nName actually exist, and is it an ITE node?
          match (nNameOpt,
                 Option.bind (fun o -> Map.tryFind o g.Contents)
                             nNameOpt) with
          | (Some nName,
             Some (ITEGuards ({ Cond = xc },
                              { Cond = yc }), outEdges, inEdges)) ->
              // Are there only two out edges, and only one in edges?
              if (Set.count outEdges = 2 && Set.count inEdges = 1)
              then
                  let oE, iE = Set.toList outEdges, Set.toList inEdges
                  let outA, outB = oE.[0], oE.[1]
                  let inA : InEdge = iE.[0]
  
                  (* Translate xc and yc to pre-state, because that's what
                   * the assumes will be.
                   *)
                  let xcPre = (liftMarker Before always).BSub xc
                  let ycPre = (liftMarker Before always).BSub yc
  
                  // Are the out edges assumes over xc and yc?
                  match (outA.Command, outB.Command) with
                  | ([ { Name = aN ; Params = [ BExpr aP ] } ],
                     [ { Name = bN ; Params = [ BExpr bP ] } ])
                    when (aN = "Assume" && bN = "Assume"
                          && (equivHolds
                                  (orEquiv
                                       (andEquiv (equiv aP xcPre)
                                                 (equiv bP ycPre))
                                       (andEquiv (equiv aP ycPre)
                                                 (equiv bP xcPre))))) ->
                      let removed' =
                          outA.Name :: outB.Name :: inA.Name :: removed
  
                      let aCmd = inA.Command @ outA.Command
  
                      g
                      // Remove the existing edges first.
                      |> rmEdgesBetween inA.Src nName
                      |> rmEdgesBetween nName outA.Dest
                      |> rmEdgesBetween nName outB.Dest
                      // Then, remove the node.
                      |> rmNode nName
                      // Then, add the new edges.
                      |> mkEdgeBetween (String.concat "__" [ inA.Name
                                                             outA.Name ])
                                       inA.Src
                                       outA.Dest
                                       (inA.Command @ outA.Command)
                      |> mkEdgeBetween (String.concat "__" [ inA.Name
                                                             outB.Name ])
                                       inA.Src
                                       outB.Dest
                                       (inA.Command @ outB.Command)
                      |> (fun g' -> removed', g', None)
                  | _ -> (removed, g, nNameOpt)
              else (removed, g, nNameOpt)
          | _ -> (removed, g, nNameOpt)
  
      /// <summary>
      ///     Optimises a graph.
  
negative.code:     ///     an Option containing the name of the node to optimise.
      /// </param>
      /// <returns>
      ///     A triple containing the list of edge names removed, an
      ///     optimised graph, and an Option containing the node name if it was
      ///     not removed.
      /// </returns>
      let collapseITEs =
          expandNodeIn <|
              fun nName nView outEdges inEdges g removed ->
                  match nView with
                  | ITEGuards ({ Cond = xc }, { Cond = yc }) ->
                      // Are there only two out edges, and only one in edges?
                      if (Set.count outEdges = 2 && Set.count inEdges = 1)
                      then
                          let oE, iE = Set.toList outEdges, Set.toList inEdges
                          let outA, outB = oE.[0], oE.[1]
                          let inA : InEdge = iE.[0]
  
                          (* Translate xc and yc to pre-state, to match the
                             commands. *)
                          let xcPre = (liftMarker Before always).BSub xc
                          let ycPre = (liftMarker Before always).BSub yc
  
                          // Are the out edges assumes over xc and yc?
                          match (outA.Command, outB.Command) with
                          | ([ { Name = aN ; Params = [ BExpr aP ] } ],
                             [ { Name = bN ; Params = [ BExpr bP ] } ])
                              when (aN = "Assume" && bN = "Assume"
                                    && equivHolds <|
                                           orEquiv
                                               (andEquiv (equiv aP xcPre)
                                                         (equiv bP ycPre))
                                               (andEquiv (equiv aP ycPre)
                                                         (equiv bP xcPre))) ->
                              let removed' =
                                  outA.Name :: outB.Name :: inA.Name :: removed
  
                              let aCmd = inA.Command @ outA.Command
  
                              g
                              // Remove the existing edges first.
                              |> rmEdgesBetween inA.Src nName
                              |> rmEdgesBetween nName outA.Dest
                              |> rmEdgesBetween nName outB.Dest
                              // Then, remove the node.
                              |> rmNode nName
                              // Then, add the new edges.
                              |> mkEdgeBetween (glueNames inA outA)
                                               inA.Src
                                               outA.Dest
                                               (inA.Command @ outA.Command)
                              |> mkEdgeBetween (glueNames inA outB)
                                               inA.Src
                                               outB.Dest
                                               (inA.Command @ outB.Command)
                              |> (fun g' -> removed', g', None)
                          | _ -> (removed, g, Some nName)
                      else (removed, g, Some nName)
                  | _ -> (removed, g, Some nName)
  
  
      /// <summary>
      ///     Performs a node-wise optimisation on every node in the graph.
  