diff --git a/src/math/lp/lar_core_solver.h b/src/math/lp/lar_core_solver.h
index 1773317be..258bfdad2 100644
--- a/src/math/lp/lar_core_solver.h
+++ b/src/math/lp/lar_core_solver.h
@@ -81,8 +81,8 @@ public:
     void backup_x() { m_backup_x = m_r_x; }
 
     void restore_x() {
+        SASSERT(m_backup_x.size() == m_r_A.column_count());
         m_r_x = m_backup_x;
-        m_r_x.reserve(m_m());
     }
 
     vector<impq> const& r_x() const { return m_r_x; }
diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp
index bfedd12e4..dae20dc69 100644
--- a/src/math/lp/nra_solver.cpp
+++ b/src/math/lp/nra_solver.cpp
@@ -241,16 +241,16 @@ struct solver::imp {
             lra.init_model();
             for (lp::constraint_index ci : lra.constraints().indices())
                 if (!check_constraint(ci)) {
-                    VERIFY(!m_coi.constraints().contains(ci));
                     IF_VERBOSE(0, verbose_stream() << "constraint " << ci << " violated\n";
                                lra.constraints().display(verbose_stream()));
+                    UNREACHABLE();
                     return l_undef;
                 }
             for (auto const &m : m_nla_core.emons()) {
                 if (!check_monic(m)) {
-                    VERIFY(!m_coi.mons().contains(m.var()));
                     IF_VERBOSE(0, verbose_stream() << "monic " << m << " violated\n";
                                lra.constraints().display(verbose_stream()));
+                    UNREACHABLE();
                     return l_undef;
                 }
             }
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 05053f4ea..91c47bbf8 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -3988,6 +3988,7 @@ public:
         lp::impq term_max;
         lp::lp_status st;
         lpvar vi = 0;
+        unsigned size_of_backup = lp().column_count();
         if (has_int()) {
             lp().backup_x();
         }
@@ -4008,7 +4009,8 @@ public:
 
             if (has_int() && lp().has_inf_int()) {
                 st = lp::lp_status::FEASIBLE;
-                lp().restore_x();
+                if (lp().column_count() == size_of_backup)
+                    lp().restore_x();
             }
             if (m_nla && (st == lp::lp_status::OPTIMAL || st == lp::lp_status::UNBOUNDED)) {
                 switch (check_nla(level)) {
@@ -4020,7 +4022,8 @@ public:
                     st = lp::lp_status::UNBOUNDED;
                     break;
                 }                
-                lp().restore_x();
+                if (lp().column_count() == size_of_backup)
+                    lp().restore_x();
             }                
         }
         switch (st) {