From 7446112fbec0e67f4935ce57834d91d0d4ad5612 Mon Sep 17 00:00:00 2001 From: kper Date: Wed, 15 Oct 2025 14:35:57 +0200 Subject: [PATCH] Implement more cases for `finite_set_decl_plugin::are_distinct` (#7978) * Implement more cases for finite_set_decl_plugin::are_distinct * Adapted distinctive checks for finite sets --- src/ast/finite_set_decl_plugin.cpp | 3 +++ 1 file changed, 3 insertions(+) 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;