theory_lra: eagerly propagate offset equalities x=y (fixes #10065)

When a term column x - y is fixed to 0 (e.g. from t <= ca and t >= ca),
theory_lra previously discovered the implied equality x = y only lazily via
assume_eqs() during final_check. On the FP fuel-recursive axiom in issue #10065
this discovery is starved by E-matching, which unfolds the recursion and
bit-blasts an exploding FP subproblem before the branch closes.

Add propagate_offset_eq() to detect a fixed 2-variable offset term with opposite
unit-scaled coefficients and propagate the operand equality x = y directly to the
core, so congruence closure merges dependent terms immediately. This mirrors the
offset-row propagation performed by theory_arith (propagate_cheap_eq) and matches
its behavior on this benchmark (timeout -> unsat 0.06s, 2 quant-instantiations).

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 726c4e71-03ff-45f6-8322-5253254e1d7e

src/math/lp/lp_api.h

@@ -108,6 +108,7 @@ namespace lp_api {
         unsigned m_num_iterations_with_no_progress;
         unsigned m_need_to_solve_inf;
         unsigned m_fixed_eqs;
+        unsigned m_offset_eqs;
         unsigned m_conflicts;
         unsigned m_bound_propagations1;
         unsigned m_bound_propagations2;
@@ -129,6 +130,7 @@ namespace lp_api {
             st.update("arith-pivots", m_need_to_solve_inf);
             st.update("arith-plateau-iterations", m_num_iterations_with_no_progress);
             st.update("arith-fixed-eqs", m_fixed_eqs);
+            st.update("arith-offset-eqs", m_offset_eqs);
             st.update("arith-conflicts", m_conflicts);
             st.update("arith-bound-propagations-lp", m_bound_propagations1);
             st.update("arith-bound-propagations-cheap", m_bound_propagations2);

src/smt/theory_lra.cpp

@@ -3532,7 +3532,55 @@ public:
         ctx().assign_eq(x, y, eq_justification(js));
     }
     
+    //
+    // Offset equality propagation.
+    // When the column t is a term  c*x - c*y (two operands with opposite unit
+    // coefficients) that is fixed at 0, then x = y. Propagate this equality to
+    // the core so congruence closure can merge terms that depend on x and y.
+    // Without this, theory_lra only detects such equalities lazily through
+    // assume_eqs() during final_check, which can be starved (e.g. by E-matching)
+    // long before it fires. theory_arith performs the analogous propagation in
+    // propagate_cheap_eq (offset rows).
+    //
+    bool propagate_offset_eq(lp::lpvar t, u_dependency* dep, rational const& bound) {
+        if (!bound.is_zero())
+            return false;
+        if (!lp().column_has_term(t))
+            return false;
+        u_map<rational> coeffs;
+        term2coeffs(lp().get_term(t), coeffs);
+        if (coeffs.size() != 2)
+            return false;
+        auto it = coeffs.begin();
+        theory_var w1 = it->m_key;
+        rational   c1 = it->m_value;
+        ++it;
+        theory_var w2 = it->m_key;
+        rational   c2 = it->m_value;
+        if (c1 + c2 != 0)
+            return false;
+        if (w1 == w2)
+            return false;
+        enode* x = get_enode(w1);
+        enode* y = get_enode(w2);
+        if (!x || !y)
+            return false;
+        if (x->get_sort() != y->get_sort())
+            return false;
+        if (x->get_root() == y->get_root())
+            return false;
+        if (is_int(w1) != is_int(w2))
+            return false;
+        reset_evidence();
+        set_evidence(dep, m_core, m_eqs);
+        ++m_stats.m_offset_eqs;
+        assign_eq(w1, w2);
+        return true;
+    }
+
     void fixed_var_eh(theory_var v, lp::lpvar t, u_dependency* dep, rational const& bound) {
+        if (propagate_offset_eq(t, dep, bound))
+            return;
         theory_var w = null_theory_var;
         enode* x = get_enode(v);
         if (m_value2var.find(bound, w))