SAT modulo theory solvers are SAT solvers that, in addition to the Booleans, are able to reason over integers, real numbers, and the like. Such solvers are nowdays used in numerous applications, for example, in the static analysis of computer software. Yaga is a new, prototypical SMT solver, which is is developed at Charles University. The goal of this topic will be to design and implement new algorithms for this solver, for example, improved heuristics for finding variable instantiations, or improved algorithms for non-linear arithmetic.