summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/inst_strategy_cbqi.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/inst_strategy_cbqi.cpp')
-rw-r--r--src/theory/quantifiers/inst_strategy_cbqi.cpp6
1 files changed, 4 insertions, 2 deletions
diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index 149330c61..d2637a555 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -692,8 +692,10 @@ CegInstantiator * InstStrategyCegqi::getInstantiator( Node q ) {
void InstStrategyCegqi::registerQuantifier( Node q ) {
if( options::cbqiPreRegInst() ){
- //just get the instantiator
- getInstantiator( q );
+ if( doCbqi( q ) ){
+ //just get the instantiator
+ getInstantiator( q );
+ }
}
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback