Version abc60611

44 files changed, 2006 insertions, 785 deletions

diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 1fb57f67..29a95e46 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -53,7 +53,6 @@ typedef enum {
     ABC_NTK_LOGIC,      // 2:  network with PIs/POs, latches, and nodes
     ABC_NTK_STRASH,     // 3:  structurally hashed AIG (two input AND gates with c-attributes on edges)
     ABC_NTK_SEQ,        // 4:  sequential AIG (two input AND gates with c- and latch-attributes on edges)
-    ABC_NTK_BLACKBOX,   // 5:  black box about which nothing is known
     ABC_NTK_OTHER       // 6:  unused
 } Abc_NtkType_t;
 
@@ -89,8 +88,9 @@ typedef enum {
     ABC_OBJ_LATCH,      // 3:  latch
     ABC_OBJ_PI,         // 4:  primary input terminal
     ABC_OBJ_PO,         // 5:  primary output terminal
-    ABC_OBJ_BOX,        // 6:  abstract box
-    ABC_OBJ_OTHER       // 7:  unused
+    ABC_OBJ_ASSERT,     // 6:  assertion output
+    ABC_OBJ_BOX,        // 7:  box
+    ABC_OBJ_OTHER       // 8:  unused
 } Abc_ObjType_t;
 
 // latch initial values
@@ -107,9 +107,11 @@ typedef enum {
 ////////////////////////////////////////////////////////////////////////
 
 //typedef int                   bool;
+#ifndef __cplusplus
 #ifndef bool
 #define bool int
 #endif
+#endif
 
 typedef struct Abc_Obj_t_       Abc_Obj_t;
 typedef struct Abc_Ntk_t_       Abc_Ntk_t;
@@ -120,101 +122,82 @@ typedef struct Abc_Time_t_      Abc_Time_t;
 
 struct Abc_Time_t_
 {
-    float            Rise;
-    float            Fall;
-    float            Worst;
+    float             Rise;
+    float             Fall;
+    float             Worst;
 };
 
 struct Abc_Obj_t_ // 12 words
 {
     // high-level information
-    Abc_Ntk_t *      pNtk;          // the host network
-    int              Id;            // the object ID
+    Abc_Ntk_t *       pNtk;          // the host network
+    int               Id;            // the object ID
     // internal information
-    unsigned         Type    :  3;  // the object type
-    unsigned         fMarkA  :  1;  // the multipurpose mark
-    unsigned         fMarkB  :  1;  // the multipurpose mark
-    unsigned         fMarkC  :  1;  // the multipurpose mark
-    unsigned         fPhase  :  1;  // the flag to mark the phase of equivalent node
-    unsigned         fExor   :  1;  // marks AIG node that is a root of EXOR
-    unsigned         fCompl0 :  1;  // complemented attribute of the first fanin in the AIG
-    unsigned         fCompl1 :  1;  // complemented attribute of the second fanin in the AIG 
-    unsigned         TravId  : 10;  // the traversal ID (if changed, update Abc_NtkIncrementTravId)
-    unsigned         Level   : 12;  // the level of the node
+    unsigned          Type    :  3;  // the object type
+    unsigned          fMarkA  :  1;  // the multipurpose mark
+    unsigned          fMarkB  :  1;  // the multipurpose mark
+    unsigned          fMarkC  :  1;  // the multipurpose mark
+    unsigned          fPhase  :  1;  // the flag to mark the phase of equivalent node
+    unsigned          fExor   :  1;  // marks AIG node that is a root of EXOR
+    unsigned          fPersist:  1;  // marks the persistant AIG node
+    unsigned          fCompl0 :  1;  // complemented attribute of the first fanin in the AIG
+    unsigned          fCompl1 :  1;  // complemented attribute of the second fanin in the AIG 
+    unsigned          TravId  :  9;  // the traversal ID (if changed, update Abc_NtkIncrementTravId)
+    unsigned          Level   : 12;  // the level of the node
     // connectivity
-    Vec_Int_t        vFanins;       // the array of fanins
-    Vec_Int_t        vFanouts;      // the array of fanouts
+    Vec_Int_t         vFanins;       // the array of fanins
+    Vec_Int_t         vFanouts;      // the array of fanouts
     // miscellaneous
-    void *           pData;         // the network specific data (SOP, BDD, gate, equiv class, etc)
-    Abc_Obj_t *      pNext;         // the next pointer in the hash table
-    Abc_Obj_t *      pCopy;         // the copy of this object
+    void *            pData;         // the network specific data (SOP, BDD, gate, equiv class, etc)
+    Abc_Obj_t *       pNext;         // the next pointer in the hash table
+    Abc_Obj_t *       pCopy;         // the copy of this object
 };
 
 struct Abc_Ntk_t_ 
 {
     // general information 
-    Abc_NtkType_t    ntkType;       // type of the network
-    Abc_NtkFunc_t    ntkFunc;       // functionality of the network
-    char *           pName;         // the network name
-    char *           pSpec;         // the name of the spec file if present
-    int              Id;            // network ID
-    // name representation 
-//    stmm_table *     tName2Net;     // the table hashing net names into net pointer
-//    stmm_table *     tObj2Name;     // the table hashing PI/PO/latch pointers into names
+    Abc_NtkType_t     ntkType;       // type of the network
+    Abc_NtkFunc_t     ntkFunc;       // functionality of the network
+    char *            pName;         // the network name
+    char *            pSpec;         // the name of the spec file if present
+    int               Id;            // network ID
+    Nm_Man_t *        pManName;      // name manager (stores names of objects)
     // components of the network
-    Vec_Ptr_t *      vObjs;         // the array of all objects (net, nodes, latches)
-    Vec_Ptr_t *      vCis;          // the array of combinational inputs  (PIs followed by latches)
-    Vec_Ptr_t *      vCos;          // the array of combinational outputs (POs followed by latches)
-    Vec_Ptr_t *      vAsserts;      // the array of assertions
-    Vec_Ptr_t *      vLats;         // the array of latches (or the cutset in the sequential network)
-    Vec_Ptr_t *      vCutSet;       // the array of cutset nodes (used in the sequential AIG)
-    // the stats about the number of living objects
-    int              nObjs;         // the number of live objs
-    int              nNets;         // the number of live nets
-    int              nNodes;        // the number of live nodes
-    int              nBoxes;        // the number of live nodes
-    int              nLatches;      // the number of live latches
-    int              nPis;          // the number of primary inputs
-    int              nPos;          // the number of primary outputs
-    int              nAsserts;      // the number of assertion primary outputs
-    // the functionality manager 
-    void *           pManFunc;      // AIG manager, BDD manager, or memory manager for SOPs
-    // the global functions (BDDs)
-    void *           pManGlob;      // the BDD manager
-    Vec_Ptr_t *      vFuncsGlob;    // the BDDs of CO functions
-    // the timing manager (for mapped networks)
-    Abc_ManTime_t *  pManTime;      // stores arrival/required times for all nodes
-    // the cut manager (for AIGs)
-    void *           pManCut;       // stores information about the cuts computed for the nodes
-    // level information (for AIGs)
-    int              LevelMax;      // maximum number of levels
-    Vec_Int_t *      vLevelsR;      // level in the reverse topological order 
-    // support information
-    Vec_Ptr_t *      vSupps;
-    // the satisfiable assignment of the miter
-    int *            pModel;
-    // the external don't-care if given
-    Abc_Ntk_t *      pExdc;         // the EXDC network
-    // miscellaneous data members
-    unsigned         nTravIds;      // the unique traversal IDs of nodes
-    Vec_Ptr_t *      vPtrTemp;      // the temporary array
-    Vec_Int_t *      vIntTemp;      // the temporary array
-    Vec_Str_t *      vStrTemp;      // the temporary array
-    void *           pData;         // the temporary pointer
-    // name manager
-    Nm_Man_t *       pManName;
+    Vec_Ptr_t *       vObjs;         // the array of all objects (net, nodes, latches, etc)
+    Vec_Ptr_t *       vCis;          // the array of combinational inputs  (PIs, latches)
+    Vec_Ptr_t *       vCos;          // the array of combinational outputs (POs, asserts, latches)
+    Vec_Ptr_t *       vPis;          // the array of PIs
+    Vec_Ptr_t *       vPos;          // the array of POs
+    Vec_Ptr_t *       vLatches;      // the array of latches (or the cutset in the sequential network)
+    Vec_Ptr_t *       vAsserts;      // the array of assertions
+    Vec_Ptr_t *       vCutSet;       // the array of cutset nodes (used in the sequential AIG)
+    // the number of living objects
+    int               nObjs;         // the number of live objs
+    int               nNets;         // the number of live nets
+    int               nNodes;        // the number of live nodes
+    int               nBoxes;        // the number of live nodes
     // the backup network and the step number
-    Abc_Ntk_t *      pNetBackup;    // the pointer to the previous backup network
-    int              iStep;         // the generation number for the given network
-    // hierarchical design
-    stmm_table *     tName2Model;   // the table hashing names into network pointers (or NULL if no hierarchy)
-    Vec_Int_t *      pBlackBoxes;   // stores pairs (PI num, PO num) for each model, including the base model (or NULL if no hierarchy)
-    short            fHieVisited;   // flag to mark the visited network
-    short            fHiePath;      // flag to mark the network on the path
-    // memory management
-//    Extra_MmFlex_t * pMmNames;      // memory manager for net names
-    Extra_MmFixed_t* pMmObj;        // memory manager for objects
-    Extra_MmStep_t * pMmStep;       // memory manager for arrays
+    Abc_Ntk_t *       pNetBackup;    // the pointer to the previous backup network
+    int               iStep;         // the generation number for the given network
+    // hierarchy
+    stmm_table *      tName2Model;   // the table hashing names into network pointers (or NULL if no hierarchy)
+    Vec_Int_t *       pBlackBoxes;   // stores pairs (PI num, PO num) for each model, including the base model (or NULL if no hierarchy)
+    short             fHieVisited;   // flag to mark the visited network
+    short             fHiePath;      // flag to mark the network on the path
+    // miscellaneous data members
+    unsigned          nTravIds;      // the unique traversal IDs of nodes
+    Extra_MmFixed_t * pMmObj;        // memory manager for objects
+    Extra_MmStep_t *  pMmStep;       // memory manager for arrays
+    void *            pManFunc;      // functionality manager (AIG manager, BDD manager, or memory manager for SOPs)
+    void *            pManGlob;      // the global BDD manager
+    Vec_Ptr_t *       vFuncsGlob;    // the global BDDs of CO functions
+    Abc_ManTime_t *   pManTime;      // the timing manager (for mapped networks) stores arrival/required times for all nodes
+    void *            pManCut;       // the cut manager (for AIGs) stores information about the cuts computed for the nodes
+    int               LevelMax;      // maximum number of levels
+    Vec_Int_t *       vLevelsR;      // level in the reverse topological order (for AIGs)
+    Vec_Ptr_t *       vSupps;        // CO support information
+    int *             pModel;        // counter-example (for miters)
+    Abc_Ntk_t *       pExdc;         // the EXDC network (if given)
 };
 
 ////////////////////////////////////////////////////////////////////////
@@ -236,7 +219,6 @@ static inline bool        Abc_NtkIsNetlist( Abc_Ntk_t * pNtk )       { return pN
 static inline bool        Abc_NtkIsLogic( Abc_Ntk_t * pNtk )         { return pNtk->ntkType == ABC_NTK_LOGIC;   }
 static inline bool        Abc_NtkIsStrash( Abc_Ntk_t * pNtk )        { return pNtk->ntkType == ABC_NTK_STRASH;  }
 static inline bool        Abc_NtkIsSeq( Abc_Ntk_t * pNtk )           { return pNtk->ntkType == ABC_NTK_SEQ;     }
-static inline bool        Abc_NtkIsBlackbox( Abc_Ntk_t * pNtk )      { return pNtk->ntkType == ABC_NTK_BLACKBOX;}
 
 static inline bool        Abc_NtkHasSop( Abc_Ntk_t * pNtk )          { return pNtk->ntkFunc == ABC_FUNC_SOP;    }
 static inline bool        Abc_NtkHasBdd( Abc_Ntk_t * pNtk )          { return pNtk->ntkFunc == ABC_FUNC_BDD;    }
@@ -249,7 +231,7 @@ static inline bool        Abc_NtkIsMappedNetlist( Abc_Ntk_t * pNtk ) { return pN
 static inline bool        Abc_NtkIsSopLogic( Abc_Ntk_t * pNtk )      { return pNtk->ntkFunc == ABC_FUNC_SOP && pNtk->ntkType == ABC_NTK_LOGIC  ;  }
 static inline bool        Abc_NtkIsBddLogic( Abc_Ntk_t * pNtk )      { return pNtk->ntkFunc == ABC_FUNC_BDD && pNtk->ntkType == ABC_NTK_LOGIC  ;  }
 static inline bool        Abc_NtkIsMappedLogic( Abc_Ntk_t * pNtk )   { return pNtk->ntkFunc == ABC_FUNC_MAP && pNtk->ntkType == ABC_NTK_LOGIC  ;  }
-static inline bool        Abc_NtkIsComb( Abc_Ntk_t * pNtk )          { return pNtk->nLatches == 0;      }
+static inline bool        Abc_NtkIsComb( Abc_Ntk_t * pNtk )          { return Vec_PtrSize(pNtk->vLatches) == 0;   }
 
 // reading data members of the network
 static inline char *      Abc_NtkName( Abc_Ntk_t * pNtk )            { return pNtk->pName;            }
@@ -258,7 +240,7 @@ static inline int         Abc_NtkTravId( Abc_Ntk_t * pNtk )          { return pN
 static inline Abc_Ntk_t * Abc_NtkExdc( Abc_Ntk_t * pNtk )            { return pNtk->pExdc;            }
 static inline Abc_Ntk_t * Abc_NtkBackup( Abc_Ntk_t * pNtk )          { return pNtk->pNetBackup;       }
 static inline int         Abc_NtkStep  ( Abc_Ntk_t * pNtk )          { return pNtk->iStep;            }
-static inline Abc_Obj_t * Abc_NtkConst1( Abc_Ntk_t * pNtk )          { return pNtk->vObjs->pArray[0]; }
+static inline Abc_Obj_t * Abc_NtkConst1( Abc_Ntk_t * pNtk )          { return (Abc_Obj_t *)Vec_PtrEntry( pNtk->vObjs, 0 ); }
 
 // setting data members of the network
 static inline void        Abc_NtkSetName  ( Abc_Ntk_t * pNtk, char * pName )           { pNtk->pName      = pName;      } 
@@ -267,25 +249,27 @@ static inline void        Abc_NtkSetBackup( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNetBa
 static inline void        Abc_NtkSetStep  ( Abc_Ntk_t * pNtk, int iStep )              { pNtk->iStep      = iStep;      }
 
 // getting the number of objects 
-static inline int         Abc_NtkObjNumMax( Abc_Ntk_t * pNtk )       { return pNtk->vObjs->nSize;         }
-static inline int         Abc_NtkObjNum( Abc_Ntk_t * pNtk )          { return pNtk->nObjs;                }
-static inline int         Abc_NtkNetNum( Abc_Ntk_t * pNtk )          { return pNtk->nNets;                }
-static inline int         Abc_NtkNodeNum( Abc_Ntk_t * pNtk )         { return pNtk->nNodes;               }
-static inline int         Abc_NtkLatchNum( Abc_Ntk_t * pNtk )        { return pNtk->nLatches;             }
-static inline int         Abc_NtkCutSetNodeNum( Abc_Ntk_t * pNtk )   { return Vec_PtrSize(pNtk->vCutSet); }
-static inline int         Abc_NtkPiNum( Abc_Ntk_t * pNtk )           { return pNtk->nPis;                 }
-static inline int         Abc_NtkPoNum( Abc_Ntk_t * pNtk )           { return pNtk->nPos;                 }
-static inline int         Abc_NtkCiNum( Abc_Ntk_t * pNtk )           { return pNtk->vCis->nSize;          }
-static inline int         Abc_NtkCoNum( Abc_Ntk_t * pNtk )           { return pNtk->vCos->nSize;          }
+static inline int         Abc_NtkObjNumMax( Abc_Ntk_t * pNtk )       { return Vec_PtrSize(pNtk->vObjs);         }
+static inline int         Abc_NtkObjNum( Abc_Ntk_t * pNtk )          { return pNtk->nObjs;                      }
+static inline int         Abc_NtkNetNum( Abc_Ntk_t * pNtk )          { return pNtk->nNets;                      }
+static inline int         Abc_NtkNodeNum( Abc_Ntk_t * pNtk )         { return pNtk->nNodes;                     }
+static inline int         Abc_NtkLatchNum( Abc_Ntk_t * pNtk )        { return Vec_PtrSize(pNtk->vLatches);      }
+static inline int         Abc_NtkAssertNum( Abc_Ntk_t * pNtk )       { return Vec_PtrSize(pNtk->vAsserts);      }
+static inline int         Abc_NtkCutSetNodeNum( Abc_Ntk_t * pNtk )   { return Vec_PtrSize(pNtk->vCutSet);       }
+static inline int         Abc_NtkPiNum( Abc_Ntk_t * pNtk )           { return Vec_PtrSize(pNtk->vPis);          }
+static inline int         Abc_NtkPoNum( Abc_Ntk_t * pNtk )           { return Vec_PtrSize(pNtk->vPos);          }
+static inline int         Abc_NtkCiNum( Abc_Ntk_t * pNtk )           { return Vec_PtrSize(pNtk->vCis);          }
+static inline int         Abc_NtkCoNum( Abc_Ntk_t * pNtk )           { return Vec_PtrSize(pNtk->vCos);          }
 
 // reading objects
-static inline Abc_Obj_t * Abc_NtkObj( Abc_Ntk_t * pNtk, int i )      { return Vec_PtrEntry( pNtk->vObjs, i );   }
-static inline Abc_Obj_t * Abc_NtkLatch( Abc_Ntk_t * pNtk, int i )    { return Vec_PtrEntry( pNtk->vLats, i );   }
-static inline Abc_Obj_t * Abc_NtkCutSetNode( Abc_Ntk_t * pNtk, int i){ return Vec_PtrEntry( pNtk->vCutSet, i ); }
-static inline Abc_Obj_t * Abc_NtkCi( Abc_Ntk_t * pNtk, int i )       { return Vec_PtrEntry( pNtk->vCis, i );    }
-static inline Abc_Obj_t * Abc_NtkCo( Abc_Ntk_t * pNtk, int i )       { return Vec_PtrEntry( pNtk->vCos, i );    }
-static inline Abc_Obj_t * Abc_NtkPi( Abc_Ntk_t * pNtk, int i )       { assert( i < Abc_NtkPiNum(pNtk) ); return Abc_NtkCi( pNtk, i );  }
-static inline Abc_Obj_t * Abc_NtkPo( Abc_Ntk_t * pNtk, int i )       { assert( i < Abc_NtkPoNum(pNtk) ); return Abc_NtkCo( pNtk, i );  }
+static inline Abc_Obj_t * Abc_NtkObj( Abc_Ntk_t * pNtk, int i )      { return (Abc_Obj_t *)Vec_PtrEntry( pNtk->vObjs, i );   }
+static inline Abc_Obj_t * Abc_NtkLatch( Abc_Ntk_t * pNtk, int i )    { return (Abc_Obj_t *)Vec_PtrEntry( pNtk->vLatches, i );}
+static inline Abc_Obj_t * Abc_NtkAssert( Abc_Ntk_t * pNtk, int i )   { return (Abc_Obj_t *)Vec_PtrEntry( pNtk->vAsserts, i );}
+static inline Abc_Obj_t * Abc_NtkCutSetNode( Abc_Ntk_t * pNtk, int i){ return (Abc_Obj_t *)Vec_PtrEntry( pNtk->vCutSet, i ); }
+static inline Abc_Obj_t * Abc_NtkCi( Abc_Ntk_t * pNtk, int i )       { return (Abc_Obj_t *)Vec_PtrEntry( pNtk->vCis, i );    }
+static inline Abc_Obj_t * Abc_NtkCo( Abc_Ntk_t * pNtk, int i )       { return (Abc_Obj_t *)Vec_PtrEntry( pNtk->vCos, i );    }
+static inline Abc_Obj_t * Abc_NtkPi( Abc_Ntk_t * pNtk, int i )       { return (Abc_Obj_t *)Vec_PtrEntry( pNtk->vPis, i );    }
+static inline Abc_Obj_t * Abc_NtkPo( Abc_Ntk_t * pNtk, int i )       { return (Abc_Obj_t *)Vec_PtrEntry( pNtk->vPos, i );    }
 
 // reading data members of the object
 static inline unsigned    Abc_ObjType( Abc_Obj_t * pObj )            { return pObj->Type;               }
@@ -298,26 +282,27 @@ static inline Abc_Ntk_t * Abc_ObjNtk( Abc_Obj_t * pObj )             { return pO
 static inline void *      Abc_ObjData( Abc_Obj_t * pObj )            { return pObj->pData;              }
 
 // setting data members of the network
-static inline void        Abc_ObjSetCopy( Abc_Obj_t * pObj, Abc_Obj_t * pCopy )  { pObj->pCopy    =  pCopy;    } 
-static inline void        Abc_ObjSetData( Abc_Obj_t * pObj, void * pData )       { pObj->pData    =  pData;    } 
+static inline void        Abc_ObjSetCopy( Abc_Obj_t * pObj, Abc_Obj_t * pCopy )  { pObj->pCopy =  pCopy;    } 
+static inline void        Abc_ObjSetData( Abc_Obj_t * pObj, void * pData )       { pObj->pData =  pData;    } 
 
 // working with complemented attributes of objects
-static inline bool        Abc_ObjIsComplement( Abc_Obj_t * p )       { return (bool)(((unsigned)p) & 01);           }
-static inline Abc_Obj_t * Abc_ObjRegular( Abc_Obj_t * p )            { return (Abc_Obj_t *)((unsigned)(p) & ~01);  }
-static inline Abc_Obj_t * Abc_ObjNot( Abc_Obj_t * p )                { return (Abc_Obj_t *)((unsigned)(p) ^  01);  }
-static inline Abc_Obj_t * Abc_ObjNotCond( Abc_Obj_t * p, int c )     { return (Abc_Obj_t *)((unsigned)(p) ^ (c));  }
+static inline bool        Abc_ObjIsComplement( Abc_Obj_t * p )       { return (bool)((unsigned long)p & (unsigned long)01);             }
+static inline Abc_Obj_t * Abc_ObjRegular( Abc_Obj_t * p )            { return (Abc_Obj_t *)((unsigned long)p & ~(unsigned long)01);     }
+static inline Abc_Obj_t * Abc_ObjNot( Abc_Obj_t * p )                { return (Abc_Obj_t *)((unsigned long)p ^  (unsigned long)01);     }
+static inline Abc_Obj_t * Abc_ObjNotCond( Abc_Obj_t * p, int c )     { return (Abc_Obj_t *)((unsigned long)p ^  (unsigned long)(c!=0)); }
 
 // checking the object type
 static inline bool        Abc_ObjIsNode( Abc_Obj_t * pObj )          { return pObj->Type == ABC_OBJ_NODE;   }
 static inline bool        Abc_ObjIsBox( Abc_Obj_t * pObj )           { return pObj->Type == ABC_OBJ_BOX;    }
 static inline bool        Abc_ObjIsNet( Abc_Obj_t * pObj )           { return pObj->Type == ABC_OBJ_NET;    }
 static inline bool        Abc_ObjIsLatch( Abc_Obj_t * pObj )         { return pObj->Type == ABC_OBJ_LATCH;  }
+static inline bool        Abc_ObjIsAssert( Abc_Obj_t * pObj )        { return pObj->Type == ABC_OBJ_ASSERT; }
 static inline bool        Abc_ObjIsPi( Abc_Obj_t * pObj )            { return pObj->Type == ABC_OBJ_PI;     }
 static inline bool        Abc_ObjIsPo( Abc_Obj_t * pObj )            { return pObj->Type == ABC_OBJ_PO;     }
 static inline bool        Abc_ObjIsPio( Abc_Obj_t * pObj )           { return pObj->Type == ABC_OBJ_PI || pObj->Type == ABC_OBJ_PO;    }
 static inline bool        Abc_ObjIsCi( Abc_Obj_t * pObj )            { return pObj->Type == ABC_OBJ_PI || pObj->Type == ABC_OBJ_LATCH; }
-static inline bool        Abc_ObjIsCo( Abc_Obj_t * pObj )            { return pObj->Type == ABC_OBJ_PO || pObj->Type == ABC_OBJ_LATCH; }
-static inline bool        Abc_ObjIsCio( Abc_Obj_t * pObj )           { return pObj->Type == ABC_OBJ_PI || pObj->Type == ABC_OBJ_PO || pObj->Type == ABC_OBJ_LATCH; }
+static inline bool        Abc_ObjIsCo( Abc_Obj_t * pObj )            { return pObj->Type == ABC_OBJ_PO || pObj->Type == ABC_OBJ_LATCH || pObj->Type == ABC_OBJ_ASSERT; }
+static inline bool        Abc_ObjIsCio( Abc_Obj_t * pObj )           { return pObj->Type == ABC_OBJ_PI || pObj->Type == ABC_OBJ_PO || pObj->Type == ABC_OBJ_LATCH || pObj->Type == ABC_OBJ_ASSERT; }
 
 // working with fanin/fanout edges
 static inline int         Abc_ObjFaninNum( Abc_Obj_t * pObj )        { return pObj->vFanins.nSize;      }
@@ -331,8 +316,8 @@ static inline Abc_Obj_t * Abc_ObjFanout0( Abc_Obj_t * pObj )         { return (A
 static inline Abc_Obj_t * Abc_ObjFanin( Abc_Obj_t * pObj, int i )    { return (Abc_Obj_t *)pObj->pNtk->vObjs->pArray[ pObj->vFanins.pArray[i] ];   }
 static inline Abc_Obj_t * Abc_ObjFanin0( Abc_Obj_t * pObj )          { return (Abc_Obj_t *)pObj->pNtk->vObjs->pArray[ pObj->vFanins.pArray[0] ];   }
 static inline Abc_Obj_t * Abc_ObjFanin1( Abc_Obj_t * pObj )          { return (Abc_Obj_t *)pObj->pNtk->vObjs->pArray[ pObj->vFanins.pArray[1] ];   }
-static inline Abc_Obj_t * Abc_ObjFanin0Ntk( Abc_Obj_t * pObj )       { return (Abc_Obj_t *)(Abc_NtkIsNetlist(pObj->pNtk)? Abc_ObjFanin0(pObj)  : pObj); }
-static inline Abc_Obj_t * Abc_ObjFanout0Ntk( Abc_Obj_t * pObj )      { return (Abc_Obj_t *)(Abc_NtkIsNetlist(pObj->pNtk)? Abc_ObjFanout0(pObj) : pObj); }
+static inline Abc_Obj_t * Abc_ObjFanin0Ntk( Abc_Obj_t * pObj )       { return (Abc_NtkIsNetlist(pObj->pNtk)? Abc_ObjFanin0(pObj)  : pObj);  }
+static inline Abc_Obj_t * Abc_ObjFanout0Ntk( Abc_Obj_t * pObj )      { return (Abc_NtkIsNetlist(pObj->pNtk)? Abc_ObjFanout0(pObj) : pObj);  }
 static inline bool        Abc_ObjFaninC0( Abc_Obj_t * pObj )         { return pObj->fCompl0;                                                }
 static inline bool        Abc_ObjFaninC1( Abc_Obj_t * pObj )         { return pObj->fCompl1;                                                }
 static inline bool        Abc_ObjFaninC( Abc_Obj_t * pObj, int i )   { assert( i >=0 && i < 2 ); return i? pObj->fCompl1 : pObj->fCompl0;   }
@@ -354,6 +339,11 @@ extern        bool        Abc_NodeIsConst1( Abc_Obj_t * pNode );
 extern        bool        Abc_NodeIsBuf( Abc_Obj_t * pNode );    
 extern        bool        Abc_NodeIsInv( Abc_Obj_t * pNode );    
 
+// handling persistent nodes
+static inline int         Abc_NodeIsPersistant( Abc_Obj_t * pNode )    { assert( Abc_NodeIsAigAnd(pNode) ); return pNode->fPersist; } 
+static inline void        Abc_NodeSetPersistant( Abc_Obj_t * pNode )   { assert( Abc_NodeIsAigAnd(pNode) ); pNode->fPersist = 1;    } 
+static inline void        Abc_NodeClearPersistant( Abc_Obj_t * pNode ) { assert( Abc_NodeIsAigAnd(pNode) ); pNode->fPersist = 0;    } 
+
 // working with the traversal ID
 static inline void        Abc_NodeSetTravId( Abc_Obj_t * pNode, int TravId ) { pNode->TravId = TravId;                                    }
 static inline void        Abc_NodeSetTravIdCurrent( Abc_Obj_t * pNode )      { pNode->TravId = pNode->pNtk->nTravIds;                     }
@@ -386,28 +376,29 @@ static inline int         Abc_LatchInit( Abc_Obj_t * pLatch )        { assert(Ab
 #define Abc_NtkForEachNet( pNtk, pNet, i )                                                         \
     for ( i = 0; (i < Vec_PtrSize((pNtk)->vObjs)) && (((pNet) = Abc_NtkObj(pNtk, i)), 1); i++ )    \
         if ( (pNet) == NULL || !Abc_ObjIsNet(pNet) ) {} else
-#define Abc_NtkForEachLatch( pNtk, pLatch, i )                                                     \
-    for ( i = 0; (i < Vec_PtrSize((pNtk)->vLats)) && (((pLatch) = Abc_NtkLatch(pNtk, i)), 1); i++ )\
-        if ( (pLatch) == NULL ) {} else 
 #define Abc_NtkForEachNode( pNtk, pNode, i )                                                       \
     for ( i = 0; (i < Vec_PtrSize((pNtk)->vObjs)) && (((pNode) = Abc_NtkObj(pNtk, i)), 1); i++ )   \
         if ( (pNode) == NULL || !Abc_ObjIsNode(pNode) ) {} else
-#define Abc_NtkForEachBox( pNtk, pNode, i )                                                       \
-    for ( i = 0; (i < Vec_PtrSize((pNtk)->vObjs)) && (((pNode) = Abc_NtkObj(pNtk, i)), 1); i++ )   \
-        if ( (pNode) == NULL || !Abc_ObjIsBox(pNode) ) {} else
 #define Abc_AigForEachAnd( pNtk, pNode, i )                                                        \
     for ( i = 0; (i < Vec_PtrSize((pNtk)->vObjs)) && (((pNode) = Abc_NtkObj(pNtk, i)), 1); i++ )   \
         if ( (pNode) == NULL || !Abc_NodeIsAigAnd(pNode) ) {} else
+#define Abc_NtkForEachBox( pNtk, pNode, i )                                                       \
+    for ( i = 0; (i < Vec_PtrSize((pNtk)->vObjs)) && (((pNode) = Abc_NtkObj(pNtk, i)), 1); i++ )   \
+        if ( (pNode) == NULL || !Abc_ObjIsBox(pNode) ) {} else
 #define Abc_SeqForEachCutsetNode( pNtk, pNode, i )                                                 \
     for ( i = 0; (i < Abc_NtkCutSetNodeNum(pNtk)) && (((pNode) = Abc_NtkCutSetNode(pNtk, i)), 1); i++ )\
         if ( (pNode) == NULL ) {} else
 // inputs and outputs
 #define Abc_NtkForEachPi( pNtk, pPi, i )                                                           \
     for ( i = 0; (i < Abc_NtkPiNum(pNtk)) && (((pPi) = Abc_NtkPi(pNtk, i)), 1); i++ )
-#define Abc_NtkForEachPo( pNtk, pPo, i )                                                           \
-    for ( i = 0; (i < Abc_NtkPoNum(pNtk)) && (((pPo) = Abc_NtkPo(pNtk, i)), 1); i++ )
 #define Abc_NtkForEachCi( pNtk, pCi, i )                                                           \
     for ( i = 0; (i < Abc_NtkCiNum(pNtk)) && (((pCi) = Abc_NtkCi(pNtk, i)), 1); i++ )
+#define Abc_NtkForEachPo( pNtk, pPo, i )                                                           \
+    for ( i = 0; (i < Abc_NtkPoNum(pNtk)) && (((pPo) = Abc_NtkPo(pNtk, i)), 1); i++ )
+#define Abc_NtkForEachAssert( pNtk, pAssert, i )                                                   \
+    for ( i = 0; (i < Vec_PtrSize((pNtk)->vAsserts)) && (((pAssert) = Abc_NtkAssert(pNtk, i)), 1); i++ )
+#define Abc_NtkForEachLatch( pNtk, pLatch, i )                                                     \
+    for ( i = 0; (i < Vec_PtrSize((pNtk)->vLatches)) && (((pLatch) = Abc_NtkLatch(pNtk, i)), 1); i++ )
 #define Abc_NtkForEachCo( pNtk, pCo, i )                                                           \
     for ( i = 0; (i < Abc_NtkCoNum(pNtk)) && (((pCo) = Abc_NtkCo(pNtk, i)), 1); i++ )
 // fanin and fanouts
@@ -533,6 +524,7 @@ extern Abc_Obj_t *        Abc_NtkCreateBox( Abc_Ntk_t * pNtk );
 extern Abc_Obj_t *        Abc_NtkCreatePi( Abc_Ntk_t * pNtk );
 extern Abc_Obj_t *        Abc_NtkCreatePo( Abc_Ntk_t * pNtk );
 extern Abc_Obj_t *        Abc_NtkCreateLatch( Abc_Ntk_t * pNtk );
+extern Abc_Obj_t *        Abc_NtkCreateAssert( Abc_Ntk_t * pNtk );
 extern Abc_Obj_t *        Abc_NodeCreateConst0( Abc_Ntk_t * pNtk );
 extern Abc_Obj_t *        Abc_NodeCreateConst1( Abc_Ntk_t * pNtk );
 extern Abc_Obj_t *        Abc_NodeCreateInv( Abc_Ntk_t * pNtk, Abc_Obj_t * pFanin );
@@ -545,8 +537,6 @@ extern Abc_Obj_t *        Abc_ObjAlloc( Abc_Ntk_t * pNtk, Abc_ObjType_t Type );
 extern void               Abc_ObjRecycle( Abc_Obj_t * pObj );
 extern void               Abc_ObjAdd( Abc_Obj_t * pObj );
 /*=== abcNames.c ====================================================*/
-//extern char *             Abc_NtkRegisterName( Abc_Ntk_t * pNtk, char * pName );
-//extern char *             Abc_NtkRegisterNamePlus( Abc_Ntk_t * pNtk, char * pName, char * pSuffix );
 extern char *             Abc_ObjName( Abc_Obj_t * pNode );
 extern char *             Abc_ObjNameSuffix( Abc_Obj_t * pObj, char * pSuffix );
 extern char *             Abc_ObjNameDummy( char * pPrefix, int Num, int nDigits );
@@ -562,6 +552,7 @@ extern int                Abc_NodeCompareNames( Abc_Obj_t ** pp1, Abc_Obj_t ** p
 extern void               Abc_NtkOrderObjsByName( Abc_Ntk_t * pNtk, int fComb );
 extern void               Abc_NtkAddDummyPiNames( Abc_Ntk_t * pNtk );
 extern void               Abc_NtkAddDummyPoNames( Abc_Ntk_t * pNtk );
+extern void               Abc_NtkAddDummyAssertNames( Abc_Ntk_t * pNtk );
 extern void               Abc_NtkAddDummyLatchNames( Abc_Ntk_t * pNtk );
 extern void               Abc_NtkShortNames( Abc_Ntk_t * pNtk );
 /*=== abcNetlist.c ==========================================================*/
@@ -581,8 +572,6 @@ extern Abc_Ntk_t *        Abc_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func )
 extern Abc_Ntk_t *        Abc_NtkStartFrom( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func );
 extern Abc_Ntk_t *        Abc_NtkStartFromDual( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func );
 extern void               Abc_NtkFinalize( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
-extern void               Abc_NtkFinalizeRegular( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
-extern void               Abc_NtkFinalizeLatches( Abc_Ntk_t * pNtk );
 extern Abc_Ntk_t *        Abc_NtkStartRead( char * pName );
 extern void               Abc_NtkFinalizeRead( Abc_Ntk_t * pNtk );
 extern Abc_Ntk_t *        Abc_NtkDup( Abc_Ntk_t * pNtk );
@@ -627,7 +616,7 @@ extern int                Abc_NodeRef_rec( Abc_Obj_t * pNode );
 extern Abc_Ntk_t *        Abc_NtkRenode( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCnf, int fMulti, int fSimple, int fFactor );
 extern DdNode *           Abc_NtkRenodeDeriveBdd( DdManager * dd, Abc_Obj_t * pNodeOld, Vec_Ptr_t * vFaninsOld );
 /*=== abcSat.c ==========================================================*/
-extern int                Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nConfLimit, int nImpLimit, int fJFront, int fVerbose );
+extern int                Abc_NtkMiterSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fJFront, int fVerbose, sint64 * pNumConfs, sint64 * pNumInspects );
 extern solver *           Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk, int fJFront );
 /*=== abcSop.c ==========================================================*/
 extern char *             Abc_SopRegister( Extra_MmFlex_t * pMan, char * pName );
@@ -646,6 +635,7 @@ extern char *             Abc_SopCreateNxor( Extra_MmFlex_t * pMan, int nVars );
 extern char *             Abc_SopCreateMux( Extra_MmFlex_t * pMan );
 extern char *             Abc_SopCreateInv( Extra_MmFlex_t * pMan );
 extern char *             Abc_SopCreateBuf( Extra_MmFlex_t * pMan );
+extern char *             Abc_SopCreateFromTruth( Extra_MmFlex_t * pMan, int nVars, unsigned * pTruth );
 extern int                Abc_SopGetCubeNum( char * pSop );
 extern int                Abc_SopGetLitNum( char * pSop );
 extern int                Abc_SopGetVarNum( char * pSop );
@@ -709,6 +699,7 @@ extern int                Abc_HManPopulate( Abc_Ntk_t * pNtk );
 extern int                Abc_HManVerify( int NtkIdOld, int NtkIdNew );
 /*=== abcUtil.c ==========================================================*/
 extern void               Abc_NtkIncrementTravId( Abc_Ntk_t * pNtk );
+extern void               Abc_NtkOrderCisCos( Abc_Ntk_t * pNtk );
 extern int                Abc_NtkGetCubeNum( Abc_Ntk_t * pNtk );
 extern int                Abc_NtkGetLitNum( Abc_Ntk_t * pNtk );
 extern int                Abc_NtkGetLitFactNum( Abc_Ntk_t * pNtk );
diff --git a/src/base/abc/abcCheck.c b/src/base/abc/abcCheck.c
index 49e0e825..af6f4ef7 100644
--- a/src/base/abc/abcCheck.c
+++ b/src/base/abc/abcCheck.c
@@ -92,7 +92,8 @@ bool Abc_NtkDoCheck( Abc_Ntk_t * pNtk )
     Abc_Obj_t * pObj, * pNet, * pNode;
     int i;
 
-    if ( !Abc_NtkIsNetlist(pNtk) && !Abc_NtkIsLogic(pNtk) && !Abc_NtkIsStrash(pNtk) && !Abc_NtkIsSeq(pNtk) && !Abc_NtkIsBlackbox(pNtk) )
+    // check network types
+    if ( !Abc_NtkIsNetlist(pNtk) && !Abc_NtkIsLogic(pNtk) && !Abc_NtkIsStrash(pNtk) && !Abc_NtkIsSeq(pNtk) )
     {
         fprintf( stdout, "NetworkCheck: Unknown network type.\n" );
         return 0;
@@ -111,6 +112,22 @@ bool Abc_NtkDoCheck( Abc_Ntk_t * pNtk )
         }
     }
 
+    // check CI/CO numbers
+    if ( Abc_NtkPiNum(pNtk) + Abc_NtkLatchNum(pNtk) != Abc_NtkCiNum(pNtk) )
+    {
+        fprintf( stdout, "NetworkCheck: Number of CIs does not match number of PIs and latches.\n" );
+        fprintf( stdout, "One possible reason is that latches are added twice:\n" );
+        fprintf( stdout, "in procedure Abc_ObjAdd() and in the user's code.\n" );
+        return 0;
+    }
+    if ( Abc_NtkPoNum(pNtk) + Abc_NtkAssertNum(pNtk) + Abc_NtkLatchNum(pNtk) != Abc_NtkCoNum(pNtk) )
+    {
+        fprintf( stdout, "NetworkCheck: Number of COs does not match number of POs, asserts, and latches.\n" );
+        fprintf( stdout, "One possible reason is that latches are added twice:\n" );
+        fprintf( stdout, "in procedure Abc_ObjAdd() and in the user's code.\n" );
+        return 0;
+    }
+
     // check the names
     if ( !Abc_NtkCheckNames( pNtk ) )
         return 0;
@@ -181,14 +198,7 @@ bool Abc_NtkDoCheck( Abc_Ntk_t * pNtk )
 
     // check the EXDC network if present
     if ( pNtk->pExdc )
-    {
-//        if ( pNtk->Type != pNtk->pExdc->Type )
-//        {
-//            fprintf( stdout, "NetworkCheck: Network and its EXDC have different types.\n" );
-//            return 0;
-//        }
-        return Abc_NtkCheck( pNtk->pExdc );
-    }
+        Abc_NtkCheck( pNtk->pExdc );
 
     // check the hierarchy
     if ( Abc_NtkIsNetlist(pNtk) && pNtk->tName2Model )
@@ -226,76 +236,60 @@ bool Abc_NtkDoCheck( Abc_Ntk_t * pNtk )
 ***********************************************************************/
 bool Abc_NtkCheckNames( Abc_Ntk_t * pNtk )
 {
-    stmm_generator * gen;
-    Abc_Obj_t * pNet, * pNet2, * pObj;
+    Abc_Obj_t * pObj;
+    Vec_Int_t * vNameIds;
     char * pName;
-    int i;
+    int i, NameId;
 
-    if ( Abc_NtkIsNetlist(pNtk) )
+    // check that each CI/CO has a name
+    Abc_NtkForEachCi( pNtk, pObj, i )
     {
-/*
-        // check that the nets in the table are also in the network
-        stmm_foreach_item( pNtk->tName2Net, gen, &pName, (char**)&pNet )
+        pObj = Abc_ObjFanout0Ntk(pObj);
+        if ( Nm_ManFindNameById(pObj->pNtk->pManName, pObj->Id) == NULL )
         {
-            if ( pNet->pData != pName )
-            {
-                fprintf( stdout, "NetworkCheck: Net \"%s\" has different name compared to the one in the name table.\n", pNet->pData );
-                return 0;
-            }
-        }
-        // check that the nets with names are also in the table
-        Abc_NtkForEachNet( pNtk, pNet, i )
-        {
-            if ( pNet->pData && !stmm_lookup( pNtk->tName2Net, pNet->pData, (char**)&pNet2 ) )
-            {
-                fprintf( stdout, "NetworkCheck: Net \"%s\" is in the network but not in the name table.\n", pNet->pData );
-                return 0;
-            }
+            fprintf( stdout, "NetworkCheck: CI with ID %d is in the network but not in the name table.\n", pObj->Id );
+            return 0;
         }
-*/
     }
-/*
-    // check PI/PO/latch names
-    Abc_NtkForEachPi( pNtk, pObj, i )
+    Abc_NtkForEachCo( pNtk, pObj, i )
     {
-        if ( !stmm_lookup( pNtk->tObj2Name, (char *)pObj, &pName ) )
-        {
-            fprintf( stdout, "NetworkCheck: PI \"%s\" is in the network but not in the name table.\n", Abc_ObjName(pObj) );
-            return 0;
-        }
-        if ( Abc_NtkIsNetlist(pNtk) && strcmp( Abc_ObjName(Abc_ObjFanout0(pObj)), pName ) )
+        if ( Abc_ObjIsLatch(pObj) )
+            continue;
+        pObj = Abc_ObjFanin0Ntk(pObj);
+        if ( Nm_ManFindNameById(pObj->pNtk->pManName, pObj->Id) == NULL )
         {
-            fprintf( stdout, "NetworkCheck: PI \"%s\" has a different name compared to its net.\n", Abc_ObjName(pObj) );
+            fprintf( stdout, "NetworkCheck: CO with ID %d is in the network but not in the name table.\n", pObj->Id );
             return 0;
         }
     }
-    Abc_NtkForEachPo( pNtk, pObj, i )
+
+    if ( Abc_NtkIsNetlist(pNtk) )
     {
-        if ( !stmm_lookup( pNtk->tObj2Name, (char *)pObj, &pName ) )
-        {
-            fprintf( stdout, "NetworkCheck: PO \"%s\" is in the network but not in the name table.\n", Abc_ObjName(pObj) );
-            return 0;
-        }
-        if ( Abc_NtkIsNetlist(pNtk) && strcmp( Abc_ObjName(Abc_ObjFanin0(pObj)), pName ) )
+        Abc_NtkForEachNet( pNtk, pObj, i )
         {
-            fprintf( stdout, "NetworkCheck: PO \"%s\" has a different name compared to its net.\n", Abc_ObjName(pObj) );
-            return 0;
+            pName = Nm_ManFindNameById(pObj->pNtk->pManName, pObj->Id);
+            if ( pObj->pData && strcmp( pName, pObj->pData ) != 0 )
+            {
+                fprintf( stdout, "NetworkCheck: Net \"%s\" has different name in the name table and at the data pointer.\n", pObj->pData );
+                return 0;
+            }
         }
     }
-    Abc_NtkForEachLatch( pNtk, pObj, i )
+
+    // return the array of all IDs, which have names
+    vNameIds = Nm_ManReturnNameIds( pNtk->pManName );
+    // make sure that these IDs correspond to live objects
+    Vec_IntForEachEntry( vNameIds, NameId, i )
     {
-        if ( !stmm_lookup( pNtk->tObj2Name, (char *)pObj, &pName ) )
-        {
-            fprintf( stdout, "NetworkCheck: Latch \"%s\" is in the network but not in the name table.\n", Abc_ObjName(pObj) );
-            return 0;
-        }
-        if ( Abc_NtkIsNetlist(pNtk) && strcmp( Abc_ObjName(Abc_ObjFanout0(pObj)), pName ) )
+        if ( Vec_PtrEntry( pNtk->vObjs, NameId ) == NULL )
         {
-            fprintf( stdout, "NetworkCheck: Latch \"%s\" has a different name compared to its net.\n", Abc_ObjName(pObj) );
+            Vec_IntFree( vNameIds );
+            pName = Nm_ManFindNameById(pObj->pNtk->pManName, NameId);
+            fprintf( stdout, "NetworkCheck: Object with ID %d is deleted but its name \"%s\" remains in the name table.\n", NameId, pName );
             return 0;
         }
     }
-*/
+    Vec_IntFree( vNameIds );
     return 1;
 }
 
@@ -316,12 +310,6 @@ bool Abc_NtkCheckPis( Abc_Ntk_t * pNtk )
     Abc_Obj_t * pObj;
     int i;
 
-    if ( Abc_NtkCiNum(pNtk) != Abc_NtkPiNum(pNtk) + Abc_NtkLatchNum(pNtk) )
-    {
-        fprintf( stdout, "NetworkCheck: Incorrect size of the PI array.\n" );
-        return 0;
-    }
-
     // check that PIs are indeed PIs
     Abc_NtkForEachPi( pNtk, pObj, i )
     {
@@ -370,12 +358,6 @@ bool Abc_NtkCheckPos( Abc_Ntk_t * pNtk )
     Abc_Obj_t * pObj;
     int i;
 
-    if ( Abc_NtkCoNum(pNtk) != Abc_NtkPoNum(pNtk) + Abc_NtkLatchNum(pNtk) )
-    {
-        fprintf( stdout, "NetworkCheck: Incorrect size of the PO array.\n" );
-        return 0;
-    }
-
     // check that POs are indeed POs
     Abc_NtkForEachPo( pNtk, pObj, i )
     {
@@ -582,7 +564,7 @@ bool Abc_NtkCheckNode( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode )
 bool Abc_NtkCheckLatch( Abc_Ntk_t * pNtk, Abc_Obj_t * pLatch )
 {
     int Value = 1;
-    if ( pNtk->vLats->nSize != Abc_NtkLatchNum(pNtk) )
+    if ( pNtk->vLatches->nSize != Abc_NtkLatchNum(pNtk) )
     {
         fprintf( stdout, "NetworkCheck: Incorrect size of the latch array.\n" );
         return 0;
@@ -759,7 +741,7 @@ int Abc_NtkIsAcyclicHierarchy_rec( Abc_Ntk_t * pNtk )
         return 1;
     pNtk->fHieVisited = 1;
     // return if black box
-    if ( Abc_NtkIsBlackbox(pNtk) )
+    if ( Abc_NtkHasBlackbox(pNtk) )
         return 1;
     assert( Abc_NtkIsNetlist(pNtk) );
     // go through all the children networks
diff --git a/src/base/abc/abcDfs.c b/src/base/abc/abcDfs.c
index bd707c25..79669657 100644
--- a/src/base/abc/abcDfs.c
+++ b/src/base/abc/abcDfs.c
@@ -579,7 +579,7 @@ bool Abc_NtkIsAcyclic_rec( Abc_Obj_t * pNode )
     Abc_Obj_t * pFanin;
     int fAcyclic, i;
     assert( !Abc_ObjIsNet(pNode) );
-    if ( Abc_ObjIsCi(pNode) )
+    if ( Abc_ObjIsCi(pNode) || Abc_ObjIsBox(pNode) )
         return 1;
     assert( Abc_ObjIsNode( pNode ) || Abc_ObjIsBox( pNode ) );
     // make sure the node is not visited
@@ -607,7 +607,7 @@ bool Abc_NtkIsAcyclic_rec( Abc_Obj_t * pNode )
         if ( fAcyclic = Abc_NtkIsAcyclic_rec(pFanin) )
             continue;
         // return as soon as the loop is detected
-        fprintf( stdout, " <-- %s", Abc_ObjName(pNode) );
+        fprintf( stdout, " <-- %s", Abc_ObjName(Abc_ObjFanout0(pFanin)) );
         return 0;
     }
     // mark this node as a visited node
diff --git a/src/base/abc/abcFanio.c b/src/base/abc/abcFanio.c
index 60e847d0..2a84212e 100644
--- a/src/base/abc/abcFanio.c
+++ b/src/base/abc/abcFanio.c
@@ -50,7 +50,7 @@ void Abc_ObjAddFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanin )
     Vec_IntPushMem( pObj->pNtk->pMmStep, &pFaninR->vFanouts, pObj->Id    );
     if ( Abc_ObjIsComplement(pFanin) )
         Abc_ObjSetFaninC( pObj, Abc_ObjFaninNum(pObj)-1 );
-    Abc_HManAddFanin( pObj, pFanin );
+//    Abc_HManAddFanin( pObj, pFanin );
 }
 
 
@@ -179,7 +179,7 @@ void Abc_ObjPatchFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFaninOld, Abc_Obj_t * pFa
 ***********************************************************************/
 void Abc_ObjTransferFanout( Abc_Obj_t * pNodeFrom, Abc_Obj_t * pNodeTo )
 {
-    Vec_Ptr_t * vFanouts = pNodeFrom->pNtk->vPtrTemp;
+    Vec_Ptr_t * vFanouts;
     int nFanoutsOld, i;
     assert( !Abc_ObjIsComplement(pNodeFrom) );
     assert( !Abc_ObjIsComplement(pNodeTo) );
@@ -190,12 +190,14 @@ void Abc_ObjTransferFanout( Abc_Obj_t * pNodeFrom, Abc_Obj_t * pNodeTo )
     assert( Abc_ObjFanoutNum(pNodeFrom) > 0 );
     // get the fanouts of the old node
     nFanoutsOld = Abc_ObjFanoutNum(pNodeTo);
+    vFanouts = Vec_PtrAlloc( nFanoutsOld );
     Abc_NodeCollectFanouts( pNodeFrom, vFanouts );
     // patch the fanin of each of them
     for ( i = 0; i < vFanouts->nSize; i++ )
         Abc_ObjPatchFanin( vFanouts->pArray[i], pNodeFrom, pNodeTo );
     assert( Abc_ObjFanoutNum(pNodeFrom) == 0 );
     assert( Abc_ObjFanoutNum(pNodeTo) == nFanoutsOld + vFanouts->nSize );
+    Vec_PtrFree( vFanouts );
 }
 
 /**Function*************************************************************
diff --git a/src/base/abc/abcLatch.c b/src/base/abc/abcLatch.c
index 85dd9d8e..610e311a 100644
--- a/src/base/abc/abcLatch.c
+++ b/src/base/abc/abcLatch.c
@@ -155,9 +155,6 @@ void Abc_NtkLatchPipe( Abc_Ntk_t * pNtk, int nLatches )
             pLatch = Abc_NtkCreateLatch( pNtk );
             Abc_ObjAddFanin( pLatch, pFanin );
             Abc_LatchSetInitDc( pLatch );
-            // add the latch to the CI/CO lists
-            Vec_PtrPush( pNtk->vCis, pLatch );
-            Vec_PtrPush( pNtk->vCos, pLatch );
             // create the name of the new latch
             Abc_NtkLogicStoreName( pLatch, Abc_ObjNameDummy("LL", i*nLatches + k, nDigits) );
         }
diff --git a/src/base/abc/abcMinBase.c b/src/base/abc/abcMinBase.c
index cf5ad320..604dd96e 100644
--- a/src/base/abc/abcMinBase.c
+++ b/src/base/abc/abcMinBase.c
@@ -65,8 +65,8 @@ int Abc_NtkMinimumBase( Abc_Ntk_t * pNtk )
 ***********************************************************************/
 int Abc_NodeMinimumBase( Abc_Obj_t * pNode )
 {
-    Vec_Str_t * vSupport = pNode->pNtk->vStrTemp;
-    Vec_Ptr_t * vFanins = pNode->pNtk->vPtrTemp;
+    Vec_Str_t * vSupport;
+    Vec_Ptr_t * vFanins;
     DdNode * bTemp;
     int i, nVars;
 
@@ -74,11 +74,16 @@ int Abc_NodeMinimumBase( Abc_Obj_t * pNode )
     assert( Abc_ObjIsNode(pNode) );
 
     // compute support
+    vSupport = Vec_StrAlloc( 10 );
     nVars = Abc_NodeSupport( Cudd_Regular(pNode->pData), vSupport, Abc_ObjFaninNum(pNode) );
     if ( nVars == Abc_ObjFaninNum(pNode) )
+    {
+        Vec_StrFree( vSupport );
         return 0;
+    }
 
     // remove unused fanins
+    vFanins = Vec_PtrAlloc( Abc_ObjFaninNum(pNode) );
     Abc_NodeCollectFanins( pNode, vFanins );
     for ( i = 0; i < vFanins->nSize; i++ )
         if ( vSupport->pArray[i] == 0 )
@@ -88,6 +93,8 @@ int Abc_NodeMinimumBase( Abc_Obj_t * pNode )
     // update the function of the node
     pNode->pData = Extra_bddRemapUp( pNode->pNtk->pManFunc, bTemp = pNode->pData );   Cudd_Ref( pNode->pData );
     Cudd_RecursiveDeref( pNode->pNtk->pManFunc, bTemp );
+    Vec_PtrFree( vFanins );
+    Vec_StrFree( vSupport );
     return 1;
 }
 
diff --git a/src/base/abc/abcNames.c b/src/base/abc/abcNames.c
index f9fbe9db..4ddd2061 100644
--- a/src/base/abc/abcNames.c
+++ b/src/base/abc/abcNames.c
@@ -30,55 +30,6 @@
 
 /**Function*************************************************************
 
-  Synopsis    [Registers the name with the string memory manager.]
-
-  Description [This function should be used to register all names
-  permanentsly stored with the network. The pointer returned by
-  this procedure contains the copy of the name, which should be used
-  in all network manipulation procedures.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-char * Abc_NtkRegisterName( Abc_Ntk_t * pNtk, char * pName )
-{
-/*
-    char * pRegName;
-    if ( pName == NULL ) return NULL;
-    pRegName = Extra_MmFlexEntryFetch( pNtk->pMmNames, strlen(pName) + 1 );
-    strcpy( pRegName, pName );
-    return pRegName;
-*/
-    return NULL;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Registers the name with the string memory manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-char * Abc_NtkRegisterNamePlus( Abc_Ntk_t * pNtk, char * pName, char * pSuffix )
-{
-/*
-    char * pRegName;
-    assert( pName && pSuffix );
-    pRegName = Extra_MmFlexEntryFetch( pNtk->pMmNames, strlen(pName) + strlen(pSuffix) + 1 );
-    sprintf( pRegName, "%s%s", pName, pSuffix );
-    return pRegName;
-*/
-    return NULL;
-}
-
-/**Function*************************************************************
-
   Synopsis    [Gets the long name of the object.]
 
   Description [The temporary name is stored in a static buffer inside this
@@ -176,20 +127,7 @@ char * Abc_ObjNameDummy( char * pPrefix, int Num, int nDigits )
 ***********************************************************************/
 char * Abc_NtkLogicStoreName( Abc_Obj_t * pObjNew, char * pNameOld )
 {
-/*
-    char * pNewName;
-    assert( Abc_ObjIsCio(pObjNew) );
-    // get the new name
-    pNewName = Abc_NtkRegisterName( pObjNew->pNtk, pNameOld );
-    // add the name to the table
-    if ( stmm_insert( pObjNew->pNtk->tObj2Name, (char *)pObjNew, pNewName ) )
-    {
-        assert( 0 ); // the object is added for the second time
-    }
-    return pNewName;
-*/
-    Nm_ManStoreIdName( pObjNew->pNtk->pManName, pObjNew->Id, pNameOld, NULL );
-    return NULL;
+    return Nm_ManStoreIdName( pObjNew->pNtk->pManName, pObjNew->Id, pNameOld, NULL );
 }
 
 /**Function*************************************************************
@@ -205,21 +143,7 @@ char * Abc_NtkLogicStoreName( Abc_Obj_t * pObjNew, char * pNameOld )
 ***********************************************************************/
 char * Abc_NtkLogicStoreNamePlus( Abc_Obj_t * pObjNew, char * pNameOld, char * pSuffix )
 {
-/*
-    char * pNewName;
-    assert( pSuffix );
-    assert( Abc_ObjIsCio(pObjNew) );
-    // get the new name
-    pNewName = Abc_NtkRegisterNamePlus( pObjNew->pNtk, pNameOld, pSuffix );
-    // add the name to the table
-    if ( stmm_insert( pObjNew->pNtk->tObj2Name, (char *)pObjNew, pNewName ) )
-    {
-        assert( 0 ); // the object is added for the second time
-    }
-    return pNewName;
-*/
-    Nm_ManStoreIdName( pObjNew->pNtk->pManName, pObjNew->Id, pNameOld, pSuffix );
-    return NULL;
+    return Nm_ManStoreIdName( pObjNew->pNtk->pManName, pObjNew->Id, pNameOld, pSuffix );
 }
 
 /**Function*************************************************************
@@ -239,17 +163,20 @@ void Abc_NtkDupCioNamesTable( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew )
     int i;
     assert( Abc_NtkPiNum(pNtk) == Abc_NtkPiNum(pNtkNew) );
     assert( Abc_NtkPoNum(pNtk) == Abc_NtkPoNum(pNtkNew) );
+    assert( Abc_NtkAssertNum(pNtk) == Abc_NtkAssertNum(pNtkNew) );
     assert( Abc_NtkLatchNum(pNtk) == Abc_NtkLatchNum(pNtkNew) );
-//    assert( st_count(pNtk->tObj2Name) > 0 );
-//    assert( st_count(pNtkNew->tObj2Name) == 0 );
+    assert( Nm_ManNumEntries(pNtk->pManName) > 0 );
+    assert( Nm_ManNumEntries(pNtkNew->pManName) == 0 );
     // copy the CI/CO names if given
     Abc_NtkForEachPi( pNtk, pObj, i )
-        Abc_NtkLogicStoreName( Abc_NtkPi(pNtkNew,i),    Abc_ObjName(Abc_ObjFanout0Ntk(pObj)) );
+        Abc_NtkLogicStoreName( Abc_NtkPi(pNtkNew,i),      Abc_ObjName(Abc_ObjFanout0Ntk(pObj)) );
     Abc_NtkForEachPo( pNtk, pObj, i ) 
-        Abc_NtkLogicStoreName( Abc_NtkPo(pNtkNew,i),    Abc_ObjName(Abc_ObjFanin0Ntk(pObj)) );
+        Abc_NtkLogicStoreName( Abc_NtkPo(pNtkNew,i),      Abc_ObjName(Abc_ObjFanin0Ntk(pObj)) );
+    Abc_NtkForEachAssert( pNtk, pObj, i ) 
+        Abc_NtkLogicStoreName( Abc_NtkAssert(pNtkNew,i),  Abc_ObjName(Abc_ObjFanin0Ntk(pObj)) );
     if ( !Abc_NtkIsSeq(pNtk) )
     Abc_NtkForEachLatch( pNtk, pObj, i )
-        Abc_NtkLogicStoreName( Abc_NtkLatch(pNtkNew,i), Abc_ObjName(Abc_ObjFanout0Ntk(pObj)) );
+        Abc_NtkLogicStoreName( Abc_NtkLatch(pNtkNew,i),   Abc_ObjName(Abc_ObjFanout0Ntk(pObj)) );
 }
 
 /**Function*************************************************************
@@ -270,8 +197,8 @@ void Abc_NtkDupCioNamesTableDual( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew )
     assert( Abc_NtkPiNum(pNtk) == Abc_NtkPiNum(pNtkNew) );
     assert( Abc_NtkPoNum(pNtk) * 2 == Abc_NtkPoNum(pNtkNew) );
     assert( Abc_NtkLatchNum(pNtk) == Abc_NtkLatchNum(pNtkNew) );
-//    assert( st_count(pNtk->tObj2Name) > 0 );
-//    assert( st_count(pNtkNew->tObj2Name) == 0 );
+    assert( Nm_ManNumEntries(pNtk->pManName) > 0 );
+    assert( Nm_ManNumEntries(pNtkNew->pManName) == 0 );
     // copy the CI/CO names if given
     Abc_NtkForEachPi( pNtk, pObj, i )
         Abc_NtkLogicStoreName( Abc_NtkPi(pNtkNew,i),    Abc_ObjName(pObj) );
@@ -280,6 +207,8 @@ void Abc_NtkDupCioNamesTableDual( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew )
         Abc_NtkLogicStoreNamePlus( Abc_NtkPo(pNtkNew,2*i+0),    Abc_ObjName(pObj), "_pos" );
         Abc_NtkLogicStoreNamePlus( Abc_NtkPo(pNtkNew,2*i+1),    Abc_ObjName(pObj), "_neg" );
     }
+    Abc_NtkForEachAssert( pNtk, pObj, i ) 
+        Abc_NtkLogicStoreName( Abc_NtkAssert(pNtkNew,i),  Abc_ObjName(pObj) );
     if ( !Abc_NtkIsSeq(pNtk) )
     Abc_NtkForEachLatch( pNtk, pObj, i )
         Abc_NtkLogicStoreName( Abc_NtkLatch(pNtkNew,i), Abc_ObjName(pObj) );
@@ -439,22 +368,16 @@ void Abc_NtkOrderObjsByName( Abc_Ntk_t * pNtk, int fComb )
     Abc_NtkForEachLatch( pNtk, pObj, i )
         pObj->pCopy = (Abc_Obj_t *)Abc_ObjName(pObj);
     // order objects alphabetically
-    qsort( pNtk->vCis->pArray, pNtk->nPis, sizeof(Abc_Obj_t *), 
+    qsort( (void *)Vec_PtrArray(pNtk->vPis), Vec_PtrSize(pNtk->vPis), sizeof(Abc_Obj_t *), 
         (int (*)(const void *, const void *)) Abc_NodeCompareNames );
-    qsort( pNtk->vCos->pArray, pNtk->nPos, sizeof(Abc_Obj_t *), 
+    qsort( (void *)Vec_PtrArray(pNtk->vPos), Vec_PtrSize(pNtk->vPos), sizeof(Abc_Obj_t *), 
         (int (*)(const void *, const void *)) Abc_NodeCompareNames );
     // if the comparison if combinational (latches as PIs/POs), order them too
     if ( fComb )
-    {
-        qsort( pNtk->vLats->pArray, pNtk->nLatches, sizeof(Abc_Obj_t *), 
+        qsort( (void *)Vec_PtrArray(pNtk->vLatches), Vec_PtrSize(pNtk->vLatches), sizeof(Abc_Obj_t *), 
             (int (*)(const void *, const void *)) Abc_NodeCompareNames );
-        // add latches to make COs
-        Abc_NtkForEachLatch( pNtk, pObj, i )
-        {
-            Vec_PtrWriteEntry( pNtk->vCis, pNtk->nPis + i, pObj );
-            Vec_PtrWriteEntry( pNtk->vCos, pNtk->nPos + i, pObj );
-        }
-    }
+    // order CIs/COs first PIs/POs(Asserts) then latches
+    Abc_NtkOrderCisCos( pNtk );
     // clean the copy fields
     Abc_NtkForEachPi( pNtk, pObj, i )
         pObj->pCopy = NULL;
@@ -515,6 +438,26 @@ void Abc_NtkAddDummyPoNames( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
+void Abc_NtkAddDummyAssertNames( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj;
+    int nDigits, i;
+    nDigits = Extra_Base10Log( Abc_NtkAssertNum(pNtk) );
+    Abc_NtkForEachAssert( pNtk, pObj, i )
+        Abc_NtkLogicStoreName( pObj, Abc_ObjNameDummy("a", i, nDigits) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds dummy names.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void Abc_NtkAddDummyLatchNames( Abc_Ntk_t * pNtk )
 {
     Abc_Obj_t * pObj;
@@ -537,13 +480,11 @@ void Abc_NtkAddDummyLatchNames( Abc_Ntk_t * pNtk )
 ***********************************************************************/
 void Abc_NtkShortNames( Abc_Ntk_t * pNtk )
 {
-//    stmm_free_table( pNtk->tObj2Name );
-//    pNtk->tObj2Name = stmm_init_table(stmm_ptrcmp, stmm_ptrhash);
     Nm_ManFree( pNtk->pManName );
-    pNtk->pManName = Nm_ManCreate( Abc_NtkPiNum(pNtk) + Abc_NtkPoNum(pNtk) + Abc_NtkLatchNum(pNtk) + 10 );
-
+    pNtk->pManName = Nm_ManCreate( Abc_NtkCiNum(pNtk) + Abc_NtkCoNum(pNtk) - Abc_NtkLatchNum(pNtk) + 10 );
     Abc_NtkAddDummyPiNames( pNtk );
     Abc_NtkAddDummyPoNames( pNtk );
+    Abc_NtkAddDummyAssertNames( pNtk );
     Abc_NtkAddDummyLatchNames( pNtk );
 }
 
diff --git a/src/base/abc/abcNetlist.c b/src/base/abc/abcNetlist.c
index 75f3ed33..7d4460bf 100644
--- a/src/base/abc/abcNetlist.c
+++ b/src/base/abc/abcNetlist.c
@@ -106,33 +106,22 @@ Abc_Ntk_t * Abc_NtkNetlistToLogicHie( Abc_Ntk_t * pNtk )
     // clean the node copy fields
     Abc_NtkForEachNode( pNtk, pObj, i )
         pObj->pCopy = NULL;
-    // map the constant nodes
-    if ( Abc_NtkConst1(pNtk) )
-        Abc_NtkConst1(pNtk)->pCopy = Abc_NtkConst1(pNtkNew);
-    // clone PIs/POs and make old nets point to new terminals; create PI/PO names
-    Abc_NtkForEachPi( pNtk, pObj, i )
+    // clone PIs/POs/latches and make old nets point to new terminals; create names
+    Abc_NtkForEachCi( pNtk, pObj, i )
     {
         Abc_ObjFanout0(pObj)->pCopy = Abc_NtkDupObj(pNtkNew, pObj);
-        Abc_NtkLogicStoreName( pObj->pCopy, Abc_ObjName(pObj) );
+        Abc_NtkLogicStoreName( pObj->pCopy, Abc_ObjName(Abc_ObjFanout0(pObj)) );
     }
     Abc_NtkForEachPo( pNtk, pObj, i )
     {
         Abc_NtkDupObj(pNtkNew, pObj);
-        Abc_NtkLogicStoreName( pObj->pCopy, Abc_ObjName(pObj) );
+        Abc_NtkLogicStoreName( pObj->pCopy, Abc_ObjName(Abc_ObjFanin0(pObj)) );
     }
     // recursively flatten hierarchy, create internal logic, add new PI/PO names if there are black boxes
     Abc_NtkNetlistToLogicHie_rec( pNtkNew, pNtk, &Counter );
     if ( Counter )
         printf( "Warning: The total of %d block boxes are transformed into PI/PO pairs.\n", Counter );
-    // add latches
-    Abc_NtkForEachLatch( pNtk, pObj, i )
-    {
-        Abc_ObjFanout0(pObj)->pCopy = Abc_NtkDupObj(pNtkNew, pObj);
-        Vec_PtrPush( pNtkNew->vCis, pObj->pCopy );
-        Vec_PtrPush( pNtkNew->vCos, pObj->pCopy );
-        Abc_NtkLogicStoreName( Abc_NtkLatch(pNtkNew,i), Abc_ObjName(pObj) );
-    }
-    // collect the CO nodes
+    // connect the CO nodes
     Abc_NtkForEachCo( pNtk, pObj, i )
         Abc_ObjAddFanin( pObj->pCopy, Abc_ObjFanin0(pObj)->pCopy );
     // copy the timing information
@@ -167,62 +156,75 @@ void Abc_NtkNetlistToLogicHie_rec( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtkOld, int
     int i, k;
     // collect nodes and boxes in topological order
     vNodes = Abc_NtkDfs( pNtkOld, 0 );
-    // create logic for nodes and boxes
+    // duplicate nodes, create PIs/POs corresponding to blackboxes
+    // have to do it first if blackboxes break combinational loops
+    // (current we do not allow whiteboxes to break combinational loops)
     Vec_PtrForEachEntry( vNodes, pNode, i )
     {
-        if ( Abc_ObjFaninNum(pNode) == 0 )
-            continue;
         if ( Abc_ObjIsNode(pNode) )
         {
             // duplicate the node and save it in the fanout net
             Abc_NtkDupObj( pNtkNew, pNode );
+            Abc_ObjFanout0(pNode)->pCopy = pNode->pCopy;
+            continue;
+        }
+        assert( Abc_ObjIsBox(pNode) );
+        pNtkModel = pNode->pData;
+        if ( !Abc_NtkHasBlackbox(pNtkModel) )
+            continue;
+        // consider this blockbox
+        if ( pNtkNew->pBlackBoxes == NULL )
+        {
+            pNtkNew->pBlackBoxes = Vec_IntAlloc( 10 );
+            Vec_IntPush( pNtkNew->pBlackBoxes, (Abc_NtkPiNum(pNtkNew) << 16) | Abc_NtkPoNum(pNtkNew) );
+        }
+        sprintf( Prefix, "%s_%d_", Abc_NtkName(pNtkModel), *pCounter );
+        // create new PIs from the POs of the box
+        Abc_NtkForEachPo( pNtkModel, pObj, k )
+        {
+            pObj->pCopy = Abc_NtkCreatePi( pNtkNew );
+            Abc_ObjFanout(pNode, k)->pCopy = pObj->pCopy;
+            Abc_NtkLogicStoreNamePlus( pObj->pCopy, Prefix, Abc_ObjName(Abc_ObjFanin0(pObj)) );
+        }
+        // create new POs from the PIs of the box
+        Abc_NtkForEachPi( pNtkModel, pObj, k )
+        {
+            pObj->pCopy = Abc_NtkCreatePo( pNtkNew );
+//            Abc_ObjAddFanin( pObj->pCopy, Abc_ObjFanin(pNode, k)->pCopy );
+            Abc_NtkLogicStoreNamePlus( pObj->pCopy, Prefix, Abc_ObjName(Abc_ObjFanout0(pObj)) );
+        }
+        (*pCounter)++;
+        Vec_IntPush( pNtkNew->pBlackBoxes, (Abc_NtkPiNum(pNtkNew) << 16) | Abc_NtkPoNum(pNtkNew) );
+    }
+    // connect nodes and boxes
+    Vec_PtrForEachEntry( vNodes, pNode, i )
+    {
+        if ( Abc_ObjIsNode(pNode) )
+        {
+//            printf( "adding node %s\n", Abc_ObjName(Abc_ObjFanout0(pNode)) );
             Abc_ObjForEachFanin( pNode, pFanin, k )
                 Abc_ObjAddFanin( pNode->pCopy, pFanin->pCopy );
-            Abc_ObjFanout0(pNode)->pCopy = pNode->pCopy;
             continue;
         }
         assert( Abc_ObjIsBox(pNode) );
         pNtkModel = pNode->pData;
+//        printf( "adding model %s\n", Abc_NtkName(pNtkModel) );
         // consider the case of the black box
-        if ( Abc_NtkIsBlackbox(pNtkModel) )
+        if ( Abc_NtkHasBlackbox(pNtkModel) )
         {
-            if ( pNtkNew->pBlackBoxes == NULL )
-            {
-                pNtkNew->pBlackBoxes = Vec_IntAlloc( 10 );
-                Vec_IntPush( pNtkNew->pBlackBoxes, (Abc_NtkPiNum(pNtkNew) << 16) | Abc_NtkPoNum(pNtkNew) );
-            }
-            sprintf( Prefix, "%s_%d_", Abc_NtkName(pNtkModel), *pCounter );
-            // create new PIs from the POs of the box
-            Abc_NtkForEachPo( pNtkModel, pObj, k )
-            {
-                pObj->pCopy = Abc_NtkCreatePi( pNtkNew );
-                Abc_ObjFanout(pNode, k)->pCopy = pObj->pCopy;
-                Abc_NtkLogicStoreNamePlus( pObj->pCopy, Prefix, Abc_ObjName(pObj) );
-            }
             // create new POs from the PIs of the box
             Abc_NtkForEachPi( pNtkModel, pObj, k )
-            {
-                pObj->pCopy = Abc_NtkCreatePo( pNtkNew );
                 Abc_ObjAddFanin( pObj->pCopy, Abc_ObjFanin(pNode, k)->pCopy );
-                Abc_NtkLogicStoreNamePlus( pObj->pCopy, Prefix, Abc_ObjName(pObj) );
-            }
-            (*pCounter)++;
-            Vec_IntPush( pNtkNew->pBlackBoxes, (Abc_NtkPiNum(pNtkNew) << 16) | Abc_NtkPoNum(pNtkNew) );
-        }
-        else
-        {
-            // map the constant nodes
-            if ( Abc_NtkConst1(pNtkModel) )
-                Abc_NtkConst1(pNtkModel)->pCopy = Abc_NtkConst1(pNtkNew);
-            // transfer the nodes to the box inputs
-            Abc_NtkForEachPi( pNtkModel, pObj, k )
-                Abc_ObjFanout0(pObj)->pCopy = Abc_ObjFanin(pNode, k)->pCopy;
-            // construct recursively
-            Abc_NtkNetlistToLogicHie_rec( pNtkNew, pNtkModel, pCounter );
-            // transfer the results back
-            Abc_NtkForEachPo( pNtkModel, pObj, k )
-                Abc_ObjFanout(pNode, k)->pCopy = Abc_ObjFanin0(pObj)->pCopy;    
+            continue;
         }
+        // transfer the nodes to the box inputs
+        Abc_NtkForEachPi( pNtkModel, pObj, k )
+            Abc_ObjFanout0(pObj)->pCopy = Abc_ObjFanin(pNode, k)->pCopy;
+        // construct recursively
+        Abc_NtkNetlistToLogicHie_rec( pNtkNew, pNtkModel, pCounter );
+        // transfer the results back
+        Abc_NtkForEachPo( pNtkModel, pObj, k )
+            Abc_ObjFanout(pNode, k)->pCopy = Abc_ObjFanin0(pObj)->pCopy;    
     }
     Vec_PtrFree( vNodes );
 }
@@ -352,7 +354,7 @@ Abc_Ntk_t * Abc_NtkLogicSopToNetlist( Abc_Ntk_t * pNtk )
         // the driver is a node
 
         // get the CO name
-        pNameCo = Abc_ObjIsPo(pObj)? Abc_ObjName(pObj) : Abc_ObjNameSuffix( pObj, "_in" );
+        pNameCo = Abc_ObjIsLatch(pObj)? Abc_ObjNameSuffix( pObj, "_in" ) : Abc_ObjName(pObj);
         // make sure CO has a unique name
         assert( Abc_NtkFindNet( pNtkNew, pNameCo ) == NULL );
         // create the CO net and connect it to CO
@@ -401,6 +403,7 @@ Abc_Ntk_t * Abc_NtkAigToLogicSop( Abc_Ntk_t * pNtk )
 {
     Abc_Ntk_t * pNtkNew; 
     Abc_Obj_t * pObj, * pFanin, * pNodeNew;
+    Vec_Int_t * vInts;
     int i, k;
     assert( Abc_NtkIsStrash(pNtk) );
     // start the network
@@ -423,16 +426,17 @@ Abc_Ntk_t * Abc_NtkAigToLogicSop( Abc_Ntk_t * pNtk )
         // create an OR gate
         pNodeNew = Abc_NtkCreateNode(pNtkNew);
         // add fanins
-        Vec_IntClear( pNtk->vIntTemp );
+        vInts = Vec_IntAlloc( 10 );
         for ( pFanin = pObj; pFanin; pFanin = pFanin->pData )
         {
-            Vec_IntPush( pNtk->vIntTemp, (int)(pObj->fPhase != pFanin->fPhase) );
+            Vec_IntPush( vInts, (int)(pObj->fPhase != pFanin->fPhase) );
             Abc_ObjAddFanin( pNodeNew, pFanin->pCopy );
         }
         // create the logic function
-        pNodeNew->pData = Abc_SopCreateOrMultiCube( pNtkNew->pManFunc, pNtk->vIntTemp->nSize, pNtk->vIntTemp->pArray );
+        pNodeNew->pData = Abc_SopCreateOrMultiCube( pNtkNew->pManFunc, Vec_IntSize(vInts), Vec_IntArray(vInts) );
         // set the new node
         pObj->pCopy->pCopy = pNodeNew;
+        Vec_IntFree( vInts );
     }
     // connect the internal nodes
     Abc_NtkForEachNode( pNtk, pObj, i )
diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c
index c8bdf987..56d399f0 100644
--- a/src/base/abc/abcNtk.c
+++ b/src/base/abc/abcNtk.c
@@ -53,19 +53,14 @@ Abc_Ntk_t * Abc_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func )
     pNtk->Id          = !Abc_HManIsRunning()? 0 : Abc_HManGetNewNtkId();
     // start the object storage
     pNtk->vObjs       = Vec_PtrAlloc( 100 );
-    pNtk->vLats       = Vec_PtrAlloc( 100 );
-    pNtk->vCutSet     = Vec_PtrAlloc( 100 );
+    pNtk->vLatches    = Vec_PtrAlloc( 100 );
+    pNtk->vAsserts    = Vec_PtrAlloc( 100 );
+    pNtk->vPis        = Vec_PtrAlloc( 100 );
+    pNtk->vPos        = Vec_PtrAlloc( 100 );
     pNtk->vCis        = Vec_PtrAlloc( 100 );
     pNtk->vCos        = Vec_PtrAlloc( 100 );
-    pNtk->vAsserts    = Vec_PtrAlloc( 100 );
-    pNtk->vPtrTemp    = Vec_PtrAlloc( 100 );
-    pNtk->vIntTemp    = Vec_IntAlloc( 100 );
-    pNtk->vStrTemp    = Vec_StrAlloc( 100 );
-    // start the hash table
-//    pNtk->tName2Net   = stmm_init_table(strcmp, stmm_strhash);
-//    pNtk->tObj2Name   = stmm_init_table(stmm_ptrcmp, stmm_ptrhash);
+    pNtk->vCutSet     = Vec_PtrAlloc( 100 );
     // start the memory managers
-//    pNtk->pMmNames    = Extra_MmFlexStart();
     pNtk->pMmObj      = Extra_MmFixedStart( sizeof(Abc_Obj_t) );
     pNtk->pMmStep     = Extra_MmStepStart( ABC_NUM_STEPS );
     // get ready to assign the first Obj ID
@@ -115,7 +110,7 @@ Abc_Ntk_t * Abc_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func )
 Abc_Ntk_t * Abc_NtkStartFrom( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func )
 {
     Abc_Ntk_t * pNtkNew; 
-    Abc_Obj_t * pObj, * pObjNew;
+    Abc_Obj_t * pObj;
     int i;
     if ( pNtk == NULL )
         return NULL;
@@ -135,12 +130,10 @@ Abc_Ntk_t * Abc_NtkStartFrom( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_
         Abc_NtkDupObj(pNtkNew, pObj);
     Abc_NtkForEachPo( pNtk, pObj, i )
         Abc_NtkDupObj(pNtkNew, pObj);
+    Abc_NtkForEachAssert( pNtk, pObj, i )
+        Abc_NtkDupObj(pNtkNew, pObj);
     Abc_NtkForEachLatch( pNtk, pObj, i )
-    {
-        pObjNew = Abc_NtkDupObj(pNtkNew, pObj);
-        Vec_PtrPush( pNtkNew->vCis, pObjNew );
-        Vec_PtrPush( pNtkNew->vCos, pObjNew );
-    }
+        Abc_NtkDupObj(pNtkNew, pObj);
     if ( Abc_NtkIsStrash(pNtk) && Abc_HManIsRunning() )
     {
         Abc_HManAddProto( Abc_NtkConst1(pNtk)->pCopy, Abc_NtkConst1(pNtk) );
@@ -202,15 +195,12 @@ Abc_Ntk_t * Abc_NtkStartFromDual( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkF
         // collect first to old
         pObj->pCopy = pObjNew;
     }
+    Abc_NtkForEachAssert( pNtk, pObj, i )
+        Abc_NtkDupObj(pNtkNew, pObj);
     Abc_NtkForEachLatch( pNtk, pObj, i )
-    {
-        pObjNew = Abc_NtkDupObj(pNtkNew, pObj);
-        Vec_PtrPush( pNtkNew->vCis, pObjNew );
-        Vec_PtrPush( pNtkNew->vCos, pObjNew );
-    }
+        Abc_NtkDupObj(pNtkNew, pObj);
     // transfer the names
     Abc_NtkDupCioNamesTableDual( pNtk, pNtkNew );
-//    Abc_ManTimeDup( pNtk, pNtkNew );
     // check that the CI/CO/latches are copied correctly
     assert( Abc_NtkCiNum(pNtk)    == Abc_NtkCiNum(pNtkNew) );
     assert( Abc_NtkCoNum(pNtk)* 2 == Abc_NtkCoNum(pNtkNew) );
@@ -244,54 +234,6 @@ void Abc_NtkFinalize( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew )
 
 /**Function*************************************************************
 
-  Synopsis    [Finalizes the network using the existing network as a model.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NtkFinalizeRegular( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew )
-{
-    Abc_Obj_t * pObj, * pDriver, * pDriverNew;
-    int i;
-    // set the COs of the strashed network
-    Abc_NtkForEachCo( pNtk, pObj, i )
-    {
-        pDriver    = Abc_ObjFanin0Ntk( Abc_ObjFanin0(pObj) );
-        pDriverNew = pDriver->pCopy;
-        Abc_ObjAddFanin( pObj->pCopy, pDriverNew );
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Finalizes the network adding latches to CI/CO lists and creates their names.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NtkFinalizeLatches( Abc_Ntk_t * pNtk )
-{
-    Abc_Obj_t * pLatch;
-    int i;
-    // set the COs of the strashed network
-    Abc_NtkForEachLatch( pNtk, pLatch, i )
-    {
-        Vec_PtrPush( pNtk->vCis, pLatch );
-        Vec_PtrPush( pNtk->vCos, pLatch );
-        Abc_NtkLogicStoreName( pLatch, Abc_ObjNameSuffix(pLatch, "L") );
-    }
-}
-
-/**Function*************************************************************
-
   Synopsis    [Starts a new network using existing network as a model.]
 
   Description []
@@ -325,9 +267,9 @@ Abc_Ntk_t * Abc_NtkStartRead( char * pName )
 ***********************************************************************/
 void Abc_NtkFinalizeRead( Abc_Ntk_t * pNtk )
 {
-    Abc_Obj_t * pLatch, * pBox, * pObj;
+    Abc_Obj_t * pBox, * pObj;
     int i;
-    if ( pNtk->ntkType == ABC_NTK_BLACKBOX )
+    if ( Abc_NtkHasBlackbox(pNtk) )
     {
         pBox = Abc_NtkCreateBox(pNtk);
         Abc_NtkForEachPi( pNtk, pObj, i )
@@ -339,14 +281,8 @@ void Abc_NtkFinalizeRead( Abc_Ntk_t * pNtk )
     assert( Abc_NtkIsNetlist(pNtk) );
     // fix the net drivers
     Abc_NtkFixNonDrivenNets( pNtk );
-    // create the names table
-//    Abc_NtkCreateCioNamesTable( pNtk );
-    // add latches to the CI/CO arrays
-    Abc_NtkForEachLatch( pNtk, pLatch, i )
-    {
-        Vec_PtrPush( pNtk->vCis, pLatch );
-        Vec_PtrPush( pNtk->vCos, pLatch );
-    }
+    // reorder the CI/COs to PI/POs first
+    Abc_NtkOrderCisCos( pNtk );
 }
 
 /**Function*************************************************************
@@ -740,7 +676,6 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
     int LargePiece = (4 << ABC_NUM_STEPS);
     if ( pNtk == NULL )
         return;
-//printf( "Deleted newtork %p\n", pNtk );
     // make sure all the marks are clean
     Abc_NtkForEachObj( pNtk, pObj, i )
     {
@@ -765,26 +700,20 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
     if ( pNtk->pExdc )
         Abc_NtkDelete( pNtk->pExdc );
     // free the arrays
+    Vec_PtrFree( pNtk->vPis );
+    Vec_PtrFree( pNtk->vPos );
     Vec_PtrFree( pNtk->vCis );
     Vec_PtrFree( pNtk->vCos );
     Vec_PtrFree( pNtk->vAsserts );
+    Vec_PtrFree( pNtk->vLatches );
     Vec_PtrFree( pNtk->vObjs );
-    Vec_PtrFree( pNtk->vLats );
     Vec_PtrFree( pNtk->vCutSet );
-    Vec_PtrFree( pNtk->vPtrTemp );
-    Vec_IntFree( pNtk->vIntTemp );
-    Vec_StrFree( pNtk->vStrTemp );
     if ( pNtk->pModel ) free( pNtk->pModel );
-    // free the hash table of Obj name into Obj ID
-//    stmm_free_table( pNtk->tName2Net );
-//    stmm_free_table( pNtk->tObj2Name );
     TotalMemory  = 0;
-//    TotalMemory += Extra_MmFlexReadMemUsage(pNtk->pMmNames);
     TotalMemory += Extra_MmFixedReadMemUsage(pNtk->pMmObj);
     TotalMemory += Extra_MmStepReadMemUsage(pNtk->pMmStep);
 //    fprintf( stdout, "The total memory allocated internally by the network = %0.2f Mb.\n", ((double)TotalMemory)/(1<<20) );
     // free the storage 
-//    Extra_MmFlexStop ( pNtk->pMmNames, 0 );
     Extra_MmFixedStop( pNtk->pMmObj,   0 );
     Extra_MmStepStop ( pNtk->pMmStep,  0 );
     // free the timing manager
@@ -802,7 +731,7 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
         else
             Seq_Delete( pNtk->pManFunc );
     }
-    else if ( !Abc_NtkHasMapping(pNtk) )
+    else if ( !Abc_NtkHasMapping(pNtk) && !Abc_NtkHasBlackbox(pNtk) )
         assert( 0 );
     // name manager
     Nm_ManFree( pNtk->pManName );
@@ -815,9 +744,9 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
         stmm_foreach_item( pNtk->tName2Model, gen, &pName, (char **)&pNtkTemp )
             Abc_NtkDelete( pNtkTemp );
         stmm_free_table( pNtk->tName2Model );
-        if ( pNtk->pBlackBoxes ) 
-            Vec_IntFree( pNtk->pBlackBoxes );
     }
+    if ( pNtk->pBlackBoxes ) 
+        Vec_IntFree( pNtk->pBlackBoxes );
     free( pNtk );
 }
 
diff --git a/src/base/abc/abcObj.c b/src/base/abc/abcObj.c
index 56fcef95..53886161 100644
--- a/src/base/abc/abcObj.c
+++ b/src/base/abc/abcObj.c
@@ -101,34 +101,32 @@ void Abc_ObjAdd( Abc_Obj_t * pObj )
     // perform specialized operations depending on the object type
     if ( Abc_ObjIsNet(pObj) )
     {
-/*
-        // add the name to the table
-        if ( pObj->pData && stmm_insert( pNtk->tName2Net, pObj->pData, (char *)pObj ) )
-        {
-            printf( "Error: The net is already in the table...\n" );
-            assert( 0 );
-        }
-*/
         pNtk->nNets++;
     }
     else if ( Abc_ObjIsNode(pObj) )
     {
         pNtk->nNodes++;
     }
-    else if ( Abc_ObjIsLatch(pObj) )
-    {
-        Vec_PtrPush( pNtk->vLats, pObj );
-        pNtk->nLatches++;
-    }
     else if ( Abc_ObjIsPi(pObj) )
     {
+        Vec_PtrPush( pNtk->vPis, pObj );
         Vec_PtrPush( pNtk->vCis, pObj );
-        pNtk->nPis++;
     }
     else if ( Abc_ObjIsPo(pObj) )
     {
+        Vec_PtrPush( pNtk->vPos, pObj );
+        Vec_PtrPush( pNtk->vCos, pObj );
+    }
+    else if ( Abc_ObjIsLatch(pObj) )
+    {
+        Vec_PtrPush( pNtk->vLatches, pObj );
+        Vec_PtrPush( pNtk->vCis, pObj );
+        Vec_PtrPush( pNtk->vCos, pObj );
+    }
+    else if ( Abc_ObjIsAssert(pObj) )
+    {
+        Vec_PtrPush( pNtk->vAsserts, pObj );
         Vec_PtrPush( pNtk->vCos, pObj );
-        pNtk->nPos++;
     }
     else if ( Abc_ObjIsBox(pObj) )
     {
@@ -138,7 +136,6 @@ void Abc_ObjAdd( Abc_Obj_t * pObj )
     {
         assert( 0 );
     }
-    assert( pObj->Id >= 0 );
 }
 
 /**Function*************************************************************
@@ -155,7 +152,11 @@ void Abc_ObjAdd( Abc_Obj_t * pObj )
 Abc_Obj_t * Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj )
 {
     Abc_Obj_t * pObjNew;
+    // create the new object
     pObjNew = Abc_ObjAlloc( pNtkNew, pObj->Type );
+    // add the object to the network
+    Abc_ObjAdd( pObjNew );
+    // copy functionality/names
     if ( Abc_ObjIsNode(pObj) ) // copy the function if functionality is compatible
     {
         if ( pNtkNew->ntkFunc == pObj->pNtk->ntkFunc ) 
@@ -172,18 +173,11 @@ Abc_Obj_t * Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj )
     }
     else if ( Abc_ObjIsNet(pObj) ) // copy the name
     {
-//        pObjNew->pData = Abc_NtkRegisterName( pNtkNew, pObj->pData );
+        pObjNew->pData = Nm_ManStoreIdName( pNtkNew->pManName, pObjNew->Id, pObj->pData, NULL );
     }
     else if ( Abc_ObjIsLatch(pObj) ) // copy the reset value
         pObjNew->pData = pObj->pData;
     pObj->pCopy = pObjNew;
-    // add the object to the network
-    Abc_ObjAdd( pObjNew );
-
-
-    if ( Abc_ObjIsNet(pObj) )
-        pObjNew->pData = Nm_ManStoreIdName( pNtkNew->pManName, pObjNew->Id, pObj->pData, NULL );
-        
     return pObjNew;
 }
 
@@ -201,37 +195,34 @@ Abc_Obj_t * Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj )
 ***********************************************************************/
 void Abc_NtkDeleteObj( Abc_Obj_t * pObj )
 {
-    Vec_Ptr_t * vNodes = pObj->pNtk->vPtrTemp;
     Abc_Ntk_t * pNtk = pObj->pNtk;
+    Vec_Ptr_t * vNodes;
     int i;
 
     assert( !Abc_ObjIsComplement(pObj) );
 
     // delete fanins and fanouts
+    vNodes = Vec_PtrAlloc( 100 );
     Abc_NodeCollectFanouts( pObj, vNodes );
     for ( i = 0; i < vNodes->nSize; i++ )
         Abc_ObjDeleteFanin( vNodes->pArray[i], pObj );
     Abc_NodeCollectFanins( pObj, vNodes );
     for ( i = 0; i < vNodes->nSize; i++ )
         Abc_ObjDeleteFanin( pObj, vNodes->pArray[i] );
+    Vec_PtrFree( vNodes );
 
     // remove from the list of objects
     Vec_PtrWriteEntry( pNtk->vObjs, pObj->Id, NULL );
     pObj->Id = (1<<26)-1;
     pNtk->nObjs--;
 
+    // remove from the table of names
+    if ( Nm_ManFindNameById(pObj->pNtk->pManName, pObj->Id) )
+        Nm_ManDeleteIdName(pObj->pNtk->pManName, pObj->Id);
+
     // perform specialized operations depending on the object type
     if ( Abc_ObjIsNet(pObj) )
     {
-        assert( 0 );
-/*
-        // remove the net from the hash table of nets
-        if ( pObj->pData && !stmm_delete( pNtk->tName2Net, (char **)&pObj->pData, (char **)&pObj ) )
-        {
-            printf( "Error: The net is not in the table...\n" );
-            assert( 0 );
-        }
-*/
         pObj->pData = NULL;
         pNtk->nNets--;
     }
@@ -239,26 +230,33 @@ void Abc_NtkDeleteObj( Abc_Obj_t * pObj )
     {
         if ( Abc_NtkHasBdd(pNtk) )
             Cudd_RecursiveDeref( pNtk->pManFunc, pObj->pData );
+        pObj->pData = NULL;
         pNtk->nNodes--;
     }
     else if ( Abc_ObjIsLatch(pObj) )
     {
-        pNtk->nLatches--;
+        Vec_PtrRemove( pNtk->vLatches, pObj );
+        Vec_PtrRemove( pNtk->vCis, pObj );
+        Vec_PtrRemove( pNtk->vCos, pObj );
+    }
+    else if ( Abc_ObjIsPi(pObj) )
+    {
+        Vec_PtrRemove( pObj->pNtk->vPis, pObj );
+        Vec_PtrRemove( pObj->pNtk->vCis, pObj );
     }
     else if ( Abc_ObjIsPo(pObj) )
     {
-        assert( Abc_NtkPoNum(pObj->pNtk) > 0 );
+        Vec_PtrRemove( pObj->pNtk->vPos, pObj );
         Vec_PtrRemove( pObj->pNtk->vCos, pObj );
-        pObj->pNtk->nPos--;
-
-        assert( 0 );
-/*
-        // add the name to the table
-        if ( !stmm_delete( pObj->pNtk->tObj2Name, (char **)&pObj, NULL ) )
-        {
-            assert( 0 ); // the PO is not in the table
-        }
-*/
+    }
+    else if ( Abc_ObjIsAssert(pObj) )
+    {
+        Vec_PtrRemove( pObj->pNtk->vAsserts, pObj );
+        Vec_PtrRemove( pObj->pNtk->vCos, pObj );
+    }
+    else if ( Abc_ObjIsBox(pObj) )
+    {
+        pNtk->nBoxes--;
     }
     else
         assert( 0 );
@@ -377,9 +375,6 @@ Abc_Obj_t * Abc_NtkFindNet( Abc_Ntk_t * pNtk, char * pName )
     Abc_Obj_t * pNet;
     int ObjId;
     assert( Abc_NtkIsNetlist(pNtk) );
-//    if ( stmm_lookup( pNtk->tName2Net, pName, (char**)&pNet ) )
-//        return pNet;
-//    return NULL;
     ObjId = Nm_ManFindIdByName( pNtk->pManName, pName, NULL );
     if ( ObjId == -1 )
         return NULL;
@@ -406,7 +401,6 @@ Abc_Obj_t * Abc_NtkFindOrCreateNet( Abc_Ntk_t * pNtk, char * pName )
         return pNet;
     // create a new net
     pNet = Abc_ObjAlloc( pNtk, ABC_OBJ_NET );
-//    pNet->pData = Abc_NtkRegisterName( pNtk, pName );
     Abc_ObjAdd( pNet );
     pNet->pData = Nm_ManStoreIdName( pNtk->pManName, pNet->Id, pName, NULL );
     return pNet;
@@ -510,6 +504,25 @@ Abc_Obj_t * Abc_NtkCreateLatch( Abc_Ntk_t * pNtk )
 
 /**Function*************************************************************
 
+  Synopsis    [Create the new node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Abc_NtkCreateAssert( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj;
+    pObj = Abc_ObjAlloc( pNtk, ABC_OBJ_ASSERT );     
+    Abc_ObjAdd( pObj );
+    return pObj;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Creates inverter.]
 
   Description []
diff --git a/src/base/abc/abcSop.c b/src/base/abc/abcSop.c
index d5cc65f1..a893f3e2 100644
--- a/src/base/abc/abcSop.c
+++ b/src/base/abc/abcSop.c
@@ -360,6 +360,44 @@ char * Abc_SopCreateBuf( Extra_MmFlex_t * pMan )
     return Abc_SopRegister(pMan, "1 1\n");
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Creates the arbitrary cover from the truth table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Abc_SopCreateFromTruth( Extra_MmFlex_t * pMan, int nVars, unsigned * pTruth )
+{
+    char * pSop, * pCube;
+    int nMints, Counter, i, k;
+    // count the number of true minterms
+    Counter = 0;
+    nMints = (1 << nVars);
+    for ( i = 0; i < nMints; i++ )
+        Counter += ((pTruth[i>>5] & (1 << (i&31))) > 0);
+    // SOP is not well-defined if the truth table is constant 0
+    assert( Counter > 0 );
+    if ( Counter == 0 )
+        return NULL;
+    // start the cover
+    pSop = Abc_SopStart( pMan, Counter, nVars );
+    // create true minterms
+    Counter = 0;
+    for ( i = 0; i < nMints; i++ )
+        if ( (pTruth[i>>5] & (1 << (i&31))) > 0 )
+        {
+            pCube = pSop + Counter * (nVars + 3);
+            for ( k = 0; k < nVars; k++ )
+                pCube[k] = '0' + ((i & (1 << k)) > 0);
+            Counter++;
+        }
+    return pSop;
+}
 
 /**Function*************************************************************
 
diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c
index 034aa38f..175b17f7 100644
--- a/src/base/abc/abcUtil.c
+++ b/src/base/abc/abcUtil.c
@@ -47,7 +47,7 @@ void Abc_NtkIncrementTravId( Abc_Ntk_t * pNtk )
 {
     Abc_Obj_t * pObj;
     int i;
-    if ( pNtk->nTravIds == (1<<10)-1 )
+    if ( pNtk->nTravIds == (1<<9)-1 )
     {
         pNtk->nTravIds = 0;
         Abc_NtkForEachObj( pNtk, pObj, i )
@@ -58,6 +58,36 @@ void Abc_NtkIncrementTravId( Abc_Ntk_t * pNtk )
 
 /**Function*************************************************************
 
+  Synopsis    [Order CI/COs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkOrderCisCos( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj;
+    int i;
+    Vec_PtrClear( pNtk->vCis );
+    Vec_PtrClear( pNtk->vCos );
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        Vec_PtrPush( pNtk->vCis, pObj );
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        Vec_PtrPush( pNtk->vCos, pObj );
+    Abc_NtkForEachAssert( pNtk, pObj, i )
+        Vec_PtrPush( pNtk->vCos, pObj );
+    Abc_NtkForEachLatch( pNtk, pObj, i )
+    {
+        Vec_PtrPush( pNtk->vCis, pObj );
+        Vec_PtrPush( pNtk->vCos, pObj );
+    }
+}
+
+/**Function*************************************************************
+
   Synopsis    [Reads the number of cubes of the node.]
 
   Description []
@@ -84,7 +114,7 @@ int Abc_NtkGetCubeNum( Abc_Ntk_t * pNtk )
 
 /**Function*************************************************************
 
-  Synopsis    [Reads the number of cubes of the node.]
+  Synopsis    [Reads the number of literals in the SOPs of the nodes.]
 
   Description []
                
@@ -1029,6 +1059,12 @@ void Abc_NtkReassignIds( Abc_Ntk_t * pNtk )
         pNode->Id = Vec_PtrSize( vObjsNew );
         Vec_PtrPush( vObjsNew, pNode );
     }
+    // put assert nodes next
+    Abc_NtkForEachAssert( pNtk, pNode, i )
+    {
+        pNode->Id = Vec_PtrSize( vObjsNew );
+        Vec_PtrPush( vObjsNew, pNode );
+    }
     // put latches next
     Abc_NtkForEachLatch( pNtk, pNode, i )
     {
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 201a1208..075c64ee 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -83,9 +83,9 @@ static int Abc_CommandExdcFree     ( Abc_Frame_t * pAbc, int argc, char ** argv
 static int Abc_CommandExdcGet      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandExdcSet      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandCut          ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandXyz          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandEspresso     ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandGen          ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandXyz          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandTest         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandFraig        ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -193,9 +193,9 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Various",      "exdc_get",      Abc_CommandExdcGet,          1 );
     Cmd_CommandAdd( pAbc, "Various",      "exdc_set",      Abc_CommandExdcSet,          1 );
     Cmd_CommandAdd( pAbc, "Various",      "cut",           Abc_CommandCut,              0 );
-    Cmd_CommandAdd( pAbc, "Various",      "xyz",           Abc_CommandXyz,              1 );
     Cmd_CommandAdd( pAbc, "Various",      "espresso",      Abc_CommandEspresso,         1 );
     Cmd_CommandAdd( pAbc, "Various",      "gen",           Abc_CommandGen,              0 );
+    Cmd_CommandAdd( pAbc, "Various",      "xyz",           Abc_CommandXyz,              1 );
     Cmd_CommandAdd( pAbc, "Various",      "test",          Abc_CommandTest,             0 );
 
     Cmd_CommandAdd( pAbc, "Fraiging",     "fraig",         Abc_CommandFraig,            1 );
@@ -4297,98 +4297,6 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_CommandXyz( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
-    FILE * pOut, * pErr;
-    Abc_Ntk_t * pNtk, * pNtkRes;
-    int c;
-    int fVerbose;
-    int fUseInvs;
-    int nFaninMax;
-    extern Abc_Ntk_t * Abc_NtkXyz( Abc_Ntk_t * pNtk, int nFaninMax, bool fUseEsop, bool fUseSop, bool fUseInvs, bool fVerbose );
-
-    pNtk = Abc_FrameReadNtk(pAbc);
-    pOut = Abc_FrameReadOut(pAbc);
-    pErr = Abc_FrameReadErr(pAbc);
-
-    // set defaults
-    fVerbose = 0;
-    fUseInvs = 1;
-    nFaninMax = 128;
-    Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Nivh" ) ) != EOF )
-    {
-        switch ( c )
-        {
-        case 'N':
-            if ( globalUtilOptind >= argc )
-            {
-                fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            nFaninMax = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( nFaninMax < 0 ) 
-                goto usage;
-            break;
-        case 'i':
-            fUseInvs ^= 1;
-            break;
-        case 'v':
-            fVerbose ^= 1;
-            break;
-        case 'h':
-            goto usage;
-        default:
-            goto usage;
-        }
-    }
-    if ( pNtk == NULL )
-    {
-        fprintf( pErr, "Empty network.\n" );
-        return 1;
-    }
-
-    if ( !Abc_NtkIsStrash(pNtk) )
-    {
-        fprintf( pErr, "Only works for strashed networks.\n" );
-        return 1;
-    }
-
-    // run the command
-//    pNtkRes = Abc_NtkXyz( pNtk, nFaninMax, 1, 0, fUseInvs, fVerbose );
-    pNtkRes = NULL;
-
-    if ( pNtkRes == NULL )
-    {
-        fprintf( pErr, "Command has failed.\n" );
-        return 0;
-    }
-    // replace the current network
-    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
-    return 0;
-
-usage:
-    fprintf( pErr, "usage: xyz [-N num] [-ivh]\n" );
-    fprintf( pErr, "\t         specilized AND/OR/EXOR decomposition\n" );
-    fprintf( pErr, "\t-N num : maximum number of inputs [default = %d]\n", nFaninMax );
-    fprintf( pErr, "\t-i     : toggle the use of interters [default = %s]\n", fUseInvs? "yes": "no" );
-    fprintf( pErr, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
-    fprintf( pErr, "\t-h     : print the command usage\n");
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
 int Abc_CommandEspresso( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
@@ -4543,20 +4451,127 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandXyz( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk, * pNtkRes;
+    int c;
+    int nLutMax;
+    int nPlaMax;
+    int fVerbose;
+//    extern Abc_Ntk_t * Abc_NtkXyz( Abc_Ntk_t * pNtk, int nPlaMax, bool fUseEsop, bool fUseSop, bool fUseInvs, bool fVerbose );
+    extern void *      Abc_NtkPlayer( void * pNtk, int nLutMax, int nPlaMax, int fVerbose );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    nLutMax = 8;
+    nPlaMax = 128;
+    fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "LPvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'L':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nLutMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nLutMax < 0 ) 
+                goto usage;
+            break;
+        case 'P':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nPlaMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nPlaMax < 0 ) 
+                goto usage;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( pErr, "Only works for strashed networks.\n" );
+        return 1;
+    }
+
+    if ( nLutMax < 2 || nLutMax > 8 || nPlaMax < 8 || nPlaMax > 128  )
+    {
+        fprintf( pErr, "Incorrect LUT/PLA parameters.\n" );
+        return 1;
+    }
+
+    // run the command
+//    pNtkRes = Abc_NtkXyz( pNtk, nPlaMax, 1, 0, fUseInvs, fVerbose );
+    pNtkRes = Abc_NtkPlayer( pNtk, nLutMax, nPlaMax, fVerbose );
+    if ( pNtkRes == NULL )
+    {
+        fprintf( pErr, "Command has failed.\n" );
+        return 0;
+    }
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: xyz [-L num] [-P num] [-vh]\n" );
+    fprintf( pErr, "\t         specilized LUT/PLA decomposition\n" );
+    fprintf( pErr, "\t-L num : maximum number of LUT inputs (2<=num<=8) [default = %d]\n", nLutMax );
+    fprintf( pErr, "\t-P num : maximum number of PLA inputs/cubes (8<=num<=128) [default = %d]\n", nPlaMax );
+    fprintf( pErr, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
-    Abc_Ntk_t * pNtk;//, * pNtkRes;
+    Abc_Ntk_t * pNtk, * pNtkRes;
     int c;
     int nLevels;
 //    extern Abc_Ntk_t * Abc_NtkNewAig( Abc_Ntk_t * pNtk );
+    extern Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    nLevels = 15;
+    nLevels = 128;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "Nh" ) ) != EOF )
     {
@@ -4614,7 +4629,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 //        Cut_CellDumpToFile();
 //    else
 //        Cut_CellPrecompute();
-        Cut_CellLoad();
+//        Cut_CellLoad();
 /*
         {
             Abc_Ntk_t * pNtkRes;
@@ -4623,6 +4638,24 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
             Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
         }
 */
+//    Abc_NtkSimulteBuggyMiter( pNtk );
+
+//    Rwr_Temp();
+//    Abc_MvExperiment();
+//    Ivy_TruthTest();
+
+
+    pNtkRes = Abc_NtkIvy( pNtk );
+//    pNtkRes = Abc_NtkPlayer( pNtk, nLevels, 0 );
+//    pNtkRes = NULL;
+    if ( pNtkRes == NULL )
+    {
+        fprintf( pErr, "Command has failed.\n" );
+        return 1;
+    }
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+
     return 0;
 
 usage:
@@ -6614,9 +6647,9 @@ int Abc_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fVerbose;
     int nSeconds;
     int nConfLimit;
-    int nImpLimit;
+    int nInsLimit;
 
-    extern void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nImpLimit );
+    extern void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nInsLimit );
     extern void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fVerbose );
 
 
@@ -6629,7 +6662,7 @@ int Abc_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv )
     fVerbose =  0;
     nSeconds = 20;
     nConfLimit = 10000;   
-    nImpLimit  = 0;
+    nInsLimit  = 0;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "TCIsvh" ) ) != EOF )
     {
@@ -6663,9 +6696,9 @@ int Abc_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv )
                 fprintf( pErr, "Command line switch \"-I\" should be followed by an integer.\n" );
                 goto usage;
             }
-            nImpLimit = atoi(argv[globalUtilOptind]);
+            nInsLimit = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
-            if ( nImpLimit < 0 ) 
+            if ( nInsLimit < 0 ) 
                 goto usage;
             break;
         case 's':
@@ -6686,7 +6719,7 @@ int Abc_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // perform equivalence checking
     if ( fSat )
-        Abc_NtkCecSat( pNtk1, pNtk2, nConfLimit, nImpLimit );
+        Abc_NtkCecSat( pNtk1, pNtk2, nConfLimit, nInsLimit );
     else
         Abc_NtkCecFraig( pNtk1, pNtk2, nSeconds, fVerbose );
 
@@ -6699,7 +6732,7 @@ usage:
     fprintf( pErr, "\t         performs combinational equivalence checking\n" );
     fprintf( pErr, "\t-T num : approximate runtime limit in seconds [default = %d]\n", nSeconds );
     fprintf( pErr, "\t-C num : limit on the number of conflicts [default = %d]\n",    nConfLimit );
-    fprintf( pErr, "\t-I num : limit on the number of implications [default = %d]\n", nImpLimit );
+    fprintf( pErr, "\t-I num : limit on the number of clause inspections [default = %d]\n", nInsLimit );
     fprintf( pErr, "\t-s     : toggle \"SAT only\" and \"FRAIG + SAT\" [default = %s]\n", fSat? "SAT only": "FRAIG + SAT" );
     fprintf( pErr, "\t-v     : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
@@ -6734,9 +6767,9 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv )
     int nFrames;
     int nSeconds;
     int nConfLimit;
-    int nImpLimit;
+    int nInsLimit;
 
-    extern void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nImpLimit, int nFrames );
+    extern void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nInsLimit, int nFrames );
     extern void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nFrames, int fVerbose );
 
 
@@ -6750,7 +6783,7 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv )
     nFrames  =  3;
     nSeconds = 20;
     nConfLimit = 10000;   
-    nImpLimit  = 0;
+    nInsLimit  = 0;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "FTCIsvh" ) ) != EOF )
     {
@@ -6795,9 +6828,9 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv )
                 fprintf( pErr, "Command line switch \"-I\" should be followed by an integer.\n" );
                 goto usage;
             }
-            nImpLimit = atoi(argv[globalUtilOptind]);
+            nInsLimit = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
-            if ( nImpLimit < 0 ) 
+            if ( nInsLimit < 0 ) 
                 goto usage;
             break;
         case 'v':
@@ -6818,7 +6851,7 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // perform equivalence checking
     if ( fSat )
-        Abc_NtkSecSat( pNtk1, pNtk2, nConfLimit, nImpLimit, nFrames );
+        Abc_NtkSecSat( pNtk1, pNtk2, nConfLimit, nInsLimit, nFrames );
     else
         Abc_NtkSecFraig( pNtk1, pNtk2, nSeconds, nFrames, fVerbose );
 
@@ -6835,7 +6868,7 @@ usage:
     fprintf( pErr, "\t-F num : the number of time frames to use [default = %d]\n", nFrames );
     fprintf( pErr, "\t-T num : approximate runtime limit in seconds [default = %d]\n", nSeconds );
     fprintf( pErr, "\t-C num : limit on the number of conflicts [default = %d]\n",    nConfLimit );
-    fprintf( pErr, "\t-I num : limit on the number of implications [default = %d]\n", nImpLimit );
+    fprintf( pErr, "\t-I num : limit on the number of inspections [default = %d]\n", nInsLimit );
     fprintf( pErr, "\tfile1  : (optional) the file with the first network\n");
     fprintf( pErr, "\tfile2  : (optional) the file with the second network\n");
     fprintf( pErr, "\t         if no files are given, uses the current network and its spec\n");
@@ -6863,7 +6896,7 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fJFront;
     int fVerbose;
     int nConfLimit;
-    int nImpLimit;
+    int nInsLimit;
     int clk;
 
     pNtk = Abc_FrameReadNtk(pAbc);
@@ -6871,10 +6904,10 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv )
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    fJFront = 0;
+    fJFront    = 0;
     fVerbose   = 0;
     nConfLimit = 100000;   
-    nImpLimit  = 0;
+    nInsLimit  = 0;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "CIvjh" ) ) != EOF )
     {
@@ -6897,9 +6930,9 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv )
                 fprintf( pErr, "Command line switch \"-I\" should be followed by an integer.\n" );
                 goto usage;
             }
-            nImpLimit = atoi(argv[globalUtilOptind]);
+            nInsLimit = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
-            if ( nImpLimit < 0 ) 
+            if ( nInsLimit < 0 ) 
                 goto usage;
             break;
         case 'j':
@@ -6934,13 +6967,13 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv )
     clk = clock();
     if ( Abc_NtkIsStrash(pNtk) )
     {
-        RetValue = Abc_NtkMiterSat( pNtk, nConfLimit, nImpLimit, fJFront, fVerbose );
+        RetValue = Abc_NtkMiterSat( pNtk, (sint64)nConfLimit, (sint64)nInsLimit, fJFront, fVerbose, NULL, NULL );
     }
     else
     {
         Abc_Ntk_t * pTemp;
         pTemp = Abc_NtkStrash( pNtk, 0, 0 );
-        RetValue = Abc_NtkMiterSat( pTemp, nConfLimit, nImpLimit, fJFront, fVerbose );
+        RetValue = Abc_NtkMiterSat( pTemp, (sint64)nConfLimit, (sint64)nInsLimit, fJFront, fVerbose, NULL, NULL );
         pNtk->pModel = pTemp->pModel;  pTemp->pModel = NULL;
         Abc_NtkDelete( pTemp );
     }
@@ -6948,10 +6981,22 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv )
     // verify that the pattern is correct
     if ( RetValue == 0 && Abc_NtkPoNum(pNtk) == 1 )
     {
+        //int i;
+        //Abc_Obj_t * pObj;
         int * pSimInfo = Abc_NtkVerifySimulatePattern( pNtk, pNtk->pModel );
         if ( pSimInfo[0] != 1 )
             printf( "ERROR in Abc_NtkMiterSat(): Generated counter example is invalid.\n" );
         free( pSimInfo );
+        /*
+        // print model
+        Abc_NtkForEachPi( pNtk, pObj, i )
+        {
+            printf( "%d", (int)(pNtk->pModel[i] > 0) );
+            if ( i == 70 )
+                break;
+        }
+        printf( "\n" );
+        */
     }
 
     if ( RetValue == -1 )
@@ -6969,7 +7014,7 @@ usage:
     fprintf( pErr, "\t         solves the combinational miter using SAT solver MiniSat-1.14\n" );
     fprintf( pErr, "\t         derives CNF from the current network and leave it unchanged\n" );
     fprintf( pErr, "\t-C num : limit on the number of conflicts [default = %d]\n",    nConfLimit );
-    fprintf( pErr, "\t-I num : limit on the number of implications [default = %d]\n", nImpLimit );
+    fprintf( pErr, "\t-I num : limit on the number of inspections [default = %d]\n", nInsLimit );
     fprintf( pErr, "\t-j     : toggle the use of J-frontier [default = %s]\n", fJFront? "yes": "no" );  
     fprintf( pErr, "\t-v     : prints verbose information [default = %s]\n", fVerbose? "yes": "no" );  
     fprintf( pErr, "\t-h     : print the command usage\n");
@@ -7001,7 +7046,7 @@ int Abc_CommandProve( Abc_Frame_t * pAbc, int argc, char ** argv )
     // set defaults
     Prove_ParamsSetDefault( pParams );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "NCFLrfvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "NCFLIrfbvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -7049,12 +7094,26 @@ int Abc_CommandProve( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pParams->nMiteringLimitLast < 0 ) 
                 goto usage;
             break;
+        case 'I':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-I\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pParams->nTotalInspectLimit = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pParams->nTotalInspectLimit < 0 ) 
+                goto usage;
+            break;
         case 'r':
             pParams->fUseRewriting ^= 1;
             break;
         case 'f':
             pParams->fUseFraiging ^= 1;
             break;
+        case 'b':
+            pParams->fUseBdds ^= 1;
+            break;
         case 'v':
             pParams->fVerbose ^= 1;
             break;
@@ -7118,15 +7177,17 @@ int Abc_CommandProve( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: prove [-N num] [-C num] [-F num] [-L num] [-rfvh]\n" );
+    fprintf( pErr, "usage: prove [-N num] [-C num] [-F num] [-L num] [-I num] [-rfbvh]\n" );
     fprintf( pErr, "\t         solves combinational miter by rewriting, FRAIGing, and SAT\n" );
     fprintf( pErr, "\t         replaces the current network by the cone modified by rewriting\n" );
     fprintf( pErr, "\t-N num : max number of iterations [default = %d]\n", pParams->nItersMax );
     fprintf( pErr, "\t-C num : max starting number of conflicts in mitering [default = %d]\n", pParams->nMiteringLimitStart );
     fprintf( pErr, "\t-F num : max starting number of conflicts in fraiging [default = %d]\n", pParams->nFraigingLimitStart );
     fprintf( pErr, "\t-L num : max last-gasp number of conflicts in mitering [default = %d]\n", pParams->nMiteringLimitLast );
+    fprintf( pErr, "\t-I num : max number of clause inspections in all SAT calls [default = %d]\n", (int)pParams->nTotalInspectLimit );
     fprintf( pErr, "\t-r     : toggle the use of rewriting [default = %s]\n", pParams->fUseRewriting? "yes": "no" );  
     fprintf( pErr, "\t-f     : toggle the use of FRAIGing [default = %s]\n", pParams->fUseFraiging? "yes": "no" );  
+    fprintf( pErr, "\t-b     : toggle the use of BDDs [default = %s]\n", pParams->fUseBdds? "yes": "no" );  
     fprintf( pErr, "\t-v     : prints verbose information [default = %s]\n", pParams->fVerbose? "yes": "no" );  
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
diff --git a/src/base/abci/abcAttach.c b/src/base/abci/abcAttach.c
index 78573718..bf40e45b 100644
--- a/src/base/abci/abcAttach.c
+++ b/src/base/abci/abcAttach.c
@@ -387,13 +387,13 @@ void Abc_TruthPermute( char * pPerm, int nVars, unsigned * uTruthNode, unsigned
     nMints = (1 << nVars);
     for ( iMint = 0; iMint < nMints; iMint++ )
     {
-        if ( (uTruthNode[iMint/32] & (1 << (iMint%32))) == 0 )
+        if ( (uTruthNode[iMint>>5] & (1 << (iMint&31))) == 0 )
             continue;
         iMintPerm = 0;
         for ( v = 0; v < nVars; v++ )
             if ( iMint & (1 << v) )
                 iMintPerm |= (1 << pPerm[v]);
-        uTruthPerm[iMintPerm/32] |= (1 << (iMintPerm%32));     
+        uTruthPerm[iMintPerm>>5] |= (1 << (iMintPerm&31));     
     }
 }
 
diff --git a/src/base/abci/abcIvy.c b/src/base/abci/abcIvy.c
new file mode 100644
index 00000000..0108b520
--- /dev/null
+++ b/src/base/abci/abcIvy.c
@@ -0,0 +1,407 @@
+/**CFile****************************************************************
+
+  FileName    [abcIvy.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Strashing of the current network.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcIvy.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "dec.h"
+#include "ivy.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static Abc_Ntk_t *  Abc_NtkFromAig( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan );
+static Ivy_Man_t *  Abc_NtkToAig( Abc_Ntk_t * pNtkOld );
+
+static void         Abc_NtkStrashPerformAig( Abc_Ntk_t * pNtk, Ivy_Man_t * pMan );
+static Ivy_Obj_t *  Abc_NodeStrashAig( Ivy_Man_t * pMan, Abc_Obj_t * pNode );
+static Ivy_Obj_t *  Abc_NodeStrashAigSopAig( Ivy_Man_t * pMan, Abc_Obj_t * pNode, char * pSop );
+static Ivy_Obj_t *  Abc_NodeStrashAigExorAig( Ivy_Man_t * pMan, Abc_Obj_t * pNode, char * pSop );
+static Ivy_Obj_t *  Abc_NodeStrashAigFactorAig( Ivy_Man_t * pMan, Abc_Obj_t * pNode, char * pSop );
+extern char *       Mio_GateReadSop( void * pGate );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Gives the current ABC network to AIG manager for processing.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk )
+{
+    Ivy_Man_t * pMan;
+    Abc_Ntk_t * pNtkAig;
+    int fCleanup = 1;
+    int nNodes;
+
+    assert( !Abc_NtkIsNetlist(pNtk) );
+    assert( !Abc_NtkIsSeq(pNtk) );
+    if ( Abc_NtkIsBddLogic(pNtk) )
+    {
+        if ( !Abc_NtkBddToSop(pNtk, 0) )
+        {
+            printf( "Converting to SOPs has failed.\n" );
+            return NULL;
+        }
+    }
+    // print warning about choice nodes
+    if ( Abc_NtkGetChoiceNum( pNtk ) )
+        printf( "Warning: The choice nodes in the initial AIG are removed by strashing.\n" );
+
+    // convert to the AIG manager
+    pMan = Abc_NtkToAig( pNtk );
+
+    if ( !Ivy_ManCheck( pMan ) )
+    {
+        printf( "AIG check has failed.\n" );
+        Ivy_ManStop( pMan );
+        return NULL;
+    }
+
+
+//    Ivy_MffcTest( pMan );
+    Ivy_ManPrintStats( pMan );
+    Ivy_ManSeqRewrite( pMan, 0, 0 );
+    Ivy_ManPrintStats( pMan );
+
+    // convert from the AIG manager
+    pNtkAig = Abc_NtkFromAig( pNtk, pMan );
+    Ivy_ManStop( pMan );
+
+    // report the cleanup results
+    if ( fCleanup && (nNodes = Abc_AigCleanup(pNtkAig->pManFunc)) )
+        printf( "Warning: AIG cleanup removed %d nodes (this is not a bug).\n", nNodes );
+    // duplicate EXDC 
+    if ( pNtk->pExdc )
+        pNtkAig->pExdc = Abc_NtkDup( pNtk->pExdc );
+    // make sure everything is okay
+    if ( !Abc_NtkCheck( pNtkAig ) )
+    {
+        printf( "Abc_NtkStrash: The network check has failed.\n" );
+        Abc_NtkDelete( pNtkAig );
+        return NULL;
+    }
+    return pNtkAig;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Converts the network from the AIG manager into ABC.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkFromAig( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan )
+{
+    Vec_Int_t * vNodes;
+    Abc_Ntk_t * pNtk;
+    Abc_Obj_t * pObj, * pObjNew, * pFaninNew, * pFaninNew0, * pFaninNew1;
+    Ivy_Obj_t * pNode;
+    int i, Fanin;
+    // perform strashing
+    pNtk = Abc_NtkStartFrom( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG );
+    // transfer the pointers to the basic nodes
+    Ivy_ManConst1(pMan)->TravId = (Abc_NtkConst1(pNtk)->Id << 1);
+    Abc_NtkForEachCi( pNtkOld, pObj, i )
+        Ivy_ManPi(pMan, i)->TravId = (pObj->pCopy->Id << 1);
+    // rebuild the AIG
+    vNodes = Ivy_ManDfs( pMan );
+    Ivy_ManForEachNodeVec( pMan, vNodes, pNode, i )
+    {
+        // add the first fanins
+        Fanin = Ivy_ObjFanin0(pNode)->TravId;
+        pFaninNew0 = Abc_NtkObj( pNtk, Fanin >> 1 );
+        pFaninNew0 = Abc_ObjNotCond( pFaninNew0, Ivy_ObjFaninC0(pNode) ^ (Fanin&1) );
+        if ( Ivy_ObjIsBuf(pNode) )
+        {
+            pNode->TravId = (Abc_ObjRegular(pFaninNew0)->Id << 1) | Abc_ObjIsComplement(pFaninNew0);
+            continue;
+        }
+        // add the first second
+        Fanin = Ivy_ObjFanin1(pNode)->TravId;
+        pFaninNew1 = Abc_NtkObj( pNtk, Fanin >> 1 );
+        pFaninNew1 = Abc_ObjNotCond( pFaninNew1, Ivy_ObjFaninC1(pNode) ^ (Fanin&1) );
+        // create the new node
+        if ( Ivy_ObjIsExor(pNode) )
+            pObjNew = Abc_AigXor( pNtk->pManFunc, pFaninNew0, pFaninNew1 );
+        else
+            pObjNew = Abc_AigAnd( pNtk->pManFunc, pFaninNew0, pFaninNew1 );
+        pNode->TravId = (Abc_ObjRegular(pObjNew)->Id << 1) | Abc_ObjIsComplement(pObjNew);
+    }
+    Vec_IntFree( vNodes );
+    // connect the PO nodes
+    Abc_NtkForEachCo( pNtkOld, pObj, i )
+    {
+        pNode = Ivy_ManPo(pMan, i);
+        Fanin = Ivy_ObjFanin0(pNode)->TravId;
+        pFaninNew = Abc_NtkObj( pNtk, Fanin >> 1 );
+        pFaninNew = Abc_ObjNotCond( pFaninNew, Ivy_ObjFaninC0(pNode) ^ (Fanin&1) );
+        Abc_ObjAddFanin( pObj->pCopy, pFaninNew );
+    }
+    return pNtk;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Converts the network from the AIG manager into ABC.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ivy_Man_t * Abc_NtkToAig( Abc_Ntk_t * pNtkOld )
+{
+    Ivy_Man_t * pMan;
+    Abc_Obj_t * pObj;
+    Ivy_Obj_t * pFanin;
+    int i;
+    // create the manager
+    assert( Abc_NtkHasSop(pNtkOld) || Abc_NtkHasAig(pNtkOld) );
+    if ( Abc_NtkHasSop(pNtkOld) )
+        pMan = Ivy_ManStart( Abc_NtkCiNum(pNtkOld), Abc_NtkCoNum(pNtkOld), 3 * Abc_NtkGetLitNum(pNtkOld) + 10 );
+    else
+        pMan = Ivy_ManStart( Abc_NtkCiNum(pNtkOld), Abc_NtkCoNum(pNtkOld), 3 * Abc_NtkNodeNum(pNtkOld) + 10 );
+    // create the PIs
+    Abc_NtkConst1(pNtkOld)->pCopy = (Abc_Obj_t *)Ivy_ManConst1(pMan);
+    Abc_NtkForEachCi( pNtkOld, pObj, i )
+        pObj->pCopy = (Abc_Obj_t *)Ivy_ManPi(pMan, i);
+    // perform the conversion of the internal nodes
+    Abc_NtkStrashPerformAig( pNtkOld, pMan );
+    // create the POs
+    Abc_NtkForEachCo( pNtkOld, pObj, i )
+    {
+        pFanin = (Ivy_Obj_t *)Abc_ObjFanin0(pObj)->pCopy;
+        pFanin = Ivy_NotCond( pFanin, Abc_ObjFaninC0(pObj) );
+        Ivy_ObjConnect( Ivy_ManPo(pMan, i), pFanin );
+    }
+    Ivy_ManCleanup( pMan );
+    return pMan;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prepares the network for strashing.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkStrashPerformAig( Abc_Ntk_t * pNtk, Ivy_Man_t * pMan )
+{
+//    ProgressBar * pProgress;
+    Vec_Ptr_t * vNodes;
+    Abc_Obj_t * pNode;
+    int i;
+    vNodes = Abc_NtkDfs( pNtk, 0 );
+//    pProgress = Extra_ProgressBarStart( stdout, vNodes->nSize );
+    Vec_PtrForEachEntry( vNodes, pNode, i )
+    {
+//        Extra_ProgressBarUpdate( pProgress, i, NULL );
+        pNode->pCopy = (Abc_Obj_t *)Abc_NodeStrashAig( pMan, pNode );
+    }
+//    Extra_ProgressBarStop( pProgress );
+    Vec_PtrFree( vNodes );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Strashes one logic node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ivy_Obj_t * Abc_NodeStrashAig( Ivy_Man_t * pMan, Abc_Obj_t * pNode )
+{
+    int fUseFactor = 1;
+    char * pSop;
+    Ivy_Obj_t * pFanin0, * pFanin1;
+    extern int Abc_SopIsExorType( char * pSop );
+
+    assert( Abc_ObjIsNode(pNode) );
+
+    // consider the case when the graph is an AIG
+    if ( Abc_NtkIsStrash(pNode->pNtk) )
+    {
+        if ( Abc_NodeIsConst(pNode) )
+            return Ivy_ManConst1(pMan);
+        pFanin0 = (Ivy_Obj_t *)Abc_ObjFanin0(pNode)->pCopy;
+        pFanin0 = Ivy_NotCond( pFanin0, Abc_ObjFaninC0(pNode) );
+        pFanin1 = (Ivy_Obj_t *)Abc_ObjFanin1(pNode)->pCopy;
+        pFanin1 = Ivy_NotCond( pFanin1, Abc_ObjFaninC1(pNode) );
+        return Ivy_And( pFanin0, pFanin1 );
+    }
+
+    // get the SOP of the node
+    if ( Abc_NtkHasMapping(pNode->pNtk) )
+        pSop = Mio_GateReadSop(pNode->pData);
+    else
+        pSop = pNode->pData;
+
+    // consider the constant node
+    if ( Abc_NodeIsConst(pNode) )
+        return Ivy_NotCond( Ivy_ManConst1(pMan), Abc_SopIsConst0(pSop) );
+
+    // consider the special case of EXOR function
+    if ( Abc_SopIsExorType(pSop) )
+        return Abc_NodeStrashAigExorAig( pMan, pNode, pSop );
+
+    // decide when to use factoring
+    if ( fUseFactor && Abc_ObjFaninNum(pNode) > 2 && Abc_SopGetCubeNum(pSop) > 1 )
+        return Abc_NodeStrashAigFactorAig( pMan, pNode, pSop );
+    return Abc_NodeStrashAigSopAig( pMan, pNode, pSop );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Strashes one logic node using its SOP.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ivy_Obj_t * Abc_NodeStrashAigSopAig( Ivy_Man_t * pMan, Abc_Obj_t * pNode, char * pSop )
+{
+    Abc_Obj_t * pFanin;
+    Ivy_Obj_t * pAnd, * pSum;
+    char * pCube;
+    int i, nFanins;
+
+    // get the number of node's fanins
+    nFanins = Abc_ObjFaninNum( pNode );
+    assert( nFanins == Abc_SopGetVarNum(pSop) );
+    // go through the cubes of the node's SOP
+    pSum = Ivy_Not( Ivy_ManConst1(pMan) );
+    Abc_SopForEachCube( pSop, nFanins, pCube )
+    {
+        // create the AND of literals
+        pAnd = Ivy_ManConst1(pMan);
+        Abc_ObjForEachFanin( pNode, pFanin, i ) // pFanin can be a net
+        {
+            if ( pCube[i] == '1' )
+                pAnd = Ivy_And( pAnd, (Ivy_Obj_t *)pFanin->pCopy );
+            else if ( pCube[i] == '0' )
+                pAnd = Ivy_And( pAnd, Ivy_Not((Ivy_Obj_t *)pFanin->pCopy) );
+        }
+        // add to the sum of cubes
+        pSum = Ivy_Or( pSum, pAnd );
+    }
+    // decide whether to complement the result
+    if ( Abc_SopIsComplement(pSop) )
+        pSum = Ivy_Not(pSum);
+    return pSum;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Strashed n-input XOR function.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ivy_Obj_t * Abc_NodeStrashAigExorAig( Ivy_Man_t * pMan, Abc_Obj_t * pNode, char * pSop )
+{
+    Abc_Obj_t * pFanin;
+    Ivy_Obj_t * pSum;
+    int i, nFanins;
+    // get the number of node's fanins
+    nFanins = Abc_ObjFaninNum( pNode );
+    assert( nFanins == Abc_SopGetVarNum(pSop) );
+    // go through the cubes of the node's SOP
+    pSum = Ivy_Not( Ivy_ManConst1(pMan) );
+    for ( i = 0; i < nFanins; i++ )
+    {
+        pFanin = Abc_ObjFanin( pNode, i );
+        pSum = Ivy_Exor( pSum, (Ivy_Obj_t *)pFanin->pCopy );
+    }
+    if ( Abc_SopIsComplement(pSop) )
+        pSum = Ivy_Not(pSum);
+    return pSum;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Strashes one logic node using its SOP.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ivy_Obj_t * Abc_NodeStrashAigFactorAig( Ivy_Man_t * pMan, Abc_Obj_t * pRoot, char * pSop )
+{
+    Dec_Graph_t * pFForm;
+    Dec_Node_t * pNode;
+    Ivy_Obj_t * pAnd;
+    int i;
+
+//    extern Ivy_Obj_t * Dec_GraphToNetworkAig( Ivy_Man_t * pMan, Dec_Graph_t * pGraph );
+    extern Ivy_Obj_t * Dec_GraphToNetworkIvy( Ivy_Man_t * pMan, Dec_Graph_t * pGraph );
+
+//    assert( 0 );
+
+    // perform factoring
+    pFForm = Dec_Factor( pSop );
+    // collect the fanins
+    Dec_GraphForEachLeaf( pFForm, pNode, i )
+        pNode->pFunc = Abc_ObjFanin(pRoot,i)->pCopy;
+    // perform strashing
+//    pAnd = Dec_GraphToNetworkAig( pMan, pFForm );
+    pAnd = Dec_GraphToNetworkIvy( pMan, pFForm );
+//    pAnd = NULL;
+
+    Dec_GraphFree( pFForm );
+    return pAnd;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abci/abcMiter.c b/src/base/abci/abcMiter.c
index 490cf0c6..ecd44017 100644
--- a/src/base/abci/abcMiter.c
+++ b/src/base/abci/abcMiter.c
@@ -81,7 +81,7 @@ Abc_Ntk_t * Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb )
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkMiterInt( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb )
 {
-    char Buffer[100];
+    char Buffer[1000];
     Abc_Ntk_t * pNtkMiter;
 
     assert( Abc_NtkIsStrash(pNtk1) );
@@ -168,16 +168,12 @@ void Abc_NtkMiterPrepare( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtk
         Abc_NtkForEachLatch( pNtk1, pObj, i )
         {
             pObjNew = Abc_NtkDupObj( pNtkMiter, pObj );
-            Vec_PtrPush( pNtkMiter->vCis, pObjNew );
-            Vec_PtrPush( pNtkMiter->vCos, pObjNew );
             // add name
             Abc_NtkLogicStoreNamePlus( pObjNew, Abc_ObjName(pObj), "_1" );
         }
         Abc_NtkForEachLatch( pNtk2, pObj, i )
         {
             pObjNew = Abc_NtkDupObj( pNtkMiter, pObj );
-            Vec_PtrPush( pNtkMiter->vCis, pObjNew );
-            Vec_PtrPush( pNtkMiter->vCos, pObjNew );
             // add name
             Abc_NtkLogicStoreNamePlus( pObjNew, Abc_ObjName(pObj), "_2" );
         }
@@ -295,7 +291,7 @@ void Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNt
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkMiterAnd( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 )
 {
-    char Buffer[100];
+    char Buffer[1000];
     Abc_Ntk_t * pNtkMiter;
     Abc_Obj_t * pOutput1, * pOutput2;
     Abc_Obj_t * pRoot1, * pRoot2, * pMiter;
@@ -352,7 +348,7 @@ Abc_Ntk_t * Abc_NtkMiterAnd( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 )
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkMiterCofactor( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues )
 {
-    char Buffer[100];
+    char Buffer[1000];
     Abc_Ntk_t * pNtkMiter;
     Abc_Obj_t * pRoot, * pOutput1;
     int Value, i;
@@ -418,7 +414,7 @@ Abc_Ntk_t * Abc_NtkMiterCofactor( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues )
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkMiterForCofactors( Abc_Ntk_t * pNtk, int Out, int In1, int In2 )
 {
-    char Buffer[100];
+    char Buffer[1000];
     Abc_Ntk_t * pNtkMiter;
     Abc_Obj_t * pRoot, * pOutput1, * pOutput2, * pMiter;
 
@@ -665,7 +661,7 @@ void Abc_NtkMiterReport( Abc_Ntk_t * pMiter )
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fInitial )
 {
-    char Buffer[100];
+    char Buffer[1000];
     ProgressBar * pProgress;
     Abc_Ntk_t * pNtkFrames;
     Abc_Obj_t * pLatch, * pLatchNew;
@@ -717,8 +713,6 @@ Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fInitial )
         {
             pLatchNew = Abc_NtkLatch(pNtkFrames, i);
             Abc_ObjAddFanin( pLatchNew, pLatch->pCopy );
-            Vec_PtrPush( pNtkFrames->vCis, pLatchNew );
-            Vec_PtrPush( pNtkFrames->vCos, pLatchNew );
             Abc_NtkLogicStoreName( pLatchNew, Abc_ObjName(pLatch) );
         }
     }
@@ -728,6 +722,9 @@ Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fInitial )
     // remove dangling nodes
     Abc_AigCleanup( pNtkFrames->pManFunc );
 
+    // reorder the latches
+    Abc_NtkOrderCisCos( pNtkFrames );
+
     // make sure that everything is okay
     if ( !Abc_NtkCheck( pNtkFrames ) )
     {
@@ -773,6 +770,12 @@ void Abc_NtkAddFrame( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame )
         Abc_NtkLogicStoreNamePlus( Abc_NtkDupObj(pNtkFrames, pNode), Abc_ObjName(pNode), Buffer );
         Abc_ObjAddFanin( pNode->pCopy, Abc_ObjChild0Copy(pNode) );
     }
+    // add the new asserts
+    Abc_NtkForEachAssert( pNtk, pNode, i )
+    {
+        Abc_NtkLogicStoreNamePlus( Abc_NtkDupObj(pNtkFrames, pNode), Abc_ObjName(pNode), Buffer );
+        Abc_ObjAddFanin( pNode->pCopy, Abc_ObjChild0Copy(pNode) );
+    }
     // transfer the implementation of the latch drivers to the latches
     Abc_NtkForEachLatch( pNtk, pLatch, i )
         pLatch->pNext = Abc_ObjChild0Copy(pLatch);
@@ -795,7 +798,7 @@ void Abc_NtkAddFrame( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame )
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkFrames2( Abc_Ntk_t * pNtk, int nFrames, int fInitial, AddFrameMapping addFrameMapping, void* arg )
 {
-    char Buffer[100];
+    char Buffer[1000];
     ProgressBar * pProgress;
     Abc_Ntk_t * pNtkFrames;
     Vec_Ptr_t * vNodes;
@@ -854,9 +857,6 @@ Abc_Ntk_t * Abc_NtkFrames2( Abc_Ntk_t * pNtk, int nFrames, int fInitial, AddFram
         {
             pLatchNew = Abc_NtkLatch(pNtkFrames, i);
             Abc_ObjAddFanin( pLatchNew, pLatch->pCopy );
-
-            Vec_PtrPush( pNtkFrames->vCis, pLatchNew );
-            Vec_PtrPush( pNtkFrames->vCos, pLatchNew );
             Abc_NtkLogicStoreName( pLatchNew, Abc_ObjName(pLatch) );
         }
     }
@@ -865,6 +865,9 @@ Abc_Ntk_t * Abc_NtkFrames2( Abc_Ntk_t * pNtk, int nFrames, int fInitial, AddFram
 
     // remove dangling nodes
     Abc_AigCleanup( pNtkFrames->pManFunc );
+
+    // reorder the latches
+    Abc_NtkOrderCisCos( pNtkFrames );
     
     // make sure that everything is okay
     if ( !Abc_NtkCheck( pNtkFrames ) )
diff --git a/src/base/abci/abcMv.c b/src/base/abci/abcMv.c
new file mode 100644
index 00000000..2858b8a7
--- /dev/null
+++ b/src/base/abci/abcMv.c
@@ -0,0 +1,369 @@
+/**CFile****************************************************************
+
+  FileName    [abcMv.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Multi-valued decomposition.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcMv.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Mv_Man_t_ Mv_Man_t;
+struct Mv_Man_t_
+{
+    int         nInputs;          // the number of 4-valued input variables
+    int         nFuncs;           // the number of 4-valued functions
+    DdManager * dd;               // representation of functions
+    DdNode *    bValues[15][4];   // representation of i-sets
+    DdNode *    bValueDcs[15][4]; // representation of i-sets don't-cares
+    DdNode *    bFuncs[15];       // representation of functions
+};
+
+static void     Abc_MvDecompose( Mv_Man_t * p );
+static void     Abc_MvPrintStats( Mv_Man_t * p );
+static void     Abc_MvRead( Mv_Man_t * p );
+static void     Abc_MvDeref( Mv_Man_t * p );
+static DdNode * Abc_MvReadCube( DdManager * dd, char * pLine, int nVars );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_MvExperiment()
+{
+    Mv_Man_t * p;
+    // get the functions
+    p = ALLOC( Mv_Man_t, 1 );
+    memset( p, 0, sizeof(Mv_Man_t) );
+    p->dd = Cudd_Init( 32, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+    p->nFuncs  = 15;
+    p->nInputs =  9;
+    Abc_MvRead( p );
+    // process the functions
+    Abc_MvPrintStats( p );
+//    Cudd_ReduceHeap( p->dd, CUDD_REORDER_SYMM_SIFT, 1 );
+//    Abc_MvPrintStats( p );
+    // try detecting support reducing bound set
+    Abc_MvDecompose( p );
+
+    // remove the manager
+    Abc_MvDeref( p );
+    Extra_StopManager( p->dd );
+    free( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_MvPrintStats( Mv_Man_t * p )
+{
+    int i, v;
+    for ( i = 0; i < 15; i++ )
+    {
+        printf( "%2d : ", i );
+        printf( "%3d (%2d)    ", Cudd_DagSize(p->bFuncs[i])-1, Cudd_SupportSize(p->dd, p->bFuncs[i]) );
+        for ( v = 0; v < 4; v++ )
+            printf( "%d = %3d (%2d)  ", v, Cudd_DagSize(p->bValues[i][v])-1, Cudd_SupportSize(p->dd, p->bValues[i][v]) );
+        printf( "\n" );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Abc_MvReadCube( DdManager * dd, char * pLine, int nVars )
+{
+    DdNode * bCube, * bVar, * bTemp;
+    int i;
+    bCube = Cudd_ReadOne(dd);  Cudd_Ref( bCube );
+    for ( i = 0; i < nVars; i++ )
+    {
+        if ( pLine[i] == '-' )
+            continue;
+        else if ( pLine[i] == '0' ) // 0
+            bVar = Cudd_Not( Cudd_bddIthVar(dd, 29-i) );
+        else if ( pLine[i] == '1' ) // 1
+            bVar = Cudd_bddIthVar(dd, 29-i);
+        else assert(0);
+        bCube = Cudd_bddAnd( dd, bTemp = bCube, bVar );  Cudd_Ref( bCube );
+        Cudd_RecursiveDeref( dd, bTemp );
+    }
+    Cudd_Deref( bCube );
+    return bCube;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_MvRead( Mv_Man_t * p )
+{
+    FILE * pFile;
+    char Buffer[1000], * pLine;
+    DdNode * bCube, * bTemp, * bProd, * bVar0, * bVar1, * bCubeSum;
+    int i, v;
+
+    // start the cube
+    bCubeSum = Cudd_ReadLogicZero(p->dd);  Cudd_Ref( bCubeSum );
+
+    // start the values
+    for ( i = 0; i < 15; i++ )
+    for ( v = 0; v < 4; v++ )
+    {
+        p->bValues[i][v]   = Cudd_ReadLogicZero(p->dd);  Cudd_Ref( p->bValues[i][v] );
+        p->bValueDcs[i][v] = Cudd_ReadLogicZero(p->dd);  Cudd_Ref( p->bValueDcs[i][v] );
+    }
+
+    // read the file
+    pFile = fopen( "input.pla", "r" );
+    while ( fgets( Buffer, 1000, pFile ) )
+    {
+        if ( Buffer[0] == '#' )
+            continue;
+        if ( Buffer[0] == '.' )
+        {
+            if ( Buffer[1] == 'e' )
+                break;
+            continue;
+        }
+
+        // get the cube 
+        bCube = Abc_MvReadCube( p->dd, Buffer, 18 );  Cudd_Ref( bCube );
+
+        // add it to the values of the output functions
+        pLine = Buffer + 19;
+        for ( i = 0; i < 15; i++ )
+        {
+            if ( pLine[2*i] == '-' && pLine[2*i+1] == '-' )
+            {
+                for ( v = 0; v < 4; v++ )
+                {
+                    p->bValueDcs[i][v] = Cudd_bddOr( p->dd, bTemp = p->bValueDcs[i][v], bCube );  Cudd_Ref( p->bValueDcs[i][v] );
+                    Cudd_RecursiveDeref( p->dd, bTemp );
+                }
+                continue;
+            }
+            else if ( pLine[2*i] == '0' && pLine[2*i+1] == '0' ) // 0
+                v = 0;
+            else if ( pLine[2*i] == '1' && pLine[2*i+1] == '0' ) // 1
+                v = 1;
+            else if ( pLine[2*i] == '0' && pLine[2*i+1] == '1' ) // 2
+                v = 2;
+            else if ( pLine[2*i] == '1' && pLine[2*i+1] == '1' ) // 3
+                v = 3;
+            else assert( 0 );
+            // add the value
+            p->bValues[i][v] = Cudd_bddOr( p->dd, bTemp = p->bValues[i][v], bCube );  Cudd_Ref( p->bValues[i][v] );
+            Cudd_RecursiveDeref( p->dd, bTemp );
+        }
+
+        // add the cube
+        bCubeSum = Cudd_bddOr( p->dd, bTemp = bCubeSum, bCube );  Cudd_Ref( bCubeSum );
+        Cudd_RecursiveDeref( p->dd, bTemp );
+        Cudd_RecursiveDeref( p->dd, bCube );
+    }
+
+    // add the complement of the domain to all values
+    for ( i = 0; i < 15; i++ )
+        for ( v = 0; v < 4; v++ )
+        {
+            if ( p->bValues[i][v] == Cudd_Not(Cudd_ReadOne(p->dd)) )
+                continue;
+            p->bValues[i][v] = Cudd_bddOr( p->dd, bTemp = p->bValues[i][v], p->bValueDcs[i][v] );  Cudd_Ref( p->bValues[i][v] );
+            Cudd_RecursiveDeref( p->dd, bTemp );
+            p->bValues[i][v] = Cudd_bddOr( p->dd, bTemp = p->bValues[i][v], Cudd_Not(bCubeSum) );  Cudd_Ref( p->bValues[i][v] );
+            Cudd_RecursiveDeref( p->dd, bTemp );
+        }
+    printf( "Domain = %5.2f %%.\n", 100.0*Cudd_CountMinterm(p->dd, bCubeSum, 32)/Cudd_CountMinterm(p->dd, Cudd_ReadOne(p->dd), 32) ); 
+    Cudd_RecursiveDeref( p->dd, bCubeSum );
+
+    // create each output function
+    for ( i = 0; i < 15; i++ )
+    {
+        p->bFuncs[i] = Cudd_ReadLogicZero(p->dd);  Cudd_Ref( p->bFuncs[i] );
+        for ( v = 0; v < 4; v++ )
+        {
+            bVar0 = Cudd_NotCond( Cudd_bddIthVar(p->dd, 30), ((v & 1) == 0) );
+            bVar1 = Cudd_NotCond( Cudd_bddIthVar(p->dd, 31), ((v & 2) == 0) );
+            bCube = Cudd_bddAnd( p->dd, bVar0, bVar1 );             Cudd_Ref( bCube );
+            bProd = Cudd_bddAnd( p->dd, p->bValues[i][v], bCube );  Cudd_Ref( bProd );
+            Cudd_RecursiveDeref( p->dd, bCube );
+            // add the value
+            p->bFuncs[i] = Cudd_bddOr( p->dd, bTemp = p->bFuncs[i], bProd );  Cudd_Ref( p->bFuncs[i] );
+            Cudd_RecursiveDeref( p->dd, bTemp );
+            Cudd_RecursiveDeref( p->dd, bProd );
+        }
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_MvDeref( Mv_Man_t * p )
+{
+    int i, v;
+    for ( i = 0; i < 15; i++ )
+    for ( v = 0; v < 4; v++ )
+    {
+        Cudd_RecursiveDeref( p->dd, p->bValues[i][v] );
+        Cudd_RecursiveDeref( p->dd, p->bValueDcs[i][v] );
+    }
+    for ( i = 0; i < 15; i++ )
+        Cudd_RecursiveDeref( p->dd, p->bFuncs[i] );
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_MvDecompose( Mv_Man_t * p )
+{
+    DdNode * bCofs[16], * bVarCube1, * bVarCube2, * bVarCube, * bCube, * bVar0, * bVar1;//, * bRes;
+    int k, i1, i2, v1, v2;//, c1, c2, Counter;
+
+    bVar0 = Cudd_bddIthVar(p->dd, 30);
+    bVar1 = Cudd_bddIthVar(p->dd, 31);
+    bCube = Cudd_bddAnd( p->dd, bVar0, bVar1 );  Cudd_Ref( bCube );
+
+    for ( k = 0; k < p->nFuncs; k++ )
+    {
+        printf( "FUNCTION %d\n", k );
+        for ( i1 = 0; i1 < p->nFuncs; i1++ )
+        for ( i2 = i1+1; i2 < p->nFuncs; i2++ )
+        {
+            Vec_Ptr_t * vCofs;
+
+            for ( v1 = 0; v1 < 4; v1++ )
+            {
+                bVar0 = Cudd_NotCond( Cudd_bddIthVar(p->dd, 29-2*i1  ), ((v1 & 1) == 0) );
+                bVar1 = Cudd_NotCond( Cudd_bddIthVar(p->dd, 29-2*i1-1), ((v1 & 2) == 0) );
+                bVarCube1 = Cudd_bddAnd( p->dd, bVar0, bVar1 );  Cudd_Ref( bVarCube1 );
+                for ( v2 = 0; v2 < 4; v2++ )
+                {
+                    bVar0 = Cudd_NotCond( Cudd_bddIthVar(p->dd, 29-2*i2  ), ((v2 & 1) == 0) );
+                    bVar1 = Cudd_NotCond( Cudd_bddIthVar(p->dd, 29-2*i2-1), ((v2 & 2) == 0) );
+                    bVarCube2 = Cudd_bddAnd( p->dd, bVar0, bVar1 );         Cudd_Ref( bVarCube2 );
+                    bVarCube = Cudd_bddAnd( p->dd, bVarCube1, bVarCube2 );  Cudd_Ref( bVarCube );
+                    bCofs[v1 * 4 + v2] = Cudd_Cofactor( p->dd, p->bFuncs[k], bVarCube );  Cudd_Ref( bCofs[v1 * 4 + v2] );
+                    Cudd_RecursiveDeref( p->dd, bVarCube );
+                    Cudd_RecursiveDeref( p->dd, bVarCube2 );
+                }
+                Cudd_RecursiveDeref( p->dd, bVarCube1 );
+            }
+/*
+            // check the compatibility of cofactors
+            Counter = 0;
+            for ( c1 = 0; c1 < 16; c1++ )
+            {
+                for ( c2 = 0; c2 <= c1; c2++ )
+                    printf( " " );
+                for ( c2 = c1+1; c2 < 16; c2++ )
+                {
+                    bRes = Cudd_bddAndAbstract( p->dd, bCofs[c1], bCofs[c2], bCube );  Cudd_Ref( bRes );
+                    if ( bRes == Cudd_ReadOne(p->dd) )
+                    {
+                        printf( "+" );
+                        Counter++;
+                    }
+                    else
+                    {
+                        printf( " " );
+                    }
+                    Cudd_RecursiveDeref( p->dd, bRes );
+                }
+                printf( "\n" );
+            }
+*/
+
+            vCofs = Vec_PtrAlloc( 16 );
+            for ( v1 = 0; v1 < 4; v1++ )
+            for ( v2 = 0; v2 < 4; v2++ )
+                Vec_PtrPushUnique( vCofs, bCofs[v1 * 4 + v2] );
+            printf( "%d ", Vec_PtrSize(vCofs) );
+            Vec_PtrFree( vCofs );
+
+            // free the cofactors
+            for ( v1 = 0; v1 < 4; v1++ )
+            for ( v2 = 0; v2 < 4; v2++ )
+                Cudd_RecursiveDeref( p->dd, bCofs[v1 * 4 + v2] );
+
+            printf( "\n" );
+//            printf( "%2d, %2d : %3d\n", i1, i2, Counter );
+        }
+    }
+
+    Cudd_RecursiveDeref( p->dd, bCube );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index 2aad721b..f95591ab 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -48,12 +48,15 @@
 ***********************************************************************/
 void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
 {
-    int Num, Num2;
+    int Num;//, Num2;
 
 //    Abc_NtkDetectMatching( pNtk );
 //    return;
     fprintf( pFile, "%-13s:",       pNtk->pName );
-    fprintf( pFile, " i/o = %4d/%4d", Abc_NtkPiNum(pNtk), Abc_NtkPoNum(pNtk) );
+    if ( Abc_NtkAssertNum(pNtk) )
+        fprintf( pFile, " i/o/a = %4d/%4d/%4d", Abc_NtkPiNum(pNtk), Abc_NtkPoNum(pNtk), Abc_NtkAssertNum(pNtk) );
+    else
+        fprintf( pFile, " i/o = %4d/%4d", Abc_NtkPiNum(pNtk), Abc_NtkPoNum(pNtk) );
 
     if ( !Abc_NtkIsSeq(pNtk) )
         fprintf( pFile, "  lat = %4d", Abc_NtkLatchNum(pNtk) );
diff --git a/src/base/abci/abcProve.c b/src/base/abci/abcProve.c
index 23315223..85a58c32 100644
--- a/src/base/abci/abcProve.c
+++ b/src/base/abci/abcProve.c
@@ -30,7 +30,7 @@ extern int  Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeros, i
 extern int  Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool fUpdateLevel, bool fUseZeros, bool fUseDcs, bool fVerbose );
 extern Abc_Ntk_t * Abc_NtkFromFraig( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk );
 
-static Abc_Ntk_t * Abc_NtkMiterFraig( Abc_Ntk_t * pNtk, int nBTLimit, int * pRetValue, int * pNumFails );
+static Abc_Ntk_t * Abc_NtkMiterFraig( Abc_Ntk_t * pNtk, int nBTLimit, sint64 nInspLimit, int * pRetValue, int * pNumFails, sint64 * pNumConfs, sint64 * pNumInspects );
 static void Abc_NtkMiterPrint( Abc_Ntk_t * pNtk, char * pString, int clk, int fVerbose );
 
 
@@ -56,13 +56,14 @@ int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pPars )
 {
     Prove_Params_t * pParams = pPars;
     Abc_Ntk_t * pNtk, * pNtkTemp;
-    int RetValue, nIter, Counter, clk, timeStart = clock();
+    int RetValue, nIter, nSatFails, Counter, clk, timeStart = clock();
+    sint64 nSatConfs, nSatInspects, nInspectLimit;
 
     // get the starting network
     pNtk = *ppNtk;
     assert( Abc_NtkIsStrash(pNtk) );
     assert( Abc_NtkPoNum(pNtk) == 1 );
-
+ 
     if ( pParams->fVerbose )
     {
         printf( "RESOURCE LIMITS: Iterations = %d. Rewriting = %s. Fraiging = %s.\n",
@@ -79,7 +80,7 @@ int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pPars )
     if ( !pParams->fUseRewriting && !pParams->fUseFraiging )
     {
         clk = clock();
-        RetValue = Abc_NtkMiterSat( pNtk, pParams->nMiteringLimitLast, 0, 0, 0 );
+        RetValue = Abc_NtkMiterSat( pNtk, (sint64)pParams->nMiteringLimitLast, (sint64)0, 0, 0, NULL, NULL );
         Abc_NtkMiterPrint( pNtk, "SAT solving", clk, pParams->fVerbose );
         *ppNtk = pNtk;
         return RetValue;
@@ -98,11 +99,24 @@ int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pPars )
 
         // try brute-force SAT
         clk = clock();
-        RetValue = Abc_NtkMiterSat( pNtk, (int)(pParams->nMiteringLimitStart * pow(pParams->nMiteringLimitMulti,nIter)), 0, 0, 0 );
+        nInspectLimit = pParams->nTotalInspectLimit? pParams->nTotalInspectLimit - pParams->nTotalInspectsMade : 0;
+        RetValue = Abc_NtkMiterSat( pNtk, (sint64)(pParams->nMiteringLimitStart * pow(pParams->nMiteringLimitMulti,nIter)), (sint64)nInspectLimit, 0, 0, &nSatConfs, &nSatInspects );
         Abc_NtkMiterPrint( pNtk, "SAT solving", clk, pParams->fVerbose );
         if ( RetValue >= 0 )
             break;
 
+        // add to the number of backtracks and inspects
+        pParams->nTotalBacktracksMade += nSatConfs;
+        pParams->nTotalInspectsMade   += nSatInspects;
+        // check if global resource limit is reached
+        if ( (pParams->nTotalBacktrackLimit && pParams->nTotalBacktracksMade >= pParams->nTotalBacktrackLimit) ||
+             (pParams->nTotalInspectLimit   && pParams->nTotalInspectsMade   >= pParams->nTotalInspectLimit) )
+        {
+            printf( "Reached global limit on conflicts/inspects. Quitting.\n" );
+            *ppNtk = pNtk;
+            return -1;
+        }
+
         // try rewriting
         if ( pParams->fUseRewriting )
         {
@@ -131,18 +145,30 @@ int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pPars )
  
         if ( pParams->fUseFraiging )
         {
-            int nSatFails;
             // try FRAIGing
             clk = clock();
-            pNtk = Abc_NtkMiterFraig( pNtkTemp = pNtk, (int)(pParams->nFraigingLimitStart * pow(pParams->nFraigingLimitMulti,nIter)), &RetValue, &nSatFails );  Abc_NtkDelete( pNtkTemp );
+            nInspectLimit = pParams->nTotalInspectLimit? pParams->nTotalInspectLimit - pParams->nTotalInspectsMade : 0;
+            pNtk = Abc_NtkMiterFraig( pNtkTemp = pNtk, (int)(pParams->nFraigingLimitStart * pow(pParams->nFraigingLimitMulti,nIter)), nInspectLimit, &RetValue, &nSatFails, &nSatConfs, &nSatInspects );  Abc_NtkDelete( pNtkTemp );
             Abc_NtkMiterPrint( pNtk, "FRAIGing   ", clk, pParams->fVerbose );
 //            printf( "NumFails = %d\n", nSatFails );
             if ( RetValue >= 0 )
                 break;
+
+            // add to the number of backtracks and inspects
+            pParams->nTotalBacktracksMade += nSatConfs;
+            pParams->nTotalInspectsMade += nSatInspects;
+            // check if global resource limit is reached
+            if ( (pParams->nTotalBacktrackLimit && pParams->nTotalBacktracksMade >= pParams->nTotalBacktrackLimit) ||
+                 (pParams->nTotalInspectLimit   && pParams->nTotalInspectsMade   >= pParams->nTotalInspectLimit) )
+            {
+                printf( "Reached global limit on conflicts/inspects. Quitting.\n" );
+                *ppNtk = pNtk;
+                return -1;
+            }
         }
 
     }    
-/*
+
     // try to prove it using brute force SAT
     if ( RetValue < 0 && pParams->fUseBdds )
     {
@@ -162,7 +188,6 @@ int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pPars )
             pNtk = pNtkTemp;
         Abc_NtkMiterPrint( pNtk, "BDD building", clk, pParams->fVerbose );
     }
-*/
 
     if ( RetValue < 0 )
     {
@@ -172,7 +197,8 @@ int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pPars )
             fflush( stdout );
         }
         clk = clock();
-        RetValue = Abc_NtkMiterSat( pNtk, pParams->nMiteringLimitLast, 0, 0, 0 );
+        nInspectLimit = pParams->nTotalInspectLimit? pParams->nTotalInspectLimit - pParams->nTotalInspectsMade : 0;
+        RetValue = Abc_NtkMiterSat( pNtk, (sint64)pParams->nMiteringLimitLast, (sint64)nInspectLimit, 0, 0, NULL, NULL );
         Abc_NtkMiterPrint( pNtk, "SAT solving", clk, pParams->fVerbose );
     }
 
@@ -197,7 +223,7 @@ int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pPars )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkMiterFraig( Abc_Ntk_t * pNtk, int nBTLimit, int * pRetValue, int * pNumFails )
+Abc_Ntk_t * Abc_NtkMiterFraig( Abc_Ntk_t * pNtk, int nBTLimit, sint64 nInspLimit, int * pRetValue, int * pNumFails, sint64 * pNumConfs, sint64 * pNumInspects )
 {
     Abc_Ntk_t * pNtkNew;
     Fraig_Params_t Params, * pParams = &Params;
@@ -222,6 +248,7 @@ Abc_Ntk_t * Abc_NtkMiterFraig( Abc_Ntk_t * pNtk, int nBTLimit, int * pRetValue,
     pParams->fTryProve  = 0;              // do not try to prove the final miter
     pParams->fDoSparse  = 1;              // try proving sparse functions
     pParams->fVerbose   = 0;
+    pParams->nInspLimit = nInspLimit;
 
     // transform the target into a fraig
     pMan = Abc_NtkToFraig( pNtk, pParams, 0, 0 ); 
@@ -243,6 +270,8 @@ Abc_Ntk_t * Abc_NtkMiterFraig( Abc_Ntk_t * pNtk, int nBTLimit, int * pRetValue,
     // save the return values
     *pRetValue = RetValue;
     *pNumFails = Fraig_ManReadSatFails( pMan );
+    *pNumConfs = Fraig_ManReadConflicts( pMan );
+    *pNumInspects = Fraig_ManReadInspects( pMan );
 
     // delete the fraig manager
     Fraig_ManFree( pMan );
diff --git a/src/base/abci/abcRefactor.c b/src/base/abci/abcRefactor.c
index 9ea3ad71..3dd6c519 100644
--- a/src/base/abci/abcRefactor.c
+++ b/src/base/abci/abcRefactor.c
@@ -111,6 +111,9 @@ int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool
         // skip the constant node
         if ( Abc_NodeIsConst(pNode) )
             continue;
+        // skip persistant nodes
+        if ( Abc_NodeIsPersistant(pNode) )
+            continue;
         // skip the nodes with many fanouts
         if ( Abc_ObjFanoutNum(pNode) > 1000 )
             continue;
diff --git a/src/base/abci/abcRenode.c b/src/base/abci/abcRenode.c
index ea728858..f7d351d2 100644
--- a/src/base/abci/abcRenode.c
+++ b/src/base/abci/abcRenode.c
@@ -377,7 +377,7 @@ int Abc_NtkRenodeLimit( Abc_Obj_t * pNode, Vec_Ptr_t * vCone, int nFaninMax )
 ***********************************************************************/
 void Abc_NtkRenodeSetBounds( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax )
 {
-    Vec_Ptr_t * vCone = pNtk->vPtrTemp;
+    Vec_Ptr_t * vCone = Vec_PtrAlloc(10);
     Abc_Obj_t * pNode;
     int i, nFanouts, nConeSize;
 
@@ -414,6 +414,7 @@ void Abc_NtkRenodeSetBounds( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax )
         while ( Abc_NtkRenodeLimit(pNode, vCone, nFaninMax) );
         assert( vCone->nSize <= nFaninMax );  
     }
+    Vec_PtrFree(vCone);
 /*
     // make sure the fanin limit is met
     Abc_NtkForEachNode( pNtk, pNode, i )
diff --git a/src/base/abci/abcRestruct.c b/src/base/abci/abcRestruct.c
index 49208772..d738123a 100644
--- a/src/base/abci/abcRestruct.c
+++ b/src/base/abci/abcRestruct.c
@@ -134,6 +134,9 @@ pManRst->timeCut += clock() - clk;
         // skip the constant node
         if ( Abc_NodeIsConst(pNode) )
             continue;
+        // skip persistant nodes
+        if ( Abc_NodeIsPersistant(pNode) )
+            continue;
         // skip the node if it is inside the tree
 //        if ( Abc_ObjFanoutNum(pNode) < 2 )
 //            continue;
diff --git a/src/base/abci/abcResub.c b/src/base/abci/abcResub.c
index e9de4858..b0061b61 100644
--- a/src/base/abci/abcResub.c
+++ b/src/base/abci/abcResub.c
@@ -160,6 +160,9 @@ int Abc_NtkResubstitute( Abc_Ntk_t * pNtk, int nCutMax, int nStepsMax, bool fUpd
         // skip the constant node
         if ( Abc_NodeIsConst(pNode) )
             continue;
+        // skip persistant nodes
+        if ( Abc_NodeIsPersistant(pNode) )
+            continue;
         // skip the nodes with many fanouts
         if ( Abc_ObjFanoutNum(pNode) > 1000 )
             continue;
@@ -278,7 +281,7 @@ Abc_ManRes_t * Abc_ManResubStart( int nLeavesMax, int nDivsMax )
         pData = p->vSims->pArray[k];
         for ( i = 0; i < p->nBits; i++ )
             if ( i & (1 << k) )
-                pData[i/32] |= (1 << (i%32));
+                pData[i>>5] |= (1 << (i&31));
     }
     // create the remaining divisors
     p->vDivs1UP  = Vec_PtrAlloc( p->nDivsMax );
diff --git a/src/base/abci/abcRewrite.c b/src/base/abci/abcRewrite.c
index f11e5e9d..703f05d9 100644
--- a/src/base/abci/abcRewrite.c
+++ b/src/base/abci/abcRewrite.c
@@ -34,6 +34,7 @@
 
 static Cut_Man_t * Abc_NtkStartCutManForRewrite( Abc_Ntk_t * pNtk );
 static void        Abc_NodePrintCuts( Abc_Obj_t * pNode );
+static void        Abc_ManShowCutCone( Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -87,15 +88,39 @@ Rwr_ManAddTimeCuts( pManRwr, clock() - clk );
         // skip the constant node
         if ( Abc_NodeIsConst(pNode) )
             continue;
+        // skip persistant nodes
+        if ( Abc_NodeIsPersistant(pNode) )
+            continue;
         // skip the nodes with many fanouts
         if ( Abc_ObjFanoutNum(pNode) > 1000 )
             continue;
+//printf( "*******Node %d: \n", pNode->Id );
+
         // for each cut, try to resynthesize it
         nGain = Rwr_NodeRewrite( pManRwr, pManCut, pNode, fUpdateLevel, fUseZeros );
         if ( nGain > 0 || nGain == 0 && fUseZeros )
         {
+//            extern void Abc_RwrExpWithCut( Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves );
+
             Dec_Graph_t * pGraph = Rwr_ManReadDecs(pManRwr);
             int fCompl           = Rwr_ManReadCompl(pManRwr);
+
+//            Abc_RwrExpWithCut( pNode, Rwr_ManReadLeaves(pManRwr) );
+
+/*
+            {
+                Abc_Obj_t * pObj;
+                int i;
+                printf( "USING: (" );
+                Vec_PtrForEachEntry( Rwr_ManReadLeaves(pManRwr), pObj, i )
+                    printf( "%d ", Abc_ObjFanoutNum(Abc_ObjRegular(pObj)) );
+                printf( ")   Gain = %d.\n", nGain );
+            }
+*/
+            
+//            if ( nGain > 0 )
+//                Abc_ManShowCutCone( pNode, Rwr_ManReadLeaves(pManRwr) );
+
 /*
             if ( nGain > 0 )
             { // print stats on the MFFC
@@ -209,6 +234,163 @@ void Abc_NodePrintCuts( Abc_Obj_t * pNode )
     }
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_ManRewritePrintDivs( Vec_Ptr_t * vDivs, int nLeaves )
+{
+    Abc_Obj_t * pFanin, * pNode, * pRoot;
+    int i, k;
+    pRoot = Vec_PtrEntryLast(vDivs);
+    // print the nodes
+    Vec_PtrForEachEntry( vDivs, pNode, i )
+    {
+        if ( i < nLeaves )
+        {
+            printf( "%6d : %c\n", pNode->Id, 'a'+i );
+            continue;
+        }
+        printf( "%6d : %2d = ", pNode->Id, i );
+        // find the first fanin
+        Vec_PtrForEachEntry( vDivs, pFanin, k )
+            if ( Abc_ObjFanin0(pNode) == pFanin )
+                break;
+        if ( k < nLeaves )
+            printf( "%c", 'a' + k );
+        else
+            printf( "%d", k );
+        printf( "%s ", Abc_ObjFaninC0(pNode)? "\'" : "" );
+        // find the second fanin
+        Vec_PtrForEachEntry( vDivs, pFanin, k )
+            if ( Abc_ObjFanin1(pNode) == pFanin )
+                break;
+        if ( k < nLeaves )
+            printf( "%c", 'a' + k );
+        else
+            printf( "%d", k );
+        printf( "%s ", Abc_ObjFaninC1(pNode)? "\'" : "" );
+        if ( pNode == pRoot )
+            printf( " root" );
+        printf( "\n" );
+    }
+    printf( "\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_ManShowCutCone_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vDivs )
+{
+    if ( Abc_NodeIsTravIdCurrent(pNode) )
+        return;
+    Abc_NodeSetTravIdCurrent(pNode);
+    Abc_ManShowCutCone_rec( Abc_ObjFanin0(pNode), vDivs );
+    Abc_ManShowCutCone_rec( Abc_ObjFanin1(pNode), vDivs );
+    Vec_PtrPush( vDivs, pNode );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_ManShowCutCone( Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves )
+{
+    Abc_Ntk_t * pNtk = pNode->pNtk;
+    Abc_Obj_t * pObj;
+    Vec_Ptr_t * vDivs;
+    int i;
+    vDivs = Vec_PtrAlloc( 100 );
+    Abc_NtkIncrementTravId( pNtk );
+    Vec_PtrForEachEntry( vLeaves, pObj, i )
+    {
+        Abc_NodeSetTravIdCurrent( Abc_ObjRegular(pObj) );
+        Vec_PtrPush( vDivs, Abc_ObjRegular(pObj) );
+    }
+    Abc_ManShowCutCone_rec( pNode, vDivs );
+    Abc_ManRewritePrintDivs( vDivs, Vec_PtrSize(vLeaves) );
+    Vec_PtrFree( vDivs );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_RwrExpWithCut_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves, int fUseA )
+{
+    if ( Vec_PtrFind(vLeaves, pNode) >= 0 || Vec_PtrFind(vLeaves, Abc_ObjNot(pNode)) >= 0 )
+    {
+        if ( fUseA )
+            Abc_ObjRegular(pNode)->fMarkA = 1;
+        else
+            Abc_ObjRegular(pNode)->fMarkB = 1;
+        return;
+    }
+    assert( Abc_ObjIsNode(pNode) );
+    Abc_RwrExpWithCut_rec( Abc_ObjFanin0(pNode), vLeaves, fUseA );
+    Abc_RwrExpWithCut_rec( Abc_ObjFanin1(pNode), vLeaves, fUseA );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_RwrExpWithCut( Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves )
+{
+    Abc_Obj_t * pObj;
+    int i, CountA, CountB;
+    Abc_RwrExpWithCut_rec( Abc_ObjFanin0(pNode), vLeaves, 1 );
+    Abc_RwrExpWithCut_rec( Abc_ObjFanin1(pNode), vLeaves, 0 );
+    CountA = CountB = 0;
+    Vec_PtrForEachEntry( vLeaves, pObj, i )
+    {
+        CountA += Abc_ObjRegular(pObj)->fMarkA;
+        CountB += Abc_ObjRegular(pObj)->fMarkB;
+        Abc_ObjRegular(pObj)->fMarkA = 0;
+        Abc_ObjRegular(pObj)->fMarkB = 0;
+    }
+    printf( "(%d,%d:%d) ", CountA, CountB, CountA+CountB-Vec_PtrSize(vLeaves) );
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcRr.c b/src/base/abci/abcRr.c
index a9c61e1a..b3788d31 100644
--- a/src/base/abci/abcRr.c
+++ b/src/base/abci/abcRr.c
@@ -105,6 +105,9 @@ int Abc_NtkRR( Abc_Ntk_t * pNtk, int nFaninLevels, int nFanoutLevels, int fUseFa
     p->nFanoutLevels = nFanoutLevels;
     p->nNodesOld     = Abc_NtkNodeNum(pNtk);
     p->nLevelsOld    = Abc_AigGetLevelNum(pNtk);
+    // remember latch values
+    Abc_NtkForEachLatch( pNtk, pNode, i )
+        pNode->pNext = pNode->pData;
     // go through the nodes
     Abc_NtkCleanCopy(pNtk);
     nNodes = Abc_NtkObjNumMax(pNtk);
@@ -119,6 +122,9 @@ int Abc_NtkRR( Abc_Ntk_t * pNtk, int nFaninLevels, int nFanoutLevels, int fUseFa
         // skip the constant node
         if ( Abc_NodeIsConst(pNode) )
             continue;
+        // skip persistant nodes
+        if ( Abc_NodeIsPersistant(pNode) )
+            continue;
         // skip the nodes with many fanouts
         if ( Abc_ObjFanoutNum(pNode) > 1000 )
             continue;
@@ -209,6 +215,9 @@ int Abc_NtkRR( Abc_Ntk_t * pNtk, int nFaninLevels, int nFanoutLevels, int fUseFa
     if ( fVerbose )
         Abc_RRManPrintStats( p );
     Abc_RRManStop( p );
+    // restore latch values
+    Abc_NtkForEachLatch( pNtk, pNode, i )
+        pNode->pData = pNode->pNext, pNode->pNext = NULL;
     // put the nodes into the DFS order and reassign their IDs
     Abc_NtkReassignIds( pNtk );
     Abc_NtkGetLevelNum( pNtk );
@@ -692,6 +701,7 @@ Abc_Ntk_t * Abc_NtkWindow( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vC
     // add the PI/PO names
     Abc_NtkAddDummyPiNames( pNtkNew );
     Abc_NtkAddDummyPoNames( pNtkNew );
+    Abc_NtkAddDummyAssertNames( pNtkNew );
     // check
     if ( fCheck && !Abc_NtkCheck( pNtkNew ) )
     {
diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c
index 06376eed..b21278f7 100644
--- a/src/base/abci/abcSat.c
+++ b/src/base/abci/abcSat.c
@@ -42,12 +42,17 @@ static nMuxes;
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nConfLimit, int nImpLimit, int fJFront, int fVerbose )
+int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fJFront, int fVerbose, sint64 * pNumConfs, sint64 * pNumInspects )
 {
     solver * pSat;
     lbool   status;
     int RetValue, clk;
 
+    if ( pNumConfs )
+        *pNumConfs = 0;
+    if ( pNumInspects )
+        *pNumInspects = 0;
+
     assert( Abc_NtkIsStrash(pNtk) );
     assert( Abc_NtkLatchNum(pNtk) == 0 );
 
@@ -78,7 +83,7 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nConfLimit, int nImpLimit, int fJFron
     clk = clock();
     if ( fVerbose )
         pSat->verbosity = 1;
-    status = solver_solve( pSat, NULL, NULL, nConfLimit, nImpLimit );
+    status = solver_solve( pSat, NULL, NULL, (sint64)nConfLimit, (sint64)nInsLimit );
     if ( status == l_Undef )
     {
 //        printf( "The problem timed out.\n" );
@@ -97,6 +102,7 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nConfLimit, int nImpLimit, int fJFron
     else
         assert( 0 );
 //    PRT( "SAT solver time", clock() - clk );
+//    printf( "The number of conflicts = %d.\n", (int)pSat->solver_stats.conflicts );
 
     // if the problem is SAT, get the counterexample
     if ( status == l_True )
@@ -109,6 +115,12 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nConfLimit, int nImpLimit, int fJFron
     // free the solver
     if ( fVerbose )
         Asat_SatPrintStats( stdout, pSat );
+
+    if ( pNumConfs )
+        *pNumConfs = (int)pSat->solver_stats.conflicts;
+    if ( pNumInspects )
+        *pNumInspects = (int)pSat->solver_stats.inspects;
+
     solver_delete( pSat );
     return RetValue;
 }
@@ -401,6 +413,7 @@ int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk, int fJFront )
     Vec_Vec_t * vCircuit;
     int i, k, fUseMuxes = 1;
     int clk1 = clock(), clk;
+    int fOrderCiVarsFirst = 0;
 
     assert( Abc_NtkIsStrash(pNtk) );
 
@@ -431,6 +444,7 @@ int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk, int fJFront )
         Vec_PtrPush( vNodes, pNode );
     }
 */
+
     // collect the nodes that need clauses and top-level assignments
     Abc_NtkForEachCo( pNtk, pNode, i )
     {
@@ -526,6 +540,21 @@ int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk, int fJFront )
         }
     }
 
+    // set preferred variables
+    if ( fOrderCiVarsFirst )
+    {
+        int * pPrefVars = ALLOC( int, Abc_NtkCiNum(pNtk) );
+        int nVars = 0;
+        Abc_NtkForEachCi( pNtk, pNode, i )
+        {
+            if ( pNode->fMarkA == 0 )
+                continue;
+            pPrefVars[nVars++] = (int)pNode->pCopy;
+        }
+        nVars = ABC_MIN( nVars, 10 );
+        Asat_SolverSetPrefVars( pSat, pPrefVars, nVars );
+    }
+
     // create the variable order
     if ( fJFront )
     {
diff --git a/src/base/abci/abcSweep.c b/src/base/abci/abcSweep.c
index 08236edc..3665584e 100644
--- a/src/base/abci/abcSweep.c
+++ b/src/base/abci/abcSweep.c
@@ -571,12 +571,13 @@ int Abc_NtkSweep( Abc_Ntk_t * pNtk, int fVerbose )
 ***********************************************************************/
 void Abc_NodeSweep( Abc_Obj_t * pNode, int fVerbose )
 {
-    Vec_Ptr_t * vFanout = pNode->pNtk->vPtrTemp;
     Abc_Obj_t * pFanout, * pDriver;
+    Vec_Ptr_t * vFanout;
     int i;
     assert( Abc_ObjFaninNum(pNode) < 2 );
     assert( Abc_ObjFanoutNum(pNode) > 0 );
     // iterate through the fanouts
+    vFanout = Vec_PtrAlloc( Abc_ObjFanoutNum(pNode) );
     Abc_NodeCollectFanouts( pNode, vFanout );
     Vec_PtrForEachEntry( vFanout, pFanout, i )
     {
@@ -607,6 +608,7 @@ void Abc_NodeSweep( Abc_Obj_t * pNode, int fVerbose )
             Abc_ObjPatchFanin( pFanout, pNode, pDriver );
         }
     }
+    Vec_PtrFree( vFanout );
 }
 
 /**Function*************************************************************
diff --git a/src/base/abci/abcTrace.c b/src/base/abci/abcTrace.c
index 0275c0a1..4abe235e 100644
--- a/src/base/abci/abcTrace.c
+++ b/src/base/abci/abcTrace.c
@@ -148,7 +148,7 @@ void Abc_HManStart()
         pData = p->vSims->pArray[k];
         for ( i = 0; i < p->nBits; i++ )
             if ( i & (1 << k) )
-                pData[i/32] |= (1 << (i%32));
+                pData[i>>5] |= (1 << (i&31));
     }
     // allocate storage for the nodes
     p->pMmObj = Extra_MmFixedStart( sizeof(Abc_HObj_t) );
diff --git a/src/base/abci/abcVanEijk.c b/src/base/abci/abcVanEijk.c
index 8d8784e0..81423c30 100644
--- a/src/base/abci/abcVanEijk.c
+++ b/src/base/abci/abcVanEijk.c
@@ -544,8 +544,6 @@ Abc_Ntk_t * Abc_NtkVanEijkFrames( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCorresp, int nF
     {
         pLatchNew = Abc_NtkLatch(pNtkFrames, i);
         Abc_ObjAddFanin( pLatchNew, pLatch->pCopy );
-        Vec_PtrPush( pNtkFrames->vCis, pLatchNew );
-        Vec_PtrPush( pNtkFrames->vCos, pLatchNew );
         Abc_NtkLogicStoreName( pLatchNew, Abc_ObjName(pLatch) );
         pLatch->pNext = NULL;
     }
diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c
index e0c65058..d9478b04 100644
--- a/src/base/abci/abcVerify.c
+++ b/src/base/abci/abcVerify.c
@@ -44,7 +44,7 @@ static void  Abc_NtkVerifyReportErrorSeq( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2,
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nImpLimit )
+void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nInsLimit )
 {
     Abc_Ntk_t * pMiter;
     Abc_Ntk_t * pCnf;
@@ -85,7 +85,7 @@ void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nI
     }
 
     // solve the CNF using the SAT solver
-    RetValue = Abc_NtkMiterSat( pCnf, nConfLimit, nImpLimit, 0, 0 );
+    RetValue = Abc_NtkMiterSat( pCnf, (sint64)nConfLimit, (sint64)nInsLimit, 0, 0, NULL, NULL );
     if ( RetValue == -1 )
         printf( "Networks are undecided (SAT solver timed out).\n" );
     else if ( RetValue == 0 )
@@ -178,7 +178,14 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fV
     if ( RetValue == -1 )
         printf( "Networks are undecided (resource limits is reached).\n" );
     else if ( RetValue == 0 )
-        printf( "Networks are NOT EQUIVALENT.\n" );
+    {
+        int * pSimInfo = Abc_NtkVerifySimulatePattern( pMiter, pMiter->pModel );
+        if ( pSimInfo[0] != 1 )
+            printf( "ERROR in Abc_NtkMiterProve(): Generated counter-example is invalid.\n" );
+        else
+            printf( "Networks are NOT EQUIVALENT.\n" );
+        free( pSimInfo );
+    }
     else
         printf( "Networks are equivalent.\n" );
     if ( pMiter->pModel )
@@ -197,7 +204,7 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fV
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nImpLimit, int nFrames )
+void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nInsLimit, int nFrames )
 {
     Abc_Ntk_t * pMiter;
     Abc_Ntk_t * pFrames;
@@ -257,7 +264,7 @@ void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nI
     }
 
     // solve the CNF using the SAT solver
-    RetValue = Abc_NtkMiterSat( pCnf, nConfLimit, nImpLimit, 0, 0 );
+    RetValue = Abc_NtkMiterSat( pCnf, (sint64)nConfLimit, (sint64)nInsLimit, 0, 0, NULL, NULL );
     if ( RetValue == -1 )
         printf( "Networks are undecided (SAT solver timed out).\n" );
     else if ( RetValue == 0 )
@@ -709,6 +716,52 @@ void Abc_NtkVerifyReportErrorSeq( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pM
     if ( fRemove2 ) Abc_NtkDelete( pNtk2 );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Simulates buggy miter emailed by Mike.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkSimulteBuggyMiter( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj;
+    int i;
+    int * pModel1, * pModel2, * pResult1, * pResult2;
+    char * vPiValues1 = "01001011100000000011010110101000000";
+    char * vPiValues2 = "11001101011101011111110100100010001";
+
+    assert( strlen(vPiValues1) == (unsigned)Abc_NtkPiNum(pNtk) );
+    assert( 1 == Abc_NtkPoNum(pNtk) );
+
+    pModel1 = ALLOC( int, Abc_NtkCiNum(pNtk) );
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        pModel1[i] = vPiValues1[i] - '0';
+    Abc_NtkForEachLatch( pNtk, pObj, i )
+        pModel1[Abc_NtkPiNum(pNtk)+i] = ((int)pObj->pData) - 1;
+
+    pResult1 = Abc_NtkVerifySimulatePattern( pNtk, pModel1 );
+    printf( "Value = %d\n", pResult1[0] );
+
+    pModel2 = ALLOC( int, Abc_NtkCiNum(pNtk) );
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        pModel2[i] = vPiValues2[i] - '0';
+    Abc_NtkForEachLatch( pNtk, pObj, i )
+        pModel2[Abc_NtkPiNum(pNtk)+i] = pResult1[Abc_NtkPoNum(pNtk)+i];
+
+    pResult2 = Abc_NtkVerifySimulatePattern( pNtk, pModel2 );
+    printf( "Value = %d\n", pResult2[0] );
+
+    free( pModel1 );
+    free( pModel2 );
+    free( pResult1 );
+    free( pResult2 );
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/base/abci/module.make b/src/base/abci/module.make
index 41223c0b..c297180d 100644
--- a/src/base/abci/module.make
+++ b/src/base/abci/module.make
@@ -11,6 +11,7 @@ SRC +=    src/base/abci/abc.c \
     src/base/abci/abcFraig.c \
         src/base/abci/abcFxu.c \
         src/base/abci/abcGen.c \
+    src/base/abci/abcIvy.c \
     src/base/abci/abcMap.c \
     src/base/abci/abcMiter.c \
     src/base/abci/abcNtbdd.c \
diff --git a/src/base/io/io.h b/src/base/io/io.h
index b408293e..8c8d6bed 100644
--- a/src/base/io/io.h
+++ b/src/base/io/io.h
@@ -68,6 +68,7 @@ extern Abc_Ntk_t *        Io_ReadPla( char * pFileName, int fCheck );
 /*=== abcUtil.c ==========================================================*/
 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_ReadCreateNode( Abc_Ntk_t * pNtk, char * pNameOut, char * pNamesIn[], int nInputs );
 extern Abc_Obj_t *        Io_ReadCreateConst( Abc_Ntk_t * pNtk, char * pName, bool fConst1 );
diff --git a/src/base/io/ioReadBaf.c b/src/base/io/ioReadBaf.c
index e2aa2109..8f4a8ec4 100644
--- a/src/base/io/ioReadBaf.c
+++ b/src/base/io/ioReadBaf.c
@@ -100,8 +100,6 @@ Abc_Ntk_t * Io_ReadBaf( char * pFileName, int fCheck )
         pObj = Abc_NtkCreateLatch(pNtkNew);
         Abc_NtkLogicStoreName( pObj, pCur );  while ( *pCur++ ); 
         Vec_PtrPush( vNodes, pObj );
-        Vec_PtrPush( pNtkNew->vCis, pObj );
-        Vec_PtrPush( pNtkNew->vCos, pObj );
     }
 
     // get the pointer to the beginning of the node array
diff --git a/src/base/io/ioReadBlif.c b/src/base/io/ioReadBlif.c
index 3d33e6a3..11dd2db1 100644
--- a/src/base/io/ioReadBlif.c
+++ b/src/base/io/ioReadBlif.c
@@ -33,6 +33,7 @@ struct Io_ReadBlif_t_
     char *               pFileName;    // the name of the file
     Extra_FileReader_t * pReader;      // the input file reader
     // current processing info
+    Abc_Ntk_t *          pNtkMaster;   // the primary network
     Abc_Ntk_t *          pNtkCur;      // the primary network
     int                  LineCur;      // the line currently parsed
     // temporary storage for tokens
@@ -54,6 +55,7 @@ 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 );
@@ -151,7 +153,7 @@ Abc_Ntk_t * Io_ReadBlifNetwork( Io_ReadBlif_t * p )
         // add this network as part of the hierarchy
         if ( pNtkMaster == NULL ) // no master network so far
         {
-            pNtkMaster = pNtk;
+            p->pNtkMaster = pNtkMaster = pNtk;
             continue;
         }
         // make sure hierarchy does not have the network with this name
@@ -222,11 +224,12 @@ Abc_Ntk_t * Io_ReadBlifNetworkOne( Io_ReadBlif_t * p )
     }
 
     // read the inputs/outputs
+    if ( p->pNtkMaster == NULL )
     pProgress = Extra_ProgressBarStart( stdout, Extra_FileReaderGetFileSize(p->pReader) );
     fTokensReady = fStatus = 0;
     for ( iLine = 0; fTokensReady || (p->vTokens = Io_ReadBlifGetTokens(p)); iLine++ )
     {
-        if ( iLine % 1000 == 0 )
+        if ( p->pNtkMaster == NULL && iLine % 1000 == 0 )
         Extra_ProgressBarUpdate( pProgress, Extra_FileReaderGetCurPosition(p->pReader), NULL );
 
         // consider different line types
@@ -242,6 +245,8 @@ 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" ) )
@@ -257,8 +262,10 @@ Abc_Ntk_t * Io_ReadBlifNetworkOne( Io_ReadBlif_t * p )
         }
         else if ( !strcmp( pDirective, ".blackbox" ) )
         {
-            pNtk->ntkType = ABC_NTK_BLACKBOX;
+            pNtk->ntkType = ABC_NTK_NETLIST;
             pNtk->ntkFunc = ABC_FUNC_BLACKBOX;
+            Extra_MmFlexStop( pNtk->pManFunc, 0 );
+            pNtk->pManFunc = NULL;
         }
         else
             printf( "%s (line %d): Skipping directive \"%s\".\n", p->pFileName, 
@@ -268,6 +275,7 @@ Abc_Ntk_t * Io_ReadBlifNetworkOne( Io_ReadBlif_t * p )
         if ( fStatus == 1 )
             return NULL;
     }
+    if ( p->pNtkMaster == NULL )
     Extra_ProgressBarStop( pProgress );
     return pNtk;
 }
@@ -321,6 +329,25 @@ 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, 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;
@@ -340,7 +367,7 @@ int Io_ReadBlifNetworkLatch( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens )
         Abc_LatchSetInitDc( pLatch );
     else
     {
-        ResetValue = atoi(vTokens->pArray[3]);
+        ResetValue = atoi(vTokens->pArray[vTokens->nSize-1]);
         if ( ResetValue != 0 && ResetValue != 1 && ResetValue != 2 )
         {
             p->LineCur = Extra_FileReaderGetLineNumber(p->pReader, 0);
@@ -870,50 +897,55 @@ int Io_ReadBlifNetworkConnectBoxesOneBox( Io_ReadBlif_t * p, Abc_Obj_t * pBox, s
     // create the fanins of the box
     Abc_NtkForEachPi( pNtkModel, pObj, i )
         pObj->pCopy = NULL;
-    Vec_PtrForEachEntryStart( pNames, pName, i, 1 )
+    if ( Abc_NtkPiNum(pNtkModel) == 0 )
+        Start = 1;
+    else
     {
-        pActual = Io_ReadBlifCleanName(pName);
-        if ( pActual == NULL )
-        {
-            p->LineCur = (int)pBox->pCopy;
-            sprintf( p->sError, "Cannot parse formal/actual name pair \"%s\".", pName );
-            Io_ReadBlifPrintErrorMessage( p );
-            return 1;
-        }
-        Length = pActual - pName - 1;
-        pName[Length] = 0;
-        // find the PI net with this name
-        pObj = Abc_NtkFindNet( pNtkModel, pName );
-        if ( pObj == NULL )
-        {
-            p->LineCur = (int)pBox->pCopy;
-            sprintf( p->sError, "Cannot find formal input \"%s\" as an PI of model \"%s\".", pName, Vec_PtrEntry(pNames, 0) );
-            Io_ReadBlifPrintErrorMessage( p );
-            return 1;
-        }
-        // get the PI
-        pObj = Abc_ObjFanin0(pObj);
-        // quit if this is not a PI net
-        if ( !Abc_ObjIsPi(pObj) )
-        {
-            pName[Length] = '=';
-            Start = i;
-            break;
-        }
-        // remember the actual name in the net
-        if ( pObj->pCopy != NULL )
-        {
-            p->LineCur = (int)pBox->pCopy;
-            sprintf( p->sError, "Formal input \"%s\" is used more than once.", pName );
-            Io_ReadBlifPrintErrorMessage( p );
-            return 1;
-        }
-        pObj->pCopy = (void *)pActual;
-        // quit if we processed all PIs
-        if ( i == Abc_NtkPiNum(pNtkModel) )
+        Vec_PtrForEachEntryStart( pNames, pName, i, 1 )
         {
-            Start = i+1;
-            break;
+            pActual = Io_ReadBlifCleanName(pName);
+            if ( pActual == NULL )
+            {
+                p->LineCur = (int)pBox->pCopy;
+                sprintf( p->sError, "Cannot parse formal/actual name pair \"%s\".", pName );
+                Io_ReadBlifPrintErrorMessage( p );
+                return 1;
+            }
+            Length = pActual - pName - 1;
+            pName[Length] = 0;
+            // find the PI net with this name
+            pObj = Abc_NtkFindNet( pNtkModel, pName );
+            if ( pObj == NULL )
+            {
+                p->LineCur = (int)pBox->pCopy;
+                sprintf( p->sError, "Cannot find formal input \"%s\" as an PI of model \"%s\".", pName, Vec_PtrEntry(pNames, 0) );
+                Io_ReadBlifPrintErrorMessage( p );
+                return 1;
+            }
+            // get the PI
+            pObj = Abc_ObjFanin0(pObj);
+            // quit if this is not a PI net
+            if ( !Abc_ObjIsPi(pObj) )
+            {
+                pName[Length] = '=';
+                Start = i;
+                break;
+            }
+            // remember the actual name in the net
+            if ( pObj->pCopy != NULL )
+            {
+                p->LineCur = (int)pBox->pCopy;
+                sprintf( p->sError, "Formal input \"%s\" is used more than once.", pName );
+                Io_ReadBlifPrintErrorMessage( p );
+                return 1;
+            }
+            pObj->pCopy = (void *)pActual;
+            // quit if we processed all PIs
+            if ( i == Abc_NtkPiNum(pNtkModel) )
+            {
+                Start = i+1;
+                break;
+            }
         }
     }
     // create the fanins of the box
@@ -986,6 +1018,8 @@ int Io_ReadBlifNetworkConnectBoxesOneBox( Io_ReadBlif_t * p, Abc_Obj_t * pBox, s
         pObj->pCopy = NULL;
 
     // remove the array of names, assign the pointer to the model
+    Vec_PtrForEachEntry( pBox->pData, pName, i )
+        free( pName );
     Vec_PtrFree( pBox->pData );
     pBox->pData = pNtkModel;
     return 0;
diff --git a/src/base/io/ioUtil.c b/src/base/io/ioUtil.c
index fc37bc3f..5482eed4 100644
--- a/src/base/io/ioUtil.c
+++ b/src/base/io/ioUtil.c
@@ -80,6 +80,31 @@ 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 1e27498d..8cbd0cd0 100644
--- a/src/base/io/ioWriteBlif.c
+++ b/src/base/io/ioWriteBlif.c
@@ -30,6 +30,7 @@ static void Io_NtkWrite( FILE * pFile, Abc_Ntk_t * pNtk, int fWriteLatches );
 static void Io_NtkWriteOne( FILE * pFile, Abc_Ntk_t * pNtk, int fWriteLatches );
 static void Io_NtkWritePis( FILE * pFile, Abc_Ntk_t * pNtk, int fWriteLatches );
 static void Io_NtkWritePos( FILE * pFile, Abc_Ntk_t * pNtk, int fWriteLatches );
+static void Io_NtkWriteAsserts( FILE * pFile, Abc_Ntk_t * pNtk );
 static void Io_NtkWriteNodeGate( FILE * pFile, Abc_Obj_t * pNode );
 static void Io_NtkWriteNodeFanins( FILE * pFile, Abc_Obj_t * pNode );
 static void Io_NtkWriteNode( FILE * pFile, Abc_Obj_t * pNode );
@@ -115,7 +116,7 @@ void Io_WriteBlifNetlist( Abc_Ntk_t * pNtk, char * FileName, int fWriteLatches )
 void Io_NtkWrite( FILE * pFile, Abc_Ntk_t * pNtk, int fWriteLatches )
 {
     Abc_Ntk_t * pExdc;
-    assert( Abc_NtkIsNetlist(pNtk) || Abc_NtkIsBlackbox(pNtk) );
+    assert( Abc_NtkIsNetlist(pNtk) );
     // write the model name
     fprintf( pFile, ".model %s\n", Abc_NtkName(pNtk) );
     // write the network
@@ -159,8 +160,16 @@ void Io_NtkWriteOne( FILE * pFile, Abc_Ntk_t * pNtk, int fWriteLatches )
     Io_NtkWritePos( pFile, pNtk, fWriteLatches );
     fprintf( pFile, "\n" );
 
+    // write the assertions
+    if ( Abc_NtkAssertNum(pNtk) )
+    {
+        fprintf( pFile, ".asserts" );
+        Io_NtkWriteAsserts( pFile, pNtk );
+        fprintf( pFile, "\n" );
+    }
+
     // write the blackbox
-    if ( Abc_NtkIsBlackbox( pNtk ) )
+    if ( Abc_NtkHasBlackbox( pNtk ) )
     {
         fprintf( pFile, ".blackbox\n" );
         return;
@@ -296,6 +305,8 @@ 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;
@@ -313,6 +324,45 @@ void Io_NtkWritePos( FILE * pFile, Abc_Ntk_t * pNtk, int fWriteLatches )
     }
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Writes the assertion list.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Io_NtkWriteAsserts( FILE * pFile, Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pTerm, * pNet;
+    int LineLength;
+    int AddedLength;
+    int NameCounter;
+    int i;
+
+    LineLength  = 8;
+    NameCounter = 0;
+
+    Abc_NtkForEachAssert( pNtk, pTerm, i )
+    {
+        pNet = Abc_ObjFanin0(pTerm);
+        // get the line length after this name is written
+        AddedLength = strlen(Abc_ObjName(pNet)) + 1;
+        if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH )
+        { // write the line extender
+            fprintf( pFile, " \\\n" );
+            // reset the line length
+            LineLength  = 0;
+            NameCounter = 0;
+        }
+        fprintf( pFile, " %s", Abc_ObjName(pNet) );
+        LineLength += AddedLength;
+        NameCounter++;
+    }
+}
 
 /**Function*************************************************************
 
diff --git a/src/base/io/ioWriteVer.c b/src/base/io/ioWriteVer.c
index 75467d4d..e18f9b12 100644
--- a/src/base/io/ioWriteVer.c
+++ b/src/base/io/ioWriteVer.c
@@ -33,7 +33,6 @@ static void Io_WriteVerilogWires( FILE * pFile, Abc_Ntk_t * pNtk, int Start );
 static void Io_WriteVerilogRegs( FILE * pFile, Abc_Ntk_t * pNtk, int Start );
 static void Io_WriteVerilogGates( FILE * pFile, Abc_Ntk_t * pNtk );
 static void Io_WriteVerilogNodes( FILE * pFile, Abc_Ntk_t * pNtk );
-static void Io_WriteVerilogArgs( FILE * pFile, Abc_Obj_t * pObj, int nInMax, int fPadZeros );
 static void Io_WriteVerilogLatches( FILE * pFile, Abc_Ntk_t * pNtk );
 static int Io_WriteVerilogCheckNtk( Abc_Ntk_t * pNtk );
 static char * Io_WriteVerilogGetName( Abc_Obj_t * pObj );
@@ -225,7 +224,7 @@ void Io_WriteVerilogWires( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
     int i, Counter, nNodes;
 
     // count the number of wires
-    nNodes = 0;
+    nNodes = Abc_NtkLatchNum(pNtk);
     Abc_NtkForEachNode( pNtk, pTerm, i )
     {
         if ( i == 0 ) 
@@ -261,6 +260,24 @@ void Io_WriteVerilogWires( FILE * pFile, Abc_Ntk_t * pNtk, int Start )
         LineLength += AddedLength;
         NameCounter++;
     }
+    Abc_NtkForEachLatch( pNtk, pTerm, i )
+    {
+        pNet = Abc_ObjFanin0(pTerm);
+        Counter++;
+        // get the line length after this name is written
+        AddedLength = strlen(Abc_ObjName(pNet)) + 2;
+        if ( NameCounter && LineLength + AddedLength + 3 > IO_WRITE_LINE_LENGTH )
+        { // write the line extender
+            fprintf( pFile, "\n   " );
+            // reset the line length
+            LineLength  = 3;
+            NameCounter = 0;
+        }
+        fprintf( pFile, " %s%s", Io_WriteVerilogGetName(pNet), (Counter==nNodes)? "" : "," );
+        LineLength += AddedLength;
+        NameCounter++;
+    }
+    assert( Counter == nNodes );
 }
 
 /**Function*************************************************************
@@ -325,12 +342,15 @@ void Io_WriteVerilogLatches( FILE * pFile, Abc_Ntk_t * pNtk )
     int i;
     Abc_NtkForEachLatch( pNtk, pLatch, i )
     {
+//        fprintf( pFile, "  always@(posedge  gclk) begin %s",     Abc_ObjName(Abc_ObjFanout0(pLatch)) );
+        fprintf( pFile, "  always begin %s",     Abc_ObjName(Abc_ObjFanout0(pLatch)) );
+        fprintf( pFile, " = %s; end\n", Abc_ObjName(Abc_ObjFanin0(pLatch)) );
         if ( Abc_LatchInit(pLatch) == ABC_INIT_ZERO )
-            fprintf( pFile, "  initial begin %s = 1\'b0; end\n", Abc_ObjName(Abc_ObjFanout0(pLatch)) );
+//            fprintf( pFile, "  initial begin %s = 1\'b0; end\n", Abc_ObjName(Abc_ObjFanout0(pLatch)) );
+            fprintf( pFile, "  initial begin %s = 0; end\n", Abc_ObjName(Abc_ObjFanout0(pLatch)) );
         else if ( Abc_LatchInit(pLatch) == ABC_INIT_ONE )
-            fprintf( pFile, "  initial begin %s = 1\'b1; end\n", Abc_ObjName(Abc_ObjFanout0(pLatch)) );
-        fprintf( pFile, "  always@(posedge  gclk) begin %s",     Abc_ObjName(Abc_ObjFanout0(pLatch)) );
-        fprintf( pFile, " = %s; end\n", Abc_ObjName(Abc_ObjFanin0(pLatch)) );
+//            fprintf( pFile, "  initial begin %s = 1\'b1; end\n", Abc_ObjName(Abc_ObjFanout0(pLatch)) );
+            fprintf( pFile, "  initial begin %s = 1; end\n", Abc_ObjName(Abc_ObjFanout0(pLatch)) );
     }
 }
 
@@ -378,7 +398,7 @@ void Io_WriteVerilogGates( FILE * pFile, Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-void Io_WriteVerilogNodes( FILE * pFile, Abc_Ntk_t * pNtk )
+void Io_WriteVerilogNodes2( FILE * pFile, Abc_Ntk_t * pNtk )
 {
     Abc_Obj_t * pObj, * pFanin;
     int i, k, nFanins;
@@ -390,7 +410,8 @@ void Io_WriteVerilogNodes( FILE * pFile, Abc_Ntk_t * pNtk )
         nFanins = Abc_ObjFaninNum(pObj);
         if ( nFanins == 0 )
         {
-            fprintf( pFile, "  assign %s = 1'b%d;\n", Io_WriteVerilogGetName(Abc_ObjFanout0(pObj)), !Abc_SopIsComplement(pObj->pData) );
+//            fprintf( pFile, "  assign %s = 1'b%d;\n", Io_WriteVerilogGetName(Abc_ObjFanout0(pObj)), !Abc_SopIsComplement(pObj->pData) );
+            fprintf( pFile, "  assign %s = %d;\n", Io_WriteVerilogGetName(Abc_ObjFanout0(pObj)), !Abc_SopIsComplement(pObj->pData) );
             continue;
         }
         if ( nFanins == 1 )
@@ -410,7 +431,7 @@ void Io_WriteVerilogNodes( FILE * pFile, Abc_Ntk_t * pNtk )
 
 /**Function*************************************************************
 
-  Synopsis    [Writes the inputs.]
+  Synopsis    [Writes the nodes.]
 
   Description []
                
@@ -419,24 +440,32 @@ void Io_WriteVerilogNodes( FILE * pFile, Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-void Io_WriteVerilogArgs( FILE * pFile, Abc_Obj_t * pObj, int nInMax, int fPadZeros )
+void Io_WriteVerilogNodes( FILE * pFile, Abc_Ntk_t * pNtk )
 {
-    Abc_Obj_t * pFanin;
-    int i, Counter = 2;
-    fprintf( pFile, "(.z (%s)", Io_WriteVerilogGetName(Abc_ObjFanout0(pObj)) );
-    Abc_ObjForEachFanin( pObj, pFanin, i )
-    {
-        if ( Counter++ % 4 == 0 )
-            fprintf( pFile, "\n   " );
-        fprintf( pFile, " .i%d (%s)", i+1, Io_WriteVerilogGetName(Abc_ObjFanin(pObj,i)) );
-    }
-    for ( ; i < nInMax; i++ )
+    Abc_Obj_t * pObj, * pFanin;
+    int i, k, nFanins;
+    char pOper[] = " ? ", Symb;
+    Abc_NtkForEachNode( pNtk, pObj, i )
     {
-        if ( Counter++ % 4 == 0 )
-            fprintf( pFile, "\n   " );
-        fprintf( pFile, " .i%d (%s)", i+1, fPadZeros? "1\'b0" : "1\'b1" );
+        assert( Abc_SopGetCubeNum(pObj->pData) == 1 );
+        nFanins = Abc_ObjFaninNum(pObj);
+        if ( nFanins == 0 )
+        {
+            fprintf( pFile, "  assign %s = 1'b%d;\n", Io_WriteVerilogGetName(Abc_ObjFanout0(pObj)), !Abc_SopIsComplement(pObj->pData) );
+            continue;
+        }
+        fprintf( pFile, "  assign %s = ", Io_WriteVerilogGetName(Abc_ObjFanout0(pObj)) );
+        pOper[1] = Abc_SopIsComplement(pObj->pData) ? '|' : '&';
+        Abc_ObjForEachFanin( pObj, pFanin, k )
+        {
+            Symb = ((char*)pObj->pData)[k];
+            assert( Symb == '0' || Symb == '1' );
+            if ( Symb == '0' )
+                fprintf( pFile, "~" );
+            fprintf( pFile, "%s%s", Io_WriteVerilogGetName(pFanin), (k==nFanins-1? "" : pOper) );
+        }
+        fprintf( pFile, ";\n" );
     }
-    fprintf( pFile, ");\n" );
 }
 
 /**Function*************************************************************
diff --git a/src/base/main/mainFrame.c b/src/base/main/mainFrame.c
index 5747443c..23e304b3 100644
--- a/src/base/main/mainFrame.c
+++ b/src/base/main/mainFrame.c
@@ -446,7 +446,7 @@ void Abc_FrameDeleteAllNetworks( Abc_Frame_t * p )
         Abc_NtkDelete( pNtk );
     // set the current network empty
     p->pNtkCur = NULL;
-    fprintf( p->Out, "All networks have been deleted.\n" );
+//    fprintf( p->Out, "All networks have been deleted.\n" );
 }
 
 /**Function*************************************************************
diff --git a/src/base/main/module.make b/src/base/main/module.make
index 7a04e533..367f89f6 100644
--- a/src/base/main/module.make
+++ b/src/base/main/module.make
@@ -1,5 +1,5 @@
 SRC +=  src/base/main/main.c \
     src/base/main/mainFrame.c \
     src/base/main/mainInit.c \
-    src/base/main/mainUtils.c \
-    src/base/main/libSupport.c
+    src/base/main/libSupport.c \
+    src/base/main/mainUtils.c
diff --git a/src/base/seq/seqAigCore.c b/src/base/seq/seqAigCore.c
index 813b1ed8..358d306c 100644
--- a/src/base/seq/seqAigCore.c
+++ b/src/base/seq/seqAigCore.c
@@ -319,6 +319,7 @@ int Seq_NtkImplementRetimingBackward( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMoves, int
     // add the PI/PO names
     Abc_NtkAddDummyPiNames( pNtkProb );
     Abc_NtkAddDummyPoNames( pNtkProb );
+    Abc_NtkAddDummyAssertNames( pNtkProb );
 
     // make sure everything is okay with the network structure
     if ( !Abc_NtkDoCheck( pNtkProb ) )
@@ -358,7 +359,7 @@ int Seq_NtkImplementRetimingBackward( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMoves, int
     // solve the miter
 clk = clock();
 //    RetValue = Abc_NtkMiterSat_OldAndRusty( pNtkCnf, 30, 0 );
-    RetValue = Abc_NtkMiterSat( pNtkCnf, 500000, 50000000, 0, 0 );
+    RetValue = Abc_NtkMiterSat( pNtkCnf, (sint64)500000, (sint64)50000000, 0, 0, NULL, NULL );
 if ( fVerbose )
 if ( clock() - clk > 100 )
 {
diff --git a/src/base/seq/seqCreate.c b/src/base/seq/seqCreate.c
index b0c2e084..a553e06f 100644
--- a/src/base/seq/seqCreate.c
+++ b/src/base/seq/seqCreate.c
@@ -110,17 +110,23 @@ Abc_Ntk_t * Abc_NtkAigToSeq( Abc_Ntk_t * pNtk )
         pNtkNew->nObjs++;
     }
     pNtkNew->nNodes = pNtk->nNodes;
-    pNtkNew->nPis   = pNtk->nPis;
-    pNtkNew->nPos   = pNtk->nPos;
 
     // create PI/PO and their names
     Abc_NtkForEachPi( pNtk, pObj, i )
     {
+        Vec_PtrPush( pNtkNew->vPis, pObj->pCopy );
         Vec_PtrPush( pNtkNew->vCis, pObj->pCopy );
         Abc_NtkLogicStoreName( pObj->pCopy, Abc_ObjName(pObj) );
     }
     Abc_NtkForEachPo( pNtk, pObj, i ) 
     {
+        Vec_PtrPush( pNtkNew->vPos, pObj->pCopy );
+        Vec_PtrPush( pNtkNew->vCos, pObj->pCopy );
+        Abc_NtkLogicStoreName( pObj->pCopy, Abc_ObjName(pObj) );
+    }
+    Abc_NtkForEachAssert( pNtk, pObj, i ) 
+    {
+        Vec_PtrPush( pNtkNew->vAsserts, pObj->pCopy );
         Vec_PtrPush( pNtkNew->vCos, pObj->pCopy );
         Abc_NtkLogicStoreName( pObj->pCopy, Abc_ObjName(pObj) );
     }
@@ -252,7 +258,7 @@ void Abc_NtkAigCutsetCopy( Abc_Ntk_t * pNtk )
 Abc_Ntk_t * Abc_NtkSeqToLogicSop( Abc_Ntk_t * pNtk )
 {
     Abc_Ntk_t * pNtkNew; 
-    Abc_Obj_t * pObj, * pObjNew, * pFaninNew;
+    Abc_Obj_t * pObj, * pFaninNew;
     Seq_Lat_t * pRing;
     int i;
 
@@ -297,11 +303,7 @@ Abc_Ntk_t * Abc_NtkSeqToLogicSop( Abc_Ntk_t * pNtk )
 
     // add the latches and their names
     Abc_NtkAddDummyLatchNames( pNtkNew );
-    Abc_NtkForEachLatch( pNtkNew, pObjNew, i )
-    {
-        Vec_PtrPush( pNtkNew->vCis, pObjNew );
-        Vec_PtrPush( pNtkNew->vCos, pObjNew );
-    }
+    Abc_NtkOrderCisCos( pNtkNew );
     // fix the problem with complemented and duplicated CO edges
     Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
     if ( !Abc_NtkCheck( pNtkNew ) )
@@ -324,7 +326,7 @@ Abc_Ntk_t * Abc_NtkSeqToLogicSop( Abc_Ntk_t * pNtk )
 Abc_Ntk_t * Abc_NtkSeqToLogicSop_old( Abc_Ntk_t * pNtk )
 {
     Abc_Ntk_t * pNtkNew; 
-    Abc_Obj_t * pObj, * pObjNew, * pFaninNew;
+    Abc_Obj_t * pObj, * pFaninNew;
     int i;
 
     assert( Abc_NtkIsSeq(pNtk) );
@@ -371,11 +373,7 @@ Abc_Ntk_t * Abc_NtkSeqToLogicSop_old( Abc_Ntk_t * pNtk )
     }
     // add the latches and their names
     Abc_NtkAddDummyLatchNames( pNtkNew );
-    Abc_NtkForEachLatch( pNtkNew, pObjNew, i )
-    {
-        Vec_PtrPush( pNtkNew->vCis, pObjNew );
-        Vec_PtrPush( pNtkNew->vCos, pObjNew );
-    }
+    Abc_NtkOrderCisCos( pNtkNew );
     // fix the problem with complemented and duplicated CO edges
     Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
     if ( !Abc_NtkCheck( pNtkNew ) )
diff --git a/src/base/seq/seqFpgaCore.c b/src/base/seq/seqFpgaCore.c
index 6d0c8c97..79e44caf 100644
--- a/src/base/seq/seqFpgaCore.c
+++ b/src/base/seq/seqFpgaCore.c
@@ -280,7 +280,7 @@ Abc_Ntk_t * Seq_NtkSeqFpgaMapped( Abc_Ntk_t * pNtk )
     Abc_Seq_t * p = pNtk->pManFunc;
     Abc_Ntk_t * pNtkMap; 
     Vec_Ptr_t * vLeaves;
-    Abc_Obj_t * pObj, * pLatch, * pFaninNew;
+    Abc_Obj_t * pObj, * pFaninNew;
     Seq_Lat_t * pRing;
     int i;
 
@@ -322,11 +322,7 @@ Abc_Ntk_t * Seq_NtkSeqFpgaMapped( Abc_Ntk_t * pNtk )
 
     // add the latches and their names
     Abc_NtkAddDummyLatchNames( pNtkMap );
-    Abc_NtkForEachLatch( pNtkMap, pLatch, i )
-    {
-        Vec_PtrPush( pNtkMap->vCis, pLatch );
-        Vec_PtrPush( pNtkMap->vCos, pLatch );
-    }
+    Abc_NtkOrderCisCos( pNtkMap );
     // fix the problem with complemented and duplicated CO edges
     Abc_NtkLogicMakeSimpleCos( pNtkMap, 1 );
     // make the network minimum base
diff --git a/src/base/seq/seqMapCore.c b/src/base/seq/seqMapCore.c
index b1d4871e..a444ec58 100644
--- a/src/base/seq/seqMapCore.c
+++ b/src/base/seq/seqMapCore.c
@@ -370,7 +370,7 @@ Abc_Ntk_t * Seq_NtkSeqMapMapped( Abc_Ntk_t * pNtk )
     Seq_Match_t * pMatch;
     Abc_Ntk_t * pNtkMap; 
     Vec_Ptr_t * vLeaves;
-    Abc_Obj_t * pObj, * pLatch, * pFaninNew;
+    Abc_Obj_t * pObj, * pFaninNew;
     Seq_Lat_t * pRing;
     int i;
 
@@ -413,11 +413,7 @@ Abc_Ntk_t * Seq_NtkSeqMapMapped( Abc_Ntk_t * pNtk )
 
     // add the latches and their names
     Abc_NtkAddDummyLatchNames( pNtkMap );
-    Abc_NtkForEachLatch( pNtkMap, pLatch, i )
-    {
-        Vec_PtrPush( pNtkMap->vCis, pLatch );
-        Vec_PtrPush( pNtkMap->vCos, pLatch );
-    }
+    Abc_NtkOrderCisCos( pNtkMap );
     // fix the problem with complemented and duplicated CO edges
     Abc_NtkLogicMakeSimpleCos( pNtkMap, 1 );
     // make the network minimum base
diff --git a/src/base/seq/seqRetCore.c b/src/base/seq/seqRetCore.c
index 38915bf4..ba66a881 100644
--- a/src/base/seq/seqRetCore.c
+++ b/src/base/seq/seqRetCore.c
@@ -327,7 +327,7 @@ Abc_Ntk_t * Seq_NtkRetimeReconstruct( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkSeq )
     Abc_Seq_t * p = pNtkSeq->pManFunc;
     Seq_Lat_t * pRing0, * pRing1;
     Abc_Ntk_t * pNtkNew;
-    Abc_Obj_t * pObj, * pObjNew, * pFanin, * pFaninNew, * pMirror;
+    Abc_Obj_t * pObj, * pFanin, * pFaninNew, * pMirror;
     Vec_Ptr_t * vMirrors;
     int i, k;
 
@@ -408,11 +408,7 @@ Abc_Ntk_t * Seq_NtkRetimeReconstruct( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkSeq )
 
     // add the latches and their names
     Abc_NtkAddDummyLatchNames( pNtkNew );
-    Abc_NtkForEachLatch( pNtkNew, pObjNew, i )
-    {
-        Vec_PtrPush( pNtkNew->vCis, pObjNew );
-        Vec_PtrPush( pNtkNew->vCos, pObjNew );
-    }
+    Abc_NtkOrderCisCos( pNtkNew );
     // fix the problem with complemented and duplicated CO edges
     Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 );
     if ( !Abc_NtkCheck( pNtkNew ) )