fixed bug520

diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp
index f45250f5b3c16fa9ff1228df4869214acdb5575c..6c95bd308bd4b8f07a7262dca2b2f33fe70b2488 100644 (file)
--- a/src/theory/bv/bv_subtheory_inequality.cpp
+++ b/src/theory/bv/bv_subtheory_inequality.cpp
@@ -96,6 +96,9 @@ bool InequalitySolver::check(Theory::Effort e) {
 }
 
 EqualityStatus InequalitySolver::getEqualityStatus(TNode a, TNode b) {
+  if (!isComplete())
+    return EQUALITY_UNKNOWN;
+  
   Node a_lt_b = utils::mkNode(kind::BITVECTOR_ULT, a, b);
   Node b_lt_a = utils::mkNode(kind::BITVECTOR_ULT, b, a);