diff options
Diffstat (limited to 'test/regress/regress0/rels/rel_complex_0.cvc')
-rw-r--r-- | test/regress/regress0/rels/rel_complex_0.cvc | 31 |
1 files changed, 31 insertions, 0 deletions
diff --git a/test/regress/regress0/rels/rel_complex_0.cvc b/test/regress/regress0/rels/rel_complex_0.cvc new file mode 100644 index 000000000..dcb753973 --- /dev/null +++ b/test/regress/regress0/rels/rel_complex_0.cvc @@ -0,0 +1,31 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +r : SET OF IntPair; +z : SET OF INT; +f : INT; +g : INT; + +e : IntPair; +ASSERT e = (4, f); +ASSERT e IS_IN x; + +d : IntPair; +ASSERT d = (g,3); +ASSERT d IS_IN y; + + +ASSERT z = {f, g}; +ASSERT 0 = f - g; + + + +a : IntPair; +ASSERT a = (4,3); + +ASSERT r = (x JOIN y); + +ASSERT NOT (a IS_IN r); +CHECKSAT; |