From: lianah <lianahady@gmail.com>
Date: Tue, 26 Mar 2013 20:55:29 +0000 (-0400)
Subject: core theory currently disabled
X-Git-Tag: cvc5-1.0.0~7361^2~14
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=33a5c0897bdbfb8367dfa90342471615908df1bc;p=cvc5.git

core theory currently disabled
---

diff --git a/src/theory/bv/slicer.cpp b/src/theory/bv/slicer.cpp
index 23ae5beec..121802b65 100644
--- a/src/theory/bv/slicer.cpp
+++ b/src/theory/bv/slicer.cpp
@@ -777,8 +777,8 @@ void Slicer::getBaseDecomposition(TNode node, std::vector<Node>& decomp, std::ve
 bool Slicer::isCoreTerm(TNode node) {
   if (d_coreTermCache.find(node) == d_coreTermCache.end()) {
     Kind kind = node.getKind(); 
-    if (kind != kind::BITVECTOR_EXTRACT &&
-        kind != kind::BITVECTOR_CONCAT &&
+    if (//kind != kind::BITVECTOR_EXTRACT &&
+        //kind != kind::BITVECTOR_CONCAT &&
         kind != kind::EQUAL &&
         kind != kind::STORE &&
         kind != kind::SELECT &&