Fix issue with subtyping from set membership in models (#8282)

Fixes cvc5/cvc5-projects#480.

That benchmark now times out.

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index 7ed9dba51be08a83aaad2ceb39dfec657dbfa262..37215458fd3000a9bab686e978161c5450202fe7 100644 (file)
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -1137,10 +1137,10 @@ bool TheorySetsPrivate::collectModelValues(TheoryModel* m,
           TypeNode elementType = eqc.getType().getSetElementType();
           for (const std::pair<const Node, Node>& itmm : emems)
           {
-            Trace("sets-model")
-                << "m->getRepresentative(" << itmm.first
-                << ")= " << m->getRepresentative(itmm.first) << std::endl;
-            Node t = nm->mkSingleton(elementType, itmm.first);
+            // when we have y -> (set.member x S) where rep(x)=y, we use x
+            // in the model here. Using y may not be legal with respect to
+            // subtyping, since y may be real where x is an int.
+            Node t = nm->mkSingleton(elementType, itmm.second[0]);
             els.push_back(t);
           }
         }