diff --git a/src/smt/theory_finite_set.h b/src/smt/theory_finite_set.h
index b80377e49..0bb6f9ac5 100644
--- a/src/smt/theory_finite_set.h
+++ b/src/smt/theory_finite_set.h
@@ -94,8 +94,8 @@ namespace smt {
     class theory_finite_set : public theory {
         finite_set_util           u;
         finite_set_axioms         m_axioms;
-        obj_hashtable<expr>       m_membership_atoms;          // set of all 'x in S' atoms
-        obj_map<expr, ptr_vector<expr>>  m_set_to_elements;        // map from set S to elements x such that 'x in S' exists
+        obj_hashtable<expr>       m_membership_elements;          // set of all 'x' where there is an 'x in S' atom
+        ptr_vector<expr>          m_elements;                     // list of added x in m_membership_elements
         
     protected:
         // Override relevant methods from smt::theory
@@ -120,4 +120,4 @@ namespace smt {
         ~theory_finite_set() override {}
     };
 
-}  // namespace smt 
\ No newline at end of file
+}  // namespace smt