Fix model construction for BV with cbqi. Minor change to defaults.

3 files changed, 9 insertions, 13 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index ace33a164..aba4f3ffc 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1855,6 +1855,7 @@ void SmtEngine::setDefaults() {
   if( d_logic.isQuantified() && 
       ( ( options::decisionMode()!=decision::DECISION_STRATEGY_INTERNAL &&
           ( d_logic.isTheoryEnabled(THEORY_ARITH) || d_logic.isTheoryEnabled(THEORY_DATATYPES) || d_logic.isTheoryEnabled(THEORY_BV) ) ) ||
+        d_logic.isPure(THEORY_ARITH) || d_logic.isPure(THEORY_BV) ||
         options::cbqiAll() ) ){
     if( !options::cbqi.wasSetByUser() ){
       options::cbqi.set( true );
diff --git a/src/theory/bv/aig_bitblaster.cpp b/src/theory/bv/aig_bitblaster.cpp
index 934e2fffd..a726a0fcd 100644
--- a/src/theory/bv/aig_bitblaster.cpp
+++ b/src/theory/bv/aig_bitblaster.cpp
@@ -232,12 +232,6 @@ Abc_Obj_t* AigBitblaster::bbFormula(TNode node) {
       result = node.getConst<bool>() ? mkTrue<Abc_Obj_t*>() : mkFalse<Abc_Obj_t*>(); 
       break;
     }
-  case kind::VARIABLE:
-  case kind::SKOLEM:
-    {
-      result = mkInput(node);
-      break;
-    }
   case kind::EQUAL:
     {
       if( node[0].getType().isBoolean() ){
@@ -251,8 +245,12 @@ Abc_Obj_t* AigBitblaster::bbFormula(TNode node) {
       //else, continue...
     }
   default:
-    bbAtom(node);
-    result = getBBAtom(node);
+    if( isVar(node) ){
+      result = mkInput(node);
+    }else{
+      bbAtom(node);
+      result = getBBAtom(node);
+    }
   }
 
   cacheAig(node, result);
@@ -315,9 +313,7 @@ void AigBitblaster::makeVariable(TNode node, Bits& bits) {
 Abc_Obj_t* AigBitblaster::mkInput(TNode input) {
   Assert (!hasInput(input));
   Assert(input.getKind() == kind::BITVECTOR_BITOF ||
-         (input.getType().isBoolean() &&
-          (input.getKind() == kind::VARIABLE ||
-           input.getKind() == kind::SKOLEM)));
+         (input.getType().isBoolean() && input.isVar()));
   Abc_Obj_t* aig_input = Abc_NtkCreatePi(currentAigNtk());
   // d_aigCache.insert(std::make_pair(input, aig_input));
   d_nodeToAigInput.insert(std::make_pair(input, aig_input));
diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index c59da27f4..ccce819e6 100644
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -238,8 +238,7 @@ void CoreSolver::buildModel() {
     TNode repr = *eqcs_i;
     ++eqcs_i;
 
-    if (repr.getKind() != kind::VARIABLE &&
-        repr.getKind() != kind::SKOLEM &&
+    if (!repr.isVar() &&
         repr.getKind() != kind::CONST_BITVECTOR &&
         !d_bv->isSharedTerm(repr)) {
       continue;