1 files changed, 617 insertions, 0 deletions
diff --git a/test/regress/regress1/rels/rel_pressure_0.cvc b/test/regress/regress1/rels/rel_pressure_0.cvc
new file mode 100644
index 000000000..6cdf03600
--- /dev/null
+++ b/test/regress/regress1/rels/rel_pressure_0.cvc
@@ -0,0 +1,617 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+z : SET OF IntPair;
+r : SET OF IntPair;
+
+a11 : IntPair;
+ASSERT a11 = (1, 1);
+ASSERT a11 IS_IN x;
+a12 : IntPair;
+ASSERT a12 = (1, 2);
+ASSERT a12 IS_IN x;
+a13 : IntPair;
+ASSERT a13 = (1, 3);
+ASSERT a13 IS_IN x;
+a14 : IntPair;
+ASSERT a14 = (1, 4);
+ASSERT a14 IS_IN x;
+a15 : IntPair;
+ASSERT a15 = (1, 5);
+ASSERT a15 IS_IN x;
+a16 : IntPair;
+ASSERT a16 = (1, 6);
+ASSERT a16 IS_IN x;
+a17 : IntPair;
+ASSERT a17 = (1, 7);
+ASSERT a17 IS_IN x;
+a18 : IntPair;
+ASSERT a18 = (1, 8);
+ASSERT a18 IS_IN x;
+a19 : IntPair;
+ASSERT a19 = (1, 9);
+ASSERT a19 IS_IN x;
+a110 : IntPair;
+ASSERT a110 = (1, 10);
+ASSERT a110 IS_IN x;
+a21 : IntPair;
+ASSERT a21 = (2, 1);
+ASSERT a21 IS_IN x;
+a22 : IntPair;
+ASSERT a22 = (2, 2);
+ASSERT a22 IS_IN x;
+a23 : IntPair;
+ASSERT a23 = (2, 3);
+ASSERT a23 IS_IN x;
+a24 : IntPair;
+ASSERT a24 = (2, 4);
+ASSERT a24 IS_IN x;
+a25 : IntPair;
+ASSERT a25 = (2, 5);
+ASSERT a25 IS_IN x;
+a26 : IntPair;
+ASSERT a26 = (2, 6);
+ASSERT a26 IS_IN x;
+a27 : IntPair;
+ASSERT a27 = (2, 7);
+ASSERT a27 IS_IN x;
+a28 : IntPair;
+ASSERT a28 = (2, 8);
+ASSERT a28 IS_IN x;
+a29 : IntPair;
+ASSERT a29 = (2, 9);
+ASSERT a29 IS_IN x;
+a210 : IntPair;
+ASSERT a210 = (2, 10);
+ASSERT a210 IS_IN x;
+a31 : IntPair;
+ASSERT a31 = (3, 1);
+ASSERT a31 IS_IN x;
+a32 : IntPair;
+ASSERT a32 = (3, 2);
+ASSERT a32 IS_IN x;
+a33 : IntPair;
+ASSERT a33 = (3, 3);
+ASSERT a33 IS_IN x;
+a34 : IntPair;
+ASSERT a34 = (3, 4);
+ASSERT a34 IS_IN x;
+a35 : IntPair;
+ASSERT a35 = (3, 5);
+ASSERT a35 IS_IN x;
+a36 : IntPair;
+ASSERT a36 = (3, 6);
+ASSERT a36 IS_IN x;
+a37 : IntPair;
+ASSERT a37 = (3, 7);
+ASSERT a37 IS_IN x;
+a38 : IntPair;
+ASSERT a38 = (3, 8);
+ASSERT a38 IS_IN x;
+a39 : IntPair;
+ASSERT a39 = (3, 9);
+ASSERT a39 IS_IN x;
+a310 : IntPair;
+ASSERT a310 = (3, 10);
+ASSERT a310 IS_IN x;
+a41 : IntPair;
+ASSERT a41 = (4, 1);
+ASSERT a41 IS_IN x;
+a42 : IntPair;
+ASSERT a42 = (4, 2);
+ASSERT a42 IS_IN x;
+a43 : IntPair;
+ASSERT a43 = (4, 3);
+ASSERT a43 IS_IN x;
+a44 : IntPair;
+ASSERT a44 = (4, 4);
+ASSERT a44 IS_IN x;
+a45 : IntPair;
+ASSERT a45 = (4, 5);
+ASSERT a45 IS_IN x;
+a46 : IntPair;
+ASSERT a46 = (4, 6);
+ASSERT a46 IS_IN x;
+a47 : IntPair;
+ASSERT a47 = (4, 7);
+ASSERT a47 IS_IN x;
+a48 : IntPair;
+ASSERT a48 = (4, 8);
+ASSERT a48 IS_IN x;
+a49 : IntPair;
+ASSERT a49 = (4, 9);
+ASSERT a49 IS_IN x;
+a410 : IntPair;
+ASSERT a410 = (4, 10);
+ASSERT a410 IS_IN x;
+a51 : IntPair;
+ASSERT a51 = (5, 1);
+ASSERT a51 IS_IN x;
+a52 : IntPair;
+ASSERT a52 = (5, 2);
+ASSERT a52 IS_IN x;
+a53 : IntPair;
+ASSERT a53 = (5, 3);
+ASSERT a53 IS_IN x;
+a54 : IntPair;
+ASSERT a54 = (5, 4);
+ASSERT a54 IS_IN x;
+a55 : IntPair;
+ASSERT a55 = (5, 5);
+ASSERT a55 IS_IN x;
+a56 : IntPair;
+ASSERT a56 = (5, 6);
+ASSERT a56 IS_IN x;
+a57 : IntPair;
+ASSERT a57 = (5, 7);
+ASSERT a57 IS_IN x;
+a58 : IntPair;
+ASSERT a58 = (5, 8);
+ASSERT a58 IS_IN x;
+a59 : IntPair;
+ASSERT a59 = (5, 9);
+ASSERT a59 IS_IN x;
+a510 : IntPair;
+ASSERT a510 = (5, 10);
+ASSERT a510 IS_IN x;
+a61 : IntPair;
+ASSERT a61 = (6, 1);
+ASSERT a61 IS_IN x;
+a62 : IntPair;
+ASSERT a62 = (6, 2);
+ASSERT a62 IS_IN x;
+a63 : IntPair;
+ASSERT a63 = (6, 3);
+ASSERT a63 IS_IN x;
+a64 : IntPair;
+ASSERT a64 = (6, 4);
+ASSERT a64 IS_IN x;
+a65 : IntPair;
+ASSERT a65 = (6, 5);
+ASSERT a65 IS_IN x;
+a66 : IntPair;
+ASSERT a66 = (6, 6);
+ASSERT a66 IS_IN x;
+a67 : IntPair;
+ASSERT a67 = (6, 7);
+ASSERT a67 IS_IN x;
+a68 : IntPair;
+ASSERT a68 = (6, 8);
+ASSERT a68 IS_IN x;
+a69 : IntPair;
+ASSERT a69 = (6, 9);
+ASSERT a69 IS_IN x;
+a610 : IntPair;
+ASSERT a610 = (6, 10);
+ASSERT a610 IS_IN x;
+a71 : IntPair;
+ASSERT a71 = (7, 1);
+ASSERT a71 IS_IN x;
+a72 : IntPair;
+ASSERT a72 = (7, 2);
+ASSERT a72 IS_IN x;
+a73 : IntPair;
+ASSERT a73 = (7, 3);
+ASSERT a73 IS_IN x;
+a74 : IntPair;
+ASSERT a74 = (7, 4);
+ASSERT a74 IS_IN x;
+a75 : IntPair;
+ASSERT a75 = (7, 5);
+ASSERT a75 IS_IN x;
+a76 : IntPair;
+ASSERT a76 = (7, 6);
+ASSERT a76 IS_IN x;
+a77 : IntPair;
+ASSERT a77 = (7, 7);
+ASSERT a77 IS_IN x;
+a78 : IntPair;
+ASSERT a78 = (7, 8);
+ASSERT a78 IS_IN x;
+a79 : IntPair;
+ASSERT a79 = (7, 9);
+ASSERT a79 IS_IN x;
+a710 : IntPair;
+ASSERT a710 = (7, 10);
+ASSERT a710 IS_IN x;
+a81 : IntPair;
+ASSERT a81 = (8, 1);
+ASSERT a81 IS_IN x;
+a82 : IntPair;
+ASSERT a82 = (8, 2);
+ASSERT a82 IS_IN x;
+a83 : IntPair;
+ASSERT a83 = (8, 3);
+ASSERT a83 IS_IN x;
+a84 : IntPair;
+ASSERT a84 = (8, 4);
+ASSERT a84 IS_IN x;
+a85 : IntPair;
+ASSERT a85 = (8, 5);
+ASSERT a85 IS_IN x;
+a86 : IntPair;
+ASSERT a86 = (8, 6);
+ASSERT a86 IS_IN x;
+a87 : IntPair;
+ASSERT a87 = (8, 7);
+ASSERT a87 IS_IN x;
+a88 : IntPair;
+ASSERT a88 = (8, 8);
+ASSERT a88 IS_IN x;
+a89 : IntPair;
+ASSERT a89 = (8, 9);
+ASSERT a89 IS_IN x;
+a810 : IntPair;
+ASSERT a810 = (8, 10);
+ASSERT a810 IS_IN x;
+a91 : IntPair;
+ASSERT a91 = (9, 1);
+ASSERT a91 IS_IN x;
+a92 : IntPair;
+ASSERT a92 = (9, 2);
+ASSERT a92 IS_IN x;
+a93 : IntPair;
+ASSERT a93 = (9, 3);
+ASSERT a93 IS_IN x;
+a94 : IntPair;
+ASSERT a94 = (9, 4);
+ASSERT a94 IS_IN x;
+a95 : IntPair;
+ASSERT a95 = (9, 5);
+ASSERT a95 IS_IN x;
+a96 : IntPair;
+ASSERT a96 = (9, 6);
+ASSERT a96 IS_IN x;
+a97 : IntPair;
+ASSERT a97 = (9, 7);
+ASSERT a97 IS_IN x;
+a98 : IntPair;
+ASSERT a98 = (9, 8);
+ASSERT a98 IS_IN x;
+a99 : IntPair;
+ASSERT a99 = (9, 9);
+ASSERT a99 IS_IN x;
+a910 : IntPair;
+ASSERT a910 = (9, 10);
+ASSERT a910 IS_IN x;
+a101 : IntPair;
+ASSERT a101 = (10, 1);
+ASSERT a101 IS_IN x;
+a102 : IntPair;
+ASSERT a102 = (10, 2);
+ASSERT a102 IS_IN x;
+a103 : IntPair;
+ASSERT a103 = (10, 3);
+ASSERT a103 IS_IN x;
+a104 : IntPair;
+ASSERT a104 = (10, 4);
+ASSERT a104 IS_IN x;
+a105 : IntPair;
+ASSERT a105 = (10, 5);
+ASSERT a105 IS_IN x;
+a106 : IntPair;
+ASSERT a106 = (10, 6);
+ASSERT a106 IS_IN x;
+a107 : IntPair;
+ASSERT a107 = (10, 7);
+ASSERT a107 IS_IN x;
+a108 : IntPair;
+ASSERT a108 = (10, 8);
+ASSERT a108 IS_IN x;
+a109 : IntPair;
+ASSERT a109 = (10, 9);
+ASSERT a109 IS_IN x;
+a1010 : IntPair;
+ASSERT a1010 = (10, 10);
+ASSERT a1010 IS_IN x;
+b11 : IntPair;
+ASSERT b11 = (1, 1);
+ASSERT b11 IS_IN y;
+b12 : IntPair;
+ASSERT b12 = (1, 2);
+ASSERT b12 IS_IN y;
+b13 : IntPair;
+ASSERT b13 = (1, 3);
+ASSERT b13 IS_IN y;
+b14 : IntPair;
+ASSERT b14 = (1, 4);
+ASSERT b14 IS_IN y;
+b15 : IntPair;
+ASSERT b15 = (1, 5);
+ASSERT b15 IS_IN y;
+b16 : IntPair;
+ASSERT b16 = (1, 6);
+ASSERT b16 IS_IN y;
+b17 : IntPair;
+ASSERT b17 = (1, 7);
+ASSERT b17 IS_IN y;
+b18 : IntPair;
+ASSERT b18 = (1, 8);
+ASSERT b18 IS_IN y;
+b19 : IntPair;
+ASSERT b19 = (1, 9);
+ASSERT b19 IS_IN y;
+b110 : IntPair;
+ASSERT b110 = (1, 10);
+ASSERT b110 IS_IN y;
+b21 : IntPair;
+ASSERT b21 = (2, 1);
+ASSERT b21 IS_IN y;
+b22 : IntPair;
+ASSERT b22 = (2, 2);
+ASSERT b22 IS_IN y;
+b23 : IntPair;
+ASSERT b23 = (2, 3);
+ASSERT b23 IS_IN y;
+b24 : IntPair;
+ASSERT b24 = (2, 4);
+ASSERT b24 IS_IN y;
+b25 : IntPair;
+ASSERT b25 = (2, 5);
+ASSERT b25 IS_IN y;
+b26 : IntPair;
+ASSERT b26 = (2, 6);
+ASSERT b26 IS_IN y;
+b27 : IntPair;
+ASSERT b27 = (2, 7);
+ASSERT b27 IS_IN y;
+b28 : IntPair;
+ASSERT b28 = (2, 8);
+ASSERT b28 IS_IN y;
+b29 : IntPair;
+ASSERT b29 = (2, 9);
+ASSERT b29 IS_IN y;
+b210 : IntPair;
+ASSERT b210 = (2, 10);
+ASSERT b210 IS_IN y;
+b31 : IntPair;
+ASSERT b31 = (3, 1);
+ASSERT b31 IS_IN y;
+b32 : IntPair;
+ASSERT b32 = (3, 2);
+ASSERT b32 IS_IN y;
+b33 : IntPair;
+ASSERT b33 = (3, 3);
+ASSERT b33 IS_IN y;
+b34 : IntPair;
+ASSERT b34 = (3, 4);
+ASSERT b34 IS_IN y;
+b35 : IntPair;
+ASSERT b35 = (3, 5);
+ASSERT b35 IS_IN y;
+b36 : IntPair;
+ASSERT b36 = (3, 6);
+ASSERT b36 IS_IN y;
+b37 : IntPair;
+ASSERT b37 = (3, 7);
+ASSERT b37 IS_IN y;
+b38 : IntPair;
+ASSERT b38 = (3, 8);
+ASSERT b38 IS_IN y;
+b39 : IntPair;
+ASSERT b39 = (3, 9);
+ASSERT b39 IS_IN y;
+b310 : IntPair;
+ASSERT b310 = (3, 10);
+ASSERT b310 IS_IN y;
+b41 : IntPair;
+ASSERT b41 = (4, 1);
+ASSERT b41 IS_IN y;
+b42 : IntPair;
+ASSERT b42 = (4, 2);
+ASSERT b42 IS_IN y;
+b43 : IntPair;
+ASSERT b43 = (4, 3);
+ASSERT b43 IS_IN y;
+b44 : IntPair;
+ASSERT b44 = (4, 4);
+ASSERT b44 IS_IN y;
+b45 : IntPair;
+ASSERT b45 = (4, 5);
+ASSERT b45 IS_IN y;
+b46 : IntPair;
+ASSERT b46 = (4, 6);
+ASSERT b46 IS_IN y;
+b47 : IntPair;
+ASSERT b47 = (4, 7);
+ASSERT b47 IS_IN y;
+b48 : IntPair;
+ASSERT b48 = (4, 8);
+ASSERT b48 IS_IN y;
+b49 : IntPair;
+ASSERT b49 = (4, 9);
+ASSERT b49 IS_IN y;
+b410 : IntPair;
+ASSERT b410 = (4, 10);
+ASSERT b410 IS_IN y;
+b51 : IntPair;
+ASSERT b51 = (5, 1);
+ASSERT b51 IS_IN y;
+b52 : IntPair;
+ASSERT b52 = (5, 2);
+ASSERT b52 IS_IN y;
+b53 : IntPair;
+ASSERT b53 = (5, 3);
+ASSERT b53 IS_IN y;
+b54 : IntPair;
+ASSERT b54 = (5, 4);
+ASSERT b54 IS_IN y;
+b55 : IntPair;
+ASSERT b55 = (5, 5);
+ASSERT b55 IS_IN y;
+b56 : IntPair;
+ASSERT b56 = (5, 6);
+ASSERT b56 IS_IN y;
+b57 : IntPair;
+ASSERT b57 = (5, 7);
+ASSERT b57 IS_IN y;
+b58 : IntPair;
+ASSERT b58 = (5, 8);
+ASSERT b58 IS_IN y;
+b59 : IntPair;
+ASSERT b59 = (5, 9);
+ASSERT b59 IS_IN y;
+b510 : IntPair;
+ASSERT b510 = (5, 10);
+ASSERT b510 IS_IN y;
+b61 : IntPair;
+ASSERT b61 = (6, 1);
+ASSERT b61 IS_IN y;
+b62 : IntPair;
+ASSERT b62 = (6, 2);
+ASSERT b62 IS_IN y;
+b63 : IntPair;
+ASSERT b63 = (6, 3);
+ASSERT b63 IS_IN y;
+b64 : IntPair;
+ASSERT b64 = (6, 4);
+ASSERT b64 IS_IN y;
+b65 : IntPair;
+ASSERT b65 = (6, 5);
+ASSERT b65 IS_IN y;
+b66 : IntPair;
+ASSERT b66 = (6, 6);
+ASSERT b66 IS_IN y;
+b67 : IntPair;
+ASSERT b67 = (6, 7);
+ASSERT b67 IS_IN y;
+b68 : IntPair;
+ASSERT b68 = (6, 8);
+ASSERT b68 IS_IN y;
+b69 : IntPair;
+ASSERT b69 = (6, 9);
+ASSERT b69 IS_IN y;
+b610 : IntPair;
+ASSERT b610 = (6, 10);
+ASSERT b610 IS_IN y;
+b71 : IntPair;
+ASSERT b71 = (7, 1);
+ASSERT b71 IS_IN y;
+b72 : IntPair;
+ASSERT b72 = (7, 2);
+ASSERT b72 IS_IN y;
+b73 : IntPair;
+ASSERT b73 = (7, 3);
+ASSERT b73 IS_IN y;
+b74 : IntPair;
+ASSERT b74 = (7, 4);
+ASSERT b74 IS_IN y;
+b75 : IntPair;
+ASSERT b75 = (7, 5);
+ASSERT b75 IS_IN y;
+b76 : IntPair;
+ASSERT b76 = (7, 6);
+ASSERT b76 IS_IN y;
+b77 : IntPair;
+ASSERT b77 = (7, 7);
+ASSERT b77 IS_IN y;
+b78 : IntPair;
+ASSERT b78 = (7, 8);
+ASSERT b78 IS_IN y;
+b79 : IntPair;
+ASSERT b79 = (7, 9);
+ASSERT b79 IS_IN y;
+b710 : IntPair;
+ASSERT b710 = (7, 10);
+ASSERT b710 IS_IN y;
+b81 : IntPair;
+ASSERT b81 = (8, 1);
+ASSERT b81 IS_IN y;
+b82 : IntPair;
+ASSERT b82 = (8, 2);
+ASSERT b82 IS_IN y;
+b83 : IntPair;
+ASSERT b83 = (8, 3);
+ASSERT b83 IS_IN y;
+b84 : IntPair;
+ASSERT b84 = (8, 4);
+ASSERT b84 IS_IN y;
+b85 : IntPair;
+ASSERT b85 = (8, 5);
+ASSERT b85 IS_IN y;
+b86 : IntPair;
+ASSERT b86 = (8, 6);
+ASSERT b86 IS_IN y;
+b87 : IntPair;
+ASSERT b87 = (8, 7);
+ASSERT b87 IS_IN y;
+b88 : IntPair;
+ASSERT b88 = (8, 8);
+ASSERT b88 IS_IN y;
+b89 : IntPair;
+ASSERT b89 = (8, 9);
+ASSERT b89 IS_IN y;
+b810 : IntPair;
+ASSERT b810 = (8, 10);
+ASSERT b810 IS_IN y;
+b91 : IntPair;
+ASSERT b91 = (9, 1);
+ASSERT b91 IS_IN y;
+b92 : IntPair;
+ASSERT b92 = (9, 2);
+ASSERT b92 IS_IN y;
+b93 : IntPair;
+ASSERT b93 = (9, 3);
+ASSERT b93 IS_IN y;
+b94 : IntPair;
+ASSERT b94 = (9, 4);
+ASSERT b94 IS_IN y;
+b95 : IntPair;
+ASSERT b95 = (9, 5);
+ASSERT b95 IS_IN y;
+b96 : IntPair;
+ASSERT b96 = (9, 6);
+ASSERT b96 IS_IN y;
+b97 : IntPair;
+ASSERT b97 = (9, 7);
+ASSERT b97 IS_IN y;
+b98 : IntPair;
+ASSERT b98 = (9, 8);
+ASSERT b98 IS_IN y;
+b99 : IntPair;
+ASSERT b99 = (9, 9);
+ASSERT b99 IS_IN y;
+b910 : IntPair;
+ASSERT b910 = (9, 10);
+ASSERT b910 IS_IN y;
+b101 : IntPair;
+ASSERT b101 = (10, 1);
+ASSERT b101 IS_IN y;
+b102 : IntPair;
+ASSERT b102 = (10, 2);
+ASSERT b102 IS_IN y;
+b103 : IntPair;
+ASSERT b103 = (10, 3);
+ASSERT b103 IS_IN y;
+b104 : IntPair;
+ASSERT b104 = (10, 4);
+ASSERT b104 IS_IN y;
+b105 : IntPair;
+ASSERT b105 = (10, 5);
+ASSERT b105 IS_IN y;
+b106 : IntPair;
+ASSERT b106 = (10, 6);
+ASSERT b106 IS_IN y;
+b107 : IntPair;
+ASSERT b107 = (10, 7);
+ASSERT b107 IS_IN y;
+b108 : IntPair;
+ASSERT b108 = (10, 8);
+ASSERT b108 IS_IN y;
+b109 : IntPair;
+ASSERT b109 = (10, 9);
+ASSERT b109 IS_IN y;
+b1010 : IntPair;
+ASSERT b1010 = (10, 10);
+ASSERT b1010 IS_IN y;
+
+ASSERT (1, 9) IS_IN z;
+
+a : IntPair;
+ASSERT a = (9,1);
+ASSERT r = (((TRANSPOSE x) JOIN y) JOIN z);
+ASSERT NOT (a IS_IN (TRANSPOSE r));
+
+CHECKSAT;