1 files changed, 27 insertions, 0 deletions
diff --git a/test/regress/regress0/rels/rel_complex_1.cvc.smt2 b/test/regress/regress0/rels/rel_complex_1.cvc.smt2
new file mode 100644
index 000000000..823fb7ed1
--- /dev/null
+++ b/test/regress/regress0/rels/rel_complex_1.cvc.smt2
@@ -0,0 +1,27 @@
+; EXPECT: unsat
+(set-option :incremental false)
+(set-logic ALL)
+
+
+(declare-fun x () (Set (Tuple Int Int)))
+(declare-fun y () (Set (Tuple Int Int)))
+(declare-fun r () (Set (Tuple Int Int)))
+(declare-fun w () (Set (Tuple Int)))
+(declare-fun z () (Set (Tuple Int)))
+(declare-fun r2 () (Set (Tuple Int Int)))
+(declare-fun a () (Tuple Int Int))
+(assert (= a (mkTuple 3 1)))
+(assert (member a x))
+(declare-fun d () (Tuple Int Int))
+(assert (= d (mkTuple 1 3)))
+(assert (member d y))
+(declare-fun e () (Tuple Int Int))
+(assert (= e (mkTuple 4 3)))
+(assert (= r (join x y)))
+(assert (member (mkTuple 1) w))
+(assert (member (mkTuple 2) z))
+(assert (= r2 (product w z)))
+(assert (not (member e r)))
+(assert (subset r r2))
+(assert (not (member (mkTuple 3 3) r2)))
+(check-sat)