diff --git a/src/ast/finite_set_decl_plugin.cpp b/src/ast/finite_set_decl_plugin.cpp
index 3a3a96bce..3c8c14042 100644
--- a/src/ast/finite_set_decl_plugin.cpp
+++ b/src/ast/finite_set_decl_plugin.cpp
@@ -139,7 +139,10 @@ func_decl * finite_set_decl_plugin::mk_func_decl(decl_kind k, unsigned num_param
                 m_manager->raise_exception("set.empty requires one sort parameter");
                 return nullptr;
             }
-            range = to_sort(parameters[0].get_ast());
+            sort* element_sort = to_sort(parameters[0].get_ast());
+            // Create finite_set_sort from element_sort
+            parameter set_param(element_sort);
+            range = m_manager->mk_sort(m_family_id, FINITE_SET_SORT, 1, &set_param);
         }        
         return mk_empty(range);
     case OP_FINITE_SET_SINGLETON:
diff --git a/src/ast/rewriter/finite_set_rewriter.cpp b/src/ast/rewriter/finite_set_rewriter.cpp
index 9489c69dd..66399747c 100644
--- a/src/ast/rewriter/finite_set_rewriter.cpp
+++ b/src/ast/rewriter/finite_set_rewriter.cpp
@@ -64,14 +64,20 @@ br_status finite_set_rewriter::mk_intersect(unsigned num_args, expr * const * ar
 br_status finite_set_rewriter::mk_difference(expr * arg1, expr * arg2, expr_ref & result) {
     // set.difference(x, x) -> set.empty
     if (arg1 == arg2) {
-        // Get the element sort from the set sort
+        // Get the set sort
         sort* set_sort = arg1->get_sort();
         SASSERT(m_util.is_finite_set(set_sort));
         
-        // Get element sort - the parameter of the set sort
-        sort* elem_sort = to_sort(set_sort->get_parameter(0).get_ast());
-        result = m_util.mk_empty(elem_sort);
-        return BR_DONE;
+        // Create empty set with the same set sort
+        // We need to get the element sort from the parameters
+        if (set_sort->get_num_parameters() > 0) {
+            parameter const& param = set_sort->get_parameter(0);
+            if (param.is_ast() && is_sort(param.get_ast())) {
+                sort* elem_sort = to_sort(param.get_ast());
+                result = m_util.mk_empty(elem_sort);
+                return BR_DONE;
+            }
+        }
     }
     
     return BR_FAILED;
diff --git a/src/ast/rewriter/finite_set_rewriter.h b/src/ast/rewriter/finite_set_rewriter.h
index 261abe339..78203cc8e 100644
--- a/src/ast/rewriter/finite_set_rewriter.h
+++ b/src/ast/rewriter/finite_set_rewriter.h
@@ -26,6 +26,7 @@ where the signature is defined in finite_set_decl_plugin.h.
 
 #include "ast/finite_set_decl_plugin.h"
 #include "ast/rewriter/rewriter_types.h"
+#include "util/params.h"
 
 /**
    \brief Cheap rewrite rules for finite sets