From 5b175c1bcd13dca93e66e6150d6eca8d44239c1b Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 28 Jan 2025 19:24:32 -0800
Subject: [PATCH] fix crashes in sls_datatype

---
 src/ast/sls/sls_datatype_plugin.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/ast/sls/sls_datatype_plugin.cpp b/src/ast/sls/sls_datatype_plugin.cpp
index 105bfa0db..4de6ca1c9 100644
--- a/src/ast/sls/sls_datatype_plugin.cpp
+++ b/src/ast/sls/sls_datatype_plugin.cpp
@@ -274,7 +274,7 @@ namespace sls {
     }
 
     expr_ref datatype_plugin::get_value(expr* e) {
-        if (!dt.is_datatype(e))
+        if (!dt.is_datatype(e) || !g)
             return expr_ref(m);
         if (m_axiomatic_mode) {
             init_values();
@@ -325,7 +325,7 @@ namespace sls {
             bool has_null = false;
             for (auto arg : euf::enode_args(con)) {
                 if (dt.is_datatype(arg->get_sort())) {
-                    auto val_arg = m_values.get(arg->get_root_id());
+                    auto val_arg = m_values.get(arg->get_root_id(), nullptr);
                     if (!val_arg)
                         has_null = true;
                     leaf2root.insert_if_not_there(arg->get_root(), euf::enode_vector()).push_back(n);