Removing an always true comparison (unsigned) >= 0u. (#1582)

diff --git a/src/theory/bv/bvgauss.cpp b/src/theory/bv/bvgauss.cpp
index d0e2266a79f65218cc6f47c1bf982210923817e8..0e20885417b78912b6b1ed36e2ee48a0bf036279 100644 (file)
--- 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;
         }