In the past several years, syntax-guided synthesis (SyGuS) solvers have made significant progress as efficient backend reasoners in several applications. One approach for syntax-guided synthesis, as implemented in the SMT solver CVC4, has shown that SMT solvers can act as efficient stand-alone tools for synthesis. This talk focuses on a new enumerative approach for invariant synthesis in the SMT solver CVC4. We describe a divide-and-conquer approach that makes use of an evolving set of refinement lemmas that constrain concrete points of the invariant-to-synthesize. We show its applicability to synthesis in multiple SMT domains, including for synthesizing invariants that involve non-linear arithmetic.