let add ~(no_duplicates: bool) (selection_lookahead: selection_lookahead)
  (literal: literal) (raw_context_unifier: raw_context_unifier) : unit =

  if not (is_full selection_lookahead) then begin
    let literal =
      Term.insert_literal literal
    in
    let index =
      selection_lookahead.sl_candidates#find literal
    in
      (* we could also do a p-preserving subsumption test,
         but that's too expensive. *)
      index#add ~no_duplicates:no_duplicates literal.Term.atom raw_context_unifier;
      selection_lookahead.sl_size <- selection_lookahead.sl_size + 1;
    end