Another minor fix for sets related to sharing + finite element types.

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 5550ee1b00fa370b89b926916641f1784564b9e7..7d2bbf3d12529e601ba6745780cb0ab84053be0c 100644 (file)
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -532,6 +532,9 @@ void TheorySetsPrivate::fullEffortCheck(){
       if( tn.isSet() ){
         isSet = true;
         d_set_eqc.push_back( eqc );
+        if( d_equalityEngine.isTriggerTerm(eqc, THEORY_SETS) ){
+          d_set_eqc_relevant[eqc] = true;
+        }
       }
       Trace("sets-eqc") << "[" << eqc << "] : ";
       eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine );

diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am
index eeced74306adb2fc1a809a805c4ef48e1c62f6bf..62f8665ec65bbd72d01ba0a489bee6e92bbdf1f9 100644 (file)
--- a/test/regress/regress0/sets/Makefile.am
+++ b/test/regress/regress0/sets/Makefile.am
@@ -72,7 +72,8 @@ TESTS =       \
        card-5.smt2 \
        card-6.smt2 \
        card-7.smt2 \
-       abt-min.smt2
+       abt-min.smt2 \
+       abt-te-exh.smt2
 
 
 EXTRA_DIST = $(TESTS)

diff --git a/test/regress/regress0/sets/abt-te-exh.smt2 b/test/regress/regress0/sets/abt-te-exh.smt2
new file mode 100644 (file)
index 0000000..f87429f
--- /dev/null
+++ b/test/regress/regress0/sets/abt-te-exh.smt2
@@ -0,0 +1,13 @@
+; COMMAND-LINE: --finite-model-find
+; EXPECT: sat
+(set-logic ALL)
+(declare-sort Atom 0)
+
+(declare-fun j ((Set Atom)) Atom)
+(declare-fun kk (Atom (Set Atom)) (Set Atom))
+(declare-fun n () (Set Atom))
+
+(assert (forall ((b Atom)) (= (as emptyset (Set Atom)) (kk (j (singleton b)) n))))
+
+(check-sat)
+