let select (candidates: candidates) : selected option =
  (* build all unprocessed candidates *)
  ignore (build_unprocessed ~force:true candidates : bool);
  
  let candidate =
    match candidates.cd_preselected with
      | Some _ as conflicting ->
          (* if there a is lookahead closing candidate, chose it *)
          candidates.cd_preselected <- None;
          conflicting
          
      | None ->
          get_best_candidate candidates
  in
    match candidate with
      | None ->
          (* all candidates processed,
             so all lookahead candidates must be subsumed by the context by now and can be dropped. *)
          candidates.cd_lookahead <- Selection_lookahead.create Const.max_assert_lookahead;
          None
            
      | Some (candidate, assert_literal, index) ->
          (* added candidates are just forgotten.
             as they are added eagerly in the choice point of their creation
             they are removed on backtracking anyway. *)

          let assert_literal =
            Term.insert_literal assert_literal
          in
          let context_literals =
            Context_unifier.get_context_literals
              candidate.ca_raw_context_unifier.Context_unifier.rcu_context_partners
          in
          let context_unifier =
            Context_unifier.recompute_full_unifier ~recompute:false candidate.ca_raw_context_unifier
          in
            State.apply_propagation
              candidates.cd_state
              assert_literal
              context_unifier
              candidate.ca_raw_context_unifier.Context_unifier.rcu_space.Context_unifier.cus_clause
              candidate.ca_raw_context_unifier.Context_unifier.rcu_space.Context_unifier.cus_vars
              index
              (Context_unifier.create_space_utility_inc candidate.ca_raw_context_unifier.Context_unifier.rcu_space)
              context_literals;
            
            Some {
              Selection_types.candidate_type = State.Propagation;
              Selection_types.literal = assert_literal;
              Selection_types.raw_context_unifier = candidate.ca_raw_context_unifier;
            }