Version abc81014

30 files changed, 916 insertions, 233 deletions

diff --git a/abc.dsp b/abc.dsp
index 0e7f00b1..b7d65ae3 100644
--- a/abc.dsp
+++ b/abc.dsp
@@ -3474,6 +3474,10 @@ SOURCE=.\src\aig\ssw\sswCore.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\ssw\sswDyn.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\ssw\sswInt.h
 # End Source File
 # Begin Source File
diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 18bcb1b4..2e409312 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -634,6 +634,7 @@ extern int             Aig_ManLevels( Aig_Man_t * p );
 extern void            Aig_ManResetRefs( Aig_Man_t * p );
 extern void            Aig_ManCleanMarkA( Aig_Man_t * p );
 extern void            Aig_ManCleanMarkB( Aig_Man_t * p );
+extern void            Aig_ManCleanMarkAB( Aig_Man_t * p );
 extern void            Aig_ManCleanData( Aig_Man_t * p );
 extern void            Aig_ObjCleanData_rec( Aig_Obj_t * pObj );
 extern void            Aig_ObjCollectMulti( Aig_Obj_t * pFunc, Vec_Ptr_t * vSuper );
diff --git a/src/aig/aig/aigDfs.c b/src/aig/aig/aigDfs.c
index 568d6a68..db80a7f9 100644
--- a/src/aig/aig/aigDfs.c
+++ b/src/aig/aig/aigDfs.c
@@ -699,6 +699,8 @@ void Aig_Support_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vSupp )
     if ( Aig_ObjIsTravIdCurrent(p, pObj) )
         return;
     Aig_ObjSetTravIdCurrent(p, pObj);
+    if ( Aig_ObjIsConst1(pObj) )
+        return;
     if ( Aig_ObjIsPi(pObj) )
     {
         Vec_PtrPush( vSupp, pObj );
diff --git a/src/aig/aig/aigUtil.c b/src/aig/aig/aigUtil.c
index 00685ef8..e5b4d2c7 100644
--- a/src/aig/aig/aigUtil.c
+++ b/src/aig/aig/aigUtil.c
@@ -168,6 +168,25 @@ void Aig_ManCleanMarkB( Aig_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Cleans fMarkB.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManCleanMarkAB( Aig_Man_t * p )
+{
+    Aig_Obj_t * pObj;
+    int i;
+    Aig_ManForEachObj( p, pObj, i )
+        pObj->fMarkA = pObj->fMarkB = 0;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Cleans the data pointers for the nodes.]
 
   Description []
diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
index dc98adc9..e7cd0550 100644
--- a/src/aig/fra/fra.h
+++ b/src/aig/fra/fra.h
@@ -118,6 +118,8 @@ struct Fra_Sec_t_
     int              nFramesMax;        // the max number of frames used for induction
     int              nBTLimit;          // the conflict limit at a node
     int              nBTLimitGlobal;    // the global conflict limit
+    int              nBTLimitInter;     // the conflict limit for interpolation
+    int              nBddVarsMax;       // the state space limit for BDD reachability
     int              nBddMax;           // the max number of BDD nodes
     int              nBddIterMax;       // the limit on the number of BDD iterations
     int              fPhaseAbstract;    // enables phase abstraction
@@ -361,7 +363,7 @@ extern int                 Fra_NodesAreClause( Fra_Man_t * p, Aig_Obj_t * pOld,
 extern int                 Fra_NodeIsConst( Fra_Man_t * p, Aig_Obj_t * pNew );
 /*=== fraSec.c ========================================================*/
 extern void                Fra_SecSetDefaultParams( Fra_Sec_t * p );
-extern int                 Fra_FraigSec( Aig_Man_t * p, Fra_Sec_t * pParSec );
+extern int                 Fra_FraigSec( Aig_Man_t * p, Fra_Sec_t * pParSec, Aig_Man_t ** ppResult );
 /*=== fraSim.c ========================================================*/
 extern int                 Fra_SmlNodeHash( Aig_Obj_t * pObj, int nTableSize );
 extern int                 Fra_SmlNodeIsConst( Aig_Obj_t * pObj );
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index f7674f7d..c8b35b28 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -32,7 +32,7 @@
 
 /**Function*************************************************************
 
-  Synopsis    [Performs AIG rewriting on the constaint manager.]
+  Synopsis    [Performs AIG rewriting on the constraint manager.]
 
   Description []
                
@@ -536,7 +536,7 @@ p->timeTrav += clock() - clk2;
         // report the intermediate results
         if ( pPars->fVerbose )
         {
-            printf( "%3d : Const = %6d. Cl = %6d.  L = %6d. LR = %6d.  ", 
+            printf( "%3d : C = %6d. Cl = %6d.  L = %6d. LR = %6d.  ", 
                 nIter, Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), 
                 Fra_ClassesCountLits(p->pCla), p->pManFraig->nAsserts );
             if ( p->pCla->vImps )
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index 216ed8df..cae37f85 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -51,6 +51,8 @@ void Fra_SecSetDefaultParams( Fra_Sec_t * p )
     p->nFramesMax        =       4;  // the max number of frames used for induction
     p->nBTLimit          =    1000;  // conflict limit at a node during induction 
     p->nBTLimitGlobal    = 5000000;  // global conflict limit during induction
+    p->nBTLimitInter     =   10000;  // conflict limit during interpolation
+    p->nBddVarsMax       =     150;  // the limit on the number of registers in BDD reachability
     p->nBddMax           =   50000;  // the limit on the number of BDD nodes 
     p->nBddIterMax       = 1000000;  // the limit on the number of BDD iterations
     p->fPhaseAbstract    =       0;  // enables phase abstraction
@@ -81,7 +83,7 @@ void Fra_SecSetDefaultParams( Fra_Sec_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Fra_FraigSec( Aig_Man_t * p, Fra_Sec_t * pParSec )
+int Fra_FraigSec( Aig_Man_t * p, Fra_Sec_t * pParSec, Aig_Man_t ** ppResult )
 {
     Ssw_Pars_t Pars2, * pPars2 = &Pars2;
     Fra_Ssw_t Pars, * pPars = &Pars;
@@ -461,6 +463,7 @@ clk = clock();
         int Depth;
 
         Inter_ManSetDefaultParams( pPars );
+        pPars->nBTLimit = pParSec->nBTLimitInter;
         pPars->fVerbose = pParSec->fVeryVerbose;
         if ( Saig_ManPoNum(pNew) == 1 )
         {
@@ -495,7 +498,7 @@ PRT( "Time", clock() - clk );
     }
 
     // try reachability analysis
-    if ( pParSec->fReachability && RetValue == -1 && Aig_ManRegNum(pNew) > 0 && Aig_ManRegNum(pNew) < 150 )
+    if ( pParSec->fReachability && RetValue == -1 && Aig_ManRegNum(pNew) > 0 && Aig_ManRegNum(pNew) < pParSec->nBddVarsMax )
     {
         extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose, int fSilent );
         pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew); 
@@ -563,6 +566,8 @@ PRT( "Time", clock() - clkTotal );
         FREE( pNew->pSeqModel );
         }
     }
+    if ( ppResult != NULL )
+        *ppResult = Aig_ManDupSimpleDfs( pNew );
     if ( pNew )
         Aig_ManStop( pNew );
     return RetValue;
diff --git a/src/aig/mfx/mfxResub.c b/src/aig/mfx/mfxResub.c
index 7179173b..006656ee 100644
--- a/src/aig/mfx/mfxResub.c
+++ b/src/aig/mfx/mfxResub.c
@@ -463,6 +463,9 @@ int Mfx_ResubNode( Mfx_Man_t * p, Nwk_Obj_t * pNode )
     }
     if ( Nwk_ObjFaninNum(pNode) == p->nFaninMax )
         return 0;
+
+    return 0; /// !!!!! temporary workaround
+
     // try replacing area critical fanins while adding two new fanins
     Nwk_ObjForEachFanin( pNode, pFanin, i )
         if ( !Nwk_ObjIsCi(pFanin) && Nwk_ObjFanoutNum(pFanin) == 1 )
diff --git a/src/aig/ssw/module.make b/src/aig/ssw/module.make
index 915f7dd0..a7d940b4 100644
--- a/src/aig/ssw/module.make
+++ b/src/aig/ssw/module.make
@@ -3,6 +3,7 @@ SRC +=    src/aig/ssw/sswAig.c \
     src/aig/ssw/sswClass.c \
     src/aig/ssw/sswCnf.c \
     src/aig/ssw/sswCore.c \
+    src/aig/ssw/sswDyn.c \
     src/aig/ssw/sswLcorr.c \
     src/aig/ssw/sswMan.c \
     src/aig/ssw/sswPart.c \
diff --git a/src/aig/ssw/ssw.h b/src/aig/ssw/ssw.h
index 2d067a17..73226dbe 100644
--- a/src/aig/ssw/ssw.h
+++ b/src/aig/ssw/ssw.h
@@ -17,7 +17,7 @@
   Revision    [$Id: ssw.h,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
 
 ***********************************************************************/
- 
+
 #ifndef __SSW_H__
 #define __SSW_H__
 
@@ -55,12 +55,16 @@ struct Ssw_Pars_t_
     int              fLatchCorr;    // perform register correspondence
     int              fSemiFormal;   // enable semiformal filtering
     int              fUniqueness;   // enable uniqueness constraints
+    int              fDynamic;      // enable dynamic addition of constraints
     int              fVerbose;      // verbose stats
     int              fFlopVerbose;  // verbose printout of redundant flops
     // optimized latch correspondence
     int              fLatchCorrOpt; // perform register correspondence (optimized)
     int              nSatVarMax;    // max number of SAT vars before recycling SAT solver (optimized latch corr only)
     int              nRecycleCalls; // calls to perform before recycling SAT solver (optimized latch corr only)
+    // optimized signal correspondence
+    int              nSatVarMax2;   // max number of SAT vars before recycling SAT solver (optimized latch corr only)
+    int              nRecycleCalls2;// calls to perform before recycling SAT solver (optimized latch corr only)
     // internal parameters
     int              nIters;        // the number of iterations performed
     int              nConflicts;    // the total number of conflicts performed
diff --git a/src/aig/ssw/sswClass.c b/src/aig/ssw/sswClass.c
index cfbb138c..f234a58f 100644
--- a/src/aig/ssw/sswClass.c
+++ b/src/aig/ssw/sswClass.c
@@ -493,11 +493,22 @@ void Ssw_ClassesRemoveNode( Ssw_Cla_t * p, Aig_Obj_t * pObj )
 ***********************************************************************/
 Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs, int fVerbose )
 {
+//    int nFrames =  4;
+//    int nWords  =  1;
+//    int nIters  = 16;
+
+//    int nFrames = 32;
+//    int nWords  =  4;
+//    int nIters  =  0;
+
+    int nFrames =  4;
+    int nWords  =  2;
+    int nIters  = 16;
     Ssw_Cla_t * p;
     Ssw_Sml_t * pSml;
     Aig_Obj_t ** ppTable, ** ppNexts, ** ppClassNew;
     Aig_Obj_t * pObj, * pTemp, * pRepr;
-    int i, k, nTableSize, nNodes, iEntry, nEntries, nEntries2;
+    int i, k, nTableSize, nNodes, iEntry, nEntries, nEntries2, RetValue;
     int clk;
 
     // start the classes
@@ -505,10 +516,13 @@ Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs,
 
     // perform sequential simulation
 clk = clock();
-    pSml = Ssw_SmlSimulateSeq( pAig, 0, 32, 4 );
+    pSml = Ssw_SmlSimulateSeq( pAig, 0, nFrames, nWords );
 if ( fVerbose )
 {
-PRT( "Simulation of 32 frames with 4 words", clock() - clk );
+    printf( "Allocated %.2f Mb for simulation information.\n", 
+        1.0*(sizeof(unsigned) * Aig_ManObjNumMax(pAig) * nFrames * nWords)/(1<<20) );
+    printf( "Initial simulation of %d frames with %d words.     ", nFrames, nWords );
+    PRT( "Time", clock() - clk );
 }
 
     // set comparison procedures
@@ -603,13 +617,36 @@ clk = clock();
 
     // now it is time to refine the classes
     Ssw_ClassesRefine( p, 1 );
+if ( fVerbose )
+{
+    printf( "Collecting candidate equivalence classes.        " );
+PRT( "Time", clock() - clk );
+}
+
+clk = clock();
+    // perform iterative refinement using simulation
+    k = 0;
+    for ( i = 1; i < nIters; i++ )
+    {
+        Ssw_SmlResimulateSeq( pSml );
+        // simulate internal nodes
+        Ssw_SmlSimulateOne( pSml );
+        // check equivalence classes
+        RetValue = Ssw_ClassesRefineConst1( p, 1 );
+        RetValue += Ssw_ClassesRefine( p, 1 );
+        k++;
+        if ( RetValue == 0 )
+            break;
+    }
     Ssw_ClassesCheck( p );
     Ssw_SmlStop( pSml );
-//    Ssw_ClassesPrint( p, 0 );
 if ( fVerbose )
 {
-PRT( "Collecting candidate equival classes", clock() - clk );
+    printf( "Simulation of %d frames with %d words (%2d rounds). ", 
+        nFrames, nWords, k );
+    PRT( "Time", clock() - clk );
 }
+//    Ssw_ClassesPrint( p, 0 );
     return p;
 }
 
diff --git a/src/aig/ssw/sswCnf.c b/src/aig/ssw/sswCnf.c
index d068bb78..c5ea9b28 100644
--- a/src/aig/ssw/sswCnf.c
+++ b/src/aig/ssw/sswCnf.c
@@ -77,6 +77,8 @@ Ssw_Sat_t * Ssw_SatStart( int fPolarFlip )
 ***********************************************************************/
 void Ssw_SatStop( Ssw_Sat_t * p )
 {
+//    printf( "Recycling SAT solver with %d vars and %d restarts.\n", 
+//        p->pSat->size, p->pSat->stats.starts );
     if ( p->pSat )
         sat_solver_delete( p->pSat );
     Vec_IntFree( p->vSatVars );
diff --git a/src/aig/ssw/sswCore.c b/src/aig/ssw/sswCore.c
index 39f4c736..6db8cc3a 100644
--- a/src/aig/ssw/sswCore.c
+++ b/src/aig/ssw/sswCore.c
@@ -60,6 +60,9 @@ void Ssw_ManSetDefaultParams( Ssw_Pars_t * p )
     p->fLatchCorrOpt  =       0;  // performs optimized register correspondence
     p->nSatVarMax     =    1000;  // the max number of SAT variables
     p->nRecycleCalls  =      50;  // calls to perform before recycling SAT solver
+    // signal correspondence
+    p->nSatVarMax2    =    5000;  // the max number of SAT variables
+    p->nRecycleCalls2 =     250;  // calls to perform before recycling SAT solver
     // return values
     p->nIters         =       0;  // the number of iterations performed
 }
@@ -95,7 +98,7 @@ void Ssw_ManSetDefaultParamsLcorr( Ssw_Pars_t * p )
 ***********************************************************************/
 Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p )
 {
-    int nSatProof, nSatCallsSat, nRecycles, nSatFailsReal;
+    int nSatProof, nSatCallsSat, nRecycles, nSatFailsReal, nUniques;
     Aig_Man_t * pAigNew;
     int RetValue, nIter;
     int clk, clkTotal = clock();
@@ -137,7 +140,7 @@ Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p )
     }
 */
     // refine classes using induction
-    nSatProof = nSatCallsSat = nRecycles = nSatFailsReal = 0;
+    nSatProof = nSatCallsSat = nRecycles = nSatFailsReal = nUniques = 0;
     for ( nIter = 0; ; nIter++ )
     {
 clk = clock();
@@ -147,29 +150,44 @@ clk = clock();
             RetValue = Ssw_ManSweepLatch( p );
             if ( p->pPars->fVerbose )
             {
-                printf( "%3d : Const = %6d. Cl = %6d. Pr = %5d. Cex = %5d. Rcl = %3d. F = %3d. ", 
+                printf( "%3d : C =%7d. Cl =%7d. Pr =%6d. Cex =%5d. Rcl = %3d. F = %3d. ", 
                     nIter, Ssw_ClassesCand1Num(p->ppClasses), Ssw_ClassesClassNum(p->ppClasses), 
                     p->nSatProof-nSatProof, p->nSatCallsSat-nSatCallsSat, 
                     p->nRecycles-nRecycles, p->nSatFailsReal-nSatFailsReal );
                 PRT( "T", clock() - clk );
-                nSatProof     = p->nSatProof;
-                nSatCallsSat  = p->nSatCallsSat;
-                nRecycles     = p->nRecycles;
-                nSatFailsReal = p->nSatFailsReal;
             } 
         }
         else
         {
-            RetValue = Ssw_ManSweep( p );
+            if ( p->pPars->fDynamic )
+                RetValue = Ssw_ManSweepDyn( p );
+            else
+                RetValue = Ssw_ManSweep( p );
             p->pPars->nConflicts += p->pMSat->pSat->stats.conflicts;
             if ( p->pPars->fVerbose )
             {
-                printf( "%3d : Const = %6d. Cl = %6d. LR = %6d. NR = %6d. U = %3d. F = %2d. ", 
+                printf( "%3d : C =%7d. Cl =%7d. LR =%6d. NR =%6d. ", 
                     nIter, Ssw_ClassesCand1Num(p->ppClasses), Ssw_ClassesClassNum(p->ppClasses), 
-                    p->nConstrReduced, Aig_ManNodeNum(p->pFrames), p->nUniques, p->nSatFailsReal );
+                    p->nConstrReduced, Aig_ManNodeNum(p->pFrames) );
+                if ( p->pPars->fUniqueness )
+                    printf( "U =%4d. ", p->nUniques-nUniques );
+                else if ( p->pPars->fDynamic )
+                {
+                    printf( "Cex =%5d. ", p->nSatCallsSat-nSatCallsSat );
+                    printf( "R =%3d. ",   p->nRecycles-nRecycles );
+                }
+                printf( "F =%3d. ", p->nSatFailsReal-nSatFailsReal );
                 PRT( "T", clock() - clk );
             } 
         }
+        nSatProof     = p->nSatProof;
+        nSatCallsSat  = p->nSatCallsSat;
+        nRecycles     = p->nRecycles;
+        nSatFailsReal = p->nSatFailsReal;
+        nUniques      = p->nUniques;
+
+        p->nVarsMax  = AIG_MAX( p->nVarsMax,  p->pMSat->nSatVars );
+        p->nCallsMax = AIG_MAX( p->nCallsMax, p->pMSat->nSolverCalls );
         Ssw_SatStop( p->pMSat );
         p->pMSat = NULL;
         Ssw_ManCleanup( p );
@@ -234,13 +252,12 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
     {
         pPars->nFramesAddSim = 0;
         if ( pPars->nFramesK != 2 )
-            printf( "Setting K = 2 for uniqueness constaints to work.\n" );
+            printf( "Setting K = 2 for uniqueness constraints to work.\n" );
         pPars->nFramesK = 2;
     }
     if ( pPars->fLatchCorrOpt )
     {
         pPars->fLatchCorr = 1;
-        pPars->nFramesAddSim = 0;
     }
     else
     {
@@ -259,7 +276,12 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
         // perform one round of seq simulation and generate candidate equivalence classes
         p->ppClasses = Ssw_ClassesPrepare( pAig, pPars->fLatchCorr, pPars->nMaxLevs, pPars->fVerbose );
 //        p->ppClasses = Ssw_ClassesPrepareTargets( pAig );
-        p->pSml = Ssw_SmlStart( pAig, 0, p->nFrames + p->pPars->nFramesAddSim, 1 );
+        if ( pPars->fLatchCorrOpt )
+            p->pSml = Ssw_SmlStart( pAig, 0, 2, 1 );
+        else if ( pPars->fDynamic )
+            p->pSml = Ssw_SmlStart( pAig, 0, p->nFrames + p->pPars->nFramesAddSim, 1 );
+        else
+            p->pSml = Ssw_SmlStart( pAig, 0, 1 + p->pPars->nFramesAddSim, 1 );
         Ssw_ClassesSetData( p->ppClasses, p->pSml, Ssw_SmlObjHashWord, Ssw_SmlObjIsConstWord, Ssw_SmlObjsAreEqualWord );
     }
     else
@@ -271,7 +293,7 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
     // perform refinement of classes
     pAigNew = Ssw_SignalCorrespondenceRefine( p );    
     if ( pPars->fUniqueness )
-        printf( "Uniqueness constaint = %3d. Prevented counter-examples = %3d.\n", 
+        printf( "Uniqueness constraints = %3d. Prevented counter-examples = %3d.\n", 
             p->nUniquesAdded, p->nUniquesUseful );
     // cleanup
     Ssw_ManStop( p );
diff --git a/src/aig/ssw/sswDyn.c b/src/aig/ssw/sswDyn.c
new file mode 100644
index 00000000..d5559408
--- /dev/null
+++ b/src/aig/ssw/sswDyn.c
@@ -0,0 +1,384 @@
+/**CFile****************************************************************
+
+  FileName    [sswDyn.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Inductive prover with constraints.]
+
+  Synopsis    [Dynamic loading of constraints.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - September 1, 2008.]
+
+  Revision    [$Id: sswDyn.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "sswInt.h"
+#include "bar.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Label PIs nodes of the frames corresponding to PIs of AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_ManLabelPiNodes( Ssw_Man_t * p )
+{
+    Aig_Obj_t * pObj, * pObjFrames;
+    int f, i;
+    Aig_ManConst1( p->pFrames )->fMarkA = 1;
+    Aig_ManConst1( p->pFrames )->fMarkB = 1;
+    for ( f = 0; f < p->nFrames; f++ )
+    {
+        Saig_ManForEachPi( p->pAig, pObj, i )
+        {
+            pObjFrames = Ssw_ObjFrame( p, pObj, f );
+            assert( Aig_ObjIsPi(pObjFrames) );
+            assert( pObjFrames->fMarkB == 0 );
+            pObjFrames->fMarkA = 1;
+            pObjFrames->fMarkB = 1;
+        }
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects new POs in p->vNewPos.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_ManCollectPis_rec( Aig_Obj_t * pObj, Vec_Ptr_t * vNewPis )
+{
+    assert( !Aig_IsComplement(pObj) );
+    if ( pObj->fMarkA )
+        return;
+    pObj->fMarkA = 1;
+    if ( Aig_ObjIsPi(pObj) )
+    {
+        Vec_PtrPush( vNewPis, pObj );
+        return;
+    }
+    assert( Aig_ObjIsNode(pObj) );
+    Ssw_ManCollectPis_rec( Aig_ObjFanin0(pObj), vNewPis );
+    Ssw_ManCollectPis_rec( Aig_ObjFanin1(pObj), vNewPis );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects new POs in p->vNewPos.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_ManCollectPos_rec( Ssw_Man_t * p, Aig_Obj_t * pObj, Vec_Int_t * vNewPos )
+{
+    Aig_Obj_t * pFanout;
+    int iFanout = -1, i;
+    assert( !Aig_IsComplement(pObj) );
+    if ( pObj->fMarkB )
+        return;
+    pObj->fMarkB = 1;
+    if ( pObj->Id > p->nSRMiterMaxId )
+        return;
+    if ( Aig_ObjIsPo(pObj) )
+    {
+        // skip if it is a register input PO
+        if ( Aig_ObjPioNum(pObj) >= Aig_ManPoNum(p->pFrames)-Aig_ManRegNum(p->pAig) )
+            return;
+        // add the number of this constraint
+        Vec_IntPush( vNewPos, Aig_ObjPioNum(pObj)/2 );
+        return;
+    }
+    // visit the fanouts
+    assert( p->pFrames->pFanData != NULL );
+    Aig_ObjForEachFanout( p->pFrames, pObj, pFanout, iFanout, i )
+        Ssw_ManCollectPos_rec( p, pFanout, vNewPos );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Loads logic cones and relevant constraints.]
+
+  Description [Both pRepr and pObj are objects of the AIG. 
+  The result is the current SAT solver loaded with the logic cones
+  for pRepr and pObj corresponding to them in the frames, 
+  as well as all the relevant constraints.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_ManLoadSolver( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj )
+{
+    Aig_Obj_t * pObjFrames, * pReprFrames;
+    Aig_Obj_t * pTemp, * pObj0, * pObj1;
+    int i, iConstr, RetValue;
+
+    assert( pRepr != pObj );
+    // get the corresponding frames nodes
+    pReprFrames = Aig_Regular( Ssw_ObjFrame( p, pRepr, p->pPars->nFramesK ) );
+    pObjFrames  = Aig_Regular( Ssw_ObjFrame( p, pObj,  p->pPars->nFramesK ) );
+    assert( pReprFrames != pObjFrames );
+ /*
+    // compute the AIG support 
+    Vec_PtrClear( p->vNewLos );
+    Ssw_ManCollectPis_rec( pRepr, p->vNewLos );
+    Ssw_ManCollectPis_rec( pObj,  p->vNewLos );
+    // add logic cones for register outputs
+    Vec_PtrForEachEntry( p->vNewLos, pTemp, i )
+    {
+        pObj0 = Aig_Regular( Ssw_ObjFrame( p, pTemp, p->pPars->nFramesK ) );
+        Ssw_CnfNodeAddToSolver( p->pMSat, pObj0 );
+    }
+*/
+    // add cones for the nodes
+    Ssw_CnfNodeAddToSolver( p->pMSat, pReprFrames );
+    Ssw_CnfNodeAddToSolver( p->pMSat, pObjFrames );
+
+    // compute the frames support 
+    Vec_PtrClear( p->vNewLos );
+    Ssw_ManCollectPis_rec( pReprFrames, p->vNewLos );
+    Ssw_ManCollectPis_rec( pObjFrames,  p->vNewLos );
+    // these nodes include both nodes corresponding to PIs and LOs
+    // (the nodes corresponding to PIs should be labeled with fMarkB!)
+
+    // collect the related constraint POs
+    Vec_IntClear( p->vNewPos );
+    Vec_PtrForEachEntry( p->vNewLos, pTemp, i )
+        Ssw_ManCollectPos_rec( p, pTemp, p->vNewPos );
+    // check if the corresponding pairs are added
+    Vec_IntForEachEntry( p->vNewPos, iConstr, i )
+    {
+        pObj0 = Aig_ManPo( p->pFrames, 2*iConstr   );
+        pObj1 = Aig_ManPo( p->pFrames, 2*iConstr+1 );
+//        if ( pObj0->fMarkB && pObj1->fMarkB )
+        if ( pObj0->fMarkB || pObj1->fMarkB )
+        {
+            pObj0->fMarkB = 1;
+            pObj1->fMarkB = 1;
+            Ssw_NodesAreConstrained( p, Aig_ObjChild0(pObj0), Aig_ObjChild0(pObj1) );
+        }
+    }
+    if ( p->pMSat->pSat->qtail != p->pMSat->pSat->qhead )
+    {
+        RetValue = sat_solver_simplify(p->pMSat->pSat);
+        assert( RetValue != 0 );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Tranfers simulation information from FRAIG to AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_ManSweepTransferDyn( Ssw_Man_t * p )
+{
+    Aig_Obj_t * pObj, * pObjFraig;
+    unsigned * pInfo;
+    int i, f, nFrames;
+
+    // transfer simulation information
+    Aig_ManForEachPi( p->pAig, pObj, i )
+    {
+        pObjFraig = Ssw_ObjFrame( p, pObj, 0 );
+        if ( pObjFraig == Aig_ManConst0(p->pFrames) )
+        {
+            Ssw_SmlObjAssignConst( p->pSml, pObj, 0, 0 );
+            continue;
+        }
+        assert( !Aig_IsComplement(pObjFraig) );
+        assert( Aig_ObjIsPi(pObjFraig) );
+        pInfo = Vec_PtrEntry( p->vSimInfo, Aig_ObjPioNum(pObjFraig) );
+        Ssw_SmlObjSetWord( p->pSml, pObj, pInfo[0], 0, 0 );
+    }
+    // set random simulation info for the second frame
+    for ( f = 1; f < p->nFrames; f++ )
+    {
+        Saig_ManForEachPi( p->pAig, pObj, i )
+        {
+            pObjFraig = Ssw_ObjFrame( p, pObj, f );
+            assert( !Aig_IsComplement(pObjFraig) );
+            assert( Aig_ObjIsPi(pObjFraig) );
+            pInfo = Vec_PtrEntry( p->vSimInfo, Aig_ObjPioNum(pObjFraig) );
+            Ssw_SmlObjSetWord( p->pSml, pObj, pInfo[0], 0, f );
+        }
+    }
+    // create random info
+    nFrames = Ssw_SmlNumFrames( p->pSml );
+    for ( ; f < nFrames; f++ )
+    {
+        Saig_ManForEachPi( p->pAig, pObj, i )
+            Ssw_SmlAssignRandomFrame( p->pSml, pObj, f );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs one round of simulation with counter-examples.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ssw_ManSweepResimulateDyn( Ssw_Man_t * p, int f )
+{
+    int RetValue1, RetValue2, clk = clock();
+    // transfer PI simulation information from storage
+//    Ssw_SmlAssignDist1Plus( p->pSml, p->pPatWords );
+    Ssw_ManSweepTransferDyn( p );
+    // simulate internal nodes
+//    Ssw_SmlSimulateOneFrame( p->pSml );
+    Ssw_SmlSimulateOne( p->pSml );
+    // check equivalence classes
+    RetValue1 = Ssw_ClassesRefineConst1( p->ppClasses, 1 );
+    RetValue2 = Ssw_ClassesRefine( p->ppClasses, 1 );
+    // prepare simulation info for the next round
+    Vec_PtrCleanSimInfo( p->vSimInfo, 0, 1 );
+    p->nPatterns = 0;
+    p->nSimRounds++;
+p->timeSimSat += clock() - clk;
+    return RetValue1 > 0 || RetValue2 > 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs fraiging for the internal nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ssw_ManSweepDyn( Ssw_Man_t * p )
+{ 
+    Bar_Progress_t * pProgress = NULL;
+    Aig_Obj_t * pObj, * pObjNew;
+    int clk, i, f;
+
+    // perform speculative reduction
+clk = clock();
+    // create timeframes
+    p->pFrames = Ssw_FramesWithClasses( p );
+    Aig_ManFanoutStart( p->pFrames );
+    p->nSRMiterMaxId = Aig_ManObjNumMax( p->pFrames );
+
+    // map constants and PIs of the last frame
+    f = p->pPars->nFramesK;
+    Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
+    Saig_ManForEachPi( p->pAig, pObj, i )
+        Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreatePi(p->pFrames) );
+    Aig_ManSetPioNumbers( p->pFrames );
+    // label nodes corresponding to primary inputs
+    Ssw_ManLabelPiNodes( p );
+p->timeReduce += clock() - clk;
+
+    // prepare simulation info
+    assert( p->vSimInfo == NULL );
+    p->vSimInfo = Vec_PtrAllocSimInfo( Aig_ManPiNum(p->pFrames), 1 );
+    Vec_PtrCleanSimInfo( p->vSimInfo, 0, 1 );
+
+    // sweep internal nodes
+    p->fRefined = 0;
+    Ssw_ClassesClearRefined( p->ppClasses );
+    if ( p->pPars->fVerbose )
+        pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) );
+    Aig_ManForEachObj( p->pAig, pObj, i )
+    {
+        if ( p->pPars->fVerbose )
+            Bar_ProgressUpdate( pProgress, i, NULL );
+        if ( Saig_ObjIsLo(p->pAig, pObj) )
+            p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0 );
+        else if ( Aig_ObjIsNode(pObj) )
+        { 
+            pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
+            Ssw_ObjSetFrame( p, pObj, f, pObjNew );
+            p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0 );
+        }
+        // check if it is time to recycle the solver
+        if ( p->pMSat->pSat == NULL || 
+            (p->pPars->nSatVarMax2 && 
+             p->pMSat->nSatVars > p->pPars->nSatVarMax2 && 
+             p->nRecycleCalls > p->pPars->nRecycleCalls2) )
+        {
+            // resimulate
+            if ( p->nPatterns > 0 )
+                Ssw_ManSweepResimulateDyn( p, f );
+//                printf( "Recycling SAT solver with %d vars and %d calls.\n", 
+//                    p->pMSat->nSatVars, p->nRecycleCalls );
+//            Aig_ManCleanMarkAB( p->pAig );
+            Aig_ManCleanMarkAB( p->pFrames );
+            // label nodes corresponding to primary inputs
+            Ssw_ManLabelPiNodes( p );
+            // replace the solver
+            if ( p->pMSat )
+            {
+                p->nVarsMax  = AIG_MAX( p->nVarsMax,  p->pMSat->nSatVars );
+                p->nCallsMax = AIG_MAX( p->nCallsMax, p->pMSat->nSolverCalls );
+                Ssw_SatStop( p->pMSat );
+                p->nRecycles++;
+                p->nRecyclesTotal++;
+                p->nRecycleCalls = 0;
+            }
+            p->pMSat = Ssw_SatStart( 0 );
+            assert( p->nPatterns == 0 );
+        }
+        // resimulate
+        if ( p->nPatterns == 32 )
+            Ssw_ManSweepResimulateDyn( p, f );
+    }
+    // resimulate
+    if ( p->nPatterns > 0 )
+        Ssw_ManSweepResimulateDyn( p, f );
+    // collect stats
+    if ( p->pPars->fVerbose )
+        Bar_ProgressStop( pProgress );
+
+    // cleanup
+//    Ssw_ClassesCheck( p->ppClasses );
+    return p->fRefined;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/ssw/sswInt.h b/src/aig/ssw/sswInt.h
index 0a3f7e21..8d8d3265 100644
--- a/src/aig/ssw/sswInt.h
+++ b/src/aig/ssw/sswInt.h
@@ -72,14 +72,20 @@ struct Ssw_Man_t_
     int              nCallsUnsat;    // the number of UNSAT calls in this round
     int              nRecycleCalls;  // the number of calls since last recycling
     int              nRecycles;      // the number of time SAT solver was recycled
-    int              nConeMax;       // the maximum cone size
+    int              nRecyclesTotal; // the number of time SAT solver was recycled
+    int              nVarsMax;       // the maximum variables in the solver
+    int              nCallsMax;      // the maximum number of SAT calls
     // uniqueness
     Vec_Ptr_t *      vCommon;        // the set of common variables in the logic cones
-    int              iOutputLit;     // the output literal of the uniqueness constaint
+    int              iOutputLit;     // the output literal of the uniqueness constraint
     Vec_Int_t *      vDiffPairs;     // is set to 1 if reg pair can be diff
-    int              nUniques;       // the number of uniqueness constaints used 
+    int              nUniques;       // the number of uniqueness constraints used 
     int              nUniquesAdded;  // useful uniqueness constraints
     int              nUniquesUseful; // useful uniqueness constraints
+    // dynamic constraint addition
+    int              nSRMiterMaxId;  // max ID after which the last frame begins
+    Vec_Ptr_t *      vNewLos;        // new time frame LOs of to constrain
+    Vec_Int_t *      vNewPos;        // new time frame POs of to add constraints
     // sequential simulator
     Ssw_Sml_t *      pSml;
     // counter example storage
@@ -93,7 +99,6 @@ struct Ssw_Man_t_
     int              nSatCalls;      // the number of SAT calls
     int              nSatProof;      // the number of proofs
     int              nSatFailsReal;  // the number of timeouts
-    int              nSatFailsTotal; // the number of timeouts
     int              nSatCallsUnsat; // the number of unsat SAT calls
     int              nSatCallsSat;   // the number of sat SAT calls
     // node/register/lit statistics
@@ -124,9 +129,9 @@ struct Ssw_Sat_t_
     sat_solver *     pSat;           // recyclable SAT solver
     int              nSatVars;       // the counter of SAT variables
     Vec_Int_t *      vSatVars;       // mapping of each node into its SAT var
-    int              nSatVarsTotal;  // the total number of SAT vars created
     Vec_Ptr_t *      vFanins;        // fanins of the CNF node
     Vec_Ptr_t *      vUsedPis;       // the PIs with SAT variables 
+    int              nSolverCalls;   // the total number of SAT calls
 };
 
 // internal frames manager
@@ -211,6 +216,9 @@ extern void          Ssw_CnfNodeAddToSolver( Ssw_Sat_t * p, Aig_Obj_t * pObj );
 extern int           Ssw_CnfGetNodeValue( Ssw_Sat_t * p, Aig_Obj_t * pObjFraig );
 /*=== sswCore.c ===================================================*/
 extern Aig_Man_t *   Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p );
+/*=== sswDyn.c ===================================================*/
+extern void          Ssw_ManLoadSolver( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj );
+extern int           Ssw_ManSweepDyn( Ssw_Man_t * p );
 /*=== sswLcorr.c ==========================================================*/
 extern int           Ssw_ManSweepLatch( Ssw_Man_t * p );
 /*=== sswMan.c ===================================================*/
@@ -229,15 +237,18 @@ extern int           Ssw_SmlObjIsConstWord( Ssw_Sml_t * p, Aig_Obj_t * pObj );
 extern int           Ssw_SmlObjsAreEqualWord( Ssw_Sml_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );
 extern int           Ssw_SmlObjIsConstBit( void * p, Aig_Obj_t * pObj );
 extern int           Ssw_SmlObjsAreEqualBit( void * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );
+extern void          Ssw_SmlAssignRandomFrame( Ssw_Sml_t * p, Aig_Obj_t * pObj, int iFrame );
 extern Ssw_Sml_t *   Ssw_SmlStart( Aig_Man_t * pAig, int nPref, int nFrames, int nWordsFrame );
 extern void          Ssw_SmlClean( Ssw_Sml_t * p );
 extern void          Ssw_SmlStop( Ssw_Sml_t * p );
+extern int           Ssw_SmlNumFrames( Ssw_Sml_t * p );
 extern void          Ssw_SmlObjAssignConst( Ssw_Sml_t * p, Aig_Obj_t * pObj, int fConst1, int iFrame );
 extern void          Ssw_SmlObjSetWord( Ssw_Sml_t * p, Aig_Obj_t * pObj, unsigned Word, int iWord, int iFrame );
 extern void          Ssw_SmlAssignDist1Plus( Ssw_Sml_t * p, unsigned * pPat );
 extern void          Ssw_SmlSimulateOne( Ssw_Sml_t * p );
 extern void          Ssw_SmlSimulateOneFrame( Ssw_Sml_t * p );
 extern Ssw_Sml_t *   Ssw_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nWords );
+extern void          Ssw_SmlResimulateSeq( Ssw_Sml_t * p );
 /*=== sswSimSat.c ===================================================*/
 extern void          Ssw_ManResimulateBit( Ssw_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr );
 extern void          Ssw_ManResimulateWord( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr, int f );
@@ -248,7 +259,7 @@ extern int           Ssw_ManSweepBmc( Ssw_Man_t * p );
 extern int           Ssw_ManSweep( Ssw_Man_t * p );
 /*=== sswUnique.c ===================================================*/
 extern void          Ssw_UniqueRegisterPairInfo( Ssw_Man_t * p );
-extern int           Ssw_ManUniqueOne( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj );
+extern int           Ssw_ManUniqueOne( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj, int fVerbose );
 extern int           Ssw_ManUniqueAddConstraint( Ssw_Man_t * p, Vec_Ptr_t * vCommon, int f1, int f2 );
 
 #ifdef __cplusplus
diff --git a/src/aig/ssw/sswLcorr.c b/src/aig/ssw/sswLcorr.c
index d374c5f6..8cb8b81b 100644
--- a/src/aig/ssw/sswLcorr.c
+++ b/src/aig/ssw/sswLcorr.c
@@ -300,6 +300,8 @@ int Ssw_ManSweepLatch( Ssw_Man_t * p )
              p->pMSat->nSatVars > p->pPars->nSatVarMax &&
              p->nRecycleCalls > p->pPars->nRecycleCalls )
         {
+            p->nVarsMax  = AIG_MAX( p->nVarsMax,  p->pMSat->nSatVars );
+            p->nCallsMax = AIG_MAX( p->nCallsMax, p->pMSat->nSolverCalls );
             Ssw_SatStop( p->pMSat );
             p->pMSat = Ssw_SatStart( 0 );
             p->nRecycles++;
@@ -311,7 +313,6 @@ int Ssw_ManSweepLatch( Ssw_Man_t * p )
         Ssw_ManSweepResimulate( p );
     // cleanup
     Vec_PtrFree( vClass );
-    p->nSatFailsTotal += p->nSatFailsReal;
 //    if ( p->pPars->fVerbose )
 //        Bar_ProgressStop( pProgress );
 
diff --git a/src/aig/ssw/sswMan.c b/src/aig/ssw/sswMan.c
index 1b29037c..91f6e713 100644
--- a/src/aig/ssw/sswMan.c
+++ b/src/aig/ssw/sswMan.c
@@ -58,6 +58,9 @@ Ssw_Man_t * Ssw_ManCreate( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
     // allocate storage for sim pattern
     p->nPatWords     = Aig_BitWordNum( Saig_ManPiNum(pAig) * p->nFrames + Saig_ManRegNum(pAig) );
     p->pPatWords     = ALLOC( unsigned, p->nPatWords ); 
+    // other
+    p->vNewLos       = Vec_PtrAlloc( 100 );
+    p->vNewPos       = Vec_IntAlloc( 100 );
     return p;
 }
 
@@ -101,10 +104,10 @@ void Ssw_ManPrintStats( Ssw_Man_t * p )
     printf( "AIG       : PI = %d. PO = %d. Latch = %d. Node = %d.  Ave SAT vars = %d.\n", 
         Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), Saig_ManRegNum(p->pAig), Aig_ManNodeNum(p->pAig), 
         0/p->pPars->nIters );
-    printf( "SAT calls : Proof = %d. Cex = %d. Fail = %d. Equivs = %d. Str = %d.\n", 
-        p->nSatProof, p->nSatCallsSat, p->nSatFailsTotal, Ssw_ManCountEquivs(p), p->nStrangers );
-    printf( "SAT solver: Vars = %d. Max cone = %d. Recycles = %d. Rounds = %d.\n", 
-        0, p->nConeMax, p->nRecycles, p->nSimRounds );
+    printf( "SAT calls : Proof = %d. Cex = %d. Fail = %d. Lits proved = %d.\n", 
+        p->nSatProof, p->nSatCallsSat, p->nSatFailsReal, Ssw_ManCountEquivs(p) );
+    printf( "SAT solver: Vars max = %d. Calls max = %d. Recycles = %d. Sim rounds = %d.\n", 
+        p->nVarsMax, p->nCallsMax, p->nRecyclesTotal, p->nSimRounds );
     printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%).  RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n", 
         p->nNodesBeg, p->nNodesEnd, 100.0*(p->nNodesBeg-p->nNodesEnd)/(p->nNodesBeg?p->nNodesBeg:1), 
         p->nRegsBeg, p->nRegsEnd, 100.0*(p->nRegsBeg-p->nRegsEnd)/(p->nRegsBeg?p->nRegsBeg:1) );
@@ -135,10 +138,11 @@ void Ssw_ManPrintStats( Ssw_Man_t * p )
 ***********************************************************************/
 void Ssw_ManCleanup( Ssw_Man_t * p )
 {
+//    Aig_ManCleanMarkAB( p->pAig );
     assert( p->pMSat == NULL );
     if ( p->pFrames )
     {
-        Aig_ManCleanMarkA( p->pFrames );
+        Aig_ManCleanMarkAB( p->pFrames );
         Aig_ManStop( p->pFrames );
         p->pFrames = NULL;
         memset( p->pNodeToFrames, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p->pAig) * p->nFrames );
@@ -165,8 +169,6 @@ void Ssw_ManCleanup( Ssw_Man_t * p )
 ***********************************************************************/
 void Ssw_ManStop( Ssw_Man_t * p )
 {
-    Aig_ManCleanMarkA( p->pAig );
-    Aig_ManCleanMarkB( p->pAig );
     if ( p->pPars->fVerbose )
         Ssw_ManPrintStats( p );
     if ( p->ppClasses )
@@ -175,6 +177,8 @@ void Ssw_ManStop( Ssw_Man_t * p )
         Ssw_SmlStop( p->pSml );
     if ( p->vDiffPairs )
         Vec_IntFree( p->vDiffPairs );
+    Vec_PtrFree( p->vNewLos );
+    Vec_IntFree( p->vNewPos );
     Vec_PtrFree( p->vCommon );
     FREE( p->pNodeToFrames );
     FREE( p->pPatWords );
diff --git a/src/aig/ssw/sswSat.c b/src/aig/ssw/sswSat.c
index fc902560..2fd0fba3 100644
--- a/src/aig/ssw/sswSat.c
+++ b/src/aig/ssw/sswSat.c
@@ -44,6 +44,7 @@ int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
     int nBTLimit = p->pPars->nBTLimit;
     int pLits[3], nLits, RetValue, RetValue1, clk;//, status;
     p->nSatCalls++;
+    p->pMSat->nSolverCalls++;
 
     // sanity checks
     assert( !Aig_IsComplement(pOld) );
@@ -231,7 +232,7 @@ int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
     // consider the constant 1 case
     if ( pOld == Aig_ManConst1(p->pFrames) )
     {
-        // add constaint A = 1  ---->  A
+        // add constraint A = 1  ---->  A
         pLits[0] = toLitCond( Ssw_ObjSatNum(p->pMSat,pNew), fComplNew );
         if ( p->pPars->fPolarFlip )
         {
@@ -242,7 +243,7 @@ int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
     }
     else
     {
-        // add constaint A = B  ---->  (A v !B)(!A v B)
+        // add constraint A = B  ---->  (A v !B)(!A v B)
 
         // (A v !B)
         pLits[0] = toLitCond( Ssw_ObjSatNum(p->pMSat,pOld), 0 );
diff --git a/src/aig/ssw/sswSemi.c b/src/aig/ssw/sswSemi.c
index b445c2c4..572ab076 100644
--- a/src/aig/ssw/sswSemi.c
+++ b/src/aig/ssw/sswSemi.c
@@ -267,7 +267,7 @@ int Ssw_FilterUsingSemi( Ssw_Man_t * pMan, int fCheckTargets, int nConfMax, int
     }
     if ( fVerbose )
     {
-        printf( "AIG : Const = %6d. Cl = %6d. Nodes = %6d.  ConfMax = %6d. FramesMax = %6d.\n", 
+        printf( "AIG : C = %6d. Cl = %6d. Nodes = %6d.  ConfMax = %6d. FramesMax = %6d.\n", 
             Ssw_ClassesCand1Num(p->pMan->ppClasses), Ssw_ClassesClassNum(p->pMan->ppClasses), 
             Aig_ManNodeNum(p->pMan->pAig), p->nConfMax, p->nFramesSweep );
     } 
@@ -279,7 +279,7 @@ clk = clock();
         Frames = Ssw_ManFilterBmc( p, Iter, fCheckTargets );
         if ( fVerbose )
         {
-            printf( "%3d : Const = %6d. Cl = %6d. NR = %6d. F = %3d. C = %5d. P = %3d. %s ", 
+            printf( "%3d : C = %6d. Cl = %6d. NR = %6d. F = %3d. C = %5d. P = %3d. %s ", 
                 Iter, Ssw_ClassesCand1Num(p->pMan->ppClasses), Ssw_ClassesClassNum(p->pMan->ppClasses), 
                 Aig_ManNodeNum(p->pMan->pFrames), Frames, (int)p->pMan->pMSat->pSat->stats.conflicts, p->nPatterns, 
                 p->pMan->nSatFailsReal? "f" : " " );
@@ -300,7 +300,6 @@ clk = clock();
     pMan->nSatCalls = 0;
     pMan->nSatProof = 0;
     pMan->nSatFailsReal = 0; 
-    pMan->nSatFailsTotal = 0;
     pMan->nSatCallsUnsat = 0;
     pMan->nSatCallsSat = 0;  
     pMan->timeSimSat = 0;    
diff --git a/src/aig/ssw/sswSim.c b/src/aig/ssw/sswSim.c
index b80c3710..ce6ca38c 100644
--- a/src/aig/ssw/sswSim.c
+++ b/src/aig/ssw/sswSim.c
@@ -359,11 +359,15 @@ int * Ssw_SmlCheckOutput( Ssw_Sml_t * p )
 void Ssw_SmlAssignRandom( Ssw_Sml_t * p, Aig_Obj_t * pObj )
 {
     unsigned * pSims;
-    int i;
+    int i, f;
     assert( Aig_ObjIsPi(pObj) );
     pSims = Ssw_ObjSim( p, pObj->Id );
     for ( i = 0; i < p->nWordsTotal; i++ )
         pSims[i] = Ssw_ObjRandomSim();
+    // set the first bit 0 in each frame
+    assert( p->nWordsFrame * p->nFrames == p->nWordsTotal );
+    for ( f = 0; f < p->nFrames; f++ )
+        pSims[p->nWordsFrame*f] <<= 1;
 }
 
 /**Function*************************************************************
@@ -381,6 +385,7 @@ void Ssw_SmlAssignRandomFrame( Ssw_Sml_t * p, Aig_Obj_t * pObj, int iFrame )
 {
     unsigned * pSims;
     int i;
+    assert( iFrame < p->nFrames );
     assert( Aig_ObjIsPi(pObj) );
     pSims = Ssw_ObjSim( p, pObj->Id ) + p->nWordsFrame * iFrame;
     for ( i = 0; i < p->nWordsFrame; i++ )
@@ -402,6 +407,7 @@ void Ssw_SmlObjAssignConst( Ssw_Sml_t * p, Aig_Obj_t * pObj, int fConst1, int iF
 {
     unsigned * pSims;
     int i;
+    assert( iFrame < p->nFrames );
     assert( Aig_ObjIsPi(pObj) );
     pSims = Ssw_ObjSim( p, pObj->Id ) + p->nWordsFrame * iFrame;
     for ( i = 0; i < p->nWordsFrame; i++ )
@@ -422,6 +428,7 @@ void Ssw_SmlObjAssignConst( Ssw_Sml_t * p, Aig_Obj_t * pObj, int fConst1, int iF
 void Ssw_SmlObjSetWord( Ssw_Sml_t * p, Aig_Obj_t * pObj, unsigned Word, int iWord, int iFrame )
 {
     unsigned * pSims;
+    assert( iFrame < p->nFrames );
     assert( Aig_ObjIsPi(pObj) );
     pSims = Ssw_ObjSim( p, pObj->Id ) + p->nWordsFrame * iFrame;
     pSims[iWord] = Word;
@@ -429,39 +436,6 @@ void Ssw_SmlObjSetWord( Ssw_Sml_t * p, Aig_Obj_t * pObj, unsigned Word, int iWor
 
 /**Function*************************************************************
 
-  Synopsis    [Assings random simulation info for the PIs.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Ssw_SmlInitialize( Ssw_Sml_t * p, int fInit )
-{
-    Aig_Obj_t * pObj;
-    int i;
-    if ( fInit )
-    {
-        assert( Aig_ManRegNum(p->pAig) > 0 );
-        assert( Aig_ManRegNum(p->pAig) < Aig_ManPiNum(p->pAig) );
-        // assign random info for primary inputs
-        Saig_ManForEachPi( p->pAig, pObj, i )
-            Ssw_SmlAssignRandom( p, pObj );
-        // assign the initial state for the latches
-        Saig_ManForEachLo( p->pAig, pObj, i )
-            Ssw_SmlObjAssignConst( p, pObj, 0, 0 );
-    }
-    else
-    {
-        Aig_ManForEachPi( p->pAig, pObj, i )
-            Ssw_SmlAssignRandom( p, pObj );
-    }
-}
-
-/**Function*************************************************************
-
   Synopsis    [Assings distance-1 simulation info for the PIs.]
 
   Description []
@@ -558,6 +532,7 @@ void Ssw_SmlNodeSimulate( Ssw_Sml_t * p, Aig_Obj_t * pObj, int iFrame )
 {
     unsigned * pSims, * pSims0, * pSims1;
     int fCompl, fCompl0, fCompl1, i;
+    assert( iFrame < p->nFrames );
     assert( !Aig_IsComplement(pObj) );
     assert( Aig_ObjIsNode(pObj) );
     assert( iFrame == 0 || p->nWordsFrame < p->nWordsTotal );
@@ -623,6 +598,8 @@ int Ssw_SmlNodesCompareInFrame( Ssw_Sml_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pO
 {
     unsigned * pSims0, * pSims1;
     int i;
+    assert( iFrame0 < p->nFrames );
+    assert( iFrame1 < p->nFrames );
     assert( !Aig_IsComplement(pObj0) );
     assert( !Aig_IsComplement(pObj1) );
     assert( iFrame0 == 0 || p->nWordsFrame < p->nWordsTotal );
@@ -652,6 +629,7 @@ void Ssw_SmlNodeCopyFanin( Ssw_Sml_t * p, Aig_Obj_t * pObj, int iFrame )
 {
     unsigned * pSims, * pSims0;
     int fCompl, fCompl0, i;
+    assert( iFrame < p->nFrames );
     assert( !Aig_IsComplement(pObj) );
     assert( Aig_ObjIsPo(pObj) );
     assert( iFrame == 0 || p->nWordsFrame < p->nWordsTotal );
@@ -685,6 +663,7 @@ void Ssw_SmlNodeTransferNext( Ssw_Sml_t * p, Aig_Obj_t * pOut, Aig_Obj_t * pIn,
 {
     unsigned * pSims0, * pSims1;
     int i;
+    assert( iFrame < p->nFrames );
     assert( !Aig_IsComplement(pOut) );
     assert( !Aig_IsComplement(pIn) );
     assert( Aig_ObjIsPo(pOut) );
@@ -698,6 +677,92 @@ void Ssw_SmlNodeTransferNext( Ssw_Sml_t * p, Aig_Obj_t * pOut, Aig_Obj_t * pIn,
         pSims1[i] = pSims0[i];
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Simulates one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_SmlNodeTransferFirst( Ssw_Sml_t * p, Aig_Obj_t * pOut, Aig_Obj_t * pIn )
+{
+    unsigned * pSims0, * pSims1;
+    int i;
+    assert( !Aig_IsComplement(pOut) );
+    assert( !Aig_IsComplement(pIn) );
+    assert( Aig_ObjIsPo(pOut) );
+    assert( Aig_ObjIsPi(pIn) );
+    assert( p->nWordsFrame < p->nWordsTotal );
+    // get hold of the simulation information
+    pSims0 = Ssw_ObjSim(p, pOut->Id) + p->nWordsFrame * (p->nFrames-1);
+    pSims1 = Ssw_ObjSim(p, pIn->Id);
+    // copy information as it is
+    for ( i = 0; i < p->nWordsFrame; i++ )
+        pSims1[i] = pSims0[i];
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Assings random simulation info for the PIs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_SmlInitialize( Ssw_Sml_t * p, int fInit )
+{
+    Aig_Obj_t * pObj;
+    int i;
+    if ( fInit )
+    {
+        assert( Aig_ManRegNum(p->pAig) > 0 );
+        assert( Aig_ManRegNum(p->pAig) < Aig_ManPiNum(p->pAig) );
+        // assign random info for primary inputs
+        Saig_ManForEachPi( p->pAig, pObj, i )
+            Ssw_SmlAssignRandom( p, pObj );
+        // assign the initial state for the latches
+        Saig_ManForEachLo( p->pAig, pObj, i )
+            Ssw_SmlObjAssignConst( p, pObj, 0, 0 );
+    }
+    else
+    {
+        Aig_ManForEachPi( p->pAig, pObj, i )
+            Ssw_SmlAssignRandom( p, pObj );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Assings random simulation info for the PIs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_SmlReinitialize( Ssw_Sml_t * p )
+{
+    Aig_Obj_t * pObj, * pObjLi, * pObjLo;
+    int i;
+    assert( Aig_ManRegNum(p->pAig) > 0 );
+    assert( Aig_ManRegNum(p->pAig) < Aig_ManPiNum(p->pAig) );
+    // assign random info for primary inputs
+    Saig_ManForEachPi( p->pAig, pObj, i )
+        Ssw_SmlAssignRandom( p, pObj );
+    // copy simulation info into the inputs
+    Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
+        Ssw_SmlNodeTransferFirst( p, pObjLi, pObjLo );
+}
 
 /**Function*************************************************************
 
@@ -744,12 +809,12 @@ clk = clock();
         // copy simulation info into outputs
         Saig_ManForEachPo( p->pAig, pObj, i )
             Ssw_SmlNodeCopyFanin( p, pObj, f );
-        // quit if this is the last timeframe
-        if ( f == p->nFrames - 1 )
-            break;
         // copy simulation info into outputs
         Saig_ManForEachLi( p->pAig, pObj, i )
             Ssw_SmlNodeCopyFanin( p, pObj, f );
+        // quit if this is the last timeframe
+        if ( f == p->nFrames - 1 )
+            break;
         // copy simulation info into the inputs
         Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
             Ssw_SmlNodeTransferNext( p, pObjLi, pObjLo, f );
@@ -845,6 +910,22 @@ void Ssw_SmlStop( Ssw_Sml_t * p )
     free( p );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Deallocates simulation manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ssw_SmlNumFrames( Ssw_Sml_t * p )
+{
+    return p->nFrames;
+}
+
 
 /**Function*************************************************************
 
@@ -887,6 +968,24 @@ Ssw_Sml_t * Ssw_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nW
     return p;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Performs next round of sequential simulation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_SmlResimulateSeq( Ssw_Sml_t * p )
+{
+    Ssw_SmlReinitialize( p );
+    Ssw_SmlSimulateOne( p );
+    p->fNonConstOut = Ssw_SmlCheckNonConstOutputs( p );
+}
+
 
 
 /**Function*************************************************************
diff --git a/src/aig/ssw/sswSweep.c b/src/aig/ssw/sswSweep.c
index 36e8bab3..a2f3c175 100644
--- a/src/aig/ssw/sswSweep.c
+++ b/src/aig/ssw/sswSweep.c
@@ -69,6 +69,37 @@ int Ssw_ManGetSatVarValue( Ssw_Man_t * p, Aig_Obj_t * pObj, int f )
 
 /**Function*************************************************************
 
+  Synopsis    [Performs fraiging for the internal nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_CheckConstraints( Ssw_Man_t * p )
+{
+    Aig_Obj_t * pObj, * pObj2;
+    int nConstrPairs, i;
+    int Counter = 0;
+    nConstrPairs = Aig_ManPoNum(p->pFrames)-Aig_ManRegNum(p->pAig);
+    assert( (nConstrPairs & 1) == 0 );
+    for ( i = 0; i < nConstrPairs; i += 2 )
+    {
+        pObj  = Aig_ManPo( p->pFrames, i   );
+        pObj2 = Aig_ManPo( p->pFrames, i+1 );
+        if ( Ssw_NodesAreEquiv( p, Aig_ObjFanin0(pObj), Aig_ObjFanin0(pObj2) ) != 1 )
+        {
+            Ssw_NodesAreConstrained( p, Aig_ObjChild0(pObj), Aig_ObjChild0(pObj2) );
+            Counter++;
+        }
+    }
+    printf( "Total constraints = %d. Added constraints = %d.\n", nConstrPairs/2, Counter );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Copy pattern from the solver into the internal storage.]
 
   Description []
@@ -78,13 +109,13 @@ int Ssw_ManGetSatVarValue( Ssw_Man_t * p, Aig_Obj_t * pObj, int f )
   SeeAlso     []
 
 ***********************************************************************/
-void Ssw_SmlSavePatternAig( Ssw_Man_t * p, int f )
+void Ssw_SmlSavePatternAigPhase( Ssw_Man_t * p, int f )
 {
     Aig_Obj_t * pObj;
     int i;
     memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
     Aig_ManForEachPi( p->pAig, pObj, i )
-        if ( Ssw_ManGetSatVarValue( p, pObj, f ) )
+        if ( Aig_ObjPhaseReal( Ssw_ObjFrame(p, pObj, f) ) )
             Aig_InfoSetBit( p->pPatWords, i );
 }
 
@@ -99,18 +130,48 @@ void Ssw_SmlSavePatternAig( Ssw_Man_t * p, int f )
   SeeAlso     []
 
 ***********************************************************************/
-void Ssw_SmlSavePatternAigPhase( Ssw_Man_t * p, int f )
+void Ssw_SmlSavePatternAig( Ssw_Man_t * p, int f )
 {
     Aig_Obj_t * pObj;
     int i;
     memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
     Aig_ManForEachPi( p->pAig, pObj, i )
-        if ( Aig_ObjPhaseReal( Ssw_ObjFrame(p, pObj, f) ) )
+        if ( Ssw_ManGetSatVarValue( p, pObj, f ) )
             Aig_InfoSetBit( p->pPatWords, i );
 }
 
 /**Function*************************************************************
 
+  Synopsis    [Saves one counter-example into internal storage.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_SmlAddPatternDyn( Ssw_Man_t * p )
+{
+    Aig_Obj_t * pObj;
+    unsigned * pInfo;
+    int i, nVarNum;
+    // iterate through the PIs of the frames
+    Vec_PtrForEachEntry( p->pMSat->vUsedPis, pObj, i )
+    {
+        assert( Aig_ObjIsPi(pObj) );
+        nVarNum = Ssw_ObjSatNum( p->pMSat, pObj );
+        assert( nVarNum > 0 );
+        if ( sat_solver_var_value( p->pMSat->pSat, nVarNum ) )
+        {
+            pInfo = Vec_PtrEntry( p->vSimInfo, Aig_ObjPioNum(pObj) );
+            Aig_InfoSetBit( pInfo, p->nPatterns );
+        }
+    }
+}
+
+/**Function*************************************************************
+
   Synopsis    [Performs fraiging for one node.]
 
   Description [Returns the fraiged node.]
@@ -123,7 +184,7 @@ void Ssw_SmlSavePatternAigPhase( Ssw_Man_t * p, int f )
 int Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc )
 { 
     Aig_Obj_t * pObjRepr, * pObjFraig, * pObjFraig2, * pObjReprFraig;
-    int RetValue;
+    int RetValue, clk;
     // get representative of this class
     pObjRepr = Aig_ObjRepr( p->pAig, pObj );
     if ( pObjRepr == NULL )
@@ -134,48 +195,47 @@ int Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc )
     pObjReprFraig = Ssw_ObjFrame( p, pObjRepr, f );
     // check if constant 0 pattern distinquishes these nodes
     assert( pObjFraig != NULL && pObjReprFraig != NULL );
-    if ( (pObj->fPhase == pObjRepr->fPhase) != (Aig_ObjPhaseReal(pObjFraig) == Aig_ObjPhaseReal(pObjReprFraig)) )
+    assert( (pObj->fPhase == pObjRepr->fPhase) == (Aig_ObjPhaseReal(pObjFraig) == Aig_ObjPhaseReal(pObjReprFraig)) );
+    // if the fraiged nodes are the same, return
+    if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) )
+        return 0; 
+    // add constraints on demand
+    if ( !fBmc && p->pPars->fDynamic )
     {
-        p->nStrangers++;
-        Ssw_SmlSavePatternAigPhase( p, f );
+clk = clock();
+        Ssw_ManLoadSolver( p, pObjRepr, pObj );
+        p->nRecycleCalls++;
+p->timeMarkCones += clock() - clk;
     }
+    // call equivalence checking
+    if ( Aig_Regular(pObjFraig) != Aig_ManConst1(p->pFrames) )
+        RetValue = Ssw_NodesAreEquiv( p, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) );
     else
-    { 
-        // if the fraiged nodes are the same, return
-        if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) )
-            return 0; 
-        // call equivalence checking
-        if ( Aig_Regular(pObjFraig) != Aig_ManConst1(p->pFrames) )
-            RetValue = Ssw_NodesAreEquiv( p, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) );
-        else
-            RetValue = Ssw_NodesAreEquiv( p, Aig_Regular(pObjFraig), Aig_Regular(pObjReprFraig) );
-        if ( RetValue == 1 )  // proved equivalent
-        {
-            pObjFraig2 = Aig_NotCond( pObjReprFraig, pObj->fPhase ^ pObjRepr->fPhase );
-            Ssw_ObjSetFrame( p, pObj, f, pObjFraig2 );
-            return 0;
-        }
-        if ( RetValue == -1 ) // timed out
-        {
-            Ssw_ClassesRemoveNode( p->ppClasses, pObj );
-            return 1;
-        }
-        // disproved the equivalence
-        Ssw_SmlSavePatternAig( p, f );
+        RetValue = Ssw_NodesAreEquiv( p, Aig_Regular(pObjFraig), Aig_Regular(pObjReprFraig) );
+    if ( RetValue == 1 )  // proved equivalent
+    {
+        pObjFraig2 = Aig_NotCond( pObjReprFraig, pObj->fPhase ^ pObjRepr->fPhase );
+        Ssw_ObjSetFrame( p, pObj, f, pObjFraig2 );
+        return 0;
     }
-    if ( !fBmc && p->pPars->fUniqueness && p->pPars->nFramesK > 1 && 
-        Ssw_ManUniqueOne( p, pObjRepr, pObj ) && p->iOutputLit == -1 )
+    if ( RetValue == -1 ) // timed out
+    {
+        Ssw_ClassesRemoveNode( p->ppClasses, pObj );
+        return 1;
+    }
+    // disproved the equivalence
+    if ( !fBmc && p->pPars->fDynamic )
+    {
+        Ssw_SmlAddPatternDyn( p );
+        p->nPatterns++;
+        return 1;
+    }
+    else
+        Ssw_SmlSavePatternAig( p, f );
+    // consider uniqueness
+    if ( !fBmc && !p->pPars->fDynamic && p->pPars->fUniqueness && p->pPars->nFramesK > 1 && 
+        Ssw_ManUniqueOne( p, pObjRepr, pObj, p->pPars->fVerbose ) && p->iOutputLit == -1 )
     {
-/*
-        if ( Ssw_ManUniqueAddConstraint( p, p->vCommon, 0, 1 ) )
-        {
-            int RetValue;
-            assert( p->iOutputLit > -1 );
-            RetValue = Ssw_ManSweepNode( p, pObj, f, 0 );
-            p->iOutputLit = -1;
-            return RetValue;
-        }
-*/
         if ( Ssw_ManUniqueAddConstraint( p, p->vCommon, 0, 1 ) )
         {
             int RetValue2 = Ssw_NodesAreEquiv( p, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) );
@@ -186,7 +246,7 @@ int Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc )
             {
                 int x;
 //                printf( "Second time:\n" );
-                x = Ssw_ManUniqueOne( p, pObjRepr, pObj );
+                x = Ssw_ManUniqueOne( p, pObjRepr, pObj, p->pPars->fVerbose );
                 Ssw_SmlSavePatternAig( p, f );
                 Ssw_ManResimulateWord( p, pObj, pObjRepr, f );
                 if ( Aig_ObjRepr( p->pAig, pObj ) == pObjRepr )
@@ -286,63 +346,17 @@ p->timeBmc += clock() - clk;
   SeeAlso     []
 
 ***********************************************************************/
-void Ssw_CheckConstaints( Ssw_Man_t * p )
-{
-    Aig_Obj_t * pObj, * pObj2;
-    int nConstrPairs, i;
-    int Counter = 0;
-    nConstrPairs = Aig_ManPoNum(p->pFrames)-Aig_ManRegNum(p->pAig);
-    assert( (nConstrPairs & 1) == 0 );
-    for ( i = 0; i < nConstrPairs; i += 2 )
-    {
-        pObj  = Aig_ManPo( p->pFrames, i   );
-        pObj2 = Aig_ManPo( p->pFrames, i+1 );
-        if ( Ssw_NodesAreEquiv( p, Aig_ObjFanin0(pObj), Aig_ObjFanin0(pObj2) ) != 1 )
-        {
-            Ssw_NodesAreConstrained( p, Aig_ObjChild0(pObj), Aig_ObjChild0(pObj2) );
-            Counter++;
-        }
-    }
-    printf( "Total constraints = %d. Added constraints = %d.\n", nConstrPairs/2, Counter );
- }
-
-/**Function*************************************************************
-
-  Synopsis    [Performs fraiging for the internal nodes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
 int Ssw_ManSweep( Ssw_Man_t * p )
 { 
     Bar_Progress_t * pProgress = NULL;
     Aig_Obj_t * pObj, * pObj2, * pObjNew;
-    int nConstrPairs, clk, i, f;
-//    int v; 
+    int nConstrPairs, clk, i, f, v;
 
     // perform speculative reduction
 clk = clock();
     // create timeframes
     p->pFrames = Ssw_FramesWithClasses( p );
-    // add constraints
-//    p->pMSat = Ssw_SatStart( 0 );
-//    Ssw_ManStartSolver( p );
-/*
-    {
-        int clk2 = clock();
-        Ssw_CheckConstaints( p );
-        PRT( "Time", clock() - clk2 );
-    }
-
-    Ssw_ManCleanup( p );
-    p->pFrames = Ssw_FramesWithClasses( p );
-    p->pMSat = Ssw_SatStart( 0 );
-//    Ssw_ManStartSolver( p );
-*/
+    // add constants
     nConstrPairs = Aig_ManPoNum(p->pFrames)-Aig_ManRegNum(p->pAig);
     assert( (nConstrPairs & 1) == 0 );
     for ( i = 0; i < nConstrPairs; i += 2 )
@@ -358,39 +372,22 @@ clk = clock();
         Ssw_CnfNodeAddToSolver( p->pMSat, Aig_ObjFanin0(pObj) );//
     }
     sat_solver_simplify( p->pMSat->pSat );
-p->timeReduce += clock() - clk;
-
-//Ssw_ManUnique( p );
 
     // map constants and PIs of the last frame
     f = p->pPars->nFramesK;
     Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
     Saig_ManForEachPi( p->pAig, pObj, i )
         Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreatePi(p->pFrames) );
-    // make sure LOs are assigned
-    Saig_ManForEachLo( p->pAig, pObj, i )
-        assert( Ssw_ObjFrame( p, pObj, f ) != NULL );
-/*
-    // mark the PI/LO of the last frame
-    Aig_ManForEachPi( p->pAig, pObj, i )
-    {
-        pObjNew = Ssw_ObjFrame( p, pObj, f );
-        Aig_Regular(pObjNew)->fMarkA = 1;
-    }
-*/
-////    
-/*
+p->timeReduce += clock() - clk;
+
     // bring up the previous frames
     if ( p->pPars->fUniqueness )
         for ( v = 0; v < f; v++ )
             Saig_ManForEachLo( p->pAig, pObj, i )
                 Ssw_CnfNodeAddToSolver( p->pMSat, Aig_Regular(Ssw_ObjFrame(p, pObj, v)) );
-*/
-////
+
     // sweep internal nodes
     p->fRefined = 0;
-    p->nSatFailsReal = 0;
-    p->nUniques = 0;
     Ssw_ClassesClearRefined( p->ppClasses );
     if ( p->pPars->fVerbose )
         pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) );
@@ -402,13 +399,11 @@ p->timeReduce += clock() - clk;
             p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0 );
         else if ( Aig_ObjIsNode(pObj) )
         { 
-            pObj->fMarkA = Aig_ObjFanin0(pObj)->fMarkA | Aig_ObjFanin1(pObj)->fMarkA;
             pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
             Ssw_ObjSetFrame( p, pObj, f, pObjNew );
             p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0 );
         }
     }
-    p->nSatFailsTotal += p->nSatFailsReal;
     if ( p->pPars->fVerbose )
         Bar_ProgressStop( pProgress );
 
diff --git a/src/aig/ssw/sswUnique.c b/src/aig/ssw/sswUnique.c
index 0d9b016f..d6590716 100644
--- a/src/aig/ssw/sswUnique.c
+++ b/src/aig/ssw/sswUnique.c
@@ -42,7 +42,7 @@
 void Ssw_UniqueRegisterPairInfo( Ssw_Man_t * p )
 {
     Aig_Obj_t * pObjLo, * pObj0, * pObj1;
-    int i;
+    int i, RetValue, Counter;
     if ( p->vDiffPairs == NULL )
         p->vDiffPairs = Vec_IntAlloc( Saig_ManRegNum(p->pAig) );
     Vec_IntClear( p->vDiffPairs );
@@ -54,13 +54,22 @@ void Ssw_UniqueRegisterPairInfo( Ssw_Man_t * p )
             Vec_IntPush( p->vDiffPairs, 0 );
         else if ( pObj0 == Aig_Not(pObj1) )
             Vec_IntPush( p->vDiffPairs, 1 );
+//        else
+//            Vec_IntPush( p->vDiffPairs, 1 );
+        else if ( Aig_ObjPhaseReal(pObj0) != Aig_ObjPhaseReal(pObj1) )
+            Vec_IntPush( p->vDiffPairs, 1 );
         else 
         {
-            // assume that if the nodes are structurally different
-            // they can also be functionally different
-            Vec_IntPush( p->vDiffPairs, 1 );
+            RetValue = Ssw_NodesAreEquiv( p, Aig_Regular(pObj0), Aig_Regular(pObj1) );
+            Vec_IntPush( p->vDiffPairs, RetValue!=1 );
         }
     }
+    assert( Vec_IntSize(p->vDiffPairs) == Saig_ManRegNum(p->pAig) );
+    // count the number of ones
+    Counter = 0;
+    Vec_IntForEachEntry( p->vDiffPairs, RetValue, i )
+        Counter += RetValue;
+//    printf( "The number of different register pairs = %d.\n", Counter );
 }
 
 
@@ -75,9 +84,8 @@ void Ssw_UniqueRegisterPairInfo( Ssw_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Ssw_ManUniqueOne( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj )
+int Ssw_ManUniqueOne( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj, int fVerbose )
 {
-    int fVerbose = 0;
     Aig_Obj_t * ppObjs[2], * pTemp;
     int i, k, Value0, Value1, RetValue, fFeasible;
 
@@ -93,12 +101,15 @@ int Ssw_ManUniqueOne( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj )
     fFeasible = 0;
     k = 0;
     Vec_PtrForEachEntry( p->vCommon, pTemp, i )
-        if ( Saig_ObjIsLo(p->pAig, pTemp) )
-        {
-            Vec_PtrWriteEntry( p->vCommon, k++, pTemp );
-            if ( Vec_IntEntry(p->vDiffPairs, Aig_ObjPioNum(pTemp) - Saig_ManPiNum(p->pAig)) )
-                fFeasible = 1;
-        }
+    {
+        assert( Aig_ObjIsPi(pTemp) );
+        if ( !Saig_ObjIsLo(p->pAig, pTemp) )
+            continue;
+        assert( Aig_ObjPioNum(pTemp) > 0 );
+        Vec_PtrWriteEntry( p->vCommon, k++, pTemp );
+        if ( Vec_IntEntry(p->vDiffPairs, Aig_ObjPioNum(pTemp) - Saig_ManPiNum(p->pAig)) )
+            fFeasible = 1;
+    }
     Vec_PtrShrink( p->vCommon, k );
 
     if ( fVerbose )
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 1dce3257..31c6ba5e 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -8335,7 +8335,7 @@ int Abc_CommandSenseInput( Abc_Frame_t * pAbc, int argc, char ** argv )
 
 usage:
     fprintf( pErr, "usage: senseinput [-C num] [-vh]\n" );
-    fprintf( pErr, "\t         computes sensitivity of POs to PIs under constaint\n" );
+    fprintf( pErr, "\t         computes sensitivity of POs to PIs under constraint\n" );
     fprintf( pErr, "\t         constraint should be represented as the last PO" );
     fprintf( pErr, "\t-C num : the max number of conflicts at a node [default = %d]\n", nConfLim );
     fprintf( pErr, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
@@ -13559,7 +13559,7 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv )
     // set defaults
     Ssw_ManSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "PQFCLNSIplfuvwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "PQFCLNSIVMplfudvwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -13651,6 +13651,28 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nItersStop < 0 ) 
                 goto usage;
             break;
+        case 'V':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-V\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nSatVarMax2 = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nSatVarMax2 < 0 ) 
+                goto usage;
+            break;
+        case 'M':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-M\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nRecycleCalls2 = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nRecycleCalls2 < 0 ) 
+                goto usage;
+            break;
         case 'p':
             pPars->fPolarFlip ^= 1;
             break;
@@ -13663,6 +13685,9 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'u':
             pPars->fUniqueness ^= 1;
             break;
+        case 'd':
+            pPars->fDynamic ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -13693,19 +13718,7 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv )
         printf( "This command works only for structrally hashed networks. Run \"st\".\n" );
         return 0;
     }
-/*
-    if ( pPars->nFramesK > 1 && pPars->fUse1Hot )
-    {
-        printf( "Currrently can only use one-hotness for simple induction (K=1).\n" );
-        return 0;
-    }
 
-    if ( pPars->nFramesP && pPars->fUse1Hot )
-    {
-        printf( "Currrently can only use one-hotness without prefix.\n" );
-        return 0;
-    }
-*/
     // get the new network
     pNtkRes = Abc_NtkDarSeqSweep2( pNtk, pPars );
     if ( pNtkRes == NULL )
@@ -13718,7 +13731,7 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: scorr [-PQFCLNSI <num>] [-plfuvwh]\n" );
+    fprintf( pErr, "usage: scorr [-PQFCLNSIVM <num>] [-pludvwh]\n" );
     fprintf( pErr, "\t         performs sequential sweep using K-step induction\n" );
     fprintf( pErr, "\t-P num : max partition size (0 = no partitioning) [default = %d]\n", pPars->nPartSize );
     fprintf( pErr, "\t-Q num : partition overlap (0 = no overlap) [default = %d]\n", pPars->nOverSize );
@@ -13728,12 +13741,15 @@ usage:
     fprintf( pErr, "\t-N num : number of last POs treated as constraints (0=none) [default = %d]\n", pPars->nConstrs );
     fprintf( pErr, "\t-S num : additional simulation frames for c-examples (0=none) [default = %d]\n", pPars->nFramesAddSim );
     fprintf( pErr, "\t-I num : iteration number to stop and output SR-model (0=none) [default = %d]\n", pPars->nItersStop );
+    fprintf( pErr, "\t-V num : min var num needed to recycle the SAT solver [default = %d]\n", pPars->nSatVarMax2 );
+    fprintf( pErr, "\t-M num : min call num needed to recycle the SAT solver [default = %d]\n", pPars->nRecycleCalls2 );
     fprintf( pErr, "\t-p     : toggle alighning polarity of SAT variables [default = %s]\n", pPars->fPolarFlip? "yes": "no" );
     fprintf( pErr, "\t-l     : toggle latch correspondence only [default = %s]\n", pPars->fLatchCorr? "yes": "no" );
-//    fprintf( pErr, "\t-f     : toggle filtering using interative BMC [default = %s]\n", pPars->fSemiFormal? "yes": "no" );
+//    fprintf( pErr, "\t-f     : toggle filtering using iterative BMC [default = %s]\n", pPars->fSemiFormal? "yes": "no" );
     fprintf( pErr, "\t-u     : toggle using uniqueness constraints [default = %s]\n", pPars->fUniqueness? "yes": "no" );
-    fprintf( pErr, "\t-v     : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-d     : toggle dynamic addition of constraints [default = %s]\n", pPars->fDynamic? "yes": "no" );
     fprintf( pErr, "\t-w     : toggle printout of flop equivalences [default = %s]\n", pPars->fFlopVerbose? "yes": "no" );
+    fprintf( pErr, "\t-v     : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
 }
@@ -15213,7 +15229,7 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv )
     Fra_SecSetDefaultParams( pSecPar );
 //    pSecPar->TimeLimit = 300;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "cbFCGBRarmfijwvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "cbFCGDVBRarmfijwvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -15256,6 +15272,28 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pSecPar->nBTLimitGlobal < 0 ) 
                 goto usage;
             break;
+        case 'D':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-D\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pSecPar->nBTLimitInter = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pSecPar->nBTLimitInter < 0 ) 
+                goto usage;
+            break;
+        case 'V':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-V\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pSecPar->nBddVarsMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pSecPar->nBddVarsMax < 0 ) 
+                goto usage;
+            break;
         case 'B':
             if ( globalUtilOptind >= argc )
             {
@@ -15321,11 +15359,13 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: dprove [-FCGBR num] [-cbarmfijwvh]\n" );
+    fprintf( pErr, "usage: dprove [-FCGDVBR num] [-cbarmfijwvh]\n" );
     fprintf( pErr, "\t         performs SEC on the sequential miter\n" );
     fprintf( pErr, "\t-F num : the limit on the depth of induction [default = %d]\n", pSecPar->nFramesMax );
     fprintf( pErr, "\t-C num : the conflict limit at a node during induction [default = %d]\n", pSecPar->nBTLimit );
     fprintf( pErr, "\t-G num : the global conflict limit during induction [default = %d]\n", pSecPar->nBTLimitGlobal );
+    fprintf( pErr, "\t-D num : the conflict limit during interpolation [default = %d]\n", pSecPar->nBTLimitInter );
+    fprintf( pErr, "\t-V num : the flop count limit for BDD-based reachablity [default = %d]\n", pSecPar->nBddVarsMax );
     fprintf( pErr, "\t-B num : the BDD size limit in BDD-based reachablity [default = %d]\n", pSecPar->nBddMax );
     fprintf( pErr, "\t-R num : the max number of reachability iterations [default = %d]\n", pSecPar->nBddIterMax );
     fprintf( pErr, "\t-c     : toggles using CEC before attempting SEC [default = %s]\n", pSecPar->fTryComb? "yes": "no" );
@@ -19221,12 +19261,37 @@ int Abc_CommandAbc8Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nMinDomSize < 0 ) 
                 goto usage;
             break;
+        case 'V':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-V\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nSatVarMax2 = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nSatVarMax2 < 0 ) 
+                goto usage;
+            break;
+        case 'M':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-M\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nRecycleCalls2 = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nRecycleCalls2 < 0 ) 
+                goto usage;
+            break;
         case 'p':
             pPars->fPolarFlip ^= 1;
             break;
         case 'l':
             pPars->fLatchCorr ^= 1;
             break;
+        case 'd':
+            pPars->fDynamic ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -19249,6 +19314,13 @@ int Abc_CommandAbc8Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 0;
     }
 
+    if ( pPars->fDynamic && (pPars->nPartSize || pPars->nOverSize) )
+    {
+        pPars->nPartSize = 0;
+        pPars->nOverSize = 0;
+        printf( "With dynamic partitioning (-d) enabled, static one (-P <num> -Q <num>) is ignored.\n" );
+    }
+
     // get the input file name
     pNtlNew = Ntl_ManScorr( pAbc->pAbc8Ntl, pPars );
     if ( pNtlNew == NULL )
@@ -19273,7 +19345,7 @@ int Abc_CommandAbc8Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( stdout, "usage: *scorr [-PQFCLNSD <num>] [-plvh]\n" );
+    fprintf( stdout, "usage: *scorr [-PQFCLNSDVM <num>] [-plvh]\n" );
     fprintf( stdout, "\t         performs sequential sweep using K-step induction\n" );
     fprintf( stdout, "\t-P num : max partition size (0 = no partitioning) [default = %d]\n", pPars->nPartSize );
     fprintf( stdout, "\t-Q num : partition overlap (0 = no overlap) [default = %d]\n", pPars->nOverSize );
@@ -19283,8 +19355,11 @@ usage:
     fprintf( stdout, "\t-N num : number of last POs treated as constraints (0=none) [default = %d]\n", pPars->nConstrs );
     fprintf( stdout, "\t-S num : additional simulation frames for c-examples (0=none) [default = %d]\n", pPars->nFramesAddSim );
     fprintf( stdout, "\t-D num : min size of a clock domain used for synthesis [default = %d]\n", pPars->nMinDomSize );
+    fprintf( stdout, "\t-V num : min var num needed to recycle the SAT solver [default = %d]\n", pPars->nSatVarMax2 );
+    fprintf( stdout, "\t-M num : min call num needed to recycle the SAT solver [default = %d]\n", pPars->nRecycleCalls2 );
     fprintf( stdout, "\t-p     : toggle alighning polarity of SAT variables [default = %s]\n", pPars->fPolarFlip? "yes": "no" );
     fprintf( stdout, "\t-l     : toggle latch correspondence only [default = %s]\n", pPars->fLatchCorr? "yes": "no" );
+    fprintf( stdout, "\t-d     : toggle dynamic addition of constraints [default = %s]\n", pPars->fDynamic? "yes": "no" );
     fprintf( stdout, "\t-v     : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
     fprintf( stdout, "\t-h     : print the command usage\n");
     return 1;
@@ -19619,7 +19694,7 @@ int Abc_CommandAbc8DSec( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
 
     extern void Fra_SecSetDefaultParams( Fra_Sec_t * pSecPar );
-    extern int Fra_FraigSec( Aig_Man_t * p, Fra_Sec_t * pSecPar );
+    extern int Fra_FraigSec( Aig_Man_t * p, Fra_Sec_t * pSecPar, Aig_Man_t ** ppResult );
     extern Aig_Man_t * Ntl_ManPrepareSec( char * pFileName1, char * pFileName2 );
 
     // set defaults
@@ -19678,7 +19753,7 @@ int Abc_CommandAbc8DSec( Abc_Frame_t * pAbc, int argc, char ** argv )
     pAig = Ntl_ManPrepareSec( pArgvNew[0], pArgvNew[1] );
     if ( pAig == NULL )
         return 0;
-    Fra_FraigSec( pAig, pSecPar );
+    Fra_FraigSec( pAig, pSecPar, NULL );
     Aig_ManStop( pAig );
     return 0;
 
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index a142de31..3e7f3b65 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -1694,7 +1694,7 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar )
     }
     else
     {
-        RetValue = Fra_FraigSec( pMan, pSecPar );
+        RetValue = Fra_FraigSec( pMan, pSecPar, NULL );
         FREE( pNtk->pModel );
         FREE( pNtk->pSeqModel );
         pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
@@ -1793,7 +1793,7 @@ int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Fra_Sec_t * pSecPar )
     assert( pMan->nRegs > 0 );
 
     // perform verification
-    RetValue = Fra_FraigSec( pMan, pSecPar );
+    RetValue = Fra_FraigSec( pMan, pSecPar, NULL );
     Aig_ManStop( pMan );
     return RetValue;
 }
diff --git a/src/base/abci/abcSense.c b/src/base/abci/abcSense.c
index f3d71a54..a1e5b98a 100644
--- a/src/base/abci/abcSense.c
+++ b/src/base/abci/abcSense.c
@@ -140,7 +140,7 @@ Abc_Ntk_t * Abc_NtkSensitivityMiter( Abc_Ntk_t * pNtk, int iVar )
 
 /**Function*************************************************************
 
-  Synopsis    [Computing sensitivity of POs to POs under constaints.]
+  Synopsis    [Computing sensitivity of POs to POs under constraints.]
 
   Description [The input network is a combinatonal AIG. The last output
   is a constraint. The procedure returns the list of number of PIs, 
diff --git a/src/base/abci/abcSweep.c b/src/base/abci/abcSweep.c
index c5f4bb1e..2b78ceae 100644
--- a/src/base/abci/abcSweep.c
+++ b/src/base/abci/abcSweep.c
@@ -88,6 +88,7 @@ bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fExdc, int fVerbose,
 
     // perform fraiging of the AIG
     Fraig_ParamsSetDefault( &Params );
+    Params.fInternal = 1;
     pMan = Abc_NtkToFraig( pNtkAig, &Params, 0, 0 );   
     // cannot use EXDC with FRAIG because it can create classes of equivalent FRAIG nodes
     // with representative nodes that do not correspond to the nodes with the current network
diff --git a/src/base/main/mainMC.c b/src/base/main/mainMC.c
index 84c75b7b..dcabaf36 100644
--- a/src/base/main/mainMC.c
+++ b/src/base/main/mainMC.c
@@ -107,7 +107,7 @@ int main( int argc, char * argv[] )
             pSecPar->fSilent         =   1;  // disable phase-abstraction
 
             Dar_LibStart();
-            RetValue = Fra_FraigSec( pAig, pSecPar );
+            RetValue = Fra_FraigSec( pAig, pSecPar, NULL );
             Dar_LibStop();
             Cnf_ClearMemory();
         }
diff --git a/src/map/mapper/mapperMatch.c b/src/map/mapper/mapperMatch.c
index 74b83f75..32af030a 100644
--- a/src/map/mapper/mapperMatch.c
+++ b/src/map/mapper/mapperMatch.c
@@ -226,7 +226,7 @@ int Map_MatchNodePhase( Map_Man_t * p, Map_Node_t * pNode, int fPhase )
             Area2 = Map_SwitchCutRef( pNode, pNode->pCutBest[fPhase], fPhase );
         else 
             assert( 0 );
-        assert( Area2 < Area1 + p->fEpsilon );
+//        assert( Area2 < Area1 + p->fEpsilon );
     }
 
     // make sure that the requited times are met
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