fix #6582

Z3Prover · Feb 13, 2023 · 3dc91de · 3dc91de
1 parent 2b77012
commit 3dc91de
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 1 deletion.
diff --git 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
@@ -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: