let create_space ?(register: bool = true) (space_registry: space_registry)
  (problem_literals: problem_literals)
  (clause: clause)
  (process_close_candidate: raw_context_unifier -> unit)
  (process_assert_candidate: raw_context_unifier -> bool)
  (process_split_candidate: raw_context_unifier -> unit)
  (is_element_incomplete_assert: Context.element -> bool)
  (is_element_incomplete_split: Context.element -> bool)
  (is_lemma: bool)
  : context_unifier_space =
  match clause with
    | [] ->
        (* empty clause, i.e. unsatisfiable clause set,
           should be caught when the clause is added to the system. *)
        failwith "Context_unifier_space.create"

    | _ ->
        create_space' ~register:register space_registry problem_literals
          process_close_candidate process_assert_candidate process_split_candidate
          is_element_incomplete_assert is_element_incomplete_split
          clause is_lemma