diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index 386ad296d3b..4d1cc6edb65 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -1745,6 +1745,13 @@ bool core::influences_nl_var(lpvar j) const {
     return false;
 }
 
+void core::set_use_nra_model(bool m) {
+    if (m != m_use_nra_model) {
+        trail().push(value_trail(m_use_nra_model));
+        m_use_nra_model = m;        
+    }
+}
+    
 void core::collect_statistics(::statistics & st) {
     st.update("arith-nla-explanations", m_stats.m_nla_explanations);
     st.update("arith-nla-lemmas", m_stats.m_nla_lemmas);
diff --git a/src/math/lp/nla_core.h b/src/math/lp/nla_core.h
index 016ff6e9dec..938bcbe8367 100644
--- a/src/math/lp/nla_core.h
+++ b/src/math/lp/nla_core.h
@@ -418,7 +418,7 @@ class core {
     bool var_is_big(lpvar) const;
     bool has_real(const factorization&) const;
     bool has_real(const monic& m) const;
-    void set_use_nra_model(bool m) { m_use_nra_model = m; }
+    void set_use_nra_model(bool m);
     bool use_nra_model() const { return m_use_nra_model; }
     void collect_statistics(::statistics&);
 private: