diff --git a/src/qe/mbp/mbp_dt_tg.cpp b/src/qe/mbp/mbp_dt_tg.cpp index 96b45eb59..4bbb4ed3b 100644 --- a/src/qe/mbp/mbp_dt_tg.cpp +++ b/src/qe/mbp/mbp_dt_tg.cpp @@ -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)) {