diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index 3f578212d..0493f0516 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -833,7 +833,7 @@ void cmd_context::init_manager_core(bool new_manager) {
         register_plugin(symbol("fpa"),      alloc(fpa_decl_plugin), logic_has_fpa());
         register_plugin(symbol("datalog_relation"), alloc(datalog::dl_decl_plugin), !has_logic());
         register_plugin(symbol("specrels"), alloc(special_relations_decl_plugin), !has_logic());
-        register_plugin(symbol("finite_set"), alloc(finite_set_decl_plugin), !has_logic());
+        register_plugin(symbol("finite_set"), alloc(finite_set_decl_plugin), !has_logic() || smt_logics::logic_has_finite_sets(m_logic));
     }
     else {
         // the manager was created by an external module
@@ -850,7 +850,7 @@ void cmd_context::init_manager_core(bool new_manager) {
         load_plugin(symbol("seq"),      logic_has_seq(), fids);
         load_plugin(symbol("fpa"),      logic_has_fpa(), fids);
         load_plugin(symbol("pb"),       logic_has_pb(), fids);
-        load_plugin(symbol("finite_set"), !has_logic(), fids);
+        load_plugin(symbol("finite_set"), smt_logics::logic_has_finite_sets(m_logic) || !has_logic(), fids);
 
         for (family_id fid : fids) {
             decl_plugin * p = m_manager->get_plugin(fid);
diff --git a/src/solver/smt_logics.cpp b/src/solver/smt_logics.cpp
index 0942ed3fe..a02b90880 100644
--- a/src/solver/smt_logics.cpp
+++ b/src/solver/smt_logics.cpp
@@ -24,8 +24,8 @@ Revision History:
 bool smt_logics::supported_logic(symbol const & s) {
     return logic_has_uf(s) || logic_is_all(s) || logic_has_fd(s) || 
         logic_has_arith(s) || logic_has_bv(s) ||
-        logic_has_array(s) || logic_has_seq(s) || logic_has_str(s) ||
-        logic_has_horn(s) || logic_has_fpa(s) || logic_has_datatype(s);
+        logic_has_array(s) || logic_has_seq(s) || logic_has_str(s) || logic_has_horn(s) || logic_has_fpa(s) ||
+           logic_has_datatype(s) || logic_has_finite_sets(s);
 }
 
 bool smt_logics::logic_has_reals_only(symbol const& s) {
@@ -71,6 +71,13 @@ bool smt_logics::logic_has_bv(symbol const & s) {
         str == "HORN";
 }
 
+bool smt_logics::logic_has_finite_sets(symbol const &s) {
+    auto str = s.str();
+    return
+        str.find("FS") != std::string::npos ||
+        logic_is_all(s);
+}
+
 bool smt_logics::logic_has_array(symbol const & s) {
     auto str = s.str();
     return
diff --git a/src/solver/smt_logics.h b/src/solver/smt_logics.h
index 80bebabcc..9a32e5708 100644
--- a/src/solver/smt_logics.h
+++ b/src/solver/smt_logics.h
@@ -27,6 +27,7 @@ public:
     static bool logic_has_arith(symbol const & s);
     static bool logic_has_bv(symbol const & s);
     static bool logic_has_array(symbol const & s);
+    static bool logic_has_finite_sets(symbol const &s);
     static bool logic_has_seq(symbol const & s);
     static bool logic_has_str(symbol const & s);
     static bool logic_has_fpa(symbol const & s);