let get_lemma ~(uip: bool) (state: state) (context: context) (context_unifier: subst)
  (clause: clause) (conflict_literals: literal array) (regress_stop: choice_point) : clause option =
  (* fake data to get the regression with the closing clause started *)
  let closing_info =
    State.create_literal_info Lemma.close_literal State.Propagation
      (State.active_choice_point state) context_unifier
      clause [] conflict_literals (-1) (fun () -> ())
      (* must just have some dependency to not be taken as a root assert *)
      (Some [regress_stop])
  in
  let regression_start = {
    tr_context_literal = Lemma.close_literal;
    (* pseudo-context literal: most recent context element *)
    tr_context_literal_id = Pervasives.max_int;
    tr_context_literal_instance = Lemma.close_literal;
    tr_regress_info = closing_info;
  }
  in

  (* do the regression *)
  let regressed =
    regress ~uip:uip
      state context regress_stop
      (To_regress.add regression_start To_regress.empty)
  in

  let unground =
    generalize regressed
  in
  let simplified =
    Term.remove_duplicates (Lemma.simplify unground)
  in

  let normalized =
    Term.sort_clause simplified
  in
    (* needed to avoid learning right splits as real lemmas *)
    match clause, normalized with
      | unit_clause :: [], unit_lemma :: [] when
          Unification.is_literal_instance unit_lemma unit_clause ->
          None
            
      | _ ->
          (* normalize variables. *)
          Some (Subst.apply_to_clause Subst.empty normalized 0)