SMT is exhaustively searching in the S (SAT), not necessarily in the MT (theory).
Let's dig a little deeper into what an SMT solver actually is: SAT-modulo-theories. That means, it can solve boolean formulas, but instead of just containing boolean variables, there are logical predicates over some theory (e.g. the reals with $\le$ and some operations).
So an SMT solver contains two parts: a SAT solver and a theory solver. It's the SAT solver that is working exhaustively. The theory solvers work in a number of ways, depending on which theory you're using.
To solve an SMT formula, the solver takes each logical statement in the theory and replaces it with a boolean variable, giving a pure SAT problem. It passes that off to the SAT solver, and either gets UNSAT in which case there's no solution regardless of the theory, or it gets a T/F assignment for each variable.
Then, we make a single statement in the theory that is the conjunction of all of the statements that were given True in the above step, and the negation of all the ones that were False in the above step, pass it off to the theory solver, and see if it can find values for the variables that satisfy the statement. Critically, there is no disjunction in the statement: it's not an arbitrary logical formula, it's just a sequence of formulas in the theory.
Then, the theory solver either gives SAT or UNSAT. If it gives SAT, you win, you've found a satisfying assignment. If it gives UNSAT, then you've learned something new: that particular combination of predicates is not possible in the theory. So you take the boolean version of your formula, negate it, and add that to your problem, since you've learned something from your theory.
You repeat until either you get boolean UNSAT or the theory solver gives you SAT.
So SMT is just a way to take a theory solver that can't handle disjunctions and turning it into one that can. Things get more complicated with advanced features like datatypes, quantifiers, etc. But that's the basic idea.
The theory solver isn't searching exhaustively. For reals it's probably doing simplex or something similar. But it is classical, in the sense that we assume every statement in the theory is either true or false. That said, as @MevenLennon-Bertrand says in the comments, it is still complete: if there is a solution, it will find it. It's just not finding it by checking one by one.