diff --git a/src/ast/finite_set_decl_plugin.cpp b/src/ast/finite_set_decl_plugin.cpp
index 3a3a96bce..e5b9ee61b 100644
--- a/src/ast/finite_set_decl_plugin.cpp
+++ b/src/ast/finite_set_decl_plugin.cpp
@@ -139,7 +139,9 @@ 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());
+            parameter param(element_sort);
+            range = m_manager->mk_sort(m_family_id, FINITE_SET_SORT, 1, &param);
         }        
         return mk_empty(range);
     case OP_FINITE_SET_SINGLETON:
diff --git a/src/ast/rewriter/finite_set_axioms.cpp b/src/ast/rewriter/finite_set_axioms.cpp
index 18d97637d..5a9c4c5d8 100644
--- a/src/ast/rewriter/finite_set_axioms.cpp
+++ b/src/ast/rewriter/finite_set_axioms.cpp
@@ -24,11 +24,15 @@ Revision History:
 #include "ast/rewriter/finite_set_axioms.h"
 
 // a ~ set.empty => not (x in a)
+// x is an element, generate axiom that x is not in any empty set of x's type
 void finite_set_axioms::in_empty_axiom(expr *x) {
-    expr_ref_vector clause(m);
-    sort* s = x->get_sort();
-    expr_ref empty_set(u.mk_empty(s), m);
+    // Generate: not (x in empty_set)
+    // where empty_set is the empty set of x's type
+    sort* elem_sort = x->get_sort();
+    expr_ref empty_set(u.mk_empty(elem_sort), m);
     expr_ref x_in_empty(u.mk_in(x, empty_set), m);
+    
+    expr_ref_vector clause(m);
     clause.push_back(m.mk_not(x_in_empty));
     m_add_clause(clause);
 }