Fixed: split terms / assign literals may be empty for trivial formulas.
When the setup is empty or contains the empty or when it is assumed to be consistent and only relevant split terms are considered, the set of split terms may be empty. Then however the formula must not contain any terms and hence must be trivially valid or invalid. This is now considered in Solver::Split(), Solver::Assign().
Loading
Please register or sign in to comment