1 files changed, 21 insertions, 0 deletions
diff --git a/test/regress/regress1/rels/bv1-unit.cvc b/test/regress/regress1/rels/bv1-unit.cvc
new file mode 100644
index 000000000..970ebdc8c
--- /dev/null
+++ b/test/regress/regress1/rels/bv1-unit.cvc
@@ -0,0 +1,21 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+DATATYPE unit = u END;
+BvPair: TYPE = [BITVECTOR(1), unit, BITVECTOR(1)];
+x : SET OF BvPair;
+y : SET OF BvPair;
+
+a : BITVECTOR(1);
+b : BITVECTOR(1);
+c : BITVECTOR(1);
+d : BITVECTOR(1);
+e : BITVECTOR(1);
+
+ASSERT NOT ( b = c );
+
+ASSERT (a, u, b) IS_IN x;
+ASSERT (a, u, c) IS_IN x;
+ASSERT (d, u, a) IS_IN y;
+ASSERT NOT ( ( a, u, u, a ) IS_IN (x JOIN y));
+
+CHECKSAT;