diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-04-25 21:29:49 +0000 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2012-04-25 21:29:49 +0000 |
| commit | bdf233b3cade8f289b6cd22c6360771a042a7a14 (patch) | |
| tree | 98cbd46f483f5c578b3fb51442b864bb3f32a78b /src/prop | |
| parent | c0f5194dd56c5127c5c6dab5e59997eccc2d78a5 (diff) | |
fix for de+lemmas
for the first time make regress passes even if JH is enabled
Diffstat (limited to 'src/prop')
| -rw-r--r-- | src/prop/prop_engine.cpp | 2 |
1 files changed, 2 insertions, 0 deletions
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 |