- let status3 =
- if status2.NodeStatus.node.todo == StateSet.empty then status2
- else begin
- let status3 = eval_trans auto cache2 cache5 tag fcs1 nss1 ps status2 in
- IFTRACE(html tree node _i status3
- "Updating transitions (after next-sibling)");
- if status3 != status2 then status.(node_id) <- status3;
- status3
- end
- in
- let unstable_self =
- (* if either our left or right child is unstable or if we
- still have transitions pending, the current node is
- unstable *)
- unstable_left
- || unstable_right
- || StateSet.empty != status3.NodeStatus.node.todo
- in
- Bitvector.unsafe_set unstable node_id unstable_self;
- IFTRACE((if not unstable_self then
- Html.finalize_node
- node_id
- _i
- Ata.(StateSet.intersect status3.NodeStatus.node.sat
- (get_selecting_states auto))));
- unstable_self
+ if status2.NodeStatus.node.todo != StateSet.empty then
+ let status3 = eval_trans auto cache2 cache5 tag fcs1 nss1 ps status2 in
+ if status3 != status2 then status.(node_id) <- status3