diff options
Diffstat (limited to 'test/regress/regress1/rels/joinImg_1.cvc.smt2')
| -rw-r--r-- | test/regress/regress1/rels/joinImg_1.cvc.smt2 | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/test/regress/regress1/rels/joinImg_1.cvc.smt2 b/test/regress/regress1/rels/joinImg_1.cvc.smt2 new file mode 100644 index 000000000..3c5664d76 --- /dev/null +++ b/test/regress/regress1/rels/joinImg_1.cvc.smt2 @@ -0,0 +1,18 @@ +; EXPECT: unsat +(set-option :incremental false) +(set-logic ALL) +(set-option :sets-ext true) +(declare-sort Atom 0) +(declare-fun x () (Set (Tuple Atom Atom))) +(declare-fun y () (Set (Tuple Atom Atom))) +(declare-fun r () (Set (Tuple Atom Atom))) +(declare-fun t () (Set (Tuple Atom))) +(declare-fun a () Atom) +(declare-fun b () Atom) +(declare-fun c () Atom) +(declare-fun d () Atom) +(declare-fun e () Atom) +(assert (member (mkTuple a) (join_image x 2))) +(assert (= x (union (union (singleton (mkTuple b c)) (singleton (mkTuple d e))) (singleton (mkTuple c e))))) +(assert (not (= a b))) +(check-sat) |