Microsoft Research’s SMT solver. Decides satisfiability of formulas over combined theories (linear arithmetic, arrays, bitvectors, uninterpreted functions, …) using DPLL(T). The workhorse behind Dafny, Boogie, Verus, Lean, and many others.
Key facts
Built on DPLL(T) — SAT search interleaved with theory propagation.
Decidable fragments: QF_LIA, QF_BV, QF_UF, arrays; quantifier handling via E-matching/MBQI.
Returns sat / unsat / unknown; sat comes with a model.