We can easily create a SAT solver that is guaranteed to halt with "SAT" or "Unsat", by simply enumerating all possible solutions. Afaik, SOTA SAT solvers like kissat always halt, though in the worst case it might take exponential time.
However, for SMT solvers for real-valued problems, or unbounded integer problems, the solution space is infinite, so this guarantee is non-trivial.
My understanding is that researchers try to find restrictions of SMT problems that are decidable. Is there an overview of such decidable SMT problems and their complexity class?
