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