diff --git a/src/qe/mbp/mbp_dt_tg.cpp b/src/qe/mbp/mbp_dt_tg.cpp
index b844843cd..1f970476e 100644
--- a/src/qe/mbp/mbp_dt_tg.cpp
+++ b/src/qe/mbp/mbp_dt_tg.cpp
@@ -166,15 +166,14 @@ struct mbp_dt_tg::impl {
                 // Only apply rm_accessor if the model confirms the argument
                 // has the constructor that this accessor belongs to.
                 // Otherwise we introduce a contradictory is-cons literal.
-                func_decl *cons =
+                func_decl *acc_cons =
                     m_dt_util.get_accessor_constructor(to_app(term)->get_decl());
-                func_decl *rec = m_dt_util.get_constructor_recognizer(cons);
+                func_decl *rec = m_dt_util.get_constructor_recognizer(acc_cons);
                 expr_ref is_rec(m.mk_app(rec, to_app(term)->get_arg(0)), m);
                 if (!m_mdl.is_true(is_rec)) {
-                    // Ground the argument so the accessor term becomes
-                    // constructively ground. This preserves any enclosing
-                    // literal (e.g., (not (is-nil (tl nil)))) as a guard in
-                    // the output, preventing an over-approximation.
+                    // The accessor's argument does not have the expected constructor in the model.
+                    // Add a guard literal and skip rm_accessor so we don't force a contradictory
+                    // constructor constraint on the argument.
                     expr_ref is(m.mk_not(is_rec), m);
                     m_tg.add_lit(is);
                     mark_seen(term);
diff --git a/src/test/mbp_qel.cpp b/src/test/mbp_qel.cpp
index 1ff262785..3e85d52bb 100644
--- a/src/test/mbp_qel.cpp
+++ b/src/test/mbp_qel.cpp
@@ -239,6 +239,7 @@ static void test_dt_multiple_vars() {
 
     VERIFY(!m.is_false(projected));
     VERIFY(mdl->is_true(projected));
+    VERIFY(vars.empty());
 
     std::cout << "  PASS\n\n";
 }