From f50f21198e636e7f4b7a913139102f6562173887 Mon Sep 17 00:00:00 2001 From: Hari Govind V K Date: Thu, 20 Feb 2025 17:54:59 +0000 Subject: [PATCH] Fix #7505 (#7565) * fix #7505 * rename --- src/qe/mbp/mbp_dt_tg.cpp | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/qe/mbp/mbp_dt_tg.cpp b/src/qe/mbp/mbp_dt_tg.cpp index 626e8a0e4..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()) && - is_var(to_app(term)->get_arg(0))); - TRACE("mbp_tg", tout << "applying rm_select on " << expr_ref(term, m);); + has_var(to_app(term)->get_arg(0))); + 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); @@ -162,10 +162,10 @@ struct mbp_dt_tg::impl { if (m_tg.is_cgr(term)) continue; if (is_app(term) && 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); progress = true; - rm_select(term); + rm_accessor(term); continue; } if (is_constructor_app(term, cons, rhs)) {