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/logic_info.cpp | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

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

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),
-- 
cgit v1.2.3