From a49d2b2067ad5caaae4f6bcab81e10b209b863f0 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Fri, 2 Jan 2026 10:54:36 -1000
Subject: [PATCH] add a check in entry_invariant()

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/math/lp/dioph_eq.cpp | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/math/lp/dioph_eq.cpp b/src/math/lp/dioph_eq.cpp
index 9929134fa..5068147a3 100644
--- a/src/math/lp/dioph_eq.cpp
+++ b/src/math/lp/dioph_eq.cpp
@@ -2239,6 +2239,10 @@ namespace lp {
                 if (var_is_fresh(p.var()))
                     continue;
                 unsigned j = local_to_lar_solver(p.var());
+                if (j == UINT_MAX) {
+                    TRACE(dio, tout << "(local: " << "x" << p.var() << ") is not registered \nbad entry:"; print_entry(ei, tout) << "\n";);
+                    return false;
+                }
                 if (is_fixed(j)) {
                     TRACE(dio, tout << "x" << j << "(local: " << "x" << p.var() << ") should not be fixed\nbad entry:"; print_entry(ei, tout) << "\n";);
                     return false;