Version abc80610

43 files changed, 1463 insertions, 721 deletions

diff --git a/Makefile b/Makefile
index a7097489..1afaae05 100644
--- a/Makefile
+++ b/Makefile
@@ -24,7 +24,9 @@ MODULES := src/base/abc src/base/abci src/base/cmd \
 
 default: $(PROG)
 
-#OPTFLAGS  := -DNDEBUG -O3
+#OPTFLAGS  := -DNDEBUG -O3 -DLIN
+#OPTFLAGS  := -DNDEBUG -O3 -DLIN64
+#OPTFLAGS  := -g -O -DLIN
 OPTFLAGS  := -g -O -DLIN64
 
 CFLAGS   += -Wall -Wno-unused-function $(OPTFLAGS) $(patsubst %, -I%, $(MODULES)) 
diff --git a/abc.dsp b/abc.dsp
index 2831bf81..6887188d 100644
--- a/abc.dsp
+++ b/abc.dsp
@@ -3294,6 +3294,10 @@ SOURCE=.\src\aig\saig\saigIoa.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\saig\saigMiter.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\saig\saigPhase.c
 # End Source File
 # Begin Source File
diff --git a/abctestlib.dsw b/abctestlib.dsw
deleted file mode 100644
index 7ae6cac9..00000000
--- a/abctestlib.dsw
+++ /dev/null
@@ -1,29 +0,0 @@
-Microsoft Developer Studio Workspace File, Format Version 6.00
-# WARNING: DO NOT EDIT OR DELETE THIS WORKSPACE FILE!
-
-###############################################################################
-
-Project: "abctestlib"=.\abctestlib.dsp - Package Owner=<4>
-
-Package=<5>
-{{{
-}}}
-
-Package=<4>
-{{{
-}}}
-
-###############################################################################
-
-Global:
-
-Package=<5>
-{{{
-}}}
-
-Package=<3>
-{{{
-}}}
-
-###############################################################################
-
diff --git a/readme b/readme
index b1588510..13bb8e15 100644
--- a/readme
+++ b/readme
@@ -1,6 +1,8 @@
 Often the code comes directly from a Windows computer.
 The following steps may be needed to compile it on UNIX:
 
+Modify Makefile to have -DLIN (for 32-bits) or -DLIN64 (for 64-bits)
+
 >> dos2unix Makefile Makefile
 >> dos2unix depends.sh depends.sh
 >> chmod 755 depends.sh
diff --git a/readmeaig b/readmeaig
new file mode 100644
index 00000000..ba179bbd
--- /dev/null
+++ b/readmeaig
@@ -0,0 +1,24 @@
+Using AIG Package in ABC
+
+- Download the latest snapshot of ABC
+- Compile the code found in "abc\src\aig\aig", "abc\src\aig\saig", and "abc\src\misc\vec" as a static library.
+- Link the library to the project.
+- Add #include "saig.h".
+- Start the AIG package using Aig_ManStart().
+- Assign primary inputs using Aig_ObjCreatePi().
+- Assign register outputs using Aig_ObjCreatePi().
+(it is important to create all PIs first, before creating register outputs).
+- Construct AIG in the topological order using Aig_And(), Aig_Or(), Aig_Not(), etc.
+- If constant-0/1 AIG nodes are needed, use Aig_ManConst0() or Aig_ManConst1()
+- Create primary outputs using Aig_ObjCreatePo().
+- Create register inputs using Aig_ObjCreatePo().
+(it is important to create all POs first, before creating register inputs).
+- Set the number of registers by calling Aig_ManSetRegNum().
+- Remove dangling AIG nodes (produced by structural hashing) using Aig_ManCleanup().
+- Call the consistency checking procedure Aig_ManCheck().
+- Dump AIG into a file using the new BLIF dumper Saig_ManDumpBlif().
+- For each object in the design annotated with the constructed AIG node (pNode), remember its AIG node ID by calling Aig_ObjId( Aig_Regular(pNode) ). To check whether the corresponding AIG node is complemented use Aig_IsComplement(pNode).
+- Quit the AIG package using Aig_ManStop().
+The above process should not produce memory leaks.
+
+
diff --git a/src/aig/aig/aigScl.c b/src/aig/aig/aigScl.c
index 2adcabfb..2c779c40 100644
--- a/src/aig/aig/aigScl.c
+++ b/src/aig/aig/aigScl.c
@@ -591,10 +591,11 @@ void Aig_ManComputeSccs( Aig_Man_t * p )
 Aig_Man_t * Aig_ManScl( Aig_Man_t * pAig, int fLatchConst, int fLatchEqual, int fVerbose )
 {
     extern void Saig_ManReportUselessRegisters( Aig_Man_t * pAig );
+    extern int Saig_ManReportComplements( Aig_Man_t * p );
 
     Aig_Man_t * pAigInit, * pAigNew;
     Aig_Obj_t * pFlop1, * pFlop2;
-    int i, Entry1, Entry2, nTruePis;
+    int i, Entry1, Entry2, nTruePis;//, nRegs;
     // store the original AIG
     assert( pAig->vFlopNums == NULL );
     pAigInit = pAig;
@@ -627,6 +628,11 @@ Aig_Man_t * Aig_ManScl( Aig_Man_t * pAig, int fLatchConst, int fLatchEqual, int
     Aig_ManSeqCleanup( pAigNew );
 
     Saig_ManReportUselessRegisters( pAigNew );
+    if ( Aig_ManRegNum(pAigNew) == 0 )
+        return pAigNew;
+//    nRegs = Saig_ManReportComplements( pAigNew );
+//    if ( nRegs ) 
+//    printf( "The number of complemented registers = %d.\n", nRegs );
     return pAigNew;
 }
 
diff --git a/src/aig/bbr/bbr.h b/src/aig/bbr/bbr.h
index 504fc463..69d5fae7 100644
--- a/src/aig/bbr/bbr.h
+++ b/src/aig/bbr/bbr.h
@@ -74,7 +74,7 @@ extern void        Aig_ManFreeGlobalBdds( Aig_Man_t * p, DdManager * dd );
 extern int         Aig_ManSizeOfGlobalBdds( Aig_Man_t * p );
 extern DdManager * Aig_ManComputeGlobalBdds( Aig_Man_t * p, int nBddSizeMax, int fDropInternal, int fReorder, int fVerbose );
 /*=== bbrReach.c ==========================================================*/
-extern int         Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose );
+extern int         Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose, int fSilent );
 
 #ifdef __cplusplus
 }
diff --git a/src/aig/bbr/bbrReach.c b/src/aig/bbr/bbrReach.c
index 95bfe1ba..a78a3fb2 100644
--- a/src/aig/bbr/bbrReach.c
+++ b/src/aig/bbr/bbrReach.c
@@ -203,7 +203,7 @@ DdNode ** Aig_ManCreatePartitions( DdManager * dd, Aig_Man_t * p, int fReorder,
   SeeAlso     []
 
 ***********************************************************************/
-int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, DdNode * bInitial, DdNode ** pbOutputs, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose )
+int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, DdNode * bInitial, DdNode ** pbOutputs, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose, int fSilent )
 {
     int fInternalReorder = 0;
     Bbr_ImageTree_t * pTree;
@@ -231,7 +231,8 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D
     free( pbVarsY );
     if ( pTree == NULL )
     {
-        printf( "BDDs blew up during qualitification scheduling.  " );
+        if ( !fSilent )
+            printf( "BDDs blew up during qualitification scheduling.  " );
         return -1;
     }
 
@@ -247,7 +248,8 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D
             bNext = Bbr_bddImageCompute2( pTree2, bCurrent );  
         if ( bNext == NULL )
         {
-            printf( "BDDs blew up during image computation.  " );
+            if ( !fSilent )
+                printf( "BDDs blew up during image computation.  " );
             if ( fPartition )
                 Bbr_bddImageTreeDelete( pTree );
             else
@@ -271,7 +273,8 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D
         {
             if ( !Cudd_bddLeq( dd, bNext, Cudd_Not(pbOutputs[i]) ) )
             {
-                printf( "Output %d was asserted in frame %d.  ", i, nIters );
+                if ( !fSilent )
+                    printf( "Output %d was asserted in frame %d.  ", i, nIters );
                 Cudd_RecursiveDeref( dd, bReached );
                 bReached = NULL;
                 break;
@@ -326,10 +329,12 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D
     Cudd_RecursiveDeref( dd, bReached );
     if ( nIters > nIterMax || Cudd_DagSize(bReached) > nBddMax )
     {
-         printf( "Verified only for states reachable in %d frames.  ", nIters );
-         return -1; // undecided
+        if ( !fSilent )
+            printf( "Verified only for states reachable in %d frames.  ", nIters );
+        return -1; // undecided
     }
-    printf( "The miter is proved unreachable after %d iterations.  ", nIters );
+    if ( !fSilent )
+        printf( "The miter is proved unreachable after %d iterations.  ", nIters );
     return 1; // unreachable
 }
 
@@ -344,7 +349,7 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D
   SeeAlso     []
 
 ***********************************************************************/
-int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose )
+int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose, int fSilent )
 {
     DdManager * dd;
     DdNode ** pbParts, ** pbOutputs;
@@ -357,7 +362,8 @@ int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fParti
     dd = Aig_ManComputeGlobalBdds( p, nBddMax, 1, fReorder, fVerbose );    
     if ( dd == NULL )
     {
-        printf( "The number of intermediate BDD nodes exceeded the limit (%d).\n", nBddMax );
+        if ( !fSilent )
+            printf( "The number of intermediate BDD nodes exceeded the limit (%d).\n", nBddMax );
         return -1;
     }
     if ( fVerbose )
@@ -378,14 +384,15 @@ int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fParti
     {
         if ( !Cudd_bddLeq( dd, bInitial, Cudd_Not(pbOutputs[i]) ) )
         {
-            printf( "The miter output %d is proved REACHABLE in the initial state.  ", i );
+            if ( !fSilent )
+                printf( "The miter output %d is proved REACHABLE in the initial state.  ", i );
             RetValue = 0;
             break;
         }
     }
     // explore reachable states
     if ( RetValue == -1 )
-        RetValue = Aig_ManComputeReachable( dd, p, pbParts, bInitial, pbOutputs, nBddMax, nIterMax, fPartition, fReorder, fVerbose ); 
+        RetValue = Aig_ManComputeReachable( dd, p, pbParts, bInitial, pbOutputs, nBddMax, nIterMax, fPartition, fReorder, fVerbose, fSilent ); 
 
     // cleanup
     Cudd_RecursiveDeref( dd, bInitial );
@@ -401,8 +408,11 @@ int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fParti
         Bbr_StopManager( dd );
 
     // report the runtime
+    if ( !fSilent )
+    {
     PRT( "Time", clock() - clk );
     fflush( stdout );
+    }
     return RetValue;
 }
 
diff --git a/src/aig/cnf/cnf.h b/src/aig/cnf/cnf.h
index e664b1bc..bf109b17 100644
--- a/src/aig/cnf/cnf.h
+++ b/src/aig/cnf/cnf.h
@@ -139,7 +139,7 @@ extern void            Cnf_DataLift( Cnf_Dat_t * p, int nVarsPlus );
 extern void            Cnf_DataPrint( Cnf_Dat_t * p, int fReadable );
 extern void            Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable );
 extern void *          Cnf_DataWriteIntoSolver( Cnf_Dat_t * p, int nFrames, int fInit );
-extern void            Cnf_DataWriteOrClause( void * pSat, Cnf_Dat_t * pCnf );
+extern int             Cnf_DataWriteOrClause( void * pSat, Cnf_Dat_t * pCnf );
 /*=== cnfMap.c ========================================================*/
 extern void            Cnf_DeriveMapping( Cnf_Man_t * p );
 extern int             Cnf_ManMapForCnf( Cnf_Man_t * p );
diff --git a/src/aig/cnf/cnfMan.c b/src/aig/cnf/cnfMan.c
index b6ed3da0..fc71f936 100644
--- a/src/aig/cnf/cnfMan.c
+++ b/src/aig/cnf/cnfMan.c
@@ -362,7 +362,7 @@ void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p, int nFrames, int fInit )
   SeeAlso     []
 
 ***********************************************************************/
-void Cnf_DataWriteOrClause( void * p, Cnf_Dat_t * pCnf )
+int Cnf_DataWriteOrClause( void * p, Cnf_Dat_t * pCnf )
 {
     sat_solver * pSat = p;
     Aig_Obj_t * pObj;
@@ -371,8 +371,12 @@ void Cnf_DataWriteOrClause( void * p, Cnf_Dat_t * pCnf )
     Aig_ManForEachPo( pCnf->pMan, pObj, i )
         pLits[i] = toLitCond( pCnf->pVarNums[pObj->Id], 0 );
     if ( !sat_solver_addclause( pSat, pLits, pLits + Aig_ManPoNum(pCnf->pMan) ) )
-        assert( 0 );
+    {
+        free( pLits );
+        return 0;
+    }
     free( pLits );
+    return 1;
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
index 7549dfca..025ce046 100644
--- a/src/aig/fra/fra.h
+++ b/src/aig/fra/fra.h
@@ -104,6 +104,7 @@ struct Fra_Ssw_t_
     int              fWriteImps;        // write implications into a file
     int              fUse1Hot;          // use one-hotness constraints
     int              fVerbose;          // enable verbose output 
+    int              fSilent;           // disable any output 
     int              nIters;            // the number of iterations performed
     float            TimeLimit;         // the runtime budget for this call
 };
@@ -121,6 +122,7 @@ struct Fra_Sec_t_
     int              fInterpolation;    // enables interpolation
     int              fReachability;     // enables BDD based reachability
     int              fStopOnFirstFail;  // enables stopping after first output of a miter has failed to prove
+    int              fSilent;           // disables all output
     int              fVerbose;          // enables verbose reporting of statistics
     int              fVeryVerbose;      // enables very verbose reporting  
     int              TimeLimit;         // enables the timeout
diff --git a/src/aig/fra/fraCec.c b/src/aig/fra/fraCec.c
index e91478a4..d67839a4 100644
--- a/src/aig/fra/fraCec.c
+++ b/src/aig/fra/fraCec.c
@@ -53,19 +53,22 @@ int Fra_FraigSat( Aig_Man_t * pMan, sint64 nConfLimit, sint64 nInsLimit, int fVe
     // derive CNF
     pCnf = Cnf_Derive( pMan, Aig_ManPoNum(pMan) );
 //    pCnf = Cnf_DeriveSimple( pMan, Aig_ManPoNum(pMan) );
-    // convert into the SAT solver
+    // convert into SAT solver
     pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
-    // add the OR clause for the outputs
-    Cnf_DataWriteOrClause( pSat, pCnf );
-    vCiIds = Cnf_DataCollectPiSatNums( pCnf, pMan );
-    Cnf_DataFree( pCnf );
-    // solve SAT
     if ( pSat == NULL )
     {
-        Vec_IntFree( vCiIds );
-//        printf( "Trivially unsat\n" );
+        Cnf_DataFree( pCnf );
         return 1;
     }
+    // add the OR clause for the outputs
+    if ( !Cnf_DataWriteOrClause( pSat, pCnf ) )
+    {
+        sat_solver_delete( pSat );
+        Cnf_DataFree( pCnf );
+        return 1;
+    }
+    vCiIds = Cnf_DataCollectPiSatNums( pCnf, pMan );
+    Cnf_DataFree( pCnf );
 
 
 //    printf( "Created SAT problem with %d variable and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) );
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index df92792a..9c52d0e2 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -422,7 +422,8 @@ PRT( "Time", clock() - clk );
 
     if ( pParams->TimeLimit != 0.0 && clock() > TimeToStop )
     {
-        printf( "Fra_FraigInduction(): Runtime limit exceeded.\n" );
+        if ( !pParams->fSilent )
+            printf( "Fra_FraigInduction(): Runtime limit exceeded.\n" );
         goto finish;
     }
 
@@ -452,7 +453,8 @@ PRT( "Time", clock() - clk );
 
         if ( pParams->TimeLimit != 0.0 && clock() > TimeToStop )
         {
-            printf( "Fra_FraigInduction(): Runtime limit exceeded.\n" );
+            if ( !pParams->fSilent )
+                printf( "Fra_FraigInduction(): Runtime limit exceeded.\n" );
             goto finish;
         }
 
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index 4528b9c4..96c0de77 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -53,11 +53,12 @@ void Fra_SecSetDefaultParams( Fra_Sec_t * p )
     p->fInterpolation    =   1;  // enables interpolation
     p->fReachability     =   1;  // enables BDD based reachability
     p->fStopOnFirstFail  =   1;  // enables stopping after first output of a miter has failed to prove
+    p->fSilent           =   0;  // disables all output
     p->fVerbose          =   0;  // enables verbose reporting of statistics
     p->fVeryVerbose      =   0;  // enables very verbose reporting  
     p->TimeLimit         =   0;  // enables the timeout
     // internal parameters
-    p->fReportSolution   =   1;  // enables specialized format for reporting solution
+    p->fReportSolution   =   0;  // enables specialized format for reporting solution
 }
 
 /**Function*************************************************************
@@ -158,7 +159,8 @@ clk = clock();
         TimeLeft = AIG_MAX( TimeLeft, 0.0 );
         if ( TimeLeft == 0.0 )
         {
-            printf( "Runtime limit exceeded.\n" );
+            if ( !pParSec->fSilent )
+                printf( "Runtime limit exceeded.\n" );
             RetValue = -1;
             TimeOut = 1;
             goto finish;
@@ -166,14 +168,16 @@ clk = clock();
     }
     pNew = Fra_FraigLatchCorrespondence( pTemp = pNew, 0, 1000, 1, pParSec->fVeryVerbose, &nIter, TimeLeft );
     p->pSeqModel = pTemp->pSeqModel; pTemp->pSeqModel = NULL;
-    Aig_ManStop( pTemp );
     if ( pNew == NULL )
     {
         if ( p->pSeqModel )
         {
             RetValue = 0;
-            printf( "Networks are NOT EQUIVALENT after simulation.   " );
+            if ( !pParSec->fSilent )
+            {
+                printf( "Networks are NOT EQUIVALENT after simulation.   " );
 PRT( "Time", clock() - clkTotal );
+            }
             if ( pParSec->fReportSolution && !pParSec->fRecursive )
             {
             printf( "SOLUTION: FAIL       " );
@@ -186,6 +190,7 @@ PRT( "Time", clock() - clkTotal );
         TimeOut = 1;
         goto finish;
     }
+    Aig_ManStop( pTemp );
 
     if ( pParSec->fVerbose )
     {
@@ -201,7 +206,8 @@ PRT( "Time", clock() - clk );
         TimeLeft = AIG_MAX( TimeLeft, 0.0 );
         if ( TimeLeft == 0.0 )
         {
-            printf( "Runtime limit exceeded.\n" );
+            if ( !pParSec->fSilent )
+                printf( "Runtime limit exceeded.\n" );
             RetValue = -1;
             TimeOut = 1;
             goto finish;
@@ -235,7 +241,8 @@ PRT( "Time", clock() - clk );
         TimeLeft = AIG_MAX( TimeLeft, 0.0 );
         if ( TimeLeft == 0.0 )
         {
-            printf( "Runtime limit exceeded.\n" );
+            if ( !pParSec->fSilent )
+                printf( "Runtime limit exceeded.\n" );
             RetValue = -1;
             TimeOut = 1;
             goto finish;
@@ -273,7 +280,8 @@ PRT( "Time", clock() - clk );
             TimeLeft = AIG_MAX( TimeLeft, 0.0 );
             if ( TimeLeft == 0.0 )
             {
-                printf( "Runtime limit exceeded.\n" );
+                if ( !pParSec->fSilent )
+                    printf( "Runtime limit exceeded.\n" );
                 RetValue = -1;
                 TimeOut = 1;
                 goto finish;
@@ -283,6 +291,7 @@ PRT( "Time", clock() - clk );
 clk = clock();
         pPars->nFramesK = nFrames;
         pPars->TimeLimit = TimeLeft;
+        pPars->fSilent = pParSec->fSilent;
         pNew = Fra_FraigInduction( pTemp = pNew, pPars );
         if ( pNew == NULL )
         {
@@ -357,8 +366,11 @@ PRT( "Time", clock() - clk );
             Fra_SmlStop( pSml );
             Aig_ManStop( pNew );
             RetValue = 0;
-            printf( "Networks are NOT EQUIVALENT after simulation.   " );
+            if ( !pParSec->fSilent )
+            {
+                printf( "Networks are NOT EQUIVALENT after simulation.   " );
 PRT( "Time", clock() - clkTotal );
+            }
             if ( pParSec->fReportSolution && !pParSec->fRecursive )
             {
             printf( "SOLUTION: FAIL       " );
@@ -399,10 +411,10 @@ PRT( "Time", clock() - clk );
     // try reachability analysis
     if ( pParSec->fReachability && RetValue == -1 && Aig_ManRegNum(pNew) > 0 && Aig_ManRegNum(pNew) < 150 )
     {
-        extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose );
+        extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose, int fSilent );
         pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew); 
         pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew); 
-        RetValue = Aig_ManVerifyUsingBdds( pNew, 100000, 1000, 1, 1, 0 );
+        RetValue = Aig_ManVerifyUsingBdds( pNew, 100000, 1000, 1, 1, 0, pParSec->fSilent );
     }
 
     // try one-output at a time
@@ -414,8 +426,9 @@ PRT( "Time", clock() - clk );
         for ( i = 0; i < Aig_ManPoNum(pNew)-Aig_ManRegNum(pNew); i++ )
             if ( !Aig_ObjIsConst1( Aig_ObjFanin0(Aig_ManPo(pNew,i)) ) )
                 Counter++;
-        printf( "*** The miter has %d outputs (out of %d total) unsolved in the multi-output form.\n", 
-            Counter, Aig_ManPoNum(pNew)-Aig_ManRegNum(pNew) );
+        if ( !pParSec->fSilent )
+            printf( "*** The miter has %d outputs (out of %d total) unsolved in the multi-output form.\n", 
+                Counter, Aig_ManPoNum(pNew)-Aig_ManRegNum(pNew) );
         iCount = 0;
         for ( i = 0; i < Aig_ManPoNum(pNew)-Aig_ManRegNum(pNew); i++ )
         {
@@ -427,7 +440,8 @@ PRT( "Time", clock() - clk );
                 TimeLeft = AIG_MAX( TimeLeft, 0.0 );
                 if ( TimeLeft == 0.0 )
                 {
-                    printf( "Runtime limit exceeded.\n" );
+                    if ( !pParSec->fSilent )
+                        printf( "Runtime limit exceeded.\n" );
                     TimeOut = 1;
                     goto finish;
                 }
@@ -438,7 +452,8 @@ PRT( "Time", clock() - clk );
             if ( Aig_ObjIsConst1( Aig_ObjFanin0(Aig_ManPo(pNew,i)) ) )
                 continue;
             iCount++;
-            printf( "*** Running output %d of the miter (number %d out of %d unsolved).\n", i, iCount, Counter );
+            if ( !pParSec->fSilent )
+                printf( "*** Running output %d of the miter (number %d out of %d unsolved).\n", i, iCount, Counter );
             pNew2 = Aig_ManDupOneOutput( pNew, i );
             
             TimeLimitCopy = pParSec->TimeLimit;
@@ -462,15 +477,19 @@ PRT( "Time", clock() - clk );
             RetValue = -1;
         else
             RetValue = 1;
-        printf( "*** Finished running separate outputs of the miter.\n" );
+        if ( !pParSec->fSilent )
+            printf( "*** Finished running separate outputs of the miter.\n" );
     }
 
 finish:
     // report the miter
     if ( RetValue == 1 )
     {
-        printf( "Networks are equivalent.   " );
+        if ( !pParSec->fSilent )
+        {
+            printf( "Networks are equivalent.   " );
 PRT( "Time", clock() - clkTotal );
+        }
         if ( pParSec->fReportSolution && !pParSec->fRecursive )
         {
         printf( "SOLUTION: PASS       " );
@@ -479,8 +498,11 @@ PRT( "Time", clock() - clkTotal );
     }
     else if ( RetValue == 0 )
     {
-        printf( "Networks are NOT EQUIVALENT.   " );
+        if ( !pParSec->fSilent )
+        {
+            printf( "Networks are NOT EQUIVALENT.   " );
 PRT( "Time", clock() - clkTotal );
+        }
         if ( pParSec->fReportSolution && !pParSec->fRecursive )
         {
         printf( "SOLUTION: FAIL       " );
@@ -489,14 +511,17 @@ PRT( "Time", clock() - clkTotal );
     }
     else 
     {
-        printf( "Networks are UNDECIDED.   " );
+        if ( !pParSec->fSilent )
+        {
+            printf( "Networks are UNDECIDED.   " );
 PRT( "Time", clock() - clkTotal );
+        }
         if ( pParSec->fReportSolution && !pParSec->fRecursive )
         {
         printf( "SOLUTION: UNDECIDED  " );
 PRT( "Time", clock() - clkTotal );
         }
-        if ( !TimeOut )
+        if ( !TimeOut && !pParSec->fSilent )
         {
             static int Counter = 1;
             char pFileName[1000];
diff --git a/src/aig/fra/fraSec80516.zip b/src/aig/fra/fraSec80516.zip
deleted file mode 100644
index 0adf10df..00000000
--- a/src/aig/fra/fraSec80516.zip
+++ /dev/null
diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c
index 00a35fcd..53493201 100644
--- a/src/aig/fra/fraSim.c
+++ b/src/aig/fra/fraSim.c
@@ -1119,20 +1119,22 @@ int Fra_SmlWriteCounterExample( FILE * pFile, Aig_Man_t * pAig, Fra_Cex_t * p )
     RetValue = !Fra_SmlNodeIsZero( pSml, Aig_ManPo(pAig, p->iPo) );
 
     // write the output file
-    fprintf( pFile, "1\n" );
     for ( i = 0; i <= p->iFrame; i++ )
     {
+/*
         Aig_ManForEachLoSeq( pAig, pObj, k )
         {
             pSims = Fra_ObjSim(pSml, pObj->Id);
             fprintf( pFile, "%d", (int)(pSims[i] != 0) );
         }
         fprintf( pFile, " " );
+*/
         Aig_ManForEachPiSeq( pAig, pObj, k )
         {
             pSims = Fra_ObjSim(pSml, pObj->Id);
             fprintf( pFile, "%d", (int)(pSims[i] != 0) );
         }
+/*
         fprintf( pFile, " " );
         Aig_ManForEachPoSeq( pAig, pObj, k )
         {
@@ -1145,6 +1147,7 @@ int Fra_SmlWriteCounterExample( FILE * pFile, Aig_Man_t * pAig, Fra_Cex_t * p )
             pSims = Fra_ObjSim(pSml, pObj->Id);
             fprintf( pFile, "%d", (int)(pSims[i] != 0) );
         }
+*/
         fprintf( pFile, "\n" );
     }
 
diff --git a/src/aig/ivy/ivyFraig.c b/src/aig/ivy/ivyFraig.c
index d049d660..0d9d42a3 100644
--- a/src/aig/ivy/ivyFraig.c
+++ b/src/aig/ivy/ivyFraig.c
@@ -2260,8 +2260,8 @@ p->timeSat += clock() - clk;
     {
 p->timeSatUnsat += clock() - clk;
         pLits[0] = lit_neg( pLits[0] );
-        RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 1 );
-        assert( RetValue );
+//        RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 1 );
+//        assert( RetValue );
         // continue solving the other implication
         p->nSatCallsUnsat++;
     }
diff --git a/src/aig/ntl/ntl.h b/src/aig/ntl/ntl.h
index 4179754c..b496cb13 100644
--- a/src/aig/ntl/ntl.h
+++ b/src/aig/ntl/ntl.h
@@ -43,6 +43,7 @@ extern "C" {
 
 typedef struct Ntl_Man_t_    Ntl_Man_t;
 typedef struct Ntl_Mod_t_    Ntl_Mod_t;
+typedef struct Ntl_Reg_t_    Ntl_Reg_t;
 typedef struct Ntl_Obj_t_    Ntl_Obj_t;
 typedef struct Ntl_Net_t_    Ntl_Net_t;
 typedef struct Ntl_Lut_t_    Ntl_Lut_t;
@@ -65,6 +66,7 @@ struct Ntl_Man_t_
     char *             pName;          // the name of this design
     char *             pSpec;          // the name of input file
     Vec_Ptr_t *        vModels;        // the array of all models used to represent boxes
+    int                BoxTypes[15];   // the array of box types among the models
     // memory managers
     Aig_MmFlex_t *     pMemObjs;       // memory for objects
     Aig_MmFlex_t *     pMemSops;       // memory for SOPs
@@ -75,6 +77,12 @@ struct Ntl_Man_t_
     Vec_Int_t *        vBox1Cos;       // the first COs of the boxes
     Aig_Man_t *        pAig;           // the extracted AIG
     Tim_Man_t *        pManTime;       // the timing manager
+    int                iLastCi;        // the last true CI
+    Vec_Ptr_t *        vLatchIns;      // the AIG nodes driving latch inputs for internal latches
+    // hashing names into models
+    Ntl_Mod_t **       pModTable;      // the hash table of names into models
+    int                nModTableSize;  // the allocated table size
+    int                nModEntries;    // the number of entries in the hash table
 };
 
 struct Ntl_Mod_t_
@@ -86,21 +94,33 @@ struct Ntl_Mod_t_
     Vec_Ptr_t *        vPis;           // the array of PI objects
     Vec_Ptr_t *        vPos;           // the array of PO objects
     int                nObjs[NTL_OBJ_VOID]; // counter of objects of each type
-    int                fKeep;          // indicates persistant model
+    // box attributes
+    unsigned int       attrWhite :  1; // box has known logic
+    unsigned int       attrBox   :  1; // box is to remain unmapped
+    unsigned int       attrComb  :  1; // box is combinational
+    unsigned int       attrKeep  :  1; // box cannot be removed by structural sweep
     // hashing names into nets
     Ntl_Net_t **       pTable;         // the hash table of names into nets
     int                nTableSize;     // the allocated table size
     int                nEntries;       // the number of entries in the hash table
     // delay information
     Vec_Int_t *        vDelays;
-    Vec_Int_t *        vArrivals;
-    Vec_Int_t *        vRequireds;
+    Vec_Int_t *        vTimeInputs;
+    Vec_Int_t *        vTimeOutputs;
     float *            pDelayTable;   
     // other data members
+    Ntl_Mod_t *        pNext;
     void *             pCopy;
     int                nUsed, nRems;
 }; 
 
+struct Ntl_Reg_t_
+{
+    unsigned int       regInit   :  2; // register initial value
+    unsigned int       regType   :  3; // register type
+    unsigned int       regClass  : 28; // register class
+};
+
 struct Ntl_Obj_t_
 {
     Ntl_Mod_t *        pModel;         // the model  
@@ -113,7 +133,11 @@ struct Ntl_Obj_t_
     union {                            // functionality
         Ntl_Mod_t *    pImplem;        // model (for boxes)
         char *         pSop;           // SOP (for logic nodes)
-        unsigned       LatchId;        // init state + register class (for latches) 
+        Ntl_Reg_t      LatchId;        // init state + register class (for latches) 
+    };
+    union {                            // clock / other data
+        Ntl_Net_t *    pClock;         // clock (for registers)
+        void *         pTemp;          // other data 
     };
     Ntl_Net_t *        pFanio[0];      // fanins/fanouts
 };
@@ -164,8 +188,6 @@ static inline int         Ntl_ModelNodeNum( Ntl_Mod_t * p )       { return p->nO
 static inline int         Ntl_ModelLut1Num( Ntl_Mod_t * p )       { return p->nObjs[NTL_OBJ_LUT1];              } 
 static inline int         Ntl_ModelLatchNum( Ntl_Mod_t * p )      { return p->nObjs[NTL_OBJ_LATCH];             } 
 static inline int         Ntl_ModelBoxNum( Ntl_Mod_t * p )        { return p->nObjs[NTL_OBJ_BOX];               } 
-static inline int         Ntl_ModelCiNum( Ntl_Mod_t * p )         { return p->nObjs[NTL_OBJ_PI] + p->nObjs[NTL_OBJ_LATCH]; } 
-static inline int         Ntl_ModelCoNum( Ntl_Mod_t * p )         { return p->nObjs[NTL_OBJ_PO] + p->nObjs[NTL_OBJ_LATCH]; } 
 
 static inline Ntl_Obj_t * Ntl_ModelPi( Ntl_Mod_t * p, int i )     { return (Ntl_Obj_t *)Vec_PtrEntry(p->vPis, i);            } 
 static inline Ntl_Obj_t * Ntl_ModelPo( Ntl_Mod_t * p, int i )     { return (Ntl_Obj_t *)Vec_PtrEntry(p->vPos, i);            } 
@@ -173,8 +195,6 @@ static inline Ntl_Obj_t * Ntl_ModelPo( Ntl_Mod_t * p, int i )     { return (Ntl_
 static inline char *      Ntl_ModelPiName( Ntl_Mod_t * p, int i ) { return Ntl_ModelPi(p, i)->pFanio[0]->pName; } 
 static inline char *      Ntl_ModelPoName( Ntl_Mod_t * p, int i ) { return Ntl_ModelPo(p, i)->pFanio[0]->pName; } 
 
-static inline int         Ntl_ModelIsBlackBox( Ntl_Mod_t * p )    { return Ntl_ModelPiNum(p) + Ntl_ModelPoNum(p) == Vec_PtrSize(p->vObjs); } 
-
 static inline int         Ntl_ObjFaninNum( Ntl_Obj_t * p )        { return p->nFanins;                          } 
 static inline int         Ntl_ObjFanoutNum( Ntl_Obj_t * p )       { return p->nFanouts;                         } 
 
@@ -193,6 +213,23 @@ static inline Ntl_Net_t * Ntl_ObjFanout( Ntl_Obj_t * p, int i )   { return p->pF
 static inline void        Ntl_ObjSetFanin( Ntl_Obj_t * p, Ntl_Net_t * pNet, int i )    { p->pFanio[i] = pNet;   } 
 static inline void        Ntl_ObjSetFanout( Ntl_Obj_t * p, Ntl_Net_t * pNet, int i )   { p->pFanio[p->nFanins+i] = pNet; pNet->pDriver = p; } 
 
+static inline int         Ntl_ObjIsInit1( Ntl_Obj_t * p )         { assert( Ntl_ObjIsLatch(p) ); return p->LatchId.regInit == 1;   } 
+static inline void        Ntl_ObjSetInit0( Ntl_Obj_t * p )        { assert( Ntl_ObjIsLatch(p) ); p->LatchId.regInit = 0;           } 
+
+static inline int         Ntl_BoxIsWhite( Ntl_Obj_t * p )         { assert( Ntl_ObjIsBox(p) ); return p->pImplem->attrWhite;    } 
+static inline int         Ntl_BoxIsBlack( Ntl_Obj_t * p )         { assert( Ntl_ObjIsBox(p) ); return !p->pImplem->attrWhite;   } 
+static inline int         Ntl_BoxIsComb( Ntl_Obj_t * p )          { assert( Ntl_ObjIsBox(p) ); return p->pImplem->attrComb;     } 
+static inline int         Ntl_BoxIsSeq( Ntl_Obj_t * p )           { assert( Ntl_ObjIsBox(p) ); return !p->pImplem->attrComb;    } 
+
+static inline int         Ntl_ObjIsMapLeaf( Ntl_Obj_t * p )       { return Ntl_ObjIsPi(p) || (Ntl_ObjIsBox(p) && Ntl_BoxIsSeq(p));   } 
+static inline int         Ntl_ObjIsMapRoot( Ntl_Obj_t * p )       { return Ntl_ObjIsPo(p) || (Ntl_ObjIsBox(p) && Ntl_BoxIsSeq(p));   } 
+
+static inline int         Ntl_ObjIsCombLeaf( Ntl_Obj_t * p )      { return Ntl_ObjIsPi(p) || (Ntl_ObjIsBox(p) && (Ntl_BoxIsSeq(p) || Ntl_BoxIsBlack(p)));   } 
+static inline int         Ntl_ObjIsCombRoot( Ntl_Obj_t * p )      { return Ntl_ObjIsPo(p) || (Ntl_ObjIsBox(p) && (Ntl_BoxIsSeq(p) || Ntl_BoxIsBlack(p)));   } 
+
+static inline int         Ntl_ObjIsSeqLeaf( Ntl_Obj_t * p )       { return Ntl_ObjIsPi(p) || (Ntl_ObjIsBox(p) && Ntl_BoxIsBlack(p));   } 
+static inline int         Ntl_ObjIsSeqRoot( Ntl_Obj_t * p )       { return Ntl_ObjIsPo(p) || (Ntl_ObjIsBox(p) && Ntl_BoxIsBlack(p));   } 
+
 ////////////////////////////////////////////////////////////////////////
 ///                         ITERATORS                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -203,10 +240,10 @@ static inline void        Ntl_ObjSetFanout( Ntl_Obj_t * p, Ntl_Net_t * pNet, int
     Vec_PtrForEachEntry( p->vCis, pNet, i )
 #define Ntl_ManForEachCoNet( p, pNet, i )                                       \
     Vec_PtrForEachEntry( p->vCos, pNet, i )
-#define Ntl_ManForEachNode( p, pObj, i )                                   \
+#define Ntl_ManForEachNode( p, pObj, i )                                        \
     for ( i = 0; (i < Vec_PtrSize(p->vNodes)) && (((pObj) = Vec_PtrEntry(p->vNodes, i)), 1); i++ ) \
         if ( (pObj) == NULL || !Ntl_ObjIsNode(pObj) ) {} else
-#define Ntl_ManForEachBox( p, pObj, i )                                    \
+#define Ntl_ManForEachBox( p, pObj, i )                                         \
     for ( i = 0; (i < Vec_PtrSize(p->vNodes)) && (((pObj) = Vec_PtrEntry(p->vNodes, i)), 1); i++ ) \
         if ( (pObj) == NULL || !Ntl_ObjIsBox(pObj) ) {} else
 
@@ -214,6 +251,9 @@ static inline void        Ntl_ObjSetFanout( Ntl_Obj_t * p, Ntl_Net_t * pNet, int
     for ( i = 0; (i < Vec_PtrSize(pNwk->vPis)) && (((pObj) = (Ntl_Obj_t*)Vec_PtrEntry(pNwk->vPis, i)), 1); i++ )
 #define Ntl_ModelForEachPo( pNwk, pObj, i )                                     \
     for ( i = 0; (i < Vec_PtrSize(pNwk->vPos)) && (((pObj) = (Ntl_Obj_t*)Vec_PtrEntry(pNwk->vPos, i)), 1); i++ )
+#define Ntl_ModelForEachNet( pNwk, pNet, i )                                    \
+    for ( i = 0; i < pNwk->nTableSize; i++ )                                    \
+        for ( pNet = pNwk->pTable[i]; pNet; pNet = pNet->pNext ) 
 #define Ntl_ModelForEachObj( pNwk, pObj, i )                                    \
     for ( i = 0; (i < Vec_PtrSize(pNwk->vObjs)) && (((pObj) = (Ntl_Obj_t*)Vec_PtrEntry(pNwk->vObjs, i)), 1); i++ ) \
         if ( pObj == NULL ) {} else
@@ -226,15 +266,31 @@ static inline void        Ntl_ObjSetFanout( Ntl_Obj_t * p, Ntl_Net_t * pNet, int
 #define Ntl_ModelForEachBox( pNwk, pObj, i )                                    \
     for ( i = 0; (i < Vec_PtrSize(pNwk->vObjs)) && (((pObj) = (Ntl_Obj_t*)Vec_PtrEntry(pNwk->vObjs, i)), 1); i++ ) \
         if ( (pObj) == NULL || !Ntl_ObjIsBox(pObj) ) {} else
-#define Ntl_ModelForEachNet( pNwk, pNet, i )                                    \
-    for ( i = 0; i < pNwk->nTableSize; i++ )                                    \
-        for ( pNet = pNwk->pTable[i]; pNet; pNet = pNet->pNext ) 
 
 #define Ntl_ObjForEachFanin( pObj, pFanin, i )                                  \
     for ( i = 0; (i < (pObj)->nFanins) && (((pFanin) = (pObj)->pFanio[i]), 1); i++ )
 #define Ntl_ObjForEachFanout( pObj, pFanout, i )                                \
     for ( i = 0; (i < (pObj)->nFanouts) && (((pFanout) = (pObj)->pFanio[(pObj)->nFanins+i]), 1); i++ )
 
+#define Ntl_ModelForEachMapLeaf( pNwk, pObj, i )                                \
+    for ( i = 0; (i < Vec_PtrSize(pNwk->vObjs)) && (((pObj) = (Ntl_Obj_t*)Vec_PtrEntry(pNwk->vObjs, i)), 1); i++ ) \
+        if ( (pObj) == NULL || !Ntl_ObjIsMapLeaf(pObj) ) {} else
+#define Ntl_ModelForEachMapRoot( pNwk, pObj, i )                                \
+    for ( i = 0; (i < Vec_PtrSize(pNwk->vObjs)) && (((pObj) = (Ntl_Obj_t*)Vec_PtrEntry(pNwk->vObjs, i)), 1); i++ ) \
+        if ( (pObj) == NULL || !Ntl_ObjIsMapRoot(pObj) ) {} else
+#define Ntl_ModelForEachCombLeaf( pNwk, pObj, i )                                \
+    for ( i = 0; (i < Vec_PtrSize(pNwk->vObjs)) && (((pObj) = (Ntl_Obj_t*)Vec_PtrEntry(pNwk->vObjs, i)), 1); i++ ) \
+        if ( (pObj) == NULL || !Ntl_ObjIsCombLeaf(pObj) ) {} else
+#define Ntl_ModelForEachCombRoot( pNwk, pObj, i )                                \
+    for ( i = 0; (i < Vec_PtrSize(pNwk->vObjs)) && (((pObj) = (Ntl_Obj_t*)Vec_PtrEntry(pNwk->vObjs, i)), 1); i++ ) \
+        if ( (pObj) == NULL || !Ntl_ObjIsCombRoot(pObj) ) {} else
+#define Ntl_ModelForEachSeqLeaf( pNwk, pObj, i )                                \
+    for ( i = 0; (i < Vec_PtrSize(pNwk->vObjs)) && (((pObj) = (Ntl_Obj_t*)Vec_PtrEntry(pNwk->vObjs, i)), 1); i++ ) \
+        if ( (pObj) == NULL || !Ntl_ObjIsSeqLeaf(pObj) ) {} else
+#define Ntl_ModelForEachSeqRoot( pNwk, pObj, i )                                \
+    for ( i = 0; (i < Vec_PtrSize(pNwk->vObjs)) && (((pObj) = (Ntl_Obj_t*)Vec_PtrEntry(pNwk->vObjs, i)), 1); i++ ) \
+        if ( (pObj) == NULL || !Ntl_ObjIsSeqRoot(pObj) ) {} else
+
 ////////////////////////////////////////////////////////////////////////
 ///                    FUNCTION DECLARATIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -247,17 +303,17 @@ extern ABC_DLL void            Ntl_ManPrepareCec( char * pFileName1, char * pFil
 extern ABC_DLL Aig_Man_t *     Ntl_ManPrepareSec( char * pFileName1, char * pFileName2 );
 /*=== ntlExtract.c ==========================================================*/
 extern ABC_DLL Aig_Man_t *     Ntl_ManExtract( Ntl_Man_t * p );
-extern ABC_DLL Aig_Man_t *     Ntl_ManCollapse( Ntl_Man_t * p, int fSeq );
-extern ABC_DLL Aig_Man_t *     Ntl_ManCollapseForCec( Ntl_Man_t * p );
-extern ABC_DLL Aig_Man_t *     Ntl_ManCollapseForSec( Ntl_Man_t * p1, Ntl_Man_t * p2 );
+extern ABC_DLL Aig_Man_t *     Ntl_ManCollapseComb( Ntl_Man_t * p );
+extern ABC_DLL Aig_Man_t *     Ntl_ManCollapseSeq( Ntl_Man_t * p );
 /*=== ntlInsert.c ==========================================================*/
 extern ABC_DLL Ntl_Man_t *     Ntl_ManInsertMapping( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t * pAig );
 extern ABC_DLL Ntl_Man_t *     Ntl_ManInsertAig( Ntl_Man_t * p, Aig_Man_t * pAig );
 extern ABC_DLL Ntl_Man_t *     Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk );
 /*=== ntlCheck.c ==========================================================*/
 extern ABC_DLL int             Ntl_ManCheck( Ntl_Man_t * pMan );
-extern ABC_DLL int             Ntl_ModelCheck( Ntl_Mod_t * pModel );
+extern ABC_DLL int             Ntl_ModelCheck( Ntl_Mod_t * pModel, int fMain );
 extern ABC_DLL void            Ntl_ModelFixNonDrivenNets( Ntl_Mod_t * pModel );
+extern ABC_DLL void            Ntl_ModelTransformLatches( Ntl_Mod_t * pModel );
 /*=== ntlMan.c ============================================================*/
 extern ABC_DLL Ntl_Man_t *     Ntl_ManAlloc();
 extern ABC_DLL void            Ntl_ManCleanup( Ntl_Man_t * p );
@@ -269,10 +325,12 @@ extern ABC_DLL int             Ntl_ManLatchNum( Ntl_Man_t * p );
 extern ABC_DLL Ntl_Mod_t *     Ntl_ManFindModel( Ntl_Man_t * p, char * pName );
 extern ABC_DLL void            Ntl_ManPrintStats( Ntl_Man_t * p );
 extern ABC_DLL Tim_Man_t *     Ntl_ManReadTimeMan( Ntl_Man_t * p );
+extern ABC_DLL void            Ntl_ManPrintTypes( Ntl_Man_t * p );
 extern ABC_DLL Ntl_Mod_t *     Ntl_ModelAlloc( Ntl_Man_t * pMan, char * pName );
 extern ABC_DLL Ntl_Mod_t *     Ntl_ModelStartFrom( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld );
 extern ABC_DLL Ntl_Mod_t *     Ntl_ModelDup( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld );
 extern ABC_DLL void            Ntl_ModelFree( Ntl_Mod_t * p );
+extern ABC_DLL Ntl_Mod_t *     Ntl_ManCreateLatchModel( Ntl_Man_t * pMan, int Init );
 /*=== ntlMap.c ============================================================*/
 extern ABC_DLL Vec_Ptr_t *     Ntl_MappingAlloc( int nLuts, int nVars );
 extern ABC_DLL Vec_Ptr_t *     Ntl_MappingFromAig( Aig_Man_t * p );
@@ -294,11 +352,13 @@ extern ABC_DLL int             Ntl_ManSweep( Ntl_Man_t * p, int fVerbose );
 /*=== ntlTable.c ==========================================================*/
 extern ABC_DLL Ntl_Net_t *     Ntl_ModelFindNet( Ntl_Mod_t * p, char * pName );
 extern ABC_DLL Ntl_Net_t *     Ntl_ModelFindOrCreateNet( Ntl_Mod_t * p, char * pName );
-extern ABC_DLL int             Ntl_ModelFindPioNumber( Ntl_Mod_t * p, char * pName, int * pNumber );
+extern ABC_DLL int             Ntl_ModelFindPioNumber( Ntl_Mod_t * p, int fPiOnly, int fPoOnly, char * pName, int * pNumber );
 extern ABC_DLL int             Ntl_ModelSetNetDriver( Ntl_Obj_t * pObj, Ntl_Net_t * pNet );
 extern ABC_DLL int             Ntl_ModelClearNetDriver( Ntl_Obj_t * pObj, Ntl_Net_t * pNet );
 extern ABC_DLL void            Ntl_ModelDeleteNet( Ntl_Mod_t * p, Ntl_Net_t * pNet );
 extern ABC_DLL int             Ntl_ModelCountNets( Ntl_Mod_t * p );
+extern ABC_DLL int             Ntl_ManAddModel( Ntl_Man_t * p, Ntl_Mod_t * pModel );
+extern ABC_DLL Ntl_Mod_t *     Ntl_ManFindModel( Ntl_Man_t * p, char * pName );
 /*=== ntlTime.c ==========================================================*/
 extern ABC_DLL Tim_Man_t *     Ntl_ManCreateTiming( Ntl_Man_t * p );
 /*=== ntlReadBlif.c ==========================================================*/
@@ -315,9 +375,14 @@ extern ABC_DLL Vec_Ptr_t *     Ntl_ManCollectCiNames( Ntl_Man_t * p );
 extern ABC_DLL Vec_Ptr_t *     Ntl_ManCollectCoNames( Ntl_Man_t * p );
 extern ABC_DLL void            Ntl_ManMarkCiCoNets( Ntl_Man_t * p );
 extern ABC_DLL void            Ntl_ManUnmarkCiCoNets( Ntl_Man_t * p );
-extern ABC_DLL int             Ntl_ManCheckNetsAreNotMarked( Ntl_Mod_t * pModel );
 extern ABC_DLL void            Ntl_ManSetZeroInitValues( Ntl_Man_t * p );
 extern ABC_DLL void            Ntl_ManTransformInitValues( Ntl_Man_t * p );
+extern ABC_DLL int             Ntl_ModelCombLeafNum( Ntl_Mod_t * p );
+extern ABC_DLL int             Ntl_ModelCombRootNum( Ntl_Mod_t * p );
+extern ABC_DLL int             Ntl_ModelSeqLeafNum( Ntl_Mod_t * p );
+extern ABC_DLL int             Ntl_ModelSeqRootNum( Ntl_Mod_t * p );
+extern ABC_DLL int             Ntl_ModelCheckNetsAreNotMarked( Ntl_Mod_t * pModel );
+extern ABC_DLL void            Ntl_ModelClearNets( Ntl_Mod_t * pModel );
 
 #ifdef __cplusplus
 }
diff --git a/src/aig/ntl/ntlCheck.c b/src/aig/ntl/ntlCheck.c
index d5100312..d3aecc8d 100644
--- a/src/aig/ntl/ntlCheck.c
+++ b/src/aig/ntl/ntlCheck.c
@@ -40,11 +40,100 @@
   SeeAlso     []
 
 ***********************************************************************/
-int Ntl_ModelCheck( Ntl_Mod_t * pModel )
+int Ntl_ModelCheck( Ntl_Mod_t * pModel, int fMain )
 {
     Ntl_Obj_t * pObj;
     Ntl_Net_t * pNet;
     int i, k, fStatus = 1;
+
+    // check root level model
+    if ( fMain )
+    {
+        if ( Ntl_ModelLatchNum(pModel) > 0 )
+        {
+            printf( "Root level model has %d registers.\n", pModel->pName, Ntl_ModelLatchNum(pModel) );
+            fStatus = 0;
+        }
+        goto checkobjs;
+    }
+
+    // check delay information
+    if ( pModel->attrBox && pModel->attrComb )
+    {
+        if ( pModel->vDelays == NULL )
+        {
+            printf( "Warning: Comb model %s does not have delay info. Default 1.0 delays are assumed.\n", pModel->pName );
+            pModel->vDelays = Vec_IntAlloc( 3 );
+            Vec_IntPush( pModel->vDelays, -1 );
+            Vec_IntPush( pModel->vDelays, -1 );
+            Vec_IntPush( pModel->vDelays, Aig_Float2Int(1.0) );        
+        }
+        if ( pModel->vTimeInputs != NULL )
+        {
+            printf( "Combinational model %s has input arrival/required time information.\n", pModel->pName );
+            fStatus = 0;
+        }
+        if ( pModel->vTimeOutputs != NULL )
+        {
+            printf( "Combinational model %s has output arrival/required time information.\n", pModel->pName );
+            fStatus = 0;
+        }
+    }
+    if ( pModel->attrBox && !pModel->attrComb )
+    {
+        if ( pModel->vDelays != NULL )
+        {
+            printf( "Sequential model %s has delay info.\n", pModel->pName );
+            fStatus = 0;
+        }
+        if ( pModel->vTimeInputs == NULL )
+        {
+            printf( "Warning: Seq model %s does not have input arrival/required time info. Default 0.0 is assumed.\n", pModel->pName );
+            pModel->vTimeInputs = Vec_IntAlloc( 2 );
+            Vec_IntPush( pModel->vTimeInputs, -1 );
+            Vec_IntPush( pModel->vTimeInputs, Aig_Float2Int(1.0) );        
+        }
+        if ( pModel->vTimeOutputs == NULL )
+        {
+            printf( "Warning: Seq model %s does not have output arrival/required time info. Default 0.0 is assumed.\n", pModel->pName );
+            pModel->vTimeOutputs = Vec_IntAlloc( 2 );
+            Vec_IntPush( pModel->vTimeOutputs, -1 );
+            Vec_IntPush( pModel->vTimeOutputs, Aig_Float2Int(1.0) );        
+        }
+    }
+
+    // check box attributes
+    if ( pModel->attrBox )
+    {
+        if ( !pModel->attrWhite )
+        {
+            if ( Ntl_ModelNodeNum(pModel) + Ntl_ModelLut1Num(pModel) > 0 )
+            {
+                printf( "Model %s is a blackbox, yet it has %d nodes.\n", pModel->pName, Ntl_ModelNodeNum(pModel) + Ntl_ModelLut1Num(pModel) );
+                fStatus = 0;
+            }
+            if ( Ntl_ModelLatchNum(pModel) > 0 )
+            {
+                printf( "Model %s is a blackbox, yet it has %d registers.\n", pModel->pName, Ntl_ModelLatchNum(pModel) );
+                fStatus = 0;
+            }
+            return fStatus;
+        }
+        // this is a white box
+        if ( pModel->attrComb && Ntl_ModelNodeNum(pModel) + Ntl_ModelLut1Num(pModel) == 0 )
+        {
+            printf( "Model %s is a comb blackbox, yet it has no nodes.\n", pModel->pName );
+            fStatus = 0;
+        }
+        if ( !pModel->attrComb && Ntl_ModelLatchNum(pModel) == 0 )
+        {
+            printf( "Model %s is a seq blackbox, yet it has no registers.\n", pModel->pName );
+            fStatus = 0;
+        }
+    }
+
+checkobjs:
+    // check nets
     Ntl_ModelForEachNet( pModel, pNet, i )
     {
         if ( pNet->pName == NULL )
@@ -58,6 +147,8 @@ int Ntl_ModelCheck( Ntl_Mod_t * pModel )
             fStatus = 0;
         }
     }
+
+    // check objects
     Ntl_ModelForEachObj( pModel, pObj, i )
     {
         Ntl_ObjForEachFanin( pObj, pNet, k )
@@ -89,8 +180,8 @@ int Ntl_ModelCheck( Ntl_Mod_t * pModel )
 ***********************************************************************/
 int Ntl_ManCheck( Ntl_Man_t * pMan )
 {
-    Ntl_Mod_t * pMod1, * pMod2;
-    int i, k, fStatus = 1;
+    Ntl_Mod_t * pMod1;
+    int i, fStatus = 1;
     // check that the models have unique names
     Ntl_ManForEachModel( pMan, pMod1, i )
     {
@@ -99,16 +190,6 @@ int Ntl_ManCheck( Ntl_Man_t * pMan )
             printf( "Model %d does not have a name\n", i );
             fStatus = 0;
         }
-        Ntl_ManForEachModel( pMan, pMod2, k )
-        {
-            if ( i >= k )
-                continue;
-            if ( strcmp(pMod1->pName, pMod2->pName) == 0 )
-            {
-                printf( "Models %d and %d have the same name (%s).\n", i, k, pMod1->pName );
-                fStatus = 0;
-            }
-        }
     }
     // check that the models (except the first one) do not have boxes
     Ntl_ManForEachModel( pMan, pMod1, i )
@@ -124,9 +205,8 @@ int Ntl_ManCheck( Ntl_Man_t * pMan )
     // check models
     Ntl_ManForEachModel( pMan, pMod1, i )
     {
-        if ( !Ntl_ModelCheck( pMod1 ) )
+        if ( !Ntl_ModelCheck( pMod1, i==0 ) )
             fStatus = 0;
-        break;
     }
     return fStatus;
 }
@@ -150,7 +230,7 @@ void Ntl_ModelFixNonDrivenNets( Ntl_Mod_t * pModel )
     Ntl_Obj_t * pNode;
     int i;
 
-    if ( Ntl_ModelIsBlackBox(pModel) )
+    if ( !pModel->attrWhite )
         return;
 
     // check for non-driven nets
@@ -186,6 +266,37 @@ void Ntl_ModelFixNonDrivenNets( Ntl_Mod_t * pModel )
     Vec_PtrFree( vNets );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Fixed problems with non-driven nets in the model.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntl_ModelTransformLatches( Ntl_Mod_t * pModel )
+{ 
+    Ntl_Mod_t * pMod[3] = { NULL };
+    Ntl_Obj_t * pLatch;
+    int i, Init;
+    if ( Ntl_ModelLatchNum(pModel) == 0 )
+        return;
+    Ntl_ModelForEachLatch( pModel, pLatch, i )
+    {
+        Init = pLatch->LatchId.regInit;
+        if ( pMod[Init] == NULL )
+            pMod[Init] = Ntl_ManCreateLatchModel( pModel->pMan, Init );
+        pLatch->pImplem = pMod[Init];
+        pLatch->Type = NTL_OBJ_BOX;
+    }
+    printf( "Root level model %s: %d registers turned into white seq boxes.\n", pModel->pName, Ntl_ModelLatchNum(pModel) );
+    pModel->nObjs[NTL_OBJ_BOX] += Ntl_ModelLatchNum(pModel);
+    pModel->nObjs[NTL_OBJ_LATCH] = 0;
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/aig/ntl/ntlEc.c b/src/aig/ntl/ntlEc.c
index 8c7f7156..3ed6556d 100644
--- a/src/aig/ntl/ntlEc.c
+++ b/src/aig/ntl/ntlEc.c
@@ -42,33 +42,48 @@
 void Ntl_ManCreateMissingInputs( Ntl_Mod_t * p1, Ntl_Mod_t * p2, int fSeq )
 {
     Ntl_Obj_t * pObj;
-    Ntl_Net_t * pNet;
-    int i;
-    Ntl_ModelForEachPi( p1, pObj, i )
-    {
-        pNet = Ntl_ModelFindNet( p2, Ntl_ObjFanout0(pObj)->pName );
-        if ( pNet == NULL )
-            Ntl_ModelCreatePiWithName( p2, Ntl_ObjFanout0(pObj)->pName );
-    }
-    Ntl_ModelForEachPi( p2, pObj, i )
+    Ntl_Net_t * pNet, * pNext;
+    int i, k;
+    if ( fSeq )
     {
-        pNet = Ntl_ModelFindNet( p1, Ntl_ObjFanout0(pObj)->pName );
-        if ( pNet == NULL )
-            Ntl_ModelCreatePiWithName( p1, Ntl_ObjFanout0(pObj)->pName );
+        Ntl_ModelForEachSeqLeaf( p1, pObj, i )
+        {
+            Ntl_ObjForEachFanout( pObj, pNext, k )
+            {
+                pNet = Ntl_ModelFindNet( p2, pNext->pName );
+                if ( pNet == NULL )
+                    Ntl_ModelCreatePiWithName( p2, pNext->pName );
+            }
+        }
+        Ntl_ModelForEachSeqLeaf( p2, pObj, i )
+        {
+            Ntl_ObjForEachFanout( pObj, pNext, k )
+            {
+                pNet = Ntl_ModelFindNet( p1, pNext->pName );
+                if ( pNet == NULL )
+                    Ntl_ModelCreatePiWithName( p1, pNext->pName );
+            }
+        }
     }
-    if ( !fSeq )
+    else
     {
-        Ntl_ModelForEachLatch( p1, pObj, i )
+        Ntl_ModelForEachCombLeaf( p1, pObj, i )
         {
-            pNet = Ntl_ModelFindNet( p2, Ntl_ObjFanout0(pObj)->pName );
-            if ( pNet == NULL )
-                Ntl_ModelCreatePiWithName( p2, Ntl_ObjFanout0(pObj)->pName );
+            Ntl_ObjForEachFanout( pObj, pNext, k )
+            {
+                pNet = Ntl_ModelFindNet( p2, pNext->pName );
+                if ( pNet == NULL )
+                    Ntl_ModelCreatePiWithName( p2, pNext->pName );
+            }
         }
-        Ntl_ModelForEachLatch( p2, pObj, i )
+        Ntl_ModelForEachCombLeaf( p2, pObj, i )
         {
-            pNet = Ntl_ModelFindNet( p1, Ntl_ObjFanout0(pObj)->pName );
-            if ( pNet == NULL )
-                Ntl_ModelCreatePiWithName( p1, Ntl_ObjFanout0(pObj)->pName );
+            Ntl_ObjForEachFanout( pObj, pNext, k )
+            {
+                pNet = Ntl_ModelFindNet( p1, pNext->pName );
+                if ( pNet == NULL )
+                    Ntl_ModelCreatePiWithName( p1, pNext->pName );
+            }
         }
     }
 }
@@ -89,38 +104,45 @@ void Ntl_ManDeriveCommonCis( Ntl_Man_t * pMan1, Ntl_Man_t * pMan2, int fSeq )
     Ntl_Mod_t * p1 = Ntl_ManRootModel(pMan1);
     Ntl_Mod_t * p2 = Ntl_ManRootModel(pMan2);
     Ntl_Obj_t * pObj;
-    Ntl_Net_t * pNet;
-    int i;
-    if ( fSeq )
-        assert( Ntl_ModelPiNum(p1) == Ntl_ModelPiNum(p2) );
-    else
-        assert( Ntl_ModelCiNum(p1) == Ntl_ModelCiNum(p2) );
+    Ntl_Net_t * pNet, * pNext;
+    int i, k;
     // order the CIs 
     Vec_PtrClear( pMan1->vCis );
     Vec_PtrClear( pMan2->vCis );
-    Ntl_ModelForEachPi( p1, pObj, i )
+    if ( fSeq ) 
     {
-        pNet = Ntl_ModelFindNet( p2, Ntl_ObjFanout0(pObj)->pName );
-        if ( pNet == NULL )
+        assert( Ntl_ModelSeqLeafNum(p1) == Ntl_ModelSeqLeafNum(p2) );
+        Ntl_ModelForEachSeqLeaf( p1, pObj, i )
         {
-            printf( "Ntl_ManDeriveCommonCis(): Internal error!\n" );
-            return;
+            Ntl_ObjForEachFanout( pObj, pNext, k )
+            {
+                pNet = Ntl_ModelFindNet( p2, pNext->pName );
+                if ( pNet == NULL )
+                {
+                    printf( "Ntl_ManDeriveCommonCis(): Internal error!\n" );
+                    return;
+                }
+                Vec_PtrPush( pMan1->vCis, pNext );    
+                Vec_PtrPush( pMan2->vCis, pNet );  
+            }
         }
-        Vec_PtrPush( pMan1->vCis, pObj );    
-        Vec_PtrPush( pMan2->vCis, pNet->pDriver );    
     }
-    if ( !fSeq )
+    else
     {
-        Ntl_ModelForEachLatch( p1, pObj, i )
+        assert( Ntl_ModelCombLeafNum(p1) == Ntl_ModelCombLeafNum(p2) );
+        Ntl_ModelForEachCombLeaf( p1, pObj, i )
         {
-            pNet = Ntl_ModelFindNet( p2, Ntl_ObjFanout0(pObj)->pName );
-            if ( pNet == NULL )
+            Ntl_ObjForEachFanout( pObj, pNext, k )
             {
-                printf( "Ntl_ManDeriveCommonCis(): Internal error!\n" );
-                return;
+                pNet = Ntl_ModelFindNet( p2, pNext->pName );
+                if ( pNet == NULL )
+                {
+                    printf( "Ntl_ManDeriveCommonCis(): Internal error!\n" );
+                    return;
+                }
+                Vec_PtrPush( pMan1->vCis, pNext );    
+                Vec_PtrPush( pMan2->vCis, pNet );  
             }
-            Vec_PtrPush( pMan1->vCis, pObj );    
-            Vec_PtrPush( pMan2->vCis, pNet->pDriver );    
         }
     }
 }
@@ -141,45 +163,47 @@ void Ntl_ManDeriveCommonCos( Ntl_Man_t * pMan1, Ntl_Man_t * pMan2, int fSeq )
     Ntl_Mod_t * p1 = Ntl_ManRootModel(pMan1);
     Ntl_Mod_t * p2 = Ntl_ManRootModel(pMan2);
     Ntl_Obj_t * pObj;
-    Ntl_Net_t * pNet;
-    int i;
-//    if ( fSeq )
-//        assert( Ntl_ModelPoNum(p1) == Ntl_ModelPoNum(p2) );
-//    else
-//        assert( Ntl_ModelCoNum(p1) == Ntl_ModelCoNum(p2) );
-    // remember PO in the corresponding net of the second design
-    Ntl_ModelForEachPo( p2, pObj, i )
-        Ntl_ObjFanin0(pObj)->pCopy = pObj;
+    Ntl_Net_t * pNet, * pNext;
+    int i, k;
     // order the COs 
     Vec_PtrClear( pMan1->vCos );
     Vec_PtrClear( pMan2->vCos );
-    Ntl_ModelForEachPo( p1, pObj, i )
+    if ( fSeq ) 
     {
-        pNet = Ntl_ModelFindNet( p2, Ntl_ObjFanin0(pObj)->pName );
-        if ( pNet == NULL )
+        assert( Ntl_ModelSeqRootNum(p1) == Ntl_ModelSeqRootNum(p2) );
+        Ntl_ModelForEachSeqRoot( p1, pObj, i )
         {
-            printf( "Ntl_ManDeriveCommonCos(): Cannot find output %s in the second design. Skipping it!\n", 
-                Ntl_ObjFanin0(pObj)->pName );
-            continue;
+            Ntl_ObjForEachFanin( pObj, pNext, k )
+            {
+                pNet = Ntl_ModelFindNet( p2, pNext->pName );
+                if ( pNet == NULL )
+                {
+                    printf( "Ntl_ManDeriveCommonCos(): Cannot find output %s in the second design. Skipping it!\n", 
+                        pNext->pName );
+                    continue;
+                }
+                Vec_PtrPush( pMan1->vCos, pNext );    
+                Vec_PtrPush( pMan2->vCos, pNet );  
+            }
         }
-        Vec_PtrPush( pMan1->vCos, pObj );    
-        Vec_PtrPush( pMan2->vCos, pNet->pCopy );    
     }
-    if ( !fSeq )
+    else
     {
-        Ntl_ModelForEachLatch( p2, pObj, i )
-            Ntl_ObjFanin0(pObj)->pCopy = pObj;
-        Ntl_ModelForEachLatch( p1, pObj, i )
+        assert( Ntl_ModelCombRootNum(p1) == Ntl_ModelCombRootNum(p2) );
+        Ntl_ModelForEachCombRoot( p1, pObj, i )
         {
-            pNet = Ntl_ModelFindNet( p2, Ntl_ObjFanin0(pObj)->pName );
-            if ( pNet == NULL )
+            Ntl_ObjForEachFanin( pObj, pNext, k )
             {
-                printf( "Ntl_ManDeriveCommonCos(): Cannot find output %s in the second design. Skipping it!\n", 
-                    Ntl_ObjFanin0(pObj)->pName );
-                continue;
+                pNet = Ntl_ModelFindNet( p2, pNext->pName );
+                if ( pNet == NULL )
+                {
+                    printf( "Ntl_ManDeriveCommonCos(): Cannot find output %s in the second design. Skipping it!\n", 
+                        pNext->pName );
+                    continue;
+                }
+                Vec_PtrPush( pMan1->vCos, pNext );    
+                Vec_PtrPush( pMan2->vCos, pNet );  
             }
-            Vec_PtrPush( pMan1->vCos, pObj );    
-            Vec_PtrPush( pMan2->vCos, pNet->pCopy );    
         }
     }
 }
@@ -214,19 +238,19 @@ void Ntl_ManPrepareCec( char * pFileName1, char * pFileName2, Aig_Man_t ** ppMan
     // make sure they are compatible
     pModel1 = Ntl_ManRootModel( pMan1 );
     pModel2 = Ntl_ManRootModel( pMan2 );
-    if ( Ntl_ModelCiNum(pModel1) != Ntl_ModelCiNum(pModel2) )
+    if ( Ntl_ModelCombLeafNum(pModel1) != Ntl_ModelCombLeafNum(pModel2) )
     {
         printf( "Warning: The number of inputs in the designs is different (%d and %d).\n", 
-            Ntl_ModelCiNum(pModel1), Ntl_ModelCiNum(pModel2) );
+            Ntl_ModelCombLeafNum(pModel1), Ntl_ModelCombLeafNum(pModel2) );
     }
-    if ( Ntl_ModelCoNum(pModel1) != Ntl_ModelCoNum(pModel2) )
+    if ( Ntl_ModelCombRootNum(pModel1) != Ntl_ModelCombRootNum(pModel2) )
     {
         printf( "Warning: The number of outputs in the designs is different (%d and %d).\n", 
-            Ntl_ModelCoNum(pModel1), Ntl_ModelCoNum(pModel2) );
+            Ntl_ModelCombRootNum(pModel1), Ntl_ModelCombRootNum(pModel2) );
     }
     // normalize inputs/outputs
     Ntl_ManCreateMissingInputs( pModel1, pModel2, 0 );
-    if ( Ntl_ModelCiNum(pModel1) != Ntl_ModelCiNum(pModel2) )
+    if ( Ntl_ModelCombLeafNum(pModel1) != Ntl_ModelCombLeafNum(pModel2) )
     {
         if ( pMan1 )  Ntl_ManFree( pMan1 );
         if ( pMan2 )  Ntl_ManFree( pMan2 );
@@ -243,8 +267,8 @@ void Ntl_ManPrepareCec( char * pFileName1, char * pFileName2, Aig_Man_t ** ppMan
         return;
     }
     // derive AIGs
-    *ppMan1 = Ntl_ManCollapseForCec( pMan1 );
-    *ppMan2 = Ntl_ManCollapseForCec( pMan2 );
+    *ppMan1 = Ntl_ManCollapseComb( pMan1 );
+    *ppMan2 = Ntl_ManCollapseComb( pMan2 );
     // cleanup 
     Ntl_ManFree( pMan1 );
     Ntl_ManFree( pMan2 );
@@ -263,7 +287,9 @@ void Ntl_ManPrepareCec( char * pFileName1, char * pFileName2, Aig_Man_t ** ppMan
 ***********************************************************************/
 Aig_Man_t * Ntl_ManPrepareSec( char * pFileName1, char * pFileName2 )
 {
-    Aig_Man_t * pAig;
+    extern Aig_Man_t * Saig_ManCreateMiter( Aig_Man_t * p1, Aig_Man_t * p2, int Oper );
+
+    Aig_Man_t * pAig1, * pAig2, * pAig;
     Ntl_Man_t * pMan1, * pMan2;
     Ntl_Mod_t * pModel1, * pModel2;
     // read the netlists
@@ -286,12 +312,12 @@ Aig_Man_t * Ntl_ManPrepareSec( char * pFileName1, char * pFileName2 )
         printf( "Ntl_ManPrepareSec(): The designs have no latches. Use combinational command \"*cec\".\n" );
         return NULL;
     }
-    if ( Ntl_ModelPiNum(pModel1) != Ntl_ModelPiNum(pModel2) )
+    if ( Ntl_ModelSeqLeafNum(pModel1) != Ntl_ModelSeqLeafNum(pModel2) )
     {
         printf( "Warning: The number of inputs in the designs is different (%d and %d).\n", 
             Ntl_ModelPiNum(pModel1), Ntl_ModelPiNum(pModel2) );
     }
-    if ( Ntl_ModelPoNum(pModel1) != Ntl_ModelPoNum(pModel2) )
+    if ( Ntl_ModelSeqRootNum(pModel1) != Ntl_ModelSeqRootNum(pModel2) )
     {
         printf( "Warning: The number of outputs in the designs is different (%d and %d).\n", 
             Ntl_ModelPoNum(pModel1), Ntl_ModelPoNum(pModel2) );
@@ -308,9 +334,12 @@ Aig_Man_t * Ntl_ManPrepareSec( char * pFileName1, char * pFileName2 )
         return NULL;
     }
     // derive AIGs
-    pAig = Ntl_ManCollapseForSec( pMan1, pMan2 );
+    pAig1 = Ntl_ManCollapseSeq( pMan1 );
+    pAig2 = Ntl_ManCollapseSeq( pMan2 );
+    pAig = Saig_ManCreateMiter( pAig1, pAig2, 0 );
+    Aig_ManStop( pAig1 );
+    Aig_ManStop( pAig2 );
     // cleanup
-    pMan1->pAig = pMan2->pAig = NULL;
     Ntl_ManFree( pMan1 );
     Ntl_ManFree( pMan2 );
     return pAig;
diff --git a/src/aig/ntl/ntlExtract.c b/src/aig/ntl/ntlExtract.c
index be6626df..a552f949 100644
--- a/src/aig/ntl/ntlExtract.c
+++ b/src/aig/ntl/ntlExtract.c
@@ -178,6 +178,9 @@ int Ntl_ManExtract_rec( Ntl_Man_t * p, Ntl_Net_t * pNet )
     if ( Ntl_ObjIsBox(pObj) )
     {
         int LevelCur, LevelMax = -TIM_ETERNITY;
+        assert( Ntl_BoxIsComb(pObj) );
+        assert( Ntl_ModelLatchNum(pObj->pImplem) == 0 );
+        assert( pObj->pImplem->vDelays != NULL );
         Vec_IntPush( p->vBox1Cos, Aig_ManPoNum(p->pAig) );
         Ntl_ObjForEachFanin( pObj, pNetFanin, i )
         {
@@ -218,7 +221,7 @@ Aig_Man_t * Ntl_ManExtract( Ntl_Man_t * p )
     Ntl_Mod_t * pRoot;
     Ntl_Obj_t * pObj;
     Ntl_Net_t * pNet;
-    int i, nUselessObjects;
+    int i, k, nUselessObjects;
     Ntl_ManCleanup( p );
     assert( Vec_PtrSize(p->vCis) == 0 );
     assert( Vec_PtrSize(p->vCos) == 0 );
@@ -231,63 +234,39 @@ Aig_Man_t * Ntl_ManExtract( Ntl_Man_t * p )
     p->pAig->pSpec = Aig_UtilStrsav( p->pSpec );
     // get the root model
     pRoot = Ntl_ManRootModel( p );
+    assert( Ntl_ModelLatchNum(pRoot) == 0 );
     // clear net visited flags
-    Ntl_ModelForEachNet( pRoot, pNet, i )
+    Ntl_ModelClearNets( pRoot );
+    // collect mapping leafs
+    Ntl_ModelForEachMapLeaf( pRoot, pObj, i )
     {
-        pNet->nVisits = 0;
-        pNet->pCopy = NULL;
-    }
-    // collect primary inputs
-    Ntl_ModelForEachPi( pRoot, pObj, i )
-    {
-        assert( Ntl_ObjFanoutNum(pObj) == 1 );
-        pNet = Ntl_ObjFanout0(pObj);
-        Vec_PtrPush( p->vCis, pNet );
-        pNet->pCopy = Aig_ObjCreatePi( p->pAig );
-        if ( pNet->nVisits )
-        {
-            printf( "Ntl_ManExtract(): Primary input appears twice in the list.\n" );
-            return 0;
-        }
-        pNet->nVisits = 2;
-    }
-    // collect latch outputs
-    Ntl_ModelForEachLatch( pRoot, pObj, i )
-    {
-        assert( Ntl_ObjFanoutNum(pObj) == 1 );
-        pNet = Ntl_ObjFanout0(pObj);
-        Vec_PtrPush( p->vCis, pNet );
-        pNet->pCopy = Aig_ObjCreatePi( p->pAig );
-        if ( pNet->nVisits )
+        assert( !Ntl_ObjIsBox(pObj) || Ntl_BoxIsBlack(pObj) || Ntl_ModelLatchNum(pObj->pImplem) > 0 );
+        Ntl_ObjForEachFanout( pObj, pNet, k )
         {
-            printf( "Ntl_ManExtract(): Latch output is duplicated or defined as a primary input.\n" );
-            return 0;
+            Vec_PtrPush( p->vCis, pNet );
+            pNet->pCopy = Aig_ObjCreatePi( p->pAig );
+            if ( pNet->nVisits )
+            {
+                printf( "Ntl_ManExtract(): Seq leaf is duplicated or defined as a primary input.\n" );
+                return 0;
+            }
+            pNet->nVisits = 2;
         }
-        pNet->nVisits = 2;
     }
-    // visit the nodes starting from primary outputs
-    Ntl_ModelForEachPo( pRoot, pObj, i )
+    p->iLastCi = Aig_ManPiNum(p->pAig);
+    // collect mapping roots
+    Ntl_ModelForEachMapRoot( pRoot, pObj, i )
     {
-        pNet = Ntl_ObjFanin0(pObj);
-        if ( !Ntl_ManExtract_rec( p, pNet ) )
-        {
-            printf( "Ntl_ManExtract(): Error: Combinational loop is detected.\n" );
-            return 0;
-        }
-        Vec_PtrPush( p->vCos, pNet );
-        Aig_ObjCreatePo( p->pAig, pNet->pCopy );
-    }
-    // visit the nodes starting from latch inputs 
-    Ntl_ModelForEachLatch( pRoot, pObj, i )
-    {
-        pNet = Ntl_ObjFanin0(pObj);
-        if ( !Ntl_ManExtract_rec( p, pNet ) )
+        Ntl_ObjForEachFanin( pObj, pNet, k )
         {
-            printf( "Ntl_ManExtract(): Error: Combinational loop is detected.\n" );
-            return 0;
+            if ( !Ntl_ManExtract_rec( p, pNet ) )
+            {
+                printf( "Ntl_ManExtract(): Error: Combinational loop is detected.\n" );
+                return 0;
+            }
+            Vec_PtrPush( p->vCos, pNet );
+            Aig_ObjCreatePo( p->pAig, pNet->pCopy );
         }
-        Vec_PtrPush( p->vCos, pNet );
-        Aig_ObjCreatePo( p->pAig, pNet->pCopy );
     }
     // visit dangling boxes
     Ntl_ModelForEachBox( pRoot, pObj, i )
@@ -314,6 +293,9 @@ Aig_Man_t * Ntl_ManExtract( Ntl_Man_t * p )
     return pAig;    
 }
 
+
+
+
 /**Function*************************************************************
 
   Synopsis    [Collects the nodes in a topological order.]
@@ -325,9 +307,9 @@ Aig_Man_t * Ntl_ManExtract( Ntl_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Ntl_ManBuildModelAig( Ntl_Man_t * p, Ntl_Obj_t * pBox )
+int Ntl_ManCollapseBox_rec( Ntl_Man_t * p, Ntl_Obj_t * pBox, int fSeq )
 {
-    extern int Ntl_ManCollapse_rec( Ntl_Man_t * p, Ntl_Net_t * pNet );
+    extern int Ntl_ManCollapse_rec( Ntl_Man_t * p, Ntl_Net_t * pNet, int fSeq );
     Ntl_Mod_t * pModel = pBox->pImplem;
     Ntl_Obj_t * pObj;
     Ntl_Net_t * pNet, * pNetBox;
@@ -335,8 +317,7 @@ int Ntl_ManBuildModelAig( Ntl_Man_t * p, Ntl_Obj_t * pBox )
     assert( Ntl_ObjFaninNum(pBox) == Ntl_ModelPiNum(pModel) );
     assert( Ntl_ObjFanoutNum(pBox) == Ntl_ModelPoNum(pModel) );
     // clear net visited flags
-    Ntl_ModelForEachNet( pModel, pNet, i )
-        pNet->nVisits = 0;
+    Ntl_ModelClearNets( pModel );
     // transfer from the box to the PIs of the model
     Ntl_ModelForEachPi( pModel, pObj, i )
     {
@@ -345,17 +326,41 @@ int Ntl_ManBuildModelAig( Ntl_Man_t * p, Ntl_Obj_t * pBox )
         pNet->pCopy = pNetBox->pCopy;
         pNet->nVisits = 2;
     }
+    // check if there are registers
+    if ( Ntl_ModelLatchNum(pModel) )
+    {
+        Ntl_ModelForEachLatch( pModel, pObj, i )
+        {
+            pNet = Ntl_ObjFanout0(pObj);
+            pNet->pCopy = Aig_ObjCreatePi( p->pAig );
+            if ( fSeq && Ntl_ObjIsInit1( pObj ) )
+                pNet->pCopy = Aig_Not(pNet->pCopy);
+            pNet->nVisits = 2;
+        }
+    }
     // compute AIG for the internal nodes
     Ntl_ModelForEachPo( pModel, pObj, i )
-        if ( !Ntl_ManCollapse_rec( p, Ntl_ObjFanin0(pObj) ) )
-            return 0;
-    // transfer from the POs of the model to the box
-    Ntl_ModelForEachPo( pModel, pObj, i )
     {
         pNet = Ntl_ObjFanin0(pObj);
+        if ( !Ntl_ManCollapse_rec( p, pNet, fSeq ) )
+            return 0;
         pNetBox = Ntl_ObjFanout( pBox, i );
         pNetBox->pCopy = pNet->pCopy;
     }
+    // compute AIGs for the registers
+    if ( Ntl_ModelLatchNum(pModel) )
+    {
+        Ntl_ModelForEachLatch( pModel, pObj, i )
+        {
+            pNet = Ntl_ObjFanin0(pObj);
+            if ( !Ntl_ManCollapse_rec( p, pNet, fSeq ) )
+                return 0;
+            if ( fSeq && Ntl_ObjIsInit1( pObj ) )
+                Vec_PtrPush( p->vLatchIns, Aig_Not(pNet->pCopy) );
+            else
+                Vec_PtrPush( p->vLatchIns, pNet->pCopy );
+        }
+    }
     return 1;
 }
 
@@ -370,7 +375,7 @@ int Ntl_ManBuildModelAig( Ntl_Man_t * p, Ntl_Obj_t * pBox )
   SeeAlso     []
 
 ***********************************************************************/
-int Ntl_ManCollapse_rec( Ntl_Man_t * p, Ntl_Net_t * pNet )
+int Ntl_ManCollapse_rec( Ntl_Man_t * p, Ntl_Net_t * pNet, int fSeq )
 {
     Ntl_Obj_t * pObj;
     Ntl_Net_t * pNetFanin;
@@ -388,12 +393,13 @@ int Ntl_ManCollapse_rec( Ntl_Man_t * p, Ntl_Net_t * pNet )
     assert( Ntl_ObjIsNode(pObj) || Ntl_ObjIsBox(pObj) );
     // visit the input nets of the box
     Ntl_ObjForEachFanin( pObj, pNetFanin, i )
-        if ( !Ntl_ManCollapse_rec( p, pNetFanin ) )
+        if ( !Ntl_ManCollapse_rec( p, pNetFanin, fSeq ) )
             return 0;
     // add box inputs/outputs to COs/CIs
     if ( Ntl_ObjIsBox(pObj) )
     {
-        if ( !Ntl_ManBuildModelAig( p, pObj ) )
+        assert( Ntl_BoxIsWhite(pObj) );
+        if ( !Ntl_ManCollapseBox_rec( p, pObj, fSeq ) )
             return 0;
     }
     if ( Ntl_ObjIsNode(pObj) )
@@ -417,310 +423,125 @@ int Ntl_ManCollapse_rec( Ntl_Man_t * p, Ntl_Net_t * pNet )
 Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p, int fSeq )
 {
     Aig_Man_t * pAig;
+    Aig_Obj_t * pTemp;
     Ntl_Mod_t * pRoot;
-    Ntl_Obj_t * pObj;
     Ntl_Net_t * pNet;
     int i;
-    // start the AIG manager
-    assert( p->pAig == NULL );
+    assert( Vec_PtrSize(p->vCis) != 0 );
+    assert( Vec_PtrSize(p->vCos) != 0 );
+    assert( Vec_PtrSize(p->vLatchIns) == 0 );
+    // clear net visited flags
+    pRoot = Ntl_ManRootModel(p);
+    Ntl_ModelClearNets( pRoot );
+    assert( Ntl_ModelLatchNum(pRoot) == 0 );
+    // create the manager
     p->pAig = Aig_ManStart( 10000 );
     p->pAig->pName = Aig_UtilStrsav( p->pName );
     p->pAig->pSpec = Aig_UtilStrsav( p->pSpec );
-    // get the root model
-    pRoot = Ntl_ManRootModel( p );
-    // clear net visited flags
-    Ntl_ModelForEachNet( pRoot, pNet, i )
-    {
-        pNet->nVisits = 0;
-        pNet->pCopy = NULL;
-    }
-    // collect primary inputs
-    Ntl_ModelForEachPi( pRoot, pObj, i )
-    {
-        assert( Ntl_ObjFanoutNum(pObj) == 1 );
-        pNet = Ntl_ObjFanout0(pObj);
-        pNet->pCopy = Aig_ObjCreatePi( p->pAig );
-        if ( pNet->nVisits )
-        {
-            printf( "Ntl_ManCollapse(): Primary input appears twice in the list.\n" );
-            return 0;
-        }
-        pNet->nVisits = 2;
-    }
-    // collect latch outputs
-    Ntl_ModelForEachLatch( pRoot, pObj, i )
+    // set the inputs
+    Ntl_ManForEachCiNet( p, pNet, i )
     {
-        assert( Ntl_ObjFanoutNum(pObj) == 1 );
-        pNet = Ntl_ObjFanout0(pObj);
         pNet->pCopy = Aig_ObjCreatePi( p->pAig );
-        if ( fSeq && (pObj->LatchId & 3) == 1 )
-            pNet->pCopy = Aig_Not(pNet->pCopy);
         if ( pNet->nVisits )
         {
-            printf( "Ntl_ManCollapse(): Latch output is duplicated or defined as a primary input.\n" );
+            printf( "Ntl_ManCollapseForCec(): Primary input appears twice in the list.\n" );
             return 0;
         }
         pNet->nVisits = 2;
     }
-    // visit the nodes starting from primary outputs
-    Ntl_ModelForEachPo( pRoot, pObj, i )
+    // derive the outputs
+    Ntl_ManForEachCoNet( p, pNet, i )
     {
-        pNet = Ntl_ObjFanin0(pObj);
-        if ( !Ntl_ManCollapse_rec( p, pNet ) )
+        if ( !Ntl_ManCollapse_rec( p, pNet, fSeq ) )
         {
-            printf( "Ntl_ManCollapse(): Error: Combinational loop is detected.\n" );
+            printf( "Ntl_ManCollapseForCec(): Error: Combinational loop is detected.\n" );
             return 0;
         }
         Aig_ObjCreatePo( p->pAig, pNet->pCopy );
     }
-    // visit the nodes starting from latch inputs outputs
-    Ntl_ModelForEachLatch( pRoot, pObj, i )
-    {
-        pNet = Ntl_ObjFanin0(pObj);
-        if ( !Ntl_ManCollapse_rec( p, pNet ) )
-        {
-            printf( "Ntl_ManCollapse(): Error: Combinational loop is detected.\n" );
-            return 0;
-        }
-        if ( fSeq && (pObj->LatchId & 3) == 1 )
-            Aig_ObjCreatePo( p->pAig, Aig_Not(pNet->pCopy) );
-        else
-            Aig_ObjCreatePo( p->pAig, pNet->pCopy );
-    }
+    // add the latch inputs
+    Vec_PtrForEachEntry( p->vLatchIns, pTemp, i )
+        Aig_ObjCreatePo( p->pAig, pTemp );
     // cleanup the AIG
+    Aig_ManSetRegNum( p->pAig, Vec_PtrSize(p->vLatchIns) );
     Aig_ManCleanup( p->pAig );
     pAig = p->pAig; p->pAig = NULL;
     return pAig;    
 }
 
+
 /**Function*************************************************************
 
-  Synopsis    [Derives AIG for CEC.]
+  Synopsis    [Collapses the netlist combinationally.]
 
-  Description [Uses CIs/COs collected in the internal arrays.]
+  Description [Checks for combinational loops. Collects PI/PO nets.
+  Collects nodes in the topological order.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Ntl_ManCollapseForCec( Ntl_Man_t * p )
+Aig_Man_t * Ntl_ManCollapseComb( Ntl_Man_t * p )
 {
-    Aig_Man_t * pAig;
     Ntl_Mod_t * pRoot;
     Ntl_Obj_t * pObj;
     Ntl_Net_t * pNet;
-    int i;
-    // clear net visited flags
+    int i, k;
+    Vec_PtrClear( p->vCis );
+    Vec_PtrClear( p->vCos );
+    Vec_PtrClear( p->vLatchIns );
+    // prepare the model
     pRoot = Ntl_ManRootModel(p);
-    Ntl_ModelForEachNet( pRoot, pNet, i )
-    {
-        pNet->nVisits = 0;
-        pNet->pCopy = NULL;
-    }
-    // create the manager
-    p->pAig = Aig_ManStart( 10000 );
-    p->pAig->pName = Aig_UtilStrsav( p->pName );
-    p->pAig->pSpec = Aig_UtilStrsav( p->pSpec );
-    // set the inputs
-    Ntl_ManForEachCiNet( p, pObj, i )
-    {
-        assert( Ntl_ObjFanoutNum(pObj) == 1 );
-        pNet = Ntl_ObjFanout0(pObj);
-        pNet->pCopy = Aig_ObjCreatePi( p->pAig );
-        if ( pNet->nVisits )
-        {
-            printf( "Ntl_ManCollapseForCec(): Primary input appears twice in the list.\n" );
-            return 0;
-        }
-        pNet->nVisits = 2;
-    }
-    // derive the outputs
-    Ntl_ManForEachCoNet( p, pObj, i )
-    {
-        pNet = Ntl_ObjFanin0(pObj);
-        if ( !Ntl_ManCollapse_rec( p, pNet ) )
-        {
-            printf( "Ntl_ManCollapseForCec(): Error: Combinational loop is detected.\n" );
-            return 0;
-        }
-        Aig_ObjCreatePo( p->pAig, pNet->pCopy );
-    }
-    // cleanup the AIG
-    Aig_ManCleanup( p->pAig );
-    pAig = p->pAig; p->pAig = NULL;
-    return pAig;    
+    // collect the leaves for this traversal
+    Ntl_ModelForEachCombLeaf( pRoot, pObj, i )
+        Ntl_ObjForEachFanout( pObj, pNet, k )
+            Vec_PtrPush( p->vCis, pNet );
+    // collect the roots for this traversal
+    Ntl_ModelForEachCombRoot( pRoot, pObj, i )
+        Ntl_ObjForEachFanin( pObj, pNet, k )
+            Vec_PtrPush( p->vCos, pNet );
+    // perform the traversal
+    return Ntl_ManCollapse( p, 0 );
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Derives AIG for SEC.]
+  Synopsis    [Collapses the netlist combinationally.]
 
-  Description [Uses CIs/COs collected in the internal arrays.]
+  Description [Checks for combinational loops. Collects PI/PO nets.
+  Collects nodes in the topological order.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Ntl_ManCollapseForSec( Ntl_Man_t * p1, Ntl_Man_t * p2 )
+Aig_Man_t * Ntl_ManCollapseSeq( Ntl_Man_t * p )
 {
-    Aig_Man_t * pAig;
-    Aig_Obj_t * pMiter;
-    Ntl_Mod_t * pRoot1, * pRoot2;
+    Ntl_Mod_t * pRoot;
     Ntl_Obj_t * pObj;
     Ntl_Net_t * pNet;
-    Vec_Ptr_t * vPairs;
-    int i;
-    assert( Vec_PtrSize(p1->vCis) > 0 );
-    assert( Vec_PtrSize(p1->vCos) > 0 );
-    assert( Vec_PtrSize(p1->vCis) == Vec_PtrSize(p2->vCis) );
-    assert( Vec_PtrSize(p1->vCos) == Vec_PtrSize(p2->vCos) );
-
-    // create the manager
-    pAig = p1->pAig = p2->pAig = Aig_ManStart( 10000 );
-    pAig->pName = Aig_UtilStrsav( p1->pName );
-    pAig->pSpec = Aig_UtilStrsav( p1->pSpec );
-    vPairs = Vec_PtrStart( 2 * Vec_PtrSize(p1->vCos) );
-    // placehoder output to be used later for the miter output
-    Aig_ObjCreatePo( pAig, Aig_ManConst1(pAig) );
-
-    /////////////////////////////////////////////////////
-    // clear net visited flags
-    pRoot1 = Ntl_ManRootModel(p1);
-    Ntl_ModelForEachNet( pRoot1, pNet, i )
-    {
-        pNet->nVisits = 0;
-        pNet->pCopy = NULL;
-    }
-    // primary inputs
-    Ntl_ManForEachCiNet( p1, pObj, i )
-    {
-        assert( Ntl_ObjFanoutNum(pObj) == 1 );
-        pNet = Ntl_ObjFanout0(pObj);
-        pNet->pCopy = Aig_ObjCreatePi( pAig );
-        if ( pNet->nVisits )
-        {
-            printf( "Ntl_ManCollapseForSec(): Primary input appears twice in the list.\n" );
-            return 0;
-        }
-        pNet->nVisits = 2;
-    }
-    // latch outputs
-    Ntl_ModelForEachLatch( pRoot1, pObj, i )
-    {
-        assert( Ntl_ObjFanoutNum(pObj) == 1 );
-        pNet = Ntl_ObjFanout0(pObj);
-        pNet->pCopy = Aig_ObjCreatePi( pAig );
-        if ( (pObj->LatchId & 3) == 1 )
-            pNet->pCopy = Aig_Not(pNet->pCopy);
-        if ( pNet->nVisits )
-        {
-            printf( "Ntl_ManCollapseForSec(): Latch output is duplicated or defined as a primary input.\n" );
-            return 0;
-        }
-        pNet->nVisits = 2;
-    }
-    // derive the outputs
-    Ntl_ManForEachCoNet( p1, pObj, i )
-    {
-        pNet = Ntl_ObjFanin0(pObj);
-        if ( !Ntl_ManCollapse_rec( p1, pNet ) )
-        {
-            printf( "Ntl_ManCollapseForSec(): Error: Combinational loop is detected.\n" );
-            return 0;
-        }
-//        Aig_ObjCreatePo( pAig, pNet->pCopy );
-        Vec_PtrWriteEntry( vPairs, 2 * i, pNet->pCopy );
-    }
-    // visit the nodes starting from latch inputs outputs
-    Ntl_ModelForEachLatch( pRoot1, pObj, i )
-    {
-        pNet = Ntl_ObjFanin0(pObj);
-        if ( !Ntl_ManCollapse_rec( p1, pNet ) )
-        {
-            printf( "Ntl_ManCollapseForSec(): Error: Combinational loop is detected.\n" );
-            return 0;
-        }
-        if ( (pObj->LatchId & 3) == 1 )
-            Aig_ObjCreatePo( pAig, Aig_Not(pNet->pCopy) );
-        else
-            Aig_ObjCreatePo( pAig, pNet->pCopy );
-    }
-
-    /////////////////////////////////////////////////////
-    // clear net visited flags
-    pRoot2 = Ntl_ManRootModel(p2);
-    Ntl_ModelForEachNet( pRoot2, pNet, i )
-    {
-        pNet->nVisits = 0;
-        pNet->pCopy = NULL;
-    }
-    // primary inputs
-    Ntl_ManForEachCiNet( p2, pObj, i )
-    {
-        assert( Ntl_ObjFanoutNum(pObj) == 1 );
-        pNet = Ntl_ObjFanout0(pObj);
-        pNet->pCopy = Aig_ManPi( pAig, i );
-        if ( pNet->nVisits )
-        {
-            printf( "Ntl_ManCollapseForSec(): Primary input appears twice in the list.\n" );
-            return 0;
-        }
-        pNet->nVisits = 2;
-    }
-    // latch outputs
-    Ntl_ModelForEachLatch( pRoot2, pObj, i )
-    {
-        assert( Ntl_ObjFanoutNum(pObj) == 1 );
-        pNet = Ntl_ObjFanout0(pObj);
-        pNet->pCopy = Aig_ObjCreatePi( pAig );
-        if ( (pObj->LatchId & 3) == 1 )
-            pNet->pCopy = Aig_Not(pNet->pCopy);
-        if ( pNet->nVisits )
-        {
-            printf( "Ntl_ManCollapseForSec(): Latch output is duplicated or defined as a primary input.\n" );
-            return 0;
-        }
-        pNet->nVisits = 2;
-    }
-    // derive the outputs
-    Ntl_ManForEachCoNet( p2, pObj, i )
-    {
-        pNet = Ntl_ObjFanin0(pObj);
-        if ( !Ntl_ManCollapse_rec( p2, pNet ) )
-        {
-            printf( "Ntl_ManCollapseForSec(): Error: Combinational loop is detected.\n" );
-            return 0;
-        }
-//        Aig_ObjCreatePo( pAig, pNet->pCopy );
-        Vec_PtrWriteEntry( vPairs, 2 * i + 1, pNet->pCopy );
-    }
-    // visit the nodes starting from latch inputs outputs
-    Ntl_ModelForEachLatch( pRoot2, pObj, i )
-    {
-        pNet = Ntl_ObjFanin0(pObj);
-        if ( !Ntl_ManCollapse_rec( p2, pNet ) )
-        {
-            printf( "Ntl_ManCollapseForSec(): Error: Combinational loop is detected.\n" );
-            return 0;
-        }
-        if ( (pObj->LatchId & 3) == 1 )
-            Aig_ObjCreatePo( pAig, Aig_Not(pNet->pCopy) );
-        else
-            Aig_ObjCreatePo( pAig, pNet->pCopy );
-    }
-
-    /////////////////////////////////////////////////////
-    pMiter = Aig_Miter(pAig, vPairs);
-    Vec_PtrFree( vPairs );
-    Aig_ObjPatchFanin0( pAig, Aig_ManPo(pAig,0), pMiter  );
-    Aig_ManSetRegNum( pAig, Ntl_ModelLatchNum( pRoot1 ) + Ntl_ModelLatchNum( pRoot2 ) );
-    Aig_ManCleanup( pAig );
-    return pAig;    
+    int i, k;
+    Vec_PtrClear( p->vCis );
+    Vec_PtrClear( p->vCos );
+    Vec_PtrClear( p->vLatchIns );
+    // prepare the model
+    pRoot = Ntl_ManRootModel(p);
+    // collect the leaves for this traversal
+    Ntl_ModelForEachSeqLeaf( pRoot, pObj, i )
+        Ntl_ObjForEachFanout( pObj, pNet, k )
+            Vec_PtrPush( p->vCis, pNet );
+    // collect the roots for this traversal
+    Ntl_ModelForEachSeqRoot( pRoot, pObj, i )
+        Ntl_ObjForEachFanin( pObj, pNet, k )
+            Vec_PtrPush( p->vCos, pNet );
+    // perform the traversal
+    return Ntl_ManCollapse( p, 1 );
 }
 
 
+
 /**Function*************************************************************
 
   Synopsis    [Increments reference counter of the net.]
@@ -806,11 +627,7 @@ Nwk_Man_t * Ntl_ManExtractNwk( Ntl_Man_t * p, Aig_Man_t * pAig, Tim_Man_t * pMan
     vCover = Vec_IntAlloc( 100 );
     vMemory = Vec_IntAlloc( 1 << 16 );
     // count the number of fanouts of each net
-    Ntl_ModelForEachNet( pRoot, pNet, i )
-    {
-        pNet->pCopy = NULL;
-        pNet->fMark = 0;
-    }
+    Ntl_ModelClearNets( pRoot );
     Ntl_ModelForEachObj( pRoot, pObj, i )
         Ntl_ObjForEachFanin( pObj, pNet, k )
             Ntl_NetIncrementRefs( pNet );
@@ -867,11 +684,7 @@ Nwk_Man_t * Ntl_ManExtractNwk( Ntl_Man_t * p, Aig_Man_t * pAig, Tim_Man_t * pMan
         }
     }
 //    Aig_ManCleanPioNumbers( pAig );
-    Ntl_ModelForEachNet( pRoot, pNet, i )
-    {
-        pNet->pCopy = NULL;
-        pNet->fMark = 0;
-    }
+    Ntl_ModelClearNets( pRoot );
     Vec_IntFree( vCover );
     Vec_IntFree( vMemory );
     // create timing manager from the current design
diff --git a/src/aig/ntl/ntlFraig.c b/src/aig/ntl/ntlFraig.c
index 6de41679..cdc1323b 100644
--- a/src/aig/ntl/ntlFraig.c
+++ b/src/aig/ntl/ntlFraig.c
@@ -203,7 +203,7 @@ void Ntl_ManResetComplemented( Ntl_Man_t * p, Aig_Man_t * pAigCol )
     pRoot = Ntl_ManRootModel(p);
     Ntl_ModelForEachLatch( pRoot, pObj, i )
     {
-        if ( (pObj->LatchId & 3) == 1 )
+        if ( Ntl_ObjIsInit1( pObj ) )
         {
             pObjCol = Ntl_ObjFanout0(pObj)->pCopy;
             assert( pObjCol->fPhase == 0 );
@@ -275,7 +275,7 @@ Ntl_Man_t * Ntl_ManFraig( Ntl_Man_t * p, int nPartSize, int nConfLimit, int nLev
     // collapse the AIG
     pAig = Ntl_ManExtract( p );
     pNew = Ntl_ManInsertAig( p, pAig );
-    pAigCol = Ntl_ManCollapse( pNew, 0 );
+    pAigCol = Ntl_ManCollapseComb( pNew );
 
     // perform fraiging for the given design
     nPartSize = nPartSize? nPartSize : Aig_ManPoNum(pAigCol);
@@ -309,7 +309,7 @@ Ntl_Man_t * Ntl_ManScl( Ntl_Man_t * p, int fLatchConst, int fLatchEqual, int fVe
     // collapse the AIG
     pAig = Ntl_ManExtract( p );
     pNew = Ntl_ManInsertAig( p, pAig );
-    pAigCol = Ntl_ManCollapse( pNew, 1 );
+    pAigCol = Ntl_ManCollapseSeq( pNew );
 
     // perform SCL for the given design
     Aig_ManSetRegNum( pAigCol, Ntl_ModelLatchNum(Ntl_ManRootModel(p)) );
@@ -343,7 +343,7 @@ Ntl_Man_t * Ntl_ManLcorr( Ntl_Man_t * p, int nConfMax, int fVerbose )
     // collapse the AIG
     pAig = Ntl_ManExtract( p );
     pNew = Ntl_ManInsertAig( p, pAig );
-    pAigCol = Ntl_ManCollapse( pNew, 1 );
+    pAigCol = Ntl_ManCollapseSeq( pNew );
 
     // perform SCL for the given design
     Aig_ManSetRegNum( pAigCol, Ntl_ModelLatchNum(Ntl_ManRootModel(p)) );
@@ -377,7 +377,7 @@ Ntl_Man_t * Ntl_ManSsw( Ntl_Man_t * p, Fra_Ssw_t * pPars )
     // collapse the AIG
     pAig = Ntl_ManExtract( p );
     pNew = Ntl_ManInsertAig( p, pAig );
-    pAigCol = Ntl_ManCollapse( pNew, 1 );
+    pAigCol = Ntl_ManCollapseSeq( pNew );
 
     // perform SCL for the given design
     Aig_ManSetRegNum( pAigCol, Ntl_ModelLatchNum(Ntl_ManRootModel(p)) );
@@ -502,7 +502,7 @@ void Ntl_ManFlipEdges( Ntl_Man_t * p, Aig_Man_t * pAigCol )
     iLatch = 0;
     Ntl_ModelForEachLatch( pRoot, pObj, i )
     {
-        if ( (pObj->LatchId & 3) == 1 )
+        if ( Ntl_ObjIsInit1( pObj ) )
         {
             pObjCol = Aig_ManPi( pAigCol, Ntl_ModelPiNum(pRoot) + iLatch );
             assert( pObjCol->fMarkA == 0 );
@@ -524,7 +524,7 @@ void Ntl_ManFlipEdges( Ntl_Man_t * p, Aig_Man_t * pAigCol )
     iLatch = 0;
     Ntl_ModelForEachLatch( pRoot, pObj, i )
     {
-        if ( (pObj->LatchId & 3) == 1 )
+        if ( Ntl_ObjIsInit1( pObj ) )
         {
             // flip the latch input
             pObjCol = Aig_ManPo( pAigCol, Ntl_ModelPoNum(pRoot) + iLatch );
@@ -554,7 +554,7 @@ Ntl_Man_t * Ntl_ManSsw2( Ntl_Man_t * p, Fra_Ssw_t * pPars )
     Ntl_Man_t * pNew;
     Aig_Man_t * pAigRed, * pAigCol;
     // collapse the AIG
-    pAigCol = Ntl_ManCollapse( p, 1 );
+    pAigCol = Ntl_ManCollapseSeq( p );
     Aig_ManSetRegNum( pAigCol, Ntl_ModelLatchNum(Ntl_ManRootModel(p)) );
     // transform the collapsed AIG
     pAigRed = Fra_FraigInduction( pAigCol, pPars );
diff --git a/src/aig/ntl/ntlInsert.c b/src/aig/ntl/ntlInsert.c
index 3cd9470b..9675eb28 100644
--- a/src/aig/ntl/ntlInsert.c
+++ b/src/aig/ntl/ntlInsert.c
@@ -257,7 +257,7 @@ Ntl_Man_t * Ntl_ManInsertAig( Ntl_Man_t * p, Aig_Man_t * pAig )
 ***********************************************************************/
 Ntl_Man_t * Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk )
 {
-    char Buffer[100];
+    char Buffer[100]; 
     Vec_Ptr_t * vObjs;
     Vec_Int_t * vTruth;
     Vec_Int_t * vCover;
diff --git a/src/aig/ntl/ntlMan.c b/src/aig/ntl/ntlMan.c
index e80e02c6..0083e04c 100644
--- a/src/aig/ntl/ntlMan.c
+++ b/src/aig/ntl/ntlMan.c
@@ -50,9 +50,14 @@ Ntl_Man_t * Ntl_ManAlloc()
     p->vCos = Vec_PtrAlloc( 1000 );
     p->vNodes = Vec_PtrAlloc( 1000 );
     p->vBox1Cos = Vec_IntAlloc( 1000 );
+    p->vLatchIns = Vec_PtrAlloc( 1000 );
     // start the manager
     p->pMemObjs = Aig_MmFlexStart();
     p->pMemSops = Aig_MmFlexStart();
+    // allocate model table
+    p->nModTableSize = Aig_PrimeCudd( 100 );
+    p->pModTable = ALLOC( Ntl_Mod_t *, p->nModTableSize );
+    memset( p->pModTable, 0, sizeof(Ntl_Mod_t *) * p->nModTableSize );
     return p;
 }
 
@@ -185,14 +190,16 @@ void Ntl_ManFree( Ntl_Man_t * p )
             Ntl_ModelFree( pModel );
         Vec_PtrFree( p->vModels );
     }
-    if ( p->vCis )     Vec_PtrFree( p->vCis );
-    if ( p->vCos )     Vec_PtrFree( p->vCos );
-    if ( p->vNodes )   Vec_PtrFree( p->vNodes );
-    if ( p->vBox1Cos ) Vec_IntFree( p->vBox1Cos );
-    if ( p->pMemObjs ) Aig_MmFlexStop( p->pMemObjs, 0 );
-    if ( p->pMemSops ) Aig_MmFlexStop( p->pMemSops, 0 );
-    if ( p->pAig )     Aig_ManStop( p->pAig );
-    if ( p->pManTime ) Tim_ManStop( p->pManTime );
+    if ( p->vCis )      Vec_PtrFree( p->vCis );
+    if ( p->vCos )      Vec_PtrFree( p->vCos );
+    if ( p->vNodes )    Vec_PtrFree( p->vNodes );
+    if ( p->vBox1Cos )  Vec_IntFree( p->vBox1Cos );
+    if ( p->vLatchIns ) Vec_PtrFree( p->vLatchIns );
+    if ( p->pMemObjs )  Aig_MmFlexStop( p->pMemObjs, 0 );
+    if ( p->pMemSops )  Aig_MmFlexStop( p->pMemSops, 0 );
+    if ( p->pAig )      Aig_ManStop( p->pAig );
+    if ( p->pManTime )  Tim_ManStop( p->pManTime );
+    FREE( p->pModTable );
     free( p );
 }
 
@@ -239,7 +246,7 @@ int Ntl_ManLatchNum( Ntl_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Ntl_Mod_t * Ntl_ManFindModel( Ntl_Man_t * p, char * pName )
+Ntl_Mod_t * Ntl_ManFindModel_old( Ntl_Man_t * p, char * pName )
 {
     Ntl_Mod_t * pModel;
     int i;
@@ -276,6 +283,8 @@ void Ntl_ManPrintStats( Ntl_Man_t * p )
     printf( "\n" );
     fflush( stdout );
     assert( Ntl_ModelLut1Num(pRoot) == Ntl_ModelCountLut1(pRoot) );
+    Ntl_ManPrintTypes( p );
+    fflush( stdout );
 }
 
 /**Function*************************************************************
@@ -296,6 +305,67 @@ Tim_Man_t * Ntl_ManReadTimeMan( Ntl_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Saves the model type.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntl_ManSaveBoxType( Ntl_Obj_t * pObj )
+{
+    Ntl_Mod_t * pModel = pObj->pImplem;
+    int Number = 0;
+    assert( Ntl_ObjIsBox(pObj) );
+    Number |= (pModel->attrWhite << 0);
+    Number |= (pModel->attrBox   << 1);
+    Number |= (pModel->attrComb  << 2);
+    Number |= (pModel->attrKeep  << 3);
+    pModel->pMan->BoxTypes[Number]++;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Saves the model type.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntl_ManPrintTypes( Ntl_Man_t * p )
+{
+    Ntl_Mod_t * pModel;
+    Ntl_Obj_t * pObj;
+    int i;
+    pModel = Ntl_ManRootModel( p );
+    if ( Ntl_ModelBoxNum(pModel) == 0 )
+        return;
+    printf( "BOX STATISTICS:\n" );
+    Ntl_ModelForEachBox( pModel, pObj, i )
+        Ntl_ManSaveBoxType( pObj );
+    for ( i = 0; i < 15; i++ )
+    {
+        if ( !p->BoxTypes[i] )
+            continue;
+        printf( "%5d :", p->BoxTypes[i] );
+        printf( " %s", ((i & 1) > 0)? "white": "black" );
+        printf( " %s", ((i & 2) > 0)? "box  ": "logic" );
+        printf( " %s", ((i & 4) > 0)? "comb ": "seq  " );
+        printf( " %s", ((i & 8) > 0)? "keep ": "sweep" );
+        printf( "\n" );
+    }
+    printf( "Total box instances = %6d.\n\n", Ntl_ModelBoxNum(pModel) );
+    for ( i = 0; i < 15; i++ )
+        p->BoxTypes[i] = 0;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Allocates the model.]
 
   Description []
@@ -311,16 +381,25 @@ Ntl_Mod_t * Ntl_ModelAlloc( Ntl_Man_t * pMan, char * pName )
     // start the manager
     p = ALLOC( Ntl_Mod_t, 1 );
     memset( p, 0, sizeof(Ntl_Mod_t) );
+    p->attrBox   = 1;
+    p->attrComb  = 1;
+    p->attrWhite = 1;
+    p->attrKeep  = 0;
     p->pMan  = pMan;
     p->pName = Ntl_ManStoreName( p->pMan, pName );
-    Vec_PtrPush( pMan->vModels, p );
-    p->vObjs = Vec_PtrAlloc( 1000 );
-    p->vPis  = Vec_PtrAlloc( 100 );
-    p->vPos  = Vec_PtrAlloc( 100 );
+    p->vObjs = Vec_PtrAlloc( 100 );
+    p->vPis  = Vec_PtrAlloc( 10 );
+    p->vPos  = Vec_PtrAlloc( 10 ); 
     // start the table
-    p->nTableSize = Aig_PrimeCudd( 1000 );
+    p->nTableSize = Aig_PrimeCudd( 100 );
     p->pTable = ALLOC( Ntl_Net_t *, p->nTableSize );
     memset( p->pTable, 0, sizeof(Ntl_Net_t *) * p->nTableSize );
+    // add model to the table
+    if ( !Ntl_ManAddModel( pMan, p ) )
+    {
+        Ntl_ModelFree( p );
+        return NULL;
+    }
     return p;
 }
 
@@ -371,11 +450,14 @@ Ntl_Mod_t * Ntl_ModelStartFrom( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld )
             if ( pNet->pCopy != NULL )
                 Ntl_ObjSetFanout( pObj->pCopy, pNet->pCopy, k );
         if ( Ntl_ObjIsLatch(pObj) )
+        {
             ((Ntl_Obj_t *)pObj->pCopy)->LatchId = pObj->LatchId;
+            ((Ntl_Obj_t *)pObj->pCopy)->pClock = pObj->pClock->pCopy;
+        }
     }
     pModelNew->vDelays = pModelOld->vDelays? Vec_IntDup( pModelOld->vDelays ) : NULL;
-    pModelNew->vArrivals = pModelOld->vArrivals? Vec_IntDup( pModelOld->vArrivals ) : NULL;
-    pModelNew->vRequireds = pModelOld->vRequireds? Vec_IntDup( pModelOld->vRequireds ) : NULL;
+    pModelNew->vTimeInputs = pModelOld->vTimeInputs? Vec_IntDup( pModelOld->vTimeInputs ) : NULL;
+    pModelNew->vTimeOutputs = pModelOld->vTimeOutputs? Vec_IntDup( pModelOld->vTimeOutputs ) : NULL;
     return pModelNew;
 }
 
@@ -397,11 +479,20 @@ Ntl_Mod_t * Ntl_ModelDup( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld )
     Ntl_Obj_t * pObj;
     int i, k;
     pModelNew = Ntl_ModelAlloc( pManNew, pModelOld->pName );
+    pModelNew->attrWhite = pModelOld->attrWhite;
+    pModelNew->attrBox     = pModelOld->attrBox;
+    pModelNew->attrComb     = pModelOld->attrComb;
+    pModelNew->attrKeep     = pModelOld->attrKeep;
     Ntl_ModelForEachObj( pModelOld, pObj, i )
         pObj->pCopy = Ntl_ModelDupObj( pModelNew, pObj );
     Ntl_ModelForEachNet( pModelOld, pNet, i )
     {
         pNet->pCopy = Ntl_ModelFindOrCreateNet( pModelNew, pNet->pName );
+        if ( pNet->pDriver == NULL )
+        {
+            assert( !pModelOld->attrWhite );
+            continue;
+        }
         ((Ntl_Net_t *)pNet->pCopy)->pDriver = pNet->pDriver->pCopy;
         assert( pNet->pDriver->pCopy != NULL );
     }
@@ -412,13 +503,16 @@ Ntl_Mod_t * Ntl_ModelDup( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld )
         Ntl_ObjForEachFanout( pObj, pNet, k )
             Ntl_ObjSetFanout( pObj->pCopy, pNet->pCopy, k );
         if ( Ntl_ObjIsLatch(pObj) )
+        {
             ((Ntl_Obj_t *)pObj->pCopy)->LatchId = pObj->LatchId;
+            ((Ntl_Obj_t *)pObj->pCopy)->pClock = pObj->pClock->pCopy;
+        }
         if ( Ntl_ObjIsNode(pObj) )
             ((Ntl_Obj_t *)pObj->pCopy)->pSop = Ntl_ManStoreSop( pManNew->pMemSops, pObj->pSop );
     }
     pModelNew->vDelays = pModelOld->vDelays? Vec_IntDup( pModelOld->vDelays ) : NULL;
-    pModelNew->vArrivals = pModelOld->vArrivals? Vec_IntDup( pModelOld->vArrivals ) : NULL;
-    pModelNew->vRequireds = pModelOld->vRequireds? Vec_IntDup( pModelOld->vRequireds ) : NULL;
+    pModelNew->vTimeInputs = pModelOld->vTimeInputs? Vec_IntDup( pModelOld->vTimeInputs ) : NULL;
+    pModelNew->vTimeOutputs = pModelOld->vTimeOutputs? Vec_IntDup( pModelOld->vTimeOutputs ) : NULL;
     return pModelNew;
 }
 
@@ -435,10 +529,10 @@ Ntl_Mod_t * Ntl_ModelDup( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld )
 ***********************************************************************/
 void Ntl_ModelFree( Ntl_Mod_t * p )
 {
-    assert( Ntl_ManCheckNetsAreNotMarked(p) );
-    if ( p->vRequireds )  Vec_IntFree( p->vRequireds );
-    if ( p->vArrivals )   Vec_IntFree( p->vArrivals );
-    if ( p->vDelays )     Vec_IntFree( p->vDelays );
+    assert( Ntl_ModelCheckNetsAreNotMarked(p) );
+    if ( p->vTimeOutputs )  Vec_IntFree( p->vTimeOutputs );
+    if ( p->vTimeInputs )   Vec_IntFree( p->vTimeInputs );
+    if ( p->vDelays )       Vec_IntFree( p->vDelays );
     Vec_PtrFree( p->vObjs );
     Vec_PtrFree( p->vPis );
     Vec_PtrFree( p->vPos );
@@ -446,6 +540,45 @@ void Ntl_ModelFree( Ntl_Mod_t * p )
     free( p );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Create model equal to the latch with the given init value.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ntl_Mod_t * Ntl_ManCreateLatchModel( Ntl_Man_t * pMan, int Init )
+{
+    char Name[100];
+    Ntl_Mod_t * pModel;
+    Ntl_Obj_t * pObj;
+    Ntl_Net_t * pNetLi, * pNetLo;
+    // create model
+    sprintf( Name, "%s%d", "latch", Init );
+    pModel = Ntl_ModelAlloc( pMan, Name );
+    pModel->attrWhite = 1;
+    pModel->attrBox   = 1;
+    pModel->attrComb  = 0;
+    pModel->attrKeep  = 0;
+    // create primary input
+    pObj = Ntl_ModelCreatePi( pModel );
+    pNetLi = Ntl_ModelFindOrCreateNet( pModel, "li" );
+    Ntl_ModelSetNetDriver( pObj, pNetLi );
+    // create latch 
+    pObj = Ntl_ModelCreateLatch( pModel );
+    pObj->LatchId.regInit = Init;
+    pObj->pFanio[0] = pNetLi;
+    // create primary output
+    pNetLo = Ntl_ModelFindOrCreateNet( pModel, "lo" );
+    Ntl_ModelSetNetDriver( pObj, pNetLo );
+    pObj = Ntl_ModelCreatePo( pModel, pNetLo );
+    return pModel;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/ntl/ntlReadBlif.c b/src/aig/ntl/ntlReadBlif.c
index a291f8a0..ebfb2a80 100644
--- a/src/aig/ntl/ntlReadBlif.c
+++ b/src/aig/ntl/ntlReadBlif.c
@@ -38,8 +38,8 @@ struct Ioa_ReadMod_t_
     Vec_Ptr_t *          vNames;       // .names lines
     Vec_Ptr_t *          vSubckts;     // .subckt lines
     Vec_Ptr_t *          vDelays;      // .delay lines
-    Vec_Ptr_t *          vArrivals;    // .input_arrival lines
-    Vec_Ptr_t *          vRequireds;   // .output_required lines
+    Vec_Ptr_t *          vTimeInputs;  // .input_arrival/required lines
+    Vec_Ptr_t *          vTimeOutputs; // .output_required/arrival lines
     int                  fBlackBox;    // indicates blackbox model
     // the resulting network
     Ntl_Mod_t *          pNtk;   
@@ -249,14 +249,14 @@ static Ioa_ReadMod_t * Ioa_ReadModAlloc()
     Ioa_ReadMod_t * p;
     p = ALLOC( Ioa_ReadMod_t, 1 );
     memset( p, 0, sizeof(Ioa_ReadMod_t) );
-    p->vInputs  = Vec_PtrAlloc( 512 );
-    p->vOutputs = Vec_PtrAlloc( 512 );
-    p->vLatches = Vec_PtrAlloc( 512 );
-    p->vNames   = Vec_PtrAlloc( 512 );
-    p->vSubckts = Vec_PtrAlloc( 512 );
-    p->vDelays  = Vec_PtrAlloc( 512 );
-    p->vArrivals  = Vec_PtrAlloc( 512 );
-    p->vRequireds = Vec_PtrAlloc( 512 );
+    p->vInputs  = Vec_PtrAlloc( 8 );
+    p->vOutputs = Vec_PtrAlloc( 8 );
+    p->vLatches = Vec_PtrAlloc( 8 );
+    p->vNames   = Vec_PtrAlloc( 8 );
+    p->vSubckts = Vec_PtrAlloc( 8 );
+    p->vDelays  = Vec_PtrAlloc( 8 );
+    p->vTimeInputs  = Vec_PtrAlloc( 8 );
+    p->vTimeOutputs = Vec_PtrAlloc( 8 );
     return p;
 }
 
@@ -279,8 +279,8 @@ static void Ioa_ReadModFree( Ioa_ReadMod_t * p )
     Vec_PtrFree( p->vNames );
     Vec_PtrFree( p->vSubckts );
     Vec_PtrFree( p->vDelays );
-    Vec_PtrFree( p->vArrivals );
-    Vec_PtrFree( p->vRequireds );
+    Vec_PtrFree( p->vTimeInputs );
+    Vec_PtrFree( p->vTimeOutputs );
     free( p );
 }
 
@@ -509,10 +509,12 @@ static void Ioa_ReadReadPreparse( Ioa_ReadMan_t * p )
             Vec_PtrPush( p->pLatest->vSubckts, pCur );
         else if ( !strncmp(pCur, "delay", 5) )
             Vec_PtrPush( p->pLatest->vDelays, pCur );
-        else if ( !strncmp(pCur, "input_arrival", 13) )
-            Vec_PtrPush( p->pLatest->vArrivals, pCur );
-        else if ( !strncmp(pCur, "output_required", 15) )
-            Vec_PtrPush( p->pLatest->vRequireds, pCur );
+        else if ( !strncmp(pCur, "input_arrival", 13) ||
+                  !strncmp(pCur, "input_required", 14) )
+            Vec_PtrPush( p->pLatest->vTimeInputs, pCur );
+        else if ( !strncmp(pCur, "output_required", 14) ||
+                  !strncmp(pCur, "output_arrival", 13) )
+            Vec_PtrPush( p->pLatest->vTimeOutputs, pCur );
         else if ( !strncmp(pCur, "blackbox", 8) )
             p->pLatest->fBlackBox = 1;
         else if ( !strncmp(pCur, "model", 5) ) 
@@ -522,7 +524,12 @@ static void Ioa_ReadReadPreparse( Ioa_ReadMan_t * p )
             p->pLatest->pMan = p;
         }
         else if ( !strncmp(pCur, "attrib", 6) ) 
-            p->pLatest->pAttrib = pCur;
+        {
+            if ( p->pLatest->pAttrib != NULL )
+                fprintf( stdout, "Line %d: Skipping second .attrib line for this model.\n", Ioa_ReadGetLine(p, pCur) );
+            else
+                p->pLatest->pAttrib = pCur;
+        }
         else if ( !strncmp(pCur, "end", 3) )
         {
             if ( p->pLatest )
@@ -537,15 +544,6 @@ static void Ioa_ReadReadPreparse( Ioa_ReadMan_t * p )
         else if ( !strncmp(pCur, "no_merge", 8) ) 
         {
         }
-        else if ( !strncmp(pCur, "attribute", 9) ) 
-        {
-        }
-        else if ( !strncmp(pCur, "input_required", 14) ) 
-        {
-        }
-        else if ( !strncmp(pCur, "output_arrival", 14) ) 
-        {
-        }
         else
         {
             pCur--;
@@ -593,10 +591,10 @@ static int Ioa_ReadReadInterfaces( Ioa_ReadMan_t * p )
         Vec_PtrForEachEntry( pMod->vDelays, pLine, k )
             if ( !Ioa_ReadParseLineDelay( pMod, pLine ) )
                 return 0;
-        Vec_PtrForEachEntry( pMod->vArrivals, pLine, k )
+        Vec_PtrForEachEntry( pMod->vTimeInputs, pLine, k )
             if ( !Ioa_ReadParseLineTimes( pMod, pLine, 0 ) )
                 return 0;
-        Vec_PtrForEachEntry( pMod->vRequireds, pLine, k )
+        Vec_PtrForEachEntry( pMod->vTimeOutputs, pLine, k )
             if ( !Ioa_ReadParseLineTimes( pMod, pLine, 1 ) )
                 return 0;
     }
@@ -643,6 +641,8 @@ static Ntl_Man_t * Ioa_ReadParse( Ioa_ReadMan_t * p )
         return NULL;
     // update the design name
     pMod = Vec_PtrEntry( p->vModels, 0 );
+    if ( Ntl_ModelLatchNum(pMod->pNtk) > 0 )
+        Ntl_ModelTransformLatches( pMod->pNtk );
     p->pDesign->pName = Ntl_ManStoreName( p->pDesign, pMod->pNtk->pName );
     // return the network
     pDesign = p->pDesign;
@@ -674,6 +674,11 @@ static int Ioa_ReadParseLineModel( Ioa_ReadMod_t * p, char * pLine )
         return 0;
     }
     p->pNtk = Ntl_ModelAlloc( p->pMan->pDesign, Vec_PtrEntry(vTokens, 1) );
+    if ( p->pNtk == NULL )
+    {
+        sprintf( p->pMan->sError, "Line %d: Model %s already exists.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens, 1) );
+        return 0;
+    }
     return 1;
 }
 
@@ -692,23 +697,33 @@ static int Ioa_ReadParseLineAttrib( Ioa_ReadMod_t * p, char * pLine )
 {
     Vec_Ptr_t * vTokens = p->pMan->vTokens;
     char * pToken;
+    int i;
     Ioa_ReadSplitIntoTokens( vTokens, pLine, '\0' );
     pToken = Vec_PtrEntry( vTokens, 0 );
     assert( !strncmp(pToken, "attrib", 6) );
-/*
-    if ( Vec_PtrSize(vTokens) != 2 )
-    {
-        sprintf( p->pMan->sError, "Line %d: The number of entries (%d) in .attrib line is different from two.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrSize(vTokens) );
-        return 0;
-    }
-    if ( strcmp( Vec_PtrEntry(vTokens, 1), "keep" ) == 0 )
-        p->pNtk->fKeep = 1;
-    else
+    Vec_PtrForEachEntryStart( vTokens, pToken, i, 1 )
     {
-        sprintf( p->pMan->sError, "Line %d: Unknown attribute (%s) in the .attrib line of model %s.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens, 1), p->pNtk->pName );
-        return 0;
+        pToken = Vec_PtrEntry( vTokens, i );
+        if ( strcmp( pToken, "white" ) == 0 )
+            p->pNtk->attrWhite = 1;
+        else if ( strcmp( pToken, "black" ) == 0 )
+            p->pNtk->attrWhite = 0;
+        else if ( strcmp( pToken, "box" ) == 0 )
+            p->pNtk->attrBox = 1;
+        else if ( strcmp( pToken, "white" ) == 0 )
+            p->pNtk->attrWhite = 1;
+        else if ( strcmp( pToken, "comb" ) == 0 )
+            p->pNtk->attrComb = 1;
+        else if ( strcmp( pToken, "seq" ) == 0 )
+            p->pNtk->attrComb = 0;
+        else if ( strcmp( pToken, "keep" ) == 0 )
+            p->pNtk->attrKeep = 1;
+        else 
+        {
+            sprintf( p->pMan->sError, "Line %d: Unknown attribute (%s) in the .attrib line of model %s.", Ioa_ReadGetLine(p->pMan, pToken), pToken, p->pNtk->pName );
+            return 0;
+        }
     }
-*/
     return 1;
 }
 
@@ -792,7 +807,6 @@ static int Ioa_ReadParseLineLatch( Ioa_ReadMod_t * p, char * pLine )
     Ntl_Net_t * pNetLi, * pNetLo;
     Ntl_Obj_t * pObj;
     char * pToken, * pNameLi, * pNameLo;
-    int Init, Class;
     Ioa_ReadSplitIntoTokens( vTokens, pLine, '\0' );
     pToken = Vec_PtrEntry(vTokens,0);
     assert( !strcmp(pToken, "latch") );
@@ -815,31 +829,47 @@ static int Ioa_ReadParseLineLatch( Ioa_ReadMod_t * p, char * pLine )
     }
     // get initial value
     if ( Vec_PtrSize(vTokens) > 3 )
-        Init = atoi( Vec_PtrEntry(vTokens,Vec_PtrSize(vTokens)-1) );
+        pObj->LatchId.regInit = atoi( Vec_PtrEntry(vTokens,Vec_PtrSize(vTokens)-1) );
     else
-        Init = 2;
-    if ( Init < 0 || Init > 2 )
+        pObj->LatchId.regInit = 2;
+    if ( pObj->LatchId.regInit < 0 || pObj->LatchId.regInit > 2 )
     {
         sprintf( p->pMan->sError, "Line %d: Initial state of the latch is incorrect \"%s\".", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens,3) );
         return 0;
     }
     // get the register class
     if ( Vec_PtrSize(vTokens) == 6 )
-        Class = atoi( Vec_PtrEntry(vTokens,3) );
-    else
-        Class = 0;
-    if ( Class < 0 || Class > (1<<24) )
     {
-        sprintf( p->pMan->sError, "Line %d: Class of the latch is incorrect \"%s\".", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens,4) );
+        pToken = Vec_PtrEntry(vTokens,3);
+        if ( strcmp( pToken, "fe" ) == 0 )
+            pObj->LatchId.regType = 1;
+        else if ( strcmp( pToken, "re" ) == 0 )
+            pObj->LatchId.regType = 2;
+        else if ( strcmp( pToken, "ah" ) == 0 )
+            pObj->LatchId.regType = 3;
+        else if ( strcmp( pToken, "al" ) == 0 )
+            pObj->LatchId.regType = 4;
+        else if ( strcmp( pToken, "as" ) == 0 )
+            pObj->LatchId.regType = 5;
+        else if ( pToken[0] >= '0' && pToken[0] <= '9' )
+            pObj->LatchId.regClass = atoi(pToken);
+        else
+        {
+            sprintf( p->pMan->sError, "Line %d: Type/class of the latch is incorrect \"%s\".", Ioa_ReadGetLine(p->pMan, pToken), pToken );
+            return 0;
+        }
+    }
+    if ( pObj->LatchId.regClass < 0 || pObj->LatchId.regClass > (1<<24) )
+    {
+        sprintf( p->pMan->sError, "Line %d: Class of the latch is incorrect \"%s\".", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens,3) );
         return 0;
     }
-    pObj->LatchId = (Class << 2) | Init;
     // get the clock
     if ( Vec_PtrSize(vTokens) == 5 || Vec_PtrSize(vTokens) == 6 )
     {
         pToken = Vec_PtrEntry(vTokens,Vec_PtrSize(vTokens)-2);
         pNetLi = Ntl_ModelFindOrCreateNet( p->pNtk, pToken );
-//        pObj->pFanio[1] = pNetLi;
+        pObj->pClock = pNetLi;
     }
     return 1;
 }
@@ -984,7 +1014,7 @@ static int Ioa_ReadParseLineDelay( Ioa_ReadMod_t * p, char * pLine )
     RetValue1 = 0; Number1 = -1;
     if ( Vec_PtrSize(vTokens) > 2 )
     {
-        RetValue1 = Ntl_ModelFindPioNumber( p->pNtk, Vec_PtrEntry(vTokens, 1), &Number1 );
+        RetValue1 = Ntl_ModelFindPioNumber( p->pNtk, 0, 0, Vec_PtrEntry(vTokens, 1), &Number1 );
         if ( RetValue1 == 0 )
         {
             sprintf( p->pMan->sError, "Line %d: Cannot find signal \"%s\" among PIs/POs.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens, 1) );
@@ -994,7 +1024,7 @@ static int Ioa_ReadParseLineDelay( Ioa_ReadMod_t * p, char * pLine )
     RetValue2 = 0; Number2 = -1;
     if ( Vec_PtrSize(vTokens) > 3 )
     {
-        RetValue2 = Ntl_ModelFindPioNumber( p->pNtk, Vec_PtrEntry(vTokens, 2), &Number2 );
+        RetValue2 = Ntl_ModelFindPioNumber( p->pNtk, 0, 0, Vec_PtrEntry(vTokens, 2), &Number2 );
         if ( RetValue2 == 0 )
         {
             sprintf( p->pMan->sError, "Line %d: Cannot find signal \"%s\" among PIs/POs.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens, 2) );
@@ -1037,19 +1067,19 @@ static int Ioa_ReadParseLineDelay( Ioa_ReadMod_t * p, char * pLine )
 static int Ioa_ReadParseLineTimes( Ioa_ReadMod_t * p, char * pLine, int fOutput )
 {
     Vec_Ptr_t * vTokens = p->pMan->vTokens;
-    int RetValue, Number;
+    int RetValue, Number = -1;
     char * pToken, * pTokenNum;
     float Delay;
     assert( sizeof(float) == sizeof(int) );
     Ioa_ReadSplitIntoTokens( vTokens, pLine, '\0' );
     pToken = Vec_PtrEntry(vTokens,0);
     if ( fOutput )
-        assert( !strcmp(pToken, "output_required") );
+        assert( !strncmp(pToken, "output_", 7) );
     else
-        assert( !strcmp(pToken, "input_arrival") );
-    if ( Vec_PtrSize(vTokens) != 3 )
+        assert( !strncmp(pToken, "input_", 6) );
+    if ( Vec_PtrSize(vTokens) != 2 && Vec_PtrSize(vTokens) != 3 )
     {
-        sprintf( p->pMan->sError, "Line %d: Delay line does not have a valid number of parameters (3).", Ioa_ReadGetLine(p->pMan, pToken) );
+        sprintf( p->pMan->sError, "Line %d: Delay line does not have a valid number of parameters (2 or 3).", Ioa_ReadGetLine(p->pMan, pToken) );
         return 0;
     }
     // find the delay number
@@ -1068,31 +1098,37 @@ static int Ioa_ReadParseLineTimes( Ioa_ReadMod_t * p, char * pLine, int fOutput
     // find the PI/PO numbers
     if ( fOutput )
     {
-        RetValue = Ntl_ModelFindPioNumber( p->pNtk, Vec_PtrEntry(vTokens, 1), &Number );
-        if ( RetValue == 0 )
+        if ( Vec_PtrSize(vTokens) == 3 )
         {
-            sprintf( p->pMan->sError, "Line %d: Cannot find signal \"%s\" among POs.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens, 1) );
-            return 0;
+            RetValue = Ntl_ModelFindPioNumber( p->pNtk, 0, 1, Vec_PtrEntry(vTokens, 1), &Number );
+            if ( RetValue == 0 )
+            {
+                sprintf( p->pMan->sError, "Line %d: Cannot find signal \"%s\" among POs.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens, 1) );
+                return 0;
+            }
         }
         // store the values
-        if ( p->pNtk->vRequireds == NULL )
-            p->pNtk->vRequireds = Vec_IntAlloc( 100 );
-        Vec_IntPush( p->pNtk->vRequireds, Number );
-        Vec_IntPush( p->pNtk->vRequireds, Aig_Float2Int(Delay) );        
+        if ( p->pNtk->vTimeOutputs == NULL )
+            p->pNtk->vTimeOutputs = Vec_IntAlloc( 100 );
+        Vec_IntPush( p->pNtk->vTimeOutputs, Number );
+        Vec_IntPush( p->pNtk->vTimeOutputs, Aig_Float2Int(Delay) );        
     }
     else
     {
-        RetValue = Ntl_ModelFindPioNumber( p->pNtk, Vec_PtrEntry(vTokens, 1), &Number );
-        if ( RetValue == 0 )
+        if ( Vec_PtrSize(vTokens) == 3 )
         {
-            sprintf( p->pMan->sError, "Line %d: Cannot find signal \"%s\" among PIs.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens, 1) );
-            return 0;
+            RetValue = Ntl_ModelFindPioNumber( p->pNtk, 1, 0, Vec_PtrEntry(vTokens, 1), &Number );
+            if ( RetValue == 0 )
+            {
+                sprintf( p->pMan->sError, "Line %d: Cannot find signal \"%s\" among PIs.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens, 1) );
+                return 0;
+            }
         }
         // store the values
-        if ( p->pNtk->vArrivals == NULL )
-            p->pNtk->vArrivals = Vec_IntAlloc( 100 );
-        Vec_IntPush( p->pNtk->vArrivals, Number );
-        Vec_IntPush( p->pNtk->vArrivals, Aig_Float2Int(Delay) );        
+        if ( p->pNtk->vTimeInputs == NULL )
+            p->pNtk->vTimeInputs = Vec_IntAlloc( 100 );
+        Vec_IntPush( p->pNtk->vTimeInputs, Number );
+        Vec_IntPush( p->pNtk->vTimeInputs, Aig_Float2Int(Delay) );        
     }
     return 1;
 }
diff --git a/src/aig/ntl/ntlSweep.c b/src/aig/ntl/ntlSweep.c
index 8309e1b3..991d701a 100644
--- a/src/aig/ntl/ntlSweep.c
+++ b/src/aig/ntl/ntlSweep.c
@@ -79,7 +79,7 @@ void Ntl_ManSweepMark( Ntl_Man_t * p )
         Ntl_ManSweepMark_rec( p, pObj );
     // start from the persistant boxes
     Ntl_ModelForEachBox( pRoot, pObj, i )
-        if ( pObj->pImplem->fKeep )
+        if ( pObj->pImplem->attrKeep )
             Ntl_ManSweepMark_rec( p, pObj );
 }
 
diff --git a/src/aig/ntl/ntlTable.c b/src/aig/ntl/ntlTable.c
index c3acc0b1..fe58e2f8 100644
--- a/src/aig/ntl/ntlTable.c
+++ b/src/aig/ntl/ntlTable.c
@@ -189,7 +189,7 @@ Ntl_Net_t * Ntl_ModelFindOrCreateNet( Ntl_Mod_t * p, char * pName )
   SeeAlso     []
 
 ***********************************************************************/
-int Ntl_ModelFindPioNumber( Ntl_Mod_t * p, char * pName, int * pNumber )
+int Ntl_ModelFindPioNumber( Ntl_Mod_t * p, int fPiOnly, int fPoOnly, char * pName, int * pNumber )
 {
     Ntl_Net_t * pNet;
     Ntl_Obj_t * pObj;
@@ -198,6 +198,30 @@ int Ntl_ModelFindPioNumber( Ntl_Mod_t * p, char * pName, int * pNumber )
     pNet = Ntl_ModelFindNet( p, pName );
     if ( pNet == NULL )
         return 0;
+    if ( fPiOnly )
+    {
+        Ntl_ModelForEachPi( p, pObj, i )
+        {
+            if ( Ntl_ObjFanout0(pObj) == pNet )
+            {
+                *pNumber = i;
+                return -1;
+            }
+        }
+        return 0;
+    }
+    if ( fPoOnly )
+    {
+        Ntl_ModelForEachPo( p, pObj, i )
+        {
+            if ( Ntl_ObjFanin0(pObj) == pNet )
+            {
+                *pNumber = i;
+                return 1;
+            }
+        }
+        return 0;
+    }
     Ntl_ModelForEachPo( p, pObj, i )
     {
         if ( Ntl_ObjFanin0(pObj) == pNet )
@@ -281,6 +305,97 @@ int Ntl_ModelCountNets( Ntl_Mod_t * p )
     return Counter;
 }
 
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Resizes the table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntl_ManModelTableResize( Ntl_Man_t * p )
+{
+    Ntl_Mod_t ** pModTableNew, ** ppSpot, * pEntry, * pEntry2;
+    int nModTableSizeNew, Counter, e, clk;
+clk = clock();
+    // get the new table size
+    nModTableSizeNew = Aig_PrimeCudd( 3 * p->nModTableSize ); 
+    // allocate a new array
+    pModTableNew = ALLOC( Ntl_Mod_t *, nModTableSizeNew );
+    memset( pModTableNew, 0, sizeof(Ntl_Mod_t *) * nModTableSizeNew );
+    // rehash entries 
+    Counter = 0;
+    for ( e = 0; e < p->nModTableSize; e++ )
+        for ( pEntry = p->pModTable[e], pEntry2 = pEntry? pEntry->pNext : NULL; 
+              pEntry; pEntry = pEntry2, pEntry2 = pEntry? pEntry->pNext : NULL )
+            {
+                ppSpot = pModTableNew + Ntl_HashString( pEntry->pName, nModTableSizeNew );
+                pEntry->pNext = *ppSpot;
+                *ppSpot = pEntry;
+                Counter++;
+            }
+    assert( Counter == p->nModEntries );
+//    printf( "Increasing the structural table size from %6d to %6d. ", p->nTableSize, nTableSizeNew );
+//    PRT( "Time", clock() - clk );
+    // replace the table and the parameters
+    free( p->pModTable );
+    p->pModTable = pModTableNew;
+    p->nModTableSize = nModTableSizeNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Finds or creates the net.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntl_ManAddModel( Ntl_Man_t * p, Ntl_Mod_t * pModel )
+{
+    Ntl_Mod_t * pEnt;
+    unsigned Key = Ntl_HashString( pModel->pName, p->nModTableSize );
+    for ( pEnt = p->pModTable[Key]; pEnt; pEnt = pEnt->pNext )
+        if ( !strcmp( pEnt->pName, pModel->pName ) )
+            return 0;
+    pModel->pNext = p->pModTable[Key];
+    p->pModTable[Key] = pModel;
+    if ( ++p->nModEntries > 2 * p->nModTableSize )
+        Ntl_ManModelTableResize( p );
+    Vec_PtrPush( p->vModels, pModel );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Finds or creates the net.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ntl_Mod_t * Ntl_ManFindModel( Ntl_Man_t * p, char * pName )
+{
+    Ntl_Mod_t * pEnt;
+    unsigned Key = Ntl_HashString( pName, p->nModTableSize );
+    for ( pEnt = p->pModTable[Key]; pEnt; pEnt = pEnt->pNext )
+        if ( !strcmp( pEnt->pName, pName ) )
+            return pEnt;
+    return NULL;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/ntl/ntlTime.c b/src/aig/ntl/ntlTime.c
index 94691ab8..c23a4e24 100644
--- a/src/aig/ntl/ntlTime.c
+++ b/src/aig/ntl/ntlTime.c
@@ -88,13 +88,27 @@ Tim_Man_t * Ntl_ManCreateTiming( Ntl_Man_t * p )
     // start the timing manager
     pMan = Tim_ManStart( Aig_ManPiNum(p->pAig), Aig_ManPoNum(p->pAig) );
     // unpack the data in the arrival times
-    if ( pRoot->vArrivals )
-        Vec_IntForEachEntry( pRoot->vArrivals, Entry, i )
-            Tim_ManInitCiArrival( pMan, Entry, Aig_Int2Float(Vec_IntEntry(pRoot->vArrivals,++i)) );
+    if ( pRoot->vTimeInputs )
+    {
+        Vec_IntForEachEntry( pRoot->vTimeInputs, Entry, i )
+        {
+            if ( Entry == -1 )
+                Tim_ManSetCiArrivalAll( pMan, Aig_Int2Float(Vec_IntEntry(pRoot->vTimeInputs,++i)) );
+            else
+                Tim_ManInitCiArrival( pMan, Entry, Aig_Int2Float(Vec_IntEntry(pRoot->vTimeInputs,++i)) );
+        }
+    }
     // unpack the data in the required times
-    if ( pRoot->vRequireds )
-        Vec_IntForEachEntry( pRoot->vRequireds, Entry, i )
-            Tim_ManInitCoRequired( pMan, Entry, Aig_Int2Float(Vec_IntEntry(pRoot->vRequireds,++i)) );
+    if ( pRoot->vTimeOutputs )
+    {
+        Vec_IntForEachEntry( pRoot->vTimeOutputs, Entry, i )
+        {
+            if ( Entry == -1 )
+                Tim_ManSetCoRequiredAll( pMan, Aig_Int2Float(Vec_IntEntry(pRoot->vTimeOutputs,++i)) );
+            else
+                Tim_ManInitCoRequired( pMan, Entry, Aig_Int2Float(Vec_IntEntry(pRoot->vTimeOutputs,++i)) );
+        }
+    }
     // derive timing tables
     vDelayTables = Vec_PtrAlloc( Vec_PtrSize(p->vModels) );
     Ntl_ManForEachModel( p, pModel, i )
@@ -106,7 +120,7 @@ Tim_Man_t * Ntl_ManCreateTiming( Ntl_Man_t * p )
     Tim_ManSetDelayTables( pMan, vDelayTables );
     // set up the boxes
     iBox = 0;
-    curPi = Ntl_ModelCiNum(pRoot);
+    curPi = p->iLastCi;
     Ntl_ManForEachBox( p, pObj, i )
     {
         Tim_ManCreateBoxFirst( pMan, Vec_IntEntry(p->vBox1Cos, iBox), Ntl_ObjFaninNum(pObj), curPi, Ntl_ObjFanoutNum(pObj), pObj->pImplem->pDelayTable );
diff --git a/src/aig/ntl/ntlUtil.c b/src/aig/ntl/ntlUtil.c
index 6849889d..c9ef2dc4 100644
--- a/src/aig/ntl/ntlUtil.c
+++ b/src/aig/ntl/ntlUtil.c
@@ -238,26 +238,6 @@ void Ntl_ManUnmarkCiCoNets( Ntl_Man_t * p )
 
 /**Function*************************************************************
 
-  Synopsis    [Unmarks the CI/CO nets.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Ntl_ManCheckNetsAreNotMarked( Ntl_Mod_t * pModel )
-{
-    Ntl_Net_t * pNet;
-    int i;
-    Ntl_ModelForEachNet( pModel, pNet, i )
-        assert( pNet->fMark == 0 );
-    return 1;
-}
-
-/**Function*************************************************************
-
   Synopsis    [Convert initial values of registers to be zero.]
 
   Description []
@@ -274,7 +254,7 @@ void Ntl_ManSetZeroInitValues( Ntl_Man_t * p )
     int i;
     pRoot = Ntl_ManRootModel(p);
     Ntl_ModelForEachLatch( pRoot, pObj, i )
-        pObj->LatchId &= ~3;
+        pObj->LatchId.regInit = 0;
 }
 
 /**Function*************************************************************
@@ -296,7 +276,7 @@ void Ntl_ManAddInverters( Ntl_Obj_t * pObj )
     Ntl_Net_t * pNetLo, * pNetLi, * pNetLoInv, * pNetLiInv;
     Ntl_Obj_t * pNode;
     int nLength, RetValue;
-    assert( (pObj->LatchId & 3) == 1 );
+    assert( Ntl_ObjIsInit1( pObj ) );
     // get the nets
     pNetLi = Ntl_ObjFanin0(pObj);
     pNetLo = Ntl_ObjFanout0(pObj);
@@ -362,11 +342,132 @@ void Ntl_ManTransformInitValues( Ntl_Man_t * p )
     pRoot = Ntl_ManRootModel(p);
     Ntl_ModelForEachLatch( pRoot, pObj, i )
     {
-        if ( (pObj->LatchId & 3) == 1 )
+        if ( Ntl_ObjIsInit1( pObj ) )
             Ntl_ManAddInverters( pObj );
-        pObj->LatchId &= ~3;
+        pObj->LatchId.regInit = 0;
     }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of CIs in the model.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntl_ModelCombLeafNum( Ntl_Mod_t * p )
+{
+    Ntl_Obj_t * pObj;
+    int i, Counter = 0;
+    Ntl_ModelForEachCombLeaf( p, pObj, i )
+        Counter += Ntl_ObjFanoutNum( pObj );
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of COs in the model.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntl_ModelCombRootNum( Ntl_Mod_t * p )
+{
+    Ntl_Obj_t * pObj;
+    int i, Counter = 0;
+    Ntl_ModelForEachCombRoot( p, pObj, i )
+        Counter += Ntl_ObjFaninNum( pObj );
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of CIs in the model.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntl_ModelSeqLeafNum( Ntl_Mod_t * p )
+{
+    Ntl_Obj_t * pObj;
+    int i, Counter = 0;
+    Ntl_ModelForEachSeqLeaf( p, pObj, i )
+        Counter += Ntl_ObjFanoutNum( pObj );
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of COs in the model.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntl_ModelSeqRootNum( Ntl_Mod_t * p )
+{
+    Ntl_Obj_t * pObj;
+    int i, Counter = 0;
+    Ntl_ModelForEachSeqRoot( p, pObj, i )
+        Counter += Ntl_ObjFaninNum( pObj );
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Unmarks the CI/CO nets.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntl_ModelCheckNetsAreNotMarked( Ntl_Mod_t * pModel )
+{
+    Ntl_Net_t * pNet;
+    int i;
+    Ntl_ModelForEachNet( pModel, pNet, i )
+        assert( pNet->fMark == 0 );
+    return 1;
+}
+
+/**Function*************************************************************
 
+  Synopsis    [Unmarks the CI/CO nets.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntl_ModelClearNets( Ntl_Mod_t * pModel )
+{
+    Ntl_Net_t * pNet;
+    int i;
+    Ntl_ModelForEachNet( pModel, pNet, i )
+    {
+        pNet->nVisits = 0;
+        pNet->pCopy = NULL;
+    }
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/ntl/ntlWriteBlif.c b/src/aig/ntl/ntlWriteBlif.c
index 51d41c26..f93e3fa1 100644
--- a/src/aig/ntl/ntlWriteBlif.c
+++ b/src/aig/ntl/ntlWriteBlif.c
@@ -40,15 +40,22 @@
   SeeAlso     []
 
 ***********************************************************************/
-void Ioa_WriteBlifModel( FILE * pFile, Ntl_Mod_t * pModel )
+void Ioa_WriteBlifModel( FILE * pFile, Ntl_Mod_t * pModel, int fMain )
 {
     Ntl_Obj_t * pObj;
     Ntl_Net_t * pNet;
     float Delay;
-    int i, k, fClockAdded = 0;
+    int i, k;
     fprintf( pFile, ".model %s\n", pModel->pName );
-    if ( pModel->fKeep )
-        fprintf( pFile, ".attrib keep\n" );
+    if ( pModel->attrWhite || pModel->attrBox || pModel->attrComb || pModel->attrKeep )
+    {
+        fprintf( pFile, ".attrib" );
+        fprintf( pFile, " %s", pModel->attrWhite? "white": "black" );
+        fprintf( pFile, " %s", pModel->attrBox?   "box"  : "logic" );
+        fprintf( pFile, " %s", pModel->attrComb?  "comb" : "seq"   );
+//        fprintf( pFile, " %s", pModel->attrKeep?  "keep" : "sweep" );
+        fprintf( pFile, "\n" );
+    }
     fprintf( pFile, ".inputs" );
     Ntl_ModelForEachPi( pModel, pObj, i )
         fprintf( pFile, " %s", Ntl_ObjFanout0(pObj)->pName );
@@ -63,19 +70,25 @@ void Ioa_WriteBlifModel( FILE * pFile, Ntl_Mod_t * pModel )
         for ( i = 0; i < Vec_IntSize(pModel->vDelays); i += 3 )
         {
             fprintf( pFile, ".delay" );
-            fprintf( pFile, " %s", Ntl_ObjFanout0(Ntl_ModelPi(pModel, Vec_IntEntry(pModel->vDelays,i)))->pName );
-            fprintf( pFile, " %s", Ntl_ObjFanin0(Ntl_ModelPo(pModel, Vec_IntEntry(pModel->vDelays,i+1)))->pName );
+            if ( Vec_IntEntry(pModel->vDelays,i) != -1 )
+                fprintf( pFile, " %s", Ntl_ObjFanout0(Ntl_ModelPi(pModel, Vec_IntEntry(pModel->vDelays,i)))->pName );
+            if ( Vec_IntEntry(pModel->vDelays,i+1) != -1 )
+                fprintf( pFile, " %s", Ntl_ObjFanin0(Ntl_ModelPo(pModel, Vec_IntEntry(pModel->vDelays,i+1)))->pName );
             fprintf( pFile, " %.3f", Aig_Int2Float(Vec_IntEntry(pModel->vDelays,i+2)) );
             fprintf( pFile, "\n" );
         }
     }
-    if ( pModel->vArrivals )
+    if ( pModel->vTimeInputs )
     {
-        for ( i = 0; i < Vec_IntSize(pModel->vArrivals); i += 2 )
+        for ( i = 0; i < Vec_IntSize(pModel->vTimeInputs); i += 2 )
         {
-            fprintf( pFile, ".input_arrival" );
-            fprintf( pFile, " %s", Ntl_ObjFanout0(Ntl_ModelPi(pModel, Vec_IntEntry(pModel->vArrivals,i)))->pName );
-            Delay = Aig_Int2Float(Vec_IntEntry(pModel->vArrivals,i+1));
+            if ( fMain )
+                fprintf( pFile, ".input_arrival" );
+            else
+                fprintf( pFile, ".input_required" );
+            if ( Vec_IntEntry(pModel->vTimeInputs,i) != -1 )
+                fprintf( pFile, " %s", Ntl_ObjFanout0(Ntl_ModelPi(pModel, Vec_IntEntry(pModel->vTimeInputs,i)))->pName );
+            Delay = Aig_Int2Float(Vec_IntEntry(pModel->vTimeInputs,i+1));
             if ( Delay == -TIM_ETERNITY )
                 fprintf( pFile, " -inf" );
             else if ( Delay == TIM_ETERNITY )
@@ -85,13 +98,17 @@ void Ioa_WriteBlifModel( FILE * pFile, Ntl_Mod_t * pModel )
             fprintf( pFile, "\n" );
         }
     }
-    if ( pModel->vRequireds )
+    if ( pModel->vTimeOutputs )
     {
-        for ( i = 0; i < Vec_IntSize(pModel->vRequireds); i += 2 )
+        for ( i = 0; i < Vec_IntSize(pModel->vTimeOutputs); i += 2 )
         {
-            fprintf( pFile, ".output_required" );
-            fprintf( pFile, " %s", Ntl_ObjFanin0(Ntl_ModelPo(pModel, Vec_IntEntry(pModel->vRequireds,i)))->pName );
-            Delay = Aig_Int2Float(Vec_IntEntry(pModel->vRequireds,i+1));
+            if ( fMain )
+                fprintf( pFile, ".output_required" );
+            else
+                fprintf( pFile, ".output_arrival" );
+            if ( Vec_IntEntry(pModel->vTimeOutputs,i) != -1 )
+                fprintf( pFile, " %s", Ntl_ObjFanin0(Ntl_ModelPo(pModel, Vec_IntEntry(pModel->vTimeOutputs,i)))->pName );
+            Delay = Aig_Int2Float(Vec_IntEntry(pModel->vTimeOutputs,i+1));
             if ( Delay == -TIM_ETERNITY )
                 fprintf( pFile, " -inf" );
             else if ( Delay == TIM_ETERNITY )
@@ -117,13 +134,27 @@ void Ioa_WriteBlifModel( FILE * pFile, Ntl_Mod_t * pModel )
             fprintf( pFile, ".latch" );
             fprintf( pFile, " %s", Ntl_ObjFanin0(pObj)->pName );
             fprintf( pFile, " %s", Ntl_ObjFanout0(pObj)->pName );
-            if ( pObj->LatchId >> 2 )
-                fprintf( pFile, " %d", pObj->LatchId >> 2 );
-            if ( Ntl_ObjFanin(pObj, 1) != NULL )
-                fprintf( pFile, " %s", Ntl_ObjFanin(pObj, 1)->pName );
-            else if ( pObj->LatchId >> 2 )
-                fprintf( pFile, " clock99" ), fClockAdded = 1;
-            fprintf( pFile, " %d", pObj->LatchId & 3 );
+            assert( pObj->LatchId.regType == 0 || pObj->LatchId.regClass == 0 );
+            if ( pObj->LatchId.regType )
+            {
+                if ( pObj->LatchId.regType == 1 )
+                    fprintf( pFile, " fe" );
+                else if ( pObj->LatchId.regType == 2 )
+                    fprintf( pFile, " re" );
+                else if ( pObj->LatchId.regType == 3 )
+                    fprintf( pFile, " ah" );
+                else if ( pObj->LatchId.regType == 4 )
+                    fprintf( pFile, " al" );
+                else if ( pObj->LatchId.regType == 5 )
+                    fprintf( pFile, " as" );
+                else
+                    assert( 0 );
+            }
+            else if ( pObj->LatchId.regClass )
+                fprintf( pFile, " %d", pObj->LatchId.regClass );
+            if ( pObj->pClock )
+                fprintf( pFile, " %s", pObj->pClock->pName );
+            fprintf( pFile, " %d", pObj->LatchId.regInit );
             fprintf( pFile, "\n" );
         }
         else if ( Ntl_ObjIsBox(pObj) )
@@ -136,8 +167,6 @@ void Ioa_WriteBlifModel( FILE * pFile, Ntl_Mod_t * pModel )
             fprintf( pFile, "\n" );
         }
     }
-    if ( fClockAdded )
-        fprintf( pFile, ".names clock99\n 0\n" );
     fprintf( pFile, ".end\n\n" );
 }
 
@@ -167,7 +196,7 @@ void Ioa_WriteBlif( Ntl_Man_t * p, char * pFileName )
     fprintf( pFile, "# Benchmark \"%s\" written by ABC-8 on %s\n", p->pName, Ioa_TimeStamp() );
     // write the models
     Ntl_ManForEachModel( p, pModel, i )
-        Ioa_WriteBlifModel( pFile, pModel );
+        Ioa_WriteBlifModel( pFile, pModel, i==0 );
     // close the file
     fclose( pFile );
 }
diff --git a/src/aig/saig/module.make b/src/aig/saig/module.make
index 50d6db49..6639db21 100644
--- a/src/aig/saig/module.make
+++ b/src/aig/saig/module.make
@@ -3,6 +3,7 @@ SRC +=    src/aig/saig/saigBmc.c \
     src/aig/saig/saigHaig.c \
     src/aig/saig/saigInter.c \
     src/aig/saig/saigIoa.c \
+    src/aig/saig/saigMiter.c \
     src/aig/saig/saigPhase.c \
     src/aig/saig/saigRetFwd.c \
     src/aig/saig/saigRetMin.c \
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index 67f38758..f3bd028a 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -86,6 +86,8 @@ extern void              Saig_ManDumpBlif( Aig_Man_t * p, char * pFileName );
 extern Aig_Man_t *       Saig_ManReadBlif( char * pFileName );
 /*=== saigInter.c ==========================================================*/
 extern int               Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int fRewrite, int fTransLoop, int fVerbose, int * pDepth );
+/*=== saigMiter.c ==========================================================*/
+extern Aig_Man_t *       Saig_ManCreateMiter( Aig_Man_t * p1, Aig_Man_t * p2, int Oper );
 /*=== saigPhase.c ==========================================================*/
 extern Aig_Man_t *       Saig_ManPhaseAbstract( Aig_Man_t * p, Vec_Int_t * vInits, int nFrames, int fIgnore, int fPrint, int fVerbose );
 /*=== saigRetFwd.c ==========================================================*/
diff --git a/src/aig/saig/saigBmc.c b/src/aig/saig/saigBmc.c
index 32b2d186..f03364a4 100644
--- a/src/aig/saig/saigBmc.c
+++ b/src/aig/saig/saigBmc.c
@@ -277,6 +277,8 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim
                 free( pModel );
                 Vec_IntFree( vCiIds );
 
+//                if ( piFrame )
+//                    *piFrame = i / Saig_ManPoNum(pAig);
                 RetValue = 0;
                 break;
             }
diff --git a/src/aig/saig/saigMiter.c b/src/aig/saig/saigMiter.c
new file mode 100644
index 00000000..fc721154
--- /dev/null
+++ b/src/aig/saig/saigMiter.c
@@ -0,0 +1,95 @@
+/**CFile****************************************************************
+
+  FileName    [saigMiter.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Sequential AIG package.]
+
+  Synopsis    [Computes sequential miter of two sequential AIGs.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: saigMiter.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "saig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManCreateMiter( Aig_Man_t * p1, Aig_Man_t * p2, int Oper )
+{
+    Aig_Man_t * pNew;
+    Aig_Obj_t * pObj;
+    int i;
+    assert( Saig_ManRegNum(p1) > 0 || Saig_ManRegNum(p2) > 0 );
+    assert( Saig_ManPiNum(p1) == Saig_ManPiNum(p2) );
+    assert( Saig_ManPoNum(p1) == Saig_ManPoNum(p2) );
+    pNew = Aig_ManStart( Aig_ManObjNumMax(p1) + Aig_ManObjNumMax(p2) );
+    // map constant nodes
+    Aig_ManConst1(p1)->pData = Aig_ManConst1(pNew);
+    Aig_ManConst1(p2)->pData = Aig_ManConst1(pNew);
+    // map primary inputs
+    Saig_ManForEachPi( p1, pObj, i )
+        pObj->pData = Aig_ObjCreatePi( pNew );
+    Saig_ManForEachPi( p2, pObj, i )
+        pObj->pData = Aig_ManPi( pNew, i );
+    // map register outputs
+    Saig_ManForEachLo( p1, pObj, i )
+        pObj->pData = Aig_ObjCreatePi( pNew );
+    Saig_ManForEachLo( p2, pObj, i )
+        pObj->pData = Aig_ObjCreatePi( pNew );
+    // map internal nodes
+    Aig_ManForEachNode( p1, pObj, i )
+        pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+    Aig_ManForEachNode( p2, pObj, i )
+        pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+    // create primary outputs
+    Saig_ManForEachPo( p1, pObj, i )
+    {
+        if ( Oper == 0 ) // XOR
+            pObj = Aig_Exor( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild0Copy(Aig_ManPo(p2,0)) );
+        else if ( Oper == 1 ) // implication is PO(p1) -> PO(p2)  ...  complement is PO(p1) & !PO(p2) 
+            pObj = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_Not(Aig_ObjChild0Copy(Aig_ManPo(p2,0))) );
+        else
+            assert( 0 );
+    }
+    // create register inputs
+    Saig_ManForEachLi( p1, pObj, i )
+        pObj->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+    Saig_ManForEachLi( p2, pObj, i )
+        pObj->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+    // cleanup
+    Aig_ManSetRegNum( pNew, Saig_ManRegNum(p1) + Saig_ManRegNum(p2) );
+    Aig_ManCleanup( pNew );
+    return pNew;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/saig/saigScl.c b/src/aig/saig/saigScl.c
index b747eff9..67e3e95b 100644
--- a/src/aig/saig/saigScl.c
+++ b/src/aig/saig/saigScl.c
@@ -67,6 +67,42 @@ void Saig_ManReportUselessRegisters( Aig_Man_t * pAig )
         printf( "Network has %d (out of %d) registers driven by PIs.\n", Counter2, Saig_ManRegNum(pAig) );
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    [Report the number of pairs of complemented registers.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Saig_ManReportComplements( Aig_Man_t * p )
+{
+    Aig_Obj_t * pObj, * pFanin;
+    int i, Counter = 0, Diffs = 0;
+    assert( Aig_ManRegNum(p) > 0 );
+    Aig_ManForEachObj( p, pObj, i )
+        assert( !pObj->fMarkA );
+    Aig_ManForEachLiSeq( p, pObj, i )
+    {
+        pFanin = Aig_ObjFanin0(pObj);
+        if ( pFanin->fMarkA )
+            Counter++;
+        else
+            pFanin->fMarkA = 1;
+    }
+    // count fanins that have both attributes
+    Aig_ManForEachLiSeq( p, pObj, i )
+    {
+        pFanin = Aig_ObjFanin0(pObj);
+        pFanin->fMarkA = 0;
+    }
+    return Counter;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/tim/tim.c b/src/aig/tim/tim.c
index 51970425..9d5c8f7f 100644
--- a/src/aig/tim/tim.c
+++ b/src/aig/tim/tim.c
@@ -554,6 +554,8 @@ void Tim_ManCreateBoxFirst( Tim_Man_t * p, int firstIn, int nIns, int firstOut,
     pBox = (Tim_Box_t *)Mem_FlexEntryFetch( p->pMemObj, sizeof(Tim_Box_t) + sizeof(int) * (nIns+nOuts) );
     memset( pBox, 0, sizeof(Tim_Box_t) );
     pBox->iBox = Vec_PtrSize( p->vBoxes );
+//printf( "Creating box %d: First in = %d. (%d) First out = %d. (%d)\n", pBox->iBox, 
+//       firstIn, nIns, firstOut, nOuts );
     Vec_PtrPush( p->vBoxes, pBox );
     pBox->pDelayTable = pDelayTable;
     pBox->nInputs  = nIns;
@@ -704,6 +706,25 @@ void Tim_ManSetCoRequired( Tim_Man_t * p, int iCo, float Delay )
   SeeAlso     []
 
 ***********************************************************************/
+void Tim_ManSetCiArrivalAll( Tim_Man_t * p, float Delay )
+{
+    Tim_Obj_t * pObj;
+    int i;
+    Tim_ManForEachCi( p, pObj, i )
+        Tim_ManInitCiArrival( p, i, Delay );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets the correct required times for all POs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void Tim_ManSetCoRequiredAll( Tim_Man_t * p, float Delay )
 {
     Tim_Obj_t * pObj;
diff --git a/src/aig/tim/tim.h b/src/aig/tim/tim.h
index 3b9707e0..7c6e33f1 100644
--- a/src/aig/tim/tim.h
+++ b/src/aig/tim/tim.h
@@ -81,6 +81,7 @@ extern void            Tim_ManInitCoRequired( Tim_Man_t * p, int iCo, float Dela
 extern void            Tim_ManSetCoArrival( Tim_Man_t * p, int iCo, float Delay );
 extern void            Tim_ManSetCiRequired( Tim_Man_t * p, int iCi, float Delay );
 extern void            Tim_ManSetCoRequired( Tim_Man_t * p, int iCo, float Delay );
+extern void            Tim_ManSetCiArrivalAll( Tim_Man_t * p, float Delay );
 extern void            Tim_ManSetCoRequiredAll( Tim_Man_t * p, float Delay );
 extern float           Tim_ManGetCiArrival( Tim_Man_t * p, int iCi );
 extern float           Tim_ManGetCoRequired( Tim_Man_t * p, int iCo );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index d9defa1b..450a245f 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -9298,7 +9298,7 @@ int Abc_CommandIProve( Abc_Frame_t * pAbc, int argc, char ** argv )
     Prove_Params_t Params, * pParams = &Params;
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkTemp;
-    int c, clk, RetValue;
+    int c, clk, RetValue, iOut = -1;
 
     extern int Abc_NtkIvyProve( Abc_Ntk_t ** ppNtk, void * pPars );
 
@@ -9351,8 +9351,16 @@ int Abc_CommandIProve( Abc_Frame_t * pAbc, int argc, char ** argv )
     // verify that the pattern is correct
     if ( RetValue == 0 )
     {
+        Abc_Obj_t * pObj;
+        int i;
         int * pSimInfo = Abc_NtkVerifySimulatePattern( pNtk, pNtkTemp->pModel );
-        if ( pSimInfo[0] != 1 )
+        Abc_NtkForEachCo( pNtk, pObj, i )
+            if ( pSimInfo[i] == 1 )
+            {
+                iOut = i;
+                break;
+            }
+        if ( i == Abc_NtkCoNum(pNtk) )
             printf( "ERROR in Abc_NtkMiterProve(): Generated counter-example is invalid.\n" );
         free( pSimInfo );
     }
@@ -9360,7 +9368,7 @@ int Abc_CommandIProve( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( RetValue == -1 ) 
         printf( "UNDECIDED      " );
     else if ( RetValue == 0 )
-        printf( "SATISFIABLE    " );
+        printf( "SATISFIABLE (output = %d) ", iOut );
     else
         printf( "UNSATISFIABLE  " );
     //printf( "\n" );
@@ -15634,6 +15642,7 @@ int Abc_CommandAbc8Read( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fMapped;
     int fTest;
     extern void * Ioa_ReadBlif( char * pFileName, int fCheck );
+    extern void Ioa_WriteBlif( void * p, char * pFileName );
     extern Aig_Man_t * Ntl_ManExtract( void * p );
     extern void * Ntl_ManExtractNwk( void * p, Aig_Man_t * pAig, Tim_Man_t * pManTime );
 
@@ -15678,6 +15687,7 @@ int Abc_CommandAbc8Read( Abc_Frame_t * pAbc, int argc, char ** argv )
         if ( pTemp )
         {
         Ntl_ManPrintStats( pTemp );
+//        Ioa_WriteBlif( pTemp, "test_boxes.blif" );
         Ntl_ManFree( pTemp );
         }
         return 0;
@@ -17888,6 +17898,8 @@ int Abc_CommandAbc8Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
+    printf( "Currently *cec works only for two designs given on command line.\n" );
+/*
     // derive AIGs
     pAig1 = Ntl_ManCollapse( pAbc->pAbc8Ntl, 0 );
     pTemp = Ntl_ManInsertNtk( pAbc->pAbc8Ntl, pAbc->pAbc8Nwk );
@@ -17903,6 +17915,7 @@ int Abc_CommandAbc8Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
     Fra_FraigCecTop( pAig1, pAig2, nConfLimit, nPartSize, fSmart, fVerbose );
     Aig_ManStop( pAig1 );
     Aig_ManStop( pAig2 );
+*/
     return 0;
 
 usage:
diff --git a/src/base/main/mainMC.c b/src/base/main/mainMC.c
index 3f6b81a4..84c75b7b 100644
--- a/src/base/main/mainMC.c
+++ b/src/base/main/mainMC.c
@@ -45,29 +45,36 @@
 ***********************************************************************/
 int main( int argc, char * argv[] )
 {
+    int fEnableBmcOnly = 0;  // enable to make it BMC-only
+
+    int fEnableCounter = 1;  // should be 1 in the final version
+    int fEnableComment = 0;  // should be 0 in the final version
+
     Fra_Sec_t SecPar, * pSecPar = &SecPar;
     FILE * pFile;
     Aig_Man_t * pAig;
-    int RetValue;
+    int RetValue = -1;
+    int Depth    = -1;
     // BMC parameters
-    int nFrames  = 30;
-    int nSizeMax = 200000;
+    int nFrames  = 50;
+    int nSizeMax = 500000;
     int nBTLimit = 10000;
     int fRewrite = 0;
     int fNewAlgo = 1;
     int fVerbose = 0;
+    int clkTotal = clock();
 
     if ( argc != 2 )
     {
         printf( "  Expecting one command-line argument (an input file in AIGER format).\n" );
-        printf( "  usage: %s <file.aig>", argv[0] );
+        printf( "  usage: %s <file.aig>\n", argv[0] );
         return 0;
     }
     pFile = fopen( argv[1], "r" );
     if ( pFile == NULL )
     {
         printf( "  Cannot open input AIGER file \"%s\".\n", argv[1] );
-        printf( "  usage: %s <file.aig>", argv[0] );
+        printf( "  usage: %s <file.aig>\n", argv[0] );
         return 0;
     }
     fclose( pFile );
@@ -75,33 +82,47 @@ int main( int argc, char * argv[] )
     if ( pAig == NULL )
     {
         printf( "  Parsing the AIGER file \"%s\" has failed.\n", argv[1] );
-        printf( "  usage: %s <file.aig>", argv[0] );
+        printf( "  usage: %s <file.aig>\n", argv[0] );
         return 0;
     }
 
-    // perform BMC
     Aig_ManSetRegNum( pAig, pAig->nRegs );
-    RetValue = Saig_ManBmcSimple( pAig, nFrames, nSizeMax, nBTLimit, fRewrite, fVerbose, NULL );
-
-    // perform full-blown SEC
-    if ( RetValue != 0 )
+    if ( !fEnableBmcOnly )
     {
-        extern void Dar_LibStart();
-        extern void Dar_LibStop();
-        extern void Cnf_ClearMemory();
-
-        Fra_SecSetDefaultParams( pSecPar );
-        pSecPar->nFramesMax      =   2;  // the max number of frames used for induction
-
-        Dar_LibStart();
-        RetValue = Fra_FraigSec( pAig, pSecPar );
-        Dar_LibStop();
-        Cnf_ClearMemory();
+        // perform BMC
+        if ( pAig->nRegs != 0 )
+            RetValue = Saig_ManBmcSimple( pAig, nFrames, nSizeMax, nBTLimit, fRewrite, fVerbose, NULL );
+
+        // perform full-blown SEC
+        if ( RetValue != 0 )
+        {
+            extern void Dar_LibStart();
+            extern void Dar_LibStop();
+            extern void Cnf_ClearMemory();
+
+            Fra_SecSetDefaultParams( pSecPar );
+            pSecPar->TimeLimit       = 600;
+            pSecPar->nFramesMax      =   4;  // the max number of frames used for induction
+            pSecPar->fPhaseAbstract  =   0;  // disable phase-abstraction
+            pSecPar->fSilent         =   1;  // disable phase-abstraction
+
+            Dar_LibStart();
+            RetValue = Fra_FraigSec( pAig, pSecPar );
+            Dar_LibStop();
+            Cnf_ClearMemory();
+        }
     }
 
     // perform BMC again
-    if ( RetValue == -1 )
+    if ( RetValue == -1 && pAig->nRegs != 0 )
     {
+        int nFrames  = 200;
+        int nSizeMax = 500000;
+        int nBTLimit = 10000000;
+        int fRewrite = 0;
+        RetValue = Saig_ManBmcSimple( pAig, nFrames, nSizeMax, nBTLimit, fRewrite, fVerbose, &Depth );
+        if ( RetValue != 0 )
+            RetValue = -1;
     }
 
     // decide how to report the output
@@ -111,7 +132,20 @@ int main( int argc, char * argv[] )
     if ( RetValue == 0 ) 
     {
 //        fprintf(stdout, "s SATIFIABLE\n");
+        fprintf( pFile, "1" );
+        if ( fEnableCounter  )
+        {
+        printf( "\n" );
+        if ( pAig->pSeqModel )
         Fra_SmlWriteCounterExample( pFile, pAig, pAig->pSeqModel );
+        }
+
+        if ( fEnableComment )
+        {
+        printf( "  # File %10s.  ", argv[1] );
+        PRT( "Time", clock() - clkTotal );
+        }
+
         if ( pFile != stdout )
             fclose(pFile);
         Aig_ManStop( pAig );
@@ -120,7 +154,15 @@ int main( int argc, char * argv[] )
     else if ( RetValue == 1 ) 
     {
 //    fprintf(stdout, "s UNSATISFIABLE\n");
-        fprintf( pFile, "0\n" );
+        fprintf( pFile, "0" );
+
+        if ( fEnableComment )
+        {
+        printf( "  # File %10s.  ", argv[1] );
+        PRT( "Time", clock() - clkTotal );
+        }
+        printf( "\n" );
+
         if ( pFile != stdout )
             fclose(pFile);
         Aig_ManStop( pAig );
@@ -129,6 +171,15 @@ int main( int argc, char * argv[] )
     else // if ( RetValue == -1 ) 
     {
 //    fprintf(stdout, "s UNKNOWN\n");
+        fprintf( pFile, "2" );
+
+        if ( fEnableComment )
+        {
+        printf( "  # File %10s.  ", argv[1] );
+        PRT( "Time", clock() - clkTotal );
+        }
+        printf( "\n" );
+
         if ( pFile != stdout )
             fclose(pFile);
         Aig_ManStop( pAig );
diff --git a/src/bdd/parse/parseCore.c b/src/bdd/parse/parseCore.c
index 21a37070..eb89b3e3 100644
--- a/src/bdd/parse/parseCore.c
+++ b/src/bdd/parse/parseCore.c
@@ -58,7 +58,9 @@
 #define PARSE_SYM_XOR1    '<'   // logic EXOR   (the 1st symbol) 
 #define PARSE_SYM_XOR2    '+'   // logic EXOR   (the 2nd symbol)
 #define PARSE_SYM_XOR3    '>'   // logic EXOR   (the 3rd symbol)
-#define PARSE_SYM_OR      '+'   // logic OR
+#define PARSE_SYM_XOR     '^'   // logic XOR
+#define PARSE_SYM_OR1     '+'   // logic OR
+#define PARSE_SYM_OR2     '|'   // logic OR
 #define PARSE_SYM_EQU1    '<'   // equvalence   (the 1st symbol)
 #define PARSE_SYM_EQU2    '='   // equvalence   (the 2nd symbol)
 #define PARSE_SYM_EQU3    '>'   // equvalence   (the 3rd symbol)
@@ -220,7 +222,9 @@ DdNode * Parse_FormulaParser( FILE * pOutput, char * pFormulaInit, int nVars, in
 
         case PARSE_SYM_AND1:
         case PARSE_SYM_AND2:
-        case PARSE_SYM_OR:
+        case PARSE_SYM_OR1:
+        case PARSE_SYM_OR2:
+        case PARSE_SYM_XOR:
             if ( Flag != PARSE_FLAG_VAR )
             {
                 fprintf( pOutput, "Parse_FormulaParser(): There is no variable before AND, EXOR, or OR.\n" );
@@ -229,8 +233,10 @@ DdNode * Parse_FormulaParser( FILE * pOutput, char * pFormulaInit, int nVars, in
             }
             if ( *pTemp == PARSE_SYM_AND1 || *pTemp == PARSE_SYM_AND2 )
                 Parse_StackOpPush( pStackOp, PARSE_OPER_AND );
-            else //if ( Str[Pos] == PARSE_SYM_OR )
+            else if ( *pTemp == PARSE_SYM_OR1 || *pTemp == PARSE_SYM_OR2 )
                 Parse_StackOpPush( pStackOp, PARSE_OPER_OR );
+            else //if ( Str[Pos] == PARSE_SYM_XOR )
+                Parse_StackOpPush( pStackOp, PARSE_OPER_XOR );
             Flag = PARSE_FLAG_OPER; 
             break;
 
diff --git a/src/map/if/ifMap.c b/src/map/if/ifMap.c
index 7e529ef6..75370dff 100644
--- a/src/map/if/ifMap.c
+++ b/src/map/if/ifMap.c
@@ -296,6 +296,7 @@ int If_ManPerformMappingRound( If_Man_t * p, int nCutsUsed, int Mode, int fPrepr
             }
             else if ( If_ObjIsCi(pObj) )
             {
+//printf( "processing CI %d\n", pObj->Id );
                 arrTime = Tim_ManGetCiArrival( p->pManTim, pObj->IdPio );
                 If_ObjSetArrTime( pObj, arrTime );
             }
diff --git a/src/map/mio/mioFunc.c b/src/map/mio/mioFunc.c
index 21a078f9..1fca5764 100644
--- a/src/map/mio/mioFunc.c
+++ b/src/map/mio/mioFunc.c
@@ -25,7 +25,9 @@
 
 // these symbols (and no other) can appear in the formulas
 #define MIO_SYMB_AND    '*'
-#define MIO_SYMB_OR     '+'
+#define MIO_SYMB_OR1    '+'
+#define MIO_SYMB_OR2    '|'
+#define MIO_SYMB_XOR    '^'
 #define MIO_SYMB_NOT    '!'
 #define MIO_SYMB_AFTNOT '\''
 #define MIO_SYMB_OPEN   '('
@@ -239,8 +241,9 @@ int Mio_GateCollectNames( char * pFormula, char * pPinNames[] )
 
     // remove the non-name symbols
     for ( pTemp = Buffer; *pTemp; pTemp++ )
-        if ( *pTemp == MIO_SYMB_AND  || *pTemp == MIO_SYMB_OR || *pTemp == MIO_SYMB_NOT
-          || *pTemp == MIO_SYMB_OPEN || *pTemp == MIO_SYMB_CLOSE || *pTemp == MIO_SYMB_AFTNOT )
+        if ( *pTemp == MIO_SYMB_AND || *pTemp == MIO_SYMB_OR1 || *pTemp == MIO_SYMB_OR2 
+          || *pTemp == MIO_SYMB_XOR || *pTemp == MIO_SYMB_NOT || *pTemp == MIO_SYMB_OPEN 
+          || *pTemp == MIO_SYMB_CLOSE || *pTemp == MIO_SYMB_AFTNOT )
             *pTemp = ' ';
 
     // save the names
diff --git a/src/map/mio/mioRead.c b/src/map/mio/mioRead.c
index 13c2cdcd..dc665050 100644
--- a/src/map/mio/mioRead.c
+++ b/src/map/mio/mioRead.c
@@ -265,7 +265,7 @@ Mio_Gate_t * Mio_LibraryReadGate( char ** ppToken, bool fExtendedFormat )
 
     // then rest of the expression 
     pToken = strtok( NULL, ";" );
-    pGate->pForm = Extra_UtilStrsav( pToken );
+    pGate->pForm = chomp( pToken );
 
     // read the pin info
     // start the linked list of pins
@@ -392,21 +392,27 @@ Mio_Pin_t * Mio_LibraryReadPin( char ** ppToken, bool fExtendedFormat )
   SeeAlso     []
 
 ***********************************************************************/
-char *chomp( char *s )
+char * chomp( char *s )
 {
-    char *b = ALLOC(char, strlen(s)+1), *c = b;
-    while (*s && isspace(*s))
-        ++s;
-    while (*s && !isspace(*s))
-        *c++ = *s++;
-    *c = 0;
-    return b;
+    char *a, *b, *c;
+    // remove leading spaces
+    for ( b = s; *b; b++ )
+        if ( !isspace(*b) )
+            break;
+    // strsav the string
+    a = strcpy( ALLOC(char, strlen(b)+1), b );
+    // remove trailing spaces
+    for ( c = a+strlen(a); c > a; c-- )
+        if ( *c == 0 || isspace(*c) )
+            *c = 0;
+        else
+            break;
+    return a;
 }   
         
 /**Function*************************************************************
 
-  Synopsis    [Duplicates string and returns it with leading and 
-               trailing spaces removed.]
+  Synopsis    []
 
   Description []