let select (selection: selection) : selected =

  (* first assert candidates leading immediately to a closing unifier. *)
  if Selection_assert.has_closing_candidate selection.sel_assert then begin
    match Selection_assert.select selection.sel_assert with
      | Some selected ->
          selected
            
      | None ->
          failwith "Selection.select"
  end
    
  else
  (* then unit asserts *)
          begin
            match select_unit_assert selection selection.sel_unit_asserts with
              | Some selected ->
                  selected
                    
              | None ->
                  
                  (* then standard asserts *)
                  begin
                    match Selection_assert.select selection.sel_assert with
                      | Some selected ->
                          selected
                              
                      | None ->
          
  (* then right splits *)
 begin
    match Selection_split.select_right_split selection.sel_split with
      | Some selected ->
          selected
            
      | None ->

                                  (* then left splits *)
                          
                          (* recompute deferred split candidates, if necessary *)
                          if selection.sel_no_splits_yet then begin
                            selection.sel_no_splits_yet <- false;
                            Problem_literals.compute_deferred
                              selection.sel_problem_literals Context_unifier.Split;
                          end;
                            
                          begin
                            (* still a branch to replay? *)
                            let replay =
                              match selection.sel_guiding_path with
                                | [] ->
                                    None
                                      
                                | head :: tail ->
                                    selection.sel_guiding_path <- tail;
                                    Some head
                            in
                              (* finally try to find a split literal *)
                              match Selection_split.select selection.sel_split replay with
                                | Some selected ->
                                    check_replayed_decision selected replay;
                                    selected
                                      
                                | None ->
                                    (* process kept candidates exceeding the depth limit
                                       to check if the branch is incomplete. *)
                                    if
                                      Config.is_horn selection.sel_config
                                      ||
                                      selection.sel_no_splits_yet
                                    then
                                      Selection_assert.check_exceeding selection.sel_assert
                                    else
                                      Selection_split.check_exceeding selection.sel_split;

                                    raise SATISFIABLE
                          end
                  end  
          end
  end