From: Tim King <taking@cs.nyu.edu>
Date: Fri, 9 Feb 2018 23:14:48 +0000 (-0800)
Subject: Removing an always true comparison (unsigned) >= 0u.  (#1582)
X-Git-Tag: cvc5-1.0.0~5296
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=13af27ec180e73eecc846c99bd563f85577683ee;p=cvc5.git

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

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;
         }