Case split on booleans

[bclement-ocp]

Alt-Ergo currently does not perform case splits on boolean values nested inside ADTs or records:

$ cat tests/issues/1014.smt2 
(set-logic ALL)
(declare-datatype Data ((cell (value Bool))))
(declare-const x Data)
(declare-const y Data)
(declare-const z Data)
(assert (distinct x y z))
(check-sat)

$ dune exec -- alt-ergo tests/issues/1014.smt2 
                                       
; File "tests/issues/1014.smt2", line 7, characters 1-12: I don't know (0.0005) (6 steps) (goal g_1)

unknown

Initially reported as an ADT bug in #1014, but it turns out to not be an ADT bug — instead, nobody performs case splits for booleans. It is not clear at the moment where we want to do it, but it probably should be the SAT solver since it is where we deal with the boolean theory.