1 files changed, 0 insertions, 26 deletions
diff --git a/test/regress/regress1/rels/bv1p.cvc b/test/regress/regress1/rels/bv1p.cvc
deleted file mode 100644
index ed9fdce1f..000000000
--- a/test/regress/regress1/rels/bv1p.cvc
+++ /dev/null
@@ -1,26 +0,0 @@
-% COMMAND-LINE: --jh-rlv-order
-% EXPECT: unsat
-
-% note we require jh-rlv-order on this benchmark to avoid a proof failure currently (7/7/21)
-
-OPTION "logic" "ALL";
-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;