diff --git a/src/params/smt_params.cpp b/src/params/smt_params.cpp
index a64075204c..bc456208b2 100644
--- a/src/params/smt_params.cpp
+++ b/src/params/smt_params.cpp
@@ -26,6 +26,7 @@ void smt_params::updt_local_params(params_ref const & _p) {
     m_auto_config = p.auto_config() && gparams::get_value("auto_config") == "true"; // auto-config is not scoped by smt in gparams.
     m_random_seed = p.random_seed();
     m_relevancy_lvl = p.relevancy();
+    m_relevancy_watch_filter = p.relevancy_watch_filter();
     m_ematching   = p.ematching();
     m_ho_matching = p.ho_matching();
     m_induction   = p.induction();
diff --git a/src/params/smt_params.h b/src/params/smt_params.h
index 7b5efa9919..63482ba3d9 100644
--- a/src/params/smt_params.h
+++ b/src/params/smt_params.h
@@ -88,6 +88,7 @@ struct smt_params : public preprocessor_params,
     bool             m_eq_propagation = true;
     bool             m_binary_clause_opt = true;
     unsigned         m_relevancy_lvl = 2;
+    bool             m_relevancy_watch_filter = true;
     bool             m_relevancy_lemma = false;
     unsigned         m_random_seed = 0;
     double           m_random_var_freq = 0.01;
diff --git a/src/params/smt_params_helper.pyg b/src/params/smt_params_helper.pyg
index d3f164f3bb..da7cba3758 100644
--- a/src/params/smt_params_helper.pyg
+++ b/src/params/smt_params_helper.pyg
@@ -6,6 +6,7 @@ def_module_params(module_name='smt',
                           ('logic', SYMBOL, '', 'logic used to setup the SMT solver'),
                           ('random_seed', UINT, 0, 'random seed for the smt solver'),
                           ('relevancy', UINT, 2, 'relevancy propagation heuristic: 0 - disabled, 1 - relevancy is tracked by only affects quantifier instantiation, 2 - relevancy is tracked, and an atom is only asserted if it is relevant'),
+                          ('relevancy.watch_filter', BOOL, True, 'use a monotonic membership filter to skip the watch-list map probe for unwatched literals in the relevancy propagator (behavior-preserving performance toggle)'),
                           ('macro_finder', BOOL, False, 'try to find universally quantified formulas that can be viewed as macros'),
                           ('quasi_macros', BOOL, False, 'try to find universally quantified formulas that are quasi-macros'),
                           ('restricted_quasi_macros', BOOL, False, 'try to find universally quantified formulas that are restricted quasi-macros'),
diff --git a/src/smt/smt_relevancy.cpp b/src/smt/smt_relevancy.cpp
index fcaf604558..b4a65242fe 100644
--- a/src/smt/smt_relevancy.cpp
+++ b/src/smt/smt_relevancy.cpp
@@ -148,6 +148,10 @@ namespace smt {
         // obj_map pointer-hash probe for the common unwatched-literal case at the
         // assign_eh hotspot.
         uint_set                       m_is_watched[2];
+        // When false, the m_is_watched fast-path filter is disabled and
+        // get_watches() always probes m_watches (original behavior). Toggle via
+        // the smt.relevancy.watch_filter parameter for A/B performance testing.
+        bool                           m_use_watch_filter = true;
         struct eh_trail {
             enum class kind { POS_WATCH, NEG_WATCH, HANDLER };
             kind   m_kind;
@@ -166,7 +170,9 @@ namespace smt {
         bool                           m_propagating = false;
 
         relevancy_propagator_imp(context & ctx):
-            relevancy_propagator(ctx), m_relevant_exprs(ctx.get_manager()) {}
+            relevancy_propagator(ctx), m_relevant_exprs(ctx.get_manager()) {
+            m_use_watch_filter = ctx.get_fparams().m_relevancy_watch_filter;
+        }
 
         ~relevancy_propagator_imp() override {
             ast_manager & m = get_manager();
@@ -193,7 +199,7 @@ namespace smt {
 
         relevancy_ehs * get_watches(expr * n, bool val) {
             unsigned idx = val ? 1 : 0;
-            if (!m_is_watched[idx].contains(n->get_id()))
+            if (m_use_watch_filter && !m_is_watched[idx].contains(n->get_id()))
                 return nullptr;
             relevancy_ehs * r = nullptr;
             m_watches[idx].find(n, r);
@@ -207,7 +213,8 @@ namespace smt {
                 m_watches[idx].erase(n);
             else {
                 m_watches[idx].insert(n, ehs);
-                m_is_watched[idx].insert(n->get_id());
+                if (m_use_watch_filter)
+                    m_is_watched[idx].insert(n->get_id());
             }
         }