23 lines
1.3 KiB
Diff
23 lines
1.3 KiB
Diff
--- ./src/theory/bv/bv_subtheory_algebraic.cpp.orig 2014-07-13 11:32:35.951598886 -0600
|
|
+++ ./src/theory/bv/bv_subtheory_algebraic.cpp 2015-03-08 20:00:000000000000 -0600
|
|
@@ -465,7 +465,7 @@ bool AlgebraicSolver::solve(TNode fact,
|
|
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
|
|
--- ./src/theory/bv/bv_subtheory_core.cpp.orig 2014-07-13 11:32:35.959599119 -0600
|
|
+++ ./src/theory/bv/bv_subtheory_core.cpp 2015-03-08 20:00:00.000000000 -0600
|
|
@@ -291,7 +291,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;
|