Reasoning about remainders

As part of exploring CSE in Kontrol, a few issues have come up. Specifically:

1. The backend exhibits spurious branching because it's not able to prove a large remainder (11 branches) UNSAT. An initial investigation with @geo2a revealed that the satisfiability of the remainder is not checked with respect to the current path constraint. The corresponding bug report is attached: it exhibits a 9-way branching when only an 8-way branching is expected).
2. The remainders are not minimised, in the sense that even though some branches have been cut as infeasible, we still get the negation of their constraints in the remainder (in the example, the branching is initially 11-way and then three branches are discarded).
3. The remainder is not propagated back using rule_predicate, which leads to a mischaracterisation of the branching by pyk, and causes an infinite loop in combination with 1).

From what I understand, the remainders are initially of the form #Not ( ... #Or ... ), which is then transformed into #Not (...) #And #Not (...). I believe that there is room for further simplification or minimisation at the #Or stage, perhaps even Z3 could be asked to minimise this before the transformation to #And.

nine-way-branch.tar.gz

Start by reproducing the behavior from the attached nine-way-branch.tar.gz in Kontrol and inspect how the backend checks remainders against the current path constraint. Trace the #Or-to-#And transformation and rule_predicate propagation, then verify that infeasible branches are minimized, branching is correctly characterized by pyk, and the infinite loop is eliminated.