mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

fix crashes in sls_datatype

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-01-28 19:24:32 -08:00
parent fe713eb8e9
commit 5b175c1bcd
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/ast/sls/sls_datatype_plugin.cpp
View file

@ -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);