From 391febed3bd92d924439e11a30f1336d332a6bad Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Mon, 9 Mar 2026 16:51:12 +0000
Subject: [PATCH] Fix null pointer dereferences and uninitialized variables
 from discussion #8891

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/ast/euf/euf_mam.cpp              | 1 +
 src/ast/sls/sls_euf_plugin.cpp       | 8 ++++----
 src/math/realclosure/realclosure.cpp | 6 ++++++
 src/muz/spacer/spacer_context.cpp    | 4 ++--
 src/smt/mam.cpp                      | 1 +
 5 files changed, 14 insertions(+), 6 deletions(-)

diff --git a/src/ast/euf/euf_mam.cpp b/src/ast/euf/euf_mam.cpp
index 00d9c0726..cce838c61 100644
--- a/src/ast/euf/euf_mam.cpp
+++ b/src/ast/euf/euf_mam.cpp
@@ -1402,6 +1402,7 @@ namespace euf {
                 // to check it again.
                 get_check_mark(reg) == NOT_CHECKED &&
                 is_ground(m_registers[reg]) &&
+                instr->m_enode != nullptr &&
                 get_pat_lbl_hash(reg) == instr->m_enode->get_lbl_hash();
         }
 
diff --git a/src/ast/sls/sls_euf_plugin.cpp b/src/ast/sls/sls_euf_plugin.cpp
index d1d135d1e..696944bec 100644
--- a/src/ast/sls/sls_euf_plugin.cpp
+++ b/src/ast/sls/sls_euf_plugin.cpp
@@ -289,23 +289,23 @@ namespace sls {
                     b = g.find(to_app(e)->get_arg(1));
                 }
                 if (lit.sign() && m.is_eq(e)) {
-                    if (a->get_root() == b->get_root()) {
+                    if (a && b && a->get_root() == b->get_root()) {
                         IF_VERBOSE(0, verbose_stream() << "not disequal " << lit << " " << mk_pp(e, m) << "\n");
                         ctx.display(verbose_stream());
                         UNREACHABLE();
                     }
                 }
                 else if (!lit.sign() && m.is_eq(e)) {
-                    if (a->get_root() != b->get_root()) {
+                    if (a && b && a->get_root() != b->get_root()) {
                         IF_VERBOSE(0, verbose_stream() << "not equal " << lit << " " << mk_pp(e, m) << "\n");
                         //UNREACHABLE();
                     }
                 }
-                else if (to_app(e)->get_family_id() != basic_family_id && lit.sign() && g.find(e)->get_root() != g.find(m.mk_false())->get_root()) {
+                else if (to_app(e)->get_family_id() != basic_family_id && lit.sign() && g.find(e) && g.find(m.mk_false()) && g.find(e)->get_root() != g.find(m.mk_false())->get_root()) {
                     IF_VERBOSE(0, verbose_stream() << "not alse " << lit << " " << mk_pp(e, m) << "\n");
                     //UNREACHABLE();
                 }
-                else if (to_app(e)->get_family_id() != basic_family_id && !lit.sign() && g.find(e)->get_root() != g.find(m.mk_true())->get_root()) {
+                else if (to_app(e)->get_family_id() != basic_family_id && !lit.sign() && g.find(e) && g.find(m.mk_true()) && g.find(e)->get_root() != g.find(m.mk_true())->get_root()) {
                     IF_VERBOSE(0, verbose_stream() << "not true " << lit << " " << mk_pp(e, m) << "\n");
                     //UNREACHABLE();
                 }
diff --git a/src/math/realclosure/realclosure.cpp b/src/math/realclosure/realclosure.cpp
index 80e6420bd..8b11e1725 100644
--- a/src/math/realclosure/realclosure.cpp
+++ b/src/math/realclosure/realclosure.cpp
@@ -3458,6 +3458,8 @@ namespace realclosure {
                 if (sc) sc = sc->prev();
                 i--;
             }
+            if (!sc)
+                return 0;
             return ext->sdt()->qs()[sc->qidx()].size();
         }
 
@@ -3474,6 +3476,8 @@ namespace realclosure {
                 if (sc) sc = sc->prev();
                 i--;
             }
+            if (!sc)
+                return 0;
             const polynomial & q = ext->sdt()->qs()[sc->qidx()];
             return q.size();
         }
@@ -3491,6 +3495,8 @@ namespace realclosure {
                 if (sc) sc = sc->prev();
                 i--;
             }
+            if (!sc)
+                return numeral();
             const polynomial & q = ext->sdt()->qs()[sc->qidx()];
             if (j >= q.size())
                 return numeral();
diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp
index cf27f23cb..3f46dadb4 100644
--- a/src/muz/spacer/spacer_context.cpp
+++ b/src/muz/spacer/spacer_context.cpp
@@ -3330,7 +3330,7 @@ bool context::is_reachable(pob &n)
     model_ref mdl;
 
     // used in case n is reachable
-    bool is_concrete;
+    bool is_concrete = false;
     const datalog::rule * r = nullptr;
     // denotes which predecessor's (along r) reach facts are used
     bool_vector reach_pred_used;
@@ -3521,7 +3521,7 @@ lbool context::expand_pob(pob& n, pob_ref_buffer &out)
     model_ref model;
 
     // used in case n is reachable
-    bool is_concrete;
+    bool is_concrete = false;
     const datalog::rule * r = nullptr;
     // denotes which predecessor's (along r) reach facts are used
     bool_vector reach_pred_used;
diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp
index a27fc293f..3719f30c9 100644
--- a/src/smt/mam.cpp
+++ b/src/smt/mam.cpp
@@ -1360,6 +1360,7 @@ namespace {
                 // to check it again.
                 get_check_mark(reg) == NOT_CHECKED &&
                 is_ground(m_registers[reg]) &&
+                instr->m_enode != nullptr &&
                 get_pat_lbl_hash(reg) == instr->m_enode->get_lbl_hash();
         }