let check_exceeding (candidates: candidates) : unit =
  if not (candidates.cd_unprocessed_size = 0) then
    failwith "Selection_split.check_exceeding";

  (* enter exceeding checking mode *)
  candidates.cd_check_exceeding <- true;

  (* recompute for each context literal all candidates in chronological order *)
  begin
    try
      Context.iter
        (fun element ->
           if is_marked_exceeding candidates element then
             Problem_literals.compute_for_element candidates.cd_problem_literals element Context_unifier.Split;
        )
        candidates.cd_context;

      (* build all unprocessed exceeding candidates *)
      build_unprocessed ~force:true candidates;
    with
      | EXCEEDING_EXHAUSTED ->
          ()
  end;

  (* unprocessed candidates might be in an inconsistent state due to EXCEEDING_EXHAUSTED.
     as it can only contain recomputed candidates, it can be savely emptied. *)
  clear_unprocessed candidates;

  (* leave exceeding checking mode *)
  candidates.cd_check_exceeding <- false