Version abc80910

21 files changed, 737 insertions, 157 deletions

diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 03c05420..093912c3 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -470,6 +470,7 @@ extern int             Aig_ManLevelNum( Aig_Man_t * p );
 extern int             Aig_ManChoiceLevel( Aig_Man_t * p );
 extern int             Aig_DagSize( Aig_Obj_t * pObj );
 extern int             Aig_SupportSize( Aig_Man_t * p, Aig_Obj_t * pObj );
+extern Vec_Ptr_t *     Aig_Support( Aig_Man_t * p, Aig_Obj_t * pObj );
 extern void            Aig_ConeUnmark_rec( Aig_Obj_t * pObj );
 extern Aig_Obj_t *     Aig_Transfer( Aig_Man_t * pSour, Aig_Man_t * pDest, Aig_Obj_t * pObj, int nVars );
 extern Aig_Obj_t *     Aig_Compose( Aig_Man_t * p, Aig_Obj_t * pRoot, Aig_Obj_t * pFunc, int iVar );
@@ -562,6 +563,7 @@ extern Aig_Man_t *     Aig_ManFraigPartitioned( Aig_Man_t * pAig, int nPartSize,
 extern Aig_Man_t *     Aig_ManChoiceConstructive( Vec_Ptr_t * vAigs, int fVerbose );
 /*=== aigPartReg.c =========================================================*/
 extern Vec_Ptr_t *     Aig_ManRegPartitionSimple( Aig_Man_t * pAig, int nPartSize, int nOverSize );
+extern void            Aig_ManPartDivide( Vec_Ptr_t * vResult, Vec_Int_t * vDomain, int nPartSize, int nOverSize );
 extern Vec_Ptr_t *     Aig_ManRegPartitionSmart( Aig_Man_t * pAig, int nPartSize );
 extern Aig_Man_t *     Aig_ManRegCreatePart( Aig_Man_t * pAig, Vec_Int_t * vPart, int * pnCountPis, int * pnCountRegs, int ** ppMapBack );
 extern Vec_Ptr_t *     Aig_ManRegProjectOnehots( Aig_Man_t * pAig, Aig_Man_t * pPart, Vec_Ptr_t * vOnehots, int fVerbose );
diff --git a/src/aig/aig/aigDfs.c b/src/aig/aig/aigDfs.c
index c9893ed2..3c6658d9 100644
--- a/src/aig/aig/aigDfs.c
+++ b/src/aig/aig/aigDfs.c
@@ -685,6 +685,55 @@ int Aig_SupportSize( Aig_Man_t * p, Aig_Obj_t * pObj )
 
 /**Function*************************************************************
 
+  Synopsis    [Counts the support size of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+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_ObjIsPi(pObj) )
+    {
+        Vec_PtrPush( vSupp, pObj );
+        return;
+    }
+    assert( Aig_ObjIsNode(pObj) || Aig_ObjIsBuf(pObj) );
+    Aig_Support_rec( p, Aig_ObjFanin0(pObj), vSupp );
+    if ( Aig_ObjFanin1(pObj) )
+        Aig_Support_rec( p, Aig_ObjFanin1(pObj), vSupp );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Counts the support size of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Aig_Support( Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+    Vec_Ptr_t * vSupp;
+    assert( !Aig_IsComplement(pObj) );
+    assert( !Aig_ObjIsPo(pObj) );
+    Aig_ManIncrementTravId( p );
+    vSupp = Vec_PtrAlloc( 100 );
+    Aig_Support_rec( p, pObj, vSupp );
+    return vSupp;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Transfers the AIG from one manager into another.]
 
   Description []
diff --git a/src/aig/aig/aigPartReg.c b/src/aig/aig/aigPartReg.c
index 6baeae31..36be0810 100644
--- a/src/aig/aig/aigPartReg.c
+++ b/src/aig/aig/aigPartReg.c
@@ -498,6 +498,42 @@ Vec_Ptr_t * Aig_ManRegPartitionSimple( Aig_Man_t * pAig, int nPartSize, int nOve
 
 /**Function*************************************************************
 
+  Synopsis    [Divides a large partition into several ones.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManPartDivide( Vec_Ptr_t * vResult, Vec_Int_t * vDomain, int nPartSize, int nOverSize )
+{
+    Vec_Int_t * vPart;
+    int i, Counter;
+    assert( nPartSize && Vec_IntSize(vDomain) > nPartSize );
+    if ( nOverSize >= nPartSize )
+    {
+        printf( "Overlap size (%d) is more or equal than the partition size (%d).\n", nOverSize, nPartSize );
+        printf( "Adjusting it to be equal to half of the partition size.\n" );
+        nOverSize = nPartSize/2;
+    }
+    assert( nOverSize < nPartSize );
+    for ( Counter = 0; Counter < Vec_IntSize(vDomain); Counter -= nOverSize )
+    {
+        vPart = Vec_IntAlloc( nPartSize );
+        for ( i = 0; i < nPartSize; i++, Counter++ )
+            if ( Counter < Vec_IntSize(vDomain) )
+                Vec_IntPush( vPart, Vec_IntEntry(vDomain, Counter) );
+        if ( Vec_IntSize(vPart) <= nOverSize )
+            Vec_IntFree(vPart);
+        else
+            Vec_PtrPush( vResult, vPart );
+    }
+}
+
+/**Function*************************************************************
+
   Synopsis    [Computes partitioning of registers.]
 
   Description []
diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
index 6721634e..91689196 100644
--- a/src/aig/fra/fra.h
+++ b/src/aig/fra/fra.h
@@ -283,8 +283,8 @@ static inline int          Fra_ImpCreate( int Left, int Right )
 
 /*=== fraCec.c ========================================================*/
 extern int                 Fra_FraigSat( Aig_Man_t * pMan, sint64 nConfLimit, sint64 nInsLimit, int fFlipBits, int fAndOuts, int fVerbose );
-extern int                 Fra_FraigCec( Aig_Man_t ** ppAig, int fVerbose );
-extern int                 Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nPartSize, int fSmart, int fVerbose );
+extern int                 Fra_FraigCec( Aig_Man_t ** ppAig, int nConfLimit, int fVerbose );
+extern int                 Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int nPartSize, int fSmart, int fVerbose );
 /*=== fraClass.c ========================================================*/
 extern int                 Fra_BmcNodeIsConst( Aig_Obj_t * pObj );
 extern int                 Fra_BmcNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );
diff --git a/src/aig/fra/fraCec.c b/src/aig/fra/fraCec.c
index 9046d574..fdf87ccd 100644
--- a/src/aig/fra/fraCec.c
+++ b/src/aig/fra/fraCec.c
@@ -157,11 +157,11 @@ int Fra_FraigSat( Aig_Man_t * pMan, sint64 nConfLimit, sint64 nInsLimit, int fFl
   SeeAlso     []
 
 ***********************************************************************/
-int Fra_FraigCec( Aig_Man_t ** ppAig, int fVerbose )
+int Fra_FraigCec( Aig_Man_t ** ppAig, int nConfLimit, int fVerbose )
 {
-    int nBTLimitStart =     300;  // starting SAT run
-    int nBTLimitFirst =       2;  // first fraiging iteration
-    int nBTLimitLast  = 1000000;  // the last-gasp SAT run
+    int nBTLimitStart =        300;   // starting SAT run
+    int nBTLimitFirst =          2;   // first fraiging iteration
+    int nBTLimitLast  = nConfLimit;   // the last-gasp SAT run
 
     Fra_Par_t Params, * pParams = &Params;
     Aig_Man_t * pAig = *ppAig, * pTemp;
@@ -270,7 +270,7 @@ PRT( "Time", clock() - clk );
   SeeAlso     []
 
 ***********************************************************************/
-int Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nPartSize, int fSmart, int fVerbose )
+int Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int nPartSize, int fSmart, int fVerbose )
 {
     Aig_Man_t * pAig;
     Vec_Ptr_t * vParts;
@@ -294,7 +294,7 @@ int Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nPartSize
             continue;
         if ( RetValue == 0 )
             break;
-        RetValue = Fra_FraigCec( &pAig, 0 );
+        RetValue = Fra_FraigCec( &pAig, nConfLimit, 0 );
         Vec_PtrWriteEntry( vParts, i, pAig );
         if ( RetValue == 1 )
             continue;
@@ -361,9 +361,9 @@ int Fra_FraigCecTop( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int n
     assert( Aig_ManNodeNum(pMan1) >= Aig_ManNodeNum(pMan2) );
 
     if ( nPartSize )
-        RetValue = Fra_FraigCecPartitioned( pMan1, pMan2, nPartSize, fSmart, fVerbose );
+        RetValue = Fra_FraigCecPartitioned( pMan1, pMan2, nConfLimit, nPartSize, fSmart, fVerbose );
     else // no partitioning
-        RetValue = Fra_FraigCecPartitioned( pMan1, pMan2, Aig_ManPoNum(pMan1), 0, fVerbose );
+        RetValue = Fra_FraigCecPartitioned( pMan1, pMan2, nConfLimit, Aig_ManPoNum(pMan1), 0, fVerbose );
 
     // report the miter
     if ( RetValue == 1 )
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index ce9ec69b..f7674f7d 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -233,42 +233,6 @@ void Fra_FramesAddMore( Aig_Man_t * p, int nFrames )
     free( pLatches );
 }
 
-/**Function*************************************************************
-
-  Synopsis    [Divides a large partition into several ones.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_FraigInductionPartDivide( Vec_Ptr_t * vResult, Vec_Int_t * vDomain, int nPartSize, int nOverSize )
-{
-    Vec_Int_t * vPart;
-    int i, Counter;
-    assert( nPartSize && Vec_IntSize(vDomain) > nPartSize );
-    if ( nOverSize >= nPartSize )
-    {
-        printf( "Overlap size (%d) is more or equal than the partition size (%d).\n", nOverSize, nPartSize );
-        printf( "Adjusting it to be equal to half of the partition size.\n" );
-        nOverSize = nPartSize/2;
-    }
-    assert( nOverSize < nPartSize );
-    for ( Counter = 0; Counter < Vec_IntSize(vDomain); Counter -= nOverSize )
-    {
-        vPart = Vec_IntAlloc( nPartSize );
-        for ( i = 0; i < nPartSize; i++, Counter++ )
-            if ( Counter < Vec_IntSize(vDomain) )
-                Vec_IntPush( vPart, Vec_IntEntry(vDomain, Counter) );
-        if ( Vec_IntSize(vPart) <= nOverSize )
-            Vec_IntFree(vPart);
-        else
-            Vec_PtrPush( vResult, vPart );
-    }
-}
-
 
 /**Function*************************************************************
 
@@ -304,7 +268,7 @@ Aig_Man_t * Fra_FraigInductionPart( Aig_Man_t * pAig, Fra_Ssw_t * pPars )
         Vec_PtrForEachEntry( (Vec_Ptr_t *)pAig->vClockDoms, vPart, i )
         {
             if ( nPartSize && Vec_IntSize(vPart) > nPartSize )
-                Fra_FraigInductionPartDivide( vResult, vPart, nPartSize, pPars->nOverSize );
+                Aig_ManPartDivide( vResult, vPart, nPartSize, pPars->nOverSize );
             else
                 Vec_PtrPush( vResult, Vec_IntDup(vPart) );
         }
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index 5944cf56..b8f767df 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -230,7 +230,7 @@ PRT( "Time", clock() - clk );
     }
 
     if ( pNew->nRegs == 0 )
-        RetValue = Fra_FraigCec( &pNew, 0 );
+        RetValue = Fra_FraigCec( &pNew, 100000, 0 );
 
     RetValue = Fra_FraigMiterStatus( pNew );
     if ( RetValue >= 0 )
diff --git a/src/aig/ntl/ntlFraig.c b/src/aig/ntl/ntlFraig.c
index 0a991fff..b1239e47 100644
--- a/src/aig/ntl/ntlFraig.c
+++ b/src/aig/ntl/ntlFraig.c
@@ -20,6 +20,7 @@
 
 #include "ntl.h"
 #include "fra.h"
+#include "ssw.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -494,7 +495,43 @@ Ntl_Man_t * Ntl_ManSsw( Ntl_Man_t * p, Fra_Ssw_t * pPars )
     return pNew;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Returns AIG with WB after fraiging.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ntl_Man_t * Ntl_ManScorr( Ntl_Man_t * p, Ssw_Pars_t * pPars )
+{
+    Ntl_Man_t * pNew, * pAux;
+    Aig_Man_t * pAig, * pAigCol, * pTemp;
+
+    // collapse the AIG
+    pAig = Ntl_ManExtract( p );
+    pNew = Ntl_ManInsertAig( p, pAig );
+    pAigCol = Ntl_ManCollapseSeq( pNew, pPars->nMinDomSize );
+    if ( pAigCol == NULL )
+    {
+        Aig_ManStop( pAig );
+        return pNew;
+    }
 
+    // perform SCL for the given design
+    pTemp = Ssw_SignalCorrespondence( pAigCol, pPars );
+    Aig_ManStop( pTemp );
+
+    // finalize the transformation
+    pNew = Ntl_ManFinalize( pAux = pNew, pAig, pAigCol, pPars->fVerbose );
+    Ntl_ManFree( pAux );
+    Aig_ManStop( pAig );
+    Aig_ManStop( pAigCol );
+    return pNew;
+}
 
 
 /**Function*************************************************************
diff --git a/src/aig/ssw/module.make b/src/aig/ssw/module.make
index 2619751e..b176d4db 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/sswCnf.c \
     src/aig/ssw/sswCore.c \
     src/aig/ssw/sswMan.c \
+    src/aig/ssw/sswPart.c \
     src/aig/ssw/sswSat.c \
     src/aig/ssw/sswSim.c \
     src/aig/ssw/sswSimSat.c \
diff --git a/src/aig/ssw/ssw.h b/src/aig/ssw/ssw.h
index aaaa6407..f76664ec 100644
--- a/src/aig/ssw/ssw.h
+++ b/src/aig/ssw/ssw.h
@@ -44,11 +44,14 @@ struct Ssw_Pars_t_
     int              nPartSize;     // size of the partition
     int              nOverSize;     // size of the overlap between partitions
     int              nFramesK;      // the induction depth
+    int              nFramesAddSim; // the number of additional frames to simulate
     int              nConstrs;      // treat the last nConstrs POs as seq constraints
     int              nMaxLevs;      // the max number of levels of nodes to consider
     int              nBTLimit;      // conflict limit at a node
+    int              nMinDomSize;   // min clock domain considered for optimization
     int              fPolarFlip;    // uses polarity adjustment
     int              fLatchCorr;    // perform register correspondence
+    int              fSkipCheck;    // does not run equivalence check for unaffected cones
     int              fVerbose;      // verbose stats
     // internal parameters
     int              nIters;        // the number of iterations performed
@@ -77,6 +80,8 @@ struct Ssw_Cex_t_
 /*=== sswCore.c ==========================================================*/
 extern void          Ssw_ManSetDefaultParams( Ssw_Pars_t * p );
 extern Aig_Man_t *   Ssw_SignalCorrespondence( Aig_Man_t * p, Ssw_Pars_t * pPars );
+/*=== sswPart.c ==========================================================*/
+extern Aig_Man_t *   Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars );
 
 
 #ifdef __cplusplus
diff --git a/src/aig/ssw/sswClass.c b/src/aig/ssw/sswClass.c
index 66b86009..d06cce49 100644
--- a/src/aig/ssw/sswClass.c
+++ b/src/aig/ssw/sswClass.c
@@ -46,6 +46,7 @@ struct Ssw_Cla_t_
     // temporary data
     Vec_Ptr_t *      vClassOld;        // old equivalence class after splitting
     Vec_Ptr_t *      vClassNew;        // new equivalence class(es) after splitting
+    Vec_Ptr_t *      vRefined;         // the nodes refined since the last iteration
     // procedures used for class refinement
     void *           pManData;
     unsigned (*pFuncNodeHash) (void *,Aig_Obj_t *);              // returns hash key of the node
@@ -141,6 +142,7 @@ Ssw_Cla_t * Ssw_ClassesStart( Aig_Man_t * pAig )
     p->pClassSizes  = CALLOC( int, Aig_ManObjNumMax(pAig) );
     p->vClassOld    = Vec_PtrAlloc( 100 );
     p->vClassNew    = Vec_PtrAlloc( 100 );
+    p->vRefined     = Vec_PtrAlloc( 1000 );
     assert( pAig->pReprs == NULL );
     Aig_ManReprStart( pAig, Aig_ManObjNumMax(pAig) );
     return p;
@@ -183,6 +185,7 @@ void Ssw_ClassesStop( Ssw_Cla_t * p )
 {
     if ( p->vClassNew )    Vec_PtrFree( p->vClassNew );
     if ( p->vClassOld )    Vec_PtrFree( p->vClassOld );
+    Vec_PtrFree( p->vRefined );
     FREE( p->pId2Class );
     FREE( p->pClassSizes );
     FREE( p->pMemClasses );
@@ -191,6 +194,38 @@ void Ssw_ClassesStop( Ssw_Cla_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Ssw_ClassesGetRefined( Ssw_Cla_t * p )
+{
+    return p->vRefined;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_ClassesClearRefined( Ssw_Cla_t * p )
+{
+    Vec_PtrClear( p->vRefined );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Stop representation of equivalence classes.]
 
   Description []
@@ -368,12 +403,14 @@ void Ssw_ClassesRemoveNode( Ssw_Cla_t * p, Aig_Obj_t * pObj )
     assert( p->pId2Class[pObj->Id] == NULL );
     pRepr = Aig_ObjRepr( p->pAig, pObj );
     assert( pRepr != NULL );
+    Vec_PtrPush( p->vRefined, pObj );
     if ( Ssw_ObjIsConst1Cand( p->pAig, pObj ) )
     {
         Aig_ObjSetRepr( p->pAig, pObj, NULL );
         p->nCands1--;
         return;
     }
+    Vec_PtrPush( p->vRefined, pRepr );
     Aig_ObjSetRepr( p->pAig, pObj, NULL );
     assert( p->pId2Class[pRepr->Id][0] == pRepr );
     assert( p->pClassSizes[pRepr->Id] >= 2 );
@@ -409,7 +446,7 @@ void Ssw_ClassesRemoveNode( Ssw_Cla_t * p, Aig_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
-Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs )
+Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs, int fVerbose )
 {
     Ssw_Cla_t * p;
     Ssw_Sml_t * pSml;
@@ -424,7 +461,10 @@ 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 );
+if ( fVerbose )
+{
 PRT( "Simulation of 32 frames with 4 words", clock() - clk );
+}
 
     // set comparison procedures
 clk = clock();
@@ -441,7 +481,7 @@ clk = clock();
     {
         if ( fLatchCorr )
         {
-            if ( !Saig_ObjIsPi(p->pAig, pObj) )
+            if ( !Saig_ObjIsLo(p->pAig, pObj) )
                 continue;
         }
         else
@@ -521,7 +561,10 @@ clk = clock();
     Ssw_ClassesCheck( p );
     Ssw_SmlStop( pSml );
 //    Ssw_ClassesPrint( p, 0 );
+if ( fVerbose )
+{
 PRT( "Collecting candidate equival classes", clock() - clk );
+}
     return p;
 }
 
@@ -597,8 +640,6 @@ Ssw_Cla_t * Ssw_ClassesPrepareSimple( Aig_Man_t * pAig, int fLatchCorr, int nMax
     }
     // allocate room for classes
     p->pMemClassesFree = p->pMemClasses = ALLOC( Aig_Obj_t *, p->nCands1 );
-    // set comparison procedures
-    Ssw_ClassesSetData( p, NULL, NULL, Ssw_NodeIsConstCex, Ssw_NodesAreEqualCex );
 //    Ssw_ClassesPrint( p, 0 );
     return p;
 }
@@ -631,6 +672,9 @@ int Ssw_ClassesRefineOneClass( Ssw_Cla_t * p, Aig_Obj_t * pReprOld, int fRecursi
     // check if splitting happened
     if ( Vec_PtrSize(p->vClassNew) == 0 )
         return 0;
+    // remember that this class is refined
+    Ssw_ClassForEachNode( p, pReprOld, pObj, i )
+        Vec_PtrPush( p->vRefined, pObj );
 
     // get the new representative
     pReprNew = Vec_PtrEntry( p->vClassNew, 0 );
@@ -751,7 +795,10 @@ int Ssw_ClassesRefineConst1( Ssw_Cla_t * p, int fRecursive )
         {
             pObj = Aig_ManObj( p->pAig, i );
             if ( !p->pFuncNodeIsConst( p->pManData, pObj ) )
+            {
                 Vec_PtrPush( p->vClassNew, pObj );
+                Vec_PtrPush( p->vRefined, pObj );
+            }
         }
     // check if there is a new class
     if ( Vec_PtrSize(p->vClassNew) == 0 )
diff --git a/src/aig/ssw/sswCore.c b/src/aig/ssw/sswCore.c
index 409a1ebe..e6096c54 100644
--- a/src/aig/ssw/sswCore.c
+++ b/src/aig/ssw/sswCore.c
@@ -45,8 +45,10 @@ void Ssw_ManSetDefaultParams( Ssw_Pars_t * p )
     p->nPartSize      =     0;  // size of the partition
     p->nOverSize      =     0;  // size of the overlap between partitions
     p->nFramesK       =     1;  // the induction depth
+    p->nFramesAddSim  =     2;  // additional frames to simulate
     p->nConstrs       =     0;  // treat the last nConstrs POs as seq constraints
     p->nBTLimit       =  1000;  // conflict limit at a node
+    p->nMinDomSize    =   100;  // min clock domain considered for optimization
     p->fPolarFlip     =     0;  // uses polarity adjustment
     p->fLatchCorr     =     0;  // performs register correspondence
     p->fVerbose       =     0;  // verbose stats
@@ -71,21 +73,44 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
     int RetValue, nIter, clk, clkTotal = clock();
     // reset random numbers
     Aig_ManRandom( 1 );
+
+    // consider the case of empty AIG
+    if ( Aig_ManNodeNum(pAig) == 0 )
+    {
+        pPars->nIters = 0;
+        // Ntl_ManFinalize() needs the following to satisfy an assertion
+        Aig_ManReprStart( pAig,Aig_ManObjNumMax(pAig) );
+        return Aig_ManDupOrdered(pAig);
+    }
+
+    // check and update parameters
+    assert( Aig_ManRegNum(pAig) > 0 );
+    assert( pPars->nFramesK > 0 );
+    if ( pPars->nFramesK > 1 )
+        pPars->fSkipCheck = 0;
+
+    // perform partitioning
+    if ( (pPars->nPartSize > 0 && pPars->nPartSize < Aig_ManRegNum(pAig))
+         || (pAig->vClockDoms && Vec_VecSize(pAig->vClockDoms) > 0)  )
+        return Ssw_SignalCorrespondencePart( pAig, pPars );
+
     // start the choicing manager
     p = Ssw_ManCreate( pAig, pPars );
     // compute candidate equivalence classes
+//    p->pPars->nConstrs = 1;
     if ( p->pPars->nConstrs == 0 )
     {
-        p->ppClasses = Ssw_ClassesPrepare( pAig, pPars->fLatchCorr, pPars->nMaxLevs );
-        p->pSml = Ssw_SmlStart( pAig, 0, p->nFrames + 2, 2 );
+        // perform one round of seq simulation and generate candidate equivalence classes
+        p->ppClasses = Ssw_ClassesPrepare( pAig, pPars->fLatchCorr, pPars->nMaxLevs, pPars->fVerbose );
+        p->pSml = Ssw_SmlStart( pAig, 0, p->nFrames + p->pPars->nFramesAddSim, 1 );
         Ssw_ClassesSetData( p->ppClasses, p->pSml, Ssw_SmlNodeHash, Ssw_SmlNodeIsConst, Ssw_SmlNodesAreEqual );
     }
     else
     {
-        assert( 0 );
+        // create trivial equivalence classes with all nodes being candidates for constant 1
         p->ppClasses = Ssw_ClassesPrepareSimple( pAig, pPars->fLatchCorr, pPars->nMaxLevs );
+        Ssw_ClassesSetData( p->ppClasses, NULL, NULL, Ssw_NodeIsConstCex, Ssw_NodesAreEqualCex );
     }
-//    Ssw_ClassesSetData( p->ppClasses, NULL, NULL, Ssw_NodeIsConstCex, Ssw_NodesAreEqualCex );
 
     // get the starting stats
     p->nLitsBeg  = Ssw_ClassesLitNum( p->ppClasses );
@@ -111,9 +136,11 @@ clk = clock();
         RetValue = Ssw_ManSweep( p );
         if ( pPars->fVerbose )
         {
-            printf( "%3d : Const = %6d. Cl = %6d.  L = %6d. LR = %6d.  NR = %6d. ", 
+            printf( "%3d : Const = %6d. Cl = %6d. LR = %6d. NR = %6d. F = %5d. ", 
                 nIter, Ssw_ClassesCand1Num(p->ppClasses), Ssw_ClassesClassNum(p->ppClasses), 
-                p->nConstrTotal, p->nConstrReduced, Aig_ManNodeNum(p->pFrames) );
+                p->nConstrReduced, Aig_ManNodeNum(p->pFrames), p->nSatFailsReal );
+            printf( "Use = %5d. Skip = %5d. ", 
+                p->nRefUse, p->nRefSkip );
             PRT( "T", clock() - clk );
         } 
         Ssw_ManCleanup( p );
@@ -133,6 +160,8 @@ p->timeTotal = clock() - clkTotal;
     return pAigNew;
 }
 
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/ssw/sswInt.h b/src/aig/ssw/sswInt.h
index 009c09c4..c9dd1958 100644
--- a/src/aig/ssw/sswInt.h
+++ b/src/aig/ssw/sswInt.h
@@ -57,6 +57,8 @@ struct Ssw_Man_t_
     // equivalence classes
     Ssw_Cla_t *      ppClasses;      // equivalence classes of nodes
     int              fRefined;       // is set to 1 when refinement happens
+    int              nRefUse;
+    int              nRefSkip;  
     // SAT solving
     sat_solver *     pSat;           // recyclable SAT solver
     int              nSatVars;       // the counter of SAT variables
@@ -77,8 +79,8 @@ struct Ssw_Man_t_
     // SAT calls statistics
     int              nSatCalls;      // the number of SAT calls
     int              nSatProof;      // the number of proofs
-    int              nSatFails;      // the number of timeouts
     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
@@ -91,6 +93,7 @@ struct Ssw_Man_t_
     // runtime stats
     int              timeBmc;        // bounded model checking
     int              timeReduce;     // speculative reduction
+    int              timeMarkCones;  // marking the cones not to be refined
     int              timeSimSat;     // simulation of the counter-examples
     int              timeSat;        // solving SAT
     int              timeSatSat;     // sat
@@ -136,6 +139,8 @@ extern void          Ssw_ClassesSetData( Ssw_Cla_t * p, void * pManData,
                          int (*pFuncNodeIsConst)(void *,Aig_Obj_t *),
                          int (*pFuncNodesAreEqual)(void *,Aig_Obj_t *, Aig_Obj_t *) );
 extern void          Ssw_ClassesStop( Ssw_Cla_t * p );
+extern Vec_Ptr_t *   Ssw_ClassesGetRefined( Ssw_Cla_t * p );
+extern void          Ssw_ClassesClearRefined( Ssw_Cla_t * p );
 extern int           Ssw_ClassesCand1Num( Ssw_Cla_t * p );
 extern int           Ssw_ClassesClassNum( Ssw_Cla_t * p );
 extern int           Ssw_ClassesLitNum( Ssw_Cla_t * p );
@@ -143,7 +148,7 @@ extern Aig_Obj_t **  Ssw_ClassesReadClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, int
 extern void          Ssw_ClassesCheck( Ssw_Cla_t * p );
 extern void          Ssw_ClassesPrint( Ssw_Cla_t * p, int fVeryVerbose );
 extern void          Ssw_ClassesRemoveNode( Ssw_Cla_t * p, Aig_Obj_t * pObj );
-extern Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs );
+extern Ssw_Cla_t *   Ssw_ClassesPrepare( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs, int fVerbose );
 extern Ssw_Cla_t *   Ssw_ClassesPrepareSimple( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs );
 extern int           Ssw_ClassesRefine( Ssw_Cla_t * p, int fRecursive );
 extern int           Ssw_ClassesRefineOneClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, int fRecursive );
@@ -171,6 +176,7 @@ extern int           Ssw_SmlNodesAreEqual( Ssw_Sml_t * p, Aig_Obj_t * pObj0, Aig
 extern void          Ssw_SmlAssignDist1Plus( Ssw_Sml_t * p, unsigned * pPat );
 extern void          Ssw_SmlSimulateOne( Ssw_Sml_t * p );
 /*=== sswSimSat.c ===================================================*/
+extern int           Ssw_ManOriginalPiValue( Ssw_Man_t * p, Aig_Obj_t * pObj, int f );
 extern void          Ssw_ManResimulateCex( Ssw_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr, int f );
 extern void          Ssw_ManResimulateCexTotal( Ssw_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr, int f );
 extern void          Ssw_ManResimulateCexTotalSim( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr, int f );
diff --git a/src/aig/ssw/sswMan.c b/src/aig/ssw/sswMan.c
index a6e02125..f25cee45 100644
--- a/src/aig/ssw/sswMan.c
+++ b/src/aig/ssw/sswMan.c
@@ -99,27 +99,28 @@ void Ssw_ManPrintStats( Ssw_Man_t * p )
 {
     double nMemory = 1.0*Aig_ManObjNumMax(p->pAig)*p->nFrames*(2*sizeof(int)+2*sizeof(void*))/(1<<20);
 
-    printf( "Parameters: Frames = %d. Conf limit = %d. Constrs = %d. Max lev = %d. Mem = %0.2f Mb.\n", 
-        p->pPars->nFramesK, p->pPars->nBTLimit, p->pPars->nConstrs, p->pPars->nMaxLevs, nMemory );
+    printf( "Parameters: Fr = %d. C-limit = %d. Constr = %d. SkipCheck = %d. MaxLev = %d. Mem = %0.2f Mb.\n", 
+        p->pPars->nFramesK, p->pPars->nBTLimit, p->pPars->nConstrs, p->pPars->fSkipCheck, p->pPars->nMaxLevs, nMemory );
     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), 
         p->nSatVarsTotal/p->pPars->nIters );
-    printf( "SAT calls : Proof = %d. Cex = %d. Fail = %d. FailReal = %d.  Equivs = %d. Str = %d.\n", 
-        p->nSatProof, p->nSatCallsSat, p->nSatFails, p->nSatFailsReal, Ssw_ManCountEquivs(p), p->nStrangers );
+    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( "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) );
 
-    p->timeOther = p->timeTotal-p->timeBmc-p->timeReduce-p->timeSimSat-p->timeSat;
-    PRTP( "BMC        ", p->timeBmc,      p->timeTotal );
-    PRTP( "Spec reduce", p->timeReduce,   p->timeTotal );
-    PRTP( "Sim SAT    ", p->timeSimSat,   p->timeTotal );
-    PRTP( "SAT solving", p->timeSat,      p->timeTotal );
-    PRTP( "  unsat    ", p->timeSatUnsat, p->timeTotal );
-    PRTP( "  sat      ", p->timeSatSat,   p->timeTotal );
-    PRTP( "  undecided", p->timeSatUndec, p->timeTotal );
-    PRTP( "Other      ", p->timeOther,    p->timeTotal );
-    PRTP( "TOTAL      ", p->timeTotal,    p->timeTotal );
+    p->timeOther = p->timeTotal-p->timeBmc-p->timeReduce-p->timeMarkCones-p->timeSimSat-p->timeSat;
+    PRTP( "BMC        ", p->timeBmc,       p->timeTotal );
+    PRTP( "Spec reduce", p->timeReduce,    p->timeTotal );
+    PRTP( "Mark cones ", p->timeMarkCones, p->timeTotal );
+    PRTP( "Sim SAT    ", p->timeSimSat,    p->timeTotal );
+    PRTP( "SAT solving", p->timeSat,       p->timeTotal );
+    PRTP( "  unsat    ", p->timeSatUnsat,  p->timeTotal );
+    PRTP( "  sat      ", p->timeSatSat,    p->timeTotal );
+    PRTP( "  undecided", p->timeSatUndec,  p->timeTotal );
+    PRTP( "Other      ", p->timeOther,     p->timeTotal );
+    PRTP( "TOTAL      ", p->timeTotal,     p->timeTotal );
 }
 
 /**Function*************************************************************
@@ -167,6 +168,7 @@ void Ssw_ManCleanup( Ssw_Man_t * p )
 ***********************************************************************/
 void Ssw_ManStop( Ssw_Man_t * p )
 {
+    Aig_ManCleanMarkA( p->pAig );
     if ( p->pPars->fVerbose )
         Ssw_ManPrintStats( p );
     if ( p->ppClasses )
diff --git a/src/aig/ssw/sswPart.c b/src/aig/ssw/sswPart.c
new file mode 100644
index 00000000..7eb6b8fe
--- /dev/null
+++ b/src/aig/ssw/sswPart.c
@@ -0,0 +1,129 @@
+/**CFile****************************************************************
+
+  FileName    [sswPart.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Inductive prover with constraints.]
+
+  Synopsis    [Partitioned signal correspondence.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - September 1, 2008.]
+
+  Revision    [$Id: sswPart.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "sswInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Performs partitioned sequential SAT sweepingG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
+{
+    int fPrintParts = 0;
+    char Buffer[100];
+    Aig_Man_t * pTemp, * pNew;
+    Vec_Ptr_t * vResult;
+    Vec_Int_t * vPart;
+    int * pMapBack;
+    int i, nCountPis, nCountRegs;
+    int nClasses, nPartSize, fVerbose;
+    int clk = clock();
+
+    // save parameters
+    nPartSize = pPars->nPartSize; pPars->nPartSize = 0;
+    fVerbose  = pPars->fVerbose;  pPars->fVerbose = 0;
+    // generate partitions
+    if ( pAig->vClockDoms )
+    {
+        // divide large clock domains into separate partitions
+        vResult = Vec_PtrAlloc( 100 );
+        Vec_PtrForEachEntry( (Vec_Ptr_t *)pAig->vClockDoms, vPart, i )
+        {
+            if ( nPartSize && Vec_IntSize(vPart) > nPartSize )
+                Aig_ManPartDivide( vResult, vPart, nPartSize, pPars->nOverSize );
+            else
+                Vec_PtrPush( vResult, Vec_IntDup(vPart) );
+        }
+    }
+    else
+        vResult = Aig_ManRegPartitionSimple( pAig, nPartSize, pPars->nOverSize );
+//    vResult = Aig_ManPartitionSmartRegisters( pAig, nPartSize, 0 ); 
+//    vResult = Aig_ManRegPartitionSmart( pAig, nPartSize );
+    if ( fPrintParts )
+    {
+        // print partitions
+        printf( "Simple partitioning. %d partitions are saved:\n", Vec_PtrSize(vResult) );
+        Vec_PtrForEachEntry( vResult, vPart, i )
+        {
+            extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact );
+            sprintf( Buffer, "part%03d.aig", i );
+            pTemp = Aig_ManRegCreatePart( pAig, vPart, &nCountPis, &nCountRegs, NULL );
+            Ioa_WriteAiger( pTemp, Buffer, 0, 0 );
+            printf( "part%03d.aig : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d.\n", 
+                i, Vec_IntSize(vPart), Aig_ManPiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Aig_ManNodeNum(pTemp) );
+            Aig_ManStop( pTemp );
+        }
+    }
+
+    // perform SSW with partitions
+    Aig_ManReprStart( pAig, Aig_ManObjNumMax(pAig) );
+    Vec_PtrForEachEntry( vResult, vPart, i )
+    {
+        pTemp = Aig_ManRegCreatePart( pAig, vPart, &nCountPis, &nCountRegs, &pMapBack );
+        Aig_ManSetRegNum( pTemp, pTemp->nRegs );
+        // create the projection of 1-hot registers
+        if ( pAig->vOnehots )
+            pTemp->vOnehots = Aig_ManRegProjectOnehots( pAig, pTemp, pAig->vOnehots, fVerbose );
+        // run SSW
+        pNew = Ssw_SignalCorrespondence( pTemp, pPars );
+        nClasses = Aig_TransferMappedClasses( pAig, pTemp, pMapBack );
+        if ( fVerbose )
+            printf( "%3d : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d. It = %3d. Cl = %5d.\n", 
+                i, Vec_IntSize(vPart), Aig_ManPiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Aig_ManNodeNum(pTemp), pPars->nIters, nClasses );
+        Aig_ManStop( pNew );
+        Aig_ManStop( pTemp );
+        free( pMapBack );
+    }
+    // remap the AIG
+    pNew = Aig_ManDupRepr( pAig, 0 );
+    Aig_ManSeqCleanup( pNew );
+//    Aig_ManPrintStats( pAig );
+//    Aig_ManPrintStats( pNew );
+    Vec_VecFree( (Vec_Vec_t *)vResult );
+    pPars->nPartSize = nPartSize;
+    pPars->fVerbose = fVerbose;
+    if ( fVerbose )
+    {
+        PRT( "Total time", clock() - clk );
+    }
+    return pNew;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/ssw/sswSimSat.c b/src/aig/ssw/sswSimSat.c
index 547755f0..6ef5ec20 100644
--- a/src/aig/ssw/sswSimSat.c
+++ b/src/aig/ssw/sswSimSat.c
@@ -234,7 +234,8 @@ void Ssw_ManResimulateCexTotal( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pR
     // set the PI simulation information
     Aig_ManConst1(p->pAig)->fMarkB = 1;
     Aig_ManForEachPi( p->pAig, pObj, i )
-        pObj->fMarkB = Ssw_ManOriginalPiValue( p, pObj, f );
+//        pObj->fMarkB = Ssw_ManOriginalPiValue( p, pObj, f );
+        pObj->fMarkB = Aig_InfoHasBit( p->pPatWords, i );
     // simulate internal nodes
     Aig_ManForEachNode( p->pAig, pObj, i )
         pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) )
@@ -253,27 +254,6 @@ p->timeSimSat += clock() - clk;
 
 /**Function*************************************************************
 
-  Synopsis    [Copy pattern from the solver into the internal storage.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-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 ( Ssw_ManOriginalPiValue( p, pObj, f ) )
-            Aig_InfoSetBit( p->pPatWords, i );
-}
-
-/**Function*************************************************************
-
   Synopsis    [Handle the counter-example.]
 
   Description []
@@ -287,7 +267,7 @@ void Ssw_ManResimulateCexTotalSim( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t *
 {
     int RetValue1, RetValue2, clk = clock();
     // save the counter-example
-    Ssw_SmlSavePatternAig( p, f );
+//    Ssw_SmlSavePatternAig( p, f );
     // set the PI simulation information
     Ssw_SmlAssignDist1Plus( p->pSml, p->pPatWords );
     // simulate internal nodes
diff --git a/src/aig/ssw/sswSweep.c b/src/aig/ssw/sswSweep.c
index 7c99fad2..5ad6d78e 100644
--- a/src/aig/ssw/sswSweep.c
+++ b/src/aig/ssw/sswSweep.c
@@ -31,6 +31,95 @@
 
 /**Function*************************************************************
 
+  Synopsis    [Mark nodes affected by sweep in the previous iteration.]
+
+  Description [Assumes that affected nodes are in p->ppClasses->vRefined.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_ManSweepMarkRefinement( Ssw_Man_t * p )
+{
+    Vec_Ptr_t * vRefined, * vSupp;
+    Aig_Obj_t * pObj, * pObjLo, * pObjLi;
+    int i, k;
+    vRefined = Ssw_ClassesGetRefined( p->ppClasses );
+    if ( Vec_PtrSize(vRefined) == 0 )
+    {
+        Aig_ManForEachObj( p->pAig, pObj, i )
+            pObj->fMarkA = 1;
+        return;
+    }
+    // mark the nodes to be refined
+    Aig_ManCleanMarkA( p->pAig );
+    Vec_PtrForEachEntry( vRefined, pObj, i )
+    {
+        if ( Aig_ObjIsPi(pObj) )
+        {
+            pObj->fMarkA = 1;
+            continue;
+        }
+        assert( Aig_ObjIsNode(pObj) );
+        vSupp = Aig_Support( p->pAig, pObj );
+        Vec_PtrForEachEntry( vSupp, pObjLo, k )
+            pObjLo->fMarkA = 1;
+        Vec_PtrFree( vSupp );
+    }
+    // mark refinement
+    Aig_ManForEachNode( p->pAig, pObj, i )
+        pObj->fMarkA = Aig_ObjFanin0(pObj)->fMarkA | Aig_ObjFanin1(pObj)->fMarkA;
+    Saig_ManForEachLi( p->pAig, pObj, i )
+        pObj->fMarkA |= Aig_ObjFanin0(pObj)->fMarkA;
+    Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
+        pObjLo->fMarkA |= pObjLi->fMarkA;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Copy pattern from the solver into the internal storage.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+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 ( Ssw_ManOriginalPiValue( p, pObj, f ) )
+            Aig_InfoSetBit( p->pPatWords, i );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Copy pattern from the solver into the internal storage.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+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 ( Aig_ObjPhaseReal( Ssw_ObjFraig(p, pObj, f) ) )
+            Aig_InfoSetBit( p->pPatWords, i );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Performs fraiging for one node.]
 
   Description [Returns the fraiged node.]
@@ -40,7 +129,7 @@
   SeeAlso     []
 
 ***********************************************************************/
-void Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f )
+void Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f, int fBmc )
 { 
     Aig_Obj_t * pObjRepr, * pObjFraig, * pObjFraig2, * pObjReprFraig;
     int RetValue;
@@ -50,59 +139,58 @@ void Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f )
         return;
     // get the fraiged node
     pObjFraig = Ssw_ObjFraig( p, pObj, f );
-    assert( pObjFraig != NULL );
     // get the fraiged representative
     pObjReprFraig = Ssw_ObjFraig( p, pObjRepr, f );
-    assert( pObjReprFraig != NULL );
     // check if constant 0 pattern distinquishes these nodes
+    assert( pObjFraig != NULL && pObjReprFraig != NULL );
     if ( (pObj->fPhase == pObjRepr->fPhase) != (Aig_ObjPhaseReal(pObjFraig) == Aig_ObjPhaseReal(pObjReprFraig)) )
     {
-        Aig_Obj_t * pObj;
-        int i;
-        if ( p->pSat->model.cap < p->pSat->size )
-        {
-            veci_resize(&p->pSat->model, 0);
-            for ( i = 0; i < p->pSat->size; i++ ) 
-                veci_push( &p->pSat->model, (int)l_False );
-        }
-        // set the values of SAT vars to be equal to the phase of the nodes
-        Aig_ManForEachObj( p->pFrames, pObj, i )
-            if ( Ssw_ObjSatNum( p, pObj ) )
-            {
-                int iVar = Ssw_ObjSatNum( p, pObj );
-                assert( iVar < p->pSat->size );
-                p->pSat->model.ptr[iVar] = (int)(p->pPars->fPolarFlip? 0 : (pObj->fPhase? l_True : l_False));
-                p->pSat->model.size = p->pSat->size;
-            }
         p->nStrangers++;
-        return;
+        Ssw_SmlSavePatternAigPhase( p, f );
     }
-    // if the fraiged nodes are the same, return
-    if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) )
-        return;
-//    assert( Aig_Regular(pObjFraig) != Aig_ManConst1(p->pFrames) );
-    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 ) // timed out
-    {
-//        assert( 0 );
-        Ssw_ClassesRemoveNode( p->ppClasses, pObj );
-        p->fRefined = 1;
-        return;
-    }
-    if ( RetValue == 1 )  // proved equivalent
     {
-        pObjFraig2 = Aig_NotCond( pObjReprFraig, pObj->fPhase ^ pObjRepr->fPhase );
-        Ssw_ObjSetFraig( p, pObj, f, pObjFraig2 );
-        return;
+        // if the fraiged nodes are the same, return
+        if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) )
+            return;
+        // count the number of skipped calls
+        if ( !pObj->fMarkA && !pObjRepr->fMarkA )
+            p->nRefSkip++;
+        else
+            p->nRefUse++;
+        // call equivalence checking
+        if ( p->pPars->fSkipCheck && !fBmc && !pObj->fMarkA && !pObjRepr->fMarkA )
+            RetValue = 1;
+        else 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_ObjSetFraig( p, pObj, f, pObjFraig2 );
+            return;
+        }
+        if ( RetValue == -1 ) // timed out
+        {
+            Ssw_ClassesRemoveNode( p->ppClasses, pObj );
+            p->fRefined = 1;
+            return;
+        }
+        // check if skipping calls works correctly
+        if ( p->pPars->fSkipCheck && !fBmc && !pObj->fMarkA && !pObjRepr->fMarkA )
+        {
+            assert( 0 );
+            printf( "\nMistake!!!\n" );
+        }
+        // disproved the equivalence
+        Ssw_SmlSavePatternAig( p, f );
     }
-    // disproved the equivalence
 //    Ssw_ManResimulateCex( p, pObj, pObjRepr, f );
-//    Ssw_ManResimulateCexTotal( p, pObj, pObjRepr, f );
-    Ssw_ManResimulateCexTotalSim( p, pObj, pObjRepr, f );
+    if ( p->pPars->nConstrs == 0 )
+        Ssw_ManResimulateCexTotalSim( p, pObj, pObjRepr, f );
+    else
+        Ssw_ManResimulateCexTotal( p, pObj, pObjRepr, f );
     assert( Aig_ObjRepr( p->pAig, pObj ) != pObjRepr );
     p->fRefined = 1;
 }
@@ -147,7 +235,7 @@ clk = clock();
                 Bar_ProgressUpdate( pProgress, Aig_ManObjNumMax(p->pAig) * f + i, NULL );
             pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
             Ssw_ObjSetFraig( p, pObj, f, pObjNew );
-            Ssw_ManSweepNode( p, pObj, f );
+            Ssw_ManSweepNode( p, pObj, f, 1 );
         }
         // quit if this is the last timeframe
         if ( f == p->pPars->nFramesK - 1 )
@@ -205,6 +293,12 @@ clk = clock();
     sat_solver_simplify( p->pSat );
 p->timeReduce += clock() - clk;
 
+    // mark nodes that do not have to be refined
+clk = clock();
+    if ( p->pPars->fSkipCheck )
+        Ssw_ManSweepMarkRefinement( p );
+p->timeMarkCones += clock() - clk;
+
     // map constants and PIs of the last frame
     f = p->pPars->nFramesK;
     Ssw_ObjSetFraig( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
@@ -215,6 +309,9 @@ p->timeReduce += clock() - clk;
         assert( Ssw_ObjFraig( p, pObj, f ) != NULL );
     // sweep internal nodes
     p->fRefined = 0;
+    p->nSatFailsReal = 0;
+    p->nRefUse = p->nRefSkip = 0;
+    Ssw_ClassesClearRefined( p->ppClasses );
     if ( p->pPars->fVerbose )
         pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) );
     Aig_ManForEachObj( p->pAig, pObj, i )
@@ -222,14 +319,16 @@ p->timeReduce += clock() - clk;
         if ( p->pPars->fVerbose )
             Bar_ProgressUpdate( pProgress, i, NULL );
         if ( Saig_ObjIsLo(p->pAig, pObj) )
-            Ssw_ManSweepNode( p, pObj, f );
+            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_ObjSetFraig( p, pObj, f, pObjNew );
-            Ssw_ManSweepNode( p, pObj, f );
+            Ssw_ManSweepNode( p, pObj, f, 0 );
         }
     }
+    p->nSatFailsTotal += p->nSatFailsReal;
     if ( p->pPars->fVerbose )
         Bar_ProgressStop( pProgress );
 
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 0125ae9e..3c7314ef 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -245,6 +245,7 @@ static int Abc_CommandAbc8Fraig      ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandAbc8Scl        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc8Lcorr      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc8Ssw        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc8Scorr      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc8Sweep      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc8Zero       ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
@@ -506,6 +507,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC8",         "*scl",          Abc_CommandAbc8Scl,          0 );
     Cmd_CommandAdd( pAbc, "ABC8",         "*lcorr",        Abc_CommandAbc8Lcorr,        0 );
     Cmd_CommandAdd( pAbc, "ABC8",         "*ssw",          Abc_CommandAbc8Ssw,          0 );
+    Cmd_CommandAdd( pAbc, "ABC8",         "*scorr",        Abc_CommandAbc8Scorr,        0 );
     Cmd_CommandAdd( pAbc, "ABC8",         "*sw",           Abc_CommandAbc8Sweep,        0 );
     Cmd_CommandAdd( pAbc, "ABC8",         "*zero",         Abc_CommandAbc8Zero,         0 );
 
@@ -7681,7 +7683,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk;
-    Abc_Ntk_t * pNtkRes;
+//    Abc_Ntk_t * pNtkRes;
     int c;
     int fBmc;
     int nFrames;
@@ -7700,7 +7702,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     extern Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName );
     extern Abc_Ntk_t * Abc_NtkFilter( Abc_Ntk_t * pNtk );
 //    extern Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose );
-    extern Abc_Ntk_t * Abc_NtkPcmTest( Abc_Ntk_t * pNtk, int fVerbose );
+//    extern Abc_Ntk_t * Abc_NtkPcmTest( Abc_Ntk_t * pNtk, int fVerbose );
     extern Abc_Ntk_t * Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk, int nIters, int nSteps, int fRetimingOnly, int fAddBugs, int fUseCnf, int fVerbose );
 //    extern void Abc_NtkDarTestBlif( char * pFileName );
 //    extern Abc_Ntk_t * Abc_NtkDarPartition( Abc_Ntk_t * pNtk );
@@ -7869,7 +7871,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 */
 
 
-
+/*
 //    pNtkRes = Abc_NtkDar( pNtk );
 //    pNtkRes = Abc_NtkDarRetime( pNtk, nLevels, 1 ); 
 //    pNtkRes = Abc_NtkPcmTestAig( pNtk, fVerbose );
@@ -7883,7 +7885,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     // replace the current network
     Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
     return 0;
-
+*/
 
 
 //    Abc_NtkDarClau( pNtk, nFrames, nLevels, fBmc, fVerbose, fVeryVerbose );
@@ -13483,7 +13485,7 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: ssweep [-PQNFL num] [-lrfetvh]\n" );
+    fprintf( pErr, "usage: ssweep [-PQNFL <num>] [-lrfetvh]\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 );
@@ -13528,7 +13530,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, "PQFCLNplvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "PQFCLNSplsvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -13595,7 +13597,18 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv )
             }
             pPars->nConstrs = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
-            if ( pPars->nConstrs <= 0 ) 
+            if ( pPars->nConstrs < 0 ) 
+                goto usage;
+            break;
+        case 'S':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-S\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nFramesAddSim = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nFramesAddSim < 0 ) 
                 goto usage;
             break;
         case 'p':
@@ -13604,6 +13617,9 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'l':
             pPars->fLatchCorr ^= 1;
             break;
+        case 's':
+            pPars->fSkipCheck ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -13656,7 +13672,7 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: scorr [-PQFCLN num] [-plvh]\n" );
+    fprintf( pErr, "usage: scorr [-PQFCLNS <num>] [-plsvh]\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 );
@@ -13664,8 +13680,10 @@ usage:
     fprintf( pErr, "\t-C num : max number of conflicts at a node (0=inifinite) [default = %d]\n", pPars->nBTLimit );
     fprintf( pErr, "\t-L num : max number of levels to consider (0=all) [default = %d]\n", pPars->nMaxLevs );
     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-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-s     : toggle skipping unaffected cones [default = %s]\n", pPars->fSkipCheck? "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;
@@ -14586,7 +14604,7 @@ int Abc_CommandDCec( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fMiter;
 
     extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fAlignPol, int fAndOuts, int fVerbose );
-    extern int Abc_NtkDarCec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fPartition, int fVerbose );
+    extern int Abc_NtkDarCec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int fPartition, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -14687,7 +14705,7 @@ int Abc_CommandDCec( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( fSat && fMiter )
         Abc_NtkDSat( pNtk1, nConfLimit, nInsLimit, 0, 0, fVerbose );
     else
-        Abc_NtkDarCec( pNtk1, pNtk2, fPartition, fVerbose );
+        Abc_NtkDarCec( pNtk1, pNtk2, nConfLimit, fPartition, fVerbose );
 
     if ( fDelete1 ) Abc_NtkDelete( pNtk1 );
     if ( fDelete2 ) Abc_NtkDelete( pNtk2 );
@@ -18764,6 +18782,182 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandAbc8Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    void * pNtlNew;
+    Ssw_Pars_t Pars, * pPars = &Pars;
+    int c;
+    extern Aig_Man_t * Ntl_ManExtract( void * p );
+    extern void * Ntl_ManScorr( void * p, Ssw_Pars_t * pPars );
+    extern int Ntl_ManIsComb( void * p );
+
+    // set defaults
+    Ssw_ManSetDefaultParams( pPars );
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "PQFCLNSplsvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'P':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-P\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nPartSize = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nPartSize < 2 ) 
+                goto usage;
+            break;
+        case 'Q':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-Q\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nOverSize = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nOverSize < 0 ) 
+                goto usage;
+            break;
+        case 'F':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-F\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nFramesK = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nFramesK <= 0 ) 
+                goto usage;
+            break;
+        case 'C':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-C\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nBTLimit = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nBTLimit <= 0 ) 
+                goto usage;
+            break;
+        case 'L':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-L\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nMaxLevs = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nMaxLevs <= 0 ) 
+                goto usage;
+            break;
+        case 'N':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-N\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nConstrs = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nConstrs < 0 ) 
+                goto usage;
+            break;
+        case 'S':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-S\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nFramesAddSim = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nFramesAddSim < 0 ) 
+                goto usage;
+            break;
+        case 'p':
+            pPars->fPolarFlip ^= 1;
+            break;
+        case 'l':
+            pPars->fLatchCorr ^= 1;
+            break;
+        case 's':
+            pPars->fSkipCheck ^= 1;
+            break;
+        case 'v':
+            pPars->fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pAbc->pAbc8Ntl == NULL )
+    {
+        printf( "Abc_CommandAbc8Ssw(): There is no design to SAT sweep.\n" );
+        return 1;
+    }
+
+    if ( Ntl_ManIsComb(pAbc->pAbc8Ntl) )
+    {
+        fprintf( stdout, "The network is combinational (run \"*fraig\").\n" );
+        return 0;
+    }
+
+    // get the input file name
+    pNtlNew = Ntl_ManScorr( pAbc->pAbc8Ntl, pPars );
+    if ( pNtlNew == NULL )
+    {
+        printf( "Abc_CommandAbc8Scorr(): Tranformation of the AIG has failed.\n" );
+        return 1;
+    }
+
+    Abc_FrameClearDesign(); 
+    pAbc->pAbc8Ntl = pNtlNew;
+    if ( pAbc->pAbc8Ntl == NULL )
+    {
+        printf( "Abc_CommandAbc8Scorr(): Reading BLIF has failed.\n" );
+        return 1;
+    }
+    pAbc->pAbc8Aig = Ntl_ManExtract( pAbc->pAbc8Ntl );
+    if ( pAbc->pAbc8Aig == NULL )
+    {
+        printf( "Abc_CommandAbc8Scorr(): AIG extraction has failed.\n" );
+        return 1;
+    }
+    return 0;
+
+usage:
+    fprintf( stdout, "usage: *scorr [-PQFCLNS <num>] [-plsvh]\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 );
+    fprintf( stdout, "\t-F num : number of time frames for induction (1=simple) [default = %d]\n", pPars->nFramesK );
+    fprintf( stdout, "\t-C num : max number of conflicts at a node (0=inifinite) [default = %d]\n", pPars->nBTLimit );
+    fprintf( stdout, "\t-L num : max number of levels to consider (0=all) [default = %d]\n", pPars->nMaxLevs );
+    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-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-s     : toggle skipping unaffected cones [default = %s]\n", pPars->fSkipCheck? "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;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandAbc8Sweep( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     void * pNtlTemp;
@@ -18956,7 +19150,7 @@ int Abc_CommandAbc8Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
     extern int Fra_FraigCecTop( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int nPartSize, int fSmart, int fVerbose );
 
     // set defaults
-    nConfLimit = 10000;   
+    nConfLimit = 100000;   
     nPartSize  = 100;
     fSmart     = 0;
     fVerbose   = 0;
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index c430137c..37cd6853 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -1084,7 +1084,7 @@ int Abc_NtkPartitionedSat( Abc_Ntk_t * pNtk, int nAlgo, int nPartSize, int nConf
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkDarCec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fPartition, int fVerbose )
+int Abc_NtkDarCec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int fPartition, int fVerbose )
 {
     Aig_Man_t * pMan, * pMan1, * pMan2;
     Abc_Ntk_t * pMiter;
@@ -1102,7 +1102,7 @@ int Abc_NtkDarCec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fPartition, int fVe
     {
         pMan1 = Abc_NtkToDar( pNtk1, 0, 0 );
         pMan2 = Abc_NtkToDar( pNtk2, 0, 0 );
-        RetValue = Fra_FraigCecPartitioned( pMan1, pMan2, 100, 1, fVerbose );
+        RetValue = Fra_FraigCecPartitioned( pMan1, pMan2, nConfLimit, 100, 1, fVerbose );
         Aig_ManStop( pMan1 );
         Aig_ManStop( pMan2 );
         goto finish;
@@ -1152,7 +1152,7 @@ int Abc_NtkDarCec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fPartition, int fVe
         return -1;
     }
     // perform verification
-    RetValue = Fra_FraigCec( &pMan, fVerbose );
+    RetValue = Fra_FraigCec( &pMan, 100000, fVerbose );
     // transfer model if given
     if ( pNtk2 == NULL )
         pNtk1->pModel = pMan->pData, pMan->pData = NULL;
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