From 1a2547995acc5a98c8969e628ac5e1c45b0efe94 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Fri, 17 Jun 2016 15:55:56 -0500
Subject: Support for separation logic. Enable cbqi by default for pure BV.

---
 src/theory/quantifiers/inst_strategy_cbqi.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'src/theory/quantifiers/inst_strategy_cbqi.cpp')

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;
       }
     }
-- 
cgit v1.2.3