STLmc is a bounded model checker for signal temporal logic (STL) of hybrid systems. The algorithm of the tool is refutationally complete for STL properties of bounded signals. It reduces bounded STL model checking problems into the satisfiability of a first-order logic formula over the reals. The satisfiability of the formula can be determined using SMT solvers (Z3, Yices2, or dReal3). STLmc supports an input modelling language to describe hybrid automata and STL properties. The tool searches for counterexample trajectories that falsify the given STL formulas and if counterexamples exist, the tool generates counterexample graphs.