Parallelizing SMT Solvers via Dynamic Partitioning, Core-Guided Search-Space Pruning, and Online Backbone Detection