symbols yields an interesting modeling language. However, satisfiability of

such formulas is undecidable, even if we restrict the uninterpreted predicate

symbols to arity one. In order to find decidable fragments of this language, it

is necessary to restrict the expressiveness of the arithmetic part. One

possible path is to confine arithmetic expressions to difference constraints of

the form $x -- y \\mathrel{\\#} c$, where $\\#$ ranges over the standard relations

$<, \\leq, =, \\neq, \\geq, >$ and $x,y$ are universally quantified. However, it

is known that combining difference constraints with uninterpreted predicate

symbols yields an undecidable satisfiability problem again. In this paper, it

is shown that satisfiability becomes decidable if we in addition bound the

ranges of universally quantified variables. As bounded intervals over the reals

still comprise infinitely many values, a trivial instantiation procedure is not

sufficient to solve the problem.

},\n}\n'