Several bug fixes and other improvements.

14 files changed, 159 insertions, 133 deletions

diff --git a/src/aig/aig/aigCuts.c b/src/aig/aig/aigCuts.c
index 6de19484..1bcf69ce 100644
--- a/src/aig/aig/aigCuts.c
+++ b/src/aig/aig/aigCuts.c
@@ -56,9 +56,7 @@ Aig_ManCut_t * Aig_ManCutStart( Aig_Man_t * pMan, int nCutsMax, int nLeafMax, in
     p->fTruth   = fTruth;
     p->fVerbose = fVerbose;
     p->pAig     = pMan;
-    // allocate room for cuts and equivalent nodes
-    p->pCuts    = ABC_ALLOC( Aig_Cut_t *, Aig_ManObjNumMax(pMan) );
-    memset( p->pCuts, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(pMan) );
+    p->pCuts    = ABC_CALLOC( Aig_Cut_t *, Aig_ManObjNumMax(pMan) );
     // allocate memory manager
     p->nTruthWords = Aig_TruthWordNum(nLeafMax);
     p->nCutSize = sizeof(Aig_Cut_t) + sizeof(int) * nLeafMax + fTruth * sizeof(unsigned) * p->nTruthWords;
diff --git a/src/aig/kit/kitDsd.c b/src/aig/kit/kitDsd.c
index fbf92e48..f16d94d9 100644
--- a/src/aig/kit/kitDsd.c
+++ b/src/aig/kit/kitDsd.c
@@ -307,7 +307,8 @@ void Kit_DsdPrintExpanded( Kit_DsdNtk_t * pNtk )
 void Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars )
 {
     Kit_DsdNtk_t * pTemp, * pTemp2;
-    pTemp = Kit_DsdDecomposeMux( pTruth, nVars, 5 );
+//    pTemp = Kit_DsdDecomposeMux( pTruth, nVars, 5 );
+    pTemp = Kit_DsdDecomposeMux( pTruth, nVars, 8 );
 //    Kit_DsdPrintExpanded( pTemp );
     pTemp2 = Kit_DsdExpand( pTemp );
     Kit_DsdPrint( stdout, pTemp2 );
@@ -2090,7 +2091,7 @@ int Kit_DsdTestCofs( Kit_DsdNtk_t * pNtk, unsigned * pTruthInit )
 //        Extra_PrintBinary( stdout, pTruth, (1 << pNtk->nVars) ); 
         Extra_PrintHexadecimal( stdout, pTruth, pNtk->nVars ); 
         printf( "\n" );
-        Kit_DsdPrint( stdout, pNtk );
+        Kit_DsdPrint( stdout, pNtk ), printf( "\n" );
     }
     for ( i = 0; i < pNtk->nVars; i++ )
     {
@@ -2102,7 +2103,7 @@ int Kit_DsdTestCofs( Kit_DsdNtk_t * pNtk, unsigned * pTruthInit )
         if ( fVerbose )
         {
             printf( "Cof%d0: ", i );
-            Kit_DsdPrint( stdout, pNtk0 );
+            Kit_DsdPrint( stdout, pNtk0 ), printf( "\n" );
         }
 
         Kit_TruthCofactor1New( pCofs2[1], pTruth, pNtk->nVars, i );
@@ -2113,7 +2114,7 @@ int Kit_DsdTestCofs( Kit_DsdNtk_t * pNtk, unsigned * pTruthInit )
         if ( fVerbose )
         {
             printf( "Cof%d1: ", i );
-            Kit_DsdPrint( stdout, pNtk1 );
+            Kit_DsdPrint( stdout, pNtk1 ), printf( "\n" );
         }
 
 //        if ( Kit_DsdCheckVar4Dec2( pNtk0, pNtk1 ) )
@@ -2215,7 +2216,7 @@ void Kit_DsdTest( unsigned * pTruth, int nVars )
     pNtk = Kit_DsdExpand( pTemp = pNtk );
     Kit_DsdNtkFree( pTemp );
 
-    Kit_DsdPrint( stdout, pNtk );
+    Kit_DsdPrint( stdout, pNtk ), printf( "\n" );
 
 //    if ( Kit_DsdFindLargeBox(pNtk, Kit_DsdLit2Var(pNtk->Root)) )
 //        Kit_DsdTestCofs( pNtk, pTruth );
@@ -2277,7 +2278,7 @@ void Kit_DsdPrecompute4Vars()
             RetValue = Kit_DsdTestCofs( pNtk, &uTruth );
             printf( "\n" );
             printf( "%3d : Non-DSD function  %s  %s\n", i, Buffer + 2, RetValue? "implementable" : "" );
-            Kit_DsdPrint( stdout, pNtk );
+            Kit_DsdPrint( stdout, pNtk ), printf( "\n" );
 
             Counter1++;
             Counter2 += RetValue;
@@ -2456,9 +2457,9 @@ int Kit_DsdCofactoring( unsigned * pTruth, int nVars, int * pCofVars, int nLimit
                 Kit_DsdNtkFree( pTemp );
 
                 printf( "Cof%d%d: ", nStep+1, 2*i+0 );
-                Kit_DsdPrint( stdout, ppNtks[nStep+1][2*i+0] );
+                Kit_DsdPrint( stdout, ppNtks[nStep+1][2*i+0] ), printf( "\n" );
                 printf( "Cof%d%d: ", nStep+1, 2*i+1 );
-                Kit_DsdPrint( stdout, ppNtks[nStep+1][2*i+1] );
+                Kit_DsdPrint( stdout, ppNtks[nStep+1][2*i+1] ), printf( "\n" );
             }
         }
     }
@@ -2500,7 +2501,7 @@ void Kit_DsdPrintCofactors( unsigned * pTruth, int nVars, int nCofLevel, int fVe
     ppNtks[0] = Kit_DsdExpand( pTemp = ppNtks[0] );
     Kit_DsdNtkFree( pTemp );
     if ( fVerbose )
-        Kit_DsdPrint( stdout, ppNtks[0] );
+        Kit_DsdPrint( stdout, ppNtks[0] ), printf( "\n" );
     Kit_DsdNtkFree( ppNtks[0] );
 
     // allocate storage for cofactors
@@ -2551,7 +2552,7 @@ void Kit_DsdPrintCofactors( unsigned * pTruth, int nVars, int nCofLevel, int fVe
             if ( fVerbose )
             {
                 printf( "Cof%d%d: ", nSteps, i );
-                Kit_DsdPrint( stdout, ppNtks[i] );
+                Kit_DsdPrint( stdout, ppNtks[i] ), printf( "\n" );
             }
             // compute the largest non-decomp block
             nPrimeSizeCur  = Kit_DsdNonDsdSizeMax(ppNtks[i]);
@@ -2600,7 +2601,7 @@ void Kit_DsdPrintCofactors( unsigned * pTruth, int nVars, int nCofLevel, int fVe
             if ( fVerbose )
             {
                 printf( "Cof%d%d: ", nSteps, i );
-                Kit_DsdPrint( stdout, ppNtks[i] );
+                Kit_DsdPrint( stdout, ppNtks[i] ), printf( "\n" );
             }
             // compute the largest non-decomp block
             nPrimeSizeCur  = Kit_DsdNonDsdSizeMax(ppNtks[i]);
@@ -2651,7 +2652,7 @@ void Kit_DsdPrintCofactors( unsigned * pTruth, int nVars, int nCofLevel, int fVe
             if ( fVerbose )
             {
                 printf( "Cof%d%d: ", nSteps, i );
-                Kit_DsdPrint( stdout, ppNtks[i] );
+                Kit_DsdPrint( stdout, ppNtks[i] ), printf( "\n" );
             }
             // compute the largest non-decomp block
             nPrimeSizeCur  = Kit_DsdNonDsdSizeMax(ppNtks[i]);
@@ -2704,7 +2705,7 @@ void Kit_DsdPrintCofactors( unsigned * pTruth, int nVars, int nCofLevel, int fVe
             if ( fVerbose )
             {
                 printf( "Cof%d%d: ", nSteps, i );
-                Kit_DsdPrint( stdout, ppNtks[i] );
+                Kit_DsdPrint( stdout, ppNtks[i] ), printf( "\n" );
             }
             // compute the largest non-decomp block
             nPrimeSizeCur  = Kit_DsdNonDsdSizeMax(ppNtks[i]);
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 034df03f..fbd6b479 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -85,18 +85,16 @@ typedef enum {
 typedef enum { 
     ABC_OBJ_NONE = 0,   //  0:  unknown
     ABC_OBJ_CONST1,     //  1:  constant 1 node (AIG only)
-    ABC_OBJ_PIO,        //  2:  inout terminal
-    ABC_OBJ_PI,         //  3:  primary input terminal
-    ABC_OBJ_PO,         //  4:  primary output terminal
-    ABC_OBJ_BI,         //  5:  box input terminal
-    ABC_OBJ_BO,         //  6:  box output terminal
-    ABC_OBJ_ASSERT,     //  7:  assertion terminal
-    ABC_OBJ_NET,        //  8:  net
-    ABC_OBJ_NODE,       //  9:  node
-    ABC_OBJ_LATCH,      // 10:  latch
-    ABC_OBJ_WHITEBOX,   // 11:  box with known contents
-    ABC_OBJ_BLACKBOX,   // 12:  box with unknown contents
-    ABC_OBJ_NUMBER      // 13:  unused
+    ABC_OBJ_PI,         //  2:  primary input terminal
+    ABC_OBJ_PO,         //  3:  primary output terminal
+    ABC_OBJ_BI,         //  4:  box input terminal
+    ABC_OBJ_BO,         //  5:  box output terminal
+    ABC_OBJ_NET,        //  6:  net
+    ABC_OBJ_NODE,       //  7:  node
+    ABC_OBJ_LATCH,      //  8:  latch
+    ABC_OBJ_WHITEBOX,   //  9:  box with known contents
+    ABC_OBJ_BLACKBOX,   // 10:  box with unknown contents
+    ABC_OBJ_NUMBER      // 11:  unused
 } Abc_ObjType_t;
 
 // latch initial values
@@ -150,8 +148,8 @@ struct Abc_Obj_t_ // 12 words
     Vec_Int_t         vFanouts;      // the array of fanouts
     // miscellaneous
     union {
-    void *            pData;         // the network specific data (SOP, BDD, gate, equiv class, etc)
-    int iData;
+        void *        pData;         // the network specific data (SOP, BDD, gate, equiv class, etc)
+        int           iData;
     };
     Abc_Obj_t *       pNext;         // the next pointer in the hash table
     union {                          // temporary store for user's data
@@ -315,7 +313,6 @@ static inline Abc_Obj_t * Abc_NtkCreatePi( Abc_Ntk_t * pNtk )        { return Ab
 static inline Abc_Obj_t * Abc_NtkCreatePo( Abc_Ntk_t * pNtk )        { return Abc_NtkCreateObj( pNtk, ABC_OBJ_PO );         }
 static inline Abc_Obj_t * Abc_NtkCreateBi( Abc_Ntk_t * pNtk )        { return Abc_NtkCreateObj( pNtk, ABC_OBJ_BI );         }
 static inline Abc_Obj_t * Abc_NtkCreateBo( Abc_Ntk_t * pNtk )        { return Abc_NtkCreateObj( pNtk, ABC_OBJ_BO );         }
-static inline Abc_Obj_t * Abc_NtkCreateAssert( Abc_Ntk_t * pNtk )    { return Abc_NtkCreateObj( pNtk, ABC_OBJ_ASSERT );     }
 static inline Abc_Obj_t * Abc_NtkCreateNet( Abc_Ntk_t * pNtk )       { return Abc_NtkCreateObj( pNtk, ABC_OBJ_NET );        }
 static inline Abc_Obj_t * Abc_NtkCreateNode( Abc_Ntk_t * pNtk )      { return Abc_NtkCreateObj( pNtk, ABC_OBJ_NODE );       }
 static inline Abc_Obj_t * Abc_NtkCreateLatch( Abc_Ntk_t * pNtk )     { return Abc_NtkCreateObj( pNtk, ABC_OBJ_LATCH );      }
@@ -355,14 +352,13 @@ static inline void        Abc_ObjSetCopy( Abc_Obj_t * pObj, Abc_Obj_t * pCopy )
 static inline void        Abc_ObjSetData( Abc_Obj_t * pObj, void * pData )       { pObj->pData =  pData;    } 
 
 // checking the object type
-static inline int         Abc_ObjIsPio( Abc_Obj_t * pObj )           { return pObj->Type == ABC_OBJ_PIO;     }
+static inline int         Abc_ObjIsNone( Abc_Obj_t * pObj )          { return pObj->Type == ABC_OBJ_NONE;    }
 static inline int         Abc_ObjIsPi( Abc_Obj_t * pObj )            { return pObj->Type == ABC_OBJ_PI;      }
 static inline int         Abc_ObjIsPo( Abc_Obj_t * pObj )            { return pObj->Type == ABC_OBJ_PO;      }
 static inline int         Abc_ObjIsBi( Abc_Obj_t * pObj )            { return pObj->Type == ABC_OBJ_BI;      }
 static inline int         Abc_ObjIsBo( Abc_Obj_t * pObj )            { return pObj->Type == ABC_OBJ_BO;      }
-static inline int         Abc_ObjIsAssert( Abc_Obj_t * pObj )        { return pObj->Type == ABC_OBJ_ASSERT;  }
 static inline int         Abc_ObjIsCi( Abc_Obj_t * pObj )            { return pObj->Type == ABC_OBJ_PI || pObj->Type == ABC_OBJ_BO; }
-static inline int         Abc_ObjIsCo( Abc_Obj_t * pObj )            { return pObj->Type == ABC_OBJ_PO || pObj->Type == ABC_OBJ_BI || pObj->Type == ABC_OBJ_ASSERT; }
+static inline int         Abc_ObjIsCo( Abc_Obj_t * pObj )            { return pObj->Type == ABC_OBJ_PO || pObj->Type == ABC_OBJ_BI; }
 static inline int         Abc_ObjIsTerm( Abc_Obj_t * pObj )          { return Abc_ObjIsCi(pObj) || Abc_ObjIsCo(pObj); }
 static inline int         Abc_ObjIsNet( Abc_Obj_t * pObj )           { return pObj->Type == ABC_OBJ_NET;     }
 static inline int         Abc_ObjIsNode( Abc_Obj_t * pObj )          { return pObj->Type == ABC_OBJ_NODE;    }
@@ -824,6 +820,7 @@ extern ABC_DLL int                Abc_SopGetVarNum( char * pSop );
 extern ABC_DLL int                Abc_SopGetPhase( char * pSop );
 extern ABC_DLL int                Abc_SopGetIthCareLit( char * pSop, int i );
 extern ABC_DLL void               Abc_SopComplement( char * pSop );
+extern ABC_DLL void               Abc_SopComplementVar( char * pSop, int iVar );
 extern ABC_DLL int                Abc_SopIsComplement( char * pSop );
 extern ABC_DLL int                Abc_SopIsConst0( char * pSop );
 extern ABC_DLL int                Abc_SopIsConst1( char * pSop );
@@ -899,6 +896,10 @@ extern ABC_DLL Vec_Ptr_t *        Abc_NtkSaveCopy( Abc_Ntk_t * pNtk );
 extern ABC_DLL void               Abc_NtkLoadCopy( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCopies );
 extern ABC_DLL void               Abc_NtkCleanNext( Abc_Ntk_t * pNtk );
 extern ABC_DLL void               Abc_NtkCleanMarkA( Abc_Ntk_t * pNtk );
+extern ABC_DLL void               Abc_NtkCleanMarkB( Abc_Ntk_t * pNtk );
+extern ABC_DLL void               Abc_NtkCleanMarkC( Abc_Ntk_t * pNtk );
+extern ABC_DLL void               Abc_NtkCleanMarkAB( Abc_Ntk_t * pNtk );
+extern ABC_DLL void               Abc_NtkCleanMarkABC( Abc_Ntk_t * pNtk );
 extern ABC_DLL Abc_Obj_t *        Abc_NodeFindCoFanout( Abc_Obj_t * pNode );
 extern ABC_DLL Abc_Obj_t *        Abc_NodeFindNonCoFanout( Abc_Obj_t * pNode );
 extern ABC_DLL Abc_Obj_t *        Abc_NodeHasUniqueCoFanout( Abc_Obj_t * pNode );
diff --git a/src/base/abc/abcObj.c b/src/base/abc/abcObj.c
index 4c17962b..36fd6397 100644
--- a/src/base/abc/abcObj.c
+++ b/src/base/abc/abcObj.c
@@ -120,9 +120,6 @@ Abc_Obj_t * Abc_NtkCreateObj( Abc_Ntk_t * pNtk, Abc_ObjType_t Type )
         case ABC_OBJ_CONST1: 
             assert(0); 
             break;
-        case ABC_OBJ_PIO:    
-            assert(0); 
-            break;
         case ABC_OBJ_PI:     
             Vec_PtrPush( pNtk->vPis, pObj );
             Vec_PtrPush( pNtk->vCis, pObj );
@@ -196,9 +193,6 @@ void Abc_NtkDeleteObj( Abc_Obj_t * pObj )
         case ABC_OBJ_CONST1: 
             assert(0); 
             break;
-        case ABC_OBJ_PIO:    
-            assert(0); 
-            break;
         case ABC_OBJ_PI:     
             Vec_PtrRemove( pNtk->vPis, pObj );
             Vec_PtrRemove( pNtk->vCis, pObj );
diff --git a/src/base/abc/abcSop.c b/src/base/abc/abcSop.c
index 9e751f0a..e562a32a 100644
--- a/src/base/abc/abcSop.c
+++ b/src/base/abc/abcSop.c
@@ -628,6 +628,31 @@ void Abc_SopComplement( char * pSop )
   SeeAlso     []
 
 ***********************************************************************/
+void Abc_SopComplementVar( char * pSop, int iVar )
+{
+    char * pCube;
+    int nVars = Abc_SopGetVarNum(pSop);
+    assert( iVar < nVars );
+    Abc_SopForEachCube( pSop, nVars, pCube )
+    {
+        if ( pCube[iVar] == '0' )
+            pCube[iVar] = '1';
+        else if ( pCube[iVar] == '1' )
+            pCube[iVar] = '0';
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_SopIsComplement( char * pSop )
 {
     char * pCur;
diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c
index 38d800d0..e063a238 100644
--- a/src/base/abc/abcUtil.c
+++ b/src/base/abc/abcUtil.c
@@ -617,7 +617,7 @@ void Abc_NtkLoadCopy( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCopies )
 void Abc_NtkCleanNext( Abc_Ntk_t * pNtk )
 {
     Abc_Obj_t * pObj;
-    int i = 0;
+    int i;
     Abc_NtkForEachObj( pNtk, pObj, i )
         pObj->pNext = NULL;
 }
@@ -636,13 +636,89 @@ void Abc_NtkCleanNext( Abc_Ntk_t * pNtk )
 void Abc_NtkCleanMarkA( Abc_Ntk_t * pNtk )
 {
     Abc_Obj_t * pObj;
-    int i = 0;
+    int i;
     Abc_NtkForEachObj( pNtk, pObj, i )
         pObj->fMarkA = 0;
 }
 
 /**Function*************************************************************
 
+  Synopsis    [Cleans the copy field of all objects.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkCleanMarkB( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj;
+    int i;
+    Abc_NtkForEachObj( pNtk, pObj, i )
+        pObj->fMarkB = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Cleans the copy field of all objects.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkCleanMarkC( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj;
+    int i;
+    Abc_NtkForEachObj( pNtk, pObj, i )
+        pObj->fMarkC = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Cleans the copy field of all objects.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkCleanMarkAB( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj;
+    int i;
+    Abc_NtkForEachObj( pNtk, pObj, i )
+        pObj->fMarkA = pObj->fMarkB = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Cleans the copy field of all objects.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkCleanMarkABC( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj;
+    int i;
+    Abc_NtkForEachObj( pNtk, pObj, i )
+        pObj->fMarkA = pObj->fMarkB = pObj->fMarkC = 0;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Checks if the internal node has CO fanout.]
 
   Description []
@@ -928,9 +1004,18 @@ int Abc_NodeIsExorType( Abc_Obj_t * pNode )
     // if the children are not ANDs, this is not EXOR
     if ( Abc_ObjFaninNum(pNode0) != 2 || Abc_ObjFaninNum(pNode1) != 2 )
         return 0;
-    // otherwise, the node is EXOR iff its grand-children are the same
-    return (Abc_ObjFaninId0(pNode0) == Abc_ObjFaninId0(pNode1) || Abc_ObjFaninId0(pNode0) == Abc_ObjFaninId1(pNode1)) &&
-           (Abc_ObjFaninId1(pNode0) == Abc_ObjFaninId0(pNode1) || Abc_ObjFaninId1(pNode0) == Abc_ObjFaninId1(pNode1));
+    // this is AIG, which means the fanins should be ordered
+    assert( Abc_ObjFaninId0(pNode0) != Abc_ObjFaninId1(pNode1) || 
+            Abc_ObjFaninId0(pNode1) != Abc_ObjFaninId1(pNode0) );
+    // if grand children are not the same, this is not EXOR
+    if ( Abc_ObjFaninId0(pNode0) != Abc_ObjFaninId0(pNode1) ||
+         Abc_ObjFaninId1(pNode0) != Abc_ObjFaninId1(pNode1) )
+         return 0;
+    // finally, if the complemented edges are matched, this is not EXOR
+    if ( Abc_ObjFaninC0(pNode0) == Abc_ObjFaninC0(pNode1) || 
+         Abc_ObjFaninC1(pNode0) == Abc_ObjFaninC1(pNode1) )
+         return 0;
+    return 1;
 }
 
 /**Function*************************************************************
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 9d30fee8..566762e3 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -855,6 +855,10 @@ void Abc_End( Abc_Frame_t * pAbc )
     Abc_FrameClearDesign(); 
 
     {
+//        extern void Au_TabManPrint();
+//        Au_TabManPrint();
+    }
+    {
         extern void If_LutLibFree( If_Lib_t * pLutLib );
         if ( Abc_FrameGetGlobalFrame()->pAbc8Lib )
             If_LutLibFree( (If_Lib_t *)Abc_FrameGetGlobalFrame()->pAbc8Lib );
@@ -8666,8 +8670,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 
 /*
 {
-    extern Abc_Ntk_t * Abc_NtkBddDec( Abc_Ntk_t * pNtk, int fVerbose );
-    pNtkRes = Abc_NtkBddDec( pNtk, fVerbose );
+    extern Abc_Ntk_t * Au_ManDeriveFromAig( Abc_Ntk_t * pAig );
+    pNtkRes = Au_ManDeriveFromAig( pNtk );
     if ( pNtkRes == NULL )
     {
         Abc_Print( -1, "Command has failed.\n" );
@@ -8679,12 +8683,12 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 */
 
 //    Abc_NtkCheckAbsorb( pNtk, 4 );
-
+/*
     if ( fBmc )
         Abc_NktMffcServerTest( pNtk );
     else
         Abc_ResPartitionTest( pNtk );
-
+*/
 //    Abc_NtkHelloWorld( pNtk );
 //    Abc_NktMffcTest( pNtk );
 //    Abc_NktMffcServerTest( pNtk );
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 62f9b325..b28d3de4 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -231,7 +231,6 @@ Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
 {
     Vec_Ptr_t * vNodes;
     Abc_Ntk_t * pNtkNew;
-    Abc_Obj_t * pObjNew;
     Aig_Obj_t * pObj;
     int i;
     assert( pMan->nAsserts == 0 );
@@ -259,13 +258,6 @@ Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
         Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), (Abc_Obj_t *)Aig_ObjChild0Copy(pObj) );
     }
     // if there are assertions, add them
-    if ( pMan->nAsserts > 0 )
-        Aig_ManForEachAssert( pMan, pObj, i )
-        {
-            pObjNew = Abc_NtkCreateAssert(pNtkNew);
-            Abc_ObjAssignName( pObjNew, "assert_", Abc_ObjName(pObjNew) );
-            Abc_ObjAddFanin( pObjNew, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj) );
-        }
     if ( !Abc_NtkCheck( pNtkNew ) )
         fprintf( stdout, "Abc_NtkFromDar(): Network check has failed.\n" );
     return pNtkNew;
@@ -386,13 +378,6 @@ Abc_Ntk_t * Abc_NtkFromDarSeqSweep( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan )
         }
     }
     // if there are assertions, add them
-    if ( pMan->nAsserts > 0 )
-        Aig_ManForEachAssert( pMan, pObj, i )
-        {
-            pObjNew = Abc_NtkCreateAssert(pNtkNew);
-            Abc_ObjAssignName( pObjNew, "assert_", Abc_ObjName(pObjNew) );
-            Abc_ObjAddFanin( pObjNew, (Abc_Obj_t *)Aig_ObjChild0Copy(pObj) );
-        }
     if ( !Abc_NtkCheck( pNtkNew ) )
         fprintf( stdout, "Abc_NtkFromDar(): Network check has failed.\n" );
     return pNtkNew;
diff --git a/src/base/abci/abcMffc.c b/src/base/abci/abcMffc.c
index 1a1a81b2..0ffc6f1d 100644
--- a/src/base/abci/abcMffc.c
+++ b/src/base/abci/abcMffc.c
@@ -95,23 +95,11 @@ void Abc_MffcRef_rec( Abc_Obj_t * pNode )
 void Abc_MffcCollectNodes( Abc_Obj_t ** pNodes, int nNodes, Vec_Ptr_t * vNodes )
 {
     int i;
-/*
-    for ( i = 0; i < nNodes; i++ )
-    {
-        pNodes[i]->vFanouts.nSize += 100;
-//Abc_ObjPrint( stdout, pNodes[i] );
-    }
-//printf( "\n" );
-*/
-
     Vec_PtrClear( vNodes );
     for ( i = 0; i < nNodes; i++ )
         Abc_MffcDeref_rec( pNodes[i], vNodes );
     for ( i = 0; i < nNodes; i++ )
         Abc_MffcRef_rec( pNodes[i] );
-
-//    for ( i = 0; i < nNodes; i++ )
-//        pNodes[i]->vFanouts.nSize -= 100;
 }
 
 /**Function*************************************************************
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index 9f52d71f..bd5f986f 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -693,7 +693,8 @@ void Abc_NtkPrintMffc( FILE * pFile, Abc_Ntk_t * pNtk )
     int i;
     extern void Abc_NodeMffcConeSuppPrint( Abc_Obj_t * pNode );
     Abc_NtkForEachNode( pNtk, pNode, i )
-        Abc_NodeMffcConeSuppPrint( pNode );
+        if ( Abc_ObjFanoutNum(pNode) > 1 )
+            Abc_NodeMffcConeSuppPrint( pNode );
 }
 
 /**Function*************************************************************
@@ -1147,9 +1148,6 @@ void Abc_ObjPrint( FILE * pFile, Abc_Obj_t * pObj )
         case ABC_OBJ_CONST1: 
             fprintf( pFile, "Const1 " );  
             break;
-        case ABC_OBJ_PIO:    
-            fprintf( pFile, "PIO    " );  
-            break;
         case ABC_OBJ_PI:     
             fprintf( pFile, "PI     " );  
             break;
@@ -1162,9 +1160,6 @@ void Abc_ObjPrint( FILE * pFile, Abc_Obj_t * pObj )
         case ABC_OBJ_BO:     
             fprintf( pFile, "BO     " );  
             break;
-        case ABC_OBJ_ASSERT:     
-            fprintf( pFile, "Assert " );  
-            break;
         case ABC_OBJ_NET:  
             fprintf( pFile, "Net    " );  
             break;
diff --git a/src/base/io/ioAbc.h b/src/base/io/ioAbc.h
index 1c75db54..d5415384 100644
--- a/src/base/io/ioAbc.h
+++ b/src/base/io/ioAbc.h
@@ -138,7 +138,6 @@ extern void               Io_Write( Abc_Ntk_t * pNtk, char * pFileName, Io_FileT
 extern void               Io_WriteHie( Abc_Ntk_t * pNtk, char * pBaseName, char * pFileName );
 extern Abc_Obj_t *        Io_ReadCreatePi( Abc_Ntk_t * pNtk, char * pName );
 extern Abc_Obj_t *        Io_ReadCreatePo( Abc_Ntk_t * pNtk, char * pName );
-extern Abc_Obj_t *        Io_ReadCreateAssert( Abc_Ntk_t * pNtk, char * pName );
 extern Abc_Obj_t *        Io_ReadCreateLatch( Abc_Ntk_t * pNtk, char * pNetLI, char * pNetLO );
 extern Abc_Obj_t *        Io_ReadCreateResetLatch( Abc_Ntk_t * pNtk, int fBlifMv );
 extern Abc_Obj_t *        Io_ReadCreateResetMux( Abc_Ntk_t * pNtk, char * pResetLO, char * pDataLI, int fBlifMv );
diff --git a/src/base/io/ioReadBlif.c b/src/base/io/ioReadBlif.c
index 2093df3c..a1241354 100644
--- a/src/base/io/ioReadBlif.c
+++ b/src/base/io/ioReadBlif.c
@@ -59,7 +59,6 @@ static Abc_Ntk_t * Io_ReadBlifNetwork( Io_ReadBlif_t * p );
 static Abc_Ntk_t * Io_ReadBlifNetworkOne( Io_ReadBlif_t * p );
 static int Io_ReadBlifNetworkInputs( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens );
 static int Io_ReadBlifNetworkOutputs( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens );
-static int Io_ReadBlifNetworkAsserts( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens );
 static int Io_ReadBlifNetworkLatch( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens );
 static int Io_ReadBlifNetworkNames( Io_ReadBlif_t * p, Vec_Ptr_t ** pvTokens );
 static int Io_ReadBlifNetworkGate( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens );
@@ -266,8 +265,6 @@ Abc_Ntk_t * Io_ReadBlifNetworkOne( Io_ReadBlif_t * p )
             fStatus = Io_ReadBlifNetworkInputs( p, p->vTokens );
         else if ( !strcmp( pDirective, ".outputs" ) )
             fStatus = Io_ReadBlifNetworkOutputs( p, p->vTokens );
-        else if ( !strcmp( pDirective, ".asserts" ) )
-            fStatus = Io_ReadBlifNetworkAsserts( p, p->vTokens );
         else if ( !strcmp( pDirective, ".input_arrival" ) )
             fStatus = Io_ReadBlifNetworkInputArrival( p, p->vTokens );
         else if ( !strcmp( pDirective, ".default_input_arrival" ) )
@@ -354,25 +351,6 @@ int Io_ReadBlifNetworkOutputs( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens )
   SeeAlso     []
 
 ***********************************************************************/
-int Io_ReadBlifNetworkAsserts( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens )
-{
-    int i;
-    for ( i = 1; i < vTokens->nSize; i++ )
-        Io_ReadCreateAssert( p->pNtkCur, (char *)vTokens->pArray[i] );
-    return 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
 int Io_ReadBlifNetworkLatch( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens )
 { 
     Abc_Ntk_t * pNtk = p->pNtkCur;
diff --git a/src/base/io/ioUtil.c b/src/base/io/ioUtil.c
index a4dbf949..9a50c0c8 100644
--- a/src/base/io/ioUtil.c
+++ b/src/base/io/ioUtil.c
@@ -599,31 +599,6 @@ Abc_Obj_t * Io_ReadCreatePo( Abc_Ntk_t * pNtk, char * pName )
 
 /**Function*************************************************************
 
-  Synopsis    [Creates PO terminal and net.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Obj_t * Io_ReadCreateAssert( Abc_Ntk_t * pNtk, char * pName )
-{
-    Abc_Obj_t * pNet, * pTerm;
-    // get the PO net
-    pNet  = Abc_NtkFindNet( pNtk, pName );
-    if ( pNet && Abc_ObjFaninNum(pNet) == 0 )
-        printf( "Warning: Assert \"%s\" appears twice in the list.\n", pName );
-    pNet  = Abc_NtkFindOrCreateNet( pNtk, pName );
-    // add the PO node
-    pTerm = Abc_NtkCreateAssert( pNtk );
-    Abc_ObjAddFanin( pTerm, pNet );
-    return pTerm;
-}
-
-/**Function*************************************************************
-
   Synopsis    [Create a latch with the given input/output.]
 
   Description [By default, the latch value is unknown (ABC_INIT_NONE).]
diff --git a/src/base/io/ioWriteBlif.c b/src/base/io/ioWriteBlif.c
index 7233161b..cade2ea9 100644
--- a/src/base/io/ioWriteBlif.c
+++ b/src/base/io/ioWriteBlif.c
@@ -362,8 +362,6 @@ void Io_NtkWritePos( FILE * pFile, Abc_Ntk_t * pNtk, int fWriteLatches )
     {
         Abc_NtkForEachCo( pNtk, pTerm, i )
         {
-            if ( Abc_ObjIsAssert(pTerm) )
-                continue;
             pNet = Abc_ObjFanin0(pTerm);
             // get the line length after this name is written
             AddedLength = strlen(Abc_ObjName(pNet)) + 1;