let unify_constraints ~(recompute: bool) (constraints : ((literal * int) * (literal * int)) list) : subst =
  let unify_terms =
    if recompute then
      Unification_RPreserving.unify_terms
    else
      Unification_Preserving.unify_terms
  in
    List.fold_left
      (fun subst ((literal1, offset1), (literal2, offset2)) ->
         unify_terms
           subst
           literal1.Term.atom offset1
           literal2.Term.atom offset2
      )
      Subst.empty
      constraints