Support for separation logic. Enable cbqi by default for pure BV.

1 files changed, 2 insertions, 2 deletions

diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index d2637a555..523d868b5 100644
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -190,7 +190,7 @@ bool InstStrategyCbqi::hasNonCbqiOperator( Node n, std::map< Node, bool >& visit
 bool InstStrategyCbqi::hasNonCbqiVariable( Node q ){
   for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
     TypeNode tn = q[0][i].getType();
-    if( !tn.isInteger() && !tn.isReal() && !tn.isBoolean() ){
+    if( !tn.isInteger() && !tn.isReal() && !tn.isBoolean() && !tn.isBitVector() ){
       if( options::cbqiSplx() ){
         return true;
       }else{
@@ -242,7 +242,7 @@ Node InstStrategyCbqi::getNextDecisionRequest(){
       Node cel = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( q );
       bool value;
       if( !d_quantEngine->getValuation().hasSatValue( cel, value ) ){
-        Trace("cbqi-debug2") << "CBQI: get next decision " << cel << std::endl;
+        Trace("cbqi-dec") << "CBQI: get next decision " << cel << std::endl;
         return cel;
       }
     }