fix for de+lemmas

for the first time make regress passes even if JH is enabled

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index d1eaec231cb364238cd971ebd05072c6fe0a60f4..212a99a8e39b8b91afeea30ec0d95582b6fb333d 100644 (file)
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -117,6 +117,8 @@ void PropEngine::assertLemma(TNode node, bool negated, bool removable) {
     NodeBuilder<> nb(kind::NOT);
     nb << node;
     d_decisionEngine->addAssertion(nb.constructNode());
+  } else {
+    d_decisionEngine->addAssertion(node);
   }
 
   //TODO This comment is now false