E-unification problems are central in automated deduction. In this work, we consider unification modulo theories that extend the well-known
ACI or
ACUI by adding a binary symbol

*

that distributes over the
AC(
U)
I-symbol

+.

If this distributivity is one-sided (say, to the left), we get the theory denoted
AC(
U)
IDl; we show that
AC(
U)
IDl-unification is DEXPTIME-complete. If

*

is assumed two-sided distributive over

+,

we get the theory denoted
AC(
U)
ID; we show unification modulo
AC(
U)
ID to be NEXPTIME-decidable and DEXPTIME-hard. Both
AC(
U)
IDl and
AC(
U)
ID seem to be of practical interest, for example, in the analysis of programs modeled in terms of process algebras. Our results, for the two theories considered, are obtained through two entirely different lines of reasoning. A consequence of our methods of proof is that, modulo the theory that adds to
AC(
U)
ID the assumption that

*

is associative-commutative, or just associative, unification is undecidable.
Keywords rewriting - equational unification - counter machines - Post correspondence problem - set constraints - decidability - complexity