From 13445858f33d780e2a6e6f893a5f275d79b5ba42 Mon Sep 17 00:00:00 2001
From: hgvk94 <hgvk94@gmail.com>
Date: Wed, 19 Feb 2025 19:41:42 -0500
Subject: [PATCH] fix #7505

---
 src/qe/mbp/mbp_dt_tg.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/qe/mbp/mbp_dt_tg.cpp b/src/qe/mbp/mbp_dt_tg.cpp
index 626e8a0e4..96b45eb59 100644
--- a/src/qe/mbp/mbp_dt_tg.cpp
+++ b/src/qe/mbp/mbp_dt_tg.cpp
@@ -75,7 +75,7 @@ struct mbp_dt_tg::impl {
     void rm_select(expr *term) {
         SASSERT(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)));
         TRACE("mbp_tg", tout << "applying rm_select on " << expr_ref(term, m););
         expr *v = to_app(term)->get_arg(0);
         expr_ref sel(m);
@@ -162,7 +162,7 @@ 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);