fixup for incremental solving

4 files changed, 8 insertions, 8 deletions

diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp
index aca81e176..91482526a 100644
--- a/src/theory/bv/bitblaster.cpp
+++ b/src/theory/bv/bitblaster.cpp
@@ -100,7 +100,7 @@ void Bitblaster::bbAtom(TNode node) {
   Node atom_definition = mkNode(kind::IFF, node, atom_bb);
 
   if (!options::bitvectorEagerBitblast()) {
-    d_cnfStream->convertAndAssert(atom_definition, true, false);
+    d_cnfStream->convertAndAssert(atom_definition, false, false);
     d_bitblastedAtoms.insert(node);
   } else {
     d_bvOutput->lemma(atom_definition, false);
diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp
index e76e2ace9..f90bee19d 100644
--- a/src/theory/logic_info.cpp
+++ b/src/theory/logic_info.cpp
@@ -31,7 +31,7 @@ namespace CVC4 {
 
 LogicInfo::LogicInfo() :
   d_logicString(""),
-  d_theories(),
+  d_theories(THEORY_LAST, false),
   d_sharingTheories(0),
   d_integers(true),
   d_reals(true),
@@ -40,14 +40,13 @@ LogicInfo::LogicInfo() :
   d_locked(false) {
 
   for(TheoryId id = THEORY_FIRST; id < THEORY_LAST; ++id) {
-    d_theories[id] = false;// ensure it's cleared
     enableTheory(id);
   }
 }
 
 LogicInfo::LogicInfo(std::string logicString) throw(IllegalArgumentException) :
   d_logicString(""),
-  d_theories(),
+  d_theories(THEORY_LAST, false),
   d_sharingTheories(0),
   d_integers(false),
   d_reals(false),
@@ -61,7 +60,7 @@ LogicInfo::LogicInfo(std::string logicString) throw(IllegalArgumentException) :
 
 LogicInfo::LogicInfo(const char* logicString) throw(IllegalArgumentException) :
   d_logicString(""),
-  d_theories(),
+  d_theories(THEORY_LAST, false),
   d_sharingTheories(0),
   d_integers(false),
   d_reals(false),
diff --git a/src/theory/logic_info.h b/src/theory/logic_info.h
index e2d8f3da6..fd81ea629 100644
--- a/src/theory/logic_info.h
+++ b/src/theory/logic_info.h
@@ -22,6 +22,7 @@
 #define __CVC4__LOGIC_INFO_H
 
 #include <string>
+#include <vector>
 #include "expr/kind.h"
 
 namespace CVC4 {
@@ -43,7 +44,7 @@ namespace CVC4 {
  */
 class CVC4_PUBLIC LogicInfo {
   mutable std::string d_logicString; /**< an SMT-LIB-like logic string */
-  bool d_theories[theory::THEORY_LAST]; /**< set of active theories */
+  std::vector<bool> d_theories; /**< set of active theories */
   size_t d_sharingTheories; /**< count of theories that need sharing */
 
   // for arithmetic
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;