Incremental solving?
Closed this issue · 1 comments
DennisYurichev commented
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
marekpiotrow commented
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