let backtrack (selection: selection) (retracted: choice_point) (explanation: literal list) : unit =
(*  decay_clause_utility selection;*)

  (* backtracking invalidates everything from the last split on,
     so in particular all asserted literals are retracted. *)

  selection.sel_best_closing := None;

  Problem_literals.backtrack selection.sel_problem_literals;

  (* partial context unifiers - dependent on Problem_literals.backtrack
     backtrack only not subsumed clauses to avoid jumping through memory.
     for lemmas this showed to be potentially expensive.
  *)
  Array.iter
    (fun space ->
       if Problem_literals.is_space_subsumed selection.sel_problem_literals space then
         ()
       else
         Context_unifier_space.backtrack space
    )
    selection.sel_clause_spaces;

  List.iter
    (fun (space, _) ->
       if Problem_literals.is_space_subsumed selection.sel_problem_literals space then
         ()
       else
         Context_unifier_space.backtrack space
    )
    selection.sel_lemma_spaces;


  (* candidates *)
  Selection_assert.backtrack selection.sel_assert;
  Selection_split.backtrack selection.sel_split retracted explanation;
  
  begin
    match Config.lemma selection.sel_config with
      | Flags.LM_Propositional ->
          Lemma_propositional.backtrack selection.sel_lemmas_propositional;

      | Flags.LM_None
      | Flags.LM_Grounded
      | Flags.LM_Lifted ->
          ()
  end