diff options
| -rw-r--r-- | src/theory/bv/bv_subtheory_inequality.cpp | 3 |
1 files changed, 3 insertions, 0 deletions
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); |