diff --git a/src/ast/finite_set_decl_plugin.cpp b/src/ast/finite_set_decl_plugin.cpp
index 3a3a96bce..002887905 100644
--- a/src/ast/finite_set_decl_plugin.cpp
+++ b/src/ast/finite_set_decl_plugin.cpp
@@ -204,6 +204,9 @@ bool finite_set_decl_plugin::are_distinct(app* e1, app* e2) const {
         return true;
     if (r.is_singleton(e1) && r.is_empty(e2))
         return true;
+    if(r.is_singleton(e1) && r.is_singleton(e2))
+        return m_manager->are_distinct(e1, e2);
+    
     // TODO: could be extended to cases where we can prove the sets are different by containing one element
     // that the other doesn't contain. Such as (union (singleton a) (singleton b)) and (singleton c) where c is different from a, b.
     return false;