diff options
author | Tim King <taking@cs.nyu.edu> | 2018-02-09 15:14:48 -0800 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-02-09 17:14:48 -0600 |
commit | 13af27ec180e73eecc846c99bd563f85577683ee (patch) | |
tree | 945152e50f21fde1e5f1aabad2374a1270e75cb2 | |
parent | 4316ad4be1f9bd9fb0842a84804f2642318cb893 (diff) |
Removing an always true comparison (unsigned) >= 0u. (#1582)
-rw-r--r-- | src/theory/bv/bvgauss.cpp | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/theory/bv/bvgauss.cpp b/src/theory/bv/bvgauss.cpp index d0e2266a7..0e2088541 100644 --- a/src/theory/bv/bvgauss.cpp +++ b/src/theory/bv/bvgauss.cpp @@ -88,9 +88,11 @@ unsigned BVGaussElim::getMinBwExpr(Node expr) { case kind::BITVECTOR_EXTRACT: { - unsigned w = utils::getSize(n); + const unsigned size = utils::getSize(n); + const unsigned low = utils::getExtractLow(n); + const unsigned child_min_width = visited[n[0]]; visited[n] = std::min( - w, std::max(visited[n[0]] - utils::getExtractLow(n), 0u)); + size, child_min_width >= low ? child_min_width - low : 0u); Assert(visited[n] <= visited[n[0]]); break; } |