let apply_split_left (state: state) (literal: literal) (context_unifier: subst)
    (clause: clause) (clause_vars: Subst.var list) (clause_index: int) (clause_value: unit -> unit)    
    : choice_point =

  let id =
    try
      Counter.next state.st_id
    with
      | Counter.OVERFLOW ->
          raise (Const.NO_SOLUTION "State.apply_split_left: state id overflow")
  in
  let new_choice_point = {
    cp_id = id;
    cp_split_literal = literal;
    cp_right_splits = [];
    cp_valid = true;
  }
  in

  let branch_node =
    create_literal_info literal SplitLeft new_choice_point
      context_unifier clause clause_vars [| |] clause_index clause_value (Some ([new_choice_point]))
  in
    LiteralTable.add state.st_literal_info literal branch_node;

    (* extend the branch *)
    state.st_branch <- new_choice_point :: state.st_branch;
    new_choice_point