assertion is hit in SimpSolver::relocAll

[Victor Khomenko]

Dear all,

I have the following problem: an assertion in SimpSolver::relocAll is
hit, and I'm not sure whether it's a bug in MiniSat itself or it's
because of my (rather unsavoury) use of it.

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 normally this assertion is not hit as Solver::checkGarbage
might decide not to call garbageCollect.


So, is this a real bug or I'm missing something?

Thanks,
Victor.

[Niklas Sörensson]

Hi Victor,

I think it's a bug. Is this with the development version of MiniSat?
If so, can you add it to the bug tracker so I don't forget?

/Niklas

[Victor Khomenko]

Hi Niklas,

It's in the current version @github, but is likely to be in the
previous versions too - this behaviour is not easy to reproduce. I've
submitted it as an issue @github.

Victor.

> > Victor.- Hide quoted text -
>
> - Show quoted text -

[Andreas Morgenstern]

Hi Niklas,

did you work on that problem?
I'm facing the same problem in a different context.
As Victor pointed out, the problem is very hard to reproduce.

Andreas

[Niklas Sörensson]

Hello Andreas,

No, I have not had time to check this out and I might not be able to
do so at all unfortunately since I no longer work in academia. It
don't think it should be that hard to correct though.

/Niklas