Strategy for different types of SMT problems

[huhuhu777]

What is the basis for selecting a solution strategy for different types of SMT problems? For example, what SMT problems use the SAT solver?

[NikolajBjorner]

It checks the "set-logic" configuration and checks the formula itself.
If the formula can be converted to SAT, such as though bitblasting, it uses the SAT backend.