From d08ee0c791ef930386dccf3fa394b820d6bd11d2 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 10 Mar 2022 16:30:10 -0600 Subject: [PATCH] Fix issue with subtyping from set membership in models (#8282) Fixes cvc5/cvc5-projects#480. That benchmark now times out. --- src/theory/sets/theory_sets_private.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) 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); } } -- 2.30.2