Interpolation Support for Yaga SMT Solver

We extend the Yaga SMT solver with support for Craig interpolation. Yaga is an SMT solver based on the Model-Constructing Satisfiability Calculus, which integrates theory reasoning directly into the search process. While Yaga already supports satisfi- ability checking for quantifier-free linear real arithmetic and uninterpreted functions, it currently lacks interpolation capabilities required by modern verification workflows. In this thesis, we implement model-based interpolation in Yaga, following an interpolation- modulo-models approach that does not rely on clausal proofs. The implementation in- cludes modifications to Yaga's parsing, control flow, as well as its core components. We evaluate the implementation on SMT-LIB benchmarks, where we validate the correctness of generated interpolants and compare performance with existing SMT solvers.