Version abc81025

19 files changed, 1330 insertions, 1486 deletions

diff --git a/src/aig/fra/fraCec.c b/src/aig/fra/fraCec.c
index fdf87ccd..190281c9 100644
--- a/src/aig/fra/fraCec.c
+++ b/src/aig/fra/fraCec.c
@@ -175,7 +175,11 @@ int Fra_FraigCec( Aig_Man_t ** ppAig, int nConfLimit, int fVerbose )
     RetValue = Fra_FraigMiterStatus( pAig );
 //    assert( RetValue == -1 );
     if ( RetValue >= 0 )
+    {
+        pAig->pData = ALLOC( int, Aig_ManPiNum(pAig) );
+        memset( pAig->pData, 0, sizeof(int) * Aig_ManPiNum(pAig) );
         return RetValue;
+    }
 
     // if SAT only, solve without iteration
 clk = clock();
diff --git a/src/aig/ntl/ntl.h b/src/aig/ntl/ntl.h
index 5f1f724f..a82157c0 100644
--- a/src/aig/ntl/ntl.h
+++ b/src/aig/ntl/ntl.h
@@ -139,6 +139,7 @@ struct Ntl_Obj_t_
     union {                            // clock / other data
         Ntl_Net_t *    pClock;         // clock (for registers)
         void *         pTemp;          // other data 
+        int            iTemp;          // other data
     };
     Ntl_Net_t *        pFanio[0];      // fanins/fanouts
 };
@@ -149,8 +150,8 @@ struct Ntl_Net_t_
     void *             pCopy;          // the copy of this object
     union {
         void *         pCopy2;         // the copy of this object
-        int            iTemp;          // other data
         float          dTemp;          // other data
+        int            iTemp;          // other data
     };
     Ntl_Obj_t *        pDriver;        // driver of the net
     char               nVisits;        // the number of times the net is visited
@@ -352,6 +353,7 @@ 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 void            Ntl_ModelSetPioNumbers( Ntl_Mod_t * p );
 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 );
diff --git a/src/aig/ntl/ntlEc.c b/src/aig/ntl/ntlEc.c
index 4850f647..0d41006e 100644
--- a/src/aig/ntl/ntlEc.c
+++ b/src/aig/ntl/ntlEc.c
@@ -351,6 +351,7 @@ Aig_Man_t * Ntl_ManPrepareSec( char * pFileName1, char * pFileName2 )
     pAig1 = Ntl_ManCollapse( pMan1, 1 );
     pAig2 = Ntl_ManCollapse( pMan2, 1 );
     pAig = Saig_ManCreateMiter( pAig1, pAig2, 0 );
+    Aig_ManCleanup( pAig );
     Aig_ManStop( pAig1 );
     Aig_ManStop( pAig2 );
     // cleanup
diff --git a/src/aig/ntl/ntlReadBlif.c b/src/aig/ntl/ntlReadBlif.c
index 30f972c8..800b711c 100644
--- a/src/aig/ntl/ntlReadBlif.c
+++ b/src/aig/ntl/ntlReadBlif.c
@@ -745,6 +745,7 @@ static int Ioa_ReadReadInterfaces( Ioa_ReadMan_t * p )
             if ( !Ioa_ReadParseLineOutputs( pMod, pLine ) )
                 return 0;
         // parse the delay info
+        Ntl_ModelSetPioNumbers( pMod->pNtk );
         Vec_PtrForEachEntry( pMod->vDelays, pLine, k )
             if ( !Ioa_ReadParseLineDelay( pMod, pLine ) )
                 return 0;
@@ -954,6 +955,7 @@ static int Ioa_ReadParseLineOutputs( Ioa_ReadMod_t * p, char * pLine )
     {
         pNet = Ntl_ModelFindOrCreateNet( p->pNtk, pToken );
         pObj = Ntl_ModelCreatePo( p->pNtk, pNet );
+        pNet->pCopy = pObj;
     }
     return 1;
 }
diff --git a/src/aig/ntl/ntlReadBlif_old.c b/src/aig/ntl/ntlReadBlif_old.c
deleted file mode 100644
index ebfb2a80..00000000
--- a/src/aig/ntl/ntlReadBlif_old.c
+++ /dev/null
@@ -1,1261 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [ntlReadBlif.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Command processing package.]
-
-  Synopsis    [Procedures to read BLIF file.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - January 8, 2007.]
-
-  Revision    [$Id: ntlReadBlif.c,v 1.00 2007/01/08 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "ntl.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-typedef struct Ioa_ReadMod_t_ Ioa_ReadMod_t;   // parsing model
-typedef struct Ioa_ReadMan_t_ Ioa_ReadMan_t;   // parsing manager
-
-struct Ioa_ReadMod_t_
-{
-    // file lines
-    char *               pFirst;       // .model line
-    char *               pAttrib;      // .attrib line
-    Vec_Ptr_t *          vInputs;      // .inputs lines
-    Vec_Ptr_t *          vOutputs;     // .outputs lines
-    Vec_Ptr_t *          vLatches;     // .latch lines
-    Vec_Ptr_t *          vNames;       // .names lines
-    Vec_Ptr_t *          vSubckts;     // .subckt lines
-    Vec_Ptr_t *          vDelays;      // .delay 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;   
-    // the parent manager
-    Ioa_ReadMan_t *      pMan;         
-};
-
-struct Ioa_ReadMan_t_
-{
-    // general info about file
-    char *               pFileName;    // the name of the file
-    char *               pBuffer;      // the contents of the file
-    Vec_Ptr_t *          vLines;       // the line beginnings
-    // the results of reading
-    Ntl_Man_t *          pDesign;      // the design under construction
-    // intermediate storage for models
-    Vec_Ptr_t *          vModels;      // vector of models
-    Ioa_ReadMod_t *      pLatest;      // the current model
-    // current processing info
-    Vec_Ptr_t *          vTokens;      // the current tokens
-    Vec_Ptr_t *          vTokens2;     // the current tokens
-    Vec_Str_t *          vFunc;        // the local function
-    // error reporting
-    char                 sError[512];  // the error string generated during parsing
-    // statistics 
-    int                  nTablesRead;  // the number of processed tables
-    int                  nTablesLeft;  // the number of dangling tables
-};
-
-// static functions
-static Ioa_ReadMan_t *   Ioa_ReadAlloc();
-static void              Ioa_ReadFree( Ioa_ReadMan_t * p );
-static Ioa_ReadMod_t *   Ioa_ReadModAlloc();
-static void              Ioa_ReadModFree( Ioa_ReadMod_t * p );
-static char *            Ioa_ReadLoadFile( char * pFileName );
-static void              Ioa_ReadReadPreparse( Ioa_ReadMan_t * p );
-static int               Ioa_ReadReadInterfaces( Ioa_ReadMan_t * p );
-static Ntl_Man_t *       Ioa_ReadParse( Ioa_ReadMan_t * p );
-static int               Ioa_ReadParseLineModel( Ioa_ReadMod_t * p, char * pLine );
-static int               Ioa_ReadParseLineAttrib( Ioa_ReadMod_t * p, char * pLine );
-static int               Ioa_ReadParseLineInputs( Ioa_ReadMod_t * p, char * pLine );
-static int               Ioa_ReadParseLineOutputs( Ioa_ReadMod_t * p, char * pLine );
-static int               Ioa_ReadParseLineLatch( Ioa_ReadMod_t * p, char * pLine );
-static int               Ioa_ReadParseLineSubckt( Ioa_ReadMod_t * p, char * pLine );
-static int               Ioa_ReadParseLineDelay( Ioa_ReadMod_t * p, char * pLine );
-static int               Ioa_ReadParseLineTimes( Ioa_ReadMod_t * p, char * pLine, int fOutput );
-static int               Ioa_ReadParseLineNamesBlif( Ioa_ReadMod_t * p, char * pLine );
-
-static int               Ioa_ReadCharIsSpace( char s )   { return s == ' ' || s == '\t' || s == '\r' || s == '\n';             }
-static int               Ioa_ReadCharIsSopSymb( char s ) { return s == '0' || s == '1' || s == '-' || s == '\r' || s == '\n';  }
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Reads the network from the BLIF file.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Ntl_Man_t * Ioa_ReadBlif( char * pFileName, int fCheck )
-{
-    FILE * pFile;
-    Ioa_ReadMan_t * p;
-    Ntl_Man_t * pDesign;
-//    int nNodes;
-
-    // check that the file is available
-    pFile = fopen( pFileName, "rb" );
-    if ( pFile == NULL )
-    {
-        printf( "Ioa_ReadBlif(): The file is unavailable (absent or open).\n" );
-        return 0;
-    }
-    fclose( pFile );
-
-    // start the file reader
-    p = Ioa_ReadAlloc();
-    p->pFileName = pFileName;
-    p->pBuffer   = Ioa_ReadLoadFile( pFileName );
-    if ( p->pBuffer == NULL )
-    {
-        Ioa_ReadFree( p );
-        return NULL;
-    }
-    // set the design name
-    p->pDesign = Ntl_ManAlloc( pFileName );
-    p->pDesign->pName = Ntl_ManStoreFileName( p->pDesign, pFileName );
-    p->pDesign->pSpec = Ntl_ManStoreName( p->pDesign, pFileName );
-    // prepare the file for parsing
-    Ioa_ReadReadPreparse( p );
-    // parse interfaces of each network
-    if ( !Ioa_ReadReadInterfaces( p ) )
-    {
-        if ( p->sError[0] )
-            fprintf( stdout, "%s\n", p->sError );
-        Ioa_ReadFree( p );
-        return NULL;
-    }
-    // construct the network
-    pDesign = Ioa_ReadParse( p );
-    if ( p->sError[0] )
-        fprintf( stdout, "%s\n", p->sError );
-    if ( pDesign == NULL )
-    {
-        Ioa_ReadFree( p );
-        return NULL;
-    }
-    p->pDesign = NULL;
-    Ioa_ReadFree( p );
-// pDesign should be linked to all models of the design
-
-    // make sure that everything is okay with the network structure
-    if ( fCheck )
-    {
-        if ( !Ntl_ManCheck( pDesign ) )
-        {
-            printf( "Ioa_ReadBlif: The check has failed for design %s.\n", pDesign->pName );
-            Ntl_ManFree( pDesign );
-            return NULL;
-        }
-
-    }
-    // transform the design by removing the CO drivers
-//    if ( (nNodes = Ntl_ManReconnectCoDrivers(pDesign)) )
-//        printf( "The design was transformed by removing %d buf/inv CO drivers.\n", nNodes );
-//Ioa_WriteBlif( pDesign, "_temp_.blif" );
-    return pDesign;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Allocates the BLIF parsing structure.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static Ioa_ReadMan_t * Ioa_ReadAlloc()
-{
-    Ioa_ReadMan_t * p;
-    p = ALLOC( Ioa_ReadMan_t, 1 );
-    memset( p, 0, sizeof(Ioa_ReadMan_t) );
-    p->vLines   = Vec_PtrAlloc( 512 );
-    p->vModels  = Vec_PtrAlloc( 512 );
-    p->vTokens  = Vec_PtrAlloc( 512 );
-    p->vTokens2 = Vec_PtrAlloc( 512 );
-    p->vFunc    = Vec_StrAlloc( 512 );
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Frees the BLIF parsing structure.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static void Ioa_ReadFree( Ioa_ReadMan_t * p )
-{
-    Ioa_ReadMod_t * pMod;
-    int i;
-    if ( p->pDesign )
-        Ntl_ManFree( p->pDesign );
-    if ( p->pBuffer )  
-        free( p->pBuffer );
-    if ( p->vLines )
-        Vec_PtrFree( p->vLines );
-    if ( p->vModels )
-    {
-        Vec_PtrForEachEntry( p->vModels, pMod, i )
-            Ioa_ReadModFree( pMod );
-        Vec_PtrFree( p->vModels );
-    }
-    Vec_PtrFree( p->vTokens );
-    Vec_PtrFree( p->vTokens2 );
-    Vec_StrFree( p->vFunc );
-    free( p );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Allocates the BLIF parsing structure for one model.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-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( 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;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Deallocates the BLIF parsing structure for one model.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static void Ioa_ReadModFree( Ioa_ReadMod_t * p )
-{
-    Vec_PtrFree( p->vInputs );
-    Vec_PtrFree( p->vOutputs );
-    Vec_PtrFree( p->vLatches );
-    Vec_PtrFree( p->vNames );
-    Vec_PtrFree( p->vSubckts );
-    Vec_PtrFree( p->vDelays );
-    Vec_PtrFree( p->vTimeInputs );
-    Vec_PtrFree( p->vTimeOutputs );
-    free( p );
-}
-
-
-
-/**Function*************************************************************
-
-  Synopsis    [Counts the number of given chars.]
-
-  Description []
-  
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static int Ioa_ReadCountChars( char * pLine, char Char )
-{
-    char * pCur;
-    int Counter = 0;
-    for ( pCur = pLine; *pCur; pCur++ )
-        if ( *pCur == Char )
-            Counter++;
-    return Counter;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Collects the already split tokens.]
-
-  Description []
-  
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static void Ioa_ReadCollectTokens( Vec_Ptr_t * vTokens, char * pInput, char * pOutput )
-{
-    char * pCur;
-    Vec_PtrClear( vTokens );
-    for ( pCur = pInput; pCur < pOutput; pCur++ )
-    {
-        if ( *pCur == 0 )
-            continue;
-        Vec_PtrPush( vTokens, pCur );
-        while ( *++pCur );
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Splits the line into tokens.]
-
-  Description []
-  
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static void Ioa_ReadSplitIntoTokens( Vec_Ptr_t * vTokens, char * pLine, char Stop )
-{
-    char * pCur;
-    // clear spaces
-    for ( pCur = pLine; *pCur != Stop; pCur++ )
-        if ( Ioa_ReadCharIsSpace(*pCur) )
-            *pCur = 0;
-    // collect tokens
-    Ioa_ReadCollectTokens( vTokens, pLine, pCur );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Splits the line into tokens.]
-
-  Description []
-  
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static void Ioa_ReadSplitIntoTokensAndClear( Vec_Ptr_t * vTokens, char * pLine, char Stop, char Char )
-{
-    char * pCur;
-    // clear spaces
-    for ( pCur = pLine; *pCur != Stop; pCur++ )
-        if ( Ioa_ReadCharIsSpace(*pCur) || *pCur == Char )
-            *pCur = 0;
-    // collect tokens
-    Ioa_ReadCollectTokens( vTokens, pLine, pCur );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns the 1-based number of the line in which the token occurs.]
-
-  Description []
-  
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static int Ioa_ReadGetLine( Ioa_ReadMan_t * p, char * pToken )
-{
-    char * pLine;
-    int i;
-    Vec_PtrForEachEntry( p->vLines, pLine, i )
-        if ( pToken < pLine )
-            return i;
-    return -1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Reads the file into a character buffer.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static char * Ioa_ReadLoadFile( char * pFileName )
-{
-    FILE * pFile;
-    int nFileSize;
-    char * pContents;
-    pFile = fopen( pFileName, "rb" );
-    if ( pFile == NULL )
-    {
-        printf( "Ioa_ReadLoadFile(): The file is unavailable (absent or open).\n" );
-        return NULL;
-    }
-    fseek( pFile, 0, SEEK_END );  
-    nFileSize = ftell( pFile ); 
-    if ( nFileSize == 0 )
-    {
-        printf( "Ioa_ReadLoadFile(): The file is empty.\n" );
-        return NULL;
-    }
-    pContents = ALLOC( char, nFileSize + 10 );
-    rewind( pFile );
-    fread( pContents, nFileSize, 1, pFile );
-    fclose( pFile );
-    // finish off the file with the spare .end line
-    // some benchmarks suddenly break off without this line
-    strcpy( pContents + nFileSize, "\n.end\n" );
-    return pContents;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Prepares the parsing.]
-
-  Description [Performs several preliminary operations:
-  - Cuts the file buffer into separate lines.
-  - Removes comments and line extenders.
-  - Sorts lines by directives.
-  - Estimates the number of objects.
-  - Allocates room for the objects.
-  - Allocates room for the hash table.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static void Ioa_ReadReadPreparse( Ioa_ReadMan_t * p )
-{
-    char * pCur, * pPrev;
-    int i, fComment = 0;
-    // parse the buffer into lines and remove comments
-    Vec_PtrPush( p->vLines, p->pBuffer );
-    for ( pCur = p->pBuffer; *pCur; pCur++ )
-    {
-        if ( *pCur == '\n' )
-        {
-            *pCur = 0;
-//            if ( *(pCur-1) == '\r' )
-//                *(pCur-1) = 0;
-            fComment = 0;
-            Vec_PtrPush( p->vLines, pCur + 1 );
-        }
-        else if ( *pCur == '#' )
-            fComment = 1;
-        // remove comments
-        if ( fComment )
-            *pCur = 0;
-    }
-
-    // unfold the line extensions and sort lines by directive
-    Vec_PtrForEachEntry( p->vLines, pCur, i )
-    {
-        if ( *pCur == 0 )
-            continue;
-        // find previous non-space character
-        for ( pPrev = pCur - 2; pPrev >= p->pBuffer; pPrev-- )
-            if ( !Ioa_ReadCharIsSpace(*pPrev) )
-                break;
-        // if it is the line extender, overwrite it with spaces
-        if ( *pPrev == '\\' )
-        {
-            for ( ; *pPrev; pPrev++ )
-                *pPrev = ' ';
-            *pPrev = ' ';
-            continue;
-        }
-        // skip spaces at the beginning of the line
-        while ( Ioa_ReadCharIsSpace(*pCur++) );
-        // parse directives
-        if ( *(pCur-1) != '.' )
-            continue;
-        if ( !strncmp(pCur, "names", 5) )
-            Vec_PtrPush( p->pLatest->vNames, pCur );
-        else if ( !strncmp(pCur, "latch", 5) )
-            Vec_PtrPush( p->pLatest->vLatches, pCur );
-        else if ( !strncmp(pCur, "inputs", 6) )
-            Vec_PtrPush( p->pLatest->vInputs, pCur );
-        else if ( !strncmp(pCur, "outputs", 7) )
-            Vec_PtrPush( p->pLatest->vOutputs, pCur );
-        else if ( !strncmp(pCur, "subckt", 6) )
-            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) ||
-                  !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) ) 
-        {
-            p->pLatest = Ioa_ReadModAlloc();
-            p->pLatest->pFirst = pCur;
-            p->pLatest->pMan = p;
-        }
-        else if ( !strncmp(pCur, "attrib", 6) ) 
-        {
-            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 )
-                Vec_PtrPush( p->vModels, p->pLatest );
-            p->pLatest = NULL;
-        }
-        else if ( !strncmp(pCur, "exdc", 4) )
-        {
-            fprintf( stdout, "Line %d: Skipping EXDC network.\n", Ioa_ReadGetLine(p, pCur) );
-            break;
-        }
-        else if ( !strncmp(pCur, "no_merge", 8) ) 
-        {
-        }
-        else
-        {
-            pCur--;
-            if ( pCur[strlen(pCur)-1] == '\r' )
-                pCur[strlen(pCur)-1] = 0;
-            fprintf( stdout, "Line %d: Skipping line \"%s\".\n", Ioa_ReadGetLine(p, pCur), pCur );
-        }
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Parses interfaces of the models.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static int Ioa_ReadReadInterfaces( Ioa_ReadMan_t * p )
-{
-    Ioa_ReadMod_t * pMod;
-    char * pLine;
-    int i, k;
-    // iterate through the models
-    Vec_PtrForEachEntry( p->vModels, pMod, i )
-    {
-        // parse the model
-        if ( !Ioa_ReadParseLineModel( pMod, pMod->pFirst ) )
-            return 0;
-        // parse the model attributes
-        if ( pMod->pAttrib && !Ioa_ReadParseLineAttrib( pMod, pMod->pAttrib ) )
-            return 0;
-        // parse the inputs
-        Vec_PtrForEachEntry( pMod->vInputs, pLine, k )
-            if ( !Ioa_ReadParseLineInputs( pMod, pLine ) )
-                return 0;
-        // parse the outputs
-        Vec_PtrForEachEntry( pMod->vOutputs, pLine, k )
-            if ( !Ioa_ReadParseLineOutputs( pMod, pLine ) )
-                return 0;
-        // parse the delay info
-        Vec_PtrForEachEntry( pMod->vDelays, pLine, k )
-            if ( !Ioa_ReadParseLineDelay( pMod, pLine ) )
-                return 0;
-        Vec_PtrForEachEntry( pMod->vTimeInputs, pLine, k )
-            if ( !Ioa_ReadParseLineTimes( pMod, pLine, 0 ) )
-                return 0;
-        Vec_PtrForEachEntry( pMod->vTimeOutputs, pLine, k )
-            if ( !Ioa_ReadParseLineTimes( pMod, pLine, 1 ) )
-                return 0;
-    }
-    return 1;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-  
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static Ntl_Man_t * Ioa_ReadParse( Ioa_ReadMan_t * p )
-{
-    Ntl_Man_t * pDesign;
-    Ioa_ReadMod_t * pMod;
-    char * pLine;
-    int i, k;
-    // iterate through the models
-    Vec_PtrForEachEntry( p->vModels, pMod, i )
-    {
-        // parse the latches
-        Vec_PtrForEachEntry( pMod->vLatches, pLine, k )
-            if ( !Ioa_ReadParseLineLatch( pMod, pLine ) )
-                return NULL;
-        // parse the nodes
-        Vec_PtrForEachEntry( pMod->vNames, pLine, k )
-            if ( !Ioa_ReadParseLineNamesBlif( pMod, pLine ) )
-                return NULL;
-        // parse the subcircuits
-        Vec_PtrForEachEntry( pMod->vSubckts, pLine, k )
-            if ( !Ioa_ReadParseLineSubckt( pMod, pLine ) )
-                return NULL;
-        // finalize the network
-        Ntl_ModelFixNonDrivenNets( pMod->pNtk );
-    }
-    if ( i == 0 )
-        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;
-    p->pDesign = NULL;
-    return pDesign;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Parses the model line.]
-
-  Description []
-  
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static int Ioa_ReadParseLineModel( Ioa_ReadMod_t * p, char * pLine )
-{
-    Vec_Ptr_t * vTokens = p->pMan->vTokens;
-    char * pToken;
-    Ioa_ReadSplitIntoTokens( vTokens, pLine, '\0' );
-    pToken = Vec_PtrEntry( vTokens, 0 );
-    assert( !strcmp(pToken, "model") );
-    if ( Vec_PtrSize(vTokens) != 2 )
-    {
-        sprintf( p->pMan->sError, "Line %d: The number of entries (%d) in .model line is different from two.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrSize(vTokens) );
-        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;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Parses the model line.]
-
-  Description []
-  
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-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) );
-    Vec_PtrForEachEntryStart( vTokens, pToken, i, 1 )
-    {
-        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;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Parses the inputs line.]
-
-  Description []
-  
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static int Ioa_ReadParseLineInputs( Ioa_ReadMod_t * p, char * pLine )
-{
-    Ntl_Net_t * pNet;
-    Ntl_Obj_t * pObj;
-    Vec_Ptr_t * vTokens = p->pMan->vTokens;
-    char * pToken;
-    int i;
-    Ioa_ReadSplitIntoTokens( vTokens, pLine, '\0' );
-    pToken = Vec_PtrEntry(vTokens, 0);
-    assert( !strcmp(pToken, "inputs") );
-    Vec_PtrForEachEntryStart( vTokens, pToken, i, 1 )
-    {
-        pObj = Ntl_ModelCreatePi( p->pNtk );
-        pNet = Ntl_ModelFindOrCreateNet( p->pNtk, pToken );
-        if ( !Ntl_ModelSetNetDriver( pObj, pNet ) )
-        {
-            sprintf( p->pMan->sError, "Line %d: Net %s already has a driver.", Ioa_ReadGetLine(p->pMan, pToken), pNet->pName );
-            return 0;
-        }
-    }
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Parses the outputs line.]
-
-  Description []
-  
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static int Ioa_ReadParseLineOutputs( Ioa_ReadMod_t * p, char * pLine )
-{
-    Ntl_Net_t * pNet;
-    Ntl_Obj_t * pObj;
-    Vec_Ptr_t * vTokens = p->pMan->vTokens;
-    char * pToken;
-    int i;
-    Ioa_ReadSplitIntoTokens( vTokens, pLine, '\0' );
-    pToken = Vec_PtrEntry(vTokens, 0);
-    assert( !strcmp(pToken, "outputs") );
-    Vec_PtrForEachEntryStart( vTokens, pToken, i, 1 )
-    {
-        pNet = Ntl_ModelFindOrCreateNet( p->pNtk, pToken );
-        pObj = Ntl_ModelCreatePo( p->pNtk, pNet );
-    }
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Parses the latches line.]
-
-  Description []
-  
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static int Ioa_ReadParseLineLatch( Ioa_ReadMod_t * p, char * pLine )
-{
-    Vec_Ptr_t * vTokens = p->pMan->vTokens;
-    Ntl_Net_t * pNetLi, * pNetLo;
-    Ntl_Obj_t * pObj;
-    char * pToken, * pNameLi, * pNameLo;
-    Ioa_ReadSplitIntoTokens( vTokens, pLine, '\0' );
-    pToken = Vec_PtrEntry(vTokens,0);
-    assert( !strcmp(pToken, "latch") );
-    if ( Vec_PtrSize(vTokens) < 3 )
-    {
-        sprintf( p->pMan->sError, "Line %d: Latch does not have input name and output name.", Ioa_ReadGetLine(p->pMan, pToken) );
-        return 0;
-    }
-    // create latch
-    pNameLi = Vec_PtrEntry( vTokens, 1 );
-    pNameLo = Vec_PtrEntry( vTokens, 2 );
-    pNetLi  = Ntl_ModelFindOrCreateNet( p->pNtk, pNameLi );
-    pNetLo  = Ntl_ModelFindOrCreateNet( p->pNtk, pNameLo );
-    pObj    = Ntl_ModelCreateLatch( p->pNtk );
-    pObj->pFanio[0] = pNetLi;
-    if ( !Ntl_ModelSetNetDriver( pObj, pNetLo ) )
-    {
-        sprintf( p->pMan->sError, "Line %d: Net %s already has a driver.", Ioa_ReadGetLine(p->pMan, pToken), pNetLo->pName );
-        return 0;
-    }
-    // get initial value
-    if ( Vec_PtrSize(vTokens) > 3 )
-        pObj->LatchId.regInit = atoi( Vec_PtrEntry(vTokens,Vec_PtrSize(vTokens)-1) );
-    else
-        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 )
-    {
-        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;
-    }
-    // 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->pClock = pNetLi;
-    }
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Parses the subckt line.]
-
-  Description []
-  
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static int Ioa_ReadParseLineSubckt( Ioa_ReadMod_t * p, char * pLine )
-{
-    Vec_Ptr_t * vTokens = p->pMan->vTokens;
-    Ntl_Mod_t * pModel;
-    Ntl_Obj_t * pBox, * pTerm;
-    Ntl_Net_t * pNet;
-    char * pToken, * pName, ** ppNames;
-    int nEquals, i, k;
-
-    // split the line into tokens
-    nEquals = Ioa_ReadCountChars( pLine, '=' );
-    Ioa_ReadSplitIntoTokensAndClear( vTokens, pLine, '\0', '=' );
-    pToken = Vec_PtrEntry(vTokens,0);
-    assert( !strcmp(pToken, "subckt") );
-
-    // get the model for this box
-    pName = Vec_PtrEntry(vTokens,1);
-    pModel = Ntl_ManFindModel( p->pMan->pDesign, pName );
-    if ( pModel == NULL )
-    {
-        sprintf( p->pMan->sError, "Line %d: Cannot find the model for subcircuit %s.", Ioa_ReadGetLine(p->pMan, pToken), pName );
-        return 0;
-    }
-/*
-    // temporary fix for splitting the .subckt line
-    if ( nEquals < Ntl_ModelPiNum(pModel) + Ntl_ModelPoNum(pModel) )
-    { 
-        Vec_Ptr_t * vTokens2 = Vec_PtrAlloc( 10 );
-        // get one additional token
-        pToken = Vec_PtrEntry( vTokens, Vec_PtrSize(vTokens) - 1 );
-        for ( ; *pToken; pToken++ );
-        for ( ; *pToken == 0; pToken++ );
-        Ioa_ReadSplitIntoTokensAndClear( vTokens2, pToken, '\0', '=' );
-//        assert( Vec_PtrSize( vTokens2 ) == 2 );
-        Vec_PtrForEachEntry( vTokens2, pToken, i )
-            Vec_PtrPush( vTokens, pToken );
-        nEquals += Vec_PtrSize(vTokens2)/2;
-        Vec_PtrFree( vTokens2 );
-    }
-*/    
-    // check if the number of tokens is correct
-    if ( nEquals != Ntl_ModelPiNum(pModel) + Ntl_ModelPoNum(pModel) )
-    {
-        sprintf( p->pMan->sError, "Line %d: The number of ports (%d) in .subckt %s differs from the sum of PIs and POs of the model (%d).", 
-            Ioa_ReadGetLine(p->pMan, pToken), nEquals, pName, Ntl_ModelPiNum(pModel) + Ntl_ModelPoNum(pModel) );
-        return 0;
-    }
-
-    // get the names
-    ppNames = (char **)Vec_PtrArray(vTokens) + 2;
-
-    // create the box with these terminals
-    pBox = Ntl_ModelCreateBox( p->pNtk, Ntl_ModelPiNum(pModel), Ntl_ModelPoNum(pModel) );
-    pBox->pImplem = pModel;
-    Ntl_ModelForEachPi( pModel, pTerm, i )
-    {
-        // find this terminal among the formal inputs of the subcircuit
-        pName = Ntl_ObjFanout0(pTerm)->pName;
-        for ( k = 0; k < nEquals; k++ )
-            if ( !strcmp( ppNames[2*k], pName ) )
-                break;
-        if ( k == nEquals )
-        {
-            sprintf( p->pMan->sError, "Line %d: Cannot find PI \"%s\" of the model \"%s\" as a formal input of the subcircuit.", 
-                Ioa_ReadGetLine(p->pMan, pToken), pName, pModel->pName );
-            return 0;
-        }
-        // create the BI with the actual name
-        pNet = Ntl_ModelFindOrCreateNet( p->pNtk, ppNames[2*k+1] );
-        Ntl_ObjSetFanin( pBox, pNet, i );
-    }
-    Ntl_ModelForEachPo( pModel, pTerm, i )
-    {
-        // find this terminal among the formal outputs of the subcircuit
-        pName = Ntl_ObjFanin0(pTerm)->pName;
-        for ( k = 0; k < nEquals; k++ )
-            if ( !strcmp( ppNames[2*k], pName ) )
-                break;
-        if ( k == nEquals )
-        {
-            sprintf( p->pMan->sError, "Line %d: Cannot find PO \"%s\" of the model \"%s\" as a formal output of the subcircuit.", 
-                Ioa_ReadGetLine(p->pMan, pToken), pName, pModel->pName );
-            return 0;
-        }
-        // create the BI with the actual name
-        pNet = Ntl_ModelFindOrCreateNet( p->pNtk, ppNames[2*k+1] );
-        Ntl_ObjSetFanout( pBox, pNet, i );
-    }
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Parses the subckt line.]
-
-  Description []
-  
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static int Ioa_ReadParseLineDelay( Ioa_ReadMod_t * p, char * pLine )
-{
-    Vec_Ptr_t * vTokens = p->pMan->vTokens;
-    int RetValue1, RetValue2, Number1, Number2, Temp;
-    char * pToken, * pTokenNum;
-    float Delay;
-    assert( sizeof(float) == sizeof(int) );
-    Ioa_ReadSplitIntoTokens( vTokens, pLine, '\0' );
-    pToken = Vec_PtrEntry(vTokens,0);
-    assert( !strcmp(pToken, "delay") );
-    if ( Vec_PtrSize(vTokens) < 2 && Vec_PtrSize(vTokens) > 4 )
-    {
-        sprintf( p->pMan->sError, "Line %d: Delay line does not have a valid number of parameters (1, 2, or 3).", Ioa_ReadGetLine(p->pMan, pToken) );
-        return 0;
-    }
-    // find the delay number
-    pTokenNum = Vec_PtrEntryLast(vTokens);
-    Delay = atof( pTokenNum );
-    if ( Delay == 0.0 && pTokenNum[0] != '0' )
-    {
-        sprintf( p->pMan->sError, "Line %d: Delay value (%s) appears to be invalid.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntryLast(vTokens) );
-        return 0;
-    }
-    // find the PI/PO numbers
-    RetValue1 = 0; Number1 = -1;
-    if ( Vec_PtrSize(vTokens) > 2 )
-    {
-        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) );
-            return 0;
-        }
-    }
-    RetValue2 = 0; Number2 = -1;
-    if ( Vec_PtrSize(vTokens) > 3 )
-    {
-        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) );
-            return 0;
-        }
-    }
-    if ( RetValue1 == RetValue2 && RetValue1 )
-    {
-        sprintf( p->pMan->sError, "Line %d: Both signals \"%s\" and \"%s\" listed appear to be PIs or POs.", 
-            Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens, 1), Vec_PtrEntry(vTokens, 2) );
-        return 0;
-    }
-    if ( RetValue2 < RetValue1 )
-    {
-        Temp = RetValue2; RetValue2 = RetValue1; RetValue1 = Temp;
-        Temp = Number2;   Number2 = Number1;     Number1 = Temp;
-    }
-    assert( RetValue1 == 0 || RetValue1 == -1 );
-    assert( RetValue2 == 0 || RetValue2 ==  1 );
-    // store the values
-    if ( p->pNtk->vDelays == NULL )
-        p->pNtk->vDelays = Vec_IntAlloc( 100 );
-    Vec_IntPush( p->pNtk->vDelays, Number1 );
-    Vec_IntPush( p->pNtk->vDelays, Number2 );
-    Vec_IntPush( p->pNtk->vDelays, Aig_Float2Int(Delay) );        
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Parses the subckt line.]
-
-  Description []
-  
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static int Ioa_ReadParseLineTimes( Ioa_ReadMod_t * p, char * pLine, int fOutput )
-{
-    Vec_Ptr_t * vTokens = p->pMan->vTokens;
-    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( !strncmp(pToken, "output_", 7) );
-    else
-        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 (2 or 3).", Ioa_ReadGetLine(p->pMan, pToken) );
-        return 0;
-    }
-    // find the delay number
-    pTokenNum = Vec_PtrEntryLast(vTokens);
-    if ( !strcmp( pTokenNum, "-inf" ) )
-        Delay = -TIM_ETERNITY;
-    else if ( !strcmp( pTokenNum, "inf" ) ) 
-        Delay = TIM_ETERNITY;
-    else
-        Delay = atof( pTokenNum );
-    if ( Delay == 0.0 && pTokenNum[0] != '0' )
-    {
-        sprintf( p->pMan->sError, "Line %d: Delay value (%s) appears to be invalid.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntryLast(vTokens) );
-        return 0;
-    }
-    // find the PI/PO numbers
-    if ( fOutput )
-    {
-        if ( Vec_PtrSize(vTokens) == 3 )
-        {
-            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->vTimeOutputs == NULL )
-            p->pNtk->vTimeOutputs = Vec_IntAlloc( 100 );
-        Vec_IntPush( p->pNtk->vTimeOutputs, Number );
-        Vec_IntPush( p->pNtk->vTimeOutputs, Aig_Float2Int(Delay) );        
-    }
-    else
-    {
-        if ( Vec_PtrSize(vTokens) == 3 )
-        {
-            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->vTimeInputs == NULL )
-            p->pNtk->vTimeInputs = Vec_IntAlloc( 100 );
-        Vec_IntPush( p->pNtk->vTimeInputs, Number );
-        Vec_IntPush( p->pNtk->vTimeInputs, Aig_Float2Int(Delay) );        
-    }
-    return 1;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Constructs the SOP cover from the file parsing info.]
-
-  Description []
-  
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static char * Ioa_ReadParseTableBlif( Ioa_ReadMod_t * p, char * pTable, int nFanins )
-{
-    Vec_Ptr_t * vTokens = p->pMan->vTokens;
-    Vec_Str_t * vFunc = p->pMan->vFunc;
-    char * pProduct, * pOutput;
-    int i, Polarity = -1;
-
-    p->pMan->nTablesRead++;
-    // get the tokens
-    Ioa_ReadSplitIntoTokens( vTokens, pTable, '.' );
-    if ( Vec_PtrSize(vTokens) == 0 )
-        return Ntl_ManStoreSop( p->pMan->pDesign->pMemSops, " 0\n" );
-    if ( Vec_PtrSize(vTokens) == 1 )
-    {
-        pOutput = Vec_PtrEntry( vTokens, 0 );
-        if ( ((pOutput[0] - '0') & 0x8E) || pOutput[1] )
-        {
-            sprintf( p->pMan->sError, "Line %d: Constant table has wrong output value \"%s\".", Ioa_ReadGetLine(p->pMan, pOutput), pOutput );
-            return NULL;
-        }
-        return Ntl_ManStoreSop( p->pMan->pDesign->pMemSops, (pOutput[0] == '0') ? " 0\n" : " 1\n" );
-    }
-    pProduct = Vec_PtrEntry( vTokens, 0 );
-    if ( Vec_PtrSize(vTokens) % 2 == 1 )
-    {
-        sprintf( p->pMan->sError, "Line %d: Table has odd number of tokens (%d).", Ioa_ReadGetLine(p->pMan, pProduct), Vec_PtrSize(vTokens) );
-        return NULL;
-    }
-    // parse the table
-    Vec_StrClear( vFunc );
-    for ( i = 0; i < Vec_PtrSize(vTokens)/2; i++ )
-    {
-        pProduct = Vec_PtrEntry( vTokens, 2*i + 0 );
-        pOutput  = Vec_PtrEntry( vTokens, 2*i + 1 );
-        if ( strlen(pProduct) != (unsigned)nFanins )
-        {
-            sprintf( p->pMan->sError, "Line %d: Cube \"%s\" has size different from the fanin count (%d).", Ioa_ReadGetLine(p->pMan, pProduct), pProduct, nFanins );
-            return NULL;
-        }
-        if ( ((pOutput[0] - '0') & 0x8E) || pOutput[1] )
-        {
-            sprintf( p->pMan->sError, "Line %d: Output value \"%s\" is incorrect.", Ioa_ReadGetLine(p->pMan, pProduct), pOutput );
-            return NULL;
-        }
-        if ( Polarity == -1 )
-            Polarity = pOutput[0] - '0';
-        else if ( Polarity != pOutput[0] - '0' )
-        {
-            sprintf( p->pMan->sError, "Line %d: Output value \"%s\" differs from the value in the first line of the table (%d).", Ioa_ReadGetLine(p->pMan, pProduct), pOutput, Polarity );
-            return NULL;
-        }
-        // parse one product 
-        Vec_StrAppend( vFunc, pProduct );
-        Vec_StrPush( vFunc, ' ' );
-        Vec_StrPush( vFunc, pOutput[0] );
-        Vec_StrPush( vFunc, '\n' );
-    }
-    Vec_StrPush( vFunc, '\0' );
-    return Vec_StrArray( vFunc );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Parses the nodes line.]
-
-  Description []
-  
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static int Ioa_ReadParseLineNamesBlif( Ioa_ReadMod_t * p, char * pLine )
-{
-    Vec_Ptr_t * vTokens = p->pMan->vTokens;
-    Ntl_Obj_t * pNode;
-    Ntl_Net_t * pNetOut, * pNetIn;
-    char * pNameOut, * pNameIn;
-    int i;
-    Ioa_ReadSplitIntoTokens( vTokens, pLine, '\0' );
-    // parse the mapped node
-//    if ( !strcmp(Vec_PtrEntry(vTokens,0), "gate") )
-//        return Ioa_ReadParseLineGateBlif( p, vTokens );
-    // parse the regular name line
-    assert( !strcmp(Vec_PtrEntry(vTokens,0), "names") );
-    pNameOut = Vec_PtrEntryLast( vTokens );
-    pNetOut = Ntl_ModelFindOrCreateNet( p->pNtk, pNameOut );
-    // create fanins
-    pNode = Ntl_ModelCreateNode( p->pNtk, Vec_PtrSize(vTokens) - 2 );
-    for ( i = 0; i < Vec_PtrSize(vTokens) - 2; i++ )
-    {
-        pNameIn = Vec_PtrEntry(vTokens, i+1);
-        pNetIn = Ntl_ModelFindOrCreateNet( p->pNtk, pNameIn );
-        Ntl_ObjSetFanin( pNode, pNetIn, i );
-    }
-    if ( !Ntl_ModelSetNetDriver( pNode, pNetOut ) )
-    {
-        sprintf( p->pMan->sError, "Line %d: Signal \"%s\" is defined more than once.", Ioa_ReadGetLine(p->pMan, pNameOut), pNameOut );
-        return 0;
-    }
-    // parse the table of this node
-    pNode->pSop = Ioa_ReadParseTableBlif( p, pNameOut + strlen(pNameOut), pNode->nFanins );
-    if ( pNode->pSop == NULL )
-        return 0;
-    pNode->pSop = Ntl_ManStoreSop( p->pNtk->pMan->pMemSops, pNode->pSop );
-    return 1;
-}
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/aig/ntl/ntlTable.c b/src/aig/ntl/ntlTable.c
index fe58e2f8..208b4491 100644
--- a/src/aig/ntl/ntlTable.c
+++ b/src/aig/ntl/ntlTable.c
@@ -180,6 +180,27 @@ Ntl_Net_t * Ntl_ModelFindOrCreateNet( Ntl_Mod_t * p, char * pName )
 
 /**Function*************************************************************
 
+  Synopsis    [Assigns numbers to PIs and POs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntl_ModelSetPioNumbers( Ntl_Mod_t * p )
+{
+    Ntl_Obj_t * pObj;
+    int i;
+    Ntl_ModelForEachPi( p, pObj, i )
+        pObj->iTemp = i;
+    Ntl_ModelForEachPo( p, pObj, i )
+        pObj->iTemp = i;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Returns -1, 0, +1 (when it is PI, not found, or PO).]
 
   Description []
@@ -189,7 +210,7 @@ Ntl_Net_t * Ntl_ModelFindOrCreateNet( Ntl_Mod_t * p, char * pName )
   SeeAlso     []
 
 ***********************************************************************/
-int Ntl_ModelFindPioNumber( Ntl_Mod_t * p, int fPiOnly, int fPoOnly, char * pName, int * pNumber )
+int Ntl_ModelFindPioNumber_old( Ntl_Mod_t * p, int fPiOnly, int fPoOnly, char * pName, int * pNumber )
 {
     Ntl_Net_t * pNet;
     Ntl_Obj_t * pObj;
@@ -243,6 +264,60 @@ int Ntl_ModelFindPioNumber( Ntl_Mod_t * p, int fPiOnly, int fPoOnly, char * pNam
 
 /**Function*************************************************************
 
+  Synopsis    [Returns -1, 0, +1 (when it is PI, not found, or PO).]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntl_ModelFindPioNumber( Ntl_Mod_t * p, int fPiOnly, int fPoOnly, char * pName, int * pNumber )
+{
+    Ntl_Net_t * pNet;
+    Ntl_Obj_t * pTerm;
+    *pNumber = -1;
+    pNet = Ntl_ModelFindNet( p, pName );
+    if ( pNet == NULL )
+        return 0;
+    if ( fPiOnly )
+    {
+        pTerm = pNet->pDriver;
+        if ( pTerm && Ntl_ObjIsPi(pTerm) )
+        {
+            *pNumber = pTerm->iTemp;
+            return -1;
+        }
+        return 0;
+    }
+    if ( fPoOnly )
+    {
+        pTerm = pNet->pCopy;
+        if ( pTerm && Ntl_ObjIsPo(pTerm) )
+        {
+            *pNumber = pTerm->iTemp;
+            return 1;
+        }
+        return 0;
+    }
+    pTerm = pNet->pCopy;
+    if ( pTerm && Ntl_ObjIsPo(pTerm) )
+    {
+        *pNumber = pTerm->iTemp;
+        return 1;
+    }
+    pTerm = pNet->pDriver;
+    if ( pTerm && Ntl_ObjIsPi(pTerm) )
+    {
+        *pNumber = pTerm->iTemp;
+        return -1;
+    }
+    return 0;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Sets the driver of the net.]
 
   Description []
diff --git a/src/aig/nwk/nwkCheck.c b/src/aig/nwk/nwkCheck.c
index 0890ced8..f20d61f2 100644
--- a/src/aig/nwk/nwkCheck.c
+++ b/src/aig/nwk/nwkCheck.c
@@ -55,7 +55,7 @@ int Nwk_ManCheck( Nwk_Man_t * p )
     Nwk_ManForEachObj( p, pObj, i )
     {
         Nwk_ObjForEachFanin( pObj, pNext, k )
-            if ( Nwk_ObjFindFanout( pNext, pObj ) == -1 )
+            if ( Nwk_ObjFanoutNum(pNext) < 100 && Nwk_ObjFindFanout( pNext, pObj ) == -1 )
                 printf( "Nwk_ManCheck(): Object %d has fanin %d which does not have a corresponding fanout.\n", pObj->Id, pNext->Id );
         Nwk_ObjForEachFanout( pObj, pNext, k )
             if ( Nwk_ObjFindFanin( pNext, pObj ) == -1 )
diff --git a/src/aig/saig/module.make b/src/aig/saig/module.make
index 48d91438..7063bd2a 100644
--- a/src/aig/saig/module.make
+++ b/src/aig/saig/module.make
@@ -1,5 +1,6 @@
 SRC +=    src/aig/saig/saigAbs.c \
     src/aig/saig/saigBmc.c \
+    src/aig/saig/saigBmc2.c \
     src/aig/saig/saigCone.c \
     src/aig/saig/saigDup.c \
     src/aig/saig/saigHaig.c \
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index f0c8fb54..a6f5631b 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -99,6 +99,7 @@ extern Aig_Man_t *       Saig_ManCreateMiter( Aig_Man_t * p1, Aig_Man_t * p2, in
 extern Aig_Man_t *       Saig_ManCreateMiterComb( Aig_Man_t * p1, Aig_Man_t * p2, int Oper );
 extern Aig_Man_t *       Saig_ManCreateMiterTwo( Aig_Man_t * pOld, Aig_Man_t * pNew, int nFrames );
 extern int               Saig_ManDemiterSimple( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAig1 );
+extern int               Saig_ManDemiterSimpleDiff( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAig1 );
 /*=== 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 5776cd4a..0bbf63f9 100644
--- a/src/aig/saig/saigBmc.c
+++ b/src/aig/saig/saigBmc.c
@@ -26,62 +26,172 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+#define AIG_VISITED       ((Aig_Obj_t *)(PORT_PTRUINT_T)1)
+
+typedef struct Saig_Bmc_t_ Saig_Bmc_t;
+struct Saig_Bmc_t_
+{
+    // parameters
+    int                   nFramesMax;     // the max number of timeframes to consider
+    int                   nConfMaxOne;    // the max number of conflicts at a target
+    int                   nConfMaxAll;    // the max number of conflicts for all targets
+    int                   nNodesMax;      // the max number of nodes to add
+    int                   fVerbose;       // enables verbose output
+    // AIG managers
+    Aig_Man_t *           pAig;           // the user's AIG manager
+    Aig_Man_t *           pFrm;           // Frames manager
+    Vec_Ptr_t *           vVisited;       // nodes visited in Frames
+    // node mapping
+    int                   nObjs;          // the largest number of an AIG object
+    Vec_Ptr_t *           vAig2Frm;       // mapping of AIG nodees into Frames nodes
+    // SAT solver
+    sat_solver *          pSat;           // SAT solver
+    Vec_Int_t *           vObj2Var;       // mapping of frames objects in CNF variables
+    int                   nSatVars;       // the number of used SAT variables
+    Vec_Ptr_t *           vTargets;       // targets to be solved in this interval
+    int                   iFramelast;     // last frame  
+    int                   iOutputLast;    // last output
+};
+
+static inline int         Saig_BmcSatNum( Saig_Bmc_t * p, Aig_Obj_t * pObj )                                { return Vec_IntGetEntry( p->vObj2Var, pObj->Id );  }
+static inline void        Saig_BmcSetSatNum( Saig_Bmc_t * p, Aig_Obj_t * pObj, int Num )                    { Vec_IntSetEntry(p->vObj2Var, pObj->Id, Num);      }
+
+static inline Aig_Obj_t * Saig_BmcObjFrame( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i )                       { return Vec_PtrGetEntry( p->vAig2Frm, p->nObjs*i+pObj->Id );     }
+static inline void        Saig_BmcObjSetFrame( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { Vec_PtrSetEntry( p->vAig2Frm, p->nObjs*i+pObj->Id, pNode );     }
+
+static inline Aig_Obj_t * Saig_BmcObjChild0( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i )                   { assert( !Aig_IsComplement(pObj) ); return Aig_NotCond(Saig_BmcObjFrame(p, Aig_ObjFanin0(pObj), i), Aig_ObjFaninC0(pObj));  }
+static inline Aig_Obj_t * Saig_BmcObjChild1( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i )                   { assert( !Aig_IsComplement(pObj) ); return Aig_NotCond(Saig_BmcObjFrame(p, Aig_ObjFanin1(pObj), i), Aig_ObjFaninC1(pObj));  }
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
-  Synopsis    [Create timeframes of the manager for BMC.]
+  Synopsis    [Create manager.]
 
-  Description [The resulting manager is combinational. POs correspond to \
-  the property outputs in each time-frame.]
+  Description []
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Saig_ManFramesBmc( Aig_Man_t * pAig, int nFrames )
+Saig_Bmc_t * Saig_BmcManStart( Aig_Man_t * pAig, int nConfMaxOne, int nConfMaxAll, int nNodesMax, int fVerbose )
 {
-    Aig_Man_t * pFrames;
-    Aig_Obj_t * pObj, * pObjLi, * pObjLo;
-    int i, f;
-    assert( Saig_ManRegNum(pAig) > 0 );
-    pFrames = Aig_ManStart( Aig_ManNodeNum(pAig) * nFrames );
-    // map the constant node
-    Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames );
-    // create variables for register outputs
+    Saig_Bmc_t * p;
+    Aig_Obj_t * pObj;
+    int i, Lit;
+    assert( Aig_ManRegNum(pAig) > 0 );
+    p = (Saig_Bmc_t *)malloc( sizeof(Saig_Bmc_t) );
+    memset( p, 0, sizeof(Saig_Bmc_t) );
+    // set parameters
+    p->nFramesMax   = 1000000;
+    p->nConfMaxOne  = nConfMaxOne;
+    p->nConfMaxAll  = nConfMaxAll;
+    p->nNodesMax    = nNodesMax;
+    p->fVerbose     = fVerbose;
+    p->pAig         = pAig;
+    p->nObjs        = Aig_ManObjNumMax(pAig);
+    // create node and variable mappings
+    p->vAig2Frm     = Vec_PtrAlloc( 0 );
+    Vec_PtrFill( p->vAig2Frm, 5 * p->nObjs, NULL );
+    p->vObj2Var     = Vec_IntAlloc( 0 );
+    Vec_IntFill( p->vObj2Var, 5 * p->nObjs, 0 );
+    // start the AIG manager and map primary inputs
+    p->pFrm         = Aig_ManStart( 5 * p->nObjs );
     Saig_ManForEachLo( pAig, pObj, i )
-        pObj->pData = Aig_ManConst0( pFrames );
-    // add timeframes
-    for ( f = 0; f < nFrames; f++ )
+        Saig_BmcObjSetFrame( p, pObj, 0, Aig_ManConst0(p->pFrm) ); 
+    // create SAT solver
+    p->pSat         = sat_solver_new();
+    sat_solver_setnvars( p->pSat, 2000 );
+    p->nSatVars = 1;
+    Lit = toLit( p->nSatVars );
+    sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
+    Saig_BmcSetSatNum( p, Aig_ManConst1(p->pFrm), p->nSatVars++ );
+    // other data structures
+    p->vTargets     = Vec_PtrAlloc( 0 );
+    p->vVisited     = Vec_PtrAlloc( 0 );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Delete manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Saig_BmcManStop( Saig_Bmc_t * p )
+{
+    Aig_ManStop( p->pFrm  );
+    Vec_PtrFree( p->vAig2Frm );
+    Vec_IntFree( p->vObj2Var );
+    sat_solver_delete( p->pSat );
+    Vec_PtrFree( p->vTargets );
+    Vec_PtrFree( p->vVisited );
+    free( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Explores the possibility of constructing the output.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Obj_t * Saig_BmcIntervalExplore_rec( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i )
+{
+    Aig_Obj_t * pRes, * p0, * p1, * pConst1 = Aig_ManConst1(p->pAig);
+    pRes = Saig_BmcObjFrame( p, pObj, i );
+    if ( pRes != NULL )
+        return pRes;
+    if ( Saig_ObjIsPi( p->pAig, pObj ) )
+        pRes = AIG_VISITED;
+    else if ( Saig_ObjIsLo( p->pAig, pObj ) )
+        pRes = Saig_BmcIntervalExplore_rec( p, Saig_ObjLoToLi(p->pAig, pObj), i-1 );
+    else if ( Aig_ObjIsPo( pObj ) )
     {
-        // create PI nodes for this frame
-        Saig_ManForEachPi( pAig, pObj, i )
-            pObj->pData = Aig_ObjCreatePi( pFrames );
-        // add internal nodes of this frame
-        Aig_ManForEachNode( pAig, pObj, i )
-            pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
-        // create POs for this frame
-        Saig_ManForEachPo( pAig, pObj, i )
-            Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) );
-        if ( f == nFrames - 1 )
-            break;
-        // save register inputs
-        Saig_ManForEachLi( pAig, pObj, i )
-            pObj->pData = Aig_ObjChild0Copy(pObj);
-        // transfer to register outputs
-        Saig_ManForEachLiLo(  pAig, pObjLi, pObjLo, i )
-            pObjLo->pData = pObjLi->pData;
+        pRes = Saig_BmcIntervalExplore_rec( p, Aig_ObjFanin0(pObj), i );
+        if ( pRes != AIG_VISITED )
+            pRes = Saig_BmcObjChild0( p, pObj, i );
+    }
+    else 
+    {
+        p0 = Saig_BmcIntervalExplore_rec( p, Aig_ObjFanin0(pObj), i );
+        if ( p0 != AIG_VISITED )
+            p0 = Saig_BmcObjChild0( p, pObj, i );
+        p1 = Saig_BmcIntervalExplore_rec( p, Aig_ObjFanin1(pObj), i );
+        if ( p1 != AIG_VISITED )
+            p1 = Saig_BmcObjChild1( p, pObj, i );
+
+        if ( p0 == Aig_Not(p1) )
+            pRes = Aig_Not(pConst1);
+        else if ( Aig_Regular(p0) == pConst1 )
+            pRes = (p0 == pConst1) ? p1 : Aig_Not(pConst1);
+        else if ( Aig_Regular(p1) == pConst1 )
+            pRes = (p1 == pConst1) ? p0 : Aig_Not(pConst1);
+        else 
+            pRes = AIG_VISITED;
+
+        if ( pRes != pConst1 && pRes != Aig_Not(pConst1) )
+            pRes = AIG_VISITED;
     }
-    Aig_ManCleanup( pFrames );
-    return pFrames;
+    Saig_BmcObjSetFrame( p, pObj, i, pRes );
+    return pRes;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Returns the number of internal nodes that are not counted yet.]
+  Synopsis    [Performs the actual construction of the output.]
 
   Description []
                
@@ -90,81 +200,70 @@ Aig_Man_t * Saig_ManFramesBmc( Aig_Man_t * pAig, int nFrames )
   SeeAlso     []
 
 ***********************************************************************/
-int Saig_ManFramesCount_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
+Aig_Obj_t * Saig_BmcIntervalConstruct_rec( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i )
 {
-    if ( !Aig_ObjIsNode(pObj) )
-        return 0;
-    if ( Aig_ObjIsTravIdCurrent(p, pObj) )
-        return 0;
-    Aig_ObjSetTravIdCurrent(p, pObj);
-    return 1 + Saig_ManFramesCount_rec( p, Aig_ObjFanin0(pObj) ) + 
-        Saig_ManFramesCount_rec( p, Aig_ObjFanin1(pObj) );
+    Aig_Obj_t * pRes;
+    pRes = Saig_BmcObjFrame( p, pObj, i );
+    assert( pRes != NULL );
+    if ( pRes != AIG_VISITED )
+        return pRes;
+    if ( Saig_ObjIsPi( p->pAig, pObj ) )
+        pRes = Aig_ObjCreatePi(p->pFrm);
+    else if ( Saig_ObjIsLo( p->pAig, pObj ) )
+        pRes = Saig_BmcIntervalConstruct_rec( p, Saig_ObjLoToLi(p->pAig, pObj), i-1 );
+    else if ( Aig_ObjIsPo( pObj ) )
+    {
+        Saig_BmcIntervalConstruct_rec( p, Aig_ObjFanin0(pObj), i );
+        pRes = Saig_BmcObjChild0( p, pObj, i );
+    }
+    else 
+    {
+        Saig_BmcIntervalConstruct_rec( p, Aig_ObjFanin0(pObj), i );
+        Saig_BmcIntervalConstruct_rec( p, Aig_ObjFanin1(pObj), i );
+        pRes = Aig_And( p->pFrm, Saig_BmcObjChild0(p, pObj, i), Saig_BmcObjChild1(p, pObj, i) );
+    }
+    Saig_BmcObjSetFrame( p, pObj, i, pRes );
+    return pRes;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Create timeframes of the manager for BMC.]
+  Synopsis    [Adds new AIG nodes to the frames.]
 
-  Description [The resulting manager is combinational. POs correspond to 
-  the property outputs in each time-frame.
-  The unrolling is stopped as soon as the number of nodes in the frames
-  exceeds the given maximum size.]
+  Description []
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Saig_ManFramesBmcLimit( Aig_Man_t * pAig, int nFrames, int nSizeMax )
+void Saig_BmcInterval( Saig_Bmc_t * p )
 {
-    Aig_Man_t * pFrames;
-    Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjPo;
-    int i, f, Counter = 0;
-    assert( Saig_ManRegNum(pAig) > 0 );
-    pFrames = Aig_ManStart( nSizeMax );
-    Aig_ManIncrementTravId( pFrames );
-    // map the constant node
-    Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames );
-    // create variables for register outputs
-    Saig_ManForEachLo( pAig, pObj, i )
-        pObj->pData = Aig_ManConst0( pFrames );
-    // add timeframes
-    Counter = 0;
-    for ( f = 0; f < nFrames; f++ )
+    Aig_Obj_t * pTarget, * pObj;
+    int i, nNodes = Aig_ManNodeNum( p->pFrm );
+    Vec_PtrClear( p->vTargets );
+    for ( ; p->iFramelast < p->nFramesMax; p->iFramelast++, p->iOutputLast = 0 )
     {
-        // create PI nodes for this frame
-        Saig_ManForEachPi( pAig, pObj, i )
-            pObj->pData = Aig_ObjCreatePi( pFrames );
-        // add internal nodes of this frame
-        Aig_ManForEachNode( pAig, pObj, i )
-            pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
-        // create POs for this frame
-        Saig_ManForEachPo( pAig, pObj, i )
+        if ( p->iOutputLast == 0 )
         {
-            pObjPo = Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) );
-            Counter += Saig_ManFramesCount_rec( pFrames, Aig_ObjFanin0(pObjPo) );
+            Saig_BmcObjSetFrame( p, Aig_ManConst1(p->pAig), p->iFramelast, Aig_ManConst1(p->pFrm) );
+            Saig_ManForEachPi( p->pAig, pObj, i )
+                Saig_BmcObjSetFrame( p, pObj, p->iFramelast, Aig_ObjCreatePi(p->pFrm) ); 
         }
-        if ( Counter >= nSizeMax )
+        for ( ; p->iOutputLast < Saig_ManPoNum(p->pAig); p->iOutputLast++ )
         {
-            Aig_ManCleanup( pFrames );
-            return pFrames;
+            if ( Aig_ManNodeNum(p->pFrm) >= nNodes + p->nNodesMax )
+                return;
+            Saig_BmcIntervalExplore_rec( p, Aig_ManPo(p->pAig, p->iOutputLast), p->nFramesMax );
+            pTarget = Saig_BmcIntervalConstruct_rec( p, Aig_ManPo(p->pAig, p->iOutputLast), p->nFramesMax );
+            Vec_PtrPush( p->vTargets, pTarget );
         }
-        if ( f == nFrames - 1 )
-            break;
-        // save register inputs
-        Saig_ManForEachLi( pAig, pObj, i )
-            pObj->pData = Aig_ObjChild0Copy(pObj);
-        // transfer to register outputs
-        Saig_ManForEachLiLo(  pAig, pObjLi, pObjLo, i )
-            pObjLo->pData = pObjLi->pData;
     }
-    Aig_ManCleanup( pFrames );
-    return pFrames;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Performs BMC for the given AIG.]
+  Synopsis    [Performs the actual construction of the output.]
 
   Description []
                
@@ -173,140 +272,179 @@ Aig_Man_t * Saig_ManFramesBmcLimit( Aig_Man_t * pAig, int nFrames, int nSizeMax
   SeeAlso     []
 
 ***********************************************************************/
-int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLimit, int fRewrite, int fVerbose, int * piFrame )
+Aig_Obj_t * Saig_BmcIntervalToAig_rec( Saig_Bmc_t * p, Aig_Man_t * pNew, Aig_Obj_t * pObj )
 {
-    sat_solver * pSat;
-    Cnf_Dat_t * pCnf;
-    Aig_Man_t * pFrames, * pAigTemp;
-    Aig_Obj_t * pObj;
-    int status, clk, Lit, i, RetValue = 1;
-    // derive the timeframes
-    clk = clock();
-    if ( nSizeMax > 0 )
-    {
-        pFrames = Saig_ManFramesBmcLimit( pAig, nFrames, nSizeMax );
-        nFrames = Aig_ManPoNum(pFrames) / Saig_ManPoNum(pAig) + ((Aig_ManPoNum(pFrames) % Saig_ManPoNum(pAig)) > 0);
-    }
-    else
-        pFrames = Saig_ManFramesBmc( pAig, nFrames );
-    if ( piFrame )
-        *piFrame = nFrames;
-    if ( fVerbose )
+    if ( pObj->pData )
+        return pObj->pData;
+    Vec_PtrPush( p->vVisited, pObj );
+    if ( Saig_BmcSatNum(p, pObj) || Aig_ObjIsPi(pObj) )
+        return pObj->pData = Aig_ObjCreatePi(pNew);
+    Saig_BmcIntervalToAig_rec( p, pNew, Aig_ObjFanin0(pObj) );
+    Saig_BmcIntervalToAig_rec( p, pNew, Aig_ObjFanin1(pObj) );
+    return pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates AIG of the newly added nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Saig_BmcIntervalToAig( Saig_Bmc_t * p )
+{
+    Aig_Man_t * pNew;
+    Aig_Obj_t * pObj, * pObjNew;
+    int i;
+    pNew = Aig_ManStart( p->nNodesMax );
+    Aig_ManConst1(p->pFrm)->pData = Aig_ManConst1(pNew);
+    Vec_PtrClear( p->vVisited );
+    Vec_PtrPush( p->vVisited, Aig_ManConst1(p->pFrm) );
+    Vec_PtrForEachEntry( p->vTargets, pObj, i )
     {
-        printf( "AIG:  PI/PO/Reg = %d/%d/%d.  Node = %6d. Lev = %5d.\n", 
-            Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), Saig_ManRegNum(pAig),
-            Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig) );
-        printf( "Time-frames (%d):  PI/PO = %d/%d.  Node = %6d. Lev = %5d.  ", 
-            nFrames, Aig_ManPiNum(pFrames), Aig_ManPoNum(pFrames), 
-            Aig_ManNodeNum(pFrames), Aig_ManLevelNum(pFrames) );
-        PRT( "Time", clock() - clk );
-        fflush( stdout );
+        pObjNew = Saig_BmcIntervalToAig_rec( p, pNew, Aig_Regular(pObj) );
+        Aig_ObjCreatePo( pNew, pObjNew );
     }
-    // rewrite the timeframes
-    if ( fRewrite )
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives CNF for the newly added nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Saig_BmcLoadCnf( Saig_Bmc_t * p, Cnf_Dat_t * pCnf )
+{
+    Aig_Obj_t * pObj, * pObjNew;
+    int i, Lits[2], VarNumOld, VarNumNew;
+    Vec_PtrForEachEntry( p->vVisited, pObj, i )
     {
-        clk = clock();
-//        pFrames = Dar_ManBalance( pAigTemp = pFrames, 0 );
-        pFrames = Dar_ManRwsat( pAigTemp = pFrames, 1, 0 );
-        Aig_ManStop( pAigTemp );
-        if ( fVerbose )
+        pObjNew   = pObj->pData;
+        pObj->pData = NULL;
+        VarNumNew = pCnf->pVarNums[ pObjNew->Id ];
+        if ( VarNumNew == -1 )
+            continue;
+        VarNumOld = Saig_BmcSatNum( p, pObj );
+        if ( VarNumOld == 0 )
         {
-            printf( "Time-frames after rewriting:  Node = %6d. Lev = %5d.  ", 
-                Aig_ManNodeNum(pFrames), Aig_ManLevelNum(pFrames) );
-            PRT( "Time", clock() - clk );
-            fflush( stdout );
+            Saig_BmcSetSatNum( p, pObj, VarNumNew );
+            continue;
         }
-    }
-    // create the SAT solver
-    clk = clock();
-    pCnf = Cnf_Derive( pFrames, Aig_ManPoNum(pFrames) );  
-    pSat = sat_solver_new();
-    sat_solver_setnvars( pSat, pCnf->nVars );
-    for ( i = 0; i < pCnf->nClauses; i++ )
-    {
-        if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
+        // add clauses connecting existing variables
+        Lits[0] = toLitCond( VarNumOld, 0 );
+        Lits[1] = toLitCond( VarNumNew, 1 );
+        if ( !sat_solver_addclause( p->pSat, Lits, Lits+2 ) )
+            assert( 0 );
+        Lits[0] = toLitCond( VarNumOld, 1 );
+        Lits[1] = toLitCond( VarNumNew, 0 );
+        if ( !sat_solver_addclause( p->pSat, Lits, Lits+2 ) )
             assert( 0 );
     }
-    if ( fVerbose )
+    // add CNF to the SAT solver
+    for ( i = 0; i < pCnf->nClauses; i++ )
+        if ( !sat_solver_addclause( p->pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
+            break;
+    if ( i < pCnf->nClauses )
+        printf( "SAT solver became UNSAT after adding clauses.\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Solves targets with the given resource limit.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Saig_BmcSolveTargets( Saig_Bmc_t * p )
+{
+    Aig_Obj_t * pObj;
+    int i, VarNum, Lit, RetValue;
+    assert( Vec_PtrSize(p->vTargets) > 0 );
+    Vec_PtrForEachEntry( p->vTargets, pObj, i )
     {
-        printf( "CNF: Variables = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals );
-        PRT( "Time", clock() - clk );
-        fflush( stdout );
+        if ( p->pSat->stats.conflicts > p->nConfMaxAll )
+            return l_Undef;
+        VarNum = Saig_BmcSatNum( p, Aig_Regular(pObj) );
+        Lit = toLitCond( VarNum, Aig_IsComplement(pObj) );
+        RetValue = sat_solver_solve( p->pSat, &Lit, &Lit + 1, (sint64)p->nConfMaxOne, (sint64)0, (sint64)0, (sint64)0 );
+        if ( RetValue == l_False ) // unsat
+            continue;
+        if ( RetValue == l_Undef ) // undecided
+            return l_Undef;
+        // generate counter-example
+        return l_True;
     }
-    status = sat_solver_simplify(pSat);
-    if ( status == 0 )
+    return l_False;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs BMC with the given parameters.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Saig_BmcPerform( Aig_Man_t * pAig, int nConfMaxOne, int nConfMaxAll, int nNodesMax, int fVerbose )
+{
+    Saig_Bmc_t * p;
+    Aig_Man_t * pNew;
+    Cnf_Dat_t * pCnf;
+    int RetValue, clk = clock();
+    p = Saig_BmcManStart( pAig, nConfMaxOne, nConfMaxAll, nNodesMax, fVerbose );
+    while ( 1 )
     {
-        if ( fVerbose )
-        {
-            printf( "The BMC problem is trivially UNSAT\n" );
-            fflush( stdout );
-        }
+        // add new logic slice to frames
+        Saig_BmcInterval( p );
+        if ( Vec_PtrSize(p->vTargets) == 0 )
+            break;
+        // convert logic slice into new AIG
+        pNew = Saig_BmcIntervalToAig( p );
+        // derive CNF for the new AIG
+        pCnf = Cnf_Derive( pNew, Aig_ManPoNum(pNew) );
+        Cnf_DataLift( pCnf, p->nSatVars );
+        p->nSatVars += pCnf->nVars;
+        // add this CNF to the solver
+        Saig_BmcLoadCnf( p, pCnf );
+        Cnf_DataFree( pCnf );
+        Aig_ManStop( pNew );
+        // solve the targets
+        RetValue = Saig_BmcSolveTargets( p );
+        if ( RetValue != l_False )
+            break;
     }
+    if ( RetValue == l_True )
+        printf( "BMC failed for output %d in frame %d.  ", p->iOutputLast, p->iFramelast );
+    else // if ( RetValue == l_False || RetValue == l_Undef )
+        printf( "BMC completed for %d timeframes.  ", p->iFramelast );
+    PRT( "Time", clock() - clk );
+    if ( p->iFramelast >= p->nFramesMax )
+        printf( "Reached limit on the number of timeframes (%d).\n", p->nFramesMax );
+    else if ( p->pSat->stats.conflicts > p->nConfMaxAll )
+        printf( "Reached global conflict limit (%d).\n", p->nConfMaxAll );
     else
-    {
-        int clkPart = clock();
-        Aig_ManForEachPo( pFrames, pObj, i )
-        {
-            Lit = toLitCond( pCnf->pVarNums[pObj->Id], 0 );
-            if ( fVerbose )
-            {
-                printf( "Solving output %2d of frame %3d ... \r", 
-                    i % Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) );
-            }
-            clk = clock();
-            status = sat_solver_solve( pSat, &Lit, &Lit + 1, (sint64)nConfLimit, (sint64)0, (sint64)0, (sint64)0 );
-            if ( fVerbose && (i % Saig_ManPoNum(pAig) == Saig_ManPoNum(pAig) - 1) )
-            {
-                printf( "Solved %2d outputs of frame %3d.  ", 
-                    Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) );
-                printf( "Conf =%8.0f. Imp =%11.0f. ", (double)pSat->stats.conflicts, (double)pSat->stats.propagations );
-                PRT( "T", clock() - clkPart );
-                clkPart = clock();
-                fflush( stdout );
-            }
-            if ( status == l_False )
-            {
-/*
-                Lit = lit_neg( Lit );
-                RetValue = sat_solver_addclause( pSat, &Lit, &Lit + 1 );
-                assert( RetValue );
-                if ( pSat->qtail != pSat->qhead )
-                {
-                    RetValue = sat_solver_simplify(pSat);
-                    assert( RetValue );
-                }
-*/
-            }
-            else if ( status == l_True )
-            {
-                extern void * Fra_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, int * pModel );
-                Vec_Int_t * vCiIds = Cnf_DataCollectPiSatNums( pCnf, pFrames );
-                int * pModel = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize );
-                pModel[Aig_ManPiNum(pFrames)] = pObj->Id;
-                pAig->pSeqModel = Fra_SmlCopyCounterExample( pAig, pFrames, pModel );
-                free( pModel );
-                Vec_IntFree( vCiIds );
-
-//                if ( piFrame )
-//                    *piFrame = i / Saig_ManPoNum(pAig);
-                RetValue = 0;
-                break;
-            }
-            else
-            {
-                if ( piFrame )
-                    *piFrame = i / Saig_ManPoNum(pAig);
-                RetValue = -1;
-                break;
-            }
-        }
-    }
-    sat_solver_delete( pSat );
-    Cnf_DataFree( pCnf );
-    Aig_ManStop( pFrames );
-    return RetValue;
+        printf( "Reached local conflict limit (%d).\n", p->nConfMaxOne );
+    Saig_BmcManStop( p );
 }
 
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/saig/saigBmc2.c b/src/aig/saig/saigBmc2.c
new file mode 100644
index 00000000..5776cd4a
--- /dev/null
+++ b/src/aig/saig/saigBmc2.c
@@ -0,0 +1,314 @@
+/**CFile****************************************************************
+
+  FileName    [saigBmc.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Sequential AIG package.]
+
+  Synopsis    [Simple BMC package.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: saigBmc.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "saig.h"
+#include "cnf.h"
+#include "satStore.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Create timeframes of the manager for BMC.]
+
+  Description [The resulting manager is combinational. POs correspond to \
+  the property outputs in each time-frame.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManFramesBmc( Aig_Man_t * pAig, int nFrames )
+{
+    Aig_Man_t * pFrames;
+    Aig_Obj_t * pObj, * pObjLi, * pObjLo;
+    int i, f;
+    assert( Saig_ManRegNum(pAig) > 0 );
+    pFrames = Aig_ManStart( Aig_ManNodeNum(pAig) * nFrames );
+    // map the constant node
+    Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames );
+    // create variables for register outputs
+    Saig_ManForEachLo( pAig, pObj, i )
+        pObj->pData = Aig_ManConst0( pFrames );
+    // add timeframes
+    for ( f = 0; f < nFrames; f++ )
+    {
+        // create PI nodes for this frame
+        Saig_ManForEachPi( pAig, pObj, i )
+            pObj->pData = Aig_ObjCreatePi( pFrames );
+        // add internal nodes of this frame
+        Aig_ManForEachNode( pAig, pObj, i )
+            pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+        // create POs for this frame
+        Saig_ManForEachPo( pAig, pObj, i )
+            Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) );
+        if ( f == nFrames - 1 )
+            break;
+        // save register inputs
+        Saig_ManForEachLi( pAig, pObj, i )
+            pObj->pData = Aig_ObjChild0Copy(pObj);
+        // transfer to register outputs
+        Saig_ManForEachLiLo(  pAig, pObjLi, pObjLo, i )
+            pObjLo->pData = pObjLi->pData;
+    }
+    Aig_ManCleanup( pFrames );
+    return pFrames;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the number of internal nodes that are not counted yet.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Saig_ManFramesCount_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+    if ( !Aig_ObjIsNode(pObj) )
+        return 0;
+    if ( Aig_ObjIsTravIdCurrent(p, pObj) )
+        return 0;
+    Aig_ObjSetTravIdCurrent(p, pObj);
+    return 1 + Saig_ManFramesCount_rec( p, Aig_ObjFanin0(pObj) ) + 
+        Saig_ManFramesCount_rec( p, Aig_ObjFanin1(pObj) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Create timeframes of the manager for BMC.]
+
+  Description [The resulting manager is combinational. POs correspond to 
+  the property outputs in each time-frame.
+  The unrolling is stopped as soon as the number of nodes in the frames
+  exceeds the given maximum size.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManFramesBmcLimit( Aig_Man_t * pAig, int nFrames, int nSizeMax )
+{
+    Aig_Man_t * pFrames;
+    Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjPo;
+    int i, f, Counter = 0;
+    assert( Saig_ManRegNum(pAig) > 0 );
+    pFrames = Aig_ManStart( nSizeMax );
+    Aig_ManIncrementTravId( pFrames );
+    // map the constant node
+    Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames );
+    // create variables for register outputs
+    Saig_ManForEachLo( pAig, pObj, i )
+        pObj->pData = Aig_ManConst0( pFrames );
+    // add timeframes
+    Counter = 0;
+    for ( f = 0; f < nFrames; f++ )
+    {
+        // create PI nodes for this frame
+        Saig_ManForEachPi( pAig, pObj, i )
+            pObj->pData = Aig_ObjCreatePi( pFrames );
+        // add internal nodes of this frame
+        Aig_ManForEachNode( pAig, pObj, i )
+            pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+        // create POs for this frame
+        Saig_ManForEachPo( pAig, pObj, i )
+        {
+            pObjPo = Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) );
+            Counter += Saig_ManFramesCount_rec( pFrames, Aig_ObjFanin0(pObjPo) );
+        }
+        if ( Counter >= nSizeMax )
+        {
+            Aig_ManCleanup( pFrames );
+            return pFrames;
+        }
+        if ( f == nFrames - 1 )
+            break;
+        // save register inputs
+        Saig_ManForEachLi( pAig, pObj, i )
+            pObj->pData = Aig_ObjChild0Copy(pObj);
+        // transfer to register outputs
+        Saig_ManForEachLiLo(  pAig, pObjLi, pObjLo, i )
+            pObjLo->pData = pObjLi->pData;
+    }
+    Aig_ManCleanup( pFrames );
+    return pFrames;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs BMC for the given AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLimit, int fRewrite, int fVerbose, int * piFrame )
+{
+    sat_solver * pSat;
+    Cnf_Dat_t * pCnf;
+    Aig_Man_t * pFrames, * pAigTemp;
+    Aig_Obj_t * pObj;
+    int status, clk, Lit, i, RetValue = 1;
+    // derive the timeframes
+    clk = clock();
+    if ( nSizeMax > 0 )
+    {
+        pFrames = Saig_ManFramesBmcLimit( pAig, nFrames, nSizeMax );
+        nFrames = Aig_ManPoNum(pFrames) / Saig_ManPoNum(pAig) + ((Aig_ManPoNum(pFrames) % Saig_ManPoNum(pAig)) > 0);
+    }
+    else
+        pFrames = Saig_ManFramesBmc( pAig, nFrames );
+    if ( piFrame )
+        *piFrame = nFrames;
+    if ( fVerbose )
+    {
+        printf( "AIG:  PI/PO/Reg = %d/%d/%d.  Node = %6d. Lev = %5d.\n", 
+            Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), Saig_ManRegNum(pAig),
+            Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig) );
+        printf( "Time-frames (%d):  PI/PO = %d/%d.  Node = %6d. Lev = %5d.  ", 
+            nFrames, Aig_ManPiNum(pFrames), Aig_ManPoNum(pFrames), 
+            Aig_ManNodeNum(pFrames), Aig_ManLevelNum(pFrames) );
+        PRT( "Time", clock() - clk );
+        fflush( stdout );
+    }
+    // rewrite the timeframes
+    if ( fRewrite )
+    {
+        clk = clock();
+//        pFrames = Dar_ManBalance( pAigTemp = pFrames, 0 );
+        pFrames = Dar_ManRwsat( pAigTemp = pFrames, 1, 0 );
+        Aig_ManStop( pAigTemp );
+        if ( fVerbose )
+        {
+            printf( "Time-frames after rewriting:  Node = %6d. Lev = %5d.  ", 
+                Aig_ManNodeNum(pFrames), Aig_ManLevelNum(pFrames) );
+            PRT( "Time", clock() - clk );
+            fflush( stdout );
+        }
+    }
+    // create the SAT solver
+    clk = clock();
+    pCnf = Cnf_Derive( pFrames, Aig_ManPoNum(pFrames) );  
+    pSat = sat_solver_new();
+    sat_solver_setnvars( pSat, pCnf->nVars );
+    for ( i = 0; i < pCnf->nClauses; i++ )
+    {
+        if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
+            assert( 0 );
+    }
+    if ( fVerbose )
+    {
+        printf( "CNF: Variables = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals );
+        PRT( "Time", clock() - clk );
+        fflush( stdout );
+    }
+    status = sat_solver_simplify(pSat);
+    if ( status == 0 )
+    {
+        if ( fVerbose )
+        {
+            printf( "The BMC problem is trivially UNSAT\n" );
+            fflush( stdout );
+        }
+    }
+    else
+    {
+        int clkPart = clock();
+        Aig_ManForEachPo( pFrames, pObj, i )
+        {
+            Lit = toLitCond( pCnf->pVarNums[pObj->Id], 0 );
+            if ( fVerbose )
+            {
+                printf( "Solving output %2d of frame %3d ... \r", 
+                    i % Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) );
+            }
+            clk = clock();
+            status = sat_solver_solve( pSat, &Lit, &Lit + 1, (sint64)nConfLimit, (sint64)0, (sint64)0, (sint64)0 );
+            if ( fVerbose && (i % Saig_ManPoNum(pAig) == Saig_ManPoNum(pAig) - 1) )
+            {
+                printf( "Solved %2d outputs of frame %3d.  ", 
+                    Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) );
+                printf( "Conf =%8.0f. Imp =%11.0f. ", (double)pSat->stats.conflicts, (double)pSat->stats.propagations );
+                PRT( "T", clock() - clkPart );
+                clkPart = clock();
+                fflush( stdout );
+            }
+            if ( status == l_False )
+            {
+/*
+                Lit = lit_neg( Lit );
+                RetValue = sat_solver_addclause( pSat, &Lit, &Lit + 1 );
+                assert( RetValue );
+                if ( pSat->qtail != pSat->qhead )
+                {
+                    RetValue = sat_solver_simplify(pSat);
+                    assert( RetValue );
+                }
+*/
+            }
+            else if ( status == l_True )
+            {
+                extern void * Fra_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, int * pModel );
+                Vec_Int_t * vCiIds = Cnf_DataCollectPiSatNums( pCnf, pFrames );
+                int * pModel = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize );
+                pModel[Aig_ManPiNum(pFrames)] = pObj->Id;
+                pAig->pSeqModel = Fra_SmlCopyCounterExample( pAig, pFrames, pModel );
+                free( pModel );
+                Vec_IntFree( vCiIds );
+
+//                if ( piFrame )
+//                    *piFrame = i / Saig_ManPoNum(pAig);
+                RetValue = 0;
+                break;
+            }
+            else
+            {
+                if ( piFrame )
+                    *piFrame = i / Saig_ManPoNum(pAig);
+                RetValue = -1;
+                break;
+            }
+        }
+    }
+    sat_solver_delete( pSat );
+    Cnf_DataFree( pCnf );
+    Aig_ManStop( pFrames );
+    return RetValue;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/saig/saigMiter.c b/src/aig/saig/saigMiter.c
index 5efcd24d..cc71f371 100644
--- a/src/aig/saig/saigMiter.c
+++ b/src/aig/saig/saigMiter.c
@@ -49,6 +49,8 @@ Aig_Man_t * Saig_ManCreateMiter( Aig_Man_t * p0, Aig_Man_t * p1, int Oper )
     assert( Saig_ManPoNum(p0) == Saig_ManPoNum(p1) );
     pNew = Aig_ManStart( Aig_ManObjNumMax(p0) + Aig_ManObjNumMax(p1) );
     pNew->pName = Aig_UtilStrsav( "miter" );
+    Aig_ManCleanData( p0 );
+    Aig_ManCleanData( p1 );
     // map constant nodes
     Aig_ManConst1(p0)->pData = Aig_ManConst1(pNew);
     Aig_ManConst1(p1)->pData = Aig_ManConst1(pNew);
@@ -85,7 +87,7 @@ Aig_Man_t * Saig_ManCreateMiter( Aig_Man_t * p0, Aig_Man_t * p1, int Oper )
         pObj->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
     // cleanup
     Aig_ManSetRegNum( pNew, Saig_ManRegNum(p0) + Saig_ManRegNum(p1) );
-    Aig_ManCleanup( pNew );
+//    Aig_ManCleanup( pNew );
     return pNew;
 }
 
@@ -184,6 +186,9 @@ Aig_Man_t * Saig_ManUnrollTwo( Aig_Man_t * pBot, Aig_Man_t * pTop, int nFrames )
                 Aig_ObjCreatePo( p, Aig_ObjChild0Copy(pObj) );
             break;
         }
+        // create POs for this frame
+        Saig_ManForEachPo( pAig, pObj, i )
+            Aig_ObjCreatePo( p, Aig_ObjChild0Copy(pObj) );
         // save register inputs
         Saig_ManForEachLi( pAig, pObj, i )
             pObj->pData = Aig_ObjChild0Copy(pObj);
@@ -213,7 +218,7 @@ Aig_Man_t * Saig_ManUnrollTwo( Aig_Man_t * pBot, Aig_Man_t * pTop, int nFrames )
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Aig_ManDupNodes_old( Aig_Man_t * p, Vec_Ptr_t * vSet )
+Aig_Man_t * Aig_ManDupNodesAll( Aig_Man_t * p, Vec_Ptr_t * vSet )
 {
     Aig_Man_t * pNew, * pCopy;
     Aig_Obj_t * pObj;
@@ -250,7 +255,7 @@ Aig_Man_t * Aig_ManDupNodes_old( Aig_Man_t * p, Vec_Ptr_t * vSet )
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Aig_ManDupNodes( Aig_Man_t * p, Vec_Ptr_t * vSet, int iPart )
+Aig_Man_t * Aig_ManDupNodesHalf( Aig_Man_t * p, Vec_Ptr_t * vSet, int iPart )
 {
     Aig_Man_t * pNew, * pCopy;
     Aig_Obj_t * pObj;
@@ -337,6 +342,79 @@ int Saig_ManDemiterSimple( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAi
             Vec_PtrFree( vSet1 );
             return 0;
         }
+        if ( Aig_ObjFaninC0(pObj) )
+            pObj0 = Aig_Not(pObj0);
+
+//        printf( "%d %d  ", Aig_Regular(pObj0)->Id, Aig_Regular(pObj1)->Id );
+        if ( Aig_Regular(pObj0)->Id < Aig_Regular(pObj1)->Id )
+        {
+            Vec_PtrPush( vSet0, pObj0 );
+            Vec_PtrPush( vSet1, pObj1 );
+        }
+        else
+        {
+            Vec_PtrPush( vSet0, pObj1 );
+            Vec_PtrPush( vSet1, pObj0 );
+        }
+    }
+//    printf( "Miter has %d constant outputs.\n", Counter );
+//    printf( "\n" );
+    if ( ppAig0 )
+    {
+        *ppAig0 = Aig_ManDupNodesHalf( p, vSet0, 0 );
+        FREE( (*ppAig0)->pName );
+        (*ppAig0)->pName = Aig_UtilStrsav( "part0" );
+    }
+    if ( ppAig1 )
+    {
+        *ppAig1 = Aig_ManDupNodesHalf( p, vSet1, 1 );
+        FREE( (*ppAig1)->pName );
+        (*ppAig1)->pName = Aig_UtilStrsav( "part1" );
+    }
+    Vec_PtrFree( vSet0 );
+    Vec_PtrFree( vSet1 );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates the AIG to have constant-0 initial state.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Saig_ManDemiterSimpleDiff( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAig1 )
+{
+    Vec_Ptr_t * vSet0, * vSet1;
+    Aig_Obj_t * pObj, * pFanin, * pObj0, * pObj1;
+    int i, Counter = 0;
+    assert( Saig_ManRegNum(p) % 2 == 0 );
+    vSet0 = Vec_PtrAlloc( Saig_ManPoNum(p) );
+    vSet1 = Vec_PtrAlloc( Saig_ManPoNum(p) );
+    Saig_ManForEachPo( p, pObj, i )
+    {
+        pFanin = Aig_ObjFanin0(pObj);
+        if ( Aig_ObjIsConst1( pFanin ) )
+        {
+            if ( !Aig_ObjFaninC0(pObj) )
+                printf( "The output number %d of the miter is constant 1.\n", i );
+            Counter++;
+            continue;
+        }
+        if ( !Aig_ObjIsNode(pFanin) || !Aig_ObjRecognizeExor( pFanin, &pObj0, &pObj1 ) )
+        {
+            printf( "The miter cannot be demitered.\n" );
+            Vec_PtrFree( vSet0 );
+            Vec_PtrFree( vSet1 );
+            return 0;
+        }
+        if ( Aig_ObjFaninC0(pObj) )
+            pObj0 = Aig_Not(pObj0);
+
 //        printf( "%d %d  ", Aig_Regular(pObj0)->Id, Aig_Regular(pObj1)->Id );
         if ( Aig_Regular(pObj0)->Id < Aig_Regular(pObj1)->Id )
         {
@@ -353,13 +431,13 @@ int Saig_ManDemiterSimple( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAi
 //    printf( "\n" );
     if ( ppAig0 )
     {
-        *ppAig0 = Aig_ManDupNodes( p, vSet0, 0 );
+        *ppAig0 = Aig_ManDupNodesAll( p, vSet0 );
         FREE( (*ppAig0)->pName );
         (*ppAig0)->pName = Aig_UtilStrsav( "part0" );
     }
     if ( ppAig1 )
     {
-        *ppAig1 = Aig_ManDupNodes( p, vSet1, 1 );
+        *ppAig1 = Aig_ManDupNodesAll( p, vSet1 );
         FREE( (*ppAig1)->pName );
         (*ppAig1)->pName = Aig_UtilStrsav( "part1" );
     }
@@ -525,14 +603,14 @@ int Saig_ManDemiter( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAig1 )
     if ( ppAig0 )
     {
         assert( 0 );
-        *ppAig0 = Aig_ManDupNodes( p, vSet0, 0 ); // not ready
+        *ppAig0 = Aig_ManDupNodesHalf( p, vSet0, 0 ); // not ready
         FREE( (*ppAig0)->pName );
         (*ppAig0)->pName = Aig_UtilStrsav( "part0" );
     }
     if ( ppAig1 )
     {
         assert( 0 );
-        *ppAig1 = Aig_ManDupNodes( p, vSet1, 1 ); // not ready
+        *ppAig1 = Aig_ManDupNodesHalf( p, vSet1, 1 ); // not ready
         FREE( (*ppAig1)->pName );
         (*ppAig1)->pName = Aig_UtilStrsav( "part1" );
     }
@@ -566,6 +644,42 @@ Aig_Man_t * Saig_ManCreateMiterTwo( Aig_Man_t * pOld, Aig_Man_t * pNew, int nFra
     return pMiter;
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    [Resimulates counter-example and returns the failed output number.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ssw_SecCexResimulate( Aig_Man_t * p, int * pModel, int * pnOutputs )
+{
+    Aig_Obj_t * pObj;
+    int i, RetValue = -1;
+    *pnOutputs = 0;
+    Aig_ManConst1(p)->fMarkA = 1;
+    Aig_ManForEachPi( p, pObj, i )
+        pObj->fMarkA = pModel[i];
+    Aig_ManForEachNode( p, pObj, i )
+        pObj->fMarkA = ( Aig_ObjFanin0(pObj)->fMarkA ^ Aig_ObjFaninC0(pObj) ) & 
+                      ( Aig_ObjFanin1(pObj)->fMarkA ^ Aig_ObjFaninC1(pObj) );
+    Aig_ManForEachPo( p, pObj, i )
+        pObj->fMarkA = Aig_ObjFanin0(pObj)->fMarkA ^ Aig_ObjFaninC0(pObj);
+    Aig_ManForEachPo( p, pObj, i )
+        if ( pObj->fMarkA )
+        {
+            if ( RetValue == -1 )
+                RetValue = i;
+            (*pnOutputs)++;
+        }
+    Aig_ManCleanMarkA(p);
+    return RetValue;
+}
+
 /**Function*************************************************************
 
   Synopsis    [Reduces SEC to CEC for the special case of seq synthesis.]
@@ -578,12 +692,16 @@ Aig_Man_t * Saig_ManCreateMiterTwo( Aig_Man_t * pOld, Aig_Man_t * pNew, int nFra
   SeeAlso     []
 
 ***********************************************************************/
-int Ssw_SecSpecial( Aig_Man_t * pPart0, Aig_Man_t * pPart1, int fVerbose )
+int Ssw_SecSpecial( Aig_Man_t * pPart0, Aig_Man_t * pPart1, int nFrames, int fVerbose )
 {
     extern int Fra_FraigCec( Aig_Man_t ** ppAig, int nConfLimit, int fVerbose );
-    int nFrames = 2;   // modify to enable comparison over any number of frames
+    int iOut, nOuts;
     Aig_Man_t * pMiterCec;
     int RetValue, clkTotal = clock();
+    Aig_ManPrintStats( pPart0 );
+    Aig_ManPrintStats( pPart1 );
+//    Aig_ManDumpBlif( pPart0, "file0.blif", NULL, NULL );
+//    Aig_ManDumpBlif( pPart1, "file1.blif", NULL, NULL );
 //    assert( Aig_ManNodeNum(pPart0) <= Aig_ManNodeNum(pPart1) );
     if ( Aig_ManNodeNum(pPart0) >= Aig_ManNodeNum(pPart1) )
     {
@@ -605,7 +723,6 @@ int Ssw_SecSpecial( Aig_Man_t * pPart0, Aig_Man_t * pPart1, int fVerbose )
     // transfer model if given
 //    if ( pNtk2 == NULL )
 //        pNtk1->pModel = pMiterCec->pData, pMiterCec->pData = NULL;
-    Aig_ManStop( pMiterCec );
     // report the miter
     if ( RetValue == 1 )
     {
@@ -616,6 +733,24 @@ PRT( "Time", clock() - clkTotal );
     {
         printf( "Networks are NOT EQUIVALENT.   " );
 PRT( "Time", clock() - clkTotal );
+        if ( pMiterCec->pData == NULL )
+            printf( "Counter-example is not available.\n" );
+        else
+        {
+            iOut = Ssw_SecCexResimulate( pMiterCec, pMiterCec->pData, &nOuts );
+            if ( iOut == -1 )
+                printf( "Counter-example verification has failed.\n" );
+            else 
+            {
+                if ( iOut < Saig_ManPoNum(pPart0) * nFrames )
+                    printf( "Primary output %d has failed in frame %d.\n", 
+                        iOut%Saig_ManPoNum(pPart0), iOut/Saig_ManPoNum(pPart0) );
+                else
+                    printf( "Flop input %d has failed in the last frame.\n", 
+                        iOut - Saig_ManPoNum(pPart0) * nFrames );
+                printf( "The counter-example detected %d incorrect POs or flop inputs.\n", nOuts );
+            }
+        }
     }
     else
     {
@@ -623,6 +758,7 @@ PRT( "Time", clock() - clkTotal );
 PRT( "Time", clock() - clkTotal );
     }
     fflush( stdout );
+    Aig_ManStop( pMiterCec );
     return RetValue;
 }
 
@@ -639,6 +775,7 @@ PRT( "Time", clock() - clkTotal );
 ***********************************************************************/
 int Ssw_SecSpecialMiter( Aig_Man_t * pMiter, int fVerbose )
 {
+    int nFrames = 2;   // modify to enable comparison over any number of frames
     Aig_Man_t * pPart0, * pPart1;
     int RetValue;
     if ( fVerbose )
@@ -657,7 +794,7 @@ int Ssw_SecSpecialMiter( Aig_Man_t * pMiter, int fVerbose )
 //        Aig_ManDumpBlif( pPart1, "part1.blif", NULL, NULL );
 //        printf( "The result of demitering is written into files \"%s\" and \"%s\".\n", "part0.blif", "part1.blif" );
     }
-    RetValue = Ssw_SecSpecial( pPart0, pPart1, fVerbose );
+    RetValue = Ssw_SecSpecial( pPart0, pPart1, nFrames, fVerbose );
     Aig_ManStop( pPart0 );
     Aig_ManStop( pPart1 );
     return RetValue;
diff --git a/src/aig/saig/saigSynch.c b/src/aig/saig/saigSynch.c
index eb0fefc9..c52f2f48 100644
--- a/src/aig/saig/saigSynch.c
+++ b/src/aig/saig/saigSynch.c
@@ -632,6 +632,7 @@ Aig_Man_t * Saig_Synchronize( Aig_Man_t * pAig1, Aig_Man_t * pAig2, int nWords,
     pAig1z = Saig_ManDupInitZero( pAig1 );
     pAig2z = Saig_ManDupInitZero( pAig2 );
     pMiter = Saig_ManCreateMiter( pAig1z, pAig2z, 0 );
+    Aig_ManCleanup( pMiter );
     Aig_ManStop( pAig1z );
     Aig_ManStop( pAig2z );
 
diff --git a/src/aig/ssw/module.make b/src/aig/ssw/module.make
index a7d940b4..1e79c955 100644
--- a/src/aig/ssw/module.make
+++ b/src/aig/ssw/module.make
@@ -4,6 +4,7 @@ SRC +=    src/aig/ssw/sswAig.c \
     src/aig/ssw/sswCnf.c \
     src/aig/ssw/sswCore.c \
     src/aig/ssw/sswDyn.c \
+    src/aig/ssw/sswIslands.c \
     src/aig/ssw/sswLcorr.c \
     src/aig/ssw/sswMan.c \
     src/aig/ssw/sswPart.c \
diff --git a/src/aig/ssw/ssw.h b/src/aig/ssw/ssw.h
index 73226dbe..4bb2356a 100644
--- a/src/aig/ssw/ssw.h
+++ b/src/aig/ssw/ssw.h
@@ -104,6 +104,7 @@ extern int           Ssw_SecSpecialMiter( Aig_Man_t * pMiter, int fVerbose );
 /*=== sswPart.c ==========================================================*/
 extern Aig_Man_t *   Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars );
 /*=== sswPairs.c ===================================================*/
+extern int           Ssw_MiterStatus( Aig_Man_t * p, int fVerbose );
 extern int           Ssw_SecWithPairs( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Vec_Int_t * vIds1, Vec_Int_t * vIds2, Ssw_Pars_t * pPars );
 extern int           Ssw_SecGeneral( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Ssw_Pars_t * pPars );
 extern int           Ssw_SecGeneralMiter( Aig_Man_t * pMiter, Ssw_Pars_t * pPars );
diff --git a/src/aig/ssw/sswClass.c b/src/aig/ssw/sswClass.c
index f234a58f..3dfee28b 100644
--- a/src/aig/ssw/sswClass.c
+++ b/src/aig/ssw/sswClass.c
@@ -446,7 +446,7 @@ void Ssw_ClassesRemoveNode( Ssw_Cla_t * p, Aig_Obj_t * pObj )
     assert( p->pId2Class[pObj->Id] == NULL );
     pRepr = Aig_ObjRepr( p->pAig, pObj );
     assert( pRepr != NULL );
-    Vec_PtrPush( p->vRefined, pObj );
+//    Vec_PtrPush( p->vRefined, pObj );
     if ( Ssw_ObjIsConst1Cand( p->pAig, pObj ) )
     {
         assert( p->pClassSizes[pRepr->Id] == 0 );
@@ -455,7 +455,7 @@ void Ssw_ClassesRemoveNode( Ssw_Cla_t * p, Aig_Obj_t * pObj )
         p->nCands1--;
         return;
     }
-    Vec_PtrPush( p->vRefined, pRepr );
+//    Vec_PtrPush( p->vRefined, pRepr );
     Aig_ObjSetRepr( p->pAig, pObj, NULL );
     assert( p->pId2Class[pRepr->Id][0] == pRepr );
     assert( p->pClassSizes[pRepr->Id] >= 2 );
@@ -793,6 +793,48 @@ Ssw_Cla_t * Ssw_ClassesPreparePairs( Aig_Man_t * pAig, Vec_Int_t ** pvClasses )
 
 /**Function*************************************************************
 
+  Synopsis    [Creates classes from the temporary representation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ssw_Cla_t * Ssw_ClassesFromIslands( Aig_Man_t * pMiter, Vec_Int_t * vPairs )
+{
+    Ssw_Cla_t * p;
+    Aig_Obj_t ** ppClassNew;
+    Aig_Obj_t * pObj, * pRepr;
+    int i;
+    // start the classes
+    p = Ssw_ClassesStart( pMiter );
+    // allocate memory for classes
+    p->pMemClasses = ALLOC( Aig_Obj_t *, Vec_IntSize(vPairs) );
+    // create classes
+    for ( i = 0; i < Vec_IntSize(vPairs); i += 2 )
+    {
+        pRepr = Aig_ManObj( pMiter, Vec_IntEntry(vPairs, i) );
+        pObj  = Aig_ManObj( pMiter, Vec_IntEntry(vPairs, i+1) );
+        assert( Aig_ObjId(pRepr) < Aig_ObjId(pObj) );
+        Aig_ObjSetRepr( pMiter, pObj, pRepr );
+        // get room for storing the class
+        ppClassNew = p->pMemClasses + i;
+        ppClassNew[0] = pRepr;
+        ppClassNew[1] = pObj;
+        // create new class
+        Ssw_ObjAddClass( p, pRepr, ppClassNew, 2 );
+    }
+    // prepare room for new classes
+    p->pMemClassesFree = NULL;
+    Ssw_ClassesCheck( p );
+//    Ssw_ClassesPrint( p, 0 );
+    return p;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Iteratively refines the classes after simulation.]
 
   Description [Returns the number of refinements performed.]
@@ -820,8 +862,8 @@ int Ssw_ClassesRefineOneClass( Ssw_Cla_t * p, Aig_Obj_t * pReprOld, int fRecursi
     if ( Vec_PtrSize(p->vClassNew) == 0 )
         return 0;
     // remember that this class is refined
-    Ssw_ClassForEachNode( p, pReprOld, pObj, i )
-        Vec_PtrPush( p->vRefined, pObj );
+//    Ssw_ClassForEachNode( p, pReprOld, pObj, i )
+//        Vec_PtrPush( p->vRefined, pObj );
 
     // get the new representative
     pReprNew = Vec_PtrEntry( p->vClassNew, 0 );
@@ -944,7 +986,7 @@ int Ssw_ClassesRefineConst1( Ssw_Cla_t * p, int fRecursive )
             if ( !p->pFuncNodeIsConst( p->pManData, pObj ) )
             {
                 Vec_PtrPush( p->vClassNew, pObj );
-                Vec_PtrPush( p->vRefined, pObj );
+//                Vec_PtrPush( p->vRefined, pObj );
             }
         }
     // check if there is a new class
diff --git a/src/aig/ssw/sswInt.h b/src/aig/ssw/sswInt.h
index 8d8d3265..90c1367f 100644
--- a/src/aig/ssw/sswInt.h
+++ b/src/aig/ssw/sswInt.h
@@ -205,6 +205,7 @@ extern Ssw_Cla_t *   Ssw_ClassesPrepare( Aig_Man_t * pAig, int fLatchCorr, int n
 extern Ssw_Cla_t *   Ssw_ClassesPrepareSimple( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs );
 extern Ssw_Cla_t *   Ssw_ClassesPrepareTargets( Aig_Man_t * pAig );
 extern Ssw_Cla_t *   Ssw_ClassesPreparePairs( Aig_Man_t * pAig, Vec_Int_t ** pvClasses );
+extern Ssw_Cla_t *   Ssw_ClassesFromIslands( Aig_Man_t * pMiter, Vec_Int_t * vPairs );
 extern int           Ssw_ClassesRefine( Ssw_Cla_t * p, int fRecursive );
 extern int           Ssw_ClassesRefineOneClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, int fRecursive );
 extern int           Ssw_ClassesRefineConst1Group( Ssw_Cla_t * p, Vec_Ptr_t * vRoots, int fRecursive );
diff --git a/src/aig/ssw/sswIslands.c b/src/aig/ssw/sswIslands.c
new file mode 100644
index 00000000..5a5783f7
--- /dev/null
+++ b/src/aig/ssw/sswIslands.c
@@ -0,0 +1,382 @@
+/**CFile****************************************************************
+
+  FileName    [sswIslands.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Inductive prover with constraints.]
+
+  Synopsis    [Detection of islands of difference.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - September 1, 2008.]
+
+  Revision    [$Id: sswIslands.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "sswInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static inline Aig_Obj_t *  Aig_ObjChild0Copy2( Aig_Obj_t * pObj )  { return Aig_ObjFanin0(pObj)->pData? Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj)) : NULL;  }
+static inline Aig_Obj_t *  Aig_ObjChild1Copy2( Aig_Obj_t * pObj )  { return Aig_ObjFanin1(pObj)->pData? Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj)) : NULL;  }
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Creates pair of structurally equivalent nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_CreatePair( Vec_Int_t * vPairs, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
+{
+    pObj0->pData = pObj1;
+    pObj1->pData = pObj0;
+    Vec_IntPush( vPairs, pObj0->Id );
+    Vec_IntPush( vPairs, pObj1->Id );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Detects islands of common logic and returns them as pairs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Ssw_DetectIslands( Aig_Man_t * p0, Aig_Man_t * p1, int nCommonFlops, int fVerbose )
+{
+    Vec_Int_t * vPairs;
+    Aig_Obj_t * pObj0, * pObj1, * pFanin0, * pFanin1;
+    int i;
+    assert( Aig_ManRegNum(p0) > 0 );
+    assert( Aig_ManRegNum(p1) > 0 );
+    assert( Aig_ManRegNum(p0) >= nCommonFlops );
+    assert( Aig_ManRegNum(p1) >= nCommonFlops );
+    assert( Saig_ManPiNum(p0) == Saig_ManPiNum(p1) );
+    assert( Saig_ManPoNum(p0) == Saig_ManPoNum(p1) );
+    Aig_ManCleanData( p0 );
+    Aig_ManCleanData( p1 );
+    // start structural equivalence
+    vPairs = Vec_IntAlloc( 1000 );
+    Ssw_CreatePair( vPairs, Aig_ManConst1(p0), Aig_ManConst1(p1) );
+    Saig_ManForEachPi( p0, pObj0, i )
+        Ssw_CreatePair( vPairs, pObj0, Aig_ManPi(p1, i) );
+    Saig_ManForEachLo( p0, pObj0, i )
+    {
+        if ( i == nCommonFlops )
+            break;
+        Ssw_CreatePair( vPairs, pObj0, Saig_ManLo(p1, i) );
+    }
+    // find structurally equivalent nodes
+    Aig_ManForEachNode( p0, pObj0, i )
+    {
+        pFanin0 = Aig_ObjChild0Copy2( pObj0 );
+        pFanin1 = Aig_ObjChild1Copy2( pObj0 );
+        if ( pFanin0 == NULL || pFanin1 == NULL )
+            continue;
+        pObj1 = Aig_TableLookupTwo( p1, pFanin0, pFanin1 );
+        if ( pObj1 == NULL )
+            continue;
+        Ssw_CreatePair( vPairs, pObj0, pObj1 );
+    }
+    return vPairs;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects additional Lis and Los.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_CollectExtraLiLo( Aig_Man_t * p, int nCommonFlops, Vec_Ptr_t * vLis, Vec_Ptr_t * vLos )
+{
+    Aig_Obj_t * pObjLo, * pObjLi;
+    int i;
+    Saig_ManForEachLiLo( p, pObjLo, pObjLi, i )
+    {
+        if ( i < nCommonFlops )
+            continue;
+        Vec_PtrPush( vLis, pObjLi );
+        Vec_PtrPush( vLos, pObjLo );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Overlays and extends the pairs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_OverlayIslands( Aig_Man_t * pTo, Aig_Man_t * pFrom, Vec_Ptr_t * vLisFrom, Vec_Ptr_t * vLosFrom, Vec_Int_t * vPairs, int nCommonFlops, int fToGoesFirst )
+{
+    Aig_Obj_t * pObjFrom, * pObjTo, * pFanin0To, * pFanin1To;
+    int i;
+    // create additional register outputs of From in To
+    Vec_PtrForEachEntry( vLosFrom, pObjFrom, i )
+    {
+        pObjTo = Aig_ObjCreatePi( pTo );
+        if( fToGoesFirst )
+            Ssw_CreatePair( vPairs, pObjTo, pObjFrom );
+        else
+            Ssw_CreatePair( vPairs, pObjFrom, pObjTo );
+    }
+    // create additional nodes of From in To
+    Aig_ManForEachNode( pFrom, pObjFrom, i )
+    {
+        if ( pObjFrom->pData != NULL )
+            continue;
+        pFanin0To = Aig_ObjChild0Copy2( pObjFrom );
+        pFanin1To = Aig_ObjChild1Copy2( pObjFrom );
+        assert( pFanin0To != NULL && pFanin1To != NULL );
+        pObjTo = Aig_And( pTo, pFanin0To, pFanin1To );
+        if( fToGoesFirst )
+            Ssw_CreatePair( vPairs, pObjTo, pObjFrom );
+        else
+            Ssw_CreatePair( vPairs, pObjFrom, pObjTo );
+    }
+    // finally recreate additional register inputs
+    Vec_PtrForEachEntry( vLisFrom, pObjFrom, i )
+    {
+        pFanin0To = Aig_ObjChild0Copy2( pObjFrom );
+        Aig_ObjCreatePo( pTo, pFanin0To );
+    }
+    // update the number of registers
+    Aig_ManSetRegNum( pTo, Aig_ManRegNum(pTo) + Vec_PtrSize(vLisFrom) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Overlays and extends the pairs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Saig_ManMiterWithIslands( Aig_Man_t * p0, Aig_Man_t * p1, Aig_Man_t ** ppMiter, Vec_Int_t * vPairs )
+{
+    Aig_Man_t * pMiter;
+    Vec_Int_t * vPairsNew;
+    Aig_Obj_t * pObj0, * pObj1;
+    int i;
+    vPairsNew = Vec_IntAlloc( 1000 );
+    pMiter = Saig_ManCreateMiter( p0, p1, 0 );
+    for ( i = 0; i < Vec_IntSize(vPairs); i += 2 )
+    {
+        pObj0 = Aig_ManObj( p0, Vec_IntEntry(vPairs, i) );
+        pObj1 = Aig_ManObj( p1, Vec_IntEntry(vPairs, i+1) );
+        pObj0 = pObj0->pData;
+        pObj1 = pObj1->pData;
+        assert( !Aig_IsComplement(pObj0) );
+        assert( !Aig_IsComplement(pObj1) );
+        if ( pObj0 == pObj1 )
+            continue;
+        assert( pObj0->Id < pObj1->Id );
+        Vec_IntPush( vPairsNew, pObj0->Id );
+        Vec_IntPush( vPairsNew, pObj1->Id );
+    }
+    *ppMiter = pMiter;
+    return vPairsNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Solves SEC using structural similarity.]
+
+  Description [Modifies both p0 and p1 by adding extra logic.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Ssw_SecWithIslandsInternal( Aig_Man_t * p0, Aig_Man_t * p1, int nCommonFlops, int fVerbose, Ssw_Pars_t * pPars )
+{
+    Ssw_Man_t * p; 
+    Ssw_Pars_t Pars;
+    Vec_Int_t * vPairs, * vPairsMiter;
+    Aig_Man_t * pMiter, * pAigNew;
+    Vec_Ptr_t * vLis0, * vLos0, * vLis1, * vLos1; 
+    int nNodes, nRegs;
+    assert( Aig_ManRegNum(p0) > 0 );
+    assert( Aig_ManRegNum(p1) > 0 );
+    assert( Aig_ManRegNum(p0) >= nCommonFlops );
+    assert( Aig_ManRegNum(p1) >= nCommonFlops );
+    assert( Saig_ManPiNum(p0) == Saig_ManPiNum(p1) );
+    assert( Saig_ManPoNum(p0) == Saig_ManPoNum(p1) );
+    // derive pairs
+    vPairs = Ssw_DetectIslands( p0, p1, nCommonFlops, fVerbose );
+    if ( fVerbose )
+    {
+        printf( "Original managers:\n" );
+        Aig_ManPrintStats( p0 );
+        Aig_ManPrintStats( p1 );
+        printf( "Detected %d PI pairs, %d LO pairs, and %d node pairs.\n", 
+            Saig_ManPiNum(p0), nCommonFlops, Vec_IntSize(vPairs)/2 - Saig_ManPiNum(p0) - nCommonFlops - 1 );
+    }
+    // complete the manager with islands
+    vLis0 = Vec_PtrAlloc( 100 );
+    vLos0 = Vec_PtrAlloc( 100 );
+    vLis1 = Vec_PtrAlloc( 100 );
+    vLos1 = Vec_PtrAlloc( 100 );
+    Ssw_CollectExtraLiLo( p0, nCommonFlops, vLis0, vLos0 );
+    Ssw_CollectExtraLiLo( p1, nCommonFlops, vLis1, vLos1 );
+
+    nRegs  = Saig_ManRegNum(p0);
+    nNodes = Aig_ManNodeNum(p0);
+    Ssw_OverlayIslands( p0, p1, vLis1, vLos1, vPairs, nCommonFlops, 1 );
+    if ( fVerbose )
+        printf( "Completed p0 with %d registers and %d nodes.\n", 
+            Saig_ManRegNum(p0) - nRegs, Aig_ManNodeNum(p0) - nNodes );   
+    
+    nRegs  = Saig_ManRegNum(p1);
+    nNodes = Aig_ManNodeNum(p1);
+    Ssw_OverlayIslands( p1, p0, vLis0, vLos0, vPairs, nCommonFlops, 0 );
+    if ( fVerbose )
+        printf( "Completed p1 with %d registers and %d nodes.\n", 
+            Saig_ManRegNum(p1) - nRegs, Aig_ManNodeNum(p1) - nNodes );   
+    if ( fVerbose )
+    {
+        printf( "Modified managers:\n" );
+        Aig_ManPrintStats( p0 );
+        Aig_ManPrintStats( p1 );
+    }
+
+    Vec_PtrFree( vLis0 );
+    Vec_PtrFree( vLos0 );
+    Vec_PtrFree( vLis1 );
+    Vec_PtrFree( vLos1 );
+    // create sequential miter
+    vPairsMiter = Saig_ManMiterWithIslands( p0, p1, &pMiter, vPairs );
+    Vec_IntFree( vPairs );
+    // if parameters are not given, create them
+    if ( pPars == NULL )
+        Ssw_ManSetDefaultParams( pPars = &Pars );
+    // start the induction manager
+    p = Ssw_ManCreate( pMiter, pPars );
+    // create equivalence classes using these IDs
+    p->ppClasses = Ssw_ClassesFromIslands( pMiter, vPairsMiter );
+    p->pSml = Ssw_SmlStart( pMiter, 0, 1 + p->pPars->nFramesAddSim, 1 );
+    Ssw_ClassesSetData( p->ppClasses, p->pSml, Ssw_SmlObjHashWord, Ssw_SmlObjIsConstWord, Ssw_SmlObjsAreEqualWord );
+    // perform refinement of classes
+    pAigNew = Ssw_SignalCorrespondenceRefine( p );
+    // cleanup
+    Ssw_ManStop( p );
+    Aig_ManStop( pMiter );
+    Vec_IntFree( vPairsMiter );
+    return pAigNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Solves SEC using structural similarity.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ssw_SecWithIslands( Aig_Man_t * p0, Aig_Man_t * p1, int nCommonFlops, int fVerbose, Ssw_Pars_t * pPars )
+{
+    Aig_Man_t * pAigRes;
+    Aig_Man_t * p0New, * p1New;
+    int RetValue, clk = clock();
+    // try the new AIGs
+//    printf( "Performing verification using structural similarity.\n" );
+    p0New = Aig_ManDupSimple( p0 );
+    p1New = Aig_ManDupSimple( p1 );
+    pAigRes = Ssw_SecWithIslandsInternal( p0New, p1New, nCommonFlops, fVerbose, pPars );
+    Aig_ManStop( p0New );
+    Aig_ManStop( p1New );
+    // report the results
+    RetValue = Ssw_MiterStatus( pAigRes, 1 );
+    if ( RetValue == 1 )
+        printf( "Verification successful.  " );
+    else if ( RetValue == 0 )
+        printf( "Verification failed with a counter-example.  " );
+    else
+        printf( "Verification UNDECIDED. The number of remaining regs = %d (total = %d).  ", 
+            Aig_ManRegNum(pAigRes), Aig_ManRegNum(p0New)+Aig_ManRegNum(p1New) );
+    PRT( "Time", clock() - clk );
+    // cleanup
+    Aig_ManStop( pAigRes );
+    return RetValue;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Solves SEC using structural similarity for the miter.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ssw_SecWithIslandsMiter( Aig_Man_t * pMiter, int nCommonFlops, int fVerbose )
+{
+    Aig_Man_t * pPart0, * pPart1;
+    int RetValue;
+    if ( fVerbose )
+        Aig_ManPrintStats( pMiter );
+    // demiter the miter
+    if ( !Saig_ManDemiterSimpleDiff( pMiter, &pPart0, &pPart1 ) )
+    {
+        printf( "Demitering has failed.\n" );
+        return -1;
+    }
+    if ( fVerbose )
+    {
+//        Aig_ManPrintStats( pPart0 );
+//        Aig_ManPrintStats( pPart1 );
+//        Aig_ManDumpBlif( pPart0, "part0.blif", NULL, NULL );
+//        Aig_ManDumpBlif( pPart1, "part1.blif", NULL, NULL );
+//        printf( "The result of demitering is written into files \"%s\" and \"%s\".\n", "part0.blif", "part1.blif" );
+    }
+    RetValue = Ssw_SecWithIslands( pPart0, pPart1, nCommonFlops, fVerbose, NULL );
+    Aig_ManStop( pPart0 );
+    Aig_ManStop( pPart1 );
+    return RetValue;
+}
+
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/ssw/sswPairs.c b/src/aig/ssw/sswPairs.c
index c77ad30d..1af357f9 100644
--- a/src/aig/ssw/sswPairs.c
+++ b/src/aig/ssw/sswPairs.c
@@ -276,6 +276,7 @@ Aig_Man_t * Ssw_SignalCorrespondenceWithPairs( Aig_Man_t * pAig1, Aig_Man_t * pA
     assert( Vec_IntSize(vIds1) == Vec_IntSize(vIds2) );
     // create sequential miter
     pMiter = Saig_ManCreateMiter( pAig1, pAig2, 0 );
+    Aig_ManCleanup( pMiter );
     // transfer information to the miter
     vPairs = Ssw_TransferSignalPairs( pMiter, pAig1, pAig2, vIds1, vIds2 );
     // create representation of the classes
@@ -413,6 +414,7 @@ int Ssw_SecGeneral( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Ssw_Pars_t * pPars )
     // try the new AIGs
     printf( "Performing general verification without node pairs.\n" );
     pMiter = Saig_ManCreateMiter( pAig1, pAig2, 0 );
+    Aig_ManCleanup( pMiter );
     pAigRes = Ssw_SignalCorrespondence( pMiter, pPars );
     Aig_ManStop( pMiter );
     // report the results