let add (selection: selection) (context_element: Context.element) : unit =
  (* propositional lemmas does its own propagation. *)
  begin
    match Config.lemma selection.sel_config with
      | Flags.LM_Propositional ->
          Lemma_propositional.extend_context selection.sel_lemmas_propositional context_element;

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

  (* compute only assert candidates *)
  if selection.sel_no_splits_yet then
    Problem_literals.add selection.sel_problem_literals context_element Context_unifier.CloseAssert

  (* compute all candidates *)
  else
    Problem_literals.add selection.sel_problem_literals context_element Context_unifier.All;

  (* raise Close, if a closing context unifier has been found *)
  raise_close selection