  First-order logic fragments mixing quantifiers, arithmetic, and uninterpreted
predicates are often undecidable, as is, for instance, Presburger arithmetic
extended with a single uninterpreted unary predicate. In the SMT world,
difference logic is a quite popular fragment of linear arithmetic which is less
expressive than Presburger arithmetic. Difference logic on integers with
uninterpreted unary predicates is known to be decidable, even in the presence
of quantifiers. We here show that (quantified) difference logic on real numbers
with a single uninterpreted unary predicate is undecidable, quite surprisingly.
Moreover, we prove that difference logic on integers, together with order on
reals, combined with uninterpreted unary predicates, remains decidable.
