gilith/metis

BUG found in metis program: Active.checkSaturated

01mf02 opened this issue · 2 comments

01mf02 commented

When running Metis 2.3-20170925 (compiled with PolyML 5.7) on some problems, I obtain the error message:

FATAL ERROR: BUG found in metis program:
Active.checkSaturated
gilith commented

Argh: that shouldn't happen!

Thanks for the bug report, I'll investigate this.

gilith commented

I've finished my investigation, and it turns out each problem exposed a different issue in the code.

meson443.p is really satisfiable, but the debug check on the saturation set was too strict and failed, causing the bug.

meson985.p is really unsatisfiable, but saturated because the procedure for generating factors of a derived clause was broken whenever the largest literals were simplified away (e.g., ~(biggest_literal = $x) / other_literals).

Thanks again for the bug report, I have made a new release that fixes both these issues, and will shortly push a commit that formally closes this issue.