From 4aa4cb063c27bfc722d5e70b465a897a766e52f0 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Thu, 30 Mar 2017 19:32:33 +0200 Subject: [PATCH] Add original problem to bug testfile --- tests/bugs/undecided.icnf | 1 + 1 file changed, 1 insertion(+) diff --git a/tests/bugs/undecided.icnf b/tests/bugs/undecided.icnf index b2529aba..cfb006c5 100644 --- a/tests/bugs/undecided.icnf +++ b/tests/bugs/undecided.icnf @@ -1,4 +1,5 @@ c Bug found using archsat commit c9e1ba0a95b23dfe222dc83ea4db376966153ae0 +c on problem: tptp-v6.1.0/Problems/COM/COM014+1.p c The bug is that when a clause is trivial, its litterals are *not* c added to the heap to decide on later; which breaks invariants later