From a6c94a1bfc5ce12a0a79fe60e1909937b5ceb578 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Mon, 9 Mar 2026 16:57:59 +0000
Subject: [PATCH] Refactor sls_euf_plugin.cpp validate_model and add SASSERT in
 udoc_relation.cpp

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/ast/sls/sls_euf_plugin.cpp | 20 ++++++++++++++------
 src/muz/rel/udoc_relation.cpp  |  1 +
 2 files changed, 15 insertions(+), 6 deletions(-)

diff --git a/src/ast/sls/sls_euf_plugin.cpp b/src/ast/sls/sls_euf_plugin.cpp
index 696944bec..8ab5f73df 100644
--- a/src/ast/sls/sls_euf_plugin.cpp
+++ b/src/ast/sls/sls_euf_plugin.cpp
@@ -301,13 +301,21 @@ namespace sls {
                         //UNREACHABLE();
                     }
                 }
-                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()) {
+                    auto* ne = g.find(e);
+                    auto* nf = g.find(m.mk_false());
+                    if (ne && nf && ne->get_root() != nf->get_root()) {
+                        IF_VERBOSE(0, verbose_stream() << "not false " << lit << " " << mk_pp(e, m) << "\n");
+                        //UNREACHABLE();
+                    }
                 }
-                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();
+                else if (to_app(e)->get_family_id() != basic_family_id && !lit.sign()) {
+                    auto* ne = g.find(e);
+                    auto* nt = g.find(m.mk_true());
+                    if (ne && nt && ne->get_root() != nt->get_root()) {
+                        IF_VERBOSE(0, verbose_stream() << "not true " << lit << " " << mk_pp(e, m) << "\n");
+                        //UNREACHABLE();
+                    }
                 }
             
         }
diff --git a/src/muz/rel/udoc_relation.cpp b/src/muz/rel/udoc_relation.cpp
index 068af24b6..17d68660e 100644
--- a/src/muz/rel/udoc_relation.cpp
+++ b/src/muz/rel/udoc_relation.cpp
@@ -54,6 +54,7 @@ namespace datalog {
                 col = column_idx(orig[i]);
                 limit = col + column_num_bits(orig[i]);
             } else {
+                SASSERT(other);
                 unsigned idx = orig[i] - get_num_cols();
                 col = get_num_bits() + other->column_idx(idx);
                 limit = col + other->column_num_bits(idx);