From 84a7a79e90212c14a0a4c451ab0251d9f3369455 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 4 Dec 2023 17:08:01 -0800 Subject: [PATCH] fix #7037 --- src/smt/theory_datatype.cpp | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp index d1216c171..cfc1f06f2 100644 --- a/src/smt/theory_datatype.cpp +++ b/src/smt/theory_datatype.cpp @@ -509,10 +509,10 @@ namespace smt { // Assuming `app` is equal to a constructor term, return the constructor enode inline enode * theory_datatype::oc_get_cstor(enode * app) { theory_var v = app->get_root()->get_th_var(get_id()); - SASSERT(v != null_theory_var); + if (v == null_theory_var) + return nullptr; v = m_find.find(v); var_data * d = m_var_data[v]; - SASSERT(d->m_constructor); return d->m_constructor; } @@ -802,8 +802,9 @@ namespace smt { return false; func_decl* con = m_util.get_accessor_constructor(f); for (enode* app : ctx.enodes_of(f)) { - enode* arg = app->get_arg(0)->get_root(); - if (is_constructor(arg) && arg->get_decl() != con) + enode* arg = app->get_arg(0); + enode* arg_con = oc_get_cstor(arg); + if (arg_con && is_constructor(arg_con) && arg_con->get_decl() != con) return true; } return false;