fixed more minor bugs

2 files changed, 6 insertions, 17 deletions

diff --git a/src/theory/bv/slicer.cpp b/src/theory/bv/slicer.cpp
index 1dbb48eed..e67c0b827 100644
--- a/src/theory/bv/slicer.cpp
+++ b/src/theory/bv/slicer.cpp
@@ -354,7 +354,7 @@ void Slicer::registerSimpleEquality(TNode eq) {
         Splinter* s = new Splinter(low -1 , 0);
         slice->addSplinter(0, s); 
       }
-      if (high + granularity < size) {
+      if (high != size - 1) {
         Splinter* s = new Splinter(size - 1, high + 1);
         slice->addSplinter(high+1, s); 
       }
@@ -427,7 +427,9 @@ bool Slicer::isCoreTerm(TNode node) {
     Kind kind = node.getKind(); 
     if (kind != kind::BITVECTOR_EXTRACT &&
         kind != kind::BITVECTOR_CONCAT &&
-        kind != kind::EQUAL && kind != kind::NOT) {
+        kind != kind::EQUAL && kind != kind::NOT &&
+        node.getMetaKind() != kind::metakind::VARIABLE &&
+        kind != kind::CONST_BITVECTOR) {
       d_coreTermCache[node] = false;
       return false; 
     } else {
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 5af5b2d23..1c746fafa 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -125,23 +125,10 @@ void TheoryBV::check(Effort e)
     d_coreSolver.addAssertions(new_assertions, e);
   }
 
-  // FIXME: this is not quite correct as it does not take into account cardinality constraints 
-
-  //if (d_coreSolver.isCoreTheory()) {
-    // paranoid check to make sure results of bit-blaster agree with slicer for core theory
-    // if (inConflict()) {
-    //   d_conflict = false;
-    //   d_bitblastSolver.addAssertions(new_assertions, Theory::EFFORT_FULL); 
-    //   Assert (inConflict()); 
-    // } else {
-    //   d_bitblastSolver.addAssertions(new_assertions, Theory::EFFORT_FULL); 
-    //   Assert (!inConflict()); 
-    // }
-  //}
-  //else {
-  
   if (!inConflict() && !d_coreSolver.isCoreTheory()) {
     // sending assertions to the bitblast solver if it's not just core theory 
+    Assert (false);
+    std::cout << "Using bitblaster \n"; 
     d_bitblastSolver.addAssertions(new_assertions, e);
   }