Fixed: inconsistency check in Setup::AddClause() was incomplete
* The guard incons_[incons.size() - 1] made no sense because inconsistency may have been detected at k = 1 but not yet at k = 0. * When for a grounding of a clause inconsistency has been detected at level k, all l > k are marked as inconsistent as well. Only if k = 0 the inconsistency check is done, otherwise we need to continue because a subsequent grounding may prove inconsistency for l < k. The former case is now handled by `if (k == 0) return', the latter case gets no special treatment because the subsequent iterations test for incons_[k].
Loading
Please register or sign in to comment