diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp
index d655316ed..926818d78 100644
--- a/src/smt/smt_setup.cpp
+++ b/src/smt/smt_setup.cpp
@@ -40,6 +40,7 @@ Revision History:
 #include "smt/theory_pb.h"
 #include "smt/theory_fpa.h"
 #include "smt/theory_polymorphism.h"
+#include "smt/theory_finite_set.h"
 
 namespace smt {
 
@@ -784,6 +785,10 @@ namespace smt {
         m_context.register_plugin(alloc(smt::theory_char, m_context));        
     }
 
+    void setup::setup_finite_set() {
+        m_context.register_plugin(alloc(smt::theory_finite_set, m_context));
+    }
+
     void setup::setup_special_relations() {
         m_context.register_plugin(alloc(smt::theory_special_relations, m_context, m_manager));
     }
@@ -807,6 +812,7 @@ namespace smt {
         setup_dl();
         setup_seq_str(st);
         setup_fpa();
+        setup_finite_set();
         setup_special_relations();
         setup_polymorphism();
         setup_relevancy(st);
diff --git a/src/smt/smt_setup.h b/src/smt/smt_setup.h
index 3d2bf47f3..897755ef7 100644
--- a/src/smt/smt_setup.h
+++ b/src/smt/smt_setup.h
@@ -102,6 +102,7 @@ namespace smt {
         void setup_seq_str(static_features const & st);
         void setup_seq();
         void setup_char();
+        void setup_finite_set();
         void setup_card();
         void setup_sls();
         void setup_i_arith();