From d545494abf6e65a10789be1943512e5ebd7db83d Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Fri, 7 Aug 2026 06:30:40 +0000
Subject: [PATCH] Handle missing crossed-bound witness conservatively

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/math/lp/lar_solver.cpp | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp
index f47031af58..a16c64c431 100644
--- a/src/math/lp/lar_solver.cpp
+++ b/src/math/lp/lar_solver.cpp
@@ -2868,6 +2868,11 @@ namespace lp {
         m_imp->m_crossed_bounds_column = j;
         const auto& ul = m_imp->m_columns[j];
         u_dependency* bdep = lower_bound? ul.lower_bound_witness() : ul.upper_bound_witness();
+        if (!bdep) {
+            m_imp->m_crossed_bounds_column = null_lpvar;
+            set_status(lp_status::UNKNOWN);
+            return;
+        }
         m_imp->m_crossed_bounds_deps = dep_manager().mk_join(bdep, dep);
         SASSERT(m_imp->m_crossed_bounds_deps != nullptr);
         set_status(lp_status::INFEASIBLE);