diff options
Diffstat (limited to 'src/theory/quantifiers/inst_strategy_cbqi.cpp')
-rw-r--r-- | src/theory/quantifiers/inst_strategy_cbqi.cpp | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp index 6a2bd5e2e..f378b4913 100644 --- a/src/theory/quantifiers/inst_strategy_cbqi.cpp +++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp @@ -19,6 +19,7 @@ #include "theory/theory_engine.h" #include "theory/quantifiers/options.h" #include "theory/quantifiers/term_database.h" +#include "theory/quantifiers/first_order_model.h" using namespace std; using namespace CVC4; @@ -255,9 +256,9 @@ void InstStrategySimplex::debugPrint( const char* c ){ //} } Debug(c) << std::endl; - - for( int q=0; q<d_quantEngine->getNumQuantifiers(); q++ ){ - Node f = d_quantEngine->getQuantifier( q ); + + for( int i=0; i<(int)d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ + Node f = d_quantEngine->getModel()->getAssertedQuantifier( i ); Debug(c) << f << std::endl; Debug(c) << " Inst constants: "; for( int i=0; i<(int)d_quantEngine->getTermDatabase()->getNumInstantiationConstants( f ); i++ ){ |