--- ./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;