gilith/metis

FATAL ERROR: BUG found in metis program: Active.simplify

01mf02 opened this issue · 2 comments

01mf02 commented

Here is one more problem that triggers a bug in Metis. The error message states:

FATAL ERROR: BUG found in metis program:
Active.simplify: clause should have been simplified away
gilith commented

Thanks Michael, I can reproduce the bug and am working to root-cause it.

gilith commented

I've root-caused the bug to some mishandling of disequalities during rewriting. For example, given the rewrite f X = c, the clause ~(f Y = g a b) / p (g a b) should be rewritten to ~(c = g a b) / p c in one step, but the buggy code caused the rewrite to return ~(c = g a b) / p (g a b). If this clause was rewritten again it would correctly return ~(c = g a b) / p c, but it shouldn't take two steps to do this.

I've released a new version - Metis 2.3 (release 20171021) - that fixes this and will shortly push a commit that closes this issue.

Thank you for the bug report, please keep them coming. You're up to two incompleteness bugs on the changelog now :-)