diff --git a/src/math/lp/nex.h b/src/math/lp/nex.h
index 592fcb834..f59aa6867 100644
--- a/src/math/lp/nex.h
+++ b/src/math/lp/nex.h
@@ -208,12 +208,12 @@ public:
     nex_mul() : m_coeff(1) {}
     nex_mul(rational const& c, vector<nex_pow> const& args) : m_coeff(c), m_children(args) {}
 
-    const rational& coeff() const { return m_coeff; }
+    const rational& coeff() const override { return m_coeff; }
     
     unsigned size() const override { return m_children.size(); }
     expr_type type() const override { return expr_type::MUL; }
     // A monomial is 'pure' if does not have a numeric coefficient.
-    bool is_pure_monomial() const { return size() == 0 || !m_children[0].e()->is_scalar(); }    
+    bool is_pure_monomial() const override { return size() == 0 || !m_children[0].e()->is_scalar(); }    
 
     std::ostream & print(std::ostream& out) const override {
         bool first = true;
@@ -236,7 +236,7 @@ public:
     const nex_pow* begin() const { return m_children.begin(); }
     const nex_pow* end() const { return m_children.end(); }
 
-    bool contains(lpvar j) const {
+    bool contains(lpvar j) const override {
         for (const nex_pow& c : *this) {
             if (c.e()->contains(j))
                 return true;
@@ -269,7 +269,7 @@ public:
         return get_degree() < 2; // todo: make it more efficient
     }
 
-     bool all_factors_are_elementary() const;
+     bool all_factors_are_elementary() const override;
 
 // #ifdef Z3DEBUG
 //     virtual void sort() {
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 2a3efa7de..fb6cb42a6 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -2364,13 +2364,12 @@ public:
         if (!should_propagate()) 
             return;
         local_bound_propagator bp(*this);
-        unsigned num_changed = lp().num_changed_bounds();
+        unsigned props = m_stats.m_bound_propagations1;
 
         lp().propagate_bounds_for_touched_rows(bp);
         if (m.canceled()) {
             return;
         }
-        unsigned props = m_stats.m_bound_propagations1;
 
         if (is_infeasible()) {
             get_infeasibility_explanation_and_set_conflict();