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

diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp
index 617b458c9b1075be77e3c92fd73650bfc30de03d..ebb7f845d3d9e2c2418496b46e049a936eec9423 100644 (file)
--- 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;