From: Dejan Jovanović <dejan.jovanovic@gmail.com>
Date: Thu, 25 Aug 2011 18:36:46 +0000 (+0000)
Subject: Fixing the broken unit tests
X-Git-Tag: cvc5-1.0.0~8490
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2faa78b68ca26f73e757f225f0786450e33c625f;p=cvc5.git

Fixing the broken unit tests
---

diff --git a/test/unit/expr/attribute_white.h b/test/unit/expr/attribute_white.h
index 571be2789..c325ed0a7 100644
--- a/test/unit/expr/attribute_white.h
+++ b/test/unit/expr/attribute_white.h
@@ -126,13 +126,9 @@ public:
     TS_ASSERT_DIFFERS(TestFlag4::s_id, TestFlag5::s_id);
 
     lastId = attr::LastAttributeId<bool, true>::s_id;
-    TS_ASSERT_LESS_THAN(theory::Asserted::s_id, lastId);
     TS_ASSERT_LESS_THAN(TestFlag1cd::s_id, lastId);
     TS_ASSERT_LESS_THAN(TestFlag2cd::s_id, lastId);
-    TS_ASSERT_DIFFERS(theory::Asserted::s_id, TestFlag1cd::s_id);
-    TS_ASSERT_DIFFERS(theory::Asserted::s_id, TestFlag2cd::s_id);
     TS_ASSERT_DIFFERS(TestFlag1cd::s_id, TestFlag2cd::s_id);
-    cout << "A: " << theory::Asserted::s_id << endl;
     cout << "1: " << TestFlag1cd::s_id << endl;
     cout << "2: " << TestFlag2cd::s_id << endl;
 
diff --git a/test/unit/prop/cnf_stream_black.h b/test/unit/prop/cnf_stream_black.h
index 0a49e6a3e..c45740da9 100644
--- a/test/unit/prop/cnf_stream_black.h
+++ b/test/unit/prop/cnf_stream_black.h
@@ -189,21 +189,22 @@ void testImplies() {
   TS_ASSERT( d_satSolver->addClauseCalled() );
 }
 
-void testIte() {
-  NodeManagerScope nms(d_nodeManager);
-  d_cnfStream->convertAndAssert(
-      d_nodeManager->mkNode(
-          kind::EQUAL,
-          d_nodeManager->mkNode(
-              kind::ITE,
-              d_nodeManager->mkVar(d_nodeManager->booleanType()),
-              d_nodeManager->mkVar(d_nodeManager->integerType()),
-              d_nodeManager->mkVar(d_nodeManager->integerType())
-          ),
-          d_nodeManager->mkVar(d_nodeManager->integerType())
-                            ), false, false);
-
-}
+// ITEs should be removed before going to CNF
+//void testIte() {
+//  NodeManagerScope nms(d_nodeManager);
+//  d_cnfStream->convertAndAssert(
+//      d_nodeManager->mkNode(
+//          kind::EQUAL,
+//          d_nodeManager->mkNode(
+//              kind::ITE,
+//              d_nodeManager->mkVar(d_nodeManager->booleanType()),
+//              d_nodeManager->mkVar(d_nodeManager->integerType()),
+//              d_nodeManager->mkVar(d_nodeManager->integerType())
+//          ),
+//          d_nodeManager->mkVar(d_nodeManager->integerType())
+//                            ), false, false);
+//
+//}
 
 void testNot() {
   NodeManagerScope nms(d_nodeManager);