From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Thu, 25 Sep 2014 22:50:04 +0000 (-0400)
Subject: fix unit test for new fair datatype enumeration
X-Git-Tag: cvc5-1.0.0~6618
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d9533928947a207b795d90a97879b8212e99c50e;p=cvc5.git

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 3dcb2db85..d9963f78c 100644
--- 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() );
   }