let unify_constraints' ~(recompute: bool) (constraints : ((literal * int) * (literal * int)) list) : Subst.hash_subst =
  let unifier =
    Subst.VarTable.create 1024
  in
  let unify_terms =
    if recompute then
      Unification_RPreserving.unify_terms Subst.empty
    else
      Unification_Preserving.unify_terms Subst.empty
  in

  let rec unify' to_unify =
    match to_unify with
      | [] ->
          ()

      | binding :: tail ->
          (* orientation avoids cycles *)
          let binding =
            Subst.orient binding
          in
          begin
            try
              let bound_term =
                Subst.VarTable.find unifier binding.Subst.sb_var
              in
              (* dereference *)
              let bind_term = Subst.dereference' unifier binding.Subst.sb_term
              and bound_term = Subst.dereference' unifier bound_term
              in
              let unifier' =
                unify_terms
                  bound_term.Subst.st_term bound_term.Subst.st_offset
                  bind_term.Subst.st_term bind_term.Subst.st_offset
              in
                unify' unifier';
            with
              | Not_found ->
                  (* var still unbound, so just add binding *)
                  Subst.VarTable.add unifier binding.Subst.sb_var binding.Subst.sb_term;
          end;
          unify' tail                
  in
    (* unify the constraints *)
    List.iter
      (fun ((literal1, offset1), (literal2, offset2)) ->
         let t1 = Subst.dereference' unifier (Subst.make_term literal1.Term.atom offset1)
         and t2 = Subst.dereference' unifier (Subst.make_term literal2.Term.atom offset2)
         in
         let unifier' =
           unify_terms
             t1.Subst.st_term t1.Subst.st_offset
             t2.Subst.st_term t2.Subst.st_offset
         in
           (* integrate the unifiers into the common unifier *)
           unify' unifier'
      )
      constraints;

    unifier