diff options
Diffstat (limited to 'test/regress/regress0/rels/join-eq-u-sat.cvc')
-rw-r--r-- | test/regress/regress0/rels/join-eq-u-sat.cvc | 22 |
1 files changed, 0 insertions, 22 deletions
diff --git a/test/regress/regress0/rels/join-eq-u-sat.cvc b/test/regress/regress0/rels/join-eq-u-sat.cvc deleted file mode 100644 index 1c45aa46b..000000000 --- a/test/regress/regress0/rels/join-eq-u-sat.cvc +++ /dev/null @@ -1,22 +0,0 @@ -% EXPECT: sat -OPTION "logic" "ALL"; -IntPair: TYPE = [INT, INT]; -x : SET OF IntPair; -y : SET OF IntPair; -DATATYPE unit = u END; -IntUPair: TYPE = [INT, unit]; -UIntPair: TYPE = [unit, INT]; -w : SET OF IntUPair; -z : SET OF UIntPair; - -ASSERT (x JOIN y) = (w JOIN z); - -ASSERT (0,1) IS_IN (x JOIN y); -ASSERT (0,u) IS_IN w; - -t : INT; -ASSERT t > 0 AND t < 3; - -ASSERT NOT (u, t ) IS_IN z; - -CHECKSAT; |