Version abc90804

committer: Baruch Sterin <baruchs@gmail.com>

24 files changed, 626 insertions, 137 deletions

diff --git a/src/aig/cec/cec.h b/src/aig/cec/cec.h
index fcadb6ab..7f445970 100644
--- a/src/aig/cec/cec.h
+++ b/src/aig/cec/cec.h
@@ -47,21 +47,23 @@ struct Cec_ParSat_t_
     int              fNonChrono;    // use non-chronological backtracling (for circuit SAT only)
     int              fPolarFlip;    // flops polarity of variables
     int              fCheckMiter;   // the circuit is the miter
-    int              fFirstStop;    // stop on the first sat output
+//    int              fFirstStop;    // stop on the first sat output
     int              fLearnCls;     // perform clause learning
     int              fVerbose;      // verbose stats
 };
 
 // simulation parameters
 typedef struct Cec_ParSim_t_ Cec_ParSim_t;
-struct Cec_ParSim_t_
+struct Cec_ParSim_t_ 
 {
     int              nWords;        // the number of simulation words
+    int              nFrames;       // the number of simulation frames
     int              nRounds;       // the number of simulation rounds
+    int              nNonRefines;   // the max number of rounds without refinement
     int              TimeLimit;     // the runtime limit in seconds
     int              fDualOut;      // miter with separate outputs
     int              fCheckMiter;   // the circuit is the miter
-    int              fFirstStop;    // stop on the first sat output
+//    int              fFirstStop;    // stop on the first sat output
     int              fSeqSimulate;  // performs sequential simulation
     int              fLatchCorr;    // consider only latch outputs
     int              fVeryVerbose;  // verbose stats
@@ -74,12 +76,14 @@ struct Cec_ParSmf_t_
 {
     int              nWords;        // the number of simulation words
     int              nRounds;       // the number of simulation rounds
-    int              nFrames;       // the number of time frames
+    int              nFrames;       // the max number of time frames
+    int              nNonRefines;   // the max number of rounds without refinement
+    int              nMinOutputs;   // the min outputs to accumulate
     int              nBTLimit;      // conflict limit at a node
     int              TimeLimit;     // the runtime limit in seconds
     int              fDualOut;      // miter with separate outputs
     int              fCheckMiter;   // the circuit is the miter
-    int              fFirstStop;    // stop on the first sat output
+//    int              fFirstStop;    // stop on the first sat output
     int              fVerbose;      // verbose stats
 };
 
@@ -96,7 +100,7 @@ struct Cec_ParFra_t_
     int              nDepthMax;     // the depth in terms of steps of speculative reduction
     int              fRewriting;    // enables AIG rewriting
     int              fCheckMiter;   // the circuit is the miter
-    int              fFirstStop;    // stop on the first sat output
+//    int              fFirstStop;    // stop on the first sat output
     int              fDualOut;      // miter with separate outputs
     int              fColorDiff;    // miter with separate outputs
     int              fVeryVerbose;  // verbose stats
@@ -109,7 +113,7 @@ struct Cec_ParCec_t_
 {
     int              nBTLimit;      // conflict limit at a node
     int              TimeLimit;     // the runtime limit in seconds
-    int              fFirstStop;    // stop on the first sat output
+//    int              fFirstStop;    // stop on the first sat output
     int              fUseSmartCnf;  // use smart CNF computation
     int              fRewriting;    // enables AIG rewriting
     int              fVeryVerbose;  // verbose stats
@@ -129,7 +133,7 @@ struct Cec_ParCor_t_
     int              fUseRings;     // use rings
     int              fMakeChoices;  // use equilvaences as choices
     int              fUseCSat;      // use circuit-based solver
-    int              fFirstStop;    // stop on the first sat output
+//    int              fFirstStop;    // stop on the first sat output
     int              fUseSmartCnf;  // use smart CNF computation
     int              fVeryVerbose;  // verbose stats
     int              fVerbose;      // verbose stats
diff --git a/src/aig/cec/cecCec.c b/src/aig/cec/cecCec.c
index a385be3e..1efa9235 100644
--- a/src/aig/cec/cecCec.c
+++ b/src/aig/cec/cecCec.c
@@ -135,7 +135,6 @@ int Cec_ManVerify( Gia_Man_t * p, Cec_ParCec_t * pPars )
     pParsFra->TimeLimit    = pPars->TimeLimit;
     pParsFra->fVerbose     = pPars->fVerbose;
     pParsFra->fCheckMiter  = 1;
-    pParsFra->fFirstStop   = 1;
     pParsFra->fDualOut     = 1;
     pNew = Cec_ManSatSweeping( p, pParsFra );
     if ( pNew == NULL )
diff --git a/src/aig/cec/cecChoice.c b/src/aig/cec/cecChoice.c
index f51d138d..fc316f46 100644
--- a/src/aig/cec/cecChoice.c
+++ b/src/aig/cec/cecChoice.c
@@ -213,7 +213,7 @@ int Cec_ManChoiceComputation_int( Gia_Man_t * pAig, Cec_ParChc_t * pPars )
     // prepare simulation manager
     Cec_ManSimSetDefaultParams( pParsSim );
     pParsSim->nWords     = pPars->nWords;
-    pParsSim->nRounds    = pPars->nRounds;
+    pParsSim->nFrames    = pPars->nRounds;
     pParsSim->fVerbose   = pPars->fVerbose;
     pParsSim->fLatchCorr   = 0;
     pParsSim->fSeqSimulate = 0;
diff --git a/src/aig/cec/cecClass.c b/src/aig/cec/cecClass.c
index fd723f30..749f7f71 100644
--- a/src/aig/cec/cecClass.c
+++ b/src/aig/cec/cecClass.c
@@ -545,7 +545,7 @@ void Cec_ManSimSavePattern( Cec_ManSim_t * p, int iPat )
 void Cec_ManSimFindBestPattern( Cec_ManSim_t * p )
 { 
     unsigned * pInfo;
-    int i, ScoreBest = 0, iPatBest = 1;
+    int i, ScoreBest = 0, iPatBest = 1; // set the first pattern
     // find the best pattern
     for ( i = 0; i < 32 * p->nWords; i++ )
         if ( ScoreBest < p->pScores[i] )
@@ -588,8 +588,8 @@ int Cec_ManSimAnalyzeOutputs( Cec_ManSim_t * p )
     // compare outputs with 0
     if ( p->pPars->fDualOut )
     {
-        assert( (Gia_ManCoNum(p->pAig) & 1) == 0 );
-        for ( i = 0; i < Gia_ManCoNum(p->pAig); i++ )
+        assert( (Gia_ManPoNum(p->pAig) & 1) == 0 );
+        for ( i = 0; i < Gia_ManPoNum(p->pAig); i++ )
         {
             pInfo  = Vec_PtrEntry( p->vCoSimInfo, i );
             pInfo2 = Vec_PtrEntry( p->vCoSimInfo, ++i );
@@ -601,7 +601,7 @@ int Cec_ManSimAnalyzeOutputs( Cec_ManSim_t * p )
                     Cec_ManSimSavePattern( p, Cec_ManSimCompareEqualFirstBit(pInfo, pInfo2, p->nWords) );
                 }
                 if ( p->pCexes == NULL )
-                    p->pCexes = ABC_CALLOC( void *, Gia_ManCoNum(p->pAig)/2 );
+                    p->pCexes = ABC_CALLOC( void *, Gia_ManPoNum(p->pAig)/2 );
                 if ( p->pCexes[i/2] == NULL )
                 {
                     p->nOuts++;
@@ -612,7 +612,7 @@ int Cec_ManSimAnalyzeOutputs( Cec_ManSim_t * p )
     }
     else
     {
-        for ( i = 0; i < Gia_ManCoNum(p->pAig); i++ )
+        for ( i = 0; i < Gia_ManPoNum(p->pAig); i++ )
         {
             pInfo = Vec_PtrEntry( p->vCoSimInfo, i );
             if ( !Cec_ManSimCompareConst( pInfo, p->nWords ) )
@@ -623,7 +623,7 @@ int Cec_ManSimAnalyzeOutputs( Cec_ManSim_t * p )
                     Cec_ManSimSavePattern( p, Cec_ManSimCompareConstFirstBit(pInfo, p->nWords) );
                 }
                 if ( p->pCexes == NULL )
-                    p->pCexes = ABC_CALLOC( void *, Gia_ManCoNum(p->pAig) );
+                    p->pCexes = ABC_CALLOC( void *, Gia_ManPoNum(p->pAig) );
                 if ( p->pCexes[i] == NULL )
                 {
                     p->nOuts++;
@@ -632,7 +632,7 @@ int Cec_ManSimAnalyzeOutputs( Cec_ManSim_t * p )
             }
         }
     }
-    return p->pCexes != NULL && p->pPars->fFirstStop;
+    return p->pCexes != NULL;
 }
 
 /**Function*************************************************************
diff --git a/src/aig/cec/cecCore.c b/src/aig/cec/cecCore.c
index 9820c05c..10c145ec 100644
--- a/src/aig/cec/cecCore.c
+++ b/src/aig/cec/cecCore.c
@@ -48,7 +48,7 @@ void Cec_ManSatSetDefaultParams( Cec_ParSat_t * p )
     p->fNonChrono     =       0;  // use non-chronological backtracling (for circuit SAT only)
     p->fPolarFlip     =       1;  // flops polarity of variables
     p->fCheckMiter    =       0;  // the circuit is the miter
-    p->fFirstStop     =       0;  // stop on the first sat output
+//    p->fFirstStop     =       0;  // stop on the first sat output
     p->fLearnCls      =       0;  // perform clause learning
     p->fVerbose       =       0;  // verbose stats
 }  
@@ -67,11 +67,13 @@ void Cec_ManSatSetDefaultParams( Cec_ParSat_t * p )
 void Cec_ManSimSetDefaultParams( Cec_ParSim_t * p )
 {
     memset( p, 0, sizeof(Cec_ParSim_t) );
-    p->nWords         =      15;  // the number of simulation words
-    p->nRounds        =      15;  // the number of simulation rounds
+    p->nWords         =      31;  // the number of simulation words
+    p->nFrames        =     100;  // the number of simulation frames
+    p->nRounds        =      20;  // the max number of simulation rounds
+    p->nNonRefines    =       3;  // the max number of rounds without refinement
     p->TimeLimit      =       0;  // the runtime limit in seconds
     p->fCheckMiter    =       0;  // the circuit is the miter
-    p->fFirstStop     =       0;  // stop on the first sat output
+//    p->fFirstStop     =       0;  // stop on the first sat output
     p->fDualOut       =       0;  // miter with separate outputs
     p->fSeqSimulate   =       0;  // performs sequential simulation
     p->fVeryVerbose   =       0;  // verbose stats
@@ -93,13 +95,15 @@ void Cec_ManSmfSetDefaultParams( Cec_ParSmf_t * p )
 {
     memset( p, 0, sizeof(Cec_ParSmf_t) );
     p->nWords         =      31;  // the number of simulation words
-    p->nRounds        =       1;  // the number of simulation rounds
-    p->nFrames        =       2;  // the number of time frames
+    p->nRounds        =     200;  // the number of simulation rounds
+    p->nFrames        =     200;  // the max number of time frames
+    p->nNonRefines    =       3;  // the max number of rounds without refinement
+    p->nMinOutputs    =       0;  // the min outputs to accumulate
     p->nBTLimit       =     100;  // conflict limit at a node
     p->TimeLimit      =       0;  // the runtime limit in seconds
     p->fDualOut       =       0;  // miter with separate outputs
     p->fCheckMiter    =       0;  // the circuit is the miter
-    p->fFirstStop     =       0;  // stop on the first sat output
+//    p->fFirstStop     =       0;  // stop on the first sat output
     p->fVerbose       =       0;  // verbose stats
 } 
 
@@ -126,7 +130,7 @@ void Cec_ManFraSetDefaultParams( Cec_ParFra_t * p )
     p->nDepthMax      =       1;  // the depth in terms of steps of speculative reduction
     p->fRewriting     =       0;  // enables AIG rewriting
     p->fCheckMiter    =       0;  // the circuit is the miter
-    p->fFirstStop     =       0;  // stop on the first sat output
+//    p->fFirstStop     =       0;  // stop on the first sat output
     p->fDualOut       =       0;  // miter with separate outputs
     p->fColorDiff     =       0;  // miter with separate outputs
     p->fVeryVerbose   =       0;  // verbose stats
@@ -149,7 +153,7 @@ void Cec_ManCecSetDefaultParams( Cec_ParCec_t * p )
     memset( p, 0, sizeof(Cec_ParCec_t) );
     p->nBTLimit       =    1000;  // conflict limit at a node
     p->TimeLimit      =       0;  // the runtime limit in seconds
-    p->fFirstStop     =       0;  // stop on the first sat output
+//    p->fFirstStop     =       0;  // stop on the first sat output
     p->fUseSmartCnf   =       0;  // use smart CNF computation
     p->fRewriting     =       0;  // enables AIG rewriting
     p->fVeryVerbose   =       0;  // verbose stats
@@ -177,7 +181,7 @@ void Cec_ManCorSetDefaultParams( Cec_ParCor_t * p )
     p->fLatchCorr     =       0;  // consider only latch outputs
     p->fUseRings      =       1;  // combine classes into rings
     p->fUseCSat       =       1;  // use circuit-based solver
-    p->fFirstStop     =       0;  // stop on the first sat output
+//    p->fFirstStop     =       0;  // stop on the first sat output
     p->fUseSmartCnf   =       0;  // use smart CNF computation
     p->fVeryVerbose   =       0;  // verbose stats
     p->fVerbose       =       0;  // verbose stats
@@ -233,31 +237,79 @@ Gia_Man_t * Cec_ManSatSolving( Gia_Man_t * pAig, Cec_ParSat_t * pPars )
 
   Synopsis    [Core procedure for simulation.]
 
-  Description []
+  Description [Returns 1 if refinement has happened.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-void Cec_ManSimulation( Gia_Man_t * pAig, Cec_ParSim_t * pPars )
+int Cec_ManSimulationOne( Gia_Man_t * pAig, Cec_ParSim_t * pPars )
 {
     Cec_ManSim_t * pSim;
-    int RetValue, clkTotal = clock();
-    if ( pPars->fSeqSimulate )
-        printf( "Performing sequential simulation of %d frames with %d words.\n", 
-            pPars->nRounds, pPars->nWords );
-    Gia_ManRandom( 1 );
+    int RetValue = 0, clkTotal = clock();
     pSim = Cec_ManSimStart( pAig, pPars );
-    if ( pAig->pReprs == NULL )
-        RetValue = Cec_ManSimClassesPrepare( pSim );
-    Cec_ManSimClassesRefine( pSim );
-    if ( pPars->fCheckMiter )
-        printf( "The number of failed outputs of the miter = %6d. (Words = %4d. Rounds = %4d.)\n", 
-            pSim->iOut, pSim->nOuts, pPars->nWords, pPars->nRounds );
+    if ( (pAig->pReprs == NULL && (RetValue = Cec_ManSimClassesPrepare( pSim ))) ||
+         (RetValue == 0 &&        (RetValue = Cec_ManSimClassesRefine( pSim ))) )
+        printf( "The number of failed outputs of the miter = %6d. (Words = %4d. Frames = %4d.)\n", 
+            pSim->nOuts, pPars->nWords, pPars->nFrames );
     if ( pPars->fVerbose )
         ABC_PRT( "Time", clock() - clkTotal );
     Cec_ManSimStop( pSim );
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Core procedure for simulation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_ManSimulation( Gia_Man_t * pAig, Cec_ParSim_t * pPars )
+{
+    int r, nLitsOld, nLitsNew, nCountNoRef = 0, fStop = 0;
+    Gia_ManRandom( 1 );
+    if ( pPars->fSeqSimulate )
+        printf( "Performing rounds of random simulation of %d frames with %d words.\n", 
+            pPars->nRounds, pPars->nFrames, pPars->nWords );
+    nLitsOld = Gia_ManEquivCountLits( pAig );
+    for ( r = 0; r < pPars->nRounds; r++ )
+    {
+        if ( Cec_ManSimulationOne( pAig, pPars ) )
+        {
+            fStop = 1;
+            break;
+        }
+        // decide when to stop
+        nLitsNew = Gia_ManEquivCountLits( pAig );
+        if ( nLitsOld == 0 || nLitsOld > nLitsNew )
+        {
+            nLitsOld = nLitsNew;
+            nCountNoRef = 0;
+        }
+        else if ( ++nCountNoRef == pPars->nNonRefines )
+        {
+            r++;
+            break;
+        }
+        assert( nLitsOld == nLitsNew );
+    }
+//    if ( pPars->fVerbose )
+    if ( r == pPars->nRounds || fStop )
+        printf( "Random simulation is stopped after %d rounds.\n", r );
+    else
+        printf( "Random simulation saturated after %d rounds.\n", r );
+    if ( pPars->fCheckMiter )
+    {
+        int nNonConsts = Cec_ManCountNonConstOutputs( pAig );
+        if ( nNonConsts )
+            printf( "The number of POs that are not const-0 candidates = %d.\n", nNonConsts );
+    }
 }
 
 /**Function*************************************************************
@@ -297,9 +349,8 @@ Gia_Man_t * Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParFra_t * pPars )
     // simulation
     Cec_ManSimSetDefaultParams( pParsSim );
     pParsSim->nWords      = pPars->nWords;
-    pParsSim->nRounds     = pPars->nRounds;
+    pParsSim->nFrames     = pPars->nRounds;
     pParsSim->fCheckMiter = pPars->fCheckMiter;
-    pParsSim->fFirstStop  = pPars->fFirstStop;
     pParsSim->fDualOut = pPars->fDualOut;
     pParsSim->fVerbose    = pPars->fVerbose;
     pSim = Cec_ManSimStart( p->pAig, pParsSim );
diff --git a/src/aig/cec/cecCorr.c b/src/aig/cec/cecCorr.c
index 96af801d..96c45907 100644
--- a/src/aig/cec/cecCorr.c
+++ b/src/aig/cec/cecCorr.c
@@ -545,7 +545,7 @@ int Cec_ManResimulateCounterExamples( Cec_ManSim_t * pSim, Vec_Int_t * vCexStore
     vPairs = Gia_ManCorrCreateRemapping( pSim->pAig );
     Gia_ManSetRefs( pSim->pAig );
 //    pSim->pPars->nWords  = 63;
-    pSim->pPars->nRounds = nFrames;
+    pSim->pPars->nFrames = nFrames;
     vSimInfo = Vec_PtrAllocSimInfo( Gia_ManRegNum(pSim->pAig) + Gia_ManPiNum(pSim->pAig) * nFrames, pSim->pPars->nWords );
     while ( iStart < Vec_IntSize(vCexStore) )
     {
@@ -580,7 +580,7 @@ int Cec_ManResimulateCounterExamplesComb( Cec_ManSim_t * pSim, Vec_Int_t * vCexS
     Vec_Ptr_t * vSimInfo; 
     int RetValue = 0, iStart = 0;
     Gia_ManSetRefs( pSim->pAig );
-    pSim->pPars->nRounds = 1;
+    pSim->pPars->nFrames = 1;
     vSimInfo = Vec_PtrAllocSimInfo( Gia_ManCiNum(pSim->pAig), pSim->pPars->nWords );
     while ( iStart < Vec_IntSize(vCexStore) )
     {
@@ -774,7 +774,7 @@ void Cec_ManLSCorrespondenceBmc( Gia_Man_t * pAig, Cec_ParCor_t * pPars, int nPr
     // prepare simulation manager
     Cec_ManSimSetDefaultParams( pParsSim );
     pParsSim->nWords     = pPars->nWords;
-    pParsSim->nRounds    = pPars->nRounds;
+    pParsSim->nFrames    = pPars->nRounds;
     pParsSim->fVerbose   = pPars->fVerbose;
     pParsSim->fLatchCorr = pPars->fLatchCorr;
     pParsSim->fSeqSimulate = 1;
@@ -853,7 +853,7 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
     // prepare simulation manager
     Cec_ManSimSetDefaultParams( pParsSim );
     pParsSim->nWords     = pPars->nWords;
-    pParsSim->nRounds    = pPars->nRounds;
+    pParsSim->nFrames    = pPars->nFrames;
     pParsSim->fVerbose   = pPars->fVerbose;
     pParsSim->fLatchCorr = pPars->fLatchCorr;
     pParsSim->fSeqSimulate = 1;
diff --git a/src/aig/cec/cecInt.h b/src/aig/cec/cecInt.h
index 9c012f73..73f108ba 100644
--- a/src/aig/cec/cecInt.h
+++ b/src/aig/cec/cecInt.h
@@ -192,8 +192,10 @@ extern Vec_Ptr_t *          Cec_ManPatCollectPatterns( Cec_ManPat_t *  pMan, int
 extern Vec_Ptr_t *          Cec_ManPatPackPatterns( Vec_Int_t * vCexStore, int nInputs, int nRegs, int nWordsInit );
 /*=== cecSeq.c ============================================================*/
 extern int                  Cec_ManSeqResimulate( Cec_ManSim_t * p, Vec_Ptr_t * vInfo );
-extern int                  Cec_ManSeqResimulateInfo( Gia_Man_t * pAig, Vec_Ptr_t * vSimInfo, Gia_Cex_t * pBestState );
+extern int                  Cec_ManSeqResimulateInfo( Gia_Man_t * pAig, Vec_Ptr_t * vSimInfo, Gia_Cex_t * pBestState, int fCheckMiter );
 extern void                 Cec_ManSeqDeriveInfoInitRandom( Vec_Ptr_t * vInfo, Gia_Man_t * pAig, Gia_Cex_t * pCex );
+extern int                  Cec_ManCountNonConstOutputs( Gia_Man_t * pAig );
+extern int                  Cec_ManCheckNonTrivialCands( Gia_Man_t * pAig );
 /*=== cecSolve.c ============================================================*/
 extern int                  Cec_ObjSatVarValue( Cec_ManSat_t * p, Gia_Obj_t * pObj );
 extern void                 Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars );
diff --git a/src/aig/cec/cecMan.c b/src/aig/cec/cecMan.c
index de71ecc9..70396cca 100644
--- a/src/aig/cec/cecMan.c
+++ b/src/aig/cec/cecMan.c
@@ -76,13 +76,13 @@ void Cec_ManSatPrintStats( Cec_ManSat_t * p )
     printf( "MinVar = %5d  ", p->pPars->nSatVarMax );
     printf( "MinCalls = %5d\n", p->pPars->nCallsRecycle );
     printf( "Unsat calls %6d  (%6.2f %%)   Ave conf = %8.1f   ", 
-        p->nSatUnsat, 100.0*p->nSatUnsat/p->nSatTotal, p->nSatUnsat? 1.0*p->nConfUnsat/p->nSatUnsat :0.0 );
+        p->nSatUnsat, p->nSatTotal? 100.0*p->nSatUnsat/p->nSatTotal : 0.0, p->nSatUnsat? 1.0*p->nConfUnsat/p->nSatUnsat :0.0 );
     ABC_PRTP( "Time", p->timeSatUnsat, p->timeTotal );
     printf( "Sat   calls %6d  (%6.2f %%)   Ave conf = %8.1f   ", 
-        p->nSatSat,   100.0*p->nSatSat/p->nSatTotal, p->nSatSat? 1.0*p->nConfSat/p->nSatSat : 0.0 );
+        p->nSatSat,   p->nSatTotal? 100.0*p->nSatSat/p->nSatTotal : 0.0,   p->nSatSat? 1.0*p->nConfSat/p->nSatSat : 0.0 );
     ABC_PRTP( "Time", p->timeSatSat,   p->timeTotal );
     printf( "Undef calls %6d  (%6.2f %%)   Ave conf = %8.1f   ", 
-        p->nSatUndec, 100.0*p->nSatUndec/p->nSatTotal, p->nSatUndec? 1.0*p->nConfUndec/p->nSatUndec : 0.0 );
+        p->nSatUndec, p->nSatTotal? 100.0*p->nSatUndec/p->nSatTotal : 0.0, p->nSatUndec? 1.0*p->nConfUndec/p->nSatUndec : 0.0 );
     ABC_PRTP( "Time", p->timeSatUndec, p->timeTotal );
     ABC_PRT( "Total time", p->timeTotal );
 }
diff --git a/src/aig/cec/cecSeq.c b/src/aig/cec/cecSeq.c
index b19950b3..49f2a018 100644
--- a/src/aig/cec/cecSeq.c
+++ b/src/aig/cec/cecSeq.c
@@ -125,9 +125,9 @@ void Cec_ManSeqDeriveInfoInitRandom( Vec_Ptr_t * vInfo, Gia_Man_t * pAig, Gia_Ce
 int Cec_ManSeqResimulate( Cec_ManSim_t * p, Vec_Ptr_t * vInfo )
 {
     unsigned * pInfo0, * pInfo1;
-    int f, i, k, w, RetValue = 0;
+    int f, i, k, w;
 //    assert( Gia_ManRegNum(p->pAig) > 0 );
-    assert( Vec_PtrSize(vInfo) == Gia_ManRegNum(p->pAig) + Gia_ManPiNum(p->pAig) * p->pPars->nRounds );
+    assert( Vec_PtrSize(vInfo) == Gia_ManRegNum(p->pAig) + Gia_ManPiNum(p->pAig) * p->pPars->nFrames );
     for ( k = 0; k < Gia_ManRegNum(p->pAig); k++ )
     {
         pInfo0 = Vec_PtrEntry( vInfo, k );
@@ -135,7 +135,7 @@ int Cec_ManSeqResimulate( Cec_ManSim_t * p, Vec_Ptr_t * vInfo )
         for ( w = 0; w < p->nWords; w++ )
             pInfo1[w] = pInfo0[w];
     }
-    for ( f = 0; f < p->pPars->nRounds; f++ )
+    for ( f = 0; f < p->pPars->nFrames; f++ )
     {
         for ( i = 0; i < Gia_ManPiNum(p->pAig); i++ )
         {
@@ -152,13 +152,10 @@ int Cec_ManSeqResimulate( Cec_ManSim_t * p, Vec_Ptr_t * vInfo )
                 pInfo1[w] = pInfo0[w];
         }
         if ( Cec_ManSimSimulateRound( p, p->vCiSimInfo, p->vCoSimInfo ) )
-        {
-            printf( "One of the outputs of the miter is asserted.\n" );
-            RetValue = 1;
-        }
+            return 1;
     }
     assert( k == Vec_PtrSize(vInfo) );
-    return RetValue;
+    return 0;
 }
 
 /**Function*************************************************************
@@ -172,15 +169,16 @@ int Cec_ManSeqResimulate( Cec_ManSim_t * p, Vec_Ptr_t * vInfo )
   SeeAlso     []
 
 ***********************************************************************/
-int Cec_ManSeqResimulateInfo( Gia_Man_t * pAig, Vec_Ptr_t * vSimInfo, Gia_Cex_t * pBestState )
+int Cec_ManSeqResimulateInfo( Gia_Man_t * pAig, Vec_Ptr_t * vSimInfo, Gia_Cex_t * pBestState, int fCheckMiter )
 {
     Cec_ParSim_t ParsSim, * pParsSim = &ParsSim;
     Cec_ManSim_t * pSim;
     int RetValue, clkTotal = clock();
     assert( (Vec_PtrSize(vSimInfo) - Gia_ManRegNum(pAig)) % Gia_ManPiNum(pAig) == 0 );
     Cec_ManSimSetDefaultParams( pParsSim );
-    pParsSim->nRounds = (Vec_PtrSize(vSimInfo) - Gia_ManRegNum(pAig)) / Gia_ManPiNum(pAig);
+    pParsSim->nFrames = (Vec_PtrSize(vSimInfo) - Gia_ManRegNum(pAig)) / Gia_ManPiNum(pAig);
     pParsSim->nWords  = Vec_PtrReadWordsSimInfo( vSimInfo );
+    pParsSim->fCheckMiter = fCheckMiter;
     Gia_ManSetRefs( pAig );
     pSim = Cec_ManSimStart( pAig, pParsSim );
     if ( pBestState )
@@ -228,25 +226,83 @@ int Cec_ManSeqResimulateCounter( Gia_Man_t * pAig, Cec_ParSim_t * pPars, Gia_Cex
         return -1;
     }
     if ( pPars->fVerbose )
-        printf( "Resimulating %d timeframes.\n", pPars->nRounds + pCex->iFrame + 1 );
+        printf( "Resimulating %d timeframes.\n", pPars->nFrames + pCex->iFrame + 1 );
     Gia_ManRandom( 1 );
     vSimInfo = Vec_PtrAllocSimInfo( Gia_ManRegNum(pAig) + 
-        Gia_ManPiNum(pAig) * (pPars->nRounds + pCex->iFrame + 1), 1 );
+        Gia_ManPiNum(pAig) * (pPars->nFrames + pCex->iFrame + 1), 1 );
     Cec_ManSeqDeriveInfoFromCex( vSimInfo, pAig, pCex );
     if ( pPars->fVerbose )
         Gia_ManEquivPrintClasses( pAig, 0, 0 );
-    RetValue = Cec_ManSeqResimulateInfo( pAig, vSimInfo, NULL );
+    RetValue = Cec_ManSeqResimulateInfo( pAig, vSimInfo, NULL, pPars->fCheckMiter );
     if ( pPars->fVerbose )
         Gia_ManEquivPrintClasses( pAig, 0, 0 );
     Vec_PtrFree( vSimInfo );
     if ( pPars->fVerbose )
         ABC_PRT( "Time", clock() - clkTotal );
+    if ( RetValue )
+        printf( "Cec_ManSeqResimulateCounter(): An output of the miter is asserted!\n" );
     return RetValue;
 }
 
 
 /**Function*************************************************************
 
+  Synopsis    [Returns the number of POs that are not const0 cands.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cec_ManCountNonConstOutputs( Gia_Man_t * pAig )
+{
+    Gia_Obj_t * pObj;
+    int i, Counter = 0;
+    if ( pAig->pReprs == NULL )
+        return -1;
+    Gia_ManForEachPo( pAig, pObj, i )
+        if ( !Gia_ObjIsConst( pAig, Gia_ObjFaninId0p(pAig, pObj) ) )
+            Counter++;
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the number of POs that are not const0 cands.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cec_ManCheckNonTrivialCands( Gia_Man_t * pAig )
+{
+    Gia_Obj_t * pObj;
+    int i, RetValue = 0;
+    if ( pAig->pReprs == NULL )
+        return 0;
+    // label internal nodes driving POs
+    Gia_ManForEachPo( pAig, pObj, i )
+        Gia_ObjFanin0(pObj)->fMark0 = 1;
+    // check if there are non-labled equivs
+    Gia_ManForEachObj( pAig, pObj, i )
+        if ( Gia_ObjIsCand(pObj) && !pObj->fMark0 && Gia_ObjRepr(pAig, i) != GIA_VOID )
+        {
+            RetValue = 1;
+            break;
+        }
+    // clean internal nodes driving POs
+    Gia_ManForEachPo( pAig, pObj, i )
+        Gia_ObjFanin0(pObj)->fMark0 = 0;
+    return RetValue;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Performs semiformal refinement of equivalence classes.]
 
   Description []
@@ -258,13 +314,15 @@ int Cec_ManSeqResimulateCounter( Gia_Man_t * pAig, Cec_ParSim_t * pPars, Gia_Cex
 ***********************************************************************/
 int Cec_ManSeqSemiformal( Gia_Man_t * pAig, Cec_ParSmf_t * pPars )
 { 
-    int nAddFrames = 10; // additional timeframes to simulate
+    int nAddFrames = 16; // additional timeframes to simulate
+    int nCountNoRef = 0;
+    int nFramesReal;
     Cec_ParSat_t ParsSat, * pParsSat = &ParsSat;
     Vec_Ptr_t * vSimInfo; 
     Vec_Str_t * vStatus;
     Gia_Cex_t * pState;
-    Gia_Man_t * pSrm;
-    int r, nPats, RetValue = -1;
+    Gia_Man_t * pSrm, * pReduce, * pAux;
+    int r, nPats, RetValue = 0;
     if ( pAig->pReprs == NULL )
     { 
         printf( "Cec_ManSeqSemiformal(): Equivalence classes are not available.\n" );
@@ -290,22 +348,36 @@ int Cec_ManSeqSemiformal( Gia_Man_t * pAig, Cec_ParSmf_t * pPars )
         Gia_ManEquivPrintClasses( pAig, 0, 0 );
     }
     // perform the given number of BMC rounds
+    Gia_ManCleanMark0( pAig );
     for ( r = 0; r < pPars->nRounds; r++ )
     {
+        if ( !Cec_ManCheckNonTrivialCands(pAig) )
+        {
+            printf( "Cec_ManSeqSemiformal: There are only trivial equiv candidates left (PO drivers). Quitting.\n" );
+            break;
+        }
 //        Gia_ManPrintCounterExample( pState );
         // derive speculatively reduced model
-        pSrm = Gia_ManSpecReduceInit( pAig, pState, pPars->nFrames, pPars->fDualOut );
-        assert( Gia_ManRegNum(pSrm) == 0 && Gia_ManPiNum(pSrm) == (Gia_ManPiNum(pAig) * pPars->nFrames) );
+//        pSrm = Gia_ManSpecReduceInit( pAig, pState, pPars->nFrames, pPars->fDualOut );
+        pSrm = Gia_ManSpecReduceInitFrames( pAig, pState, pPars->nFrames, &nFramesReal, pPars->fDualOut, pPars->nMinOutputs );
+        if ( pSrm == NULL )
+        {
+            printf( "Quitting refinement because miter could not be unrolled.\n" );
+            break;
+        }
+        assert( Gia_ManRegNum(pSrm) == 0 && Gia_ManPiNum(pSrm) == (Gia_ManPiNum(pAig) * nFramesReal) );
+        if ( pPars->fVerbose )
+            printf( "Unrolled for %d frames.\n", nFramesReal );
         // allocate room for simulation info
         vSimInfo = Vec_PtrAllocSimInfo( Gia_ManRegNum(pAig) + 
-            Gia_ManPiNum(pAig) * (pPars->nFrames + nAddFrames), pPars->nWords );
+            Gia_ManPiNum(pAig) * (nFramesReal + nAddFrames), pPars->nWords );
         Cec_ManSeqDeriveInfoInitRandom( vSimInfo, pAig, pState );
         // fill in simulation info with counter-examples
         vStatus = Cec_ManSatSolveSeq( vSimInfo, pSrm, pParsSat, Gia_ManRegNum(pAig), &nPats );
         Vec_StrFree( vStatus );
         Gia_ManStop( pSrm );
         // resimulate and refine the classes
-        RetValue = Cec_ManSeqResimulateInfo( pAig, vSimInfo, pState );
+        RetValue = Cec_ManSeqResimulateInfo( pAig, vSimInfo, pState, pPars->fCheckMiter );
         Vec_PtrFree( vSimInfo );
         assert( pState->iPo >= 0 ); // hit counter
         pState->iPo = -1;
@@ -314,11 +386,47 @@ int Cec_ManSeqSemiformal( Gia_Man_t * pAig, Cec_ParSmf_t * pPars )
             printf( "BMC = %3d ", nPats );
             Gia_ManEquivPrintClasses( pAig, 0, 0 );
         }
+
+        // write equivalence classes
+        Gia_WriteAiger( pAig, "gore.aig", 0, 0 );
+        // reduce the model
+        pReduce = Gia_ManSpecReduce( pAig, 0, 0 );
+        if ( pReduce )
+        {
+            pReduce = Gia_ManSeqStructSweep( pAux = pReduce, 1, 1, 0 );
+            Gia_ManStop( pAux );
+            Gia_WriteAiger( pReduce, "gsrm.aig", 0, 0 );
+//            printf( "Speculatively reduced model was written into file \"%s\".\n", "gsrm.aig" );
+//          Gia_ManPrintStatsShort( pReduce );
+            Gia_ManStop( pReduce );
+        }
+
+        if ( RetValue )
+        {
+            printf( "Cec_ManSeqSemiformal(): An output of the miter is asserted. Refinement stopped.\n" );
+            break;
+        }
+        // decide when to stop
+        if ( nPats > 0 )
+            nCountNoRef = 0;
+        else if ( ++nCountNoRef == pPars->nNonRefines )
+            break;
     }
     ABC_FREE( pState );
+    if ( pPars->fCheckMiter )
+    {
+        int nNonConsts = Cec_ManCountNonConstOutputs( pAig );
+        if ( nNonConsts )
+            printf( "The number of POs that are not const-0 candidates = %d.\n", nNonConsts );
+    }
     return RetValue;
 }
 
+//&r s13207.aig; &ps; &equiv; &ps; &semi -R 2 -vm
+//&r bug/50/temp.aig; &ps; &equiv -smv; &semi -v
+//r mentor/1_05c.blif; st; &get; &ps; &equiv -smv; &semi -mv
+//&r bug/50/hdl1.aig; &ps; &equiv -smv; &semi -mv; &srm; &r gsrm.aig; &ps
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/cec/cecSolve.c b/src/aig/cec/cecSolve.c
index 1aaf54ff..fa10d222 100644
--- a/src/aig/cec/cecSolve.c
+++ b/src/aig/cec/cecSolve.c
@@ -718,7 +718,7 @@ clk2 = clock();
             pPat->timeTotalSave += clock() - clk3;
         }
         // quit if one of them is solved
-        if ( pPars->fFirstStop )
+        if ( pPars->fCheckMiter )
             break;
     }
     p->timeTotal = clock() - clk;
@@ -810,12 +810,12 @@ Vec_Str_t * Cec_ManSatSolveSeq( Vec_Ptr_t * vPatts, Gia_Man_t * pAig, Cec_ParSat
         {
             if ( Gia_ObjFaninC0(pObj) )
             {
-                printf( "Constant 1 output of SRM!!!\n" );
+//                printf( "Constant 1 output of SRM!!!\n" );
                 Vec_StrPush( vStatus, 0 );
             }
             else
             {
-                printf( "Constant 0 output of SRM!!!\n" );
+//                printf( "Constant 0 output of SRM!!!\n" );
                 Vec_StrPush( vStatus, 1 );
             }
             continue;
diff --git a/src/aig/dch/dch.h b/src/aig/dch/dch.h
index 38978164..7271d256 100644
--- a/src/aig/dch/dch.h
+++ b/src/aig/dch/dch.h
@@ -68,7 +68,7 @@ struct Dch_Pars_t_
 /*=== dchCore.c ==========================================================*/
 extern void          Dch_ManSetDefaultParams( Dch_Pars_t * p );
 extern Aig_Man_t *   Dch_ComputeChoices( Aig_Man_t * pAig, Dch_Pars_t * pPars );
-
+extern void          Dch_ComputeEquivalences( Aig_Man_t * pAig, Dch_Pars_t * pPars );
 
 #ifdef __cplusplus
 }
diff --git a/src/aig/dch/dchCore.c b/src/aig/dch/dchCore.c
index 4a8d8b53..d38d5668 100644
--- a/src/aig/dch/dchCore.c
+++ b/src/aig/dch/dchCore.c
@@ -90,7 +90,7 @@ p->timeTotal = clock() - clkTotal;
     ABC_FREE( pAig->pTable );
     pResult = Dch_DeriveChoiceAig( pAig );
     // count the number of representatives
-    if ( pPars->fVerbose )
+    if ( pPars->fVerbose ) 
         printf( "STATS:  Reprs = %6d.  Equivs = %6d.  Choices = %6d.\n", 
                Dch_DeriveChoiceCountReprs( pAig ),
                Dch_DeriveChoiceCountEquivs( pResult ),
@@ -98,6 +98,38 @@ p->timeTotal = clock() - clkTotal;
     return pResult;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Performs computation of AIGs with choices.]
+
+  Description [Takes several AIGs and performs choicing.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dch_ComputeEquivalences( Aig_Man_t * pAig, Dch_Pars_t * pPars )
+{
+    Dch_Man_t * p;
+    int clk, clkTotal = clock();
+    // reset random numbers
+    Aig_ManRandom(1);
+    // start the choicing manager
+    p = Dch_ManCreate( pAig, pPars );
+    // compute candidate equivalence classes
+clk = clock(); 
+    p->ppClasses = Dch_CreateCandEquivClasses( pAig, pPars->nWords, pPars->fVerbose );
+p->timeSimInit = clock() - clk;
+//    Dch_ClassesPrint( p->ppClasses, 0 );
+    p->nLits = Dch_ClassesLitNum( p->ppClasses );
+    // perform SAT sweeping
+    Dch_ManSweep( p );
+    // free memory ahead of time
+p->timeTotal = clock() - clkTotal;
+    Dch_ManStop( p );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index 72af2466..ccb3e7b1 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -480,6 +480,7 @@ clk = clock();
         }
         else if ( pParSec->fInterSeparate )
         {
+            Ssw_Cex_t * pCex = NULL;
             Aig_Man_t * pTemp, * pAux;
             Aig_Obj_t * pObjPo;
             int i, Counter = 0;
@@ -495,8 +496,7 @@ clk = clock();
                     RetValue = Inter_ManPerformInterpolation( pTemp, pPars, &Depth );
                     if ( pTemp->pSeqModel )
                     {
-                        Ssw_Cex_t * pCex;
-                        pCex = pNew->pSeqModel = pTemp->pSeqModel; pTemp->pSeqModel = NULL;
+                        pCex = p->pSeqModel = Ssw_SmlDupCounterExample( pTemp->pSeqModel, Aig_ManRegNum(p) );
                         pCex->iPo = i;
                         Aig_ManStop( pTemp );
                         break;
@@ -520,7 +520,7 @@ clk = clock();
                 printf( "Solving output %3d (out of %3d) using interpolation.\r", i, Saig_ManPoNum(pNew) );
             }
             Aig_ManCleanup( pNew );
-            if ( pNew->pSeqModel == NULL )
+            if ( pCex == NULL )
             {
                 printf( "Interpolation left %d (out of %d) outputs unsolved              \n", Counter, Saig_ManPoNum(pNew) );
                 if ( Counter )
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index af92acc9..9dad2742 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -557,6 +557,7 @@ extern Gia_Man_t *         Gia_ManRemoveEnables( Gia_Man_t * p );
 extern int                 Gia_ManCheckTopoOrder( Gia_Man_t * p );
 extern int *               Gia_ManDeriveNexts( Gia_Man_t * p );
 extern void                Gia_ManDeriveReprs( Gia_Man_t * p );
+extern int                 Gia_ManEquivCountLits( Gia_Man_t * p );
 extern int                 Gia_ManEquivCountClasses( Gia_Man_t * p );
 extern void                Gia_ManEquivPrintOne( Gia_Man_t * p, int i, int Counter );
 extern void                Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem );
@@ -565,6 +566,7 @@ extern Gia_Man_t *         Gia_ManEquivReduceAndRemap( Gia_Man_t * p, int fSeq,
 extern int                 Gia_ManEquivSetColors( Gia_Man_t * p, int fVerbose );
 extern Gia_Man_t *         Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fVerbose );
 extern Gia_Man_t *         Gia_ManSpecReduceInit( Gia_Man_t * p, Gia_Cex_t * pInit, int nFrames, int fDualOut );
+extern Gia_Man_t *         Gia_ManSpecReduceInitFrames( Gia_Man_t * p, Gia_Cex_t * pInit, int nFramesMax, int * pnFrames, int fDualOut, int nMinOutputs );
 extern void                Gia_ManEquivTransform( Gia_Man_t * p, int fVerbose );
 extern void                Gia_ManEquivImprove( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ManEquivToChoices( Gia_Man_t * p, int nSnapshots );
@@ -663,6 +665,7 @@ extern void                Tas_ManStop( Tas_Man_t * p );
 extern Vec_Int_t *         Tas_ReadModel( Tas_Man_t * p );
 extern void                Tas_ManSatPrintStats( Tas_Man_t * p );
 extern int                 Tas_ManSolve( Tas_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pObj2 );
+extern int                 Tas_ManSolveArray( Tas_Man_t * p, Vec_Ptr_t * vObjs );
 
  
 #ifdef __cplusplus
diff --git a/src/aig/gia/giaAiger.c b/src/aig/gia/giaAiger.c
index afe9164f..6c8ace8a 100644
--- a/src/aig/gia/giaAiger.c
+++ b/src/aig/gia/giaAiger.c
@@ -841,7 +841,7 @@ void Gia_WriteAiger( Gia_Man_t * pInit, char * pFileName, int fWriteSymbols, int
     // create normalized AIG
     if ( !Gia_ManIsNormalized(pInit) )
     {
-        printf( "Gia_WriteAiger(): Normalizing AIG for writing.\n" );
+//        printf( "Gia_WriteAiger(): Normalizing AIG for writing.\n" );
         p = Gia_ManDupNormalized( pInit );
     }
     else
diff --git a/src/aig/gia/giaCSat.c b/src/aig/gia/giaCSat.c
index 644ccda5..e3aca7df 100644
--- a/src/aig/gia/giaCSat.c
+++ b/src/aig/gia/giaCSat.c
@@ -969,13 +969,13 @@ void Cbs_ManSatPrintStats( Cbs_Man_t * p )
     printf( "JustMax = %5d  ", p->Pars.nJustLimit );
     printf( "\n" );
     printf( "Unsat calls %6d  (%6.2f %%)   Ave conf = %8.1f   ", 
-        p->nSatUnsat, 100.0*p->nSatUnsat/p->nSatTotal, p->nSatUnsat? 1.0*p->nConfUnsat/p->nSatUnsat :0.0 );
+        p->nSatUnsat, p->nSatTotal? 100.0*p->nSatUnsat/p->nSatTotal :0.0, p->nSatUnsat? 1.0*p->nConfUnsat/p->nSatUnsat :0.0 );
     ABC_PRTP( "Time", p->timeSatUnsat, p->timeTotal );
     printf( "Sat   calls %6d  (%6.2f %%)   Ave conf = %8.1f   ", 
-        p->nSatSat,   100.0*p->nSatSat/p->nSatTotal, p->nSatSat? 1.0*p->nConfSat/p->nSatSat : 0.0 );
+        p->nSatSat,   p->nSatTotal? 100.0*p->nSatSat/p->nSatTotal :0.0, p->nSatSat? 1.0*p->nConfSat/p->nSatSat : 0.0 );
     ABC_PRTP( "Time", p->timeSatSat,   p->timeTotal );
     printf( "Undef calls %6d  (%6.2f %%)   Ave conf = %8.1f   ", 
-        p->nSatUndec, 100.0*p->nSatUndec/p->nSatTotal, p->nSatUndec? 1.0*p->nConfUndec/p->nSatUndec : 0.0 );
+        p->nSatUndec, p->nSatTotal? 100.0*p->nSatUndec/p->nSatTotal :0.0, p->nSatUndec? 1.0*p->nConfUndec/p->nSatUndec : 0.0 );
     ABC_PRTP( "Time", p->timeSatUndec, p->timeTotal );
     ABC_PRT( "Total time", p->timeTotal );
 }
diff --git a/src/aig/gia/giaCSatOld.c b/src/aig/gia/giaCSatOld.c
index a0d97693..bd8f061b 100644
--- a/src/aig/gia/giaCSatOld.c
+++ b/src/aig/gia/giaCSatOld.c
@@ -680,13 +680,13 @@ void Cbs0_ManSatPrintStats( Cbs0_Man_t * p )
     printf( "JustMax = %5d  ", p->Pars.nJustLimit );
     printf( "\n" );
     printf( "Unsat calls %6d  (%6.2f %%)   Ave conf = %8.1f   ", 
-        p->nSatUnsat, 100.0*p->nSatUnsat/p->nSatTotal, p->nSatUnsat? 1.0*p->nConfUnsat/p->nSatUnsat :0.0 );
+        p->nSatUnsat, p->nSatTotal? 100.0*p->nSatUnsat/p->nSatTotal :0.0, p->nSatUnsat? 1.0*p->nConfUnsat/p->nSatUnsat :0.0 );
     ABC_PRTP( "Time", p->timeSatUnsat, p->timeTotal );
     printf( "Sat   calls %6d  (%6.2f %%)   Ave conf = %8.1f   ", 
-        p->nSatSat,   100.0*p->nSatSat/p->nSatTotal, p->nSatSat? 1.0*p->nConfSat/p->nSatSat : 0.0 );
+        p->nSatSat,   p->nSatTotal? 100.0*p->nSatSat/p->nSatTotal :0.0, p->nSatSat? 1.0*p->nConfSat/p->nSatSat : 0.0 );
     ABC_PRTP( "Time", p->timeSatSat,   p->timeTotal );
     printf( "Undef calls %6d  (%6.2f %%)   Ave conf = %8.1f   ", 
-        p->nSatUndec, 100.0*p->nSatUndec/p->nSatTotal, p->nSatUndec? 1.0*p->nConfUndec/p->nSatUndec : 0.0 );
+        p->nSatUndec, p->nSatTotal? 100.0*p->nSatUndec/p->nSatTotal :0.0, p->nSatUndec? 1.0*p->nConfUndec/p->nSatUndec : 0.0 );
     ABC_PRTP( "Time", p->timeSatUndec, p->timeTotal );
     ABC_PRT( "Total time", p->timeTotal );
 }
diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c
index 8458268c..0f680e31 100644
--- a/src/aig/gia/giaEquiv.c
+++ b/src/aig/gia/giaEquiv.c
@@ -256,6 +256,69 @@ int Gia_ManEquivCheckLits( Gia_Man_t * p, int nLits )
   SeeAlso     []
 
 ***********************************************************************/
+void Gia_ManPrintStatsClasses( Gia_Man_t * p )
+{
+    int i, Counter = 0, Counter0 = 0, CounterX = 0, Proved = 0, nLits;
+    for ( i = 1; i < Gia_ManObjNum(p); i++ )
+    {
+        if ( Gia_ObjIsHead(p, i) )
+            Counter++;
+        else if ( Gia_ObjIsConst(p, i) )
+            Counter0++;
+        else if ( Gia_ObjIsNone(p, i) )
+            CounterX++;
+        if ( Gia_ObjProved(p, i) )
+            Proved++;
+    }
+    CounterX -= Gia_ManCoNum(p);
+    nLits = Gia_ManCiNum(p) + Gia_ManAndNum(p) - Counter - CounterX;
+
+//    printf( "i/o/ff =%5d/%5d/%5d  ", Gia_ManPiNum(p), Gia_ManPoNum(p), Gia_ManRegNum(p) );
+//    printf( "and =%5d  ", Gia_ManAndNum(p) );
+//    printf( "lev =%3d  ", Gia_ManLevelNum(p) );
+    printf( "cst =%3d  cls =%6d  lit =%8d\n", Counter0, Counter, nLits );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManEquivCountLits( Gia_Man_t * p )
+{
+    int i, Counter = 0, Counter0 = 0, CounterX = 0;
+    if ( p->pReprs == NULL || p->pNexts == NULL )
+        return 0;
+    for ( i = 1; i < Gia_ManObjNum(p); i++ )
+    {
+        if ( Gia_ObjIsHead(p, i) )
+            Counter++;
+        else if ( Gia_ObjIsConst(p, i) )
+            Counter0++;
+        else if ( Gia_ObjIsNone(p, i) )
+            CounterX++;
+    }
+    CounterX -= Gia_ManCoNum(p);
+    return Gia_ManCiNum(p) + Gia_ManAndNum(p) - Counter - CounterX;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem )
 {
     int i, Counter = 0, Counter0 = 0, CounterX = 0, Proved = 0, nLits;
@@ -274,6 +337,8 @@ void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem )
     nLits = Gia_ManCiNum(p) + Gia_ManAndNum(p) - Counter - CounterX;
     printf( "cst =%8d  cls =%7d  lit =%8d  unused =%8d  proof =%6d  mem =%5.2f Mb\n", 
         Counter0, Counter, nLits, CounterX, Proved, (Mem == 0.0) ? 8.0*Gia_ManObjNum(p)/(1<<20) : Mem );
+//    printf( "cst =%8d  cls =%7d  lit =%8d\n", 
+//        Counter0, Counter, nLits );
     assert( Gia_ManEquivCheckLits( p, nLits ) );
     if ( fVerbose )
     {
@@ -696,6 +761,29 @@ static inline void Gia_ManSpecBuild( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t
 
 /**Function*************************************************************
 
+  Synopsis    [Returns 1 if AIG has dangling nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManHasNoEquivs( Gia_Man_t * p )
+{
+    Gia_Obj_t * pObj;
+    int i;
+    if ( p->pReprs == NULL )
+        return 1;
+    Gia_ManForEachObj( p, pObj, i )
+        if ( Gia_ObjReprObj(p, i) != NULL )
+            break;
+    return i == Gia_ManObjNum(p);
+}
+
+/**Function*************************************************************
+
   Synopsis    [Duplicates the AIG in the DFS order.]
 
   Description []
@@ -743,16 +831,11 @@ Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fVerbose )
         printf( "Gia_ManSpecReduce(): Dual-output miter should have even number of POs.\n" );
         return NULL;
     }
-    // check if there are any equivalences defined
-    Gia_ManForEachObj( p, pObj, i )
-        if ( Gia_ObjReprObj(p, i) != NULL )
-            break;
-    if ( i == Gia_ManObjNum(p) )
+    if ( Gia_ManHasNoEquivs(p) )
     {
         printf( "Gia_ManSpecReduce(): There are no equivalences to reduce.\n" );
         return NULL;
     }
-
 /*
     if ( !Gia_ManCheckTopoOrder( p ) )
     {
@@ -792,7 +875,6 @@ Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fVerbose )
     return pNew;
 }
 
-
 /**Function*************************************************************
 
   Synopsis    [Duplicates the AIG in the DFS order.]
@@ -879,6 +961,7 @@ Gia_Man_t * Gia_ManSpecReduceInit( Gia_Man_t * p, Gia_Cex_t * pInit, int nFrames
         printf( "Gia_ManSpecReduceInit(): Dual-output miter should have even number of POs.\n" );
         return NULL;
     }
+
 /*
     if ( !Gia_ManCheckTopoOrder( p ) )
     {
@@ -918,7 +1001,7 @@ Gia_Man_t * Gia_ManSpecReduceInit( Gia_Man_t * p, Gia_Cex_t * pInit, int nFrames
         Gia_ManAppendCo( pNew, iLitNew );
     if ( Vec_IntSize(vXorLits) == 0 )
     {
-        printf( "Speculatively reduced model has no primary outputs.\n" );
+//        printf( "Speculatively reduced model has no primary outputs.\n" );
         Gia_ManAppendCo( pNew, 0 );
     }
     ABC_FREE( p->pCopies );
@@ -931,6 +1014,41 @@ Gia_Man_t * Gia_ManSpecReduceInit( Gia_Man_t * p, Gia_Cex_t * pInit, int nFrames
 
 /**Function*************************************************************
 
+  Synopsis    [Creates initialized SRM with the given number of frames.]
+
+  Description [Uses as many frames as needed to create the number of 
+  output not less than the number of equivalence literals.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManSpecReduceInitFrames( Gia_Man_t * p, Gia_Cex_t * pInit, int nFramesMax, int * pnFrames, int fDualOut, int nMinOutputs )
+{
+    Gia_Man_t * pFrames;
+    int f, nLits;
+    nLits = Gia_ManEquivCountLits( p );
+    for ( f = 1; ; f++ )
+    {
+        pFrames = Gia_ManSpecReduceInit( p, pInit, f, fDualOut );
+        if ( (nMinOutputs == 0 && Gia_ManPoNum(pFrames) >= nLits/2+1) || 
+             (nMinOutputs != 0 && Gia_ManPoNum(pFrames) >= nMinOutputs) )
+            break;
+        if ( f == nFramesMax )
+            break;
+        Gia_ManStop( pFrames );
+        pFrames = NULL;
+    }
+    if ( f == nFramesMax )
+        printf( "Stopped unrolling after %d frames.\n", nFramesMax );
+    if ( pnFrames )
+        *pnFrames = f;
+    return pFrames;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Transforms equiv classes by removing the AB nodes.]
 
   Description []
@@ -1292,6 +1410,107 @@ Gia_Man_t * Gia_ManEquivToChoices( Gia_Man_t * p, int nSnapshots )
     return pNew;
 }
 
+#include "aig.h"
+#include "saig.h"
+#include "cec.h"
+#include "giaAig.h"
+
+/**Function*************************************************************
+
+  Synopsis    [Implements iteration during speculation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_CommandSpecI( Gia_Man_t * pGia, int nFramesInit, int nBTLimitInit, int fStart, int fCheckMiter, int fVerbose )
+{
+    extern int Cec_ManCheckNonTrivialCands( Gia_Man_t * pAig );
+    Aig_Man_t * pTemp;
+    Gia_Man_t * pSrm, * pReduce, * pAux;
+    int nIter, nStart = 0;
+    if ( pGia->pReprs == NULL || pGia->pNexts == NULL )
+    {
+        printf( "Gia_CommandSpecI(): Equivalence classes are not defined.\n" );
+        return 0;
+    }
+    // (spech)*  where spech = &srm; restore save3; bmc2 -F 100 -C 25000; &resim
+    Gia_ManCleanMark0( pGia );
+    Gia_ManPrintStats( pGia, 0 );
+    for ( nIter = 0; ; nIter++ )
+    {
+        if ( Gia_ManHasNoEquivs(pGia) )
+        {
+            printf( "Gia_CommandSpecI: No equivalences left.\n" );
+            break;
+        }
+        printf( "ITER %3d : ", nIter );
+//      if ( fVerbose )
+//            printf( "Starting BMC from frame %d.\n", nStart );
+//      if ( fVerbose )
+//            Gia_ManPrintStats( pGia, 0 );
+            Gia_ManPrintStatsClasses( pGia );
+        // perform speculative reduction
+//        if ( Gia_ManPoNum(pSrm) <= Gia_ManPoNum(pGia) )
+        if ( !Cec_ManCheckNonTrivialCands(pGia) )
+        {
+            printf( "Gia_CommandSpecI: There are only trivial equiv candidates left (PO drivers). Quitting.\n" );
+            break;
+        }
+        pSrm = Gia_ManSpecReduce( pGia, 0, 0 ); 
+        // bmc2 -F 100 -C 25000
+        {
+            Gia_Cex_t * pCex;
+            int nFrames     = nFramesInit; // different from default
+            int nNodeDelta  = 2000;
+            int nBTLimit    = nBTLimitInit; // different from default
+            int nBTLimitAll = 2000000;
+            pTemp = Gia_ManToAig( pSrm, 0 );
+//            Aig_ManPrintStats( pTemp );
+            Gia_ManStop( pSrm );
+            Saig_BmcPerform( pTemp, nStart, nFrames, nNodeDelta, 20, nBTLimit, nBTLimitAll, fVerbose, 0 );
+            pCex = pTemp->pSeqModel; pTemp->pSeqModel = NULL;
+            Aig_ManStop( pTemp );
+            if ( pCex == NULL )
+            {
+                printf( "Gia_CommandSpecI(): Internal BMC could not find a counter-example.\n" );
+                break;
+            }
+            if ( fStart ) 
+                nStart = pCex->iFrame;
+            // perform simulation
+            {
+                Cec_ParSim_t Pars, * pPars = &Pars;
+                Cec_ManSimSetDefaultParams( pPars );
+                pPars->fCheckMiter = fCheckMiter;
+                if ( Cec_ManSeqResimulateCounter( pGia, pPars, pCex ) )
+                {
+                    ABC_FREE( pCex );
+                    break;
+                }
+                ABC_FREE( pCex );
+            }
+        } 
+        // write equivalence classes
+        Gia_WriteAiger( pGia, "gore.aig", 0, 0 );
+        // reduce the model
+        pReduce = Gia_ManSpecReduce( pGia, 0, 0 );
+        if ( pReduce )
+        {
+            pReduce = Gia_ManSeqStructSweep( pAux = pReduce, 1, 1, 0 );
+            Gia_ManStop( pAux );
+            Gia_WriteAiger( pReduce, "gsrm.aig", 0, 0 );
+//            printf( "Speculatively reduced model was written into file \"%s\".\n", "gsrm.aig" );
+//          Gia_ManPrintStatsShort( pReduce );
+            Gia_ManStop( pReduce );
+        }
+    }
+    return 1;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/int/intCore.c b/src/aig/int/intCore.c
index 6d29dfb9..d1f89c07 100644
--- a/src/aig/int/intCore.c
+++ b/src/aig/int/intCore.c
@@ -193,7 +193,7 @@ p->timeCnf += clock() - clk;
                 }
                 // likely spurious counter-example
                 p->nFrames += i;
-                Inter_ManClean( p );
+                Inter_ManClean( p ); 
                 break;
             }
             else if ( RetValue == -1 ) // timed out
diff --git a/src/aig/ioa/ioaReadAig.c b/src/aig/ioa/ioaReadAig.c
index b81414a5..6aaa6c64 100644
--- a/src/aig/ioa/ioaReadAig.c
+++ b/src/aig/ioa/ioaReadAig.c
@@ -88,34 +88,27 @@ Vec_Int_t * Ioa_WriteDecodeLiterals( char ** ppPos, int nEntries )
 
 /**Function*************************************************************
 
-  Synopsis    [Reads the AIG in the binary AIGER format.]
+  Synopsis    [Reads the AIG in from the memory buffer.]
 
-  Description []
+  Description [The buffer constains the AIG in AIGER format. The size gives
+  the number of types in the buffer. The buffer is allocated by the user 
+  and not deallocated by this procedure.]
   
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Ioa_ReadAiger( char * pFileName, int fCheck )
+Aig_Man_t * Ioa_ReadAigerFromMemory( char * pContents, int nFileSize, int fCheck )
 {
-//    Bar_Progress_t * pProgress;
-    FILE * pFile;
     Vec_Int_t * vLits = NULL;
     Vec_Ptr_t * vNodes, * vDrivers;//, * vTerms;
     Aig_Obj_t * pObj, * pNode0, * pNode1;
     Aig_Man_t * pNew;
-    int nTotal, nInputs, nOutputs, nLatches, nAnds, nFileSize, i;//, iTerm, nDigits;
-    char * pContents, * pDrivers, * pSymbols, * pCur, * pName;//, * pType;
+    int nTotal, nInputs, nOutputs, nLatches, nAnds, i;//, iTerm, nDigits;
+    char * pDrivers, * pSymbols, * pCur;//, * pType;
     unsigned uLit0, uLit1, uLit;
 
-    // read the file into the buffer
-    nFileSize = Ioa_FileSize( pFileName );
-    pFile = fopen( pFileName, "rb" );
-    pContents = ABC_ALLOC( char, nFileSize );
-    fread( pContents, nFileSize, 1, pFile );
-    fclose( pFile );
-
     // check if the input file format is correct
     if ( strncmp(pContents, "aig", 3) != 0 || (pContents[3] != ' ' && pContents[3] != '2') )
     {
@@ -145,10 +138,6 @@ Aig_Man_t * Ioa_ReadAiger( char * pFileName, int fCheck )
 
     // allocate the empty AIG
     pNew = Aig_ManStart( nAnds );
-    pName = Ioa_FileNameGeneric( pFileName );
-    pNew->pName = Aig_UtilStrsav( pName );
-//    pNew->pSpec = Ioa_UtilStrsav( pFileName );
-    ABC_FREE( pName );
 
     // prepare the array of nodes
     vNodes = Vec_PtrAlloc( 1 + nInputs + nLatches + nAnds );
@@ -355,7 +344,6 @@ Aig_Man_t * Ioa_ReadAiger( char * pFileName, int fCheck )
     }
 
     // skipping the comments
-    ABC_FREE( pContents );
     Vec_PtrFree( vNodes );
 
     // remove the extra nodes
@@ -372,6 +360,43 @@ Aig_Man_t * Ioa_ReadAiger( char * pFileName, int fCheck )
     return pNew;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Reads the AIG in the binary AIGER format.]
+
+  Description []
+  
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Ioa_ReadAiger( char * pFileName, int fCheck )
+{
+    FILE * pFile;
+    Aig_Man_t * pNew;
+    char * pName, * pContents;
+    int nFileSize;
+
+    // read the file into the buffer
+    nFileSize = Ioa_FileSize( pFileName );
+    pFile = fopen( pFileName, "rb" );
+    pContents = ABC_ALLOC( char, nFileSize );
+    fread( pContents, nFileSize, 1, pFile );
+    fclose( pFile );
+
+    pNew = Ioa_ReadAigerFromMemory( pContents, nFileSize, fCheck );
+    ABC_FREE( pContents );
+    if ( pNew )
+    {
+        pName = Ioa_FileNameGeneric( pFileName );
+        pNew->pName = Aig_UtilStrsav( pName );
+//        pNew->pSpec = Ioa_UtilStrsav( pFileName );
+        ABC_FREE( pName );
+    }
+    return pNew;
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/aig/ntl/ntlFraig.c b/src/aig/ntl/ntlFraig.c
index 3ca8dfd7..1d7ac393 100644
--- a/src/aig/ntl/ntlFraig.c
+++ b/src/aig/ntl/ntlFraig.c
@@ -21,6 +21,7 @@
 #include "ntl.h"
 #include "fra.h"
 #include "ssw.h"
+#include "dch.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -400,12 +401,17 @@ Ntl_Man_t * Ntl_ManFraig( Ntl_Man_t * p, int nPartSize, int nConfLimit, int nLev
     }
 
     // perform fraiging for the given design
-//    if ( fUseCSat )
-    if ( 0 )
+    if ( fUseCSat )
     {
-        extern Aig_Man_t * Cec_FraigCombinational( Aig_Man_t * pAig, int nConfs, int fVerbose );
-        pTemp = Cec_FraigCombinational( pAigCol, nConfLimit, fVerbose );
-        Aig_ManStop( pTemp );
+//        extern Aig_Man_t * Cec_FraigCombinational( Aig_Man_t * pAig, int nConfs, int fVerbose );
+//        pTemp = Cec_FraigCombinational( pAigCol, nConfLimit, fVerbose );
+//        Aig_ManStop( pTemp );
+        extern void Dch_ComputeEquivalences( Aig_Man_t * pAig, Dch_Pars_t * pPars );
+        Dch_Pars_t Pars, * pPars = &Pars;
+        Dch_ManSetDefaultParams( pPars );
+        pPars->nBTLimit = nConfLimit;
+        pPars->fVerbose = fVerbose;
+        Dch_ComputeEquivalences( pAigCol, pPars );
     }
     else
     {
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index 85d2d191..b77a4292 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -90,10 +90,10 @@ static inline Aig_Obj_t *  Saig_ObjLiToLo( Aig_Man_t * p, Aig_Obj_t * pObj )  {
 ////////////////////////////////////////////////////////////////////////
 
 /*=== sswAbs.c ==========================================================*/
-extern Aig_Man_t *       Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int nRatio, int fVerbose );
+extern Aig_Man_t *       Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int nRatio, int fUseBdds, int fUseDprove, int fUseStart, int fVerbose );
 /*=== 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 void              Saig_BmcPerform( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, int nConfMaxOne, int nConfMaxAll, int fVerbose );
+extern void              Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite );
 /*=== 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 3da92fc0..844d6f24 100644
--- a/src/aig/saig/saigAbs.c
+++ b/src/aig/saig/saigAbs.c
@@ -25,6 +25,7 @@
 #include "satStore.h"
 #include "ssw.h"
 #include "ioa.h"
+#include "fra.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -694,17 +695,38 @@ Ssw_Cex_t * Saig_ManCexShrink( Aig_Man_t * p, Aig_Man_t * pAbs, Ssw_Cex_t * pCex
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Saig_ManProofRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlops, int nFrames, int nConfMaxOne, int fVerbose )
+Aig_Man_t * Saig_ManProofRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlops, int nFrames, int nConfMaxOne, int fUseBdds, int fUseDprove, int * pnUseStart, int fVerbose )
 { 
-    extern void Saig_BmcPerform( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, int nConfMaxOne, int nConfMaxAll, int fVerbose );
+    extern void Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite );
     extern Vec_Int_t * Saig_ManExtendCounterExampleTest( Aig_Man_t * p, int iFirstPi, void * pCex, int fVerbose );
+    extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fReorderImage, int fVerbose, int fSilent );
 
     Vec_Int_t * vFlopsNew, * vPiToReg;
     Aig_Obj_t * pObj;
     int i, Entry, iFlop;
-    Saig_BmcPerform( pAbs, nFrames, 2000, nConfMaxOne, 1000000, fVerbose );
+    if ( fUseDprove && Aig_ManRegNum(pAbs) > 0 )
+    {
+        Fra_Sec_t SecPar, * pSecPar = &SecPar;
+        int RetValue;
+        Fra_SecSetDefaultParams( pSecPar );
+        pSecPar->fVerbose       = fVerbose;
+        RetValue = Fra_FraigSec( pAbs, pSecPar, NULL );
+    }
+    else if ( fUseBdds && (Aig_ManRegNum(pAbs) > 0 && Aig_ManRegNum(pAbs) <= 80) )
+    {
+        int nBddMax       = 1000000;
+        int nIterMax      = nFrames;
+        int fPartition    = 1;
+        int fReorder      = 1;
+        int fReorderImage = 1;
+        Aig_ManVerifyUsingBdds( pAbs, nBddMax, nIterMax, fPartition, fReorder, fReorderImage, fVerbose, 0 );
+    }
+    else 
+        Saig_BmcPerform( pAbs, pnUseStart? *pnUseStart: 0, nFrames, 2000, 20, nConfMaxOne, 1000000, fVerbose, 0 );
     if ( pAbs->pSeqModel == NULL )
         return NULL;
+    if ( pnUseStart )
+        *pnUseStart = ((Fra_Cex_t *)pAbs->pSeqModel)->iFrame;
 //    Saig_ManExtendCounterExampleTest( p->pAig, 0, p->pAig->pSeqModel );
     vFlopsNew = Saig_ManExtendCounterExampleTest( pAbs, Saig_ManPiNum(p), pAbs->pSeqModel, fVerbose );
     if ( Vec_IntSize(vFlopsNew) == 0 )
@@ -766,7 +788,7 @@ Aig_Man_t * Saig_ManProofRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vF
   SeeAlso     []
  
 ***********************************************************************/
-Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int nRatio, int fVerbose )
+Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int nRatio, int fUseBdds, int fUseDprove, int fUseStart, int fVerbose )
 {
     Aig_Man_t * pResult, * pTemp;
     Cnf_Dat_t * pCnf;
@@ -845,13 +867,14 @@ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax,
         Saig_AbsExtendOneStep( p, vFlops );
         if ( fVerbose )
             printf( " %d flops.\n", Vec_IntSize(vFlops) );
-    }
+    } 
 */
     // create the resulting AIG
     pResult = Saig_ManAbstraction( p, vFlops );
 
     if ( fExtend )
     {
+        int nUseStart = 0;
         if ( !fVerbose )
         {
             printf( "Init : " );
@@ -860,21 +883,19 @@ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax,
         printf( "Refining abstraction...\n" );
         for ( Iter = 0; ; Iter++ )
         {
-            char FileName[100];
-            pTemp = Saig_ManProofRefine( p, pResult, vFlops, nFramesBmc, nConfMaxBmc, fVerbose );
+            pTemp = Saig_ManProofRefine( p, pResult, vFlops, nFramesBmc, nConfMaxBmc, fUseBdds, fUseDprove, fUseStart?&nUseStart:NULL, fVerbose );
             if ( pTemp == NULL )
                 break;
             Aig_ManStop( pResult );
             pResult = pTemp;
-            printf( "%4d : ", Iter );
+            printf( "ITER %4d : ", Iter );
             if ( !fVerbose )
                 Aig_ManPrintStats( pResult );
-            else
-                printf( " -----------------------------------------------------\n" );
+//            else
+//                printf( " -----------------------------------------------------\n" );
             // output the intermediate result of abstraction
-            sprintf( FileName, "gabs%02d.aig", Iter );
-            Ioa_WriteAiger( pResult, FileName, 0, 0 );
-            printf( "Intermediate abstracted model was written into file \"%s\".\n", FileName );
+            Ioa_WriteAiger( pResult, "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(pTemp))/Aig_ManRegNum(p) < 1.0*nRatio )
             {
@@ -886,6 +907,12 @@ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax,
         }
     }
     Vec_IntFree( vFlops );
+    // write the final result
+    if ( pResult )
+    {
+        Ioa_WriteAiger( pResult, "gabs.aig", 0, 0 );
+        printf( "Final abstracted model was written into file \"%s\".\n", "gabs.aig" );
+    }
     return pResult;
 }
 
diff --git a/src/aig/saig/saigBmc.c b/src/aig/saig/saigBmc.c
index 57759594..a37be3ad 100644
--- a/src/aig/saig/saigBmc.c
+++ b/src/aig/saig/saigBmc.c
@@ -508,7 +508,7 @@ Ssw_Cex_t * Saig_BmcGenerateCounterExample( Saig_Bmc_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Saig_BmcSolveTargets( Saig_Bmc_t * p )
+int Saig_BmcSolveTargets( Saig_Bmc_t * p, int nStart, int * pnOutsSolved )
 {
     Aig_Obj_t * pObj;
     int i, VarNum, Lit, RetValue;
@@ -520,6 +520,8 @@ int Saig_BmcSolveTargets( Saig_Bmc_t * p )
     }
     Vec_PtrForEachEntry( p->vTargets, pObj, i )
     {
+        if ( ((*pnOutsSolved)++ / Saig_ManPoNum(p->pAig)) < nStart )
+            continue;
         if ( p->pSat->stats.conflicts > p->nConfMaxAll )
             return l_Undef;
         VarNum = Saig_BmcSatNum( p, Aig_Regular(pObj) );
@@ -575,11 +577,12 @@ void Saig_BmcAddTargetsAsPos( Saig_Bmc_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Saig_BmcPerform( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, int nConfMaxOne, int nConfMaxAll, int fVerbose )
+void Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite )
 {
     Saig_Bmc_t * p;
     Aig_Man_t * pNew;
     Cnf_Dat_t * pCnf;
+    int nOutsSolved = 0;
     int Iter, RetValue, clk = clock(), clk2;
     p = Saig_BmcManStart( pAig, nFramesMax, nNodesMax, nConfMaxOne, nConfMaxAll, fVerbose );
     if ( fVerbose )
@@ -609,7 +612,7 @@ void Saig_BmcPerform( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, int nConf
         Cnf_DataFree( pCnf );
         Aig_ManStop( pNew );
         // solve the targets
-        RetValue = Saig_BmcSolveTargets( p );
+        RetValue = Saig_BmcSolveTargets( p, nStart, &nOutsSolved );
         if ( fVerbose )
         {
             printf( "%3d : F = %3d. O =%4d.  And = %7d. Var = %7d. Conf = %7d. ", 
@@ -620,11 +623,21 @@ void Saig_BmcPerform( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, int nConf
             break;
     }
     if ( RetValue == l_True )
+    {
+        assert( p->iFrameFail * Saig_ManPoNum(p->pAig) + p->iOutputFail + 1 == nOutsSolved );
         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( "No output was asserted in %d frames.  ", p->iFramePrev-1 );
-    ABC_PRT( "Time", clock() - clk );
+    if ( fVerbOverwrite )
+    {
+        ABC_PRTr( "Time", clock() - clk );
+    }
+    else
+    {
+        ABC_PRT( "Time", clock() - clk );
+    }
     if ( RetValue != l_True )
     {
         if ( p->iFrameLast >= p->nFramesMax )