summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/instantiation_engine.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/instantiation_engine.cpp')
-rw-r--r--src/theory/quantifiers/instantiation_engine.cpp5
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 );
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback