From 031722bee8682005bd4c8700ef78b5f893fc48fe Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Wed, 26 Oct 2016 16:23:58 -0500
Subject: New implementation of sets+cardinality.  Merge Paul Meng's relation
 solver as extension of sets solver, add regressions.

---
 test/regress/regress0/rels/rel_tc_8.cvc | 10 ++++++++++
 1 file changed, 10 insertions(+)
 create mode 100644 test/regress/regress0/rels/rel_tc_8.cvc

(limited to 'test/regress/regress0/rels/rel_tc_8.cvc')

diff --git a/test/regress/regress0/rels/rel_tc_8.cvc b/test/regress/regress0/rels/rel_tc_8.cvc
new file mode 100644
index 000000000..9f5879c6d
--- /dev/null
+++ b/test/regress/regress0/rels/rel_tc_8.cvc
@@ -0,0 +1,10 @@
+% EXPECT: unsat
+OPTION "logic" "ALL_SUPPORTED";
+IntPair: TYPE = [INT, INT];
+x : SET OF IntPair;
+y : SET OF IntPair;
+
+ASSERT (2, 2) IS_IN (TCLOSURE x);
+ASSERT x = {}::SET OF IntPair;
+
+CHECKSAT;
-- 
cgit v1.2.3