#3 Theory Solvers Must Eagerly Detect Conflicts

[Jim Grundy]

Current assertions in the code formalize an assumption that the decision level of the SAT solver and the theory solvers move in lock-step. This can be violated in the case of theory solvers that do not detect conflict eagerly (are able to perform inference to detect conflicts when literals are set).

Subsequent releases of DPT will support lazy conflict detection in theory solvers.