1 files changed, 22 insertions, 0 deletions
diff --git a/test/regress/regress0/rels/join-eq-u-sat.cvc b/test/regress/regress0/rels/join-eq-u-sat.cvc
new file mode 100644
index 000000000..0202cbb41
--- /dev/null
+++ b/test/regress/regress0/rels/join-eq-u-sat.cvc
@@ -0,0 +1,22 @@
+% EXPECT: sat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+DATATYPE unit = u END;
+IntUPair: TYPE = [INT, unit];
+UIntPair: TYPE = [unit, INT];
+w : SET OF IntUPair;
+z : SET OF UIntPair;
+
+ASSERT  (x JOIN y) =  (w JOIN z);
+
+ASSERT (0,1) IS_IN (x JOIN y);
+ASSERT (0,u) IS_IN w;
+
+t : INT;
+ASSERT t > 0 AND t < 3;
+
+ASSERT NOT (u, t ) IS_IN z;
+
+CHECKSAT;