fix for bug586

2 files changed, 28 insertions, 1 deletions

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 128783388..7500186dd 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -164,7 +164,8 @@ BUG_TESTS = \
 	bug576.smt2 \
 	bug576a.smt2 \
 	bug578.smt2 \
-	bug585.cvc
+	bug585.cvc \
+	bug586.cvc
 
 TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS)
 
diff --git a/test/regress/regress0/bug586.cvc b/test/regress/regress0/bug586.cvc
new file mode 100644
index 000000000..7f6f247ee
--- /dev/null
+++ b/test/regress/regress0/bug586.cvc
@@ -0,0 +1,26 @@
+% EXPECT: sat
+%%%
+%%% DATA TYPES DEFINITIONS
+%%%
+
+%%% the roles
+DATATYPE
+	role = r1 | r2 | r3
+	%%% adding two more roles ( | r4 | r5 ) to the type, but never referring to them make things work
+END;
+
+%%% structured datatypes
+roleSet: TYPE = SET OF role;
+roleGammaSet: TYPE = [# pos: roleSet, neg: roleSet #];
+delta: TYPE = ARRAY role OF roleGammaSet;
+
+emptyRoleSet : roleSet;
+ASSERT emptyRoleSet = {} :: SET OF role;
+
+d: delta;
+ASSERT d[r3].pos = {r1};
+ASSERT d[r2].pos = {r2,r3};
+ASSERT d[r2].neg = {r1};
+
+CHECKSAT;
+%COUNTEREXAMPLE;