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

rename

Browse source
This commit is contained in:
hgvk94 2025-02-20 04:08:15 -05:00
parent 13445858f3
commit 3a5745aee8
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -72,11 +72,11 @@ struct mbp_dt_tg::impl {
// rewrite head(x) with y
// and x with list(y, z)
void rm_select(expr *term) {
void rm_accessor(expr *term) {
SASSERT(is_app(term) &&
m_dt_util.is_accessor(to_app(term)->get_decl()) &&
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_accessor on " << expr_ref(term, m););
expr *v = to_app(term)->get_arg(0);
expr_ref sel(m);
app_ref u(m);
@ -165,7 +165,7 @@ struct mbp_dt_tg::impl {
has_var(to_app(term)->get_arg(0))) {
mark_seen(term);
progress = true;
rm_select(term);
rm_accessor(term);
continue;
}
if (is_constructor_app(term, cons, rhs)) {