Version abc80905

14 files changed, 307 insertions, 121 deletions

diff --git a/src/aig/dch/dchMan.c b/src/aig/dch/dchMan.c
index 6c005fbf..a5faa2a6 100644
--- a/src/aig/dch/dchMan.c
+++ b/src/aig/dch/dchMan.c
@@ -170,16 +170,21 @@ void Dch_ManSatSolverRecycle( Dch_Man_t * p )
     sat_solver_setnvars( p->pSat, 1000 );
     // var 0 is not used
     // var 1 is reserved for const1 node - add the clause
-    Lit = toLit( 1 );
+    p->nSatVars = 1;
+//    p->nSatVars = 0;
+    Lit = toLit( p->nSatVars );
     if ( p->pPars->fPolarFlip )
         Lit = lit_neg( Lit );
     sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
-    p->nSatVars = 2;
+    Dch_ObjSetSatNum( p, Aig_ManConst1(p->pAigFraig), p->nSatVars++ );
+
     p->nRecycles++;
     p->nCallsSince = 0;
 }
 
 
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/dch/dchSimSat.c b/src/aig/dch/dchSimSat.c
index 1fefa6eb..7a6865bd 100644
--- a/src/aig/dch/dchSimSat.c
+++ b/src/aig/dch/dchSimSat.c
@@ -108,8 +108,11 @@ void Dch_ManResimulateSolved_rec( Dch_Man_t * p, Aig_Obj_t * pObj )
     Aig_ObjSetTravIdCurrent(p->pAigTotal, pObj);
     if ( Aig_ObjIsPi(pObj) )
     {
-        Aig_Obj_t * pObjFraig = Dch_ObjFraig( pObj );
-        int nVarNum = Dch_ObjSatNum( p, pObjFraig );
+        Aig_Obj_t * pObjFraig;
+        int nVarNum;
+        pObjFraig = Dch_ObjFraig( pObj );
+        assert( !Aig_IsComplement(pObjFraig) );
+        nVarNum = Dch_ObjSatNum( p, pObjFraig );
         // get the value from the SAT solver
         // (account for the fact that some vars may be minimized away)
         pObj->fMarkB = !nVarNum? 0 : sat_solver_var_value( p->pSat, nVarNum );
diff --git a/src/aig/fra/fraClass.c b/src/aig/fra/fraClass.c
index 498ea758..442cf80e 100644
--- a/src/aig/fra/fraClass.c
+++ b/src/aig/fra/fraClass.c
@@ -296,7 +296,7 @@ void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr, int nMaxLevs )
             if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
                 continue;
             // skip the node with more that the given number of levels
-            if ( nMaxLevs && (int)pObj->Level >= nMaxLevs )
+            if ( nMaxLevs && (int)pObj->Level > nMaxLevs )
                 continue;
         }
         // hash the node by its simulation info
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index 668c20cb..76c7abad 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -505,6 +505,7 @@ PRT( "Time", clock() - clk );
         int nLitsOld = Fra_ClassesCountLits(p->pCla);
         int nImpsOld = p->pCla->vImps? Vec_IntSize(p->pCla->vImps) : 0;
         int nHotsOld = p->vOneHots? Fra_OneHotCount(p, p->vOneHots) : 0;
+        int clk3 = clock();
 
         if ( pParams->TimeLimit != 0.0 && clock() > TimeToStop )
         {
@@ -571,7 +572,7 @@ p->timeTrav += clock() - clk2;
         // report the intermediate results
         if ( pPars->fVerbose )
         {
-            printf( "%3d : Const = %6d. Class = %6d.  L = %6d. LR = %6d.  ", 
+            printf( "%3d : Const = %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 )
@@ -579,7 +580,8 @@ p->timeTrav += clock() - clk2;
             if ( p->pPars->fUse1Hot )
                 printf( "1h = %6d. ", Fra_OneHotCount(p, p->vOneHots) );
             printf( "NR = %6d. ", Aig_ManNodeNum(p->pManFraig) );
-            printf( "\n" );
+            PRT( "T", clock() - clk3 );
+//            printf( "\n" );
         } 
 
         // perform sweeping
diff --git a/src/aig/ivy/ivyFraig.c b/src/aig/ivy/ivyFraig.c
index c306c394..25f7a3ef 100644
--- a/src/aig/ivy/ivyFraig.c
+++ b/src/aig/ivy/ivyFraig.c
@@ -2226,7 +2226,7 @@ p->timeSatFail += clock() - clk;
 int Ivy_FraigNodeIsConst( Ivy_FraigMan_t * p, Ivy_Obj_t * pNew )
 {
     int pLits[2], RetValue1, clk;
-//    int RetValue;
+    int RetValue;
 
     // make sure the nodes are not complemented
     assert( !Ivy_IsComplement(pNew) );
@@ -2261,8 +2261,8 @@ p->timeSat += clock() - clk;
     {
 p->timeSatUnsat += clock() - clk;
         pLits[0] = lit_neg( pLits[0] );
-//        RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 1 );
-//        assert( RetValue );
+        RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 1 );
+        assert( RetValue );
         // continue solving the other implication
         p->nSatCallsUnsat++;
     }
@@ -2533,6 +2533,7 @@ void Ivy_FraigNodeAddToSolver( Ivy_FraigMan_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t *
         Ivy_ObjSetFaninVec( pNode, vFanins );
     }
     Vec_PtrFree( vFrontier );
+    sat_solver_simplify( p->pSat );
 }
 
 /**Function*************************************************************
diff --git a/src/aig/ssw/sswAig.c b/src/aig/ssw/sswAig.c
index 47f15e55..9304edc7 100644
--- a/src/aig/ssw/sswAig.c
+++ b/src/aig/ssw/sswAig.c
@@ -44,7 +44,8 @@ static inline void Ssw_FramesConstrainNode( Ssw_Man_t * p, Aig_Man_t * pFrames,
 {
     Aig_Obj_t * pObjNew, * pObjNew2, * pObjRepr, * pObjReprNew;
     // skip nodes without representative
-    if ( (pObjRepr = Aig_ObjRepr(pAig, pObj)) == NULL )
+    pObjRepr = Aig_ObjRepr(pAig, pObj);
+    if ( pObjRepr == NULL )
         return;
     p->nConstrTotal++;
     assert( pObjRepr->Id < pObj->Id );
@@ -53,16 +54,26 @@ static inline void Ssw_FramesConstrainNode( Ssw_Man_t * p, Aig_Man_t * pFrames,
     // get the new node of the representative
     pObjReprNew = Ssw_ObjFraig( p, pObjRepr, iFrame );
     // if this is the same node, no need to add constraints
-    if ( Aig_Regular(pObjNew) == Aig_Regular(pObjReprNew) )
-        return;
+    if ( pObj->fPhase == pObjRepr->fPhase )
+    {
+        assert( pObjNew != Aig_Not(pObjReprNew) );
+        if ( pObjNew == pObjReprNew )
+            return;
+    }
+    else
+    {
+        assert( pObjNew != pObjReprNew );
+        if ( pObjNew == Aig_Not(pObjReprNew) )
+            return;
+    }
     p->nConstrReduced++;
     // these are different nodes - perform speculative reduction
     pObjNew2 = Aig_NotCond( pObjReprNew, pObj->fPhase ^ pObjRepr->fPhase );
     // set the new node
     Ssw_ObjSetFraig( p, pObj, iFrame, pObjNew2 );
     // add the constraint
-    Aig_ObjCreatePo( pFrames, Aig_Regular(pObjNew) );
-    Aig_ObjCreatePo( pFrames, Aig_Regular(pObjReprNew) );
+    Aig_ObjCreatePo( pFrames, pObjNew2 );
+    Aig_ObjCreatePo( pFrames, pObjNew );
 }
 
 /**Function*************************************************************
@@ -80,7 +91,7 @@ Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p )
 {
     Aig_Man_t * pFrames;
     Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjNew;
-    int i, k, f;
+    int i, f;
     assert( p->pFrames == NULL );
     assert( Aig_ManRegNum(p->pAig) > 0 );
     assert( Aig_ManRegNum(p->pAig) < Aig_ManPiNum(p->pAig) );
@@ -90,18 +101,14 @@ Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p )
     // create latches for the first frame
     Saig_ManForEachLo( p->pAig, pObj, i )
         Ssw_ObjSetFraig( p, pObj, 0, Aig_ObjCreatePi(pFrames) );
-    // create PI nodes for the frames
-    for ( f = 0; f < p->pPars->nFramesK; f++ )
-        Aig_ManForEachPiSeq( p->pAig, pObj, i )
-            Ssw_ObjSetFraig( p, pObj, f, Aig_ObjCreatePi(pFrames) );
-    // map constant nodes
-    for ( f = 0; f < p->pPars->nFramesK; f++ )
-        Ssw_ObjSetFraig( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(pFrames) );
-
     // add timeframes
     p->nConstrTotal = p->nConstrReduced = 0;
     for ( f = 0; f < p->pPars->nFramesK; f++ )
     {
+        // map constants and PIs
+        Ssw_ObjSetFraig( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(pFrames) );
+        Aig_ManForEachPiSeq( p->pAig, pObj, i )
+            Ssw_ObjSetFraig( p, pObj, f, Aig_ObjCreatePi(pFrames) );
         // set the constraints on the latch outputs
         Aig_ManForEachLoSeq( p->pAig, pObj, i )
             Ssw_FramesConstrainNode( p, pFrames, p->pAig, pObj, f );
@@ -113,7 +120,7 @@ Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p )
             Ssw_FramesConstrainNode( p, pFrames, p->pAig, pObj, f );
         }
         // transfer latch input to the latch outputs 
-        Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, k )
+        Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
             Ssw_ObjSetFraig( p, pObjLo, f+1, Ssw_ObjChild0Fra(p, pObjLi,f) );
     }
     // add the POs for the latch outputs of the last frame
@@ -124,6 +131,7 @@ Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p )
     Aig_ManCleanup( pFrames );
     // make sure the satisfying assignment is node assigned
     assert( pFrames->pData == NULL );
+//Aig_ManShow( pFrames, 0, NULL );
     return pFrames;
 }
 
diff --git a/src/aig/ssw/sswClass.c b/src/aig/ssw/sswClass.c
index bf4883e3..c84a5d3d 100644
--- a/src/aig/ssw/sswClass.c
+++ b/src/aig/ssw/sswClass.c
@@ -425,15 +425,15 @@ void Ssw_ClassesPrepare( Ssw_Cla_t * p, int fLatchCorr, int nMaxLevs )
     {
         if ( fLatchCorr )
         {
-            if ( !Aig_ObjIsPi(pObj) )
+            if ( !Saig_ObjIsPi(p->pAig, pObj) )
                 continue;
         }
         else
         {
-            if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
+            if ( !Aig_ObjIsNode(pObj) && !Saig_ObjIsPi(p->pAig, pObj) )
                 continue;
             // skip the node with more that the given number of levels
-            if ( nMaxLevs && (int)pObj->Level >= nMaxLevs )
+            if ( nMaxLevs && (int)pObj->Level > nMaxLevs )
                 continue;
         }
         // check if the node belongs to the class of constant 1
@@ -556,7 +556,7 @@ Ssw_Cla_t * Ssw_ClassesPrepareSimple( Aig_Man_t * pAig, int fLatchCorr, int nMax
     p = Ssw_ClassesStart( pAig );
     // go through the nodes
     p->nCands1 = 0;
-    Aig_ManForEachObj( p->pAig, pObj, i )
+    Aig_ManForEachObj( pAig, pObj, i )
     {
         if ( fLatchCorr )
         {
@@ -568,10 +568,10 @@ Ssw_Cla_t * Ssw_ClassesPrepareSimple( Aig_Man_t * pAig, int fLatchCorr, int nMax
             if ( !Aig_ObjIsNode(pObj) && !Saig_ObjIsLo(pAig, pObj) )
                 continue;
             // skip the node with more that the given number of levels
-            if ( nMaxLevs && (int)pObj->Level >= nMaxLevs )
+            if ( nMaxLevs && (int)pObj->Level > nMaxLevs )
                 continue;
         }
-        Ssw_ObjSetConst1Cand( p->pAig, pObj );
+        Ssw_ObjSetConst1Cand( pAig, pObj );
         p->nCands1++;
     }
     // allocate room for classes
@@ -708,6 +708,53 @@ int Ssw_ClassesRefineConst1Group( Ssw_Cla_t * p, Vec_Ptr_t * vRoots, int fRecurs
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Refine the group of constant 1 nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ssw_ClassesRefineConst1( Ssw_Cla_t * p, int fRecursive )
+{
+    Aig_Obj_t * pObj, * pReprNew, ** ppClassNew;
+    int i;
+    // collect the nodes to be refined
+    Vec_PtrClear( p->vClassNew );
+    for ( i = 0; i < Vec_PtrSize(p->pAig->vObjs); i++ )
+        if ( p->pAig->pReprs[i] == Aig_ManConst1(p->pAig) )
+        {
+            pObj = Aig_ManObj( p->pAig, i );
+            if ( !p->pFuncNodeIsConst( p->pManData, pObj ) )
+                Vec_PtrPush( p->vClassNew, pObj );
+        }
+    // check if there is a new class
+    if ( Vec_PtrSize(p->vClassNew) == 0 )
+        return 0;
+    p->nCands1 -= Vec_PtrSize(p->vClassNew);
+    pReprNew = Vec_PtrEntry( p->vClassNew, 0 );
+    Aig_ObjSetRepr( p->pAig, pReprNew, NULL );
+    if ( Vec_PtrSize(p->vClassNew) == 1 )
+        return 1;
+    // create a new class composed of these nodes
+    ppClassNew = p->pMemClassesFree;
+    p->pMemClassesFree += Vec_PtrSize(p->vClassNew);
+    Vec_PtrForEachEntry( p->vClassNew, pObj, i )
+    {
+        ppClassNew[i] = pObj;
+        Aig_ObjSetRepr( p->pAig, pObj, i? pReprNew : NULL );
+    }
+    Ssw_ObjAddClass( p, pReprNew, ppClassNew, Vec_PtrSize(p->vClassNew) );
+    // refine them recursively
+    if ( fRecursive )
+        return 1 + Ssw_ClassesRefineOneClass( p, pReprNew, 1 );
+    return 1;
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/aig/ssw/sswCore.c b/src/aig/ssw/sswCore.c
index 1e314b78..6c19ab70 100644
--- a/src/aig/ssw/sswCore.c
+++ b/src/aig/ssw/sswCore.c
@@ -48,7 +48,7 @@ void Ssw_ManSetDefaultParams( Ssw_Pars_t * p )
     p->nConstrs       =     0;  // treat the last nConstrs POs as seq constraints
     p->nBTLimit       =  1000;  // conflict limit at a node
     p->fPolarFlip     =     0;  // uses polarity adjustment
-    p->fLatchCorr     =     0;  // performs register correspondence
+    p->fLatchCorr     =     1;  // performs register correspondence
     p->fVerbose       =     1;  // verbose stats
     p->nIters         =     0;  // the number of iterations performed
 }
@@ -66,6 +66,7 @@ void Ssw_ManSetDefaultParams( Ssw_Pars_t * p )
 ***********************************************************************/
 Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
 {
+    Aig_Man_t * pAigNew;
     Ssw_Man_t * p;
     int RetValue, nIter, clk, clkTotal = clock();
     // reset random numbers
@@ -75,27 +76,33 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
     // compute candidate equivalence classes
     p->ppClasses = Ssw_ClassesPrepareSimple( pAig, pPars->fLatchCorr, pPars->nMaxLevs );
     // refine classes using BMC
-    Ssw_ClassesPrint( p->ppClasses, 0 );
+    if ( pPars->fVerbose )
+        Ssw_ClassesPrint( p->ppClasses, 0 );
     Ssw_ManSweepBmc( p );
-    Ssw_ClassesPrint( p->ppClasses, 0 );
+    Ssw_ManCleanup( p );
+    if ( pPars->fVerbose )
+        Ssw_ClassesPrint( p->ppClasses, 0 );
     // refine classes using induction
     for ( nIter = 0; ; nIter++ )
     {
 clk = clock();
-        RetValue = Ssw_ManSweep(p);
+        RetValue = Ssw_ManSweep( p );
         if ( pPars->fVerbose )
         {
-            printf( "%3d : Const = %6d. Class = %6d.  L = %6d. LR = %6d.  NR = %6d. ", 
+            printf( "%3d : Const = %6d. Cl = %6d.  L = %6d. LR = %6d.  NR = %6d. ", 
                 nIter, Ssw_ClassesCand1Num(p->ppClasses), Ssw_ClassesClassNum(p->ppClasses), 
-                p->nConstrTotal, p->nConstrReduced, p->nFrameNodes );
+                p->nConstrTotal, p->nConstrReduced, Aig_ManNodeNum(p->pFrames) );
             PRT( "T", clock() - clk );
         } 
+        Ssw_ManCleanup( p );
         if ( !RetValue )
             break;
-    }
+    } 
 p->timeTotal = clock() - clkTotal;
     Ssw_ManStop( p );
-    return Aig_ManDupRepr( pAig, 0 );
+    pAigNew = Aig_ManDupRepr( pAig, 0 );
+    Aig_ManSeqCleanup( pAigNew );
+    return pAigNew;
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/ssw/sswInt.h b/src/aig/ssw/sswInt.h
index 0e54af32..21621c0d 100644
--- a/src/aig/ssw/sswInt.h
+++ b/src/aig/ssw/sswInt.h
@@ -55,7 +55,6 @@ struct Ssw_Man_t_
     Aig_Man_t *      pAig;           // user-given AIG
     Aig_Man_t *      pFrames;        // final AIG
     Aig_Obj_t **     pNodeToFraig;   // mapping of AIG nodes into FRAIG nodes
-    int              nFrameNodes;    // the number of nodes in the timeframes
     // equivalence classes
     Ssw_Cla_t *      ppClasses;      // equivalence classes of nodes
 //    Aig_Obj_t **     pReprsProved;   // equivalences proved
@@ -70,6 +69,7 @@ struct Ssw_Man_t_
     // constraints
     int              nConstrTotal;   // the number of total constraints
     int              nConstrReduced; // the number of reduced constraints
+    int              nStragers;
     // SAT calls statistics
     int              nSatCalls;      // the number of SAT calls
     int              nSatProof;      // the number of proofs
@@ -136,6 +136,7 @@ extern Ssw_Cla_t *   Ssw_ClassesPrepareSimple( Aig_Man_t * pAig, int fLatchCorr,
 extern int           Ssw_ClassesRefine( Ssw_Cla_t * p );
 extern int           Ssw_ClassesRefineOneClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, int fRecursive );
 extern int           Ssw_ClassesRefineConst1Group( Ssw_Cla_t * p, Vec_Ptr_t * vRoots, int fRecursive );
+extern int           Ssw_ClassesRefineConst1( Ssw_Cla_t * p, int fRecursive );
 /*=== sswCnf.c ===================================================*/
 extern void          Ssw_CnfNodeAddToSolver( Ssw_Man_t * p, Aig_Obj_t * pObj );
 /*=== sswMan.c ===================================================*/
@@ -148,6 +149,7 @@ extern int           Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj
 extern int           Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
 /*=== sswSimSat.c ===================================================*/
 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 );
 /*=== sswSweep.c ===================================================*/
 extern int           Ssw_ManSweepBmc( Ssw_Man_t * p );
 extern int           Ssw_ManSweep( Ssw_Man_t * p );
diff --git a/src/aig/ssw/sswMan.c b/src/aig/ssw/sswMan.c
index 86144ebb..0b935daa 100644
--- a/src/aig/ssw/sswMan.c
+++ b/src/aig/ssw/sswMan.c
@@ -42,22 +42,25 @@
 Ssw_Man_t * Ssw_ManCreate( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
 {
     Ssw_Man_t * p;
+    // prepare the sequential AIG
+    assert( Saig_ManRegNum(pAig) > 0 );
+    Aig_ManFanoutStart( pAig );
+    Aig_ManSetPioNumbers( pAig );
     // create interpolation manager
     p = ALLOC( Ssw_Man_t, 1 );
     memset( p, 0, sizeof(Ssw_Man_t) );
     p->pPars        = pPars;
     p->pAig         = pAig;
     p->nFrames      = pPars->nFramesK + 1;
-    Aig_ManFanoutStart( pAig );
+    p->pNodeToFraig = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) * p->nFrames );
     // SAT solving
     p->nSatVars     = 1;
-    p->pSatVars     = CALLOC( int, Aig_ManObjNumMax(p->pAig) );
+    p->pSatVars     = CALLOC( int, Aig_ManObjNumMax(p->pAig) * p->nFrames );
     p->vFanins      = Vec_PtrAlloc( 100 );
     p->vSimRoots    = Vec_PtrAlloc( 1000 );
     p->vSimClasses  = Vec_PtrAlloc( 1000 );
     // equivalences proved
 //    p->pReprsProved = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) );
-    p->pNodeToFraig = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) * p->nFrames );
     return p;
 }
 
@@ -97,21 +100,19 @@ void Ssw_ManPrintStats( Ssw_Man_t * p )
 {
     printf( "Parameters: Frames = %d. Conf limit = %d. Constrs = %d.\n", 
         p->pPars->nFramesK, p->pPars->nBTLimit, p->pPars->nConstrs );
-    printf( "AIG       : PI = %d. PO = %d. Latch = %d. Node = %d.\n", 
-        Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), Saig_ManRegNum(p->pAig), Aig_ManNodeNum(p->pAig) );
-    printf( "SAT solver: Vars = %d.\n", p->nSatVars );
-    printf( "SAT calls : All = %6d. Unsat = %6d. Sat = %6d. Fail = %6d.\n", 
+    printf( "AIG       : PI = %d. PO = %d. Latch = %d. Node = %d.  SAT vars = %d.\n", 
+        Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), Saig_ManRegNum(p->pAig), Aig_ManNodeNum(p->pAig), p->nSatVars );
+    printf( "SAT calls : All = %6d. Unsat = %6d. Sat = %6d. Fail = %6d.  Equivs = %d. Str = %d.\n", 
         p->nSatCalls, p->nSatCalls-p->nSatCallsSat-p->nSatFailsReal, 
-        p->nSatCallsSat, p->nSatFailsReal );
-    printf( "Equivs    : All = %6d.\n", Ssw_ManCountEquivs(p) );
+        p->nSatCallsSat, p->nSatFailsReal, Ssw_ManCountEquivs(p), p->nStragers );
     printf( "Runtime statistics:\n" );
     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( "  sat      ", p->timeSatSat,   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 );
@@ -135,14 +136,15 @@ void Ssw_ManCleanup( Ssw_Man_t * p )
     {
         Aig_ManStop( p->pFrames );
         p->pFrames = NULL;
+        memset( p->pNodeToFraig, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p->pAig) * p->nFrames );
     }
     if ( p->pSat )
     {
         sat_solver_delete( p->pSat );
         p->pSat = NULL;
-        p->nSatVars = 0;
+//        p->nSatVars = 0;
+        memset( p->pSatVars, 0, sizeof(int) * Aig_ManObjNumMax(p->pAig) * p->nFrames );
     }
-    memset( p->pNodeToFraig, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p->pAig) * p->nFrames );
     p->nConstrTotal = 0;
     p->nConstrReduced = 0;
 }
@@ -192,11 +194,12 @@ void Ssw_ManStartSolver( Ssw_Man_t * p )
     sat_solver_setnvars( p->pSat, 10000 );
     // var 0 is not used
     // var 1 is reserved for const1 node - add the clause
-    Lit = toLit( 1 );
+    p->nSatVars = 1;
+    Lit = toLit( p->nSatVars );
     if ( p->pPars->fPolarFlip )
         Lit = lit_neg( Lit );
     sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
-    p->nSatVars = 2;
+    Ssw_ObjSetSatNum( p, Aig_ManConst1(p->pAig), p->nSatVars++ );
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/ssw/sswSat.c b/src/aig/ssw/sswSat.c
index 06abd2c9..90752baa 100644
--- a/src/aig/ssw/sswSat.c
+++ b/src/aig/ssw/sswSat.c
@@ -32,7 +32,7 @@
 
   Synopsis    [Runs equivalence test for the two nodes.]
 
-  Description []
+  Description [Both nodes should be regular and different from each other.]
                
   SideEffects []
 
@@ -42,13 +42,13 @@
 int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
 {
     int nBTLimit = p->pPars->nBTLimit;
-    int pLits[2], RetValue, RetValue1, status, clk;
+    int pLits[2], RetValue, RetValue1, clk;//, status;
     p->nSatCalls++;
 
     // sanity checks
-    assert( !Aig_IsComplement(pNew) );
     assert( !Aig_IsComplement(pOld) );
-    assert( pNew != pOld );
+    assert( !Aig_IsComplement(pNew) );
+    assert( pOld != pNew );
 
     if ( p->pSat == NULL )
         Ssw_ManStartSolver( p );
@@ -57,14 +57,6 @@ int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
     Ssw_CnfNodeAddToSolver( p, pOld );
     Ssw_CnfNodeAddToSolver( p, pNew );
 
-    // propagate unit clauses
-    if ( p->pSat->qtail != p->pSat->qhead )
-    {
-        status = sat_solver_simplify(p->pSat);
-        assert( status != 0 );
-        assert( p->pSat->qtail == p->pSat->qhead );
-    }
-
     // solve under assumptions
     // A = 1; B = 0     OR     A = 1; B = 1 
     pLits[0] = toLitCond( Ssw_ObjSatNum(p,pOld), 0 );
@@ -75,6 +67,10 @@ int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
         if ( pNew->fPhase )  pLits[1] = lit_neg( pLits[1] );
     }
 //Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
+
+    RetValue = sat_solver_simplify(p->pSat);
+    assert( RetValue != 0 );
+
 clk = clock();
     RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, 
         (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
@@ -117,6 +113,10 @@ p->timeSatUndec += clock() - clk;
         if ( pOld->fPhase )  pLits[0] = lit_neg( pLits[0] );
         if ( pNew->fPhase )  pLits[1] = lit_neg( pLits[1] );
     }
+
+    RetValue = sat_solver_simplify(p->pSat);
+    assert( RetValue != 0 );
+
 clk = clock();
     RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, 
         (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
@@ -160,23 +160,45 @@ p->timeSatUndec += clock() - clk;
 ***********************************************************************/
 int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
 {
-    int pLits[2], RetValue;
+    int pLits[2], RetValue, fComplNew;
+    Aig_Obj_t * pTemp;
 
     // sanity checks
-    assert( !Aig_IsComplement(pNew) );
-    assert( !Aig_IsComplement(pOld) );
-    assert( pNew != pOld );
+    assert( Aig_Regular(pOld) != Aig_Regular(pNew) );
 
+    // move constant to the old node
+    if ( Aig_Regular(pNew) == Aig_ManConst1(p->pFrames) )
+    {
+        assert( Aig_Regular(pOld) != Aig_ManConst1(p->pFrames) );
+        pTemp = pOld;
+        pOld  = pNew;
+        pNew  = pTemp;
+    }
+
+    // move complement to the new node
+    if ( Aig_IsComplement(pOld) )
+    {
+        pOld = Aig_Regular(pOld);
+        pNew = Aig_Not(pNew);
+    }
+
+    // start the solver
     if ( p->pSat == NULL )
         Ssw_ManStartSolver( p );
 
     // if the nodes do not have SAT variables, allocate them
     Ssw_CnfNodeAddToSolver( p, pOld );
-    Ssw_CnfNodeAddToSolver( p, pNew );
+    Ssw_CnfNodeAddToSolver( p, Aig_Regular(pNew) );
+
+    // transform the new node
+    fComplNew = Aig_IsComplement( pNew );
+    pNew = Aig_Regular( pNew );
 
+    // consider the constant 1 case
     if ( pOld == Aig_ManConst1(p->pFrames) )
     {
-        pLits[0] = toLitCond( Ssw_ObjSatNum(p,pOld), !pNew->fPhase );
+        // add constaint A = 1  ---->  A
+        pLits[0] = toLitCond( Ssw_ObjSatNum(p,pNew), fComplNew );
         if ( p->pPars->fPolarFlip )
         {
             if ( pNew->fPhase )  pLits[0] = lit_neg( pLits[0] );
@@ -186,10 +208,11 @@ int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
     }
     else
     {
-        // solve under assumptions
-        // A = 1; B = 0     OR     A = 1; B = 1 
+        // add constaint A = B  ---->  (A v !B)(!A v B)
+
+        // (A v !B)
         pLits[0] = toLitCond( Ssw_ObjSatNum(p,pOld), 0 );
-        pLits[1] = toLitCond( Ssw_ObjSatNum(p,pNew), pOld->fPhase == pNew->fPhase );
+        pLits[1] = toLitCond( Ssw_ObjSatNum(p,pNew), !fComplNew );
         if ( p->pPars->fPolarFlip )
         {
             if ( pOld->fPhase )  pLits[0] = lit_neg( pLits[0] );
@@ -200,10 +223,9 @@ int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
         RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
         assert( RetValue );
 
-        // solve under assumptions
-        // A = 0; B = 1     OR     A = 0; B = 0 
+        // (!A v B)
         pLits[0] = toLitCond( Ssw_ObjSatNum(p,pOld), 1 );
-        pLits[1] = toLitCond( Ssw_ObjSatNum(p,pNew), pOld->fPhase ^ pNew->fPhase );
+        pLits[1] = toLitCond( Ssw_ObjSatNum(p,pNew), fComplNew);
         if ( p->pPars->fPolarFlip )
         {
             if ( pOld->fPhase )  pLits[0] = lit_neg( pLits[0] );
@@ -214,16 +236,6 @@ int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
         RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
         assert( RetValue );
     }
-/*
-    // propagate unit clauses
-    if ( p->pSat->qtail != p->pSat->qhead )
-    {
-        int status;
-        status = sat_solver_simplify(p->pSat);
-        assert( status != 0 );
-        assert( p->pSat->qtail == p->pSat->qhead );
-    }
-*/
     return 1;
 }
 
diff --git a/src/aig/ssw/sswSimSat.c b/src/aig/ssw/sswSimSat.c
index 5986c27a..868a016b 100644
--- a/src/aig/ssw/sswSimSat.c
+++ b/src/aig/ssw/sswSimSat.c
@@ -92,6 +92,32 @@ void Ssw_ManCollectTfoCands( Ssw_Man_t * p, Aig_Obj_t * pObj1, Aig_Obj_t * pObj2
 
 /**Function*************************************************************
 
+  Synopsis    [Retrives value of the PI in the original AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ssw_ManOriginalPiValue( Ssw_Man_t * p, Aig_Obj_t * pObj, int f )
+{
+    Aig_Obj_t * pObjFraig;
+    int nVarNum, Value;
+    assert( Aig_ObjIsPi(pObj) );
+    pObjFraig = Ssw_ObjFraig( p, pObj, f );
+    nVarNum = Ssw_ObjSatNum( p, Aig_Regular(pObjFraig) );
+    Value = (!nVarNum)? 0 : (Aig_IsComplement(pObjFraig) ^ sat_solver_var_value( p->pSat, nVarNum ));
+    if ( p->pPars->fPolarFlip )
+    {
+        if ( Aig_Regular(pObjFraig)->fPhase )  Value ^= 1;
+    }
+    return Value;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Resimulates the cone of influence of the solved nodes.]
 
   Description []
@@ -108,11 +134,7 @@ void Ssw_ManResimulateSolved_rec( Ssw_Man_t * p, Aig_Obj_t * pObj, int f )
     Aig_ObjSetTravIdCurrent(p->pAig, pObj);
     if ( Aig_ObjIsPi(pObj) )
     {
-        Aig_Obj_t * pObjFraig = Ssw_ObjFraig( p, pObj, f );
-        int nVarNum = Ssw_ObjSatNum( p, pObjFraig );
-        // get the value from the SAT solver
-        // (account for the fact that some vars may be minimized away)
-        pObj->fMarkB = !nVarNum? 0 : sat_solver_var_value( p->pSat, nVarNum );
+        pObj->fMarkB = Ssw_ManOriginalPiValue( p, pObj, f );
         return;
     }
     Ssw_ManResimulateSolved_rec( p, Aig_ObjFanin0(pObj), f );
@@ -194,6 +216,40 @@ void Ssw_ManResimulateCex( Ssw_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr, i
 p->timeSimSat += clock() - clk;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Handle the counter-example.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_ManResimulateCexTotal( Ssw_Man_t * p, Aig_Obj_t * pCand, Aig_Obj_t * pRepr, int f )
+{
+    Aig_Obj_t * pObj;
+    int i, RetValue1, RetValue2, clk = clock();
+    // set the PI simulation information
+    Aig_ManConst1(p->pAig)->fMarkB = 1;
+    Aig_ManForEachPi( p->pAig, pObj, i )
+        pObj->fMarkB = Ssw_ManOriginalPiValue( p, pObj, f );
+    // simulate internal nodes
+    Aig_ManForEachNode( p->pAig, pObj, i )
+        pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) )
+                     & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) );
+    // check equivalence classes
+    RetValue1 = Ssw_ClassesRefineConst1( p->ppClasses, 0 );
+    RetValue2 = Ssw_ClassesRefine( p->ppClasses );
+    // make sure refinement happened
+    if ( Aig_ObjIsConst1(pRepr) )
+        assert( RetValue1 );
+    else
+        assert( RetValue2 );
+p->timeSimSat += clock() - clk;
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/aig/ssw/sswSweep.c b/src/aig/ssw/sswSweep.c
index 18796b20..0630de56 100644
--- a/src/aig/ssw/sswSweep.c
+++ b/src/aig/ssw/sswSweep.c
@@ -50,12 +50,33 @@ void Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f )
         return;
     // get the fraiged node
     pObjFraig = Ssw_ObjFraig( p, pObj, f );
-    if ( pObjFraig == NULL )
-        return;
+    assert( pObjFraig != NULL );
     // get the fraiged representative
     pObjReprFraig = Ssw_ObjFraig( p, pObjRepr, f );
-    if ( pObjReprFraig == NULL )
+    assert( pObjReprFraig != NULL );
+    // check if constant 0 pattern distinquishes these nodes
+    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->nStragers++;
         return;
+    }
     // if the fraiged nodes are the same, return
     if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) )
     {
@@ -63,10 +84,15 @@ void Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f )
 //        p->pReprsProved[ pObj->Id ] = pObjRepr;
         return;
     }
-    assert( Aig_Regular(pObjFraig) != Aig_ManConst1(p->pFrames) );
-    RetValue = Ssw_NodesAreEquiv( p, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) );
+//    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;
@@ -80,7 +106,8 @@ void Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f )
         return;
     }
     // disproved the equivalence
-    Ssw_ManResimulateCex( p, pObj, pObjRepr, f );
+//    Ssw_ManResimulateCex( p, pObj, pObjRepr, f );
+    Ssw_ManResimulateCexTotal( p, pObj, pObjRepr, f );
     assert( Aig_ObjRepr( p->pAig, pObj ) != pObjRepr );
     p->fRefined = 1;
 }
@@ -110,7 +137,8 @@ clk = clock();
 
     // sweep internal nodes
     p->fRefined = 0;
-    pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) * p->pPars->nFramesK );
+    if ( p->pPars->fVerbose )
+        pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) * p->pPars->nFramesK );
     for ( f = 0; f < p->pPars->nFramesK; f++ )
     {
         // map constants and PIs
@@ -120,17 +148,18 @@ clk = clock();
         // sweep internal nodes
         Aig_ManForEachNode( p->pAig, pObj, i )
         {
-            Bar_ProgressUpdate( pProgress, Aig_ManObjNumMax(p->pAig) * f + i, NULL );
+            if ( p->pPars->fVerbose )
+                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 );
         }
     }
-    Bar_ProgressStop( pProgress );
+    if ( p->pPars->fVerbose )
+        Bar_ProgressStop( pProgress );
 
     // cleanup
-    Ssw_ClassesCheck( p->ppClasses );
-    Ssw_ManCleanup( p );
+//    Ssw_ClassesCheck( p->ppClasses );
 p->timeBmc += clock() - clk;
     return p->fRefined;
 }
@@ -150,21 +179,21 @@ int Ssw_ManSweep( Ssw_Man_t * p )
 {
     Bar_Progress_t * pProgress = NULL;
     Aig_Obj_t * pObj, * pObj2, * pObjNew;
-    int nConstrPairs, clk, i, f = p->pPars->nFramesK;
+    int nConstrPairs, clk, i, f;
 
     // perform speculative reduction
 clk = clock();
     // create timeframes
     p->pFrames = Ssw_FramesWithClasses( p );
-    p->nFrameNodes = Aig_ManNodeNum( p->pFrames );
     // add constraints
+    Ssw_ManStartSolver( p );
     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 );
-        Ssw_NodesAreConstrained( p, Aig_ObjFanin0(pObj), Aig_ObjFanin0(pObj2) );
+        Ssw_NodesAreConstrained( p, Aig_ObjChild0(pObj), Aig_ObjChild0(pObj2) );
     }
     // build logic cones for register inputs
     for ( i = 0; i < Aig_ManRegNum(p->pAig); i++ )
@@ -175,25 +204,36 @@ clk = clock();
     sat_solver_simplify( p->pSat );
 p->timeReduce += clock() - clk;
 
-    // map constants and PIs
+    // map constants and PIs of the last frame
+    f = p->pPars->nFramesK;
     Ssw_ObjSetFraig( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
     Saig_ManForEachPi( p->pAig, pObj, i )
         Ssw_ObjSetFraig( p, pObj, f, Aig_ObjCreatePi(p->pFrames) );
+    // make sure LOs are assigned
+    Saig_ManForEachLo( p->pAig, pObj, i )
+        assert( Ssw_ObjFraig( p, pObj, f ) != NULL );
     // sweep internal nodes
     p->fRefined = 0;
-    pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) );
-    Aig_ManForEachNode( p->pAig, pObj, i )
+    if ( p->pPars->fVerbose )
+        pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) );
+    Aig_ManForEachObj( p->pAig, pObj, i )
     {
-        Bar_ProgressUpdate( pProgress, 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 );
+        if ( p->pPars->fVerbose )
+            Bar_ProgressUpdate( pProgress, i, NULL );
+        if ( Saig_ObjIsLo(p->pAig, pObj) )
+            Ssw_ManSweepNode( p, pObj, f );
+        else if ( Aig_ObjIsNode(pObj) )
+        {
+            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 );
+        }
     }
-    Bar_ProgressStop( pProgress );
+    if ( p->pPars->fVerbose )
+        Bar_ProgressStop( pProgress );
 
     // cleanup
-    Ssw_ClassesCheck( p->ppClasses );
-    Ssw_ManCleanup( p );
+//    Ssw_ClassesCheck( p->ppClasses );
     return p->fRefined;
 }
 
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 90ee04b2..8df6f066 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -453,8 +453,8 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Sequential",   "fretime",       Abc_CommandFlowRetime,       1 );
 //    Cmd_CommandAdd( pAbc, "Sequential",   "sfpga",         Abc_CommandSeqFpga,          1 );
 //    Cmd_CommandAdd( pAbc, "Sequential",   "smap",          Abc_CommandSeqMap,           1 );
-    Cmd_CommandAdd( pAbc, "Sequential",   "ssw",           Abc_CommandSeqSweep,         1 );
-    Cmd_CommandAdd( pAbc, "Sequential",   "ssw2",          Abc_CommandSeqSweep2,        1 );
+    Cmd_CommandAdd( pAbc, "Sequential",   "ssweep",        Abc_CommandSeqSweep,         1 );
+    Cmd_CommandAdd( pAbc, "Sequential",   "scorr",         Abc_CommandSeqSweep2,        1 );
     Cmd_CommandAdd( pAbc, "Sequential",   "testssw",       Abc_CommandSeqSweepTest,     0 );
     Cmd_CommandAdd( pAbc, "Sequential",   "lcorr",         Abc_CommandLcorr,            1 );
     Cmd_CommandAdd( pAbc, "Sequential",   "scleanup",      Abc_CommandSeqCleanup,       1 );
@@ -13482,7 +13482,7 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: ssw [-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 );
@@ -13655,7 +13655,7 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: ssw2 [-PQFCLN num] [-plvh]\n" );
+    fprintf( pErr, "usage: scorr [-PQFCLN num] [-plvh]\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 );