  We show that (local) confluence of terminating locally constrained rewrite
systems is undecidable, even when the underlying theory is decidable. Several
confluence criteria for logically constrained rewrite systems are known. These
were obtained by replaying existing proofs for plain term rewrite systems in a
constrained setting, involving a non-trivial effort. We present a simple
transformation from logically constrained rewrite systems to term rewrite
systems such that critical pairs of the latter correspond to constrained
critical pairs of the former. The usefulness of the transformation is
illustrated by lifting the advanced confluence results based on (almost)
development closed critical pairs as well as on parallel critical pairs to the
constrained setting.
