From a2bac119d3376ec9be68e88c51590e28772fade3 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 18 Apr 2023 08:40:51 -0700
Subject: [PATCH] differentiate fixed from offset-eq in statistics

---
 src/math/lp/lp_bound_propagator.h | 8 ++++++--
 src/math/lp/lp_settings.h         | 2 ++
 2 files changed, 8 insertions(+), 2 deletions(-)

diff --git a/src/math/lp/lp_bound_propagator.h b/src/math/lp/lp_bound_propagator.h
index 14f646fc12b..dba93398ea9 100644
--- a/src/math/lp/lp_bound_propagator.h
+++ b/src/math/lp/lp_bound_propagator.h
@@ -578,8 +578,12 @@ class lp_bound_propagator {
               );
         
         bool added = m_imp.add_eq(je, ke, exp, is_fixed);
-        if (added)
-            lp().stats().m_offset_eqs++;
+        if (added) {
+            if (is_fixed)
+                lp().stats().m_fixed_eqs++;
+            else
+                lp().stats().m_offset_eqs++;
+        }
         return added;
     }
 
diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h
index 9a38fd582cb..5234e3bf0e3 100644
--- a/src/math/lp/lp_settings.h
+++ b/src/math/lp/lp_settings.h
@@ -121,6 +121,7 @@ struct statistics {
     unsigned m_grobner_calls;
     unsigned m_grobner_conflicts;
     unsigned m_offset_eqs;
+    unsigned m_fixed_eqs;
     statistics() { reset(); }
     void reset() { memset(this, 0, sizeof(*this)); }
     void collect_statistics(::statistics& st) const {
@@ -142,6 +143,7 @@ struct statistics {
         st.update("arith-grobner-calls", m_grobner_calls);
         st.update("arith-grobner-conflicts", m_grobner_conflicts);
         st.update("arith-offset-eqs", m_offset_eqs);
+        st.update("arith-fixed-eqs", m_fixed_eqs);
 
     }
 };