Linear Temporal Logic (LTL) is the most common specification language for the verification of systems, with many efficient reasoning tools developed in the last decades. However, the propositional nature of LTL limits its applicability to finite-state systems, whereas more complex scenarios, whose dynamics depend on unbounded data or on complex relations between data elements, lead naturally to infinite-state formulations. For this reason, we recently introduced LTL Modulo Theories (LTLMT), a first-order extension of LTL that replaces propositions with first-order formulas interpreted over arbitrary theories, similarly to how Satisfiability Modulo Theories (SMT) extends the classical Boolean satisfiability problem. In contrast to other first-order extensions of LTL, LTLMT has been designed to be efficiently handled in practice by encoding it to SMT problems delivered to state-of-the-art SMT solvers. LTLMT reasoning procedures have been implemented in BLACK, a recently developed temporal reasoning tool for LTL and related logics, with promising results. The talk will overview LTLMT, its reasoning techniques, and the architecture and usage of the BLACK reasoner.