let backtrack (candidates: candidates) (retracted: choice_point) (explanation: literal list) : unit =
  let explanation =
    Array.of_list (
    Tools.list_remove_first
      (fun literal -> Term.literal_equal literal (State.left_split_literal retracted))
      explanation
    )
  in
  (* unprocessed and valid candidates are not backtracked,
     retracted ones are dropped when build *)
  backtrack_invalid candidates;

  backtrack_right_splits candidates;

  (* backtrack applied splits, store the retracted one as a right split
     -> backtrack_right_splits must be done before. *)
  backtrack_added candidates retracted explanation;

  (* assure that the right split of the currently retracted split has been found. *)
  if Const.debug then begin
    match candidates.cd_right_splits with
      | [] ->
          failwith "Selection_split.backtrack: no right split found"
            
      | _ ->
          ()
  end;

  backtrack_exceeding candidates;