Software Model Checking is emerging as one of the leading approaches to automatic program analysis. State-of-the-art software model checkers exhibit levels of automation and precision often superior to those provided by traditional software analysis tools. This success is due to a large extent to the use of Satis ability Modulo Theory (SMT) solvers to support reasoning about complex and even in nite data structures (e.g. bit-vectors, numeric data, arrays) manipulated by the program being analysed. In this talk I will survey the opportunities and challenges posed to Automated Reasoning by this new application domain.