1 files changed, 6 insertions, 1 deletions
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 26452e5e8..79ab955aa 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -296,6 +296,11 @@ EqualityStatus TheoryBV::getEqualityStatus(TNode a, TNode b)
     return EQUALITY_UNKNOWN;
   }
 
-  return d_equalitySolver.getEqualityStatus(a, b); 
+  EqualityStatus status = d_equalitySolver.getEqualityStatus(a, b);
+  if (status == EQUALITY_UNKNOWN) {
+    status = d_bitblastSolver.getEqualityStatus(a, b);
+  }
+
+  return status;
 }