diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp
index 6e689c004..bd4b4cc8c 100644
--- a/src/math/lp/lar_solver.cpp
+++ b/src/math/lp/lar_solver.cpp
@@ -593,6 +593,9 @@ namespace lp {
         m_imp->m_dependencies.pop_scope(k);
         // init the nbasis sorting
         m_imp->require_nbasis_sort();
+        // bounds were restored by the trail; any entries in m_columns_with_changed_bounds
+        // are stale and must be cleared so init_model/get_value see a clean slate
+        clear_columns_with_changed_bounds();
         set_status(lp_status::UNKNOWN);
     }
 
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 901785378..099708ad6 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -3702,7 +3702,7 @@ public:
             return alloc(expr_wrapper_proc, a.mk_numeral(m_nla->am(), nl_value(v, m_nla->tmp1()), a.is_int(o)));
         }
         else {
-            rational r = get_value(v);
+            rational r = can_get_value(v) ? get_value(v) : rational::zero();
             TRACE(arith, tout << mk_pp(o, m) << " v" << v << " := " << r << "\n";);
             SASSERT("integer variables should have integer values: " && (!a.is_int(o) || r.is_int() || m.limit().is_canceled()));
             if (a.is_int(o) && !r.is_int()) r = floor(r);