mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-03 19:35:42 +00:00
Code Activity

fix #7505

Browse source
This commit is contained in:
hgvk94 2025-02-19 19:41:42 -05:00
parent 1fec0fa35b
commit 13445858f3
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/qe/mbp/mbp_dt_tg.cpp
View file

@ -75,7 +75,7 @@ struct mbp_dt_tg::impl {
void rm_select(expr *term) { void rm_select(expr *term) {
SASSERT(is_app(term) && SASSERT(is_app(term) &&
m_dt_util.is_accessor(to_app(term)->get_decl()) && m_dt_util.is_accessor(to_app(term)->get_decl()) &&
is_var(to_app(term)->get_arg(0))); has_var(to_app(term)->get_arg(0)));
TRACE("mbp_tg", tout << "applying rm_select on " << expr_ref(term, m);); TRACE("mbp_tg", tout << "applying rm_select on " << expr_ref(term, m););
expr *v = to_app(term)->get_arg(0); expr *v = to_app(term)->get_arg(0);
expr_ref sel(m); expr_ref sel(m);
@ -162,7 +162,7 @@ struct mbp_dt_tg::impl {
if (m_tg.is_cgr(term)) continue; if (m_tg.is_cgr(term)) continue;
if (is_app(term) && if (is_app(term) &&
m_dt_util.is_accessor(to_app(term)->get_decl()) && m_dt_util.is_accessor(to_app(term)->get_decl()) &&
is_var(to_app(term)->get_arg(0))) { has_var(to_app(term)->get_arg(0))) {
mark_seen(term); mark_seen(term);
progress = true; progress = true;
rm_select(term); rm_select(term);