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_bv.cpp b/src/smt/theory_bv.cpp
index 33207d15a..0f4a6480b 100644
--- a/src/smt/theory_bv.cpp
+++ b/src/smt/theory_bv.cpp
@@ -1083,7 +1083,6 @@ namespace smt {
         for (unsigned i = 0; i <= num_args; i++) {
             expr* arg = (i == num_args)?n:n->get_arg(i);
             sort* s = get_manager().get_sort(arg);
-            s = get_manager().get_sort(arg);
             if (m_util.is_bv_sort(s) && m_util.get_bv_size(arg) > m_params.m_bv_blast_max_size) {                
                 if (!m_approximates_large_bvs) {
                     TRACE("bv", tout << "found large size bit-vector:\n" << mk_pp(n, get_manager()) << "\n";);
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; 
diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 2ae445561..bd0885fa4 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -7501,15 +7501,12 @@ namespace smt {
             expr_ref newConcat(m);
             if (arg1 != a1 || arg2 != a2) {
                 TRACE("str", tout << "resolved concat argument(s) to eqc string constants" << std::endl;);
-                int iPos = 0;
                 expr_ref_vector item1(m);
                 if (a1 != arg1) {
                     item1.push_back(ctx.mk_eq_atom(a1, arg1));
-                    iPos += 1;
                 }
                 if (a2 != arg2) {
                     item1.push_back(ctx.mk_eq_atom(a2, arg2));
-                    iPos += 1;
                 }
                 expr_ref implyL1(mk_and(item1), m);
                 newConcat = mk_concat(arg1, arg2);