The semantic splitting functionality introduced in #1027 is currently unused due to regressions in the arithmetic theory. Some of the problems it solves (notably the ability to have more communication between the splits and the CDCL solver) are expected to be helpful for the bit-vector theory, as discussed in #1027.
We should be using --enable-sat-cs (possibly with a few tweaks) for bit-vectors, and consider making it the default.
The semantic splitting functionality introduced in #1027 is currently unused due to regressions in the arithmetic theory. Some of the problems it solves (notably the ability to have more communication between the splits and the CDCL solver) are expected to be helpful for the bit-vector theory, as discussed in #1027.
We should be using
--enable-sat-cs(possibly with a few tweaks) for bit-vectors, and consider making it the default.