1 files changed, 7 insertions, 0 deletions
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 848c63a18..d1eaec231 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -112,6 +112,13 @@ void PropEngine::assertLemma(TNode node, bool negated, bool removable) {
     Dump("lemmas") << AssertCommand(BoolExpr(node.toExpr()));
   }
 
+  /* Tell decision engine */
+  if(negated) {
+    NodeBuilder<> nb(kind::NOT);
+    nb << node;
+    d_decisionEngine->addAssertion(nb.constructNode());
+  }
+
   //TODO This comment is now false
   // Assert as removable
   d_cnfStream->convertAndAssert(node, removable, negated);