From 3dc91de531dd835b723b5d572f5024a491a966cf Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 13 Feb 2023 13:20:55 -0800
Subject: [PATCH] fix #6582

---
 src/math/lp/nla_core.cpp | 7 +++++++
 src/math/lp/nla_core.h   | 2 +-
 2 files changed, 8 insertions(+), 1 deletion(-)

diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index 386ad296d3..4d1cc6edb6 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 016ff6e9de..938bcbe836 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: