mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

fix #5219

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-04-27 09:30:00 -07:00
parent d731ec7cba
commit 78571b9a51
1 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/sat/smt/dt_solver.cpp
View file

@ -703,9 +703,11 @@ namespace dt {
} }
bool solver::add_dep(euf::enode* n, top_sort<euf::enode>& dep) { bool solver::add_dep(euf::enode* n, top_sort<euf::enode>& dep) {
theory_var v = n->get_th_var(get_id());
if (!is_datatype(n->get_expr())) if (!is_datatype(n->get_expr()))
return true; return true;
theory_var v = n->get_th_var(get_id());
if (v == euf::null_theory_var)
return true;
euf::enode* con = m_var_data[m_find.find(v)]->m_constructor; euf::enode* con = m_var_data[m_find.find(v)]->m_constructor;
if (con->num_args() == 0) if (con->num_args() == 0)
dep.insert(n, nullptr); dep.insert(n, nullptr);