1 files changed, 21 insertions, 0 deletions
diff --git a/test/regress/regress1/rels/join-eq-structure.cvc.smt2 b/test/regress/regress1/rels/join-eq-structure.cvc.smt2
new file mode 100644
index 000000000..5144ac4c2
--- /dev/null
+++ b/test/regress/regress1/rels/join-eq-structure.cvc.smt2
@@ -0,0 +1,21 @@
+; EXPECT: sat
+(set-option :incremental false)
+(set-logic ALL)
+
+(declare-fun x () (Set (Tuple Int Int)))
+(declare-fun y () (Set (Tuple Int Int)))
+(declare-datatypes ((unit 0)) (((u))))
+
+
+(declare-fun w () (Set (Tuple Int unit)))
+(declare-fun z () (Set (Tuple unit Int)))
+(assert (let ((_let_1 (join w z))) (let ((_let_2 (join x y))) (or (= _let_2 _let_1) (= _let_2 (transpose _let_1))))))
+(assert (member (mkTuple 0 1) (join x y)))
+(declare-fun t () Int)
+(assert (and (>= t 0) (<= t 1)))
+(declare-fun s () Int)
+(assert (and (>= s 0) (<= s 1)))
+(assert (= (+ s t) 1))
+(assert (member (mkTuple s u) w))
+(assert (not (member (mkTuple u t) z)))
+(check-sat)