let check_exceeding (candidates: candidates) : unit =
  if Config.is_horn candidates.cd_config then begin
  if not (candidates.cd_unprocessed_size = 0) then
    failwith "Selection_assert.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.Assert;
        )
        candidates.cd_context;

      (* build all unprocessed exceeding candidates *)
      ignore (build_unprocessed ~force:true candidates: bool);
    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

  end