From: Tim King <taking@cs.nyu.edu>
Date: Wed, 13 Jun 2012 20:32:04 +0000 (+0000)
Subject: Adds debugging output to theory_engine.cpp.
X-Git-Tag: cvc5-1.0.0~8034
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ece4131f2778bd3d2e5a1acbdf0f3a4054dfd1a6;p=cvc5.git

Adds debugging output to theory_engine.cpp.
---

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index f29be08a6..8abc7a0e3 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1139,6 +1139,8 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) {
     Assert(properConflict(fullConflict));
     lemma(fullConflict, true, true);
   } else {
+    Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << "):" << std::endl;
+
     // When only one theory, the conflict should need no processing
     Assert(properConflict(conflict));
     lemma(conflict, true, true);