From 0ac27cd827035835a176a7e599530231386412cb Mon Sep 17 00:00:00 2001 From: Liana Hadarean Date: Tue, 16 Jul 2013 17:20:09 -0500 Subject: [PATCH] fixed bug520 --- src/theory/bv/bv_subtheory_inequality.cpp | 3 +++ 1 file changed, 3 insertions(+) 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); -- 2.30.2