diff --git a/src/ast/simplifiers/elim_unconstrained.cpp b/src/ast/simplifiers/elim_unconstrained.cpp
index 120fe06729..c7742861b1 100644
--- a/src/ast/simplifiers/elim_unconstrained.cpp
+++ b/src/ast/simplifiers/elim_unconstrained.cpp
@@ -116,6 +116,7 @@ eliminate:
 #include "ast/ast_ll_pp.h"
 #include "ast/ast_pp.h"
 #include "ast/recfun_decl_plugin.h"
+#include "ast/polymorphism_util.h"
 #include "ast/simplifiers/elim_unconstrained.h"
 
 elim_unconstrained::elim_unconstrained(ast_manager& m, dependent_expr_state& fmls) :
@@ -425,8 +426,18 @@ void elim_unconstrained::update_model_trail(generic_model_converter& mc, vector<
 void elim_unconstrained::reduce() {
     if (!m_config.m_enabled)
         return;
-    if (m.has_type_vars())
-        return;
+    // has_type_vars() is a manager-wide flag that is set as soon as any type variable is
+    // created, including the ones used to define polymorphic signatures of builtin plugins
+    // (e.g. finite_set) that never occur in the asserted formulas. Only bail out when the
+    // formulas actually contain type-variable typed terms, which this simplifier cannot invert.
+    if (m.has_type_vars()) {
+        polymorphism::util u(m);
+        for (unsigned i : indices()) {
+            auto [f, p, d] = m_fmls[i]();
+            if (u.has_type_vars(f))
+                return;
+        }
+    }
     generic_model_converter_ref mc = alloc(generic_model_converter, m, "elim-unconstrained");
     m_inverter.set_model_converter(mc.get());
     m_created_compound = true;
diff --git a/src/tactic/core/elim_uncnstr_tactic.cpp b/src/tactic/core/elim_uncnstr_tactic.cpp
index a0eaeead94..7aecd4d505 100644
--- a/src/tactic/core/elim_uncnstr_tactic.cpp
+++ b/src/tactic/core/elim_uncnstr_tactic.cpp
@@ -27,6 +27,7 @@ Notes:
 #include "ast/datatype_decl_plugin.h"
 #include "ast/seq_decl_plugin.h"
 #include "ast/for_each_expr.h"
+#include "ast/polymorphism_util.h"
 #include "tactic/core/collect_occs.h"
 #include "ast/ast_smt2_pp.h"
 #include "ast/ast_ll_pp.h"
@@ -936,6 +937,21 @@ class elim_uncnstr_tactic : public tactic {
         m_rw = alloc(rw, m(), produce_proofs, m_vars, m_nonvars, m_disabled, m_mc.get(), m_max_memory, m_max_steps);            
     }
 
+    // The manager-wide has_type_vars() flag is a coarse over-approximation: it becomes
+    // true as soon as any type variable is created, including the type variables used to
+    // define the polymorphic signatures of builtin plugins (e.g. finite_set). Those never
+    // occur in the actual goal, so relying on the global flag needlessly disables this
+    // tactic. Check whether the goal itself contains type-variable typed terms instead.
+    bool goal_has_type_vars(goal_ref const & g) {
+        if (!m().has_type_vars())
+            return false;
+        polymorphism::util u(m());
+        for (unsigned i = 0; i < g->size(); ++i)
+            if (u.has_type_vars(g->form(i)))
+                return true;
+        return false;
+    }
+
     void run(goal_ref const & g, goal_ref_buffer & result) {
         bool produce_proofs = g->proofs_enabled();
         TRACE(goal, g->display(tout););
@@ -945,7 +961,7 @@ class elim_uncnstr_tactic : public tactic {
         collect_occs p;
         p(*g, m_vars);
         disable_quantified(g);
-        if (m_vars.empty() || recfun::util(m()).has_rec_defs() || m().has_type_vars()) {
+        if (m_vars.empty() || recfun::util(m()).has_rec_defs() || goal_has_type_vars(g)) {
             result.push_back(g.get());
             // did not increase depth since it didn't do anything.
             return;