From 78f459b303ed292a297a36cd0c435fdd025b0865 Mon Sep 17 00:00:00 2001
From: Dejan Jovanović <dejan.jovanovic@gmail.com>
Date: Mon, 26 Nov 2012 17:40:31 +0000
Subject: fixup for incremental solving

---
 src/theory/theory_engine.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'src/theory/theory_engine.cpp')

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index cd3b34879..60d79e90e 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -341,7 +341,7 @@ void TheoryEngine::check(Theory::Effort effort) {
     Debug("theory") << "TheoryEngine::check(" << effort << "): done, we are " << (d_inConflict ? "unsat" : "sat") << (d_lemmasAdded ? " with new lemmas" : " with no new lemmas") << std::endl;
 
   } catch(const theory::Interrupted&) {
-    Trace("theory") << "TheoryEngine::check() => conflict" << endl;
+    Trace("theory") << "TheoryEngine::check() => interrupted" << endl;
   }
 
   // If fulleffort, check all theories
@@ -519,7 +519,7 @@ bool TheoryEngine::properConflict(TNode conflict) const {
 }
 
 bool TheoryEngine::properPropagation(TNode lit) const {
-  if(!getPropEngine()->isTranslatedSatLiteral(lit)) {
+  if(!getPropEngine()->isSatLiteral(lit)) {
     return false;
   }
   bool b;
-- 
cgit v1.2.3