assertion is hit in SimpSolver::relocAll

[vkhomenko]

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.

[vladrich]

I am bit by this right now. Here's a small example triggering the assertion.

#include <minisat/core/Solver.h>
#include <minisat/simp/SimpSolver.h>

using namespace std;



int main(int argc, char *argv[])
{

    Minisat::SimpSolver solver;
    solver.newVar();
    solver.newVar();
    solver.newVar();
    solver.newVar();
    solver.newVar();
    {
        Minisat::vec<Minisat::Lit> clause_1;
        Minisat::Lit a = Minisat::mkLit(2,true); 
        clause_1.push(a);
        Minisat::Lit b = Minisat::mkLit(3,true); 
        clause_1.push(b);
        Minisat::Lit c = Minisat::mkLit(4,true); 
        clause_1.push(c);
        solver.addClause(clause_1);
    }
    {
        Minisat::vec<Minisat::Lit> clause_1;
        Minisat::Lit a = Minisat::mkLit(2,true); 
        clause_1.push(a);
        Minisat::Lit b = Minisat::mkLit(3,true); 
        clause_1.push(b);
        Minisat::Lit c = Minisat::mkLit(4,false); 
        clause_1.push(c);
        solver.addClause(clause_1);
    }
    {
        Minisat::vec<Minisat::Lit> clause_1;
        Minisat::Lit a = Minisat::mkLit(2,true); 
        clause_1.push(a);
        Minisat::Lit b = Minisat::mkLit(3,false); 
        clause_1.push(b);
        Minisat::Lit c = Minisat::mkLit(4,true); 
        clause_1.push(c);
        solver.addClause(clause_1);
    }
    {
        Minisat::vec<Minisat::Lit> clause_1;
        Minisat::Lit a = Minisat::mkLit(2,true); 
        clause_1.push(a);
        Minisat::Lit b = Minisat::mkLit(3,false); 
        clause_1.push(b);
        Minisat::Lit c = Minisat::mkLit(4,false); 
        clause_1.push(c);
        solver.addClause(clause_1);
    }
    {
        Minisat::vec<Minisat::Lit> clause_1;
        Minisat::Lit a = Minisat::mkLit(2,false); 
        clause_1.push(a);
        Minisat::Lit b = Minisat::mkLit(3,true); 
        clause_1.push(b);
        Minisat::Lit c = Minisat::mkLit(4,true); 
        clause_1.push(c);
        solver.addClause(clause_1);
    }
    {
        Minisat::vec<Minisat::Lit> clause_1;
        Minisat::Lit a = Minisat::mkLit(2,false); 
        clause_1.push(a);
        Minisat::Lit b = Minisat::mkLit(3,true); 
        clause_1.push(b);
        Minisat::Lit c = Minisat::mkLit(4,false); 
        clause_1.push(c);
        solver.addClause(clause_1);
    }
    {
        Minisat::vec<Minisat::Lit> clause_1;
        Minisat::Lit a = Minisat::mkLit(2,false); 
        clause_1.push(a);
        Minisat::Lit b = Minisat::mkLit(3,false); 
        clause_1.push(b);
        Minisat::Lit c = Minisat::mkLit(4,true); 
        clause_1.push(c);
        solver.addClause(clause_1);
    }
    {
        Minisat::vec<Minisat::Lit> clause_1;
        Minisat::Lit a = Minisat::mkLit(2,false); 
        clause_1.push(a);
        Minisat::Lit b = Minisat::mkLit(3,false); 
        clause_1.push(b);
        Minisat::Lit c = Minisat::mkLit(4,false); 
        clause_1.push(c);
        solver.addClause(clause_1);
    }
    solver.solve();

    return 0;

}