fully implement the always-check-again-after-the-output-channel-is-used fix for bug #275. will finally close #275.

1 files changed, 4 insertions, 0 deletions

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index e09e9f47f..386b8bbd4 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -125,6 +125,10 @@ void TheoryEngine::check(Theory::Effort effort) {
     // Mark the lemmas flag (no lemmas added)
     d_lemmasAdded = false;
 
+    // Mark the output channel unused (if this is FULL_EFFORT, and nothing
+    // is done by the theories, no additional check will be needed)
+    d_outputChannelUsed = false;
+
     while (true) {
 
       Debug("theory") << "TheoryEngine::check(" << effort << "): running check" << std::endl;