I've only seriously examined the source of Z3, but encoding an SMT problem to multiple SAT instances remains a feature there - just convert any qf_bv problem into bit width * SAT instances / 2!

I recall that many popular simplifications required a problem to be expressible as CNF.

(I also seem to recall there is some strategy to simplify logics over Reals/Ints into BV without encoding logical "bignum circuitry" as well?)