From 6b07277cf0adf640bcd58e2afa88c7efd98c23de Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Fri, 7 Aug 2026 06:28:59 +0000
Subject: [PATCH] Fix crossed-bound dependency assertion and add regression for
 #10436

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/math/lp/lar_solver.cpp   |  5 ++---
 src/test/smt2print_parse.cpp | 16 ++++++++++++++++
 2 files changed, 18 insertions(+), 3 deletions(-)

diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp
index 3f5bdbff46..f47031af58 100644
--- a/src/math/lp/lar_solver.cpp
+++ b/src/math/lp/lar_solver.cpp
@@ -2865,12 +2865,12 @@ namespace lp {
     void lar_solver::set_crossed_bounds_column_and_deps(unsigned j, bool lower_bound, u_dependency* dep) {
         if (m_imp->m_crossed_bounds_column != null_lpvar) return; // already set
         SASSERT(m_imp->m_crossed_bounds_deps == nullptr);
-        set_status(lp_status::INFEASIBLE);
         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();
-        SASSERT(bdep != nullptr);
         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);
         TRACE(dio, tout << "crossed_bound_deps:\n";  print_explanation(tout, flatten(m_imp->m_crossed_bounds_deps)) << "\n";);
     }
     const indexed_uint_set & lar_solver::touched_rows() const { return m_imp->m_touched_rows; }
@@ -3098,4 +3098,3 @@ namespace lp {
         out << "(exit)\n";
         }
 } // namespace lp
-
diff --git a/src/test/smt2print_parse.cpp b/src/test/smt2print_parse.cpp
index 5186ec78e3..05528b9a43 100644
--- a/src/test/smt2print_parse.cpp
+++ b/src/test/smt2print_parse.cpp
@@ -405,4 +405,20 @@ void tst_smt2print_parse() {
         ENSURE(resp.find("unknown") == std::string::npos);
     }
 
+    // Regression test for GitHub issue #10436:
+    // Do not crash with crossed bounds where one side has no bound witness.
+    {
+        char const* spec =
+            "(assert (or (forall ((x Int)) (and (= 1 x) (= 0 (+ 1 (* x x)))))))\n"
+            "(check-sat)\n";
+        Z3_context ctx = Z3_mk_context(nullptr);
+        Z3_set_error_handler(ctx, setError);
+        is_error = false;
+        std::string resp = Z3_eval_smtlib2_string(ctx, spec);
+        Z3_del_context(ctx);
+        std::cout << "Issue #10436 response: " << resp << "\n";
+        ENSURE(!is_error);
+        ENSURE(resp.find("unsat") != std::string::npos);
+    }
+
 }