From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Sat, 14 Mar 2015 22:33:26 +0000 (-0500)
Subject: Bug fix for BV
X-Git-Tag: cvc5-1.0.0~6375
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=22ff3d48f9b2ff31c2c82c296052fc9badcfb800;p=cvc5.git

Bug fix for BV
---

diff --git a/src/theory/bv/bv_subtheory_algebraic.cpp b/src/theory/bv/bv_subtheory_algebraic.cpp
index 154f3d7f3..96b205bb1 100644
--- 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 fc23347c6..616b20cfd 100644
--- 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;