diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-02-16 16:19:51 -0600 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-02-16 16:19:51 -0600 |
| commit | 21b0cedd7dadd96e5d256885e3b65a926a7e4a81 (patch) | |
| tree | 9874097e04e8d36eb8db45ce2ad7cf2a2a9803b9 /src/theory/quantifiers/quant_split.cpp | |
| parent | 3a0e9d8d9a1288187db69b103dfd18ad64358f18 (diff) | |
Minor fixes for relations, quantifiers dsplit.
Diffstat (limited to 'src/theory/quantifiers/quant_split.cpp')
| -rw-r--r-- | src/theory/quantifiers/quant_split.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp index 24d26e72f..63935f170 100644 --- a/src/theory/quantifiers/quant_split.cpp +++ b/src/theory/quantifiers/quant_split.cpp @@ -89,7 +89,7 @@ void QuantDSplit::check( Theory::Effort e, unsigned quant_e ) { std::vector< Node > lemmas; for(std::map< Node, int >::iterator it = d_quant_to_reduce.begin(); it != d_quant_to_reduce.end(); ++it) { Node q = it->first; - if( d_quantEngine->getModel()->isQuantifierActive( q ) ){ + if( d_quantEngine->getModel()->isQuantifierAsserted( q ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){ if( d_added_split.find( q )==d_added_split.end() ){ d_added_split.insert( q ); std::vector< Node > bvs; |