Bug fix for BV

diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp
index 154f3d7f37b86e7a4a7ee2cf2fc53b834bb3f4ed..96b205bb1be3659e05771f2b152cfb8367b4b938 100644 (file)
--- a/src/theory/bv/bv_subtheory_algebraic.cpp
+++ b/src/theory/bv/bv_subtheory_algebraic.cpp
@@ -465,7 +465,7 @@ bool AlgebraicSolver::solve(TNode fact, TNode reason, SubstitutionEx& subst) {
   if (right.getKind() == kind::BITVECTOR_XOR &&
       left.getKind() == kind::BITVECTOR_XOR) {
     TNode var = left[0];
-    if (!var.getMetaKind() == kind::metakind::VARIABLE)
+    if (var.getMetaKind() != kind::metakind::VARIABLE)
       return false; 
 
     // simplify xor with same variable on both sides

diff --git a/src/theory/bv/bv_subtheory_core.cpp b/src/theory/bv/bv_subtheory_core.cpp
index fc23347c635f059b186b7309aca15cb6ca52d76a..616b20cfd5206785040a8823f095c8a726410289 100644 (file)
--- a/src/theory/bv/bv_subtheory_core.cpp
+++ b/src/theory/bv/bv_subtheory_core.cpp
@@ -294,7 +294,7 @@ void CoreSolver::buildModel() {
 
 bool CoreSolver::assertFactToEqualityEngine(TNode fact, TNode reason) {
   // Notify the equality engine
-  if (!d_bv->inConflict() && (!d_bv->wasPropagatedBySubtheory(fact) || !d_bv->getPropagatingSubtheory(fact) == SUB_CORE)) {
+  if (!d_bv->inConflict() && (!d_bv->wasPropagatedBySubtheory(fact) || d_bv->getPropagatingSubtheory(fact) != SUB_CORE)) {
     Debug("bv-slicer-eq") << "CoreSolver::assertFactToEqualityEngine fact=" << fact << endl;
     // Debug("bv-slicer-eq") << "                     reason=" << reason << endl;
     bool negated = fact.getKind() == kind::NOT;