diff options
Diffstat (limited to 'test/regress/regress0/rels/rel_complex_5.cvc')
-rw-r--r-- | test/regress/regress0/rels/rel_complex_5.cvc | 55 |
1 files changed, 0 insertions, 55 deletions
diff --git a/test/regress/regress0/rels/rel_complex_5.cvc b/test/regress/regress0/rels/rel_complex_5.cvc deleted file mode 100644 index d64817187..000000000 --- a/test/regress/regress0/rels/rel_complex_5.cvc +++ /dev/null @@ -1,55 +0,0 @@ -% EXPECT: unsat -OPTION "logic" "ALL_SUPPORTED"; -IntPair: TYPE = [INT, INT]; -IntTup: TYPE = [INT]; -x : SET OF IntPair; -y : SET OF IntPair; -z : SET OF IntPair; -r : SET OF IntPair; -w : SET OF IntPair; - - -f : IntPair; -ASSERT f = (3,1); -ASSERT f IS_IN x; - -g : IntPair; -ASSERT g = (1,3); -ASSERT g IS_IN y; - -h : IntPair; -ASSERT h = (3,5); -ASSERT h IS_IN x; -ASSERT h IS_IN y; - -ASSERT r = (x JOIN y); -a:IntTup; -ASSERT a = TUPLE(1); -e : IntPair; -ASSERT e = (1,1); - -ASSERT w = ({a} PRODUCT {a}); -ASSERT TRANSPOSE(w) <= y; - -ASSERT NOT (e IS_IN r); -ASSERT NOT(z = (x & y)); -ASSERT z = (x - y); -ASSERT x <= y; -ASSERT e IS_IN (r JOIN z); -ASSERT e IS_IN x; -ASSERT e IS_IN (x & y); -CHECKSAT TRUE; - - - - - - - - - - - - - - |