Decidability of difference logics with unary predicates

We investigate the decidability of a family of logics mixing
difference-logic constraints and unary uninterpreted predicates. The focus
is set on logics whose domain of interpretation is R, but the language
has a recognizer for integer values. We first establish the decidability of
the logic allowing unary uninterpreted predicates, order constraints between
real and integer variables, and difference-logic constraints between
integer variables. Afterwards, we prove the undecidability of the logic
where unary uninterpreted predicates and difference-logic constraints between
real variables are allowed.