From: Morgan Deters Date: Fri, 24 Aug 2012 21:40:46 +0000 (+0000) Subject: fix TheoryEngine::collectModelInfo() to only call collectModelInfo() on active theori... X-Git-Tag: cvc5-1.0.0~7848 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5f0f35cc281b988db6d0f3dfa4b797f91b69f6ab;p=cvc5.git fix TheoryEngine::collectModelInfo() to only call collectModelInfo() on active theories; resolves bug 380 --- 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; icollectModelInfo( 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); } } }