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