niklasso/minisat — Issue #3: assertion is hit in SimpSolver::relocAll
Author: vkhomenko
Created: 2011-11-11 20:27:17+00:00
State: open

Consider the following sequence of calls:

SimpSolver::eliminate calls
Solver::simplify, which calls
Solver::removeSatisfied (which eliminates many clauses, as the solver is used incrementally, and those clauses were deleted) and then
Solver::checkGarbage, which decides to relocate memory and calls (virtually)
SimpSolver::garbageCollect which calls
SimpSolver::relocAll

Now, the following assertion in SimpSolver::relocAll is hit:

assert(subsumption_queue.size() == 0);

(because some clauses were incrementally added, and
SimpSolver::addClause_ inserts things into subsumption_queue).

Note that this scenario might be difficult to reproduce, as Solver::checkGarbage rarely calls garbageCollect, and when it does, it's usually deep in the search rather than optimisation.