diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-11-08 10:09:53 -0600 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-11-08 10:10:08 -0600 |
commit | 2f2e9fcf1fbb27f8e799aeac2372c0a9113f01aa (patch) | |
tree | 960adfe7c475b1d5c54dbb4c43b035ee6c740151 /src/theory/quantifiers/model_engine.cpp | |
parent | 1f9f7a3bd665575fd25f0fe93547ee0564cc18c9 (diff) |
Add a few options to separation logic and sets. Minor changes to separation logic, change syntax for empty heap constraint.
Diffstat (limited to 'src/theory/quantifiers/model_engine.cpp')
-rw-r--r-- | src/theory/quantifiers/model_engine.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp index 9c09371c4..1a0faa021 100644 --- a/src/theory/quantifiers/model_engine.cpp +++ b/src/theory/quantifiers/model_engine.cpp @@ -231,7 +231,7 @@ int ModelEngine::checkModel(){ } bool ModelEngine::considerQuantifiedFormula( Node q ) { - if( !d_quantEngine->getModelBuilder()->isQuantifierActive( q ) ){ //!d_quantEngine->getModel()->isQuantifierActive( q ); + if( !d_quantEngine->getModelBuilder()->isQuantifierActive( q ) || !d_quantEngine->getModel()->isQuantifierActive( q ) ){ return false; }else{ if( options::fmfEmptySorts() ){ @@ -328,7 +328,7 @@ void ModelEngine::debugPrint( const char* c ){ for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){ Node q = d_quantEngine->getModel()->getAssertedQuantifier( i ); Trace( c ) << " "; - if( !d_quantEngine->getModelBuilder()->isQuantifierActive( q ) ){ + if( !considerQuantifiedFormula( q ) ){ Trace( c ) << "*Inactive* "; }else{ Trace( c ) << " "; |