From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Wed, 25 Apr 2012 21:29:49 +0000 (+0000)
Subject: fix for de+lemmas
X-Git-Tag: cvc5-1.0.0~8219
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=bdf233b3cade8f289b6cd22c6360771a042a7a14;p=cvc5.git

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 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