core solver fix

diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index ca414a2ff8da16cff2f95df9749a8053322c0f20..179f3a44ddb3d5bf3d12c6dc857d2d98d41a842e 100644 (file)
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -172,6 +172,10 @@ bool CoreSolver::check(Theory::Effort e) {
   bool ok = true;
   std::vector<Node> core_eqs;
   TNodeBoolMap seen;
+  // slicer does not deal with cardinality constraints yet
+  if (d_useSlicer) {
+    d_isComplete = false; 
+  }
   while (! done()) {
     TNode fact = get();
     if (d_isComplete && !isCompleteForTerm(fact, seen)) {

diff --git a/src/theory/bv/slicer.cpp b/src/theory/bv/slicer.cpp
index 0644900fabc589fb458baa876ab24a479182ee32..c37c8089de1c3d52ae8507829d809a9ab7aaecab 100644 (file)
--- a/src/theory/bv/slicer.cpp
+++ b/src/theory/bv/slicer.cpp
@@ -498,7 +498,7 @@ bool Slicer::isCoreTerm(TNode node) {
   if (d_coreTermCache.find(node) == d_coreTermCache.end()) {
     Kind kind = node.getKind();
     bool not_core;
-    if (options::bitvectorEqualitySlicer()) {
+    if (options::bitvectorEqualitySlicer() != BITVECTOR_SLICER_OFF) {
       not_core = (kind != kind::BITVECTOR_EXTRACT && kind != kind::BITVECTOR_CONCAT); 
     } else {
       not_core = true;