From: Liana Hadarean <lianahady@gmail.com>
Date: Tue, 16 Jul 2013 22:20:09 +0000 (-0500)
Subject: fixed bug520
X-Git-Tag: cvc5-1.0.0~7287^2~60
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0ac27cd827035835a176a7e599530231386412cb;p=cvc5.git

fixed bug520
---

diff --git a/src/theory/bv/bv_subtheory_inequality.cpp b/src/theory/bv/bv_subtheory_inequality.cpp
index f45250f5b..6c95bd308 100644
--- 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);