let apply_split_right (state: state) (literal: literal) (context_unifier: subst)
    (clause: clause) (clause_vars: Subst.var list) (clause_index: int) (clause_value: unit -> unit)
    (context_literals: literal array)
    : unit =
  let active =
    active_choice_point state
  in
  let literal_info =
    create_literal_info literal SplitRight active
      context_unifier clause clause_vars context_literals clause_index clause_value None
  in
    active.cp_right_splits <- literal :: active.cp_right_splits;
    LiteralTable.add state.st_literal_info literal literal_info