SMT solvers form critical infrastructure for many verification and program analysis systems. Recent fuzzing efforts since 2019 have significantly improved solver robustness, yet these approaches often fall short of systematically probing the diverse semantic subspaces within a formula’s satisfiability domain. This paper introduces subspace diversification, which systematically partitions the solution space of seed formulas to guide solvers into exploring different behavioral regions. We instantiate the idea using three general, bounded, and efficient mutation strategies that confine the space with cubes, numerical domains, and quantifiers. An extensive evaluation on Z3 and CVC4 demonstrates the effectiveness of our implementation, Canary, which uncovered 108 confirmed bugs across multiple theories and bug types.