Add the negative conjunction case

1 files changed, 11 insertions, 3 deletions

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index e4b4756bf..bd0b467f2 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -112,9 +112,17 @@ void TheoryEngine::EngineOutputChannel::registerLemmaRecipe(Node lemma, Node ori
   switch (lemma.getKind()) {
 
   case kind::AND:
-    Assert(!negated); // TODO
-    for (unsigned i = 0; i < lemma.getNumChildren(); ++i)
-      registerLemmaRecipe(lemma[i], originalLemma, false, theoryId);
+    if (!negated) {
+      for (unsigned i = 0; i < lemma.getNumChildren(); ++i)
+        registerLemmaRecipe(lemma[i], originalLemma, false, theoryId);
+    } else {
+      NodeBuilder<> builder(kind::OR);
+      for (unsigned i = 0; i < lemma.getNumChildren(); ++i)
+        builder << lemma[i].negate();
+
+      Node disjunction = (builder.getNumChildren() == 1) ? builder[0] : builder;
+      registerLemmaRecipe(disjunction, originalLemma, false, theoryId);
+    }
     break;
 
   case kind::IFF: