diff options
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r-- | src/theory/theory_engine.cpp | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 98eb81755..feed010e8 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -100,9 +100,15 @@ void TheoryEngine::EngineOutputChannel::registerLemmaRecipe(Node lemma, Node ori // During CNF conversion, conjunctions will be broken down into // multiple lemmas. In order for the recipes to match, we have to do // the same here. + + NodeManager* nm = NodeManager::currentNM(); + if (lemma.getKind() == kind::AND) { for (unsigned i = 0; i < lemma.getNumChildren(); ++i) registerLemmaRecipe(lemma[i], originalLemma, theoryId); + } else if (lemma.getKind() == kind::IFF) { + registerLemmaRecipe(nm->mkNode(kind::OR, lemma[0], lemma[1].negate()), originalLemma, theoryId); + registerLemmaRecipe(nm->mkNode(kind::OR, lemma[0].negate(), lemma[1]), originalLemma, theoryId); } // Theory lemmas have one step that proves the empty clause |