From ae8e63d4be5fb217766ae7ef8a8dd37fd6b3f189 Mon Sep 17 00:00:00 2001 From: mudathirmahgoub Date: Wed, 14 Oct 2020 18:02:27 -0500 Subject: [PATCH] Fix issue #5269 (#5270) This PR fixes issue #5269 of unnecessary calling TheorySetsRels::areEqual in a product relation (which compares the rightmost element of the first child with the leftmost element in the second child). This may violate an assertion in TheorySetsRels::areEqual that the types of the 2 elements should be the same --- src/theory/sets/theory_sets_rels.cpp | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp index 617b458c9..ebb7f845d 100644 --- a/src/theory/sets/theory_sets_rels.cpp +++ b/src/theory/sets/theory_sets_rels.cpp @@ -1040,8 +1040,14 @@ void TheorySetsRels::check(Theory::Effort level) Node r2_lmost = RelsUtils::nthElementOfTuple( r2_rep_exps[j][0], 0 ); tuple_elements.push_back(tn.getDType()[0].getConstructor()); - if( (areEqual(r1_rmost, r2_lmost) && rel.getKind() == kind::JOIN) || - rel.getKind() == kind::PRODUCT ) { + Trace("rels-debug") << "[Theory::Rels] r1_rmost: " << r1_rmost + << " of type " << r1_rmost.getType() << std::endl; + Trace("rels-debug") << "[Theory::Rels] r2_lmost: " << r2_lmost + << " of type " << r2_lmost.getType() << std::endl; + + if (rel.getKind() == kind::PRODUCT + || (rel.getKind() == kind::JOIN && areEqual(r1_rmost, r2_lmost))) + { bool isProduct = rel.getKind() == kind::PRODUCT; unsigned int k = 0; unsigned int l = 1; -- 2.30.2