From bdf233b3cade8f289b6cd22c6360771a042a7a14 Mon Sep 17 00:00:00 2001
From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Wed, 25 Apr 2012 21:29:49 +0000
Subject: [PATCH] fix for de+lemmas

for the first time make regress passes even if JH is enabled
---
 src/prop/prop_engine.cpp | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index d1eaec231..212a99a8e 100644
--- 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
-- 
2.30.2