diff options
author | Liana Hadarean <lianahady@gmail.com> | 2013-07-16 17:20:09 -0500 |
---|---|---|
committer | Liana Hadarean <lianahady@gmail.com> | 2013-07-16 17:20:09 -0500 |
commit | 0ac27cd827035835a176a7e599530231386412cb (patch) | |
tree | 1759af06972d69642dc7de56cfbdf5e7e9fb6d35 /src | |
parent | 6c01bb506f708ad980405dbd68a054ca8f9fe883 (diff) |
fixed bug520
Diffstat (limited to 'src')
-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); |