From 22ff3d48f9b2ff31c2c82c296052fc9badcfb800 Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Sat, 14 Mar 2015 17:33:26 -0500 Subject: [PATCH] Bug fix for BV --- src/theory/bv/bv_subtheory_algebraic.cpp | 2 +- src/theory/bv/bv_subtheory_core.cpp | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) 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; -- 2.30.2