From: lianah <lianahady@gmail.com>
Date: Mon, 16 Jun 2014 01:33:51 +0000 (-0400)
Subject: core solver fix
X-Git-Tag: cvc5-1.0.0~6802
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f7118b28977ba3e1460456824539e97592df7960;p=cvc5.git

core solver fix
---

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;