- unsafe_set run.sat node_id status1 status0;*)
- let fcs1 = loop_td_and_bu fc node status1 in
- if bu_todo == StateSet.empty then begin
- unsafe_set run.sat node_id status1 status0; (* write the td_states *)
- loop_td_and_bu ns node status1 (* tail call *)
- end else
- let nss1 = loop_td_and_bu ns node status1 in
- let status2 =
- eval_trans auto run.fetch_trans_cache run.bu_cache tag fcs1 nss1
- parent_sat
- status1 bu_todo summary
- in
- unsafe_set run.sat node_id status2 status0;
- status2
- end
+ unsafe_set run.sat node_id status1 status0;*)
+ let fcs1 = loop_td_and_bu fc node status1 in
+ if bu_todo == StateSet.empty then begin
+ unsafe_set run.sat node_id status1 status0; (* write the td_states *)
+ loop_td_and_bu ns node status1 (* tail call *)
+ end else
+ let nss1 = loop_td_and_bu ns node status1 in
+ let status2 =
+ eval_trans auto run.fetch_trans_cache run.bu_cache tag
+ summary fcs1
+ nss1
+ parent_sat
+ status1 bu_todo
+ in
+ unsafe_set run.sat node_id status2 status0;
+ status2
+ end