marekpiotrow/UWrMaxSat

Incremental solving?

Closed this issue · 1 comments

Marek.
Thank you for your work.
But I probably hit another bug.
Actually, I wanted to add negated (blocking) clause after calling solve(). And then I wanted to call solve() again and again.
But it crashes.

int main()
{
        void* ctx=ipamir_init();
        ipamir_add_hard(ctx, 1);
        ipamir_add_hard(ctx, 0);
        ipamir_solve(ctx);

        ipamir_add_hard(ctx, 2);
        ipamir_add_hard(ctx, 0);
        ipamir_solve(ctx);

        ipamir_release(ctx);
};

Getting:

malloc_consolidate(): invalid chunk size
zsh: IOT instruction (core dumped)  ./must_work2

All the files I'm using:
https://yurichev.com/tmp2/UWrMaxSat_bugs2.tar

Hi Dennis,
I have just fixed the problem. It was caused by my recent modification, where mem.freeAll() was called too early. Now it is done in the destructor of a MsSolver object and this solves the issue.
Marek