We present a new SMT-based model checking algorithm for verifying STL properties of cyber-physical systems. The algorithm reduces the STL bounded model checking problem to the satisfiability of a first-order logic formula over reals, which can be solved using state-of-the-art SMT solvers. Our modular translation method allows an efficient STL model checking algorithm that is refutationally complete for bounded signals, and that is much more scalable than the previous refutationally complete algorithm. We have implemented the algorithm using Yices2 as the underlying SMT solver. We compare the performance of our algorithm and other methods for STL model checking, STL satisfiability checking, and reachability analysis. Our algorithm outperforms other methods in most cases.