The answer to that question is, "Yes, if your SMT solver has strategies that provide good results for the problem in question." Unless you're implementing solv

The answer to that question is, "Yes, if your SMT solver has strategies that provide good results for the problem in question." Unless you're implementing solvers or caught up on the particulars of a solver's implementation, the best way to gauge this is to try it.