simplifyDB clears all watches. Then subsumeAll tries to purge all subsumable clauses by calling removeWatch on them. Since, however, these clauses lost the registered watch literals, markClause called in removeWatch has to overrun.
fix
by stopping reset all watches. It might be a shortcut as I coded. But it's a wrong logic.
reason
simplifyDBclears allwatches. ThensubsumeAlltries to purge all subsumable clauses by callingremoveWatchon them. Since, however, these clauses lost the registered watch literals,markClausecalled inremoveWatchhas to overrun.fix
by stopping
resetall watches. It might be a shortcut as I coded. But it's a wrong logic.