From: Andrew Reynolds Date: Thu, 10 Mar 2022 22:30:10 +0000 (-0600) Subject: Fix issue with subtyping from set membership in models (#8282) X-Git-Tag: cvc5-1.0.0~284 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d08ee0c791ef930386dccf3fa394b820d6bd11d2;p=cvc5.git 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 7ed9dba51..37215458f 100644 --- 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& 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); } }