It may well be that for some worst case instances of SAT/SMT that there is no parallel algorithm to solve them faster than a sequential algorithm unless P==NP.

But most people who are not complexity theorists (or perhaps cryptographers) are not generally interested in worst case instances, but are instead interested in solving practical problems which are often not (or even-- are practically never) worst case instances.

My own experience w/ real SMT problems is that I can usually home-brew a fair amount of parallelism by fixing some variables and then solving the derived problems w/ Z3 on each core. But the result often has fairly poor load distribution (e.g. some threads finish long before others), so it could obviously be done better by software the changes the variable its parallel on and how it distributes those variables adaptively as it goes.