From 5f0f35cc281b988db6d0f3dfa4b797f91b69f6ab Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@gmail.com>
Date: Fri, 24 Aug 2012 21:40:46 +0000
Subject: [PATCH] fix TheoryEngine::collectModelInfo() to only call
 collectModelInfo() on active theories; resolves bug 380

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

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 7cf356d2c..d4e1c89c5 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -561,10 +561,11 @@ bool TheoryEngine::properExplanation(TNode node, TNode expl) const {
 }
 
 void TheoryEngine::collectModelInfo( theory::TheoryModel* m ){
-  //consult each theory to get all relevant information concerning the model
-  for( int i=0; i<theory::THEORY_LAST; i++ ){
-    if( d_theoryTable[i] ){
-      d_theoryTable[i]->collectModelInfo( m );
+  // Consult each active theory to get all relevant information
+  // concerning the model.
+  for(TheoryId theoryId = theory::THEORY_FIRST; theoryId < theory::THEORY_LAST; ++theoryId) {
+    if(d_logicInfo.isTheoryEnabled(theoryId)) {
+      d_theoryTable[theoryId]->collectModelInfo(m);
     }
   }
 }
-- 
2.30.2