From c277b39b1b26df68dc7df6dc9df77680207ed79a Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Fri, 16 Jan 2026 23:46:26 +0000
Subject: [PATCH 1/4] Initial plan


From b5202c65c093cd6d34b473cb0dddd4c615207a72 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Fri, 16 Jan 2026 23:48:19 +0000
Subject: [PATCH 2/4] Initial analysis of segfault issue

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 test_segfault.smt2 | 6 ++++++
 1 file changed, 6 insertions(+)
 create mode 100644 test_segfault.smt2

diff --git a/test_segfault.smt2 b/test_segfault.smt2
new file mode 100644
index 000000000..1ed811abc
--- /dev/null
+++ b/test_segfault.smt2
@@ -0,0 +1,6 @@
+(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)

From 522aa69e09c6a5eedf7dd1b96a5395157112d74e 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 3/4] 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)

From bd67c3f7ae20840319d9beedc95e28be411fe6b2 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Sat, 17 Jan 2026 00:09:54 +0000
Subject: [PATCH 4/4] Clean up temporary test files

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 test_segfault.smt2   | 6 ------
 test_with_logic.smt2 | 7 -------
 2 files changed, 13 deletions(-)
 delete mode 100644 test_segfault.smt2
 delete mode 100644 test_with_logic.smt2

diff --git a/test_segfault.smt2 b/test_segfault.smt2
deleted file mode 100644
index 1ed811abc..000000000
--- a/test_segfault.smt2
+++ /dev/null
@@ -1,6 +0,0 @@
-(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)
diff --git a/test_with_logic.smt2 b/test_with_logic.smt2
deleted file mode 100644
index 60d67fdd3..000000000
--- a/test_with_logic.smt2
+++ /dev/null
@@ -1,7 +0,0 @@
-(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)