OpenSMT supports an experimental feature called lookahead-splitting for constructing partitions that can be solved independently to decide the satisfiability of an input instance. For the moment the feature is not yet integrated into the main branch, but instead lies in a branch called satsolver-reorg.
To experiment with the code, please fetch the opensmt repository and switch to the correct branch before compiling:
$ mkdir build; cd build; cmake ..; make
The feature can be enabled directly by setting options in the .smt2 file. For example
(set-option :split-num 4)
(set-option :split-format smt2)
(set-option :split-format-length "brief")
(set-option :output-dir "foo")