complexity, DPLL(T), Isabelle/HOL2, lattice basis reduction, Linear Rational Arithmetic, theory solver, unsatisfiable core.
