Version abc81027

11 files changed, 684 insertions, 259 deletions

diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c
index a1c3eb01..da138395 100644
--- a/src/aig/aig/aigMan.c
+++ b/src/aig/aig/aigMan.c
@@ -431,6 +431,7 @@ void Aig_ManSetRegNum( Aig_Man_t * p, int nRegs )
     p->nRegs = nRegs;
     p->nTruePis = Aig_ManPiNum(p) - nRegs;
     p->nTruePos = Aig_ManPoNum(p) - nRegs;
+    Aig_ManSetPioNumbers( p );
 }
 
 /**Function*************************************************************
diff --git a/src/aig/cnf/cnfMan.c b/src/aig/cnf/cnfMan.c
index 9059b9e5..7c24606c 100644
--- a/src/aig/cnf/cnfMan.c
+++ b/src/aig/cnf/cnfMan.c
@@ -122,6 +122,7 @@ Vec_Int_t * Cnf_DataCollectPiSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p )
 Cnf_Dat_t * Cnf_DataAlloc( Aig_Man_t * pAig, int nVars, int nClauses, int nLiterals )
 {
     Cnf_Dat_t * pCnf;
+    int i;
     pCnf = ALLOC( Cnf_Dat_t, 1 );
     memset( pCnf, 0, sizeof(Cnf_Dat_t) );
     pCnf->pMan = pAig;
@@ -132,7 +133,9 @@ Cnf_Dat_t * Cnf_DataAlloc( Aig_Man_t * pAig, int nVars, int nClauses, int nLiter
     pCnf->pClauses[0] = ALLOC( int, nLiterals );
     pCnf->pClauses[nClauses] = pCnf->pClauses[0] + nLiterals;
     pCnf->pVarNums = ALLOC( int, Aig_ManObjNumMax(pAig) );
-    memset( pCnf->pVarNums, 0xff, sizeof(int) * Aig_ManObjNumMax(pAig) );
+//    memset( pCnf->pVarNums, 0xff, sizeof(int) * Aig_ManObjNumMax(pAig) );
+    for ( i = 0; i < Aig_ManObjNumMax(pAig); i++ )
+        pCnf->pVarNums[i] = -1;
     return pCnf;
 }
 
@@ -196,7 +199,7 @@ void Cnf_DataLift( Cnf_Dat_t * p, int nVarsPlus )
     Aig_Obj_t * pObj;
     int v;
     Aig_ManForEachObj( p->pMan, pObj, v )
-        if ( p->pVarNums[pObj->Id] )
+        if ( p->pVarNums[pObj->Id] >= 0 )
             p->pVarNums[pObj->Id] += nVarsPlus;
     for ( v = 0; v < p->nLiterals; v++ )
         p->pClauses[0][v] += 2*nVarsPlus;
diff --git a/src/aig/cnf/cnfWrite.c b/src/aig/cnf/cnfWrite.c
index 3656aae3..860c7e3e 100644
--- a/src/aig/cnf/cnfWrite.c
+++ b/src/aig/cnf/cnfWrite.c
@@ -216,7 +216,9 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs )
 
     // create room for variable numbers
     pCnf->pVarNums = ALLOC( int, Aig_ManObjNumMax(p->pManAig) );
-    memset( pCnf->pVarNums, 0xff, sizeof(int) * Aig_ManObjNumMax(p->pManAig) );
+//    memset( pCnf->pVarNums, 0xff, sizeof(int) * Aig_ManObjNumMax(p->pManAig) );
+    for ( i = 0; i < Aig_ManObjNumMax(p->pManAig); i++ )
+        pCnf->pVarNums[i] = -1;
     // assign variables to the last (nOutputs) POs
     Number = 1;
     if ( nOutputs )
@@ -365,7 +367,9 @@ Cnf_Dat_t * Cnf_DeriveSimple( Aig_Man_t * p, int nOutputs )
 
     // create room for variable numbers
     pCnf->pVarNums = ALLOC( int, Aig_ManObjNumMax(p) );
-    memset( pCnf->pVarNums, 0xff, sizeof(int) * Aig_ManObjNumMax(p) );
+//    memset( pCnf->pVarNums, 0xff, sizeof(int) * Aig_ManObjNumMax(p) );
+    for ( i = 0; i < Aig_ManObjNumMax(p); i++ )
+        pCnf->pVarNums[i] = -1;
     // assign variables to the last (nOutputs) POs
     Number = 1;
     if ( nOutputs )
@@ -485,7 +489,9 @@ Cnf_Dat_t * Cnf_DeriveSimpleForRetiming( Aig_Man_t * p )
 
     // create room for variable numbers
     pCnf->pVarNums = ALLOC( int, Aig_ManObjNumMax(p) );
-    memset( pCnf->pVarNums, 0xff, sizeof(int) * Aig_ManObjNumMax(p) );
+//    memset( pCnf->pVarNums, 0xff, sizeof(int) * Aig_ManObjNumMax(p) );
+    for ( i = 0; i < Aig_ManObjNumMax(p); i++ )
+        pCnf->pVarNums[i] = -1;
     // assign variables to the last (nOutputs) POs
     Number = 1;
     Aig_ManForEachPo( p, pObj, i )
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index a6f5631b..02db900b 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -80,6 +80,7 @@ static inline Aig_Obj_t *  Saig_ObjLiToLo( Aig_Man_t * p, Aig_Obj_t * pObj )  {
 
 /*=== saigBmc.c ==========================================================*/
 extern int               Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fVerbose, int * piFrame );
+extern void              Saig_BmcPerform( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, int nConfMaxOne, int nConfMaxAll, int fVerbose );
 /*=== saigCone.c ==========================================================*/
 extern void              Saig_ManPrintCones( Aig_Man_t * p );
 /*=== saigDup.c ==========================================================*/
diff --git a/src/aig/saig/saigAbs.c b/src/aig/saig/saigAbs.c
index b1e36fcc..cfbba7e1 100644
--- a/src/aig/saig/saigAbs.c
+++ b/src/aig/saig/saigAbs.c
@@ -28,100 +28,102 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static inline Aig_Obj_t * Saig_ObjFrame( Aig_Obj_t ** ppMap, int nFrames, Aig_Obj_t * pObj, int i )                       { return ppMap[nFrames*pObj->Id + i];  }
-static inline void        Saig_ObjSetFrame( Aig_Obj_t ** ppMap, int nFrames, Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { ppMap[nFrames*pObj->Id + i] = pNode; }
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
-  Synopsis    [Create timeframes of the manager for BMC.]
+  Synopsis    [Creates SAT solver for BMC.]
 
-  Description [The resulting manager is combinational. The only PO is
-  the output of the last frame.]
+  Description []
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Saig_ManFramesBmcLast( Aig_Man_t * pAig, int nFrames, Aig_Obj_t *** pppMap )
+sat_solver * Saig_AbsCreateSolver( Cnf_Dat_t * pCnf, int nFrames )
 {
-    Aig_Man_t * pFrames;
-    Aig_Obj_t ** ppMap;
-    Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pResult;
-    int i, f;
-    assert( Saig_ManRegNum(pAig) > 0 );
-    // start the mapping
-    ppMap = *pppMap = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) * nFrames );
-    // start the manager
-    pFrames = Aig_ManStart( Aig_ManNodeNum(pAig) * nFrames );
-    // create variables for register outputs
-    Saig_ManForEachLo( pAig, pObj, i )
-    {
-//        pObj->pData = Aig_ManConst0( pFrames );
-        pObj->pData = Aig_ObjCreatePi( pFrames );
-        Saig_ObjSetFrame( ppMap, nFrames, pObj, 0, pObj->pData );
-    }
-    // add timeframes
-    pResult = Aig_ManConst0(pFrames);
+    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++ )
     {
-        // map the constant node
-        Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames );
-        Saig_ObjSetFrame( ppMap, nFrames, Aig_ManConst1(pAig), f, Aig_ManConst1(pAig)->pData );
-        // create PI nodes for this frame
-        Saig_ManForEachPi( pAig, pObj, i )
-        {
-            pObj->pData = Aig_ObjCreatePi( pFrames );
-            Saig_ObjSetFrame( ppMap, nFrames, pObj, f, pObj->pData );
-        }
-        // add internal nodes of this frame
-        Aig_ManForEachNode( pAig, pObj, i )
-        {
-            pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
-            Saig_ObjSetFrame( ppMap, nFrames, pObj, f, pObj->pData );
-        }
-        // OR the POs
-        Saig_ManForEachPo( pAig, pObj, i )
-            pResult = Aig_Or( pFrames, pResult, Aig_ObjChild0Copy(pObj) );
-        // create POs for this frame
-        if ( f == nFrames - 1 )
-        {
-//            Saig_ManForEachPo( pAig, pObj, i )
-//            {
-//               pObj->pData = Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) );
-//               Saig_ObjSetFrame( ppMap, nFrames, pObj, f, pObj->pData );
-//            }
-            break;
-        }
-        // save register inputs
-        Saig_ManForEachLi( pAig, pObj, i )
+        for ( i = 0; i < pCnf->nClauses; i++ )
         {
-            pObj->pData = Aig_ObjChild0Copy(pObj);
-            Saig_ObjSetFrame( ppMap, nFrames, pObj, f, pObj->pData );
+            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;
+            }
         }
-        // transfer to register outputs
-        Saig_ManForEachLiLo(  pAig, pObjLi, pObjLo, i )
+        // 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 )
         {
-            pObjLo->pData = pObjLi->pData;
-            Saig_ObjSetFrame( ppMap, nFrames, pObjLo, f, pObjLo->pData );
+            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 );
     }
-    Aig_ObjCreatePo( pFrames, pResult );
-    Aig_ManCleanup( pFrames );
-    // remove mapping for the nodes that are no longer there
-    for ( i = 0; i < Aig_ManObjNumMax(pAig) * nFrames; i++ )
-        if ( ppMap[i] && Aig_ObjIsNone( Aig_Regular(ppMap[i]) ) )
-            ppMap[i] = NULL;
-    return pFrames;
+    // 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    [Finds the set of variables involved in the UNSAT core.]
+  Synopsis    [Finds the set of clauses involved in the UNSAT core.]
 
   Description []
                
@@ -130,88 +132,40 @@ Aig_Man_t * Saig_ManFramesBmcLast( Aig_Man_t * pAig, int nFrames, Aig_Obj_t ***
   SeeAlso     []
 
 ***********************************************************************/
-int * Saig_ManFindUnsatVariables( Cnf_Dat_t * pCnf, int nRegs, int nConfMax, int fVerbose )
+Vec_Int_t * Saig_AbsSolverUnsatCore( sat_solver * pSat, int nConfMax, int fVerbose )
 {
+    Vec_Int_t * vCore;
     void * pSatCnf; 
     Intp_Man_t * pManProof;
-    Aig_Obj_t * pObj;
-    sat_solver * pSat;
-    Vec_Int_t * vCore;
-    int * pClause1, * pClause2, * pLit, * pVars, iClause, nVars;
-    int i, Lit, RetValue;
-    // create the SAT solver
-    pSat = sat_solver_new();
-    sat_solver_store_alloc( pSat ); 
-    sat_solver_setnvars( pSat, pCnf->nVars );
-    for ( i = 0; i < pCnf->nClauses; i++ )
-    {
-        if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
-        {
-            printf( "The BMC problem is trivially UNSAT.\n" );
-            sat_solver_delete( pSat );
-            return NULL;
-        }
-    }
-    Aig_ManForEachPi( pCnf->pMan, pObj, i )
-    {
-        if ( i == nRegs )
-            break;
-        assert( pCnf->pVarNums[pObj->Id] >= 0 );
-        Lit = toLitCond( pCnf->pVarNums[pObj->Id], 1 );
-        if ( !sat_solver_addclause( pSat, &Lit, &Lit+1 ) )
-            assert( 0 );
-    }
-    sat_solver_store_mark_roots( pSat ); 
+    int RetValue;
     // solve the problem
     RetValue = sat_solver_solve( pSat, NULL, NULL, (sint64)nConfMax, (sint64)0, (sint64)0, (sint64)0 );
     if ( RetValue == l_Undef )
     {
         printf( "Conflict limit is reached.\n" );
-        sat_solver_delete( pSat );
         return NULL;
     }
     if ( RetValue == l_True )
     {
         printf( "The BMC problem is SAT.\n" );
-        sat_solver_delete( pSat );
         return NULL;
     }
-    printf( "SAT solver returned UNSAT after %d conflicts.\n", pSat->stats.conflicts );
+    if ( fVerbose )
+        printf( "SAT solver returned UNSAT after %d conflicts.\n", pSat->stats.conflicts );
     assert( RetValue == l_False );
     pSatCnf = sat_solver_store_release( pSat ); 
-    sat_solver_delete( pSat );
     // derive the UNSAT core
     pManProof = Intp_ManAlloc();
     vCore = Intp_ManUnsatCore( pManProof, pSatCnf, fVerbose );
     Intp_ManFree( pManProof );
     Sto_ManFree( pSatCnf );
-    // derive the set of variables on which the core depends
-    // collect the variable numbers
-    nVars = 0;
-    pVars = ALLOC( int, pCnf->nVars );
-    memset( pVars, 0, sizeof(int) * pCnf->nVars );
-    Vec_IntForEachEntry( vCore, iClause, i )
-    {
-        pClause1 = pCnf->pClauses[iClause];
-        pClause2 = pCnf->pClauses[iClause+1];
-        for ( pLit = pClause1; pLit < pClause2; pLit++ )
-        {
-            if ( pVars[ (*pLit) >> 1 ] == 0 )
-                nVars++;
-            pVars[ (*pLit) >> 1 ] = 1;
-            if ( fVerbose )
-            printf( "%s%d ", ((*pLit) & 1)? "-" : "+", (*pLit) >> 1 );
-        }
-        if ( fVerbose )
-        printf( "\n" );
-    }
-    Vec_IntFree( vCore );
-    return pVars;
+    return vCore;
 }
 
+
 /**Function*************************************************************
 
-  Synopsis    [Labels nodes with the given CNF variable.]
+  Synopsis    [Performs proof-based abstraction using BMC of the given depth.]
 
   Description []
                
@@ -220,15 +174,44 @@ int * Saig_ManFindUnsatVariables( Cnf_Dat_t * pCnf, int nRegs, int nConfMax, int
   SeeAlso     []
 
 ***********************************************************************/
-void Saig_ManMarkIntoPresentVars_rec( Aig_Obj_t * pObj, Cnf_Dat_t * pCnf, int iVar )
+Vec_Int_t * Saig_AbsCollectRegisters( Cnf_Dat_t * pCnf, int nFrames, Vec_Int_t * vCore )
 {
-    int iVarThis = pCnf->pVarNums[pObj->Id];
-    if ( iVarThis >= 0 && iVarThis != iVar )
-        return;
-    assert( Aig_ObjIsNode(pObj) );
-    Saig_ManMarkIntoPresentVars_rec( Aig_ObjFanin0(pObj), pCnf, iVar );
-    Saig_ManMarkIntoPresentVars_rec( Aig_ObjFanin1(pObj), pCnf, iVar );
-    pCnf->pVarNums[pObj->Id] = iVar;
+    Aig_Obj_t * pObj;
+    Vec_Int_t * vFlops;
+    int * pVars, * pFlops;
+    int i, iClause, iReg, * piLit;
+    // mark register variables
+    pVars = 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 = 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 );
+    free( pFlops );
+    free( pVars );
+    return vFlops;
 }
 
 /**Function*************************************************************
@@ -244,65 +227,32 @@ void Saig_ManMarkIntoPresentVars_rec( Aig_Obj_t * pObj, Cnf_Dat_t * pCnf, int iV
 ***********************************************************************/
 Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fVerbose )
 {
+    Aig_Man_t * pResult;
     Cnf_Dat_t * pCnf;
+    sat_solver * pSat;
+    Vec_Int_t * vCore;
     Vec_Int_t * vFlops;
-    Aig_Man_t * pFrames, * pResult;
-    Aig_Obj_t ** ppAigToFrames;
-    Aig_Obj_t * pObj, * pObjFrame;
-    int f, i, * pUnsatCoreVars, clk = clock();
-    assert( Saig_ManPoNum(p) == 1 );
+    int clk = clock();
+    assert( Aig_ManRegNum(p) > 0 );
     Aig_ManSetPioNumbers( p );
     if ( fVerbose )
         printf( "Performing proof-based abstraction with %d frames and %d max conflicts.\n", nFrames, nConfMax );
-    // create the timeframes
-    pFrames = Saig_ManFramesBmcLast( p, nFrames, &ppAigToFrames );
-    printf( "AIG nodes = %d. Frames = %d.\n", Aig_ManNodeNum(p), Aig_ManNodeNum(pFrames) );
-    // convert them into CNF
-//    pCnf = Cnf_Derive( pFrames, 0 );
-    pCnf = Cnf_DeriveSimple( pFrames, 0 );
-    // collect CNF variables involved in UNSAT core
-    pUnsatCoreVars = Saig_ManFindUnsatVariables( pCnf, Saig_ManRegNum(p), nConfMax, 0 );
-    if ( pUnsatCoreVars == NULL )
+    // create CNF for the AIG
+    pCnf = Cnf_DeriveSimple( p, Aig_ManPoNum(p) );
+    // create SAT solver for the unrolled AIG
+    pSat = Saig_AbsCreateSolver( pCnf, nFrames );
+    // compute UNSAT core
+    vCore = Saig_AbsSolverUnsatCore( pSat, nConfMax, fVerbose );
+    sat_solver_delete( pSat );
+    if ( vCore == NULL )
     {
-        Aig_ManStop( pFrames );
         Cnf_DataFree( pCnf );
         return NULL;
     }
-    if ( fVerbose )
-    {
-        int Counter = 0;
-        for ( i = 0; i < pCnf->nVars; i++ )
-            Counter += pUnsatCoreVars[i];
-        printf( "The number of variables in the UNSAT core is %d (out of %d).\n", Counter, pCnf->nVars );
-    }
-    // map other nodes into existing CNF variables
-    Aig_ManForEachNode( pFrames, pObj, i )
-        if ( pCnf->pVarNums[pObj->Id] >= 0 )
-            Saig_ManMarkIntoPresentVars_rec( pObj, pCnf, pCnf->pVarNums[pObj->Id] );
-    // collect relevant registers
-    for ( f = 0; f < nFrames; f++ )
-    {
-        Saig_ManForEachLo( p, pObj, i )
-        {
-            pObjFrame = Saig_ObjFrame( ppAigToFrames, nFrames, pObj, f );
-            if ( pObjFrame == NULL )
-                continue;
-            pObjFrame = Aig_Regular(pObjFrame);
-            if ( Aig_ObjIsConst1( pObjFrame ) )
-                continue;
-            assert( pCnf->pVarNums[pObjFrame->Id] >= 0 );
-            if ( pUnsatCoreVars[ pCnf->pVarNums[pObjFrame->Id] ] )
-                pObj->fMarkA = 1;
-        }
-    }
-    // collect the flops
-    vFlops = Vec_IntAlloc( 1000 );
-    Saig_ManForEachLo( p, pObj, i )
-        if ( pObj->fMarkA )
-        {
-            pObj->fMarkA = 0;
-            Vec_IntPush( vFlops, i );
-        }
+    // collect registers
+    vFlops = Saig_AbsCollectRegisters( pCnf, nFrames, vCore );
+    Cnf_DataFree( pCnf );
+    Vec_IntFree( vCore );
     if ( fVerbose )
     {
         printf( "The number of relevant registers is %d (out of %d).\n", Vec_IntSize(vFlops), Aig_ManRegNum(p) );
@@ -310,14 +260,8 @@ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax,
     }
     // create the resulting AIG
     pResult = Saig_ManAbstraction( p, vFlops );
-    // cleanup
-    Aig_ManStop( pFrames );
-    Cnf_DataFree( pCnf );
-    free( ppAigToFrames );
-    free( pUnsatCoreVars );
     Vec_IntFree( vFlops );
     return pResult;
-
 }
 
 
diff --git a/src/aig/saig/saigBmc.c b/src/aig/saig/saigBmc.c
index 0bbf63f9..2248fb37 100644
--- a/src/aig/saig/saigBmc.c
+++ b/src/aig/saig/saigBmc.c
@@ -21,6 +21,7 @@
 #include "saig.h"
 #include "cnf.h"
 #include "satStore.h"
+#include "ssw.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -33,9 +34,9 @@ struct Saig_Bmc_t_
 {
     // parameters
     int                   nFramesMax;     // the max number of timeframes to consider
+    int                   nNodesMax;      // the max number of nodes to add
     int                   nConfMaxOne;    // the max number of conflicts at a target
     int                   nConfMaxAll;    // the max number of conflicts for all targets
-    int                   nNodesMax;      // the max number of nodes to add
     int                   fVerbose;       // enables verbose output
     // AIG managers
     Aig_Man_t *           pAig;           // the user's AIG manager
@@ -46,11 +47,14 @@ struct Saig_Bmc_t_
     Vec_Ptr_t *           vAig2Frm;       // mapping of AIG nodees into Frames nodes
     // SAT solver
     sat_solver *          pSat;           // SAT solver
-    Vec_Int_t *           vObj2Var;       // mapping of frames objects in CNF variables
     int                   nSatVars;       // the number of used SAT variables
+    Vec_Int_t *           vObj2Var;       // mapping of frames objects in CNF variables
+    // subproblems
     Vec_Ptr_t *           vTargets;       // targets to be solved in this interval
-    int                   iFramelast;     // last frame  
+    int                   iFrameLast;     // last frame  
     int                   iOutputLast;    // last output
+    int                   iFrameFail;     // failed frame 
+    int                   iOutputFail;    // failed output
 };
 
 static inline int         Saig_BmcSatNum( Saig_Bmc_t * p, Aig_Obj_t * pObj )                                { return Vec_IntGetEntry( p->vObj2Var, pObj->Id );  }
@@ -77,7 +81,7 @@ static inline Aig_Obj_t * Saig_BmcObjChild1( Saig_Bmc_t * p, Aig_Obj_t * pObj, i
   SeeAlso     []
 
 ***********************************************************************/
-Saig_Bmc_t * Saig_BmcManStart( Aig_Man_t * pAig, int nConfMaxOne, int nConfMaxAll, int nNodesMax, int fVerbose )
+Saig_Bmc_t * Saig_BmcManStart( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, int nConfMaxOne, int nConfMaxAll, int fVerbose )
 {
     Saig_Bmc_t * p;
     Aig_Obj_t * pObj;
@@ -86,10 +90,10 @@ Saig_Bmc_t * Saig_BmcManStart( Aig_Man_t * pAig, int nConfMaxOne, int nConfMaxAl
     p = (Saig_Bmc_t *)malloc( sizeof(Saig_Bmc_t) );
     memset( p, 0, sizeof(Saig_Bmc_t) );
     // set parameters
-    p->nFramesMax   = 1000000;
+    p->nFramesMax   = nFramesMax;
+    p->nNodesMax    = nNodesMax;
     p->nConfMaxOne  = nConfMaxOne;
     p->nConfMaxAll  = nConfMaxAll;
-    p->nNodesMax    = nNodesMax;
     p->fVerbose     = fVerbose;
     p->pAig         = pAig;
     p->nObjs        = Aig_ManObjNumMax(pAig);
@@ -103,15 +107,17 @@ Saig_Bmc_t * Saig_BmcManStart( Aig_Man_t * pAig, int nConfMaxOne, int nConfMaxAl
     Saig_ManForEachLo( pAig, pObj, i )
         Saig_BmcObjSetFrame( p, pObj, 0, Aig_ManConst0(p->pFrm) ); 
     // create SAT solver
+    p->nSatVars     = 1;
     p->pSat         = sat_solver_new();
     sat_solver_setnvars( p->pSat, 2000 );
-    p->nSatVars = 1;
     Lit = toLit( p->nSatVars );
     sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
     Saig_BmcSetSatNum( p, Aig_ManConst1(p->pFrm), p->nSatVars++ );
     // other data structures
     p->vTargets     = Vec_PtrAlloc( 0 );
     p->vVisited     = Vec_PtrAlloc( 0 );
+    p->iOutputFail  = -1;
+    p->iFrameFail   = -1;
     return p;
 }
 
@@ -174,15 +180,15 @@ Aig_Obj_t * Saig_BmcIntervalExplore_rec( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i
             p1 = Saig_BmcObjChild1( p, pObj, i );
 
         if ( p0 == Aig_Not(p1) )
-            pRes = Aig_Not(pConst1);
+            pRes = Aig_ManConst0(p->pFrm);
         else if ( Aig_Regular(p0) == pConst1 )
-            pRes = (p0 == pConst1) ? p1 : Aig_Not(pConst1);
+            pRes = (p0 == pConst1) ? p1 : Aig_ManConst0(p->pFrm);
         else if ( Aig_Regular(p1) == pConst1 )
-            pRes = (p1 == pConst1) ? p0 : Aig_Not(pConst1);
+            pRes = (p1 == pConst1) ? p0 : Aig_ManConst0(p->pFrm);
         else 
             pRes = AIG_VISITED;
 
-        if ( pRes != pConst1 && pRes != Aig_Not(pConst1) )
+        if ( pRes != AIG_VISITED && !Aig_ObjIsConst1(Aig_Regular(pRes)) )
             pRes = AIG_VISITED;
     }
     Saig_BmcObjSetFrame( p, pObj, i, pRes );
@@ -222,6 +228,7 @@ Aig_Obj_t * Saig_BmcIntervalConstruct_rec( Saig_Bmc_t * p, Aig_Obj_t * pObj, int
         Saig_BmcIntervalConstruct_rec( p, Aig_ObjFanin1(pObj), i );
         pRes = Aig_And( p->pFrm, Saig_BmcObjChild0(p, pObj, i), Saig_BmcObjChild1(p, pObj, i) );
     }
+    assert( pRes != AIG_VISITED );
     Saig_BmcObjSetFrame( p, pObj, i, pRes );
     return pRes;
 }
@@ -239,23 +246,30 @@ Aig_Obj_t * Saig_BmcIntervalConstruct_rec( Saig_Bmc_t * p, Aig_Obj_t * pObj, int
 ***********************************************************************/
 void Saig_BmcInterval( Saig_Bmc_t * p )
 {
-    Aig_Obj_t * pTarget, * pObj;
-    int i, nNodes = Aig_ManNodeNum( p->pFrm );
+    Aig_Obj_t * pTarget;
+//    Aig_Obj_t * pObj;
+//    int i;
+    int nNodes = Aig_ManObjNum( p->pFrm );
     Vec_PtrClear( p->vTargets );
-    for ( ; p->iFramelast < p->nFramesMax; p->iFramelast++, p->iOutputLast = 0 )
+    for ( ; p->iFrameLast < p->nFramesMax; p->iFrameLast++, p->iOutputLast = 0 )
     {
         if ( p->iOutputLast == 0 )
         {
-            Saig_BmcObjSetFrame( p, Aig_ManConst1(p->pAig), p->iFramelast, Aig_ManConst1(p->pFrm) );
-            Saig_ManForEachPi( p->pAig, pObj, i )
-                Saig_BmcObjSetFrame( p, pObj, p->iFramelast, Aig_ObjCreatePi(p->pFrm) ); 
+            Saig_BmcObjSetFrame( p, Aig_ManConst1(p->pAig), p->iFrameLast, Aig_ManConst1(p->pFrm) );
+//            Saig_ManForEachPi( p->pAig, pObj, i )
+//                Saig_BmcObjSetFrame( p, pObj, p->iFrameLast, Aig_ObjCreatePi(p->pFrm) ); 
         }
         for ( ; p->iOutputLast < Saig_ManPoNum(p->pAig); p->iOutputLast++ )
         {
-            if ( Aig_ManNodeNum(p->pFrm) >= nNodes + p->nNodesMax )
+            if ( Aig_ManObjNum(p->pFrm) >= nNodes + p->nNodesMax )
                 return;
-            Saig_BmcIntervalExplore_rec( p, Aig_ManPo(p->pAig, p->iOutputLast), p->nFramesMax );
-            pTarget = Saig_BmcIntervalConstruct_rec( p, Aig_ManPo(p->pAig, p->iOutputLast), p->nFramesMax );
+            Saig_BmcIntervalExplore_rec( p, Aig_ManPo(p->pAig, p->iOutputLast), p->iFrameLast );
+            pTarget = Saig_BmcIntervalConstruct_rec( p, Aig_ManPo(p->pAig, p->iOutputLast), p->iFrameLast );
+
+            /////////
+//            if ( Aig_ObjIsConst1(Aig_Regular(pTarget)) )
+//                continue;
+
             Vec_PtrPush( p->vTargets, pTarget );
         }
     }
@@ -281,6 +295,7 @@ Aig_Obj_t * Saig_BmcIntervalToAig_rec( Saig_Bmc_t * p, Aig_Man_t * pNew, Aig_Obj
         return pObj->pData = Aig_ObjCreatePi(pNew);
     Saig_BmcIntervalToAig_rec( p, pNew, Aig_ObjFanin0(pObj) );
     Saig_BmcIntervalToAig_rec( p, pNew, Aig_ObjFanin1(pObj) );
+    assert( pObj->pData == NULL );
     return pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
 }
 
@@ -300,13 +315,18 @@ Aig_Man_t * Saig_BmcIntervalToAig( Saig_Bmc_t * p )
     Aig_Man_t * pNew;
     Aig_Obj_t * pObj, * pObjNew;
     int i;
+    Aig_ManForEachObj( p->pFrm, pObj, i )
+        assert( pObj->pData == NULL );
+
     pNew = Aig_ManStart( p->nNodesMax );
     Aig_ManConst1(p->pFrm)->pData = Aig_ManConst1(pNew);
     Vec_PtrClear( p->vVisited );
     Vec_PtrPush( p->vVisited, Aig_ManConst1(p->pFrm) );
     Vec_PtrForEachEntry( p->vTargets, pObj, i )
     {
+//        assert( !Aig_ObjIsConst1(Aig_Regular(pObj)) );
         pObjNew = Saig_BmcIntervalToAig_rec( p, pNew, Aig_Regular(pObj) );
+        assert( !Aig_IsComplement(pObjNew) );
         Aig_ObjCreatePo( pNew, pObjNew );
     }
     return pNew;
@@ -329,12 +349,14 @@ void Saig_BmcLoadCnf( Saig_Bmc_t * p, Cnf_Dat_t * pCnf )
     int i, Lits[2], VarNumOld, VarNumNew;
     Vec_PtrForEachEntry( p->vVisited, pObj, i )
     {
-        pObjNew   = pObj->pData;
+        // get the new variable of this node
+        pObjNew     = pObj->pData;
         pObj->pData = NULL;
-        VarNumNew = pCnf->pVarNums[ pObjNew->Id ];
+        VarNumNew   = pCnf->pVarNums[ pObjNew->Id ];
         if ( VarNumNew == -1 )
             continue;
-        VarNumOld = Saig_BmcSatNum( p, pObj );
+        // get the old variable of this node
+        VarNumOld   = Saig_BmcSatNum( p, pObj );
         if ( VarNumOld == 0 )
         {
             Saig_BmcSetSatNum( p, pObj, VarNumNew );
@@ -369,11 +391,88 @@ void Saig_BmcLoadCnf( Saig_Bmc_t * p, Cnf_Dat_t * pCnf )
   SeeAlso     []
 
 ***********************************************************************/
+void Saig_BmcDeriveFailed( Saig_Bmc_t * p, int iTargetFail )
+{
+    int k;
+    p->iOutputFail = p->iOutputLast;
+    p->iFrameFail  = p->iFrameLast;
+    for ( k = Vec_PtrSize(p->vTargets); k > iTargetFail; k-- )
+    {
+        if ( p->iOutputFail == 0 )
+        {
+            p->iOutputFail = Saig_ManPoNum(p->pAig);
+            p->iFrameFail--;
+        }
+        p->iOutputFail--;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Solves targets with the given resource limit.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ssw_Cex_t * Saig_BmcGenerateCounterExample( Saig_Bmc_t * p )
+{
+    Ssw_Cex_t * pCex;
+    Aig_Obj_t * pObj, * pObjFrm;
+    int i, f, iVarNum;
+    // start the counter-example
+    pCex = Ssw_SmlAllocCounterExample( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), p->iFrameFail+1 );
+    pCex->iFrame = p->iFrameFail;
+    pCex->iPo    = p->iOutputFail;
+    // copy the bit data
+    for ( f = 0; f <= p->iFrameFail; f++ )
+    {
+        Saig_ManForEachPi( p->pAig, pObj, i )
+        {
+            pObjFrm = Saig_BmcObjFrame( p, pObj, f );
+            if ( pObjFrm == NULL )
+                continue;
+            iVarNum = Saig_BmcSatNum( p, pObjFrm );
+            if ( iVarNum == 0 )
+                continue;
+            if ( sat_solver_var_value( p->pSat, iVarNum ) )
+                Aig_InfoSetBit( pCex->pData, pCex->nRegs + Saig_ManPiNum(p->pAig) * f + i );
+        }
+    }
+    // verify the counter example
+    if ( !Ssw_SmlRunCounterExample( p->pAig, pCex ) )
+    {
+        printf( "Saig_BmcGenerateCounterExample(): Counter-example is invalid.\n" );
+        Ssw_SmlFreeCounterExample( pCex );
+        pCex = NULL;
+    }
+    return pCex;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Solves targets with the given resource limit.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Saig_BmcSolveTargets( Saig_Bmc_t * p )
 {
     Aig_Obj_t * pObj;
     int i, VarNum, Lit, RetValue;
     assert( Vec_PtrSize(p->vTargets) > 0 );
+    if ( p->pSat->qtail != p->pSat->qhead )
+    {
+        RetValue = sat_solver_simplify(p->pSat);
+        assert( RetValue != 0 );
+    }
     Vec_PtrForEachEntry( p->vTargets, pObj, i )
     {
         if ( p->pSat->stats.conflicts > p->nConfMaxAll )
@@ -386,6 +485,8 @@ int Saig_BmcSolveTargets( Saig_Bmc_t * p )
         if ( RetValue == l_Undef ) // undecided
             return l_Undef;
         // generate counter-example
+        Saig_BmcDeriveFailed( p, i );
+        p->pAig->pSeqModel = Saig_BmcGenerateCounterExample( p );
         return l_True;
     }
     return l_False;
@@ -393,6 +494,28 @@ int Saig_BmcSolveTargets( Saig_Bmc_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Saig_BmcAddTargetsAsPos( Saig_Bmc_t * p )
+{
+    Aig_Obj_t * pObj;
+    int i;
+    Vec_PtrForEachEntry( p->vTargets, pObj, i )
+        Aig_ObjCreatePo( p->pFrm, pObj );
+    Aig_ManPrintStats( p->pFrm );
+    Aig_ManCleanup( p->pFrm );
+    Aig_ManPrintStats( p->pFrm );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Performs BMC with the given parameters.]
 
   Description []
@@ -402,17 +525,27 @@ int Saig_BmcSolveTargets( Saig_Bmc_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Saig_BmcPerform( Aig_Man_t * pAig, int nConfMaxOne, int nConfMaxAll, int nNodesMax, int fVerbose )
+void Saig_BmcPerform( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, int nConfMaxOne, int nConfMaxAll, int fVerbose )
 {
     Saig_Bmc_t * p;
     Aig_Man_t * pNew;
     Cnf_Dat_t * pCnf;
-    int RetValue, clk = clock();
-    p = Saig_BmcManStart( pAig, nConfMaxOne, nConfMaxAll, nNodesMax, fVerbose );
-    while ( 1 )
+    int Iter, RetValue, clk = clock(), clk2;
+    p = Saig_BmcManStart( pAig, nFramesMax, nNodesMax, nConfMaxOne, nConfMaxAll, fVerbose );
+    if ( fVerbose )
+    {
+        printf( "AIG:  PI/PO/Reg = %d/%d/%d.  Node = %6d. Lev = %5d.\n", 
+            Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), Saig_ManRegNum(pAig),
+            Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig) );
+        printf( "Params: FramesMax = %d. NodesDelta = %d. ConfMaxOne = %d. ConfMaxAll = %d.\n", 
+            nFramesMax, nNodesMax, nConfMaxOne, nConfMaxAll );
+    }
+    for ( Iter = 0; ; Iter++ )
     {
-        // add new logic slice to frames
+        clk2 = clock();
+        // add new logic interval to frames
         Saig_BmcInterval( p );
+//        Saig_BmcAddTargetsAsPos( p );
         if ( Vec_PtrSize(p->vTargets) == 0 )
             break;
         // convert logic slice into new AIG
@@ -427,20 +560,30 @@ void Saig_BmcPerform( Aig_Man_t * pAig, int nConfMaxOne, int nConfMaxAll, int nN
         Aig_ManStop( pNew );
         // solve the targets
         RetValue = Saig_BmcSolveTargets( p );
+        if ( fVerbose )
+        {
+            printf( "%3d : F = %3d. O = %3d.  And = %7d. Var = %7d. Conf = %7d. ", 
+                Iter, p->iFrameLast, p->iOutputLast, Aig_ManNodeNum(p->pFrm), p->nSatVars, (int)p->pSat->stats.conflicts );   
+            PRT( "Time", clock() - clk2 );
+        }
         if ( RetValue != l_False )
             break;
     }
     if ( RetValue == l_True )
-        printf( "BMC failed for output %d in frame %d.  ", p->iOutputLast, p->iFramelast );
+        printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", 
+            p->iOutputFail, p->iFrameFail );
     else // if ( RetValue == l_False || RetValue == l_Undef )
-        printf( "BMC completed for %d timeframes.  ", p->iFramelast );
+        printf( "No output was asserted in %d frames.  ", p->iFrameLast );
     PRT( "Time", clock() - clk );
-    if ( p->iFramelast >= p->nFramesMax )
-        printf( "Reached limit on the number of timeframes (%d).\n", p->nFramesMax );
-    else if ( p->pSat->stats.conflicts > p->nConfMaxAll )
-        printf( "Reached global conflict limit (%d).\n", p->nConfMaxAll );
-    else
-        printf( "Reached local conflict limit (%d).\n", p->nConfMaxOne );
+    if ( RetValue != l_True )
+    {
+        if ( p->iFrameLast >= p->nFramesMax )
+            printf( "Reached limit on the number of timeframes (%d).\n", p->nFramesMax );
+        else if ( p->pSat->stats.conflicts > p->nConfMaxAll )
+            printf( "Reached global conflict limit (%d).\n", p->nConfMaxAll );
+        else
+            printf( "Reached local conflict limit (%d).\n", p->nConfMaxOne );
+    }
     Saig_BmcManStop( p );
 }
 
diff --git a/src/aig/saig/saigDup.c b/src/aig/saig/saigDup.c
index 165a08f2..61ea6ca0 100644
--- a/src/aig/saig/saigDup.c
+++ b/src/aig/saig/saigDup.c
@@ -108,13 +108,12 @@ Aig_Man_t * Saig_ManAbstraction( Aig_Man_t * pAig, Vec_Int_t * vFlops )
             pObj->fMarkA = 0;
             pObj->pData = Aig_ObjCreatePi( pAigNew );
         }
-    // add internal nodes of this frame
+    // add internal nodes 
     Aig_ManForEachNode( pAig, pObj, i )
         pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
     // create POs
-    Aig_ManForEachPo( pAig, pObj, i )
-        if ( !pObj->fMarkA )
-            Aig_ObjCreatePo( pAigNew, Aig_ObjChild0Copy(pObj) );
+    Saig_ManForEachPo( pAig, pObj, i )
+        Aig_ObjCreatePo( pAigNew, Aig_ObjChild0Copy(pObj) );
     // create LIs
     Aig_ManForEachPo( pAig, pObj, i )
         if ( pObj->fMarkA )
@@ -122,8 +121,8 @@ Aig_Man_t * Saig_ManAbstraction( Aig_Man_t * pAig, Vec_Int_t * vFlops )
             pObj->fMarkA = 0;
             Aig_ObjCreatePo( pAigNew, Aig_ObjChild0Copy(pObj) );
         }
-    Aig_ManCleanup( pAigNew );
     Aig_ManSetRegNum( pAigNew, Vec_IntSize(vFlops) );
+    Aig_ManSeqCleanup( pAigNew );
     return pAigNew;
 }
 
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index f12e94e1..ac417d14 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -212,10 +212,13 @@ static int Abc_CommandProve          ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandIProve         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandDebug          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandBmc            ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandBmc2           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandBmcInter       ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandIndcut         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandEnlarge        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandInduction      ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPBAbstraction  ( Abc_Frame_t * pAbc, int argc, char ** argv );
+
 
 static int Abc_CommandTraceStart     ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandTraceCheck     ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -480,10 +483,12 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Verification", "iprove",        Abc_CommandIProve,           1 );
     Cmd_CommandAdd( pAbc, "Verification", "debug",         Abc_CommandDebug,            0 );
     Cmd_CommandAdd( pAbc, "Verification", "bmc",           Abc_CommandBmc,              0 );
+    Cmd_CommandAdd( pAbc, "Verification", "bmc2",          Abc_CommandBmc2,             0 );
     Cmd_CommandAdd( pAbc, "Verification", "int",           Abc_CommandBmcInter,         0 );
     Cmd_CommandAdd( pAbc, "Verification", "indcut",        Abc_CommandIndcut,           0 );
     Cmd_CommandAdd( pAbc, "Verification", "enlarge",       Abc_CommandEnlarge,          1 );
     Cmd_CommandAdd( pAbc, "Verification", "ind",           Abc_CommandInduction,        0 );
+    Cmd_CommandAdd( pAbc, "Verification", "abs",           Abc_CommandPBAbstraction,    0 );
 
 
     Cmd_CommandAdd( pAbc, "ABC8",         "*r",            Abc_CommandAbc8Read,         0 );
@@ -7936,7 +7941,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
 */
 
-/*
+
     pNtkRes = Abc_NtkDarTestNtk( pNtk );
     if ( pNtkRes == NULL )
     {
@@ -7945,9 +7950,9 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     // replace the current network
     Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
-*/
 
-    Abc_NtkDarTest( pNtk );
+
+//    Abc_NtkDarTest( pNtk );
 
     return 0;
 usage:
@@ -16059,7 +16064,7 @@ usage:
 
   Description []
                
-  SideEffects []
+  SideEffects [] 
 
   SeeAlso     []
 
@@ -16072,25 +16077,29 @@ int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv )
     int nFrames;
     int nSizeMax;
     int nBTLimit;
+    int nBTLimitAll;
+    int nNodeDelta;
     int fRewrite;
     int fNewAlgo;
     int fVerbose;
 
-    extern int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fNewAlgo, int fVerbose );
+    extern int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nNodeDelta, int nBTLimit, int nBTLimitAll, int fRewrite, int fNewAlgo, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    nFrames  = 20;
-    nSizeMax = 100000;
-    nBTLimit = 10000;
-    fRewrite = 0;
-    fNewAlgo = 1;
-    fVerbose = 0;
+    nFrames     =       20;
+    nSizeMax    =   100000;
+    nBTLimit    =    10000;
+    nBTLimitAll = 10000000;
+    nNodeDelta  =     1000;
+    fRewrite    =        0;
+    fNewAlgo    =        1;
+    fVerbose    =        0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "FNCravh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "FNCGDrvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -16127,6 +16136,28 @@ int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nBTLimit < 0 ) 
                 goto usage;
             break;
+        case 'G':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-G\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nBTLimitAll = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nBTLimitAll < 0 ) 
+                goto usage;
+            break;
+        case 'D':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-D\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nNodeDelta = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nNodeDelta < 0 ) 
+                goto usage;
+            break;
         case 'r':
             fRewrite ^= 1;
             break;
@@ -16148,7 +16179,7 @@ int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
     if ( !Abc_NtkIsStrash(pNtk) )
-    {
+    { 
         fprintf( stdout, "Currently only works for structurally hashed circuits.\n" );
         return 0;
     }
@@ -16157,17 +16188,169 @@ int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( stdout, "Does not work for combinational networks.\n" );
         return 0;
     }
-    Abc_NtkDarBmc( pNtk, nFrames, nSizeMax, nBTLimit, fRewrite, fNewAlgo, fVerbose );
+    Abc_NtkDarBmc( pNtk, nFrames, nSizeMax, nNodeDelta, nBTLimit, nBTLimitAll, fRewrite, fNewAlgo, fVerbose );
     return 0;
 
 usage:
-    fprintf( pErr, "usage: bmc [-FNC num] [-ravh]\n" );
-    fprintf( pErr, "\t         perform bounded model checking\n" );
+//    fprintf( pErr, "usage: bmc [-FNCGD num] [-ravh]\n" );
+    fprintf( pErr, "usage: bmc [-FNC num] [-rvh]\n" );
+    fprintf( pErr, "\t         performs bounded model checking with static unrolling\n" );
     fprintf( pErr, "\t-F num : the number of time frames [default = %d]\n", nFrames );
     fprintf( pErr, "\t-N num : the max number of nodes in the frames [default = %d]\n", nSizeMax );
     fprintf( pErr, "\t-C num : the max number of conflicts at a node [default = %d]\n", nBTLimit );
+//    fprintf( pErr, "\t-G num : the max number of conflicts globally [default = %d]\n", nBTLimitAll );
+//    fprintf( pErr, "\t-D num : the delta in the number of nodes [default = %d]\n", nNodeDelta );
     fprintf( pErr, "\t-r     : toggle the use of rewriting [default = %s]\n", fRewrite? "yes": "no" );
-    fprintf( pErr, "\t-a     : toggle SAT sweeping and SAT solving [default = %s]\n", fNewAlgo? "SAT solving": "SAT sweeping" );
+//    fprintf( pErr, "\t-a     : toggle SAT sweeping and SAT solving [default = %s]\n", fNewAlgo? "SAT solving": "SAT sweeping" );
+    fprintf( pErr, "\t-v     : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+ 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects [] 
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandBmc2( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;
+    int c;
+    int nFrames;
+    int nSizeMax;
+    int nBTLimit;
+    int nBTLimitAll;
+    int nNodeDelta;
+    int fRewrite;
+    int fNewAlgo;
+    int fVerbose;
+
+    extern int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nNodeDelta, int nBTLimit, int nBTLimitAll, int fRewrite, int fNewAlgo, int fVerbose );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    nFrames     =     1000;
+    nSizeMax    =   200000;
+    nBTLimit    =    10000;
+    nBTLimitAll = 10000000;
+    nNodeDelta  =     1000;
+    fRewrite    =        0;
+    fNewAlgo    =        0;
+    fVerbose    =        0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "FNCGDrvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'F':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nFrames = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nFrames < 0 ) 
+                goto usage;
+            break;
+        case 'N':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nSizeMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nSizeMax < 0 ) 
+                goto usage;
+            break;
+        case 'C':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nBTLimit = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nBTLimit < 0 ) 
+                goto usage;
+            break;
+        case 'G':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-G\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nBTLimitAll = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nBTLimitAll < 0 ) 
+                goto usage;
+            break;
+        case 'D':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-D\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nNodeDelta = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nNodeDelta < 0 ) 
+                goto usage;
+            break;
+        case 'r':
+            fRewrite ^= 1;
+            break;
+        case 'a':
+            fNewAlgo ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+    if ( !Abc_NtkIsStrash(pNtk) )
+    { 
+        fprintf( stdout, "Currently only works for structurally hashed circuits.\n" );
+        return 0;
+    }
+    if ( Abc_NtkLatchNum(pNtk) == 0 )
+    {
+        fprintf( stdout, "Does not work for combinational networks.\n" );
+        return 0;
+    }
+    Abc_NtkDarBmc( pNtk, nFrames, nSizeMax, nNodeDelta, nBTLimit, nBTLimitAll, fRewrite, fNewAlgo, fVerbose );
+    return 0;
+
+usage:
+//    fprintf( pErr, "usage: bmc2 [-FNCGD num] [-ravh]\n" );
+    fprintf( pErr, "usage: bmc2 [-FCGD num] [-vh]\n" );
+    fprintf( pErr, "\t         performs bounded model checking with dynamic unrolling\n" );
+    fprintf( pErr, "\t-F num : the max number of time frames [default = %d]\n", nFrames );
+//    fprintf( pErr, "\t-N num : the max number of nodes in the frames [default = %d]\n", nSizeMax );
+    fprintf( pErr, "\t-C num : the max number of conflicts at a node [default = %d]\n", nBTLimit );
+    fprintf( pErr, "\t-G num : the max number of conflicts globally [default = %d]\n", nBTLimitAll );
+    fprintf( pErr, "\t-D num : the delta in the number of nodes [default = %d]\n", nNodeDelta );
+//    fprintf( pErr, "\t-r     : toggle the use of rewriting [default = %s]\n", fRewrite? "yes": "no" );
+//    fprintf( pErr, "\t-a     : toggle SAT sweeping and SAT solving [default = %s]\n", fNewAlgo? "SAT solving": "SAT sweeping" );
     fprintf( pErr, "\t-v     : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
@@ -16616,7 +16799,7 @@ int Abc_CommandInduction( Abc_Frame_t * pAbc, int argc, char ** argv )
     int nConfMax;
     int fVerbose;
     int c;
-    extern void Abc_NtkDarLocalize( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fVerbose );
+    extern void Abc_NtkDarInduction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -16684,7 +16867,7 @@ int Abc_CommandInduction( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // modify the current network
-    Abc_NtkDarLocalize( pNtk, nFramesMax, nConfMax, fVerbose );
+    Abc_NtkDarInduction( pNtk, nFramesMax, nConfMax, fVerbose );
     return 0;
 usage:
     fprintf( pErr, "usage: ind [-FC num] [-vh]\n" );
@@ -16695,6 +16878,107 @@ usage:
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
 }
+ 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandPBAbstraction( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk, * pNtkRes;
+    int nFramesMax;
+    int nConfMax;
+    int fVerbose;
+    int c;
+    extern Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fVerbose );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    nFramesMax =    10;
+    nConfMax   = 10000;
+    fVerbose   =     1;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "FCvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'F':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "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 )
+            {
+                fprintf( pErr, "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;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+    if ( Abc_NtkIsComb(pNtk) )
+    {
+        fprintf( pErr, "The network is combinational.\n" );
+        return 0;
+    }
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( stdout, "Currently only works for structurally hashed circuits.\n" );
+        return 0;
+    }
+
+    // modify the current network
+    pNtkRes = Abc_NtkDarPBAbstraction( pNtk, nFramesMax, nConfMax, fVerbose );
+    if ( pNtkRes == NULL )
+    {
+        fprintf( pErr, "Target enlargement has failed.\n" );
+        return 1;
+    }
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+usage:
+    fprintf( pErr, "usage: abs [-FC num] [-vh]\n" );
+    fprintf( pErr, "\t         proof-based abstraction from UNSAT core of the BMC instance\n" );
+    fprintf( pErr, "\t-F num : the max number of timeframes [default = %d]\n", nFramesMax );
+    fprintf( pErr, "\t-C num : the max number of conflicts by SAT solver [default = %d]\n", nConfMax );
+    fprintf( pErr, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
 
 
 /**Function*************************************************************
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 3e7f3b65..22f4b45c 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -1462,7 +1462,7 @@ Abc_Ntk_t * Abc_NtkDarLcorrNew( Abc_Ntk_t * pNtk, int nVarsMax, int nConfMax, in
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fNewAlgo, int fVerbose )
+int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nNodeDelta, int nBTLimit, int nBTLimitAll, int fRewrite, int fNewAlgo, int fVerbose )
 {
     Aig_Man_t * pMan;
     int status, RetValue = -1, clk = clock();
@@ -1511,6 +1511,7 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nBTLimit, in
             RetValue = 1;
         }
 */
+/*
         int iFrame;
         RetValue = Ssw_BmcDynamic( pMan, nFrames, nBTLimit, fVerbose, &iFrame );
         FREE( pNtk->pModel );
@@ -1525,6 +1526,11 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nBTLimit, in
             Fra_Cex_t * pCex = pNtk->pSeqModel;
             printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", pCex->iPo, pCex->iFrame );
         }
+*/
+        Saig_BmcPerform( pMan, nFrames, nNodeDelta, nBTLimit, nBTLimitAll, fVerbose );
+        FREE( pNtk->pModel );
+        FREE( pNtk->pSeqModel );
+        pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
     }
 PRT( "Time", clock() - clk );
     // verify counter-example
@@ -1667,7 +1673,7 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar )
     }
     if ( pSecPar->fTryBmc )
     {
-        RetValue = Abc_NtkDarBmc( pNtk, 20, 100000, 2000, 0, 1, 0 );
+        RetValue = Abc_NtkDarBmc( pNtk, 20, 100000, -1, 2000, -1, 0, 1, 0 );
         if ( RetValue == 0 )
         {
             printf( "Networks are not equivalent.\n" );
@@ -2132,9 +2138,10 @@ Abc_Ntk_t * Abc_NtkDarEnlarge( Abc_Ntk_t * pNtk, int nFrames, int fVerbose )
     Aig_ManStop( pMan );
     return pNtkAig;
 }
+
 /**Function*************************************************************
 
-  Synopsis    [Performs targe enlargement.]
+  Synopsis    [Performs induction for property only.]
 
   Description []
                
@@ -2143,7 +2150,7 @@ Abc_Ntk_t * Abc_NtkDarEnlarge( Abc_Ntk_t * pNtk, int nFrames, int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkDarLocalize( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fVerbose )
+void Abc_NtkDarInduction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fVerbose )
 {
     Aig_Man_t * pMan, * pTemp;
     int clkTotal = clock();
@@ -2173,6 +2180,41 @@ PRT( "Time", clock() - clkTotal );
 
 /**Function*************************************************************
 
+  Synopsis    [Performs proof-based abstraction.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkDarPBAbstraction( Abc_Ntk_t * pNtk, int nFramesMax, int nConfMax, int fVerbose )
+{
+    Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fVerbose );
+
+    Abc_Ntk_t * pNtkAig;
+    Aig_Man_t * pMan, * pTemp;
+    assert( Abc_NtkIsStrash(pNtk) );
+    pMan = Abc_NtkToDar( pNtk, 0, 1 );
+    if ( pMan == NULL )
+        return NULL;
+
+    Aig_ManSetRegNum( pMan, pMan->nRegs );
+    pMan = Saig_ManProofAbstraction( pTemp = pMan, nFramesMax, nConfMax, fVerbose );
+    Aig_ManStop( pTemp );
+    if ( pMan == NULL )
+        return NULL;
+
+    pNtkAig = Abc_NtkFromAigPhase( pMan );
+    pNtkAig->pName = Extra_UtilStrsav(pNtk->pName);
+    pNtkAig->pSpec = Extra_UtilStrsav(pNtk->pSpec);
+    Aig_ManStop( pMan );
+    return pNtkAig;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Interplates two networks.]
 
   Description []
@@ -2683,8 +2725,10 @@ Abc_Ntk_t * Abc_NtkDarTestNtk( Abc_Ntk_t * pNtk )
         return NULL;
 
     Aig_ManSetRegNum( pMan, pMan->nRegs );
-    pMan = Saig_ManProofAbstraction( pTemp = pMan, 10, 1000, 1 );
+    pMan = Saig_ManProofAbstraction( pTemp = pMan, 5, 10000, 1 );
     Aig_ManStop( pTemp );
+    if ( pMan == NULL )
+        return NULL;
 
     pNtkAig = Abc_NtkFromAigPhase( pMan );
     pNtkAig->pName = Extra_UtilStrsav(pNtk->pName);
diff --git a/src/map/pcm/module.make b/src/map/pcm/module.make
deleted file mode 100644
index e69de29b..00000000
--- a/src/map/pcm/module.make
+++ /dev/null
diff --git a/src/map/ply/module.make b/src/map/ply/module.make
deleted file mode 100644
index e69de29b..00000000
--- a/src/map/ply/module.make
+++ /dev/null