mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 20:18:18 +00:00
Code Activity

fix #7037

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-12-04 17:08:01 -08:00
parent f98b42ae42
commit 84a7a79e90
1 changed files with 5 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/smt/theory_datatype.cpp
View file

@ -509,10 +509,10 @@ namespace smt {
// Assuming `app` is equal to a constructor term, return the constructor enode // Assuming `app` is equal to a constructor term, return the constructor enode
inline enode * theory_datatype::oc_get_cstor(enode * app) { inline enode * theory_datatype::oc_get_cstor(enode * app) {
theory_var v = app->get_root()->get_th_var(get_id()); 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); v = m_find.find(v);
var_data * d = m_var_data[v]; var_data * d = m_var_data[v];
SASSERT(d->m_constructor);
return d->m_constructor; return d->m_constructor;
} }
@ -802,8 +802,9 @@ namespace smt {
return false; return false;
func_decl* con = m_util.get_accessor_constructor(f); func_decl* con = m_util.get_accessor_constructor(f);
for (enode* app : ctx.enodes_of(f)) { for (enode* app : ctx.enodes_of(f)) {
enode* arg = app->get_arg(0)->get_root(); enode* arg = app->get_arg(0);
if (is_constructor(arg) && arg->get_decl() != con) enode* arg_con = oc_get_cstor(arg);
if (arg_con && is_constructor(arg_con) && arg_con->get_decl() != con)
return true; return true;
} }
return false; return false;