  Timed Automata (TA) are a very popular modeling formalism for systems with
time-sensitive properties. A common task is to verify if a network of TA
satisfies a given property, usually expressed in Linear Temporal Logic (LTL),
or in a subset of Timed Computation Tree Logic (TCTL). In this paper, we build
upon the TACK bounded model checker for TA, which supports a signal-based
semantics of TA and the richer Metric Interval Temporal Logic (MITL). TACK
encodes both the TA network and property into a variant of LTL, Constraint LTL
over clocks (CLTLoc). The produced CLTLoc formula can then be solved by tools
such as Zot, which transforms CLTLoc properties into the input logics of
Satisfiability Modulo Theories (SMT) solvers. We present a novel method that
preserves TACK's encoding of MITL properties while encoding the TA network
directly into the SMT solver language, making use of both the BitVector logic
and the logic of real arithmetics. We also introduce several optimizations that
allow us to significantly outperform the CLTLoc encoding in many practical
scenarios.
