added regression test for constant eval

3 files changed, 23 insertions, 9 deletions

diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index 01378da56..85ae64d05 100644
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -123,7 +123,7 @@ bool CoreSolver::decomposeFact(TNode fact) {
     Node new_b = getBaseDecomposition(b, explanation);
 
     explanation.push_back(fact);
-    TNode reason = utils::mkAnd(explanation); 
+    Node reason = utils::mkAnd(explanation); 
   
     Assert (utils::getSize(new_a) == utils::getSize(new_b) &&
             utils::getSize(new_a) == utils::getSize(a)); 
@@ -197,11 +197,10 @@ bool CoreSolver::check(Theory::Effort e) {
 }
 
 bool CoreSolver::assertFactToEqualityEngine(TNode fact, TNode reason) {
-  Debug("bv-slicer-eq") << "CoreSolver::assertFactToEqualityEngine fact=" << fact << endl;
-  Debug("bv-slicer-eq") << "                     reason=" << reason << endl;
   // Notify the equality engine 
   if (d_useEqualityEngine && !d_bv->inConflict() && !d_bv->propagatedBy(fact, SUB_CORE) ) {
-    Trace("bitvector::core") << "     (assert " << fact << ")\n";  
+    Debug("bv-slicer-eq") << "CoreSolver::assertFactToEqualityEngine fact=" << fact << endl;
+    // Debug("bv-slicer-eq") << "                     reason=" << reason << endl;
     bool negated = fact.getKind() == kind::NOT;
     TNode predicate = negated ? fact[0] : fact;
     if (predicate.getKind() == kind::EQUAL) {
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 135b944ad..2d390b7b9 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -122,13 +122,13 @@ void TheoryBV::check(Effort e)
   }
   Assert (!ok == inConflict()); 
 
-  if (!inConflict() && !d_coreSolver.isCoreTheory()) {
-    ok = d_inequalitySolver.check(e); 
-  }
+  // if (!inConflict() && !d_coreSolver.isCoreTheory()) {
+  //   ok = d_inequalitySolver.check(e); 
+  // }
 
   Assert (!ok == inConflict());
-  //   if (!inConflict() && !d_coreSolver.isCoreTheory()) {
-  if (!inConflict() && !d_inequalitySolver.isInequalityTheory()) {
+  if (!inConflict() && !d_coreSolver.isCoreTheory()) {
+    //if (!inConflict() && !d_inequalitySolver.isInequalityTheory()) {
     ok = d_bitblastSolver.check(e); 
   }
   
diff --git a/test/regress/regress0/bv/core/constant_core.smt2 b/test/regress/regress0/bv/core/constant_core.smt2
new file mode 100644
index 000000000..c7a5a605f
--- /dev/null
+++ b/test/regress/regress0/bv/core/constant_core.smt2
@@ -0,0 +1,15 @@
+(set-logic QF_BV)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status unsat)
+(declare-fun x () (_ BitVec 3))
+(assert (and 
+(= ((_ extract 1 0) x) (concat ((_ extract 1 1) x) ((_ extract 0 0) x)))
+(= ((_ extract 0 0) x) ((_ extract 1 1) x))
+(= ((_ extract 2 2) x) ((_ extract 1 1) x))
+(= (_ bv0 1) ((_ extract 0 0) x))
+(= x (concat ((_ extract 2 2) x) ((_ extract 1 0) x)))
+(not (= (_ bv0 3) x))
+))
+(check-sat)
+(exit)
\ No newline at end of file