summaryrefslogtreecommitdiff
path: root/src/theory/theory_engine.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r--src/theory/theory_engine.cpp6
1 files changed, 5 insertions, 1 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index b89ca8fa4..1c297eda6 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1194,8 +1194,12 @@ Node TheoryEngine::getExplanation(TNode node) {
theory::LemmaStatus TheoryEngine::lemma(TNode node, bool negated, bool removable) {
if(Dump.isOn("t-lemmas")) {
+ Node n = node;
+ if (negated) {
+ n = node.negate();
+ }
Dump("t-lemmas") << CommentCommand("theory lemma: expect valid")
- << QueryCommand(node.toExpr());
+ << QueryCommand(n.toExpr());
}
// Share with other portfolio threads
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback