Case split policy may be too aggressive

[bclement-ocp]

As observed in #1004, there are issues with the BV theory where once we have split enough to determine the exact value of a bit-vector, we find a contradiction. But we do so because the problem is unsat, and since the propagators are complete (should be, at least) on ground inputs, we end up doing an expensive exhaustive search in look_for_sat, which times out quickly.

Possible solutions:

• Case-splitting directly in the SAT solver #901 (might be worth looking at using Case-splitting directly in the SAT solver #901 only for BV in a first time and migrating the other theories in a second step)
• use different split policies for different theories
• tweak the use of --case-split-policy after-theory-propagate (only split every N propagations?)