Most current technical systems (e.g., robots, trains, cars) heavily depend on computational elements in the form of computer chips and software, forming so-called cyber-physical systems. Physical systems are usually modeled in a continuous way (i.e., using real numbers) while computational systems are modeled in a discrete way (e.g., using Boolean values). Both need to be combined for the realistic modeling of cyber-physical systems, and there is an urgent need for solvers that can automatically analyze and reason about such models. Ariadne is a library that supports such reasoning about models of cyber-physical systems, for example, by computing the set of reachable state. However, while it implements state-of-the-art techniques for analyzing continuous aspects of such models, it is only able to handle discrete aspects of moderate size. The goal of this topic is to do away with this short-coming by integrating Ariadne into a so-called SAT modulo theory solver. Such solvers allow reasoning about discrete (more concretely, Boolean) models of huge size, and the resulting integration will hence be able to handle combined continuous-discrete models of a size relevant for industrial practice.