diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp
index 32b935b9ae2..74cce593d71 100644
--- a/src/sat/smt/arith_solver.cpp
+++ b/src/sat/smt/arith_solver.cpp
@@ -1518,6 +1518,7 @@ namespace arith {
 
     void solver::propagate_nla() {
         if (m_nla) {
+            m_a1 = nullptr; m_a2 = nullptr;
             m_nla->propagate();
             add_lemmas();
             lp().collect_more_rows_for_lp_propagation();
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 90e6ddce0e8..d6c14311e8f 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -2178,6 +2178,8 @@ class theory_lra::imp {
 
     void propagate_nla() {
         if (m_nla) {
+            m_a1 = nullptr; 
+            m_a2 = nullptr;
             m_nla->propagate();
             add_lemmas();
             lp().collect_more_rows_for_lp_propagation();
@@ -3385,7 +3387,7 @@ class theory_lra::imp {
     }
 
     nlsat::anum const& nl_value(theory_var v, scoped_anum& r) const {
-        SASSERT(use_nra_model());
+        SASSERT(m_nla && m_nla->use_nra_model());
         auto t = get_tv(v);
         if (t.is_term()) {