Satisfiability modulo theories

Solvers: z3, cvc5, Alt-Ergo

Nonlinear real arithmetic is decidable, proved by Tarski