You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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 text was updated successfully, but these errors were encountered:
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 text was updated successfully, but these errors were encountered: