let add (context: context) (literal: literal) (generation: int) (is_fd_incomplete: bool)
    : element =

  (* check if context gets inconsistent *)
  if Const.debug then begin
    let index =
      context.index#find (Term.request_negated_literal literal)
    in
      match index#find_unifiable ~p_preserving:true literal.Term.atom with
        | None ->
            ()

        | Some element ->
            print_endline ("in context: " ^ Term.literal_to_string element.el_literal);
            print_endline ("add:        " ^ Term.literal_to_string literal);
            failwith ("Context.add: inconsistent: " ^ Term.literal_to_string literal);
  end;

  let pars =
    parameters_of_literal literal
  in
  begin
    match context.universal, pars with
      | None, _ :: _ ->
          (* first non-universal literal *)
          context.universal <- Some (State.active_choice_point context.state)

      | _ ->
          ()
  end;

  let id =
    try
      Counter.next context.id_counter
    with
      | Counter.OVERFLOW ->
          raise (Const.NO_SOLUTION "Context.add: context id overflow")
  in
  let new_context_element = {
    el_id = id;
    el_literal = literal;
    el_choice_point = State.active_choice_point context.state;
    el_pars = pars;
    el_generation = generation;
    el_is_fd_incomplete = is_fd_incomplete;
    el_compacted = -1;
  }
  in
  (* get the index where the literal must be inserted *)
  let index =
    context.index#find new_context_element.el_literal
  in

    compact context index new_context_element;

    (* add new literal to context and index *)
    Stack.push context.context new_context_element;
    update_max_size context;

    if Config.term_indexing context.config then begin
      index#add new_context_element.el_literal.Term.atom new_context_element
    end;

    (* all index entries correspond to the term they are stored under *)
    if Const.debug then begin
      context.index#iter
        (fun _ index ->
           index#iter
           (fun term element ->
              if not (Term.term_equal term element.el_literal.Term.atom) then begin
                print_endline ("\n\n\nFAIL=====\n");
                print_endline (index#to_string);
                print_endline ("ADD: " ^ Term.literal_to_string new_context_element.el_literal);
                print_endline ("Term             : " ^ Term.term_to_string term);
                print_endline ("But node contains: " ^ element_to_string element);
                failwith "Context.add"
              end
           )
        )
    end;
    
    new_context_element