Abstract
The scalability of automated synthesis tools have improved dramatically in the past decade. In part, these advances have been made possible due to advances in underlying reasoning engines such as Satisfiability Modulo Theories (SMT) solvers. Recently, an alternative line of research incorporates techniques for syntax-guided synthesis (SyGuS) inside the SMT solver itself. This talk will give an overview of the SyGuS features of the SMT solver CVC4. It will describe high-level implementation details and ongoing work in this direction.