diff options
| author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2015-07-27 20:19:35 -0500 |
|---|---|---|
| committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2015-07-27 20:19:35 -0500 |
| commit | 8f4a7df9bd9cb59826e9769802d1345877a392ef (patch) | |
| tree | e0797f3a9a4160c6199ecfd5deb7727e562a5e91 /src/theory/quantifiers/instantiation_engine.cpp | |
| parent | 9f10a95e26e9e790a19a6f9e68a658ec2ab6d304 (diff) | |
| parent | c0079b3110a81f2ff993b7f86782266380dd102e (diff) | |
Merge branch 'master' of https://github.com/CVC4/CVC4
Diffstat (limited to 'src/theory/quantifiers/instantiation_engine.cpp')
| -rw-r--r-- | src/theory/quantifiers/instantiation_engine.cpp | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index 4fbf298f4..631216507 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -66,11 +66,10 @@ void InstantiationEngine::finishInit(){ //counterexample-based quantifier instantiation if( options::cbqi() ){ - if( !options::cbqi2() || options::cbqi.wasSetByUser() ){ + if( !options::cbqi2() ){ d_i_splx = new InstStrategySimplex( (arith::TheoryArith*)d_quantEngine->getTheoryEngine()->theoryOf( THEORY_ARITH ), d_quantEngine ); d_instStrategies.push_back( d_i_splx ); - } - if( options::cbqi2() ){ + }else{ d_i_cegqi = new InstStrategyCegqi( d_quantEngine ); d_instStrategies.push_back( d_i_cegqi ); } |