diff options
| author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2015-03-14 17:33:26 -0500 |
|---|---|---|
| committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2015-03-14 17:33:26 -0500 |
| commit | 22ff3d48f9b2ff31c2c82c296052fc9badcfb800 (patch) | |
| tree | 348c8951614d04954680b6eb36f2170a084bc11c /src/theory/bv | |
| parent | 26582bb779d06a6d1e83c1af546ad7ed673ee2e6 (diff) | |
Bug fix for BV
Diffstat (limited to 'src/theory/bv')
| -rw-r--r-- | src/theory/bv/bv_subtheory_algebraic.cpp | 2 | ||||
| -rw-r--r-- | 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; |