  We study an expressive model of timed pushdown automata extended with modular
and fractional clock constraints. We show that the binary reachability relation
is effectively expressible in hybrid linear arithmetic with a rational and an
integer sort. This subsumes analogous expressibility results previously known
for finite and pushdown timed automata with untimed stack. As key technical
tools, we use quantifier elimination for a fragment of hybrid linear arithmetic
and for cyclic order atoms, and a reduction to register pushdown automata over
cyclic order atoms.
