diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-08-24 21:40:46 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-08-24 21:40:46 +0000 |
commit | 5f0f35cc281b988db6d0f3dfa4b797f91b69f6ab (patch) | |
tree | 62b686f999055f95cd6a53d2e4a1654809246d40 /src | |
parent | 0fb11ee5999c70f8c30cf8081ddbb3eca6ded0b1 (diff) |
fix TheoryEngine::collectModelInfo() to only call collectModelInfo() on active theories; resolves bug 380
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/theory_engine.cpp | 9 |
1 files 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); } } } |