let check_assert
  (config: config)
  (bound: bound)
  (context: Context.context)
  (subst: subst)
  (context_unifier_space: context_unifier_space)
  (context_partners: context_partners)
  (is_element_incomplete: bool) :
  raw_context_unifier option =
  
  (* is the assert literal parameter free? *)
  let is_assert_valid_at (i : int) : bool =
    let assert_vars =
      Subst.get_bound_vars
        subst
        context_unifier_space.Context_unifier.cus_input_partners.(i).Context_unifier.ip_vars
    in
      List.for_all 
        (fun var ->
           Var.is_universal var.Subst.sv_var
        )
        assert_vars
  in
  
  (* has the unifier an empty remainder
     and leaves the assert literal parameter free?
     returns also the index of the assert literal. *)
  (* precheck in context_unifier_check assures that
     check_close is only called with an empty remainder,
     so check only that assert literal instance is universal. *)
  let rec is_valid_at (i: int) (assert_index: int option) : bool * int option =
    if i >= Array.length context_partners then begin
(*      not (Context_unifier.is_remainder' subst), assert_index*)
(*      true, assert_index*)
      failwith "Context_unifier_check.is_valid_at: no assert literal"
    end

    else begin
      let input_index =
        context_unifier_space.Context_unifier.cus_input_partners.(i).Context_unifier.ip_index
      in
      let context_partner =
        context_partners.(input_index)
      in
        (* no parameter in the assert literal? *)
        if context_partner.Context_unifier.cp_element == Context.assert_element then begin
          (* the is_assert_valid_at check can be really expensive, so we want to avoid it if possible *)
          if
            (* parametric propagation on lemmas *)
            (
              Config.lemma_parametric_assert config > 0
              &&
              context_unifier_space.Context_unifier.cus_lemma_learned >= Config.lemma_parametric_assert config
            )
            ||
            (* if all context literals are universal the instance must be universal *)
            Context.is_universal context
            ||
            (* if all used context literals are universal the instance must be universal *)
            (Tools.array_for_all (fun cp -> cp.Context_unifier.cp_element.Context.el_pars == []) context_partners)
            ||
            (* ok, we have to do the expensive (yes, it is) check *)
            is_assert_valid_at i
          then
            (*is_valid_at (i + 1) (Some i)*)
            true, Some i
          else begin
            false, assert_index
          end
        end

        (* empty remainder? *)
        else begin
            (*
          if
            Context_unifier.is_remainder 
              subst
              context_partner.Context_unifier.cp_element(*.Context.el_pars*)
              input_index
          then begin
            false, assert_index
          end
        
          (* yes, so continue *)
          else*)
            is_valid_at (i + 1) assert_index
        end
    end
  in
(*    if (not (Config.is_horn config)) && Context_unifier.is_remainder' subst then
      None

    else*)
    match is_valid_at 0 None with
      | false, _ ->
          None

      | true, None ->
          failwith "Context_unifier_check.check_assert"

      | true, Some assert_index ->
          let assert_clause_literal =
            context_unifier_space.Context_unifier.cus_input_partners.(assert_index).Context_unifier.ip_literal
          in
            (* this should be filtered in context_unifier_searach *)
            if
              Const.debug
              &&
              (Config.neg_assert_candidates config = Flags.NAC_Ignore)
              &&
              (not assert_clause_literal.Term.sign)
            then begin
              failwith "Context_unifier_check.check_assert: neg_assert";
            end;

            (* - within bound -> keep
               - exceeding bound and not delayed restarting -> register
               - exceeding bound and delayed restarting -> keep
               - exceeding bound and lookahead -> keep
               - otherwise: drop
            *)
            let complexity =
              bound#get_complexity_subst
                assert_clause_literal
                subst
                Subst.input_literal_offset
            in
            let keep, exceeding =
              (* exceeding bound *)
              if bound#exceeds complexity then begin
                (* exceeding bound, horn, positive, not delayed restarting -> register *)
                if Config.is_horn config && assert_clause_literal.Term.sign then begin
                  match Config.restart config with
                    | Flags.RS_Eager
                    | Flags.RS_Lazy ->
                        ignore (bound#register complexity
                                (Context_unifier.get_creation_choice_point context_partners)
                                : bool);
                    | Flags.RS_Delayed ->
                        ()
                end;
                
                (* this context element is already incomplete,
                   so all its context unifiers will be recomputed anyway if needed. *)
                if is_element_incomplete then
                  false, true

                (* keep for Delayed *)
                else if Config.restart config = Flags.RS_Delayed then
                  true, true

                (* keep for exceeding lookeahead *)
                else if Config.lookahead_exceeding config then
                  true, true

                (* otherwise drop for the time being *)
                else
                  false, true
              end

              (* within bound -> keep *)
              else
                true, false
            in
              if keep then
                (* this candidate is obeying the bound
                   or needed for the lookahead check *)
                let raw_context_unifier = 
                  Context_unifier.create_context_unifier
                    context_unifier_space
                    (Array.copy context_partners)
                    exceeding
                in
                  Some raw_context_unifier
              else
                None