+
+ and kont_pure_td summary tag parent_sat status0 status1 fc ns node node_id =
+ unsafe_set run_sat node_id status1 status0; (* write the td_states *)
+ update_res false status1 node;
+ if fc != Tree.nil then ignore (loop_td fc node status1);
+ if ns == Tree.nil then StateSet.empty else loop_td ns node status1 (* tail call *)
+ and kont_td_and_bu summary tag parent_sat status0 status1 fc ns node node_id =
+ let fcs1 = if fc == Tree.nil then StateSet.empty else loop_td_and_bu fc node status1 in
+ let nss1 = if ns == Tree.nil then StateSet.empty else loop_td_and_bu ns node status1 in
+ let status2 =
+ eval_trans run run.bu_cache tag
+ summary fcs1
+ nss1
+ parent_sat
+ status1 bu_todo
+ in
+ unsafe_set run_sat node_id status2 status0;
+ status2
+ and kont_td_and_bu_last summary tag parent_sat status0 status1 fc ns node node_id =
+ let nss1 = if ns == Tree.nil then StateSet.empty else loop_td_and_bu_last ns node status1 in
+ let fcs1 = if fc == Tree.nil then StateSet.empty else loop_td_and_bu_last fc node status1 in
+ let status2 =
+ eval_trans run run.bu_cache tag
+ summary fcs1
+ nss1
+ parent_sat
+ status1 bu_todo
+ in
+ unsafe_set run_sat node_id status2 status0;
+ if status2 != StateSet.empty then update_res true status2 node;
+ status2
+ and loop_td node parent parent_sat =
+ common node parent parent_sat kont_pure_td
+ and loop_td_and_bu node parent parent_sat =
+ common node parent parent_sat kont_td_and_bu
+ and loop_td_and_bu_last node parent parent_sat =
+ common node parent parent_sat kont_td_and_bu_last
+ in
+
+ let _ =
+ if bu_todo == StateSet.empty then
+ loop_td (Tree.root tree) Tree.nil dummy_set
+ else if last_run then
+ loop_td_and_bu_last (Tree.root tree) Tree.nil dummy_set
+ else
+ loop_td_and_bu (Tree.root tree) Tree.nil dummy_set