From bba10c7a8892f1067ee68751fd9989037a3386de Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 12 Jun 2025 11:30:54 -0700
Subject: [PATCH] dampen order lemmas

---
 src/math/lp/nla_order_lemmas.cpp | 3 +++
 src/math/lp/nla_order_lemmas.h   | 4 +++-
 2 files changed, 6 insertions(+), 1 deletion(-)

diff --git a/src/math/lp/nla_order_lemmas.cpp b/src/math/lp/nla_order_lemmas.cpp
index fb47fefcc..494681c91 100644
--- a/src/math/lp/nla_order_lemmas.cpp
+++ b/src/math/lp/nla_order_lemmas.cpp
@@ -83,6 +83,9 @@ void order::order_lemma_on_binomial(const monic& ac) {
 void order::order_lemma_on_binomial_sign(const monic& xy, lpvar x, lpvar y, int sign) {
     if (!c().var_is_int(x) && val(x).is_big())
         return;
+    if (&xy == m_last_binom)
+        return;
+    c().trail().push(value_trail(m_last_binom, &xy));
     SASSERT(!_().mon_has_zero(xy.vars()));
     int sy = rat_sign(val(y));
     new_lemma lemma(c(), __FUNCTION__);
diff --git a/src/math/lp/nla_order_lemmas.h b/src/math/lp/nla_order_lemmas.h
index c6961bc52..d53e5317c 100644
--- a/src/math/lp/nla_order_lemmas.h
+++ b/src/math/lp/nla_order_lemmas.h
@@ -18,7 +18,9 @@ public:
     order(core *c) : common(c) {}
     void order_lemma();
     
-private:
+    monic const* m_last_binom = nullptr;
+
+   private:
 
     bool order_lemma_on_ac_and_bc_and_factors(const monic& ac,
                                               const factor& a,