fix unit test for new fair datatype enumeration

diff --git a/test/unit/theory/type_enumerator_white.h b/test/unit/theory/type_enumerator_white.h
index 3dcb2db8503bbd2b7de45f2bd803348d15c10852..d9963f78cd756fe228311d94283abff0a6e852b7 100644 (file)
--- a/test/unit/theory/type_enumerator_white.h
+++ b/test/unit/theory/type_enumerator_white.h
@@ -218,41 +218,27 @@ std::cout<<"here\n";
     Node cons = Node::fromExpr(DatatypeType(listColorsType.toType()).getDatatype().getConstructor("cons"));
     Node nil = d_nm->mkNode(APPLY_CONSTRUCTOR, DatatypeType(listColorsType.toType()).getDatatype().getConstructor("nil"));
     Node red = d_nm->mkNode(APPLY_CONSTRUCTOR, DatatypeType(colorsType.toType()).getDatatype().getConstructor("red"));
+    Node orange = d_nm->mkNode(APPLY_CONSTRUCTOR, DatatypeType(colorsType.toType()).getDatatype().getConstructor("orange"));
+    Node yellow = d_nm->mkNode(APPLY_CONSTRUCTOR, DatatypeType(colorsType.toType()).getDatatype().getConstructor("yellow"));
     TS_ASSERT_EQUALS(*te, nil);
     TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, nil));
     TS_ASSERT( ! te.isFinished() );
     TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red,
                             d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, nil)));
     TS_ASSERT( ! te.isFinished() );
-    TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red,
-                            d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red,
-                            d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, nil))));
+    TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, orange, nil));
     TS_ASSERT( ! te.isFinished() );
     TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red,
                             d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red,
-                            d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red,
-                            d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, nil)))));
+                            d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, nil))));
     TS_ASSERT( ! te.isFinished() );
-    TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red,
-                            d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red,
-                            d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red,
-                            d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red,
-                            d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, nil))))));
+    TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, orange,
+                            d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, nil)));
     TS_ASSERT( ! te.isFinished() );
-    TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red,
-                            d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red,
-                            d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red,
-                            d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red,
-                            d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red,
-                            d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, nil)))))));
+    TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, yellow, nil));
     TS_ASSERT( ! te.isFinished() );
     TS_ASSERT_EQUALS(*++te, d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red,
-                            d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red,
-                            d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red,
-                            d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red,
-                            d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red,
-                            d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red,
-                            d_nm->mkNode(APPLY_CONSTRUCTOR, cons, red, nil))))))));
+                            d_nm->mkNode(APPLY_CONSTRUCTOR, cons, orange, nil)));
     TS_ASSERT( ! te.isFinished() );
   }