Fixed: Reground() missed inconsistency after G.
When new clauses made the setup inconistent (add_result == Setup::kInconsistent), this result could be lost after the re-adding of relevant clauses in case p.relevant.filter == true. This is fixed now: Reground() terminates if add_result is Setup::kInconsistent after adding newly grounded clauses. The wrong add_result was a problem because it is passed to Grounder::AddClause() and returned there, and then used by Solver::Split() and Solver::Fix() to decide further actions.
Loading
Please register or sign in to comment