From bcfa8045fabbdf0bab640a3b8082db11f7603604 Mon Sep 17 00:00:00 2001
From: Bruce Mitchener <bruce.mitchener@gmail.com>
Date: Fri, 30 Nov 2018 23:12:21 +0700
Subject: [PATCH] Sink some values into loops.

This removes some dead stores that happen prior to the loop and
ensure that no one is looking at the values outside of the
loop.
---
 src/math/polynomial/upolynomial.cpp |  6 ++----
 src/smt/theory_lra.cpp              | 10 ++++------
 2 files changed, 6 insertions(+), 10 deletions(-)

diff --git a/src/math/polynomial/upolynomial.cpp b/src/math/polynomial/upolynomial.cpp
index 5a7ed0dc1..0290a5924 100644
--- a/src/math/polynomial/upolynomial.cpp
+++ b/src/math/polynomial/upolynomial.cpp
@@ -1339,12 +1339,10 @@ namespace upolynomial {
     // Return the number of sign changes in the coefficients of p
     unsigned manager::sign_changes(unsigned sz, numeral const * p) {
         unsigned r = 0;
-        int sign, prev_sign;
-        sign = 0;
-        prev_sign = 0;
+        int prev_sign = 0;
         unsigned i = 0;
         for (; i < sz; i++) {
-            sign = sign_of(p[i]);
+            int sign = sign_of(p[i]);
             if (sign == 0)
                 continue;
             if (sign != prev_sign && prev_sign != 0)
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index ddf3e6fd2..c9db3f6b0 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -2283,16 +2283,14 @@ public:
                 
             iterator lo_inf = begin1, lo_sup = begin1;
             iterator hi_inf = begin2, hi_sup = begin2;
-            iterator lo_inf1 = begin1, lo_sup1 = begin1;
-            iterator hi_inf1 = begin2, hi_sup1 = begin2;
             bool flo_inf, fhi_inf, flo_sup, fhi_sup;
             ptr_addr_hashtable<lp_api::bound> visited;
             for (unsigned i = 0; i < atoms.size(); ++i) {
                 lp_api::bound* a1 = atoms[i];
-                lo_inf1 = next_inf(a1, lp_api::lower_t, lo_inf, end, flo_inf);
-                hi_inf1 = next_inf(a1, lp_api::upper_t, hi_inf, end, fhi_inf);
-                lo_sup1 = next_sup(a1, lp_api::lower_t, lo_sup, end, flo_sup);
-                hi_sup1 = next_sup(a1, lp_api::upper_t, hi_sup, end, fhi_sup);
+                iterator lo_inf1 = next_inf(a1, lp_api::lower_t, lo_inf, end, flo_inf);
+                iterator hi_inf1 = next_inf(a1, lp_api::upper_t, hi_inf, end, fhi_inf);
+                iterator lo_sup1 = next_sup(a1, lp_api::lower_t, lo_sup, end, flo_sup);
+                iterator hi_sup1 = next_sup(a1, lp_api::upper_t, hi_sup, end, fhi_sup);
                 if (lo_inf1 != end) lo_inf = lo_inf1; 
                 if (lo_sup1 != end) lo_sup = lo_sup1; 
                 if (hi_inf1 != end) hi_inf = hi_inf1;