iter.remove();
}
}
/* Since the agenda is already sorted it is more efficient
* to sort the children only and then merge. */
children.sort(Rule.optimisticThenObservedComparator);
nodes.merge(children, Rule.optimisticThenObservedComparator);
} else {
/* The agenda being sorted, it is not worth considering the following
* nodes. */
break;