diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp
index 3d8a18386..175fdcd01 100644
--- a/src/math/lp/lar_solver.cpp
+++ b/src/math/lp/lar_solver.cpp
@@ -1800,10 +1800,12 @@ namespace lp {
         switch (k) {
         case LT:
             k = LE;
+            Z3_fallthrough;
         case LE:
             return floor(bound);
         case GT:
             k = GE;
+            Z3_fallthrough;
         case GE:
             return ceil(bound);
         case EQ:
@@ -2028,6 +2030,7 @@ namespace lp {
         switch (kind) {
             case LT:
                 y_of_bound = -1;
+                Z3_fallthrough;
             case LE: {
                 auto up = numeric_pair<mpq>(right_side, y_of_bound);
                 if (up < m_mpq_lar_core_solver.m_r_lower_bounds[j]) {
@@ -2043,6 +2046,7 @@ namespace lp {
             }
             case GT:
                 y_of_bound = 1;
+                Z3_fallthrough;
             case GE: {
                 auto low = numeric_pair<mpq>(right_side, y_of_bound);
                 if (low > m_mpq_lar_core_solver.m_r_upper_bounds[j]) {
@@ -2145,6 +2149,7 @@ namespace lp {
         switch (kind) {
         case LT:
             y_of_bound = -1;
+            Z3_fallthrough;
         case LE:
         {
             auto up = numeric_pair<mpq>(right_side, y_of_bound);
@@ -2156,6 +2161,7 @@ namespace lp {
         break;
         case GT:
             y_of_bound = 1;
+            Z3_fallthrough;
         case GE:
         {
             auto low = numeric_pair<mpq>(right_side, y_of_bound);
@@ -2198,6 +2204,7 @@ namespace lp {
         switch (kind) {
             case LT:
                 y_of_bound = -1;
+                Z3_fallthrough;
             case LE: {
                 auto up = numeric_pair<mpq>(right_side, y_of_bound);
                 m_mpq_lar_core_solver.m_r_upper_bounds[j] = up;
diff --git a/src/math/lp/stacked_vector.h b/src/math/lp/stacked_vector.h
index 791cddc85..4c32de2d7 100644
--- a/src/math/lp/stacked_vector.h
+++ b/src/math/lp/stacked_vector.h
@@ -25,7 +25,7 @@ template < typename B> class stacked_vector {
     struct log_entry { 
         unsigned m_i; unsigned m_ts; B b;
         log_entry(unsigned i, unsigned t, B const& b): m_i(i), m_ts(t), b(b) {}
-        log_entry():m_i(UINT_MAX), m_ts(0) {}
+        log_entry():m_i(UINT_MAX), m_ts(0), b() {}
     };
     svector<unsigned> m_stack_of_vector_sizes;
     svector<unsigned> m_stack_of_change_sizes;
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index f834de00e..267805ada 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -2131,7 +2131,7 @@ public:
     }
     
     bool can_propagate_core() {
-        return m_asserted_atoms.size() > m_asserted_qhead || m_new_def;
+        return m_asserted_atoms.size() > m_asserted_qhead || m_new_def || lp().has_changed_columns();
     }
 
     bool propagate() {