Improving and updating the abstraction code.

15 files changed, 962 insertions, 2076 deletions

diff --git a/abclib.dsp b/abclib.dsp
index f689b4b6..32f161d0 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -3487,7 +3487,15 @@ SOURCE=.\src\aig\saig\saigAbs.c
 # End Source File
 # Begin Source File
 
-SOURCE=.\src\aig\saig\saigAbs2.c
+SOURCE=.\src\aig\saig\saigAbsCba.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\saig\saigAbsPba.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\saig\saigAbsStart.c
 # End Source File
 # Begin Source File
 
@@ -3539,10 +3547,6 @@ SOURCE=.\src\aig\saig\saigOutDec.c
 # End Source File
 # Begin Source File
 
-SOURCE=.\src\aig\saig\saigPba.c
-# End Source File
-# Begin Source File
-
 SOURCE=.\src\aig\saig\saigPhase.c
 # End Source File
 # Begin Source File
@@ -3787,6 +3791,10 @@ SOURCE=.\src\aig\ssw\sswRarity.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\ssw\sswRarity2.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\ssw\sswSat.c
 # End Source File
 # Begin Source File
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 2a8e6664..195abcc9 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -34,6 +34,7 @@
 
 #include "vec.h"
 #include "utilCex.h"
+#include "giaAbs.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                         PARAMETERS                               ///
@@ -195,8 +196,6 @@ extern int Gia_ManSimSimulate( Gia_Man_t * pAig, Gia_ParSim_t * pPars );
 
 
 static inline int          Gia_IntAbs( int n )                    { return (n < 0)? -n : n;                                     }
-//static inline int          Gia_Float2Int( float Val )             { return *((int *)&Val);                                      }
-//static inline float        Gia_Int2Float( int Num )               { return *((float *)&Num);                                    }
 static inline int          Gia_Float2Int( float Val )             { union { int x; float y; } v; v.y = Val; return v.x;         }
 static inline float        Gia_Int2Float( int Num )               { union { int x; float y; } v; v.x = Num; return v.y;         }
 static inline int          Gia_Base2Log( unsigned n )             { int r; if ( n < 2 ) return n; for ( r = 0, n--; n; n >>= 1, r++ ); return r; }
@@ -597,6 +596,12 @@ static inline int         Gia_ObjLutFanin( Gia_Man_t * p, int Id, int i )   { re
 ///                    FUNCTION DECLARATIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+/*=== giaAbs.c ===========================================================*/
+extern void                Gia_ManCexAbstractionStart( Gia_Man_t * p, Gia_ParAbs_t * pPars );
+Gia_Man_t *                Gia_ManCexAbstractionDerive( Gia_Man_t * pGia );
+int                        Gia_ManCexAbstractionRefine( Gia_Man_t * pGia, Abc_Cex_t * pCex, int fTryFour, int fSensePath, int fVerbose );
+extern int                 Gia_ManPbaPerform( Gia_Man_t * pGia, int nFrames, int nConfLimit, int fVerbose );
+extern int                 Gia_ManCbaPerform( Gia_Man_t * pGia, void * pPars );
 /*=== giaAiger.c ===========================================================*/
 extern int                 Gia_FileSize( char * pFileName );
 extern Gia_Man_t *         Gia_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck );
diff --git a/src/aig/gia/giaAbs.c b/src/aig/gia/giaAbs.c
index 7c20851d..7a4e51f4 100644
--- a/src/aig/gia/giaAbs.c
+++ b/src/aig/gia/giaAbs.c
@@ -20,24 +20,14 @@
  
 #include "gia.h"
 #include "giaAig.h"
-#include "giaAbs.h"
 #include "saig.h"
 
-#ifndef _WIN32
-#include <unistd.h>
-#endif
-
 ABC_NAMESPACE_IMPL_START
 
-
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-extern Vec_Int_t * Saig_ManProofAbstractionFlops( Aig_Man_t * p, Gia_ParAbs_t * pPars );
-extern Vec_Int_t * Saig_ManCexAbstractionFlops( Aig_Man_t * p, Gia_ParAbs_t * pPars );
-extern int         Saig_ManCexRefineStep( Aig_Man_t * p, Vec_Int_t * vFlops, Abc_Cex_t * pCex, int fTryFour, int fSensePath, int fVerbose );
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -147,50 +137,6 @@ Gia_Man_t * Gia_ManCexAbstraction( Gia_Man_t * p, Vec_Int_t * vFlops )
 
 /**Function*************************************************************
 
-  Synopsis    [Computes abstracted flops for the manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Int_t * Gia_ManCexAbstractionFlops( Gia_Man_t * p, Gia_ParAbs_t * pPars )
-{
-    Vec_Int_t * vFlops;
-    Aig_Man_t * pNew;
-    pNew = Gia_ManToAig( p, 0 );
-    vFlops = Saig_ManCexAbstractionFlops( pNew, pPars );
-    p->pCexSeq = pNew->pSeqModel; pNew->pSeqModel = NULL;
-    Aig_ManStop( pNew );
-    return vFlops;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes abstracted flops for the manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Int_t * Gia_ManProofAbstractionFlops( Gia_Man_t * p, Gia_ParAbs_t * pPars )
-{
-    Vec_Int_t * vFlops;
-    Aig_Man_t * pNew;
-    pNew = Gia_ManToAig( p, 0 );
-    vFlops = Saig_ManProofAbstractionFlops( pNew, pPars );
-    p->pCexSeq = pNew->pSeqModel; pNew->pSeqModel = NULL;
-    Aig_ManStop( pNew );
-    return vFlops;
-}
-
-/**Function*************************************************************
-
   Synopsis    [Starts abstraction by computing latch map.]
 
   Description []
@@ -200,18 +146,22 @@ Vec_Int_t * Gia_ManProofAbstractionFlops( Gia_Man_t * p, Gia_ParAbs_t * pPars )
   SeeAlso     []
 
 ***********************************************************************/
-void Gia_ManCexAbstractionStart( Gia_Man_t * p, Gia_ParAbs_t * pPars )
+void Gia_ManCexAbstractionStart( Gia_Man_t * pGia, Gia_ParAbs_t * pPars )
 {
     Vec_Int_t * vFlops;
-    if ( p->vFlopClasses != NULL )
+    Aig_Man_t * pNew;
+    if ( pGia->vFlopClasses != NULL )
     {
         printf( "Gia_ManCexAbstractionStart(): Abstraction latch map is present but will be rederived.\n" );
-        Vec_IntFreeP( &p->vFlopClasses );
+        Vec_IntFreeP( &pGia->vFlopClasses );
     }
-    vFlops = Gia_ManCexAbstractionFlops( p, pPars );
+    pNew = Gia_ManToAig( pGia, 0 );
+    vFlops = Saig_ManCexAbstractionFlops( pNew, pPars );
+    pGia->pCexSeq = pNew->pSeqModel; pNew->pSeqModel = NULL;
+    Aig_ManStop( pNew );
     if ( vFlops )
     {
-        p->vFlopClasses = Gia_ManFlops2Classes( p, vFlops );
+        pGia->vFlopClasses = Gia_ManFlops2Classes( pGia, vFlops );
         Vec_IntFree( vFlops );
     }
 }
@@ -278,37 +228,11 @@ int Gia_ManCexAbstractionRefine( Gia_Man_t * pGia, Abc_Cex_t * pCex, int fTryFou
     return -1;
 }
 
-/**Function*************************************************************
-
-  Synopsis    [Starts abstraction by computing latch map.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Gia_ManProofAbstractionStart( Gia_Man_t * pGia, Gia_ParAbs_t * pPars )
-{
-    Vec_Int_t * vFlops;
-    if ( pGia->vFlopClasses != NULL )
-    {
-        printf( "Gia_ManProofAbstractionStart(): Abstraction latch map is present but will be rederived.\n" );
-        Vec_IntFreeP( &pGia->vFlopClasses );
-    }
-    vFlops = Gia_ManProofAbstractionFlops( pGia, pPars );
-    if ( vFlops )
-    {
-        pGia->vFlopClasses = Gia_ManFlops2Classes( pGia, vFlops );
-        Vec_IntFree( vFlops );
-    }
-}
 
 
 /**Function*************************************************************
 
-  Synopsis    [Read flop map.]
+  Synopsis    [Transform flop list into flop map.]
 
   Description []
                
@@ -317,28 +241,19 @@ void Gia_ManProofAbstractionStart( Gia_Man_t * pGia, Gia_ParAbs_t * pPars )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Str_t * Gia_ManReadFile( char * pFileName )
+Vec_Int_t * Gia_ManFlopsSelect( Vec_Int_t * vFlops, Vec_Int_t * vFlopsNew )
 {
-    FILE * pFile;
-    Vec_Str_t * vStr;
-    int c;
-    pFile = fopen( pFileName, "r" );
-    if ( pFile == NULL )
-    {
-        printf( "Cannot open file \"%s\".\n", pFileName );
-        return NULL;
-    }
-    vStr = Vec_StrAlloc( 100 );
-    while ( (c = fgetc(pFile)) != EOF )
-        Vec_StrPush( vStr, (char)c );
-    Vec_StrPush( vStr, '\0' );
-    fclose( pFile );
-    return vStr;
+    Vec_Int_t * vSelected;
+    int i, Entry;
+    vSelected = Vec_IntAlloc( Vec_IntSize(vFlopsNew) );
+    Vec_IntForEachEntry( vFlopsNew, Entry, i )
+        Vec_IntPush( vSelected, Vec_IntEntry(vFlops, Entry) );
+    return vSelected;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Read flop map.]
+  Synopsis    [Derive unrolled timeframes.]
 
   Description []
                
@@ -347,68 +262,45 @@ Vec_Str_t * Gia_ManReadFile( char * pFileName )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Gia_ManReadBinary( char * pFileName, char * pToken )
+int Gia_ManPbaPerform( Gia_Man_t * pGia, int nFrames, int nConfLimit, int fVerbose )
 {
-    Vec_Int_t * vMap = NULL;
-    Vec_Str_t * vStr;
-    char * pStr;
-    int i, Length;
-    vStr = Gia_ManReadFile( pFileName );
-    if ( vStr == NULL )
-        return NULL;
-    pStr = Vec_StrArray( vStr );
-    pStr = strstr( pStr, pToken );
-    if ( pStr != NULL )
+    Gia_Man_t * pAbs;
+    Aig_Man_t * pAig;
+    Vec_Int_t * vFlops, * vFlopsNew, * vSelected;
+    if ( pGia->vFlopClasses == NULL )
     {
-        pStr  += strlen( pToken );
-        vMap   = Vec_IntAlloc( 100 );
-        Length = strlen( pStr );
-        for ( i = 0; i < Length; i++ )
-        {
-            if ( pStr[i] == '0' )
-                Vec_IntPush( vMap, 0 );
-            else if ( pStr[i] == '1' )
-                Vec_IntPush( vMap, 1 );
-            if ( ('a' <= pStr[i] && pStr[i] <= 'z') || 
-                 ('A' <= pStr[i] && pStr[i] <= 'Z') )
-                break;
-        }
+        printf( "Gia_ManPbaPerform(): Abstraction flop map is missing.\n" );
+        return 0;
     }
-    Vec_StrFree( vStr );
-    return vMap;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Read flop map.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
+    // derive abstraction
+    vFlops = Saig_ManClasses2Flops( pGia->vFlopClasses );
+    pAbs = Gia_ManCexAbstraction( pGia, vFlops );
+    // refine abstraction using PBA
+    pAig = Gia_ManToAigSimple( pAbs );
+    Gia_ManStop( pAbs );
+    vFlopsNew = Saig_ManPbaDerive( pAig, nFrames, nConfLimit, fVerbose );
+    Aig_ManStop( pAig );
+    // derive new classes
+    if ( vFlopsNew != NULL )
+    {
+        vSelected = Gia_ManFlopsSelect( vFlops, vFlopsNew );
+        Vec_IntFree( pGia->vFlopClasses );
+        pGia->vFlopClasses = Saig_ManFlops2Classes( Gia_ManRegNum(pGia), vSelected );
+        Vec_IntFree( vSelected );
 
-***********************************************************************/
-int Gia_ManReadInteger( char * pFileName, char * pToken )
-{
-    int Result = -1;
-    Vec_Str_t * vStr;
-    char * pStr;
-    vStr = Gia_ManReadFile( pFileName );
-    if ( vStr == NULL )
-        return -1;
-    pStr = Vec_StrArray( vStr );
-    pStr = strstr( pStr, pToken );
-    if ( pStr != NULL )
-        Result = atoi( pStr + strlen(pToken) );
-    Vec_StrFree( vStr );
-    return Result;
+        Vec_IntFree( vFlopsNew );
+        Vec_IntFree( vFlops );
+        return 1;
+    }
+    Vec_IntFree( vFlops );
+    // found counter-eample for the abstracted model
+    // or exceeded conflict limit
+    return 0;
 }
 
-
 /**Function*************************************************************
 
-  Synopsis    [Starts abstraction by computing latch map.]
+  Synopsis    [Derive unrolled timeframes.]
 
   Description []
                
@@ -417,133 +309,46 @@ int Gia_ManReadInteger( char * pFileName, char * pToken )
   SeeAlso     []
 
 ***********************************************************************/
-void Gia_ManCexAbstractionStartNew( Gia_Man_t * pGia, Gia_ParAbs_t * pPars )
+int Gia_ManCbaPerform( Gia_Man_t * pGia, void * p )
 {
-    char BufTimeOut[100];
-    char BufTimeOutVT[100];
-    char Command[1000];
-    char * pFileNameIn  = "cex_abstr_in_.aig";
-    char * pFileNameOut = "cex_abstr_out_.txt";
-    FILE * pFile;
-    Vec_Int_t * vCex;
-    int RetValue, clk; 
-    if ( pGia->vFlopClasses != NULL )
-    {
-        printf( "Gia_ManCexAbstractionStartNew(): Abstraction latch map is present but will be rederived.\n" );
-        Vec_IntFreeP( &pGia->vFlopClasses );
-    }
-    Gia_WriteAiger( pGia, pFileNameIn, 0, 0 );
-    sprintf( BufTimeOut, "-timeout=%d", pPars->TimeOut );
-    sprintf( BufTimeOutVT, "-vt=%d", pPars->TimeOutVT );
-//ABC switch  =>  cex_abstr switch
-//-cba   =>  <input> <output>
-//-pba   =>  ,bmc -pba-soft <input> <output>
-//-cba-then-pba  =>  -pba-soft <input> <output>
-//-cba-with-pba  =>  -pba <input> <output>
-    if ( pPars->Algo == 0 )
-    {
-        sprintf( Command, "cex_abstr %s %s -depth=%d -stable=%d -confl=%d -bob=%d %s %s %s %s", 
-            pPars->fVerbose? "":"-quiet", 
-            pPars->fVeryVerbose? "-sat-verbosity=1":"", 
-            pPars->nFramesBmc, pPars->nStableMax, pPars->nConfMaxBmc, pPars->nBobPar,
-            pPars->TimeOut? BufTimeOut : "", 
-            pPars->TimeOutVT? BufTimeOutVT : "", 
-            pFileNameIn, pFileNameOut );
-    }
-    else if ( pPars->Algo == 1 )
-    {
-        sprintf( Command, "cex_abstr %s %s -depth=%d -confl=%d -bob=%d ,bmc -pba-soft %s %s %s %s", 
-            pPars->fVerbose? "":"-quiet", 
-            pPars->fVeryVerbose? "-sat-verbosity=1":"", 
-            pPars->nFramesBmc, pPars->nConfMaxBmc, pPars->nBobPar,
-            pPars->TimeOut? BufTimeOut : "", 
-            pPars->TimeOutVT? BufTimeOutVT : "", 
-            pFileNameIn, pFileNameOut );
-    }
-    else if ( pPars->Algo == 2 )
-    {
-        sprintf( Command, "cex_abstr %s %s -depth=%d -stable=%d -confl=%d -bob=%d -pba-soft %s %s %s %s", 
-            pPars->fVerbose? "":"-quiet", 
-            pPars->fVeryVerbose? "-sat-verbosity=1":"", 
-            pPars->nFramesBmc, pPars->nStableMax, pPars->nConfMaxBmc, pPars->nBobPar,
-            pPars->TimeOut? BufTimeOut : "", 
-            pPars->TimeOutVT? BufTimeOutVT : "", 
-            pFileNameIn, pFileNameOut );
-    }
-    else if ( pPars->Algo == 3 )
-    {
-        sprintf( Command, "cex_abstr %s %s -depth=%d -stable=%d -confl=%d -bob=%d -pba %s %s %s %s", 
-            pPars->fVerbose? "":"-quiet", 
-            pPars->fVeryVerbose? "-sat-verbosity=1":"", 
-            pPars->nFramesBmc, pPars->nStableMax, pPars->nConfMaxBmc, pPars->nBobPar,
-            pPars->TimeOut? BufTimeOut : "", 
-            pPars->TimeOutVT? BufTimeOutVT : "", 
-            pFileNameIn, pFileNameOut );
-    }
-    else
-    {
-        printf( "Unnknown option (algo=%d). CBA (algo=0) is assumed.\n", pPars->Algo );
-        sprintf( Command, "cex_abstr %s %s -depth=%d -stable=%d -confl=%d -bob=%d %s %s %s %s", 
-            pPars->fVerbose? "":"-quiet", 
-            pPars->fVeryVerbose? "-sat-verbosity=1":"", 
-            pPars->nFramesBmc, pPars->nStableMax, pPars->nConfMaxBmc, pPars->nBobPar,
-            pPars->TimeOut? BufTimeOut : "", 
-            pPars->TimeOutVT? BufTimeOutVT : "", 
-            pFileNameIn, pFileNameOut );
-    }
-    // run the command
-    printf( "Executing command line \"%s\"\n", Command );
-    clk = clock();
-    RetValue = system( Command );
-    clk = clock() - clk;
-#ifdef WIN32
-    _unlink( pFileNameIn );
-#else
-    unlink( pFileNameIn );
-#endif
-    if ( RetValue == -1 )
-    {
-        fprintf( stdout, "Command \"%s\" did not succeed.\n", Command );
-        return;
-    }
-    // check that the input PostScript file is okay
-    if ( (pFile = fopen( pFileNameOut, "r" )) == NULL )
+    Saig_ParBmc_t * pPars = (Saig_ParBmc_t *)p;
+    Gia_Man_t * pAbs;
+    Aig_Man_t * pAig;
+    Vec_Int_t * vFlops, * vFlopsNew, * vSelected;
+    if ( pGia->vFlopClasses == NULL )
     {
-        fprintf( stdout, "Cannot open intermediate file \"%s\".\n", pFileNameOut );
-        return;
+        printf( "Gia_ManCbaPerform(): Empty abstraction is started.\n" );
+        pGia->vFlopClasses = Vec_IntStart( Gia_ManRegNum(pGia) );
     }
-    fclose( pFile ); 
-    pPars->nFramesDone = Gia_ManReadInteger( pFileNameOut, "depth:" );
-    if ( pPars->nFramesDone == -1 )
-        printf( "Gia_ManCexAbstractionStartNew(): Cannot read the number of frames covered by BMC.\n" );
-    pGia->vFlopClasses = Gia_ManReadBinary( pFileNameOut, "abstraction:" );
-    vCex = Gia_ManReadBinary( pFileNameOut, "counter-example:" );
-    if ( vCex )
+    // derive abstraction
+    vFlops = Saig_ManClasses2Flops( pGia->vFlopClasses );
+    pAbs = Gia_ManCexAbstraction( pGia, vFlops );
+    // refine abstraction using PBA
+    pAig = Gia_ManToAigSimple( pAbs );
+    Gia_ManStop( pAbs );
+    vFlopsNew = Saig_ManCbaPerform( pAig, pPars );
+    Aig_ManStop( pAig );
+    // derive new classes
+    if ( vFlopsNew != NULL )
     {
-        int nFrames = (Vec_IntSize(vCex) - Gia_ManRegNum(pGia)) / Gia_ManPiNum(pGia);
-        int nRemain = (Vec_IntSize(vCex) - Gia_ManRegNum(pGia)) % Gia_ManPiNum(pGia);
-        if ( nRemain != 0 )
-        {
-            printf( "Counter example has a wrong length.\n" );
-        }
-        else
-        {
-            printf( "Problem is satisfiable. Found counter-example in frame %d.  ", nFrames-1 );
-            Abc_PrintTime( 1, "Time", clk );
-            pGia->pCexSeq = Abc_CexCreate( Gia_ManRegNum(pGia), Gia_ManPiNum(pGia), Vec_IntArray(vCex), nFrames-1, 0, 0 );
-            if ( !Gia_ManVerifyCex( pGia, pGia->pCexSeq, 0 ) )
-                Abc_Print( 1, "Generated counter-example is INVALID.\n" );
-            pPars->Status = 0;
-        }
-        Vec_IntFreeP( &vCex );
+//        vSelected = Saig_ManFlopsSelect( vFlops, vFlopsNew );
+        vSelected = NULL;
+        Vec_IntFree( pGia->vFlopClasses );
+        pGia->vFlopClasses = Saig_ManFlops2Classes( Gia_ManRegNum(pGia), vSelected );
+        Vec_IntFree( vSelected );
+
+        Vec_IntFree( vFlopsNew );
+        Vec_IntFree( vFlops );
+        return 1;
     }
-#ifdef WIN32
-    _unlink( pFileNameOut );
-#else
-    unlink( pFileNameOut );
-#endif
+    Vec_IntFree( vFlops );
+    // found counter-eample for the abstracted model
+    // or exceeded conflict limit
+    return 0;
 }
 
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/saig/module.make b/src/aig/saig/module.make
index 454be222..1171bd46 100644
--- a/src/aig/saig/module.make
+++ b/src/aig/saig/module.make
@@ -1,5 +1,7 @@
 SRC +=    src/aig/saig/saigAbs.c \
-    src/aig/saig/saigAbs2.c \
+    src/aig/saig/saigAbsCba.c \
+    src/aig/saig/saigAbsPba.c \
+    src/aig/saig/saigAbsStart.c \
     src/aig/saig/saigBmc.c \
     src/aig/saig/saigBmc2.c \
     src/aig/saig/saigBmc3.c \
@@ -12,7 +14,6 @@ SRC +=    src/aig/saig/saigAbs.c \
     src/aig/saig/saigIoa.c \
     src/aig/saig/saigMiter.c \
     src/aig/saig/saigOutDec.c \
-    src/aig/saig/saigPba.c \
     src/aig/saig/saigPhase.c \
     src/aig/saig/saigRefSat.c \
     src/aig/saig/saigRetFwd.c \
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index 315e3a8a..93375fd8 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -124,13 +124,17 @@ static inline Aig_Obj_t *  Saig_ObjLiToLo( Aig_Man_t * p, Aig_Obj_t * pObj )  {
 ////////////////////////////////////////////////////////////////////////
 ///                    FUNCTION DECLARATIONS                         ///
 ////////////////////////////////////////////////////////////////////////
- 
+
 /*=== sswAbs.c ==========================================================*/
-extern Aig_Man_t *       Saig_ManCexAbstraction( Aig_Man_t * p, Gia_ParAbs_t * pPars );
-/*=== sswAbs2.c ==========================================================*/
-extern Aig_Man_t *       Saig_ManConCexAbstraction( Aig_Man_t * p, Gia_ParAbs_t * pPars );
-/*=== sswPba.c ==========================================================*/
-extern Aig_Man_t *       Saig_ManProofAbstraction( Aig_Man_t * p, Gia_ParAbs_t * pPars );
+extern Vec_Int_t *       Saig_ManClasses2Flops( Vec_Int_t * vFlopClasses );
+extern Vec_Int_t *       Saig_ManFlops2Classes( int nRegs, Vec_Int_t * vFlops );
+/*=== sswAbsCba.c ==========================================================*/
+extern Vec_Int_t *       Saig_ManCbaPerform( Aig_Man_t * pAig, Saig_ParBmc_t * pPars );
+/*=== sswAbsPba.c ==========================================================*/
+extern Vec_Int_t *       Saig_ManPbaDerive( Aig_Man_t * pAig, int nFrames, int nConfLimit, int fVerbose );
+/*=== sswAbsStart.c ==========================================================*/
+extern int               Saig_ManCexRefineStep( Aig_Man_t * p, Vec_Int_t * vFlops, Abc_Cex_t * pCex, int fTryFour, int fSensePath, int fVerbose );
+extern Vec_Int_t *       Saig_ManCexAbstractionFlops( Aig_Man_t * p, Gia_ParAbs_t * pPars );
 /*=== saigBmc.c ==========================================================*/
 extern int               Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fVerbose, int * piFrame, int nCofFanLit );
 extern int               Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite, int * piFrames );
diff --git a/src/aig/saig/saigAbs.c b/src/aig/saig/saigAbs.c
index 3cd508a6..0322361a 100644
--- a/src/aig/saig/saigAbs.c
+++ b/src/aig/saig/saigAbs.c
@@ -6,7 +6,7 @@
 
   PackageName [Sequential AIG package.]
 
-  Synopsis    [Counter-example-based abstraction.]
+  Synopsis    [Intergrated abstraction procedure.]
 
   Author      [Alan Mishchenko]
   
@@ -37,7 +37,7 @@ ABC_NAMESPACE_IMPL_START
 
 /**Function*************************************************************
 
-  Synopsis    [Collects internal nodes in the DFS order.]
+  Synopsis    [Transform flop map into flop list.]
 
   Description []
                
@@ -46,366 +46,36 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
-int Saig_ManFindFirstFlop_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
+Vec_Int_t * Saig_ManClasses2Flops( Vec_Int_t * vFlopClasses )
 {
-    int RetValue;
-    if ( Aig_ObjIsTravIdCurrent(p, pObj) )
-        return -1;
-    Aig_ObjSetTravIdCurrent(p, pObj);
-    if ( Saig_ObjIsPi(p, pObj) )
-        return -1;
-    if ( Saig_ObjIsLo(p, pObj) )
-    {
-        assert( Aig_ObjPioNum(pObj) >= Saig_ManPiNum(p) );
-        return Aig_ObjPioNum(pObj)-Saig_ManPiNum(p);
-    }
-    assert( Aig_ObjIsNode(pObj) );
-    RetValue = Saig_ManFindFirstFlop_rec( p, Aig_ObjFanin0(pObj) );
-    if ( RetValue >= 0 )
-        return RetValue;
-    return Saig_ManFindFirstFlop_rec( p, Aig_ObjFanin1(pObj) );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns the index of the flop that appears in the support.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Saig_ManFindFirstFlop( Aig_Man_t * p )
-{
-    Aig_ManIncrementTravId( p );
-    Aig_ObjSetTravIdCurrent( p, Aig_ManConst1(p) );
-    return Saig_ManFindFirstFlop_rec( p, Aig_ObjFanin0(Aig_ManPo(p, 0)) );
-
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Derive a new counter-example.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Cex_t * Saig_ManCexRemap( Aig_Man_t * p, Aig_Man_t * pAbs, Abc_Cex_t * pCexAbs )
-{
-    Abc_Cex_t * pCex;
-    Aig_Obj_t * pObj;
-    int i, f;
-    if ( !Saig_ManVerifyCex( pAbs, pCexAbs ) )
-        printf( "Saig_ManCexRemap(): The intial counter-example is invalid.\n" );
-    else
-        printf( "Saig_ManCexRemap(): The intial counter-example is correct.\n" );
-    // start the counter-example
-    pCex = Abc_CexAlloc( Aig_ManRegNum(p), Saig_ManPiNum(p), pCexAbs->iFrame+1 );
-    pCex->iFrame = pCexAbs->iFrame;
-    pCex->iPo    = pCexAbs->iPo;
-    // copy the bit data
-    for ( f = 0; f <= pCexAbs->iFrame; f++ )
-    {
-        Saig_ManForEachPi( pAbs, pObj, i )
-        {
-            if ( i == Saig_ManPiNum(p) )
-                break;
-            if ( Aig_InfoHasBit( pCexAbs->pData, pCexAbs->nRegs + pCexAbs->nPis * f + i ) )
-                Aig_InfoSetBit( pCex->pData, pCex->nRegs + pCex->nPis * f + i );
-        }
-    }
-    // verify the counter example
-    if ( !Saig_ManVerifyCex( p, pCex ) )
-    {
-        printf( "Saig_ManCexRemap(): Counter-example is invalid.\n" );
-        Abc_CexFree( pCex );
-        pCex = NULL;
-    }
-    else
-    {
-        printf( "Counter-example verification is successful.\n" );
-        printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). \n", pCex->iPo, pCex->iFrame );
-    }
-    return pCex;
-}
- 
-/**Function*************************************************************
-
-  Synopsis    [Find the first PI corresponding to the flop.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Saig_ManCexFirstFlopPi( Aig_Man_t * p, Aig_Man_t * pAbs )
-{ 
-    Aig_Obj_t * pObj;
-    int i;
-    assert( pAbs->vCiNumsOrig != NULL );
-    Aig_ManForEachPi( p, pObj, i )
-    {
-        if ( Vec_IntEntry(pAbs->vCiNumsOrig, i) >= Saig_ManPiNum(p) )
-            return i;
-    }
-    return -1;
-}
- 
-/**Function*************************************************************
-
-  Synopsis    [Refines abstraction using one step.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Man_t * Saig_ManCexRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlops, int nFrames, int nConfMaxOne, int fUseBdds, int fUseDprove, int fVerbose, int * pnUseStart, int * piRetValue, int * pnFrames )
-{ 
-    extern int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite, int * piFrames );
-    Vec_Int_t * vFlopsNew;
-    int i, Entry, RetValue;
-    *piRetValue = -1;
-    if ( fUseDprove && Aig_ManRegNum(pAbs) > 0 )
-    {
-/*
-        Fra_Sec_t SecPar, * pSecPar = &SecPar;
-        Fra_SecSetDefaultParams( pSecPar );
-        pSecPar->fVerbose       = fVerbose;
-        RetValue = Fra_FraigSec( pAbs, pSecPar, NULL );
-*/
-        Abc_Cex_t * pCex = NULL;
-        Aig_Man_t * pAbsOrpos = Saig_ManDupOrpos( pAbs );
-        Pdr_Par_t Pars, * pPars = &Pars;
-        Pdr_ManSetDefaultParams( pPars );
-        pPars->nTimeOut = 10;
-        pPars->fVerbose = fVerbose;
-        if ( pPars->fVerbose )
-            printf( "Running property directed reachability...\n" );
-        RetValue = Pdr_ManSolve( pAbsOrpos, pPars, &pCex );
-        if ( pCex )
-            pCex->iPo = Saig_ManFindFailedPoCex( pAbs, pCex );
-        Aig_ManStop( pAbsOrpos );
-        pAbs->pSeqModel = pCex;
-        if ( RetValue )
-            *piRetValue = 1;
-
-    }
-    else if ( fUseBdds && (Aig_ManRegNum(pAbs) > 0 && Aig_ManRegNum(pAbs) <= 80) )
-    {
-        Saig_ParBbr_t Pars, * pPars = &Pars;
-        Bbr_ManSetDefaultParams( pPars );
-        pPars->TimeLimit     = 0;
-        pPars->nBddMax       = 1000000;
-        pPars->nIterMax      = nFrames;
-        pPars->fPartition    = 1;
-        pPars->fReorder      = 1;
-        pPars->fReorderImage = 1;
-        pPars->fVerbose      = fVerbose;
-        pPars->fSilent       = 0;
-        RetValue = Aig_ManVerifyUsingBdds( pAbs, pPars );
-        if ( RetValue )
-            *piRetValue = 1;
-    }
-    else 
-    {
-        Saig_BmcPerform( pAbs, pnUseStart? *pnUseStart: 0, nFrames, 2000, 0, nConfMaxOne, 0, fVerbose, 0, pnFrames );
-    }
-    if ( pAbs->pSeqModel == NULL )
-        return NULL;
-    if ( pnUseStart )
-        *pnUseStart = pAbs->pSeqModel->iFrame;
-//    vFlopsNew = Saig_ManExtendCounterExampleTest( pAbs, Saig_ManCexFirstFlopPi(p, pAbs), pAbs->pSeqModel, 1, fVerbose );
-    vFlopsNew = Saig_ManExtendCounterExampleTest3( pAbs, Saig_ManCexFirstFlopPi(p, pAbs), pAbs->pSeqModel, fVerbose );
-    if ( vFlopsNew == NULL )
-        return NULL;
-    if ( Vec_IntSize(vFlopsNew) == 0 )
-    {
-        printf( "Discovered a true counter-example!\n" );
-        p->pSeqModel = Saig_ManCexRemap( p, pAbs, pAbs->pSeqModel );
-        Vec_IntFree( vFlopsNew );
-        *piRetValue = 0;
-        return NULL;
-    }
-    // vFlopsNew contains PI numbers that should be kept in pAbs
-    if ( fVerbose )
-        printf( "Adding %d registers to the abstraction.\n\n", Vec_IntSize(vFlopsNew) );
-    // add to the abstraction
-    Vec_IntForEachEntry( vFlopsNew, Entry, i )
-    {
-        Entry = Vec_IntEntry(pAbs->vCiNumsOrig, Entry);
-        assert( Entry >= Saig_ManPiNum(p) );
-        assert( Entry < Aig_ManPiNum(p) );
-        Vec_IntPush( vFlops, Entry-Saig_ManPiNum(p) );
-    }
-    Vec_IntFree( vFlopsNew );
-
-    Vec_IntSort( vFlops, 0 );
-    Vec_IntForEachEntryStart( vFlops, Entry, i, 1 )
-        assert( Vec_IntEntry(vFlops, i-1) != Entry );
-
-    return Saig_ManDeriveAbstraction( p, vFlops );
-}
- 
-/**Function*************************************************************
-
-  Synopsis    [Refines abstraction using one step.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Saig_ManCexRefineStep( Aig_Man_t * p, Vec_Int_t * vFlops, Abc_Cex_t * pCex, int fTryFour, int fSensePath, int fVerbose )
-{
-    Aig_Man_t * pAbs;
-    Vec_Int_t * vFlopsNew;
-    int i, Entry, clk = clock();
-    pAbs = Saig_ManDeriveAbstraction( p, vFlops );
-    if ( fSensePath )
-        vFlopsNew = Saig_ManExtendCounterExampleTest2( pAbs, Saig_ManCexFirstFlopPi(p, pAbs), pCex, fVerbose );
-    else
-//        vFlopsNew = Saig_ManExtendCounterExampleTest( pAbs, Saig_ManCexFirstFlopPi(p, pAbs), pCex, fTryFour, fVerbose );
-        vFlopsNew = Saig_ManExtendCounterExampleTest3( pAbs, Saig_ManCexFirstFlopPi(p, pAbs), pCex, fVerbose );
-    if ( vFlopsNew == NULL )
-    {
-        Aig_ManStop( pAbs );
-        return 0;
-    }
-    if ( Vec_IntSize(vFlopsNew) == 0 )
-    {
-        printf( "Refinement did not happen. Discovered a true counter-example.\n" );
-        printf( "Remapping counter-example from %d to %d primary inputs.\n", Aig_ManPiNum(pAbs), Aig_ManPiNum(p) );
-        p->pSeqModel = Saig_ManCexRemap( p, pAbs, pCex );
-        Vec_IntFree( vFlopsNew );
-        Aig_ManStop( pAbs );
-        return 0;
-    }
-    if ( fVerbose )
-    {
-        printf( "Adding %d registers to the abstraction.  ", Vec_IntSize(vFlopsNew) );
-        Abc_PrintTime( 0, "Time", clock() - clk );
-    }
-    // vFlopsNew contains PI number that should be kept in pAbs
-    // add to the abstraction
-    Vec_IntForEachEntry( vFlopsNew, Entry, i )
-    {
-        Entry = Vec_IntEntry(pAbs->vCiNumsOrig, Entry);
-        assert( Entry >= Saig_ManPiNum(p) );
-        assert( Entry < Aig_ManPiNum(p) );
-        Vec_IntPush( vFlops, Entry-Saig_ManPiNum(p) );
-    }
-    Vec_IntFree( vFlopsNew );
-    Aig_ManStop( pAbs );
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes the flops to remain after abstraction.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
- 
-***********************************************************************/
-Vec_Int_t * Saig_ManCexAbstractionFlops( Aig_Man_t * p, Gia_ParAbs_t * pPars )
-{
-    int nUseStart = 0;
-    Aig_Man_t * pAbs, * pTemp;
     Vec_Int_t * vFlops;
-    int Iter, clk = clock(), clk2 = clock();//, iFlop;
-    assert( Aig_ManRegNum(p) > 0 );
-    if ( pPars->fVerbose )
-        printf( "Performing counter-example-based refinement.\n" );
-    Aig_ManSetPioNumbers( p );
-    vFlops = Vec_IntStartNatural( 1 );
-/*
-    iFlop = Saig_ManFindFirstFlop( p );
-    assert( iFlop >= 0 );
-    vFlops = Vec_IntAlloc( 1 );
-    Vec_IntPush( vFlops, iFlop );
-*/
-    // create the resulting AIG
-    pAbs = Saig_ManDeriveAbstraction( p, vFlops );
-    if ( !pPars->fVerbose )
-    {
-        printf( "Init : " );
-        Aig_ManPrintStats( pAbs );
-    }
-    printf( "Refining abstraction...\n" );
-    for ( Iter = 0; ; Iter++ )
-    {
-        pTemp = Saig_ManCexRefine( p, pAbs, vFlops, pPars->nFramesBmc, pPars->nConfMaxBmc, pPars->fUseBdds, pPars->fUseDprove, pPars->fVerbose, pPars->fUseStart?&nUseStart:NULL, &pPars->Status, &pPars->nFramesDone );
-        if ( pTemp == NULL )
-        {
-            ABC_FREE( p->pSeqModel );
-            p->pSeqModel = pAbs->pSeqModel;
-            pAbs->pSeqModel = NULL;
-            Aig_ManStop( pAbs );
-            break;
-        }
-        Aig_ManStop( pAbs );
-        pAbs = pTemp;
-        printf( "ITER %4d : ", Iter );
-        if ( !pPars->fVerbose )
-            Aig_ManPrintStats( pAbs );
-        // output the intermediate result of abstraction
-        Ioa_WriteAiger( pAbs, "gabs.aig", 0, 0 );
-//            printf( "Intermediate abstracted model was written into file \"%s\".\n", "gabs.aig" );
-        // check if the ratio is reached
-        if ( 100.0*(Aig_ManRegNum(p)-Aig_ManRegNum(pAbs))/Aig_ManRegNum(p) < 1.0*pPars->nRatio )
-        {
-            printf( "Refinements is stopped because flop reduction is less than %d%%\n", pPars->nRatio );
-            Aig_ManStop( pAbs );
-            pAbs = NULL;
-            Vec_IntFree( vFlops );
-            vFlops = NULL;
-            break;
-        }
-    }
+    int i, Entry;
+    vFlops = Vec_IntAlloc( 100 );
+    Vec_IntForEachEntry( vFlopClasses, Entry, i )
+        if ( Entry )
+            Vec_IntPush( vFlops, i );
     return vFlops;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Performs counter-example-based abstraction.]
+  Synopsis    [Transform flop list into flop map.]
 
   Description []
                
   SideEffects []
 
   SeeAlso     []
- 
+
 ***********************************************************************/
-Aig_Man_t * Saig_ManCexAbstraction( Aig_Man_t * p, Gia_ParAbs_t * pPars )
+Vec_Int_t * Saig_ManFlops2Classes( int nRegs, Vec_Int_t * vFlops )
 {
-    Vec_Int_t * vFlops;
-    Aig_Man_t * pAbs = NULL;
-    vFlops = Saig_ManCexAbstractionFlops( p, pPars );
-    // write the final result
-    if ( vFlops )
-    {
-        pAbs = Saig_ManDeriveAbstraction( p, vFlops );
-        Ioa_WriteAiger( pAbs, "gabs.aig", 0, 0 );
-        printf( "Final abstracted model was written into file \"%s\".\n", "gabs.aig" );
-        Vec_IntFree( vFlops );
-    }
-    return pAbs;
+    Vec_Int_t * vFlopClasses;
+    int i, Entry;
+    vFlopClasses = Vec_IntStart( nRegs );
+    Vec_IntForEachEntry( vFlops, Entry, i )
+        Vec_IntWriteEntry( vFlopClasses, Entry, 1 );
+    return vFlopClasses;
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/saig/saigAbs2.c b/src/aig/saig/saigAbs2.c
deleted file mode 100644
index a4d0f973..00000000
--- a/src/aig/saig/saigAbs2.c
+++ /dev/null
@@ -1,237 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [saigAbs.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Sequential AIG package.]
-
-  Synopsis    [Counter-example-based abstraction with constraints.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: saigAbs.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "saig.h"
-#include "ssw.h"
-#include "fra.h"
-
-ABC_NAMESPACE_IMPL_START
-
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-extern int Saig_ManFindFirstFlop( Aig_Man_t * p );
-extern Aig_Man_t * Saig_ManCexRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlops, 
-    int nFrames, int nConfMaxOne, int fUseBdds, int fUseDprove, int fVerbose, int * pnUseStart, 
-    int * piRetValue, int * pnFrames );
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Returns the array of constraint numbers that are violated.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Int_t * Saig_ManFindViolatedConstrs( Aig_Man_t * p, Abc_Cex_t * pCexAbs )
-{
-    Vec_Int_t * vFailed;
-    Aig_Obj_t * pObj, * pObjRi, * pObjRo;
-    int * pPoMap, i, k, iBit;
-    pPoMap = ABC_CALLOC( int, Saig_ManPoNum(p) );
-    Aig_ManCleanMarkA(p);
-    Saig_ManForEachLo( p, pObj, i )
-        pObj->fMarkA = 0;
-    assert( pCexAbs->nBits == pCexAbs->nRegs + (pCexAbs->iFrame + 1) * pCexAbs->nPis );
-    for ( i = 0; i <= pCexAbs->iFrame; i++ )
-    {
-        iBit = pCexAbs->nRegs + i * pCexAbs->nPis;
-        Saig_ManForEachPi( p, pObj, k )
-            pObj->fMarkA = Aig_InfoHasBit(pCexAbs->pData, iBit++);
-        Aig_ManForEachNode( p, pObj, k )
-            pObj->fMarkA = (Aig_ObjFanin0(pObj)->fMarkA ^ Aig_ObjFaninC0(pObj)) & 
-                           (Aig_ObjFanin1(pObj)->fMarkA ^ Aig_ObjFaninC1(pObj));
-        Aig_ManForEachPo( p, pObj, k )
-            pObj->fMarkA = Aig_ObjFanin0(pObj)->fMarkA ^ Aig_ObjFaninC0(pObj);
-        Saig_ManForEachPo( p, pObj, k )
-            pPoMap[k] |= pObj->fMarkA;
-        Saig_ManForEachLiLo( p, pObjRi, pObjRo, k )
-            pObjRo->fMarkA = pObjRi->fMarkA;
-    }
-    Aig_ManCleanMarkA(p);
-    // collect numbers of failed constraints
-    vFailed = Vec_IntAlloc( Saig_ManPoNum(p) );
-    Saig_ManForEachPo( p, pObj, k )
-        if ( pPoMap[k] )
-            Vec_IntPush( vFailed, k );
-    ABC_FREE( pPoMap );
-    return vFailed;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes the flops to remain after abstraction.]
-
-  Description [Updates the set of included constraints.]
-               
-  SideEffects []
-
-  SeeAlso     []
- 
-***********************************************************************/
-Vec_Int_t * Saig_ManConCexAbstractionFlops( Aig_Man_t * pInit, Gia_ParAbs_t * pPars, Vec_Int_t * vConstrs )
-{
-    int nUseStart = 0;
-    Aig_Man_t * pCur, * pAbs, * pTemp;
-    Vec_Int_t * vFlops, * vFlopsCopy, * vConstrsToAdd;
-    int i, Entry, iFlop, Iter, clk = clock(), clk2 = clock();
-    assert( Aig_ManRegNum(pInit) > 0 );
-    if ( pPars->fVerbose )
-        printf( "Performing counter-example-based refinement with constraints.\n" );
-//    Aig_ManSetPioNumbers( p );
-    // create constrained AIG
-    pCur = Saig_ManDupFoldConstrs( pInit, vConstrs );
-    assert( Saig_ManPoNum(pCur) == 1 );
-    printf( "cur>>> " ); Aig_ManPrintStats( pCur );
-    // start the flop map
-    iFlop = Saig_ManFindFirstFlop( pCur );
-    assert( iFlop >= 0 );
-//    vFlops = Vec_IntStartNatural( 1 );
-    vFlops = Vec_IntAlloc( 1 );
-    Vec_IntPush( vFlops, iFlop );
-    // create the abstraction
-    pAbs = Saig_ManDeriveAbstraction( pCur, vFlops );
-    printf( "abs>>> " ); Aig_ManPrintStats( pAbs );
-    if ( !pPars->fVerbose )
-    {
-        printf( "Init : " );
-        Aig_ManPrintStats( pAbs );
-    }
-    printf( "Refining abstraction...\n" );
-    for ( Iter = 0; ; Iter++ )
-    {
-        while ( 1 )
-        {
-            vFlopsCopy = Vec_IntDup( vFlops );
-            pTemp = Saig_ManCexRefine( pCur, pAbs, vFlops, pPars->nFramesBmc, pPars->nConfMaxBmc, pPars->fUseBdds, pPars->fUseDprove, pPars->fVerbose, pPars->fUseStart?&nUseStart:NULL, &pPars->Status, &pPars->nFramesDone );
-            if ( pTemp == NULL )
-            {
-                Vec_IntFree( vFlopsCopy );
-                break;
-            }
-            vConstrsToAdd = Saig_ManFindViolatedConstrs( pInit, pAbs->pSeqModel );
-            if ( Vec_IntSize(vConstrsToAdd) == 0 )
-            {
-                Vec_IntFree( vConstrsToAdd );
-                Vec_IntFree( vFlopsCopy );
-                break;
-            }
-            // add the constraints to the base set
-            Vec_IntForEachEntry( vConstrsToAdd, Entry, i )
-            {
-//                assert( Vec_IntFind(vConstrs, Entry) == -1 );
-                Vec_IntPushUnique( vConstrs, Entry );
-            }
-            printf( "Adding %3d constraints.  The total is %3d (out of %3d).\n", 
-                Vec_IntSize(vConstrsToAdd), Vec_IntSize(vConstrs), Saig_ManPoNum(pInit)-1 );
-            Vec_IntFree( vConstrsToAdd );
-            // update the current one
-            Aig_ManStop( pCur );
-            pCur = Saig_ManDupFoldConstrs( pInit, vConstrs );
-            printf( "cur>>> " ); Aig_ManPrintStats( pCur );
-            // update the flop map
-            Vec_IntFree( vFlops );
-            vFlops = vFlopsCopy;
-//            Vec_IntFree( vFlopsCopy );
-//            vFlops = vFlops;
-            // update abstraction
-            Aig_ManStop( pAbs );
-            pAbs = Saig_ManDeriveAbstraction( pCur, vFlops );
-            printf( "abs>>> " ); Aig_ManPrintStats( pAbs );
-        }
-        Aig_ManStop( pAbs );
-        if ( pTemp == NULL )
-            break;
-        pAbs = pTemp;
-        printf( "ITER %4d : ", Iter );
-        if ( !pPars->fVerbose )
-            Aig_ManPrintStats( pAbs );
-        // output the intermediate result of abstraction
-        Ioa_WriteAiger( pAbs, "gabs.aig", 0, 0 );
-//            printf( "Intermediate abstracted model was written into file \"%s\".\n", "gabs.aig" );
-        // check if the ratio is reached
-        if ( 100.0*(Aig_ManRegNum(pCur)-Aig_ManRegNum(pAbs))/Aig_ManRegNum(pCur) < 1.0*pPars->nRatio )
-        {
-            printf( "Refinements is stopped because flop reduction is less than %d%%\n", pPars->nRatio );
-            Aig_ManStop( pAbs );
-            pAbs = NULL;
-            Vec_IntFree( vFlops );
-            vFlops = NULL;
-            break;
-        }
-    }
-    ABC_FREE( pInit->pSeqModel );
-    pInit->pSeqModel = pCur->pSeqModel;
-    pCur->pSeqModel = NULL;
-    Aig_ManStop( pCur );
-    return vFlops;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs counter-example-based abstraction.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
- 
-***********************************************************************/
-Aig_Man_t * Saig_ManConCexAbstraction( Aig_Man_t * p, Gia_ParAbs_t * pPars )
-{
-    Vec_Int_t * vFlops, * vConstrs;
-    Aig_Man_t * pCur, * pAbs = NULL;
-    assert( Saig_ManPoNum(p) > 1 ); // should contain constraint outputs
-    // start included constraints
-    vConstrs = Vec_IntAlloc( 100 );
-    // perform refinement
-    vFlops = Saig_ManConCexAbstractionFlops( p, pPars, vConstrs );
-    // write the final result
-    if ( vFlops )
-    {
-        pCur = Saig_ManDupFoldConstrs( p, vConstrs );
-        pAbs = Saig_ManDeriveAbstraction( pCur, vFlops );
-        Aig_ManStop( pCur );
-
-        Ioa_WriteAiger( pAbs, "gabs.aig", 0, 0 );
-        printf( "Final abstracted model was written into file \"%s\".\n", "gabs.aig" );
-        Vec_IntFree( vFlops );
-    }
-    Vec_IntFree( vConstrs );
-    return pAbs;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
-ABC_NAMESPACE_IMPL_END
-
diff --git a/src/aig/saig/saigAbsCba.c b/src/aig/saig/saigAbsCba.c
new file mode 100644
index 00000000..e14c5e8e
--- /dev/null
+++ b/src/aig/saig/saigAbsCba.c
@@ -0,0 +1,56 @@
+/**CFile****************************************************************
+
+  FileName    [saigAbsCba.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Sequential AIG package.]
+
+  Synopsis    [CEX-based abstraction.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: saigAbsCba.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "saig.h"
+#include "giaAig.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Derive unrolled timeframes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Saig_ManCbaPerform( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
+{
+    return 0;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/saig/saigAbsPba.c b/src/aig/saig/saigAbsPba.c
new file mode 100644
index 00000000..75f38d6c
--- /dev/null
+++ b/src/aig/saig/saigAbsPba.c
@@ -0,0 +1,259 @@
+/**CFile****************************************************************
+
+  FileName    [saigAbsPba.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Sequential AIG package.]
+
+  Synopsis    [Proof-based abstraction.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: saigAbsPba.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "saig.h"
+#include "cnf.h"
+#include "satSolver.h"
+#include "giaAig.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Collect nodes in the unrolled timeframes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Saig_ManUnrollForPba_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * vObjs, Vec_Int_t * vRoots )
+{
+    if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
+        return;
+    Aig_ObjSetTravIdCurrent(pAig, pObj);
+    if ( Aig_ObjIsPo(pObj) )
+        Saig_ManUnrollForPba_rec( pAig, Aig_ObjFanin0(pObj), vObjs, vRoots );
+    else if ( Aig_ObjIsNode(pObj) )
+    {
+        Saig_ManUnrollForPba_rec( pAig, Aig_ObjFanin0(pObj), vObjs, vRoots );
+        Saig_ManUnrollForPba_rec( pAig, Aig_ObjFanin1(pObj), vObjs, vRoots );
+    }
+    if ( vRoots && Saig_ObjIsLo( pAig, pObj ) )
+        Vec_IntPush( vRoots, Aig_ObjId( Saig_ObjLoToLi(pAig, pObj) ) );
+    Vec_IntPush( vObjs, Aig_ObjId(pObj) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives unrolled timeframes for PBA.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+ 
+***********************************************************************/
+Aig_Man_t * Saig_ManUnrollForPba( Aig_Man_t * pAig, int nFrames )
+{
+    Aig_Man_t * pFrames;     // unrolled timeframes
+    Vec_Vec_t * vFrameCos;   // the list of COs per frame
+    Vec_Vec_t * vFrameObjs;  // the list of objects per frame
+    Vec_Int_t * vRoots, * vObjs;
+    Aig_Obj_t * pObj, * pObjNew;
+    int i, f;
+    // collect COs and Objs visited in each frame
+    vFrameCos  = Vec_VecStart( nFrames );
+    vFrameObjs = Vec_VecStart( nFrames );
+    for ( f = nFrames-1; f >= 0; f-- )
+    {
+        // add POs of this frame
+        vRoots = (Vec_Int_t *)Vec_VecEntry( vFrameCos, f );
+        Saig_ManForEachPo( pAig, pObj, i )
+            Vec_IntPush( vRoots, Aig_ObjId(pObj) );
+        // collect nodes starting from the roots
+        Aig_ManIncrementTravId( pAig );
+        Aig_ManForEachNodeVec( pAig, vRoots, pObj, i )
+            Saig_ManUnrollForPba_rec( pAig, pObj, 
+                (Vec_Int_t *)Vec_VecEntry( vFrameObjs, f ),
+                (Vec_Int_t *)(f ? Vec_VecEntry(vFrameCos, f-1) : NULL) );
+    }
+    // derive unrolled timeframes
+    pFrames = Aig_ManStart( 10000 );
+    pFrames->pName = Aig_UtilStrsav( pAig->pName );
+    pFrames->pSpec = Aig_UtilStrsav( pAig->pSpec );
+    // create activation variables
+    Saig_ManForEachLo( pAig, pObj, i )
+        Aig_ObjCreatePi( pFrames );
+    // initialize the flops 
+    Saig_ManForEachLo( pAig, pObj, i )
+        pObj->pData = Aig_Mux( pFrames, Aig_ManPi(pFrames,i), Aig_ObjCreatePi(pFrames), Aig_ManConst0(pFrames) );
+    // iterate through the frames
+    pObjNew = Aig_ManConst0(pFrames);
+    for ( f = 0; f < nFrames; f++ )
+    {
+        // construct
+        vObjs = (Vec_Int_t *)Vec_VecEntry( vFrameObjs, f );
+        Aig_ManForEachNodeVec( pAig, vObjs, pObj, i )
+        {
+            if ( Aig_ObjIsNode(pObj) )
+                pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+            else if ( Aig_ObjIsPo(pObj) )
+                pObj->pData = Aig_ObjChild0Copy(pObj);
+            else if ( Saig_ObjIsPi(pAig, pObj) )
+                pObj->pData = Aig_ObjCreatePi( pFrames );
+            else if ( Aig_ObjIsConst1(pObj) )
+                pObj->pData = Aig_ManConst1(pFrames);
+            else if ( !Saig_ObjIsLo(pAig, pObj) )
+                assert( 0 );
+        }
+        // create output
+        Saig_ManForEachPo( pAig, pObj, i )
+            pObjNew = Aig_Or( pFrames, pObjNew, pObj->pData );
+        // transfer
+        if ( f == nFrames - 1 )
+            break;
+        vRoots = (Vec_Int_t *)Vec_VecEntry( vFrameCos, f );
+        Aig_ManForEachNodeVec( pAig, vRoots, pObj, i )
+        {
+            if ( Saig_ObjIsLi(pAig, pObj) )
+            {
+                int iFlopNum = Aig_ObjPioNum(pObj) - Saig_ManPoNum(pAig);
+                assert( iFlopNum >= 0 && iFlopNum < Aig_ManRegNum(pAig) );
+                Saig_ObjLiToLo(pAig, pObj)->pData = Aig_Mux( pFrames, Aig_ManPi(pFrames,iFlopNum), Aig_ObjCreatePi(pFrames), pObj->pData );
+            }
+        }
+    }
+    // cleanup
+    Vec_VecFree( vFrameCos );
+    Vec_VecFree( vFrameObjs );
+    // create output
+    Aig_ObjCreatePo( pFrames, pObjNew );
+    Aig_ManSetRegNum( pFrames, 0 );
+    // finallize
+    Aig_ManCleanup( pFrames );
+    return pFrames;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derive unrolled timeframes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Saig_ManPbaDerive( Aig_Man_t * pAig, int nFrames, int nConfLimit, int fVerbose )
+{
+    Vec_Int_t * vFlops, * vMapVar2FF, * vAssumps;
+    Aig_Man_t * pFrames;
+    sat_solver * pSat;
+    Cnf_Dat_t * pCnf;
+    Aig_Obj_t * pObj;
+    int nCoreLits, * pCoreLits;
+    int i, iVar, RetValue, clk;
+
+    // create SAT solver
+clk = clock();
+    pFrames = Saig_ManUnrollForPba( pAig, nFrames );
+if ( fVerbose )
+Aig_ManPrintStats( pFrames );
+    pCnf = Cnf_DeriveSimple( pFrames, 0 );
+    pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
+    if ( pSat == NULL )
+    {
+        Aig_ManStop( pFrames );
+        Cnf_DataFree( pCnf );
+        return NULL;
+    }
+if ( fVerbose )
+Abc_PrintTime( 1, "Preparing", clock() - clk );
+
+    // map activation variables into flop numbers
+    vAssumps = Vec_IntAlloc( Aig_ManRegNum(pAig) );
+    vMapVar2FF = Vec_IntStartFull( pCnf->nVars );
+    Aig_ManForEachPi( pFrames, pObj, i )
+    {
+        if ( i >= Aig_ManRegNum(pAig) )
+            break;
+        iVar = pCnf->pVarNums[Aig_ObjId(pObj)];
+        Vec_IntPush( vAssumps, toLitCond(iVar, 1) );
+        Vec_IntWriteEntry( vMapVar2FF, iVar, i );
+    }
+
+    // run SAT solver
+clk = clock();
+    RetValue = sat_solver_solve( pSat, Vec_IntArray(vAssumps), Vec_IntArray(vAssumps) + Vec_IntSize(vAssumps), 
+        (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
+if ( fVerbose )
+Abc_PrintTime( 1, "Solving", clock() - clk );
+    if ( RetValue != l_False )
+    {
+        if ( RetValue == l_True )
+            printf( "Saig_ManPerformPba(): Internal Error!!! The resulting problem is SAT.\n" );
+        else
+            printf( "Saig_ManPerformPba(): SAT solver timed out.\n" );
+        Vec_IntFree( vAssumps );
+        Vec_IntFree( vMapVar2FF );
+        sat_solver_delete( pSat );
+        Aig_ManStop( pFrames );
+        Cnf_DataFree( pCnf );
+        return NULL;
+    }
+    assert( RetValue == l_False ); // UNSAT
+
+    // get relevant SAT literals
+    nCoreLits = sat_solver_final( pSat, &pCoreLits );
+    assert( nCoreLits > 0 );
+    if ( fVerbose )
+        printf( "AnalizeFinal selected %d assumptions (out of %d). Conflicts = %d.\n", 
+            nCoreLits, Vec_IntSize(vAssumps), (int)pSat->stats.conflicts );
+
+    // collect flops
+    vFlops = Vec_IntAlloc( nCoreLits );
+    for ( i = 0; i < nCoreLits; i++ )
+    {
+        iVar = Vec_IntEntry( vMapVar2FF, lit_var(pCoreLits[i]) );
+        assert( iVar >= 0 && iVar < Aig_ManRegNum(pAig) );
+        Vec_IntPush( vFlops, iVar );
+    }
+    Vec_IntSort( vFlops, 0 );
+
+    // cleanup
+    Vec_IntFree( vAssumps );
+    Vec_IntFree( vMapVar2FF );
+    sat_solver_delete( pSat );
+    Cnf_DataFree( pCnf );
+    Aig_ManStop( pFrames );
+    return vFlops;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/saig/saigAbsStart.c b/src/aig/saig/saigAbsStart.c
new file mode 100644
index 00000000..6ec2c21d
--- /dev/null
+++ b/src/aig/saig/saigAbsStart.c
@@ -0,0 +1,341 @@
+/**CFile****************************************************************
+
+  FileName    [saigAbsStart.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Sequential AIG package.]
+
+  Synopsis    [Counter-example-based abstraction.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: saigAbsStart.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "saig.h"
+#include "ssw.h"
+#include "fra.h"
+#include "bbr.h"
+#include "pdr.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Find the first PI corresponding to the flop.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Saig_ManCexFirstFlopPi( Aig_Man_t * p, Aig_Man_t * pAbs )
+{ 
+    Aig_Obj_t * pObj;
+    int i;
+    assert( pAbs->vCiNumsOrig != NULL );
+    Aig_ManForEachPi( p, pObj, i )
+    {
+        if ( Vec_IntEntry(pAbs->vCiNumsOrig, i) >= Saig_ManPiNum(p) )
+            return i;
+    }
+    return -1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derive a new counter-example.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Cex_t * Saig_ManCexRemap( Aig_Man_t * p, Aig_Man_t * pAbs, Abc_Cex_t * pCexAbs )
+{
+    Abc_Cex_t * pCex;
+    Aig_Obj_t * pObj;
+    int i, f;
+    if ( !Saig_ManVerifyCex( pAbs, pCexAbs ) )
+        printf( "Saig_ManCexRemap(): The intial counter-example is invalid.\n" );
+    else
+        printf( "Saig_ManCexRemap(): The intial counter-example is correct.\n" );
+    // start the counter-example
+    pCex = Abc_CexAlloc( Aig_ManRegNum(p), Saig_ManPiNum(p), pCexAbs->iFrame+1 );
+    pCex->iFrame = pCexAbs->iFrame;
+    pCex->iPo    = pCexAbs->iPo;
+    // copy the bit data
+    for ( f = 0; f <= pCexAbs->iFrame; f++ )
+    {
+        Saig_ManForEachPi( pAbs, pObj, i )
+        {
+            if ( i == Saig_ManPiNum(p) )
+                break;
+            if ( Aig_InfoHasBit( pCexAbs->pData, pCexAbs->nRegs + pCexAbs->nPis * f + i ) )
+                Aig_InfoSetBit( pCex->pData, pCex->nRegs + pCex->nPis * f + i );
+        }
+    }
+    // verify the counter example
+    if ( !Saig_ManVerifyCex( p, pCex ) )
+    {
+        printf( "Saig_ManCexRemap(): Counter-example is invalid.\n" );
+        Abc_CexFree( pCex );
+        pCex = NULL;
+    }
+    else
+    {
+        printf( "Counter-example verification is successful.\n" );
+        printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). \n", pCex->iPo, pCex->iFrame );
+    }
+    return pCex;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Refines abstraction using one step.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManCexRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlops, int nFrames, int nConfMaxOne, int fUseBdds, int fUseDprove, int fVerbose, int * pnUseStart, int * piRetValue, int * pnFrames )
+{ 
+    extern int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite, int * piFrames );
+    Vec_Int_t * vFlopsNew;
+    int i, Entry, RetValue;
+    *piRetValue = -1;
+    if ( fUseDprove && Aig_ManRegNum(pAbs) > 0 )
+    {
+/*
+        Fra_Sec_t SecPar, * pSecPar = &SecPar;
+        Fra_SecSetDefaultParams( pSecPar );
+        pSecPar->fVerbose       = fVerbose;
+        RetValue = Fra_FraigSec( pAbs, pSecPar, NULL );
+*/
+        Abc_Cex_t * pCex = NULL;
+        Aig_Man_t * pAbsOrpos = Saig_ManDupOrpos( pAbs );
+        Pdr_Par_t Pars, * pPars = &Pars;
+        Pdr_ManSetDefaultParams( pPars );
+        pPars->nTimeOut = 10;
+        pPars->fVerbose = fVerbose;
+        if ( pPars->fVerbose )
+            printf( "Running property directed reachability...\n" );
+        RetValue = Pdr_ManSolve( pAbsOrpos, pPars, &pCex );
+        if ( pCex )
+            pCex->iPo = Saig_ManFindFailedPoCex( pAbs, pCex );
+        Aig_ManStop( pAbsOrpos );
+        pAbs->pSeqModel = pCex;
+        if ( RetValue )
+            *piRetValue = 1;
+
+    }
+    else if ( fUseBdds && (Aig_ManRegNum(pAbs) > 0 && Aig_ManRegNum(pAbs) <= 80) )
+    {
+        Saig_ParBbr_t Pars, * pPars = &Pars;
+        Bbr_ManSetDefaultParams( pPars );
+        pPars->TimeLimit     = 0;
+        pPars->nBddMax       = 1000000;
+        pPars->nIterMax      = nFrames;
+        pPars->fPartition    = 1;
+        pPars->fReorder      = 1;
+        pPars->fReorderImage = 1;
+        pPars->fVerbose      = fVerbose;
+        pPars->fSilent       = 0;
+        RetValue = Aig_ManVerifyUsingBdds( pAbs, pPars );
+        if ( RetValue )
+            *piRetValue = 1;
+    }
+    else 
+    {
+        Saig_BmcPerform( pAbs, pnUseStart? *pnUseStart: 0, nFrames, 2000, 0, nConfMaxOne, 0, fVerbose, 0, pnFrames );
+    }
+    if ( pAbs->pSeqModel == NULL )
+        return NULL;
+    if ( pnUseStart )
+        *pnUseStart = pAbs->pSeqModel->iFrame;
+//    vFlopsNew = Saig_ManExtendCounterExampleTest( pAbs, Saig_ManCexFirstFlopPi(p, pAbs), pAbs->pSeqModel, 1, fVerbose );
+    vFlopsNew = Saig_ManExtendCounterExampleTest3( pAbs, Saig_ManCexFirstFlopPi(p, pAbs), pAbs->pSeqModel, fVerbose );
+    if ( vFlopsNew == NULL )
+        return NULL;
+    if ( Vec_IntSize(vFlopsNew) == 0 )
+    {
+        printf( "Discovered a true counter-example!\n" );
+        p->pSeqModel = Saig_ManCexRemap( p, pAbs, pAbs->pSeqModel );
+        Vec_IntFree( vFlopsNew );
+        *piRetValue = 0;
+        return NULL;
+    }
+    // vFlopsNew contains PI numbers that should be kept in pAbs
+    if ( fVerbose )
+        printf( "Adding %d registers to the abstraction.\n\n", Vec_IntSize(vFlopsNew) );
+    // add to the abstraction
+    Vec_IntForEachEntry( vFlopsNew, Entry, i )
+    {
+        Entry = Vec_IntEntry(pAbs->vCiNumsOrig, Entry);
+        assert( Entry >= Saig_ManPiNum(p) );
+        assert( Entry < Aig_ManPiNum(p) );
+        Vec_IntPush( vFlops, Entry-Saig_ManPiNum(p) );
+    }
+    Vec_IntFree( vFlopsNew );
+
+    Vec_IntSort( vFlops, 0 );
+    Vec_IntForEachEntryStart( vFlops, Entry, i, 1 )
+        assert( Vec_IntEntry(vFlops, i-1) != Entry );
+
+    return Saig_ManDeriveAbstraction( p, vFlops );
+}
+ 
+/**Function*************************************************************
+
+  Synopsis    [Refines abstraction using one step.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Saig_ManCexRefineStep( Aig_Man_t * p, Vec_Int_t * vFlops, Abc_Cex_t * pCex, int fTryFour, int fSensePath, int fVerbose )
+{
+    Aig_Man_t * pAbs;
+    Vec_Int_t * vFlopsNew;
+    int i, Entry, clk = clock();
+    pAbs = Saig_ManDeriveAbstraction( p, vFlops );
+    if ( fSensePath )
+        vFlopsNew = Saig_ManExtendCounterExampleTest2( pAbs, Saig_ManCexFirstFlopPi(p, pAbs), pCex, fVerbose );
+    else
+//        vFlopsNew = Saig_ManExtendCounterExampleTest( pAbs, Saig_ManCexFirstFlopPi(p, pAbs), pCex, fTryFour, fVerbose );
+        vFlopsNew = Saig_ManExtendCounterExampleTest3( pAbs, Saig_ManCexFirstFlopPi(p, pAbs), pCex, fVerbose );
+    if ( vFlopsNew == NULL )
+    {
+        Aig_ManStop( pAbs );
+        return 0;
+    }
+    if ( Vec_IntSize(vFlopsNew) == 0 )
+    {
+        printf( "Refinement did not happen. Discovered a true counter-example.\n" );
+        printf( "Remapping counter-example from %d to %d primary inputs.\n", Aig_ManPiNum(pAbs), Aig_ManPiNum(p) );
+        p->pSeqModel = Saig_ManCexRemap( p, pAbs, pCex );
+        Vec_IntFree( vFlopsNew );
+        Aig_ManStop( pAbs );
+        return 0;
+    }
+    if ( fVerbose )
+    {
+        printf( "Adding %d registers to the abstraction.  ", Vec_IntSize(vFlopsNew) );
+        Abc_PrintTime( 0, "Time", clock() - clk );
+    }
+    // vFlopsNew contains PI number that should be kept in pAbs
+    // add to the abstraction
+    Vec_IntForEachEntry( vFlopsNew, Entry, i )
+    {
+        Entry = Vec_IntEntry(pAbs->vCiNumsOrig, Entry);
+        assert( Entry >= Saig_ManPiNum(p) );
+        assert( Entry < Aig_ManPiNum(p) );
+        Vec_IntPush( vFlops, Entry-Saig_ManPiNum(p) );
+    }
+    Vec_IntFree( vFlopsNew );
+    Aig_ManStop( pAbs );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the flops to remain after abstraction.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+ 
+***********************************************************************/
+Vec_Int_t * Saig_ManCexAbstractionFlops( Aig_Man_t * p, Gia_ParAbs_t * pPars )
+{
+    int nUseStart = 0;
+    Aig_Man_t * pAbs, * pTemp;
+    Vec_Int_t * vFlops;
+    int Iter, clk = clock(), clk2 = clock();//, iFlop;
+    assert( Aig_ManRegNum(p) > 0 );
+    if ( pPars->fVerbose )
+        printf( "Performing counter-example-based refinement.\n" );
+    Aig_ManSetPioNumbers( p );
+    vFlops = Vec_IntStartNatural( 1 );
+/*
+    iFlop = Saig_ManFindFirstFlop( p );
+    assert( iFlop >= 0 );
+    vFlops = Vec_IntAlloc( 1 );
+    Vec_IntPush( vFlops, iFlop );
+*/
+    // create the resulting AIG
+    pAbs = Saig_ManDeriveAbstraction( p, vFlops );
+    if ( !pPars->fVerbose )
+    {
+        printf( "Init : " );
+        Aig_ManPrintStats( pAbs );
+    }
+    printf( "Refining abstraction...\n" );
+    for ( Iter = 0; ; Iter++ )
+    {
+        pTemp = Saig_ManCexRefine( p, pAbs, vFlops, pPars->nFramesBmc, pPars->nConfMaxBmc, pPars->fUseBdds, pPars->fUseDprove, pPars->fVerbose, pPars->fUseStart?&nUseStart:NULL, &pPars->Status, &pPars->nFramesDone );
+        if ( pTemp == NULL )
+        {
+            ABC_FREE( p->pSeqModel );
+            p->pSeqModel = pAbs->pSeqModel;
+            pAbs->pSeqModel = NULL;
+            Aig_ManStop( pAbs );
+            break;
+        }
+        Aig_ManStop( pAbs );
+        pAbs = pTemp;
+        printf( "ITER %4d : ", Iter );
+        if ( !pPars->fVerbose )
+            Aig_ManPrintStats( pAbs );
+        // output the intermediate result of abstraction
+        Ioa_WriteAiger( pAbs, "gabs.aig", 0, 0 );
+//            printf( "Intermediate abstracted model was written into file \"%s\".\n", "gabs.aig" );
+        // check if the ratio is reached
+        if ( 100.0*(Aig_ManRegNum(p)-Aig_ManRegNum(pAbs))/Aig_ManRegNum(p) < 1.0*pPars->nRatio )
+        {
+            printf( "Refinements is stopped because flop reduction is less than %d%%\n", pPars->nRatio );
+            Aig_ManStop( pAbs );
+            pAbs = NULL;
+            Vec_IntFree( vFlops );
+            vFlops = NULL;
+            break;
+        }
+    }
+    return vFlops;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/saig/saigPba.c b/src/aig/saig/saigPba.c
deleted file mode 100644
index 65b39fc0..00000000
--- a/src/aig/saig/saigPba.c
+++ /dev/null
@@ -1,752 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [saigPba.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Sequential AIG package.]
-
-  Synopsis    [Proof-based abstraction.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: saigPba.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "saig.h"
-
-#include "cnf.h"
-#include "satSolver.h"
-#include "satStore.h"
-#include "ssw.h"
-#include "ioa.h"
-#include "fra.h"
-
-ABC_NAMESPACE_IMPL_START
-
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-static inline char Saig_AbsVisited( Vec_Str_t * p, int nObjs, Aig_Obj_t * pObj, int i )    { return Vec_StrGetEntry( p, nObjs*i+pObj->Id );    }
-static inline void Saig_AbsSetVisited( Vec_Str_t * p, int nObjs, Aig_Obj_t * pObj, int i ) { Vec_StrSetEntry( p, nObjs*i+pObj->Id, (char)1 );  }
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Finds the set of clauses involved in the UNSAT core.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Int_t * Saig_AbsSolverUnsatCore( sat_solver * pSat, int nConfMax, int fVerbose, int * piRetValue )
-{
-    Vec_Int_t * vCore;
-    void * pSatCnf; 
-    Intp_Man_t * pManProof;
-    int RetValue, clk = clock();
-    *piRetValue = -1;
-    // solve the problem
-    RetValue = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfMax, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
-    if ( RetValue == l_Undef )
-    {
-        printf( "Conflict limit is reached.\n" );
-        return NULL;
-    }
-    if ( RetValue == l_True )
-    {
-        printf( "The BMC problem is SAT.\n" );
-        *piRetValue = 0;
-        return NULL;
-    }
-    if ( fVerbose )
-    {
-        printf( "SAT solver returned UNSAT after %d conflicts.  ", pSat->stats.conflicts );
-        ABC_PRT( "Time", clock() - clk );
-    }
-    assert( RetValue == l_False );
-    pSatCnf = sat_solver_store_release( pSat ); 
-    // derive the UNSAT core
-    clk = clock();
-    pManProof = Intp_ManAlloc();
-    vCore = (Vec_Int_t *)Intp_ManUnsatCore( pManProof, (Sto_Man_t *)pSatCnf, 0 );
-    Intp_ManFree( pManProof );
-    Sto_ManFree( (Sto_Man_t *)pSatCnf );
-    if ( fVerbose )
-    {
-        printf( "SAT core contains %d clauses (out of %d).  ", Vec_IntSize(vCore), pSat->stats.clauses );
-        ABC_PRT( "Time", clock() - clk );
-    }
-    return vCore;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Mark visited nodes recursively.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Saig_AbsMarkVisited_rec( Aig_Man_t * p, Vec_Str_t * vObj2Visit, Aig_Obj_t * pObj, int i )
-{
-    if ( Saig_AbsVisited( vObj2Visit, Aig_ManObjNumMax(p), pObj, i ) )
-        return 1;
-    Saig_AbsSetVisited( vObj2Visit, Aig_ManObjNumMax(p), pObj, i );
-    if ( Saig_ObjIsPi( p, pObj ) )
-        return 1;
-    if ( Saig_ObjIsLo( p, pObj ) )
-    {
-        if ( i == 0 )
-            return 1;
-        return Saig_AbsMarkVisited_rec( p, vObj2Visit, Saig_ObjLoToLi(p, pObj), i-1 );
-    }
-    if ( Aig_ObjIsPo( pObj ) )
-        return Saig_AbsMarkVisited_rec( p, vObj2Visit, Aig_ObjFanin0(pObj), i );
-    Saig_AbsMarkVisited_rec( p, vObj2Visit, Aig_ObjFanin0(pObj), i );
-    Saig_AbsMarkVisited_rec( p, vObj2Visit, Aig_ObjFanin1(pObj), i );
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Mark visited nodes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Str_t * Saig_AbsMarkVisited( Aig_Man_t * p, int nFramesMax )
-{
-    Vec_Str_t * vObj2Visit;
-    Aig_Obj_t * pObj;
-    int i, f;
-    vObj2Visit = Vec_StrStart( Aig_ManObjNumMax(p) * nFramesMax );
-//    Saig_ManForEachLo( p, pObj, i )
-//        Saig_AbsSetVisited( vObj2Visit, Aig_ManObjNumMax(p), pObj, 0 ); 
-    for ( f = 0; f < nFramesMax; f++ )
-    {
-        Saig_AbsSetVisited( vObj2Visit, Aig_ManObjNumMax(p), Aig_ManConst1(p), f );
-        Saig_ManForEachPo( p, pObj, i )
-            Saig_AbsMarkVisited_rec( p, vObj2Visit, pObj, f );
-    }
-    return vObj2Visit;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs the actual construction of the output.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Obj_t * Saig_AbsCreateFrames_rec( Aig_Man_t * pFrame, Aig_Obj_t * pObj )
-{
-    if ( pObj->pData )
-        return (Aig_Obj_t *)pObj->pData;
-    assert( Aig_ObjIsNode(pObj) );
-    Saig_AbsCreateFrames_rec( pFrame, Aig_ObjFanin0(pObj) );
-    Saig_AbsCreateFrames_rec( pFrame, Aig_ObjFanin1(pObj) );
-    return (Aig_Obj_t *)(pObj->pData = Aig_And( pFrame, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ));
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Derives a vector of AIG managers, one for each frame.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Ptr_t * Saig_AbsCreateFrames( Aig_Man_t * p, int nFramesMax, int fVerbose )
-{
-    Vec_Ptr_t * vFrames, * vLoObjs, * vLiObjs;
-    Vec_Str_t * vObj2Visit;
-    Aig_Man_t * pFrame;
-    Aig_Obj_t * pObj;
-    int f, i;
-    vObj2Visit = Saig_AbsMarkVisited( p, nFramesMax );
-    vFrames = Vec_PtrAlloc( nFramesMax );
-    vLoObjs = Vec_PtrAlloc( 100 );
-    vLiObjs = Vec_PtrAlloc( 100 );
-    for ( f = 0; f < nFramesMax; f++ )
-    {
-        Aig_ManCleanData( p );
-        pFrame = Aig_ManStart( 1000 );
-        Aig_ManConst1(p)->pData = Aig_ManConst1(pFrame);
-        // create PIs
-        Vec_PtrClear( vLoObjs );
-        Vec_PtrClear( vLiObjs );
-        Aig_ManForEachPi( p, pObj, i )
-        { 
-            if ( Saig_AbsVisited( vObj2Visit, Aig_ManObjNumMax(p), pObj, f ) )
-            {
-                pObj->pData = Aig_ObjCreatePi(pFrame);
-                if ( i >= Saig_ManPiNum(p) )
-                    Vec_PtrPush( vLoObjs, pObj );
-            } 
-        }
-        // remember the number of (implicit) registers in this frame
-        pFrame->nAsserts = Vec_PtrSize(vLoObjs);
-        // create POs
-        Aig_ManForEachPo( p, pObj, i )
-        {
-            if ( Saig_AbsVisited( vObj2Visit, Aig_ManObjNumMax(p), pObj, f ) )
-            {
-                Saig_AbsCreateFrames_rec( pFrame, Aig_ObjFanin0(pObj) );
-                pObj->pData = Aig_ObjCreatePo( pFrame, Aig_ObjChild0Copy(pObj) );
-                if ( i >= Saig_ManPoNum(p) )
-                    Vec_PtrPush( vLiObjs, pObj );
-            }
-        }
-//        Vec_PtrPush( vFrames, Cnf_Derive(pFrame, Aig_ManPoNum(pFrame)) );
-        Vec_PtrPush( vFrames, Cnf_DeriveSimple(pFrame, Aig_ManPoNum(pFrame)) );
-        // set the new PIs to point to the corresponding registers
-        Aig_ManCleanData( pFrame );
-        Vec_PtrForEachEntry( Aig_Obj_t *, vLoObjs, pObj, i )
-            ((Aig_Obj_t *)pObj->pData)->pData = pObj;
-        Vec_PtrForEachEntry( Aig_Obj_t *, vLiObjs, pObj, i )
-            ((Aig_Obj_t *)pObj->pData)->pData = pObj;
-        if ( fVerbose )
-            printf( "%3d : PI =%8d. PO =%8d. Flop =%8d. Node =%8d.\n", 
-                f, Aig_ManPiNum(pFrame), Aig_ManPoNum(pFrame), pFrame->nAsserts, Aig_ManNodeNum(pFrame) );
-    }
-    Vec_PtrFree( vLoObjs );
-    Vec_PtrFree( vLiObjs );
-    Vec_StrFree( vObj2Visit );
-    return vFrames;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Derives a vector of AIG managers, one for each frame.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-sat_solver * Saig_AbsCreateSolverDyn( Aig_Man_t * p, Vec_Ptr_t * vFrames )
-{
-    sat_solver * pSat;
-    Cnf_Dat_t * pCnf, * pCnfPrev;
-    Vec_Int_t * vPoLits;
-    Aig_Obj_t * pObjPo, * pObjLi, * pObjLo;
-    int f, i, Lit, Lits[2], iVarOld, iVarNew, nSatVars, nRegisters;
-    // start array of output literals
-    vPoLits = Vec_IntAlloc( 100 );
-    // count the number of CNF variables
-    nSatVars = 0;
-    Vec_PtrForEachEntry( Cnf_Dat_t *, vFrames, pCnf, f )
-        nSatVars += pCnf->nVars;
-
-    // create the SAT solver
-    pSat = sat_solver_new();
-    sat_solver_store_alloc( pSat ); 
-    sat_solver_setnvars( pSat, nSatVars );
-
-    // add clauses for the timeframes
-    nSatVars = 0;
-//    Vec_PtrForEachEntryReverse( Cnf_Dat_t *, vFrames, pCnf, f )
-    Vec_PtrForEachEntry( Cnf_Dat_t *, vFrames, pCnf, f )
-    {
-        // lift clauses of this CNF
-        Cnf_DataLift( pCnf, nSatVars );
-        nSatVars += pCnf->nVars;
-        // copy clauses into the manager
-        for ( i = 0; i < pCnf->nClauses; i++ )
-        {
-            if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
-            {
-                printf( "The BMC problem is trivially UNSAT.\n" );
-                sat_solver_delete( pSat );
-                Vec_IntFree( vPoLits );
-                return NULL;
-            }
-        }
-        // remember output literal
-        Aig_ManForEachPo( pCnf->pMan, pObjPo, i )
-        {
-            if ( i == Saig_ManPoNum(p) )
-                break;
-            Vec_IntPush( vPoLits, toLit(pCnf->pVarNums[pObjPo->Id]) );
-        }
-    }
-
-    // add auxiliary clauses (output, connectors, initial)
-    // add output clause
-    if ( !sat_solver_addclause( pSat, Vec_IntArray(vPoLits), Vec_IntArray(vPoLits) + Vec_IntSize(vPoLits) ) )
-    {
-        printf( "SAT solver is not created correctly.\n" );
-        assert( 0 );
-    }
-    Vec_IntFree( vPoLits );
-
-    // add connecting clauses
-    pCnfPrev = (Cnf_Dat_t *)Vec_PtrEntry( vFrames, 0 );
-    Vec_PtrForEachEntryStart( Cnf_Dat_t *, vFrames, pCnf, f, 1 )
-    {
-        nRegisters = pCnf->pMan->nAsserts;
-        assert( nRegisters <= Aig_ManPoNum(pCnfPrev->pMan) );
-        assert( nRegisters <= Aig_ManPiNum(pCnf->pMan) );
-        for ( i = 0; i < nRegisters; i++ )
-        {
-            pObjLi = Aig_ManPo( pCnfPrev->pMan, Aig_ManPoNum(pCnfPrev->pMan) - nRegisters + i );
-            pObjLo = Aig_ManPi( pCnf->pMan,     Aig_ManPiNum(pCnf->pMan) -     nRegisters + i );
-            // get variable numbers
-            iVarOld = pCnfPrev->pVarNums[pObjLi->Id];
-            iVarNew = pCnf->pVarNums[pObjLo->Id];
-            // add clauses connecting existing variables
-            Lits[0] = toLitCond( iVarOld, 0 );
-            Lits[1] = toLitCond( iVarNew, 1 );
-            if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
-                assert( 0 );
-            Lits[0] = toLitCond( iVarOld, 1 );
-            Lits[1] = toLitCond( iVarNew, 0 );
-            if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
-                assert( 0 );
-        }
-        pCnfPrev = pCnf;
-    }
-    // add unit clauses
-    pCnf = (Cnf_Dat_t *)Vec_PtrEntry( vFrames, 0 );
-    nRegisters = pCnf->pMan->nAsserts;
-    for ( i = 0; i < nRegisters; i++ )
-    {
-        pObjLo = Aig_ManPi( pCnf->pMan, Aig_ManPiNum(pCnf->pMan) - nRegisters + i );
-        assert( pCnf->pVarNums[pObjLo->Id] >= 0 );
-        Lit = toLitCond( pCnf->pVarNums[pObjLo->Id], 1 );
-        if ( !sat_solver_addclause( pSat, &Lit, &Lit+1 ) )
-            assert( 0 );
-    }
-    sat_solver_store_mark_roots( pSat ); 
-    return pSat;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Creates SAT solver for BMC.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-sat_solver * Saig_AbsCreateSolver( Cnf_Dat_t * pCnf, int nFrames )
-{
-    sat_solver * pSat;
-    Vec_Int_t * vPoLits;
-    Aig_Obj_t * pObjPo, * pObjLi, * pObjLo;
-    int f, i, Lit, Lits[2], iVarOld, iVarNew;
-    // start array of output literals
-    vPoLits = Vec_IntAlloc( nFrames * Saig_ManPoNum(pCnf->pMan) );
-    // create the SAT solver
-    pSat = sat_solver_new();
-    sat_solver_store_alloc( pSat ); 
-    sat_solver_setnvars( pSat, pCnf->nVars * nFrames );
-
-    // add clauses for the timeframes
-    for ( f = 0; f < nFrames; f++ )
-    {
-        for ( i = 0; i < pCnf->nClauses; i++ )
-        {
-            if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
-            {
-                printf( "The BMC problem is trivially UNSAT.\n" );
-                sat_solver_delete( pSat );
-                Vec_IntFree( vPoLits );
-                return NULL;
-            }
-        }
-        // remember output literal
-        Saig_ManForEachPo( pCnf->pMan, pObjPo, i )
-            Vec_IntPush( vPoLits, toLit(pCnf->pVarNums[pObjPo->Id]) );
-        // lift CNF to the next frame
-        Cnf_DataLift( pCnf, pCnf->nVars );
-    }
-    // put CNF back to the original level
-    Cnf_DataLift( pCnf, - pCnf->nVars * nFrames );
-
-    // add auxiliary clauses (output, connectors, initial)
-    // add output clause
-    if ( !sat_solver_addclause( pSat, Vec_IntArray(vPoLits), Vec_IntArray(vPoLits) + Vec_IntSize(vPoLits) ) )
-        assert( 0 );
-    Vec_IntFree( vPoLits );
-    // add connecting clauses
-    for ( f = 0; f < nFrames; f++ )
-    {
-        // connect to the previous timeframe
-        if ( f > 0 )
-        {
-            Saig_ManForEachLiLo( pCnf->pMan, pObjLi, pObjLo, i )
-            {
-                iVarOld = pCnf->pVarNums[pObjLi->Id] - pCnf->nVars;
-                iVarNew = pCnf->pVarNums[pObjLo->Id];
-                // add clauses connecting existing variables
-                Lits[0] = toLitCond( iVarOld, 0 );
-                Lits[1] = toLitCond( iVarNew, 1 );
-                if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
-                    assert( 0 );
-                Lits[0] = toLitCond( iVarOld, 1 );
-                Lits[1] = toLitCond( iVarNew, 0 );
-                if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
-                    assert( 0 );
-            }
-        }
-        // lift CNF to the next frame
-        Cnf_DataLift( pCnf, pCnf->nVars );
-    }
-    // put CNF back to the original level
-    Cnf_DataLift( pCnf, - pCnf->nVars * nFrames );
-    // add unit clauses
-    Saig_ManForEachLo( pCnf->pMan, pObjLo, i )
-    {
-        assert( pCnf->pVarNums[pObjLo->Id] >= 0 );
-        Lit = toLitCond( pCnf->pVarNums[pObjLo->Id], 1 );
-        if ( !sat_solver_addclause( pSat, &Lit, &Lit+1 ) )
-            assert( 0 );
-    }
-    sat_solver_store_mark_roots( pSat ); 
-    return pSat;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs proof-based abstraction using BMC of the given depth.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Int_t * Saig_AbsCollectRegistersDyn( Aig_Man_t * p, Vec_Ptr_t * vFrames, Vec_Int_t * vCore )
-{
-    Aig_Obj_t * pObj;
-    Cnf_Dat_t * pCnf;
-    Vec_Int_t * vFlops;
-    int * pVars, * pFlops;
-    int i, f, iClause, iReg, * piLit, nSatVars, nSatClauses;
-    // count the number of CNF variables
-    nSatVars = 0;
-    Vec_PtrForEachEntry( Cnf_Dat_t *, vFrames, pCnf, f )
-        nSatVars += pCnf->nVars;
-    // mark register variables
-    pVars = ABC_ALLOC( int, nSatVars );
-    for ( i = 0; i < nSatVars; i++ )
-        pVars[i] = -1;
-    Vec_PtrForEachEntry( Cnf_Dat_t *, vFrames, pCnf, f )
-    {
-        Aig_ManForEachPi( pCnf->pMan, pObj, i )
-        {
-            assert( pCnf->pVarNums[pObj->Id] >= 0 );
-            assert( pCnf->pVarNums[pObj->Id] < nSatVars );
-            if ( pObj->pData == NULL )
-                continue;
-            iReg = Aig_ObjPioNum((Aig_Obj_t *)pObj->pData) - Saig_ManPiNum(p);
-            assert( iReg >= 0 && iReg < Aig_ManRegNum(p) );
-            pVars[ pCnf->pVarNums[pObj->Id] ] = iReg;
-        }
-        Aig_ManForEachPo( pCnf->pMan, pObj, i )
-        {
-            assert( pCnf->pVarNums[pObj->Id] >= 0 );
-            assert( pCnf->pVarNums[pObj->Id] < nSatVars );
-            if ( pObj->pData == NULL )
-                continue;
-            iReg = Aig_ObjPioNum((Aig_Obj_t *)pObj->pData) - Saig_ManPoNum(p);
-            assert( iReg >= 0 && iReg < Aig_ManRegNum(p) );
-            pVars[ pCnf->pVarNums[pObj->Id] ] = iReg;
-        }
-    }
-    // mark used registers
-    pFlops = ABC_CALLOC( int, Aig_ManRegNum(p) );
-    Vec_IntForEachEntry( vCore, iClause, i )
-    {
-        nSatClauses = 0;
-        Vec_PtrForEachEntry( Cnf_Dat_t *, vFrames, pCnf, f )
-        {
-            if ( iClause < nSatClauses + pCnf->nClauses )
-                break;
-            nSatClauses += pCnf->nClauses;
-        }
-        if ( f == Vec_PtrSize(vFrames) )
-            continue;
-        iClause = iClause - nSatClauses;
-        assert( iClause >= 0 );
-        assert( iClause < pCnf->nClauses );
-        // consider the clause
-        for ( piLit = pCnf->pClauses[iClause]; piLit < pCnf->pClauses[iClause+1]; piLit++ )
-        {
-            iReg = pVars[ lit_var(*piLit) ];
-            if ( iReg >= 0 )
-                pFlops[iReg] = 1;
-        }
-    }
-    // collect registers
-    vFlops = Vec_IntAlloc( Aig_ManRegNum(p) );
-    for ( i = 0; i < Aig_ManRegNum(p); i++ )
-        if ( pFlops[i] )
-            Vec_IntPush( vFlops, i );
-    ABC_FREE( pFlops );
-    ABC_FREE( pVars );
-    return vFlops;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs proof-based abstraction using BMC of the given depth.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Int_t * Saig_AbsCollectRegisters( Cnf_Dat_t * pCnf, int nFrames, Vec_Int_t * vCore )
-{
-    Aig_Obj_t * pObj;
-    Vec_Int_t * vFlops;
-    int * pVars, * pFlops;
-    int i, iClause, iReg, * piLit;
-    // mark register variables
-    pVars = ABC_ALLOC( int, pCnf->nVars );
-    for ( i = 0; i < pCnf->nVars; i++ )
-        pVars[i] = -1;
-    Saig_ManForEachLi( pCnf->pMan, pObj, i )
-        pVars[ pCnf->pVarNums[pObj->Id] ] = i;
-    Saig_ManForEachLo( pCnf->pMan, pObj, i )
-        pVars[ pCnf->pVarNums[pObj->Id] ] = i;
-    // mark used registers
-    pFlops = ABC_CALLOC( int, Aig_ManRegNum(pCnf->pMan) );
-    Vec_IntForEachEntry( vCore, iClause, i )
-    {
-        // skip auxiliary clauses
-        if ( iClause >= pCnf->nClauses * nFrames )
-            continue;
-        // consider the clause
-        iClause = iClause % pCnf->nClauses;
-        for ( piLit = pCnf->pClauses[iClause]; piLit < pCnf->pClauses[iClause+1]; piLit++ )
-        {
-            iReg = pVars[ lit_var(*piLit) ];
-            if ( iReg >= 0 )
-                pFlops[iReg] = 1;
-        }
-    }
-    // collect registers
-    vFlops = Vec_IntAlloc( Aig_ManRegNum(pCnf->pMan) );
-    for ( i = 0; i < Aig_ManRegNum(pCnf->pMan); i++ )
-        if ( pFlops[i] )
-            Vec_IntPush( vFlops, i );
-    ABC_FREE( pFlops );
-    ABC_FREE( pVars );
-    return vFlops;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs proof-based abstraction using BMC of the given depth.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Saig_AbsFreeCnfs( Vec_Ptr_t * vFrames )
-{
-    Cnf_Dat_t * pCnf;
-    int i;
-    Vec_PtrForEachEntry( Cnf_Dat_t *, vFrames, pCnf, i )
-    {
-        Aig_ManStop( pCnf->pMan );
-        Cnf_DataFree( pCnf );
-    }
-    Vec_PtrFree( vFrames );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs proof-based abstraction using BMC of the given depth.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Saig_AbsExtendOneStep( Aig_Man_t * p, Vec_Int_t * vFlops )
-{
-    Vec_Ptr_t * vFlopPtrs, * vSupp;
-    Aig_Obj_t * pObj;
-    int i, Entry;
-    // collect latch inputs
-    vFlopPtrs = Vec_PtrAlloc( 1000 );
-    Vec_IntForEachEntry( vFlops, Entry, i )
-    {
-        Vec_PtrPush( vFlopPtrs, Saig_ManLi(p, Entry) );
-        pObj = Saig_ManLo(p, Entry);
-        pObj->fMarkA = 1;
-    }
-    // collect latch outputs
-    vSupp = Vec_PtrAlloc( 1000 );
-    Aig_SupportNodes( p, (Aig_Obj_t **)Vec_PtrArray(vFlopPtrs), Vec_PtrSize(vFlopPtrs), vSupp );
-    Vec_PtrFree( vFlopPtrs );
-    // mark influencing flops
-    Vec_PtrForEachEntry( Aig_Obj_t *, vSupp, pObj, i )
-        pObj->fMarkA = 1;
-    Vec_PtrFree( vSupp );
-    // reload flops
-    Vec_IntClear( vFlops );
-    Aig_ManForEachPi( p, pObj, i )
-    {
-        if ( pObj->fMarkA == 0 )
-            continue;
-        pObj->fMarkA = 0;
-        if ( Aig_ObjPioNum(pObj)-Saig_ManPiNum(p) >= 0 )
-            Vec_IntPush( vFlops, Aig_ObjPioNum(pObj)-Saig_ManPiNum(p) );
-    }
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Performs proof-based abstraction using BMC of the given depth.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
- 
-***********************************************************************/
-Vec_Int_t * Saig_ManProofAbstractionFlops( Aig_Man_t * p, Gia_ParAbs_t * pPars )
-{
-    Vec_Int_t * vFlops;
-    sat_solver * pSat;
-    Vec_Ptr_t * vFrames = NULL;
-    Vec_Int_t * vCore;
-    Cnf_Dat_t * pCnf = NULL;
-    int clk = clock(), clk2 = clock();
-    if ( pPars->fVerbose )
-        printf( "Performing proof-based abstraction with %d frames and %d max conflicts.\n", pPars->nFramesMax, pPars->nConfMax );
-    assert( Aig_ManRegNum(p) > 0 );
-    Aig_ManSetPioNumbers( p );
-    if ( pPars->fDynamic )
-    {
-        // create CNF for the frames
-        vFrames = Saig_AbsCreateFrames( p, pPars->nFramesMax, pPars->fVerbose );
-        // create dynamic solver
-        pSat = Saig_AbsCreateSolverDyn( p, vFrames );
-    }
-    else
-    {
-        // create CNF for the AIG
-        pCnf = Cnf_DeriveSimple( p, Aig_ManPoNum(p) );
-        // create SAT solver for the unrolled AIG
-        pSat = Saig_AbsCreateSolver( pCnf, pPars->nFramesMax );
-    }
-    if ( pPars->fVerbose )
-    {
-        printf( "SAT solver: Vars = %7d. Clauses = %7d.  ", pSat->size, pSat->stats.clauses );
-        ABC_PRT( "Time", clock() - clk2 );
-    }
-    // compute UNSAT core
-    vCore = Saig_AbsSolverUnsatCore( pSat, pPars->nConfMax, pPars->fVerbose, &pPars->Status );
-    sat_solver_delete( pSat );
-    if ( vCore == NULL )
-    {
-        if ( vFrames )
-            Saig_AbsFreeCnfs( vFrames );
-        return NULL;
-    }
-    pPars->nFramesDone = pPars->nFramesMax;
-    // collect registers
-    if ( pPars->fDynamic )
-    {
-        vFlops = Saig_AbsCollectRegistersDyn( p, vFrames, vCore );
-        Saig_AbsFreeCnfs( vFrames );
-    }
-    else
-    {
-        vFlops = Saig_AbsCollectRegisters( pCnf, pPars->nFramesMax, vCore );
-        Cnf_DataFree( pCnf );
-    }
-    Vec_IntFree( vCore );
-    if ( pPars->fVerbose )
-    {
-        printf( "The number of relevant registers is %d (out of %d).  ", Vec_IntSize(vFlops), Aig_ManRegNum(p) );
-        ABC_PRT( "Time", clock() - clk );
-    }
-    return vFlops;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs proof-based abstraction using BMC of the given depth.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
- 
-***********************************************************************/
-Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, Gia_ParAbs_t * pPars )
-{
-    Vec_Int_t * vFlops;
-    Aig_Man_t * pAbs = NULL;
-    vFlops = Saig_ManProofAbstractionFlops( p, pPars );
-    // write the final result
-    if ( vFlops )
-    {
-        pAbs = Saig_ManDeriveAbstraction( p, vFlops );
-        Ioa_WriteAiger( pAbs, "gabs.aig", 0, 0 );
-        printf( "Final abstracted model was written into file \"%s\".\n", "gabs.aig" );
-        Vec_IntFree( vFlops );
-    }
-    return pAbs;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
-ABC_NAMESPACE_IMPL_END
-
diff --git a/src/aig/saig/saigRefSat.c b/src/aig/saig/saigRefSat.c
index 0b3dff23..27c243b5 100644
--- a/src/aig/saig/saigRefSat.c
+++ b/src/aig/saig/saigRefSat.c
@@ -294,10 +294,10 @@ Aig_Man_t * Saig_ManUnrollWithCex( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInpu
     }
 
     // derive unrolled timeframes
-    pFrames = Aig_ManStart( Aig_ManObjNumMax(pAig) * (pCex->iFrame+1) );
+    pFrames = Aig_ManStart( 10000 );
     pFrames->pName = Aig_UtilStrsav( pAig->pName );
     pFrames->pSpec = Aig_UtilStrsav( pAig->pSpec );
-    // initialize the flops of
+    // initialize the flops 
     Saig_ManForEachLo( pAig, pObj, i )
         pObj->pData = Aig_NotCond( Aig_ManConst1(pFrames), !Aig_InfoHasBit(pCex->pData, i) );
     // iterate through the frames
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 581af654..2492fb37 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -45,7 +45,6 @@
 #include "retInt.h"
 #include "cnf.h"
 #include "cec.h"
-#include "giaAbs.h"
 #include "pdr.h" 
 
 #include "tim.h"
@@ -247,7 +246,7 @@ static int Abc_CommandSeqCleanup             ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandCycle                  ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandXsim                   ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSim                    ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandSim2                   ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandSim3                   ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandDarPhase               ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSynch                  ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandClockGate              ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -272,7 +271,6 @@ static int Abc_CommandIndcut                 ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandEnlarge                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandTempor                 ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandInduction              ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandCegar                  ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandConstr                 ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandUnfold                 ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandFold                   ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -373,10 +371,11 @@ static int Abc_CommandAbc9Speedup            ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandAbc9Era                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Dch                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9AbsStart           ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandAbc9AbsStartNew        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9AbsDerive          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9AbsRefine          ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandAbc9PbaStart           ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9AbsPba             ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9AbsCba             ( Abc_Frame_t * pAbc, int argc, char ** argv );
+//static int Abc_CommandAbc9PbaStart           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Reparam            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Posplit            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9ReachM             ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -668,7 +667,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Sequential",   "cycle",         Abc_CommandCycle,            1 );
     Cmd_CommandAdd( pAbc, "Sequential",   "xsim",          Abc_CommandXsim,             0 );
     Cmd_CommandAdd( pAbc, "Sequential",   "sim",           Abc_CommandSim,              0 );
-    Cmd_CommandAdd( pAbc, "Sequential",   "sim2",          Abc_CommandSim2,             0 );
+    Cmd_CommandAdd( pAbc, "Sequential",   "sim3",          Abc_CommandSim3,             0 );
     Cmd_CommandAdd( pAbc, "Sequential",   "phase",         Abc_CommandDarPhase,         1 );
     Cmd_CommandAdd( pAbc, "Sequential",   "synch",         Abc_CommandSynch,            1 );
     Cmd_CommandAdd( pAbc, "Sequential",   "clockgate",     Abc_CommandClockGate,        1 );
@@ -698,7 +697,6 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Verification", "enlarge",       Abc_CommandEnlarge,          1 );
     Cmd_CommandAdd( pAbc, "Verification", "tempor",        Abc_CommandTempor,           1 );
     Cmd_CommandAdd( pAbc, "Verification", "ind",           Abc_CommandInduction,        0 );
-    Cmd_CommandAdd( pAbc, "Verification", "abs",           Abc_CommandCegar,            1 );
     Cmd_CommandAdd( pAbc, "Verification", "constr",        Abc_CommandConstr,           0 );
     Cmd_CommandAdd( pAbc, "Verification", "unfold",        Abc_CommandUnfold,           1 );
     Cmd_CommandAdd( pAbc, "Verification", "fold",          Abc_CommandFold,             1 );
@@ -794,10 +792,10 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC9",         "&era",          Abc_CommandAbc9Era,          0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&dch",          Abc_CommandAbc9Dch,          0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&abs_start",    Abc_CommandAbc9AbsStart,     0 );
-    Cmd_CommandAdd( pAbc, "ABC9",         "&abs_newstart", Abc_CommandAbc9AbsStartNew,  0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&abs_derive",   Abc_CommandAbc9AbsDerive,    0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&abs_refine",   Abc_CommandAbc9AbsRefine,    0 );
-    Cmd_CommandAdd( pAbc, "ABC9",         "&pba_start",    Abc_CommandAbc9PbaStart,     0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&abs_pba",      Abc_CommandAbc9AbsPba,       0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&abs_cba",      Abc_CommandAbc9AbsCba,       0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&reparam",      Abc_CommandAbc9Reparam,      0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&posplit",      Abc_CommandAbc9Posplit,      0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&reachm",       Abc_CommandAbc9ReachM,       0 );
@@ -15792,7 +15790,7 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_CommandSim2( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandSim3( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
     int c;
@@ -15896,7 +15894,7 @@ int Abc_CommandSim2( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: sim2 [-FWBRT num] [-vh]\n" );
+    Abc_Print( -2, "usage: sim3 [-FWBRT num] [-vh]\n" );
     Abc_Print( -2, "\t         performs random simulation of the sequential miter\n" );
     Abc_Print( -2, "\t-F num : the number of frames to simulate [default = %d]\n", nFrames );
     Abc_Print( -2, "\t-W num : the number of words to simulate [default = %d]\n",  nWords );
@@ -19643,134 +19641,6 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_CommandCegar( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
-    Gia_ParAbs_t Pars, * pPars = &Pars;
-    Abc_Ntk_t * pNtk, * pNtkRes;
-    int c;
-    extern Abc_Ntk_t * Abc_NtkDarCegar( Abc_Ntk_t * pNtk, Gia_ParAbs_t * pPars );
-
-    pNtk = Abc_FrameReadNtk(pAbc);
-    // set defaults
-    Gia_ManAbsSetDefaultParams( pPars );
-    Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "FCRcrpfvh" ) ) != EOF )
-    {
-        switch ( c )
-        {
-        case 'F':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            pPars->nFramesBmc = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->nFramesBmc < 0 ) 
-                goto usage;
-            break;
-        case 'C':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            pPars->nConfMaxBmc = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->nConfMaxBmc < 0 ) 
-                goto usage;
-            break;
-        case 'R':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-R\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            pPars->nRatio = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->nRatio < 0 ) 
-                goto usage;
-            break;
-        case 'c':
-            pPars->fConstr ^= 1;
-            break;
-        case 'r':
-            pPars->fUseBdds ^= 1;
-            break;
-        case 'p':
-            pPars->fUseDprove ^= 1;
-            break;
-        case 'f':
-            pPars->fUseStart ^= 1;
-            break;
-        case 'v':
-            pPars->fVerbose ^= 1;
-            break;
-        case 'h':
-            goto usage;
-        default:
-            goto usage;
-        }
-    }
-    if ( pNtk == NULL )
-    {
-        Abc_Print( -1, "Empty network.\n" );
-        return 1;
-    }
-    if ( Abc_NtkIsComb(pNtk) )
-    {
-        Abc_Print( -1, "The network is combinational.\n" );
-        return 0;
-    }
-    if ( !Abc_NtkIsStrash(pNtk) )
-    {
-        Abc_Print( -1, "Currently only works for structurally hashed circuits.\n" );
-        return 0;
-    }
-    if ( !(0 <= pPars->nRatio && pPars->nRatio <= 100) )
-    {
-        Abc_Print( -1, "Wrong value of parameter \"-R <num>\".\n" );
-        return 0;
-    }
-
-    // modify the current network
-    pNtkRes = Abc_NtkDarCegar( pNtk, pPars );
-    if ( pNtkRes == NULL )
-    {
-        if ( pNtk->pSeqModel == NULL )
-            Abc_Print( -1, "Abstraction has failed.\n" );
-        return 0;
-    }
-    // replace the current network
-    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
-    return 0;
-usage:
-    Abc_Print( -2, "usage: abs [-FCR num] [-crpfvh]\n" );
-    Abc_Print( -2, "\t         performs counter-example-based abstraction\n" );
-    Abc_Print( -2, "\t-F num : the max number of timeframes for BMC [default = %d]\n", pPars->nFramesBmc );
-    Abc_Print( -2, "\t-C num : the max number of conflicts by SAT solver for BMC [default = %d]\n", pPars->nConfMaxBmc );
-    Abc_Print( -2, "\t-R num : the %% of abstracted flops when refinement stops (0<=num<=100) [default = %d]\n", pPars->nRatio );
-    Abc_Print( -2, "\t-c     : toggle dynamic addition of constraints [default = %s]\n", pPars->fConstr? "yes": "no" );
-    Abc_Print( -2, "\t-r     : toggle using BDD-based reachability for filtering [default = %s]\n", pPars->fUseBdds? "yes": "no" );
-//    Abc_Print( -2, "\t-p     : toggle using \"dprove\" for filtering [default = %s]\n", pPars->fUseDprove? "yes": "no" );
-    Abc_Print( -2, "\t-p     : toggle using \"pdr\" for filtering [default = %s]\n", pPars->fUseDprove? "yes": "no" );
-    Abc_Print( -2, "\t-f     : toggle starting BMC from a later frame [default = %s]\n", pPars->fUseStart? "yes": "no" );
-    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
-    Abc_Print( -2, "\t-h     : print the command usage\n");
-    return 1;
-}
- 
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
 int Abc_CommandConstr( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Abc_Ntk_t * pNtk;
@@ -25291,6 +25161,7 @@ int Abc_CommandAbc9Equiv3( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
 //    extern int Abc_NtkDarSeqEquiv2( Abc_Ntk_t * pNtk, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose );
     extern int Ssw_RarSignalFilterGia( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose );
+    extern int Ssw_RarSignalFilterGia2( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int TimeOut, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose );
     int c;
     int nFrames    =   20;
     int nWords     =   50;
@@ -25299,9 +25170,10 @@ int Abc_CommandAbc9Equiv3( Abc_Frame_t * pAbc, int argc, char ** argv )
     int TimeOut    =    0;
     int fUseCex    =    0;
     int fLatchOnly =    0;
+    int fNewAlgo   =    0;
     int fVerbose   =    1;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "FWBRTxlvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "FWBRTxlavh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -25366,6 +25238,9 @@ int Abc_CommandAbc9Equiv3( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'l':
             fLatchOnly ^= 1;
             break;
+        case 'a':
+            fNewAlgo ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -25395,7 +25270,10 @@ int Abc_CommandAbc9Equiv3( Abc_Frame_t * pAbc, int argc, char ** argv )
         }
     }
 //    pAbc->Status = Abc_NtkDarSeqEquiv2( pNtk, nFrames, nWords, nBinSize, nRounds, TimeOut, fUseCex? pAbc->pCex: NULL, fLatchOnly, fVerbose );
-    pAbc->Status = Ssw_RarSignalFilterGia( pAbc->pGia, nFrames, nWords, nBinSize, nRounds, TimeOut, fUseCex? pAbc->pCex: NULL, fLatchOnly, fVerbose );
+    if ( fNewAlgo )
+        pAbc->Status = Ssw_RarSignalFilterGia2( pAbc->pGia, nFrames, nWords, nBinSize, nRounds, TimeOut, fUseCex? pAbc->pCex: NULL, fLatchOnly, fVerbose );
+    else
+        pAbc->Status = Ssw_RarSignalFilterGia( pAbc->pGia, nFrames, nWords, nBinSize, nRounds, TimeOut, fUseCex? pAbc->pCex: NULL, fLatchOnly, fVerbose );
 //    pAbc->nFrames = pAbc->pCex->iFrame;
 //    Abc_FrameReplaceCex( pAbc, &pAbc->pCex );
     return 0;
@@ -25403,13 +25281,14 @@ int Abc_CommandAbc9Equiv3( Abc_Frame_t * pAbc, int argc, char ** argv )
 usage:
     Abc_Print( -2, "usage: &equiv3 [-FWBRT num] [-xlvh]\n" );
     Abc_Print( -2, "\t         computes candidate equivalence classes\n" );
-    Abc_Print( -2, "\t-F num : the max number of frames for BMC [default = %d]\n", nFrames );
-    Abc_Print( -2, "\t-W num : the number of words to simulate [default = %d]\n",  nWords );
-    Abc_Print( -2, "\t-B num : the number of flops in one bin [default = %d]\n",   nBinSize );
+    Abc_Print( -2, "\t-F num : the max number of frames for BMC [default = %d]\n",    nFrames );
+    Abc_Print( -2, "\t-W num : the number of words to simulate [default = %d]\n",     nWords );
+    Abc_Print( -2, "\t-B num : the number of flops in one bin [default = %d]\n",      nBinSize );
     Abc_Print( -2, "\t-R num : the max number of simulation rounds [default = %d]\n", nRounds );
     Abc_Print( -2, "\t-T num : runtime limit in seconds for all rounds [default = %d]\n", TimeOut );
     Abc_Print( -2, "\t-x     : toggle using the current cex to perform refinement [default = %s]\n", fUseCex? "yes": "no" );
     Abc_Print( -2, "\t-l     : toggle considering only latch output equivalences [default = %s]\n", fLatchOnly? "yes": "no" );
+    Abc_Print( -2, "\t-a     : toggle using a new algorithm [default = %s]\n",        fNewAlgo? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
@@ -27930,8 +27809,6 @@ int Abc_CommandAbc9AbsStart( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Gia_ParAbs_t Pars, * pPars = &Pars;
     int c;
-    extern void Gia_ManCexAbstractionStart( Gia_Man_t * pGia, Gia_ParAbs_t * pPars );
-
     // set defaults
     Gia_ManAbsSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
@@ -28050,167 +27927,43 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_CommandAbc9AbsStartNew( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandAbc9AbsDerive( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    Gia_ParAbs_t Pars, * pPars = &Pars;
-    int c;
-    extern void Gia_ManCexAbstractionStartNew( Gia_Man_t * pGia, Gia_ParAbs_t * pPars );
-
-    // set defaults
-    Gia_ManAbsSetDefaultParams( pPars );
+    Gia_Man_t * pTemp = NULL;
+    int c, fVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "AFSCRBTVrpfvwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
     {
         switch ( c )
         {
-        case 'A':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            pPars->Algo = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->Algo < 0 ) 
-                goto usage;
-            break;
-        case 'F':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            pPars->nFramesBmc = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->nFramesBmc < 0 ) 
-                goto usage;
-            break;
-        case 'S':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            pPars->nStableMax = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->nStableMax < 0 ) 
-                goto usage;
-            break;
-        case 'C':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            pPars->nConfMaxBmc = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->nConfMaxBmc < 0 ) 
-                goto usage;
-            break;
-        case 'R':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-R\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            pPars->nRatio = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->nRatio < 0 ) 
-                goto usage;
-            break;
-        case 'B':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-B\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            pPars->nBobPar = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->nBobPar < 0 ) 
-                goto usage;
-            break;
-        case 'T':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            pPars->TimeOut = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->TimeOut < 0 ) 
-                goto usage;
-            break;
-        case 'V':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-V\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            pPars->TimeOutVT = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->TimeOutVT < 0 ) 
-                goto usage;
-            break;
-        case 'r':
-            pPars->fUseBdds ^= 1;
-            break;
-        case 'p':
-            pPars->fUseDprove ^= 1;
-            break;
-        case 'f':
-            pPars->fUseStart ^= 1;
-            break;
         case 'v':
-            pPars->fVerbose ^= 1;
-            break;
-        case 'w':
-            pPars->fVeryVerbose ^= 1;
+            fVerbose ^= 1;
             break;
         case 'h':
-            goto usage; 
+            goto usage;
         default:
             goto usage;
         }
     }
     if ( pAbc->pGia == NULL )
     {
-        Abc_Print( -1, "Abc_CommandAbc9AbsStartNew(): There is no AIG.\n" );
+        Abc_Print( -1, "Abc_CommandAbc9AbsDerive(): There is no AIG.\n" );
         return 1;
-    }
+    } 
     if ( Gia_ManRegNum(pAbc->pGia) == 0 )
     {
-        Abc_Print( -1, "Abc_CommandAbc9AbsStartNew(): The AIG is combinational.\n" );
-        return 0;
-    }
-    if ( !(0 <= pPars->nRatio && pPars->nRatio <= 100) )
-    {
-        Abc_Print( -1, "Abc_CommandAbc9AbsStartNew(): Wrong value of parameter \"-R <num>\".\n" );
+        Abc_Print( -1, "The network is combinational.\n" );
         return 0;
     }
-    Gia_ManCexAbstractionStartNew( pAbc->pGia, pPars );
-    pAbc->Status  = pPars->Status;
-    pAbc->nFrames = pPars->nFramesDone;
-    Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
-    if ( pPars->fVerbose )
-        printf( "Updating ABC solving status to be %d and bmc_frames_done to be %d.\n", pPars->Status, pAbc->nFrames );
+    pTemp = Gia_ManCexAbstractionDerive( pAbc->pGia );
+    Abc_CommandUpdate9( pAbc, pTemp );
     return 0;
+
 usage:
-    Abc_Print( -2, "usage: &abs_newstart [-AFSCBTV num] [-vwh]\n" );
-    Abc_Print( -2, "\t         initializes flop map using cex-based abstraction (by Niklas Een)\n" );
-    Abc_Print( -2, "\t-A num : selects the algorithm to use [default = %d]\n", pPars->Algo );
-    Abc_Print( -2, "\t         0 = cba\n" );
-    Abc_Print( -2, "\t         1 = pba\n" );
-    Abc_Print( -2, "\t         2 = cba-then-pba\n" );
-    Abc_Print( -2, "\t         3 = cba-with-pba\n" );
-    Abc_Print( -2, "\t-F num : the max number of timeframes for BMC [default = %d]\n", pPars->nFramesBmc );
-    Abc_Print( -2, "\t-S num : the max number of stable frames for BMC [default = %d]\n", pPars->nStableMax );
-    Abc_Print( -2, "\t-C num : the max number of conflicts by SAT solver for BMC [default = %d]\n", pPars->nConfMaxBmc );
-    Abc_Print( -2, "\t-B num : the max number of frames to wait before trying to quit [default = %d]\n", pPars->nBobPar );
-    Abc_Print( -2, "\t-T num : approximate time limit in seconds (0=infinite) [default = %d]\n", pPars->TimeOut );
-    Abc_Print( -2, "\t-V num : approximate \"virtual time\" limit in seconds (0=infinite) [default = %d]\n", pPars->TimeOutVT );
-    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
-    Abc_Print( -2, "\t-w     : toggle printing additional information [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
-    Abc_Print( -2, "\t-h     : print the command usage\n");
+    Abc_Print( -2, "usage: &abs_derive [-vh]\n" );
+    Abc_Print( -2, "\t        performs abstraction using the pre-computed flop map\n" );
+    Abc_Print( -2, "\t-v    : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h    : print the command usage\n");
     return 1;
 }
 
@@ -28225,46 +27978,27 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_CommandAbc9PbaStart( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandAbc9AbsRefine( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    Gia_ParAbs_t Pars, * pPars = &Pars;
+    Gia_Man_t * pTemp = NULL;
     int c;
-    extern void Gia_ManProofAbstractionStart( Gia_Man_t * pGia, Gia_ParAbs_t * pPars );
+    int fTryFour   = 1;
+    int fSensePath = 0;
+    int fVerbose   = 0;
 
-    // set defaults
-    Gia_ManAbsSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "FCdvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "tsvh" ) ) != EOF )
     {
         switch ( c )
         {
-        case 'F':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            pPars->nFramesMax = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->nFramesMax < 0 ) 
-                goto usage;
-            break;
-        case 'C':
-            if ( globalUtilOptind >= argc )
-            {
-                Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            pPars->nConfMax = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( pPars->nConfMax < 0 ) 
-                goto usage;
+        case 't':
+            fTryFour ^= 1;
             break;
-        case 'd':
-            pPars->fDynamic ^= 1;
+        case 's':
+            fSensePath ^= 1;
             break;
         case 'v':
-            pPars->fVerbose ^= 1;
+            fVerbose ^= 1;
             break;
         case 'h':
             goto usage;
@@ -28274,36 +28008,32 @@ int Abc_CommandAbc9PbaStart( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( pAbc->pGia == NULL )
     {
-        Abc_Print( -1, "Abc_CommandAbc9PbaStart(): There is no AIG.\n" );
+        Abc_Print( -1, "Abc_CommandAbc9AbsRefine(): There is no AIG.\n" );
         return 1;
-    }
+    } 
     if ( Gia_ManRegNum(pAbc->pGia) == 0 )
     {
-        Abc_Print( -1, "Abc_CommandAbc9PbaStart(): The AIG is combinational.\n" );
+        Abc_Print( -1, "The network is combinational.\n" );
         return 0;
+    }
+    if ( pAbc->pCex == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9AbsRefine(): There is no counter-example.\n" );
+        return 1;
     } 
-    Gia_ManProofAbstractionStart( pAbc->pGia, pPars );
-    pAbc->Status = pPars->Status;
+    pAbc->Status = Gia_ManCexAbstractionRefine( pAbc->pGia, pAbc->pCex, fTryFour, fSensePath, fVerbose );
     Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
     return 0;
+
 usage:
-    Abc_Print( -2, "usage: &pba_start [-FC num] [-dvh]\n" );
-    Abc_Print( -2, "\t         computes initial flop map using proof-based abstraction\n" );
-    Abc_Print( -2, "\t-F num : the max number of timeframes for PBA [default = %d]\n", pPars->nFramesMax );
-    Abc_Print( -2, "\t-C num : the max number of conflicts by SAT solver for PBA [default = %d]\n", pPars->nConfMax );
-//    Abc_Print( -2, "\t-G num : the max number of timeframes for BMC [default = %d]\n", pPars->nFramesBmc );
-//    Abc_Print( -2, "\t-D num : the max number of conflicts by SAT solver for BMC [default = %d]\n", pPars->nConfMaxBmc );
-//    Abc_Print( -2, "\t-R num : the %% of abstracted flops when refinement stops (0<=num<=100) [default = %d]\n", pPars->nRatio );
-    Abc_Print( -2, "\t-d     : toggle dynamic unrolling of timeframes [default = %s]\n", pPars->fDynamic? "yes": "no" );
-//    Abc_Print( -2, "\t-e     : toggle extending abstraction using COI of flops [default = %s]\n", pPars->fExtend? "yes": "no" );
-//    Abc_Print( -2, "\t-s     : toggle skipping proof-based abstraction [default = %s]\n", pPars->fSkipProof? "yes": "no" );
-//    Abc_Print( -2, "\t-r     : toggle using BDD-based reachability for filtering [default = %s]\n", pPars->fUseBdds? "yes": "no" );
-//    Abc_Print( -2, "\t-p     : toggle using \"dprove\" for filtering [default = %s]\n", pPars->fUseDprove? "yes": "no" );
-//    Abc_Print( -2, "\t-f     : toggle starting BMC from a later frame [default = %s]\n", pPars->fUseStart? "yes": "no" );
-    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
-    Abc_Print( -2, "\t-h     : print the command usage\n");
+    Abc_Print( -2, "usage: &abs_refine [-tsvh]\n" );
+    Abc_Print( -2, "\t        refines the pre-computed flop map using the counter-example\n" );
+    Abc_Print( -2, "\t-t    : toggle trying four abstractions instead of one [default = %s]\n", fTryFour? "yes": "no" );
+    Abc_Print( -2, "\t-s    : toggle using the path sensitization algorithm [default = %s]\n", fSensePath? "yes": "no" );
+    Abc_Print( -2, "\t-v    : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h    : print the command usage\n");
     return 1;
-}
+} 
 
 /**Function*************************************************************
 
@@ -28316,16 +28046,40 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_CommandAbc9AbsDerive( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandAbc9AbsPba( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    Gia_Man_t * pTemp = NULL;
-    int c, fVerbose = 0;
-    extern Gia_Man_t * Gia_ManCexAbstractionDerive( Gia_Man_t * pGia );
+    int nFramesMax = (pAbc->nFrames >= 0) ? pAbc->nFrames : 20;
+    int nConfMax   = 100000;
+    int fVerbose   =      0;
+    int c;
+
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "FCvh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'F':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nFramesMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nFramesMax < 0 ) 
+                goto usage;
+            break;
+        case 'C':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nConfMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nConfMax < 0 ) 
+                goto usage;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -28337,7 +28091,7 @@ int Abc_CommandAbc9AbsDerive( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( pAbc->pGia == NULL )
     {
-        Abc_Print( -1, "Abc_CommandAbc9AbsDerive(): There is no AIG.\n" );
+        Abc_Print( -1, "Abc_CommandAbc9AbsRefine(): There is no AIG.\n" );
         return 1;
     } 
     if ( Gia_ManRegNum(pAbc->pGia) == 0 )
@@ -28345,17 +28099,24 @@ int Abc_CommandAbc9AbsDerive( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "The network is combinational.\n" );
         return 0;
     }
-    pTemp = Gia_ManCexAbstractionDerive( pAbc->pGia );
-    Abc_CommandUpdate9( pAbc, pTemp );
+    if ( pAbc->pGia->vFlopClasses == NULL )
+    {
+        Abc_Print( -1, "The flop map is not given.\n" );
+        return 0;
+    }
+    Gia_ManPbaPerform( pAbc->pGia, nFramesMax, nConfMax, fVerbose );
+//    Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &abs_derive [-vh]\n" );
-    Abc_Print( -2, "\t        performs abstraction using the pre-computed flop map\n" );
-    Abc_Print( -2, "\t-v    : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
-    Abc_Print( -2, "\t-h    : print the command usage\n");
+    Abc_Print( -2, "usage: &abs_pba [-FC num] [-vh]\n" );
+    Abc_Print( -2, "\t         refines abstracted flop map with proof-based abstraction\n" );
+    Abc_Print( -2, "\t-F num : the max number of timeframes to unroll [default = %d]\n", nFramesMax );
+    Abc_Print( -2, "\t-C num : the max number of SAT solver conflicts [default = %d]\n", nConfMax );
+    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
-}
+} 
 
 /**Function*************************************************************
 
@@ -28368,28 +28129,64 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_CommandAbc9AbsRefine( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandAbc9AbsCba( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    Gia_Man_t * pTemp = NULL;
+    Saig_ParBmc_t Pars, * pPars = &Pars;
     int c;
-    int fTryFour   = 1;
-    int fSensePath = 0;
-    int fVerbose   = 0;
-
-    extern int Gia_ManCexAbstractionRefine( Gia_Man_t * pGia, Abc_Cex_t * pCex, int fTryFour, int fSensePath, int fVerbose );
+    Saig_ParBmcSetDefaultParams( pPars );
+    pPars->nStart     = (pAbc->nFrames >= 0) ? pAbc->nFrames : 0;
+    pPars->nFramesMax = pPars->nStart + 10;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "tsvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "SFCTvh" ) ) != EOF )
     {
         switch ( c )
         {
-        case 't':
-            fTryFour ^= 1;
+        case 'S':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nStart = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nStart < 0 ) 
+                goto usage;
             break;
-        case 's':
-            fSensePath ^= 1;
+        case 'F':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nFramesMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nFramesMax < 0 ) 
+                goto usage;
+            break;
+        case 'C':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nConfLimit = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nConfLimit < 0 ) 
+                goto usage;
+            break;
+        case 'T':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nTimeOut = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nTimeOut < 0 ) 
+                goto usage;
             break;
         case 'v':
-            fVerbose ^= 1;
+            pPars->fVerbose ^= 1;
             break;
         case 'h':
             goto usage;
@@ -28399,7 +28196,7 @@ int Abc_CommandAbc9AbsRefine( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( pAbc->pGia == NULL )
     {
-        Abc_Print( -1, "Abc_CommandAbc9AbsRefine(): There is no AIG.\n" );
+        Abc_Print( -1, "Abc_CommandAbc9AbsCba(): There is no AIG.\n" );
         return 1;
     } 
     if ( Gia_ManRegNum(pAbc->pGia) == 0 )
@@ -28407,22 +28204,20 @@ int Abc_CommandAbc9AbsRefine( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "The network is combinational.\n" );
         return 0;
     }
-    if ( pAbc->pCex == NULL )
-    {
-        Abc_Print( -1, "Abc_CommandAbc9AbsRefine(): There is no counter-example.\n" );
-        return 1;
-    } 
-    pAbc->Status = Gia_ManCexAbstractionRefine( pAbc->pGia, pAbc->pCex, fTryFour, fSensePath, fVerbose );
+    pAbc->Status = Gia_ManCbaPerform( pAbc->pGia, pPars );
+    pAbc->nFrames = pPars->iFrame;
     Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &abs_refine [-tsvh]\n" );
-    Abc_Print( -2, "\t        refines the pre-computed flop map using the counter-example\n" );
-    Abc_Print( -2, "\t-t    : toggle trying four abstractions instead of one [default = %s]\n", fTryFour? "yes": "no" );
-    Abc_Print( -2, "\t-s    : toggle using the path sensitization algorithm [default = %s]\n", fSensePath? "yes": "no" );
-    Abc_Print( -2, "\t-v    : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
-    Abc_Print( -2, "\t-h    : print the command usage\n");
+    Abc_Print( -2, "usage: &abs_cba [-SFCT num] [-vh]\n" );
+    Abc_Print( -2, "\t         refines abstracted flop map with proof-based abstraction\n" );
+    Abc_Print( -2, "\t-S num : the starting time frame [default = %d]\n", pPars->nStart );
+    Abc_Print( -2, "\t-F num : the max number of timeframes to unroll [default = %d]\n", pPars->nFramesMax );
+    Abc_Print( -2, "\t-C num : the max number of SAT solver conflicts [default = %d]\n", pPars->nConfLimit );
+    Abc_Print( -2, "\t-T num : the time out in seconds [default = %d]\n", pPars->nTimeOut );
+    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
 } 
 
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 8741b791..0f1ee007 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -33,7 +33,6 @@
 #include "gia.h"
 #include "cec.h"
 #include "csw.h"
-#include "giaAbs.h"
 #include "pdr.h" 
 
 ABC_NAMESPACE_IMPL_START
@@ -3229,66 +3228,6 @@ ABC_PRT( "Time", clock() - clkTotal );
 
 /**Function*************************************************************
 
-  Synopsis    [Performs proof-based abstraction.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Ntk_t * Abc_NtkDarCegar( Abc_Ntk_t * pNtk, Gia_ParAbs_t * pPars )
-{
-    Abc_Ntk_t * pNtkAig;
-    Aig_Man_t * pMan, * pTemp;
-    assert( Abc_NtkIsStrash(pNtk) );
-    pMan = Abc_NtkToDar( pNtk, 0, 1 );
-    if ( pMan == NULL )
-        return NULL;
-
-    if ( pPars->fConstr )
-    {
-        printf( "This option is currently not implemented.\n" );
-        Aig_ManStop( pMan );
-        return NULL;
-    }
-    if ( pPars->fConstr )
-    {
-        if ( Saig_ManDetectConstrTest(pMan) )
-        {
-            printf( "Performing abstraction while dynamically adding constraints...\n" );
-            pMan = Saig_ManDupUnfoldConstrs( pTemp = pMan );
-            Aig_ManStop( pTemp );
-            pMan = Saig_ManConCexAbstraction( pTemp = pMan, pPars );
-        }
-        else
-        {
-            printf( "Constraints are not available. Performing abstraction w/o constraints.\n" );
-            pMan = Saig_ManCexAbstraction( pTemp = pMan, pPars );
-        }
-    }
-    else
-        pMan = Saig_ManCexAbstraction( pTemp = pMan, pPars );
-    if ( pTemp->pSeqModel )
-    {
-        ABC_FREE( pNtk->pModel );
-        ABC_FREE( pNtk->pSeqModel );
-        pNtk->pSeqModel = pTemp->pSeqModel; pTemp->pSeqModel = NULL;
-    }
-    Aig_ManStop( pTemp );
-    if ( pMan == NULL )
-        return NULL;
-
-    pNtkAig = Abc_NtkAfterTrim( pMan, pNtk );
-//    pNtkAig->pName = Extra_UtilStrsav(pNtk->pName);
-//    pNtkAig->pSpec = Extra_UtilStrsav(pNtk->pSpec);
-    Aig_ManStop( pMan );
-    return pNtkAig;
-}
-
-/**Function*************************************************************
-
   Synopsis    [Interplates two networks.]
 
   Description []
@@ -4316,13 +4255,7 @@ Abc_Ntk_t * Abc_NtkDarTestNtk( Abc_Ntk_t * pNtk )
     pMan = Abc_NtkToDar( pNtk, 0, 1 );
     if ( pMan == NULL )
         return NULL;
-/*
-    Aig_ManSetRegNum( pMan, pMan->nRegs );
-    pMan = Saig_ManCexAbstraction( pTemp = pMan, 5, 10000, 0, 0, 0, -1, -1, 99, fUseBdds, fUseDprove, 0, 1 );
-    Aig_ManStop( pTemp );
-    if ( pMan == NULL )
-        return NULL;
-*/
+
 /*
     Aig_ManSetRegNum( pMan, pMan->nRegs );
     pMan = Saig_ManDualRail( pTemp = pMan, 1 );
diff --git a/src/base/cmd/cmdPlugin.c b/src/base/cmd/cmdPlugin.c
index 5617e75d..45533589 100644
--- a/src/base/cmd/cmdPlugin.c
+++ b/src/base/cmd/cmdPlugin.c
@@ -560,8 +560,6 @@ int Cmd_CommandAbcPlugIn( Abc_Frame_t * pAbc, int argc, char ** argv )
         pAbc->Status  = Abc_ManReadStatus( pFileOut, "result:" );
         // get bug-free depth
         pAbc->nFrames = Abc_ManReadInteger( pFileOut, "bug-free-depth:" );
-//        if ( pAbc->nFrames == -1 )
-//            printf( "Gia_ManCexAbstractionStartNew(): Cannot read the number of frames covered by BMC.\n" );
         // get abstraction
         pAbc->pGia->vFlopClasses = Abc_ManReadBinary( pFileOut, "abstraction:" );
         // get counter-example