Refactor regressions (#1581)

1 files changed, 26 insertions, 0 deletions

diff --git a/test/regress/regress1/rels/prod-mod-eq.cvc b/test/regress/regress1/rels/prod-mod-eq.cvc
new file mode 100644
index 000000000..96ef2ffba
--- /dev/null
+++ b/test/regress/regress1/rels/prod-mod-eq.cvc
@@ -0,0 +1,26 @@
+% EXPECT: sat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+IntPairPair: TYPE = [INT, INT, INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+z : SET OF IntPairPair;
+z1 : SET OF IntPair;
+w1 : SET OF IntPair;
+z2 : SET OF IntPair;
+w2 : SET OF IntPair;
+
+%ASSERT NOT (0,1,2,3) IS_IN (x PRODUCT y);
+
+ASSERT NOT( z = (x PRODUCT y) );
+
+ASSERT (0,1,2,3) IS_IN z;
+
+ASSERT (0,1) IS_IN z1;
+ASSERT (0,1) IS_IN z2;
+ASSERT (2,3) IS_IN w1;
+ASSERT (2,3) IS_IN w2;
+
+ASSERT ( x = z1 AND y = w1 ) OR ( x = z2 AND y = w2 );
+
+CHECKSAT;