From f92a0e2d46bce84f36535ea2af5e0ad2eee8950d Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Tue, 7 Jul 2026 20:57:47 +0000
Subject: [PATCH] Fix FP E-matching regression: remove redundant m_new_def from
 theory_lra::can_propagate_core()

---
 src/smt/theory_lra.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index d3ac4840ad..fc023c41e1 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -2237,7 +2237,7 @@ public:
     }
     
     bool can_propagate_core() {
-        return m_asserted_atoms.size() > m_asserted_qhead || m_new_def || lp().has_changed_columns() ||
+        return m_asserted_atoms.size() > m_asserted_qhead || lp().has_changed_columns() ||
                m_delay_ineqs_qhead < m_delay_ineqs.size();
     }