From 13af27ec180e73eecc846c99bd563f85577683ee Mon Sep 17 00:00:00 2001
From: Tim King <taking@cs.nyu.edu>
Date: Fri, 9 Feb 2018 15:14:48 -0800
Subject: [PATCH] Removing an always true comparison (unsigned) >= 0u.  (#1582)

---
 src/theory/bv/bvgauss.cpp | 6 ++++--
 1 file 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;
         }
-- 
2.30.2