SMT solvers enable the automated verification of complex software, but they frequently also cause performance problems, proof brittleness, and spurious errors. Debugging such issues is challenging because it is difficult to understand and predict how the solver’s complex algorithms and heuristics will interact with a given query. We present SmtScope, a tool for the automatic analysis and visualisation of z3 executions. It helps detect and explain issues in SMT queries, such as indefinite chains of quantifier instantiations (matching loops), and proliferation of quantifier instantiations. Additionally, it provides a useful interface for other tools. Compared to the existing Axiom Profiler, SmtScope offers more effective analyses, novel visualisations of matching loops and proof search, as well as more efficient algorithms, which allow SmtScope to scale to large SMT traces. Our evaluation shows that SmtScope can identify problem behaviours in real-world traces, finding hundreds of unique issues in four state-of-the-art verifiers.