Fixing the broken unit tests

diff --git a/test/unit/expr/attribute_white.h b/test/unit/expr/attribute_white.h
index 571be2789db6d852beb13952c0527452afb9f869..c325ed0a75235b83557e703994c9802207b3cbc4 100644 (file)
--- 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 0a49e6a3e5d994f01132bc8b8103fcf3d28787ea..c45740da981e5ed6b21809d31f60d9dc5f891d82 100644 (file)
--- 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);