debug (lazy("Number of actives : " ^ (string_of_int (List.length (fst actives)))));
noprint (lazy (pp_clauses actives passives));
debug (lazy("Number of actives : " ^ (string_of_int (List.length (fst actives)))));
noprint (lazy (pp_clauses actives passives));
| bag,Some (current,actives) ->
debug (lazy ("simplified to " ^ (Pp.pp_unit_clause current)));
| bag,Some (current,actives) ->
debug (lazy ("simplified to " ^ (Pp.pp_unit_clause current)));
let bag, maxvar, actives, new_clauses =
Sup.infer_right bag maxvar current actives
in
let bag, maxvar, actives, new_clauses =
Sup.infer_right bag maxvar current actives
in
in
(* we work both on the original goal and the demodulated one*)
let acc = check_and_infer ~no_demod:false iterno acc current
in
(* we work both on the original goal and the demodulated one*)
let acc = check_and_infer ~no_demod:false iterno acc current