From f7118b28977ba3e1460456824539e97592df7960 Mon Sep 17 00:00:00 2001
From: lianah <lianahady@gmail.com>
Date: Sun, 15 Jun 2014 21:33:51 -0400
Subject: [PATCH] core solver fix

---
 src/theory/bv/bv_subtheory_core.cpp | 4 ++++
 src/theory/bv/slicer.cpp            | 2 +-
 2 files changed, 5 insertions(+), 1 deletion(-)

diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index ca414a2ff..179f3a44d 100644
--- 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 0644900fa..c37c8089d 100644
--- 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; 
-- 
2.30.2