let recompute_unifier ~(recompute: bool) (raw_context_unifier: raw_context_unifier) : subst =

  let rec recompute_at (i: int) (acc: subst) : subst =
    if i >= Array.length raw_context_unifier.rcu_space.cus_input_partners then
      acc

    else
      let input_partner =
        raw_context_unifier.rcu_space.cus_input_partners.(i)
      in
      let input_index =
        input_partner.ip_index
      in
      let context_partner =
        raw_context_unifier.rcu_context_partners.(input_index)
      in
      let extended_unifier =
        try
          extend_partial_context_unifier ~recompute:recompute ~p_preserving:false
            acc input_partner context_partner
        with
          | Unification.UNIFICATION_FAIL ->
              print_endline (Subst.subst_to_string acc);
              print_endline (Term.literal_to_string input_partner.ip_literal);
              print_endline (Term.literal_to_string context_partner.cp_element.Context.el_literal);
              print_endline (raw_context_unifier_to_string raw_context_unifier);
              failwith "Context_unifier.recompute_unifier"
      in
        recompute_at (i + 1) extended_unifier
          
  in
    recompute_at 0 Subst.empty