diff options
Diffstat (limited to 'test/regress/regress0/rels/iden_1.cvc')
-rw-r--r-- | test/regress/regress0/rels/iden_1.cvc | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/test/regress/regress0/rels/iden_1.cvc b/test/regress/regress0/rels/iden_1.cvc new file mode 100644 index 000000000..f73700e88 --- /dev/null +++ b/test/regress/regress0/rels/iden_1.cvc @@ -0,0 +1,18 @@ +% EXPECT: unsat +OPTION "logic" "ALL_SUPPORTED"; +Atom:TYPE; +AtomPair: TYPE = [Atom, Atom]; +x : SET OF AtomPair; +t : SET OF [Atom]; +univ : SET OF [Atom]; + +a : Atom; +b : Atom; +c : Atom; +d : Atom; +ASSERT univ = UNIVERSE::SET OF [Atom]; +ASSERT (a, b) IS_IN x; +ASSERT (c, d) IS_IN x; +ASSERT NOT(a = b); +ASSERT IDEN(x JOIN univ) = x; +CHECKSAT; |