SMT solvers use first-order logic on top of SAT solvers with boolean logic. For example, CVC4 is an SMT solver able to accept a rich set of mixed constraints over strings, integers, reals, arrays, and algebraic datatypes.
My question is what advancements in SMT solvers have significant impacts to progress in the field of theoretical computer science? If we want to analyze the complexity of an SAT solver vs an SMT solver, is there a uniform way to deal with it? Or their components must be treated separately?
Some reference questions related between SAT/SMT solvers and TCS: