From 0115b7cadcbfa8745cb4311c137e9949195d3cb1 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Sat, 17 Jan 2026 00:04:21 +0000
Subject: [PATCH] Fix segfault in dioph_eq.cpp by adding bounds check

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/math/lp/dioph_eq.cpp | 4 ++--
 test_with_logic.smt2     | 7 +++++++
 2 files changed, 9 insertions(+), 2 deletions(-)
 create mode 100644 test_with_logic.smt2

diff --git a/src/math/lp/dioph_eq.cpp b/src/math/lp/dioph_eq.cpp
index 369306973..39744ea83 100644
--- a/src/math/lp/dioph_eq.cpp
+++ b/src/math/lp/dioph_eq.cpp
@@ -1094,11 +1094,11 @@ namespace lp {
 
                 recalculate_entry(ei);
                 
-                if (m_e_matrix.m_columns.back().size() == 0) {
+                if (!m_e_matrix.m_columns.empty() && m_e_matrix.m_columns.back().size() == 0) {
                     m_e_matrix.m_columns.pop_back();
                     m_var_register.shrink(m_e_matrix.column_count());
                 }
-                if (m_l_matrix.m_columns.back().size() == 0)
+                if (!m_l_matrix.m_columns.empty() && m_l_matrix.m_columns.back().size() == 0)
                     m_l_matrix.m_columns.pop_back();
             }
             remove_irrelevant_fresh_defs();
diff --git a/test_with_logic.smt2 b/test_with_logic.smt2
new file mode 100644
index 000000000..60d67fdd3
--- /dev/null
+++ b/test_with_logic.smt2
@@ -0,0 +1,7 @@
+(set-logic UFNIRA)
+(declare-const x Bool)
+(declare-const x3 Bool)
+(declare-const x1 Int)
+(declare-fun cd (Int Int) Int)
+(assert (forall ((a Int) (b Int) (c Int)) (or (<= a 1) (<= b 1) (exists ((d Int)) (and (ite (ite (<= (to_int (+ 1.0 0.00000001 (* (to_real b) (to_real b) (to_real b)))) (cd 0 0)) true (is_int (+ 1.0 (* 0.00000001 (/ 1.0 1000000000.0)) (* (to_real b) (to_real b) (to_real b))))) (is_int (/ 0.00000001 (+ 1.0 (to_real d)))) (ite (< (abs (to_real b)) 0.00000001) true (ite (<= (abs b) (cd 0 c)) (is_int (/ (+ 0.00000001 (* (to_real x1) (to_real x1) (to_real (to_int (/ 1.0 (to_real b)))))) (+ 1 1.0))) x3))) (ite (ite (<= b (cd 0 0)) (is_int (+ 1.0 (* (/ 1.0 1000000000.0)) (* (to_real a) (to_real a) (to_real a)))) (is_int (+ 1.0 (* 0.00000001 (/ 1.0 1000000000.0)) (* 0.00000001 (to_real x1) (to_real a)) (* (to_real a) (to_real a) (to_real a))))) x (ite (< a 1.0) true (ite (<= b (cd 0 0)) true (is_int (+ 1.0 (* 0.00000001 (/ 1.0 1000000000.0)) (* (to_real (to_int (/ (to_real d) (+ 1.0 1.0)))) (to_real (to_int (/ (to_real x1) (+ 1.0 (to_real a))))) (to_real (to_int (/ (to_real x1) (+ 1.0 (to_real a))))))))))))))))
+(check-sat)