diff options
Diffstat (limited to 'test/regress/regress1/rels/set-strat.cvc')
-rw-r--r-- | test/regress/regress1/rels/set-strat.cvc | 24 |
1 files changed, 0 insertions, 24 deletions
diff --git a/test/regress/regress1/rels/set-strat.cvc b/test/regress/regress1/rels/set-strat.cvc deleted file mode 100644 index c56a2b16e..000000000 --- a/test/regress/regress1/rels/set-strat.cvc +++ /dev/null @@ -1,24 +0,0 @@ -% EXPECT: sat -OPTION "logic" "ALL"; -IntPair: TYPE = [ INT, INT]; -SetIntPair: TYPE = [ SET OF IntPair, SET OF IntPair ]; -x : SET OF IntPair; -y : SET OF IntPair; -w : SET OF IntPair; -z : SET OF SetIntPair; - -a : IntPair; -b : IntPair; - -ASSERT NOT a = b; - -ASSERT a IS_IN x; -ASSERT b IS_IN y; -ASSERT b IS_IN w; -ASSERT (x,y) IS_IN z; -ASSERT (w,x) IS_IN z; -ASSERT NOT ( (x,x) IS_IN (z JOIN z) ); - -ASSERT (x, { ( 0, 0 ) } ) IS_IN (z JOIN z); - -CHECKSAT; |