Version abc80901

23 files changed, 2759 insertions, 14 deletions

diff --git a/abc.dsp b/abc.dsp
index 2f89110f..eabac8d2 100644
--- a/abc.dsp
+++ b/abc.dsp
@@ -42,7 +42,7 @@ RSC=rc.exe
 # PROP Ignore_Export_Lib 0
 # PROP Target_Dir ""
 # ADD BASE CPP /nologo /W3 /GX /O2 /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /c
-# ADD CPP /nologo /W3 /GX /O2 /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/misc/bzlib" /I "src/misc/zlib" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/sat/nsat" /I "src/sat/psat" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/nwk" /I "src/aig/tim" /I "src/opt/mfs" /I "src/aig/mfx" /I "src/aig/saig" /I "src/aig/bbr" /I "src/aig/int" /I "src/aig/dch" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D ABC_DLL=DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /D "ABC_USE_LIBRARIES" /FR /YX /FD /c
+# ADD CPP /nologo /W3 /GX /O2 /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/misc/bzlib" /I "src/misc/zlib" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/sat/nsat" /I "src/sat/psat" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/nwk" /I "src/aig/tim" /I "src/opt/mfs" /I "src/aig/mfx" /I "src/aig/saig" /I "src/aig/bbr" /I "src/aig/int" /I "src/aig/dch" /I "src/aig/ssw" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D ABC_DLL=DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /D "ABC_USE_LIBRARIES" /FR /YX /FD /c
 # ADD BASE RSC /l 0x409 /d "NDEBUG"
 # ADD RSC /l 0x409 /d "NDEBUG"
 BSC32=bscmake.exe
@@ -66,7 +66,7 @@ LINK32=link.exe
 # PROP Ignore_Export_Lib 0
 # PROP Target_Dir ""
 # ADD BASE CPP /nologo /W3 /Gm /GX /ZI /Od /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /GZ /c
-# ADD CPP /nologo /W3 /Gm /GX /ZI /Od /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/misc/bzlib" /I "src/misc/zlib" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/sat/nsat" /I "src/sat/psat" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/nwk" /I "src/aig/tim" /I "src/opt/mfs" /I "src/aig/mfx" /I "src/aig/saig" /I "src/aig/bbr" /I "src/aig/int" /I "src/aig/dch" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D ABC_DLL=DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /D "ABC_USE_LIBRARIES" /FR /YX /FD /GZ /c
+# ADD CPP /nologo /W3 /Gm /GX /ZI /Od /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/misc/bzlib" /I "src/misc/zlib" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/sat/nsat" /I "src/sat/psat" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/nwk" /I "src/aig/tim" /I "src/opt/mfs" /I "src/aig/mfx" /I "src/aig/saig" /I "src/aig/bbr" /I "src/aig/int" /I "src/aig/dch" /I "src/aig/ssw" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D ABC_DLL=DLLEXPORT /D "_CRT_SECURE_NO_DEPRECATE" /D "ABC_USE_LIBRARIES" /FR /YX /FD /GZ /c
 # SUBTRACT CPP /X
 # ADD BASE RSC /l 0x409 /d "_DEBUG"
 # ADD RSC /l 0x409 /d "_DEBUG"
@@ -1956,10 +1956,90 @@ SOURCE=.\src\map\if\ifUtil.c
 # Begin Group "pcm"
 
 # PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\map\pcm\pcmCore.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\pcm\pcmCut.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\pcm\pcmInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\pcm\pcmMan.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\pcm\pcmMap.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\pcm\pcmReduce.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\pcm\pcmTime.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\pcm\pcmTruth.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\pcm\pcmUtil.c
+# End Source File
 # End Group
 # Begin Group "ply"
 
 # PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\map\ply\ply.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\ply\plyAbc.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\ply\plyAig.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\ply\plyInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\ply\plyIter.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\ply\plyLib.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\ply\plyMan.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\ply\plyMap.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\ply\plyNtk.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\ply\plyPair.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\map\ply\plyPar.c
+# End Source File
 # End Group
 # End Group
 # Begin Group "misc"
@@ -3325,6 +3405,50 @@ SOURCE=.\src\aig\dch\dchSimSat.c
 SOURCE=.\src\aig\dch\dchSweep.c
 # End Source File
 # End Group
+# Begin Group "ssw"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\aig\ssw\ssw.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\ssw\sswAig.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\ssw\sswClass.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\ssw\sswCnf.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\ssw\sswCore.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\ssw\sswInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\ssw\sswMan.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\ssw\sswSat.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\ssw\sswSimSat.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\ssw\sswSweep.c
+# End Source File
+# End Group
 # End Group
 # End Group
 # Begin Group "Header Files"
diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index baba9707..03c05420 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -626,6 +626,7 @@ extern int             Aig_ObjIsMuxType( Aig_Obj_t * pObj );
 extern int             Aig_ObjRecognizeExor( Aig_Obj_t * pObj, Aig_Obj_t ** ppFan0, Aig_Obj_t ** ppFan1 );
 extern Aig_Obj_t *     Aig_ObjRecognizeMux( Aig_Obj_t * pObj, Aig_Obj_t ** ppObjT, Aig_Obj_t ** ppObjE );
 extern Aig_Obj_t *     Aig_ObjReal_rec( Aig_Obj_t * pObj );
+extern int             Aig_ObjCompareIdIncrease( Aig_Obj_t ** pp1, Aig_Obj_t ** pp2 );
 extern void            Aig_ObjPrintEqn( FILE * pFile, Aig_Obj_t * pObj, Vec_Vec_t * vLevels, int Level );
 extern void            Aig_ObjPrintVerilog( FILE * pFile, Aig_Obj_t * pObj, Vec_Vec_t * vLevels, int Level );
 extern void            Aig_ObjPrintVerbose( Aig_Obj_t * pObj, int fHaig );
diff --git a/src/aig/aig/aigUtil.c b/src/aig/aig/aigUtil.c
index 2aca98ac..fd5fedcc 100644
--- a/src/aig/aig/aigUtil.c
+++ b/src/aig/aig/aigUtil.c
@@ -438,6 +438,27 @@ Aig_Obj_t * Aig_ObjReal_rec( Aig_Obj_t * pObj )
     return Aig_NotCond( pObjNew, Aig_IsComplement(pObj) );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Procedure used for sorting the nodes in increasing order of IDs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_ObjCompareIdIncrease( Aig_Obj_t ** pp1, Aig_Obj_t ** pp2 )
+{
+    int Diff = Aig_ObjId(*pp1) - Aig_ObjId(*pp2);
+    if ( Diff < 0 )
+        return -1;
+    if ( Diff > 0 ) 
+        return 1;
+    return 0; 
+}
+
 
 /**Function*************************************************************
 
diff --git a/src/aig/dch/dchChoice.c b/src/aig/dch/dchChoice.c
index ee1ce034..19689051 100644
--- a/src/aig/dch/dchChoice.c
+++ b/src/aig/dch/dchChoice.c
@@ -89,7 +89,7 @@ int Dch_DeriveChoiceCountEquivs( Aig_Man_t * pAig )
             nEquivs++;
         }
     }
-    printf( "Removed %d classes.\n", Counter );
+//    printf( "Removed %d classes.\n", Counter );
 
     if ( Counter )
         Dch_DeriveChoiceCountEquivs( pAig );
diff --git a/src/aig/dch/dchClass.c b/src/aig/dch/dchClass.c
index ab306ca9..5d042847 100644
--- a/src/aig/dch/dchClass.c
+++ b/src/aig/dch/dchClass.c
@@ -48,7 +48,7 @@ struct Dch_Cla_t_
     Vec_Ptr_t *      vClassNew;        // new equivalence class(es) after splitting
     // procedures used for class refinement
     void *           pManData;
-    unsigned (*pFuncNodeHash) (void *,Aig_Obj_t *);              // returns has key of the node
+    unsigned (*pFuncNodeHash) (void *,Aig_Obj_t *);              // returns hash key of the node
     int (*pFuncNodeIsConst)   (void *,Aig_Obj_t *);              // returns 1 if the node is a constant
     int (*pFuncNodesAreEqual) (void *,Aig_Obj_t *, Aig_Obj_t *); // returns 1 if nodes are equal up to a complement
 };
@@ -158,7 +158,7 @@ Dch_Cla_t * Dch_ClassesStart( Aig_Man_t * pAig )
 
 ***********************************************************************/
 void Dch_ClassesSetData( Dch_Cla_t * p, void * pManData, 
-    unsigned (*pFuncNodeHash)(void *,Aig_Obj_t *),               // returns has key of the node
+    unsigned (*pFuncNodeHash)(void *,Aig_Obj_t *),               // returns hash key of the node
     int (*pFuncNodeIsConst)(void *,Aig_Obj_t *),                 // returns 1 if the node is a constant
     int (*pFuncNodesAreEqual)(void *,Aig_Obj_t *, Aig_Obj_t *) ) // returns 1 if nodes are equal up to a complement
 {
@@ -481,7 +481,7 @@ int Dch_ClassesRefineOneClass( Dch_Cla_t * p, Aig_Obj_t * pReprOld, int fRecursi
     if ( Vec_PtrSize(p->vClassNew) > 1 )
         Dch_ObjAddClass( p, pReprNew, pClassNew, Vec_PtrSize(p->vClassNew) );
 
-    // skip of the class should not be recursively refined
+    // check if the class should be recursively refined
     if ( fRecursive && Vec_PtrSize(p->vClassNew) > 1 )
         return 1 + Dch_ClassesRefineOneClass( p, pReprNew, 1 );
     return 1;
@@ -568,6 +568,8 @@ int Dch_ClassesRefineConst1Group( Dch_Cla_t * p, Vec_Ptr_t * vRoots, int fRecurs
 {
     Aig_Obj_t * pObj, * pReprNew, ** ppClassNew;
     int i;
+    if ( Vec_PtrSize(vRoots) == 0 )
+        return 0;
     // collect the nodes to be refined
     Vec_PtrClear( p->vClassNew );
     Vec_PtrForEachEntry( vRoots, pObj, i )
diff --git a/src/aig/dch/dchMan.c b/src/aig/dch/dchMan.c
index 02d91ca3..6c005fbf 100644
--- a/src/aig/dch/dchMan.c
+++ b/src/aig/dch/dchMan.c
@@ -4,7 +4,7 @@
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
-  PackageName [Computation of equivalence classes using simulation.]
+  PackageName [Choice computation for tech-mapping.]
 
   Synopsis    [Calls to the SAT solver.]
 
@@ -168,12 +168,13 @@ void Dch_ManSatSolverRecycle( Dch_Man_t * p )
     }
     p->pSat = sat_solver_new();
     sat_solver_setnvars( p->pSat, 1000 );
-    // var 0 is reserved for const1 node - add the clause
-    Lit = toLit( 0 );
+    // var 0 is not used
+    // var 1 is reserved for const1 node - add the clause
+    Lit = toLit( 1 );
     if ( p->pPars->fPolarFlip )
         Lit = lit_neg( Lit );
     sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
-    p->nSatVars = 1;
+    p->nSatVars = 2;
     p->nRecycles++;
     p->nCallsSince = 0;
 }
diff --git a/src/aig/dch/dchSim.c b/src/aig/dch/dchSim.c
index 49734b5a..44a96970 100644
--- a/src/aig/dch/dchSim.c
+++ b/src/aig/dch/dchSim.c
@@ -4,7 +4,7 @@
 
   SystemName  [ABC: Logic synthesis and verification system.]
 
-  PackageName [Computation of equivalence classes using simulation.]
+  PackageName [Choice computation for tech-mapping.]
 
   Synopsis    [Performs random simulation at the beginning.]
 
diff --git a/src/aig/dch/dchSimSat.c b/src/aig/dch/dchSimSat.c
index cdfb9271..1fefa6eb 100644
--- a/src/aig/dch/dchSimSat.c
+++ b/src/aig/dch/dchSimSat.c
@@ -86,6 +86,8 @@ void Dch_ManCollectTfoCands( Dch_Man_t * p, Aig_Obj_t * pObj1, Aig_Obj_t * pObj2
     Aig_ObjSetTravIdCurrent( p->pAigTotal, Aig_ManConst1(p->pAigTotal) );    
     Dch_ManCollectTfoCands_rec( p, pObj1 );
     Dch_ManCollectTfoCands_rec( p, pObj2 );
+    Vec_PtrSort( p->vSimRoots, Aig_ObjCompareIdIncrease );
+    Vec_PtrSort( p->vSimClasses, Aig_ObjCompareIdIncrease );
 }
 
 /**Function*************************************************************
diff --git a/src/aig/dch/dchSweep.c b/src/aig/dch/dchSweep.c
index 019f6707..36c5fc33 100644
--- a/src/aig/dch/dchSweep.c
+++ b/src/aig/dch/dchSweep.c
@@ -86,6 +86,7 @@ void Dch_ManSweepNode( Dch_Man_t * p, Aig_Obj_t * pObj )
         Dch_ManResimulateCex( p, pObj, pObjRepr );
     else
         Dch_ManResimulateCex2( p, pObj, pObjRepr );
+    assert( Aig_ObjRepr( p->pAigTotal, pObj ) != pObjRepr );
 }
 
 /**Function*************************************************************
diff --git a/src/aig/ssw/module.make b/src/aig/ssw/module.make
new file mode 100644
index 00000000..dcbe0081
--- /dev/null
+++ b/src/aig/ssw/module.make
@@ -0,0 +1,8 @@
+SRC +=    src/aig/ssw/sswAig.c \
+    src/aig/ssw/sswClass.c \
+    src/aig/ssw/sswCnf.c \
+    src/aig/ssw/sswCore.c \
+    src/aig/ssw/sswMan.c \
+    src/aig/ssw/sswSat.c \
+    src/aig/ssw/sswSimSat.c \
+    src/aig/ssw/sswSweep.c
diff --git a/src/aig/ssw/ssw.h b/src/aig/ssw/ssw.h
new file mode 100644
index 00000000..3bdc63f6
--- /dev/null
+++ b/src/aig/ssw/ssw.h
@@ -0,0 +1,79 @@
+/**CFile****************************************************************
+
+  FileName    [ssw.h] 
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Inductive prover with constraints.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - September 1, 2008.]
+
+  Revision    [$Id: ssw.h,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef __SSW_H__
+#define __SSW_H__
+
+#ifdef __cplusplus
+extern "C" { 
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+// choicing parameters
+typedef struct Ssw_Pars_t_ Ssw_Pars_t;
+struct Ssw_Pars_t_
+{
+    int              nPartSize;     // size of the partition
+    int              nOverSize;     // size of the overlap between partitions
+    int              nFramesK;      // the induction depth
+    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              fPolarFlip;    // uses polarity adjustment
+    int              fLatchCorr;    // perform register correspondence
+    int              fVerbose;      // verbose stats
+    // internal parameters
+    int              nIters;        // the number of iterations performed
+};
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== sswCore.c ==========================================================*/
+extern void          Ssw_ManSetDefaultParams( Ssw_Pars_t * p );
+extern Aig_Man_t *   Ssw_SignalCorrespondence( Aig_Man_t * p, Ssw_Pars_t * pPars );
+
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/aig/ssw/sswAig.c b/src/aig/ssw/sswAig.c
new file mode 100644
index 00000000..47f15e55
--- /dev/null
+++ b/src/aig/ssw/sswAig.c
@@ -0,0 +1,134 @@
+/**CFile****************************************************************
+
+  FileName    [sswAig.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Inductive prover with constraints.]
+
+  Synopsis    [AIG manipulation.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - September 1, 2008.]
+
+  Revision    [$Id: sswAig.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "sswInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+
+/**Function*************************************************************
+
+  Synopsis    [Performs speculative reduction for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Ssw_FramesConstrainNode( Ssw_Man_t * p, Aig_Man_t * pFrames, Aig_Man_t * pAig, Aig_Obj_t * pObj, int iFrame )
+{
+    Aig_Obj_t * pObjNew, * pObjNew2, * pObjRepr, * pObjReprNew;
+    // skip nodes without representative
+    if ( (pObjRepr = Aig_ObjRepr(pAig, pObj)) == NULL )
+        return;
+    p->nConstrTotal++;
+    assert( pObjRepr->Id < pObj->Id );
+    // get the new node 
+    pObjNew = Ssw_ObjFraig( p, pObj, iFrame );
+    // 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;
+    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) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prepares the inductive case with speculative reduction.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p )
+{
+    Aig_Man_t * pFrames;
+    Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjNew;
+    int i, k, f;
+    assert( p->pFrames == NULL );
+    assert( Aig_ManRegNum(p->pAig) > 0 );
+    assert( Aig_ManRegNum(p->pAig) < Aig_ManPiNum(p->pAig) );
+
+    // start the fraig package
+    pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->nFrames );
+    // 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++ )
+    {
+        // set the constraints on the latch outputs
+        Aig_ManForEachLoSeq( p->pAig, pObj, i )
+            Ssw_FramesConstrainNode( p, pFrames, p->pAig, pObj, f );
+        // add internal nodes of this frame
+        Aig_ManForEachNode( p->pAig, pObj, i )
+        {
+            pObjNew = Aig_And( pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
+            Ssw_ObjSetFraig( p, pObj, f, pObjNew );
+            Ssw_FramesConstrainNode( p, pFrames, p->pAig, pObj, f );
+        }
+        // transfer latch input to the latch outputs 
+        Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, k )
+            Ssw_ObjSetFraig( p, pObjLo, f+1, Ssw_ObjChild0Fra(p, pObjLi,f) );
+    }
+    // add the POs for the latch outputs of the last frame
+    Saig_ManForEachLo( p->pAig, pObj, i )
+        Aig_ObjCreatePo( pFrames, Ssw_ObjFraig( p, pObj, p->pPars->nFramesK ) );
+
+    // remove dangling nodes
+    Aig_ManCleanup( pFrames );
+    // make sure the satisfying assignment is node assigned
+    assert( pFrames->pData == NULL );
+    return pFrames;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/ssw/sswClass.c b/src/aig/ssw/sswClass.c
new file mode 100644
index 00000000..bf4883e3
--- /dev/null
+++ b/src/aig/ssw/sswClass.c
@@ -0,0 +1,716 @@
+/**CFile****************************************************************
+
+  FileName    [sswClass.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Inductive prover with constraints.]
+
+  Synopsis    [Representation of candidate equivalence classes.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - September 1, 2008.]
+
+  Revision    [$Id: sswClass.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "sswInt.h"
+
+/*
+    The candidate equivalence classes are stored as a vector of pointers 
+    to the array of pointers to the nodes in each class.
+    The first node of the class is its representative node.
+    The representative has the smallest topological order among the class nodes.
+    The nodes inside each class are ordered according to their topological order.
+    The classes are ordered according to the topo order of their representatives.
+*/
+
+// internal representation of candidate equivalence classes
+struct Ssw_Cla_t_
+{
+    // class information
+    Aig_Man_t *      pAig;             // original AIG manager
+    Aig_Obj_t ***    pId2Class;        // non-const classes by ID of repr node
+    int *            pClassSizes;      // sizes of each equivalence class
+    // statistics
+    int              nClasses;         // the total number of non-const classes
+    int              nCands1;          // the total number of const candidates
+    int              nLits;            // the number of literals in all classes
+    // memory
+    Aig_Obj_t **     pMemClasses;      // memory allocated for equivalence classes
+    Aig_Obj_t **     pMemClassesFree;  // memory allocated for equivalence classes to be used
+    // temporary data
+    Vec_Ptr_t *      vClassOld;        // old equivalence class after splitting
+    Vec_Ptr_t *      vClassNew;        // new equivalence class(es) after splitting
+    // procedures used for class refinement
+    void *           pManData;
+    unsigned (*pFuncNodeHash) (void *,Aig_Obj_t *);              // returns hash key of the node
+    int (*pFuncNodeIsConst)   (void *,Aig_Obj_t *);              // returns 1 if the node is a constant
+    int (*pFuncNodesAreEqual) (void *,Aig_Obj_t *, Aig_Obj_t *); // returns 1 if nodes are equal up to a complement
+};
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static inline Aig_Obj_t *  Ssw_ObjNext( Aig_Obj_t ** ppNexts, Aig_Obj_t * pObj )                       { return ppNexts[pObj->Id];  }
+static inline void         Ssw_ObjSetNext( Aig_Obj_t ** ppNexts, Aig_Obj_t * pObj, Aig_Obj_t * pNext ) { ppNexts[pObj->Id] = pNext; }
+
+// iterator through the equivalence classes
+#define Ssw_ManForEachClass( p, ppClass, i )                 \
+    for ( i = 0; i < Aig_ManObjNumMax(p->pAig); i++ )        \
+        if ( ((ppClass) = p->pId2Class[i]) == NULL ) {} else
+// iterator through the nodes in one class
+#define Ssw_ClassForEachNode( p, pRepr, pNode, i )           \
+    for ( i = 0; i < p->pClassSizes[pRepr->Id]; i++ )        \
+        if ( ((pNode) = p->pId2Class[pRepr->Id][i]) == NULL ) {} else
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Creates one equivalence class.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Ssw_ObjAddClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, Aig_Obj_t ** pClass, int nSize ) 
+{
+    assert( p->pId2Class[pRepr->Id] == NULL );
+    p->pId2Class[pRepr->Id] = pClass; 
+    assert( p->pClassSizes[pRepr->Id] == 0 );
+    assert( nSize > 1 );
+    p->pClassSizes[pRepr->Id] = nSize;
+    p->nClasses++;
+    p->nLits += nSize - 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Removes one equivalence class.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Aig_Obj_t ** Ssw_ObjRemoveClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr ) 
+{
+    Aig_Obj_t ** pClass = p->pId2Class[pRepr->Id];
+    int nSize;
+    assert( pClass != NULL );
+    p->pId2Class[pRepr->Id] = NULL; 
+    nSize = p->pClassSizes[pRepr->Id];
+    assert( nSize > 1 );
+    p->nClasses--;
+    p->nLits -= nSize - 1;
+    p->pClassSizes[pRepr->Id] = 0;
+    return pClass;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Starts representation of equivalence classes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ssw_Cla_t * Ssw_ClassesStart( Aig_Man_t * pAig )
+{
+    Ssw_Cla_t * p;
+    p = ALLOC( Ssw_Cla_t, 1 );
+    memset( p, 0, sizeof(Ssw_Cla_t) );
+    p->pAig         = pAig;
+    p->pId2Class    = CALLOC( Aig_Obj_t **, Aig_ManObjNumMax(pAig) );
+    p->pClassSizes  = CALLOC( int, Aig_ManObjNumMax(pAig) );
+    p->vClassOld    = Vec_PtrAlloc( 100 );
+    p->vClassNew    = Vec_PtrAlloc( 100 );
+    assert( pAig->pReprs == NULL );
+    Aig_ManReprStart( pAig, Aig_ManObjNumMax(pAig) );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Starts representation of equivalence classes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_ClassesSetData( Ssw_Cla_t * p, void * pManData, 
+    unsigned (*pFuncNodeHash)(void *,Aig_Obj_t *),               // returns hash key of the node
+    int (*pFuncNodeIsConst)(void *,Aig_Obj_t *),                 // returns 1 if the node is a constant
+    int (*pFuncNodesAreEqual)(void *,Aig_Obj_t *, Aig_Obj_t *) ) // returns 1 if nodes are equal up to a complement
+{
+    p->pManData           = pManData;
+    p->pFuncNodeHash      = pFuncNodeHash;
+    p->pFuncNodeIsConst   = pFuncNodeIsConst;
+    p->pFuncNodesAreEqual = pFuncNodesAreEqual;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stop representation of equivalence classes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_ClassesStop( Ssw_Cla_t * p )
+{
+    if ( p->vClassNew )    Vec_PtrFree( p->vClassNew );
+    if ( p->vClassOld )    Vec_PtrFree( p->vClassOld );
+    FREE( p->pId2Class );
+    FREE( p->pClassSizes );
+    FREE( p->pMemClasses );
+    free( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stop representation of equivalence classes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ssw_ClassesCand1Num( Ssw_Cla_t * p )
+{
+    return p->nCands1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stop representation of equivalence classes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ssw_ClassesClassNum( Ssw_Cla_t * p )
+{
+    return p->nClasses;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stop representation of equivalence classes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ssw_ClassesLitNum( Ssw_Cla_t * p )
+{
+    return p->nLits;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stop representation of equivalence classes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Obj_t ** Ssw_ClassesReadClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, int * pnSize )
+{
+    assert( p->pId2Class[pRepr->Id] != NULL );
+    assert( p->pClassSizes[pRepr->Id] > 1 );
+    *pnSize = p->pClassSizes[pRepr->Id];
+    return p->pId2Class[pRepr->Id];
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Checks candidate equivalence classes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_ClassesCheck( Ssw_Cla_t * p )
+{
+    Aig_Obj_t * pObj, * pPrev, ** ppClass;
+    int i, k, nLits, nClasses, nCands1;
+    nClasses = nLits = 0;
+    Ssw_ManForEachClass( p, ppClass, k )
+    {
+        pPrev = NULL;
+        Ssw_ClassForEachNode( p, ppClass[0], pObj, i )
+        {
+            if ( i == 0 )
+                assert( Aig_ObjRepr(p->pAig, pObj) == NULL );
+            else
+            {
+                assert( Aig_ObjRepr(p->pAig, pObj) == ppClass[0] );
+                assert( pPrev->Id < pObj->Id );
+                nLits++;
+            }
+            pPrev = pObj;
+        }
+        nClasses++;
+    }
+    nCands1 = 0;
+    Aig_ManForEachObj( p->pAig, pObj, i )
+        nCands1 += Ssw_ObjIsConst1Cand( p->pAig, pObj );
+    assert( p->nLits == nLits );
+    assert( p->nCands1 == nCands1 );
+    assert( p->nClasses == nClasses );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints simulation classes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_ClassesPrintOne( Ssw_Cla_t * p, Aig_Obj_t * pRepr )
+{
+    Aig_Obj_t * pObj;
+    int i;
+    printf( "{ " );
+    Ssw_ClassForEachNode( p, pRepr, pObj, i )
+        printf( "%d(%d,%d) ", pObj->Id, pObj->Level, Aig_SupportSize(p->pAig,pObj) );
+    printf( "}\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints simulation classes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_ClassesPrint( Ssw_Cla_t * p, int fVeryVerbose )
+{
+    Aig_Obj_t ** ppClass;
+    Aig_Obj_t * pObj;
+    int i;
+    printf( "Equivalence classes: Const1 = %5d. Class = %5d. Lit = %5d.\n", 
+        p->nCands1, p->nClasses, p->nLits );
+    if ( !fVeryVerbose )
+        return;
+    printf( "Constants { " );
+    Aig_ManForEachObj( p->pAig, pObj, i )
+        if ( Ssw_ObjIsConst1Cand( p->pAig, pObj ) )
+            printf( "%d(%d,%d) ", pObj->Id, pObj->Level, Aig_SupportSize(p->pAig,pObj) );
+    printf( "}\n" );
+    Ssw_ManForEachClass( p, ppClass, i )
+    {
+        printf( "%3d (%3d) : ", i, p->pClassSizes[i] );
+        Ssw_ClassesPrintOne( p, ppClass[0] );
+    }
+    printf( "\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints simulation classes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_ClassesRemoveNode( Ssw_Cla_t * p, Aig_Obj_t * pObj )
+{
+    Aig_Obj_t * pRepr, * pTemp;
+    assert( p->pId2Class[pObj->Id] == NULL );
+    pRepr = Aig_ObjRepr( p->pAig, pObj );
+    assert( pRepr != NULL );
+    Aig_ObjSetRepr( p->pAig, pObj, NULL );
+    if ( Ssw_ObjIsConst1Cand( p->pAig, pObj ) )
+    {
+        p->nCands1--;
+        return;
+    }
+    assert( p->pId2Class[pRepr->Id][0] == pRepr );
+    assert( p->pClassSizes[pRepr->Id] >= 2 );
+    if ( p->pClassSizes[pRepr->Id] == 2 )
+    {
+        p->pId2Class[pObj->Id] = NULL;
+        p->nClasses--;
+        p->pClassSizes[pRepr->Id] = 0;
+        p->nLits--;
+    }
+    else
+    {
+        int i, k = 0;
+        // remove the entry from the class
+        Ssw_ClassForEachNode( p, pRepr, pTemp, i )
+            if ( pTemp != pObj )
+                p->pId2Class[pRepr->Id][k++] = pTemp;
+        assert( k + 1 == p->pClassSizes[pRepr->Id] );
+        // reduce the class
+        p->pClassSizes[pRepr->Id]--;
+        p->nLits--;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates initial simulation classes.]
+
+  Description [Assumes that simulation info is assigned.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_ClassesPrepare( Ssw_Cla_t * p, int fLatchCorr, int nMaxLevs )
+{
+    Aig_Obj_t ** ppTable, ** ppNexts, ** ppClassNew;
+    Aig_Obj_t * pObj, * pTemp, * pRepr;
+    int i, k, nTableSize, nNodes, iEntry, nEntries, nEntries2;
+
+    // allocate the hash table hashing simulation info into nodes
+    nTableSize = Aig_PrimeCudd( Aig_ManObjNumMax(p->pAig)/4 );
+    ppTable = CALLOC( Aig_Obj_t *, nTableSize ); 
+    ppNexts = CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) ); 
+
+    // add all the nodes to the hash table
+    nEntries = 0;
+    Aig_ManForEachObj( p->pAig, pObj, i )
+    {
+        if ( fLatchCorr )
+        {
+            if ( !Aig_ObjIsPi(pObj) )
+                continue;
+        }
+        else
+        {
+            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 )
+                continue;
+        }
+        // check if the node belongs to the class of constant 1
+        if ( p->pFuncNodeIsConst( p->pManData, pObj ) )
+        {
+            Ssw_ObjSetConst1Cand( p->pAig, pObj );
+            p->nCands1++;
+            continue;
+        }
+        // hash the node by its simulation info
+        iEntry = p->pFuncNodeHash( p->pManData, pObj ) % nTableSize;
+        // add the node to the class
+        if ( ppTable[iEntry] == NULL )
+            ppTable[iEntry] = pObj;
+        else
+        {
+            // set the representative of this node
+            pRepr = ppTable[iEntry];
+            Aig_ObjSetRepr( p->pAig, pObj, pRepr );
+            // add node to the table
+            if ( Ssw_ObjNext( ppNexts, pRepr ) == NULL )
+            { // this will be the second entry
+                p->pClassSizes[pRepr->Id]++;
+                nEntries++;
+            }
+            // add the entry to the list
+            Ssw_ObjSetNext( ppNexts, pObj, Ssw_ObjNext( ppNexts, pRepr ) );
+            Ssw_ObjSetNext( ppNexts, pRepr, pObj );
+            p->pClassSizes[pRepr->Id]++;
+            nEntries++;
+        }
+    }
+
+    // allocate room for classes
+    p->pMemClasses = ALLOC( Aig_Obj_t *, nEntries + p->nCands1 );
+    p->pMemClassesFree = p->pMemClasses + nEntries;
+ 
+    // copy the entries into storage in the topological order
+    nEntries2 = 0;
+    Aig_ManForEachObj( p->pAig, pObj, i )
+    {
+        if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
+            continue;
+        nNodes = p->pClassSizes[pObj->Id];
+        // skip the nodes that are not representatives of non-trivial classes
+        if ( nNodes == 0 )
+            continue;
+        assert( nNodes > 1 );
+        // add the nodes to the class in the topological order
+        ppClassNew = p->pMemClasses + nEntries2;
+        ppClassNew[0] = pObj;
+        for ( pTemp = Ssw_ObjNext(ppNexts, pObj), k = 1; pTemp; 
+              pTemp = Ssw_ObjNext(ppNexts, pTemp), k++ )
+        {
+            ppClassNew[nNodes-k] = pTemp;
+        }
+        // add the class of nodes
+        p->pClassSizes[pObj->Id] = 0;
+        Ssw_ObjAddClass( p, pObj, ppClassNew, nNodes );
+        // increment the number of entries
+        nEntries2 += nNodes;
+    }
+    assert( nEntries == nEntries2 );
+    free( ppTable );
+    free( ppNexts );
+    // now it is time to refine the classes
+    Ssw_ClassesRefine( p );
+    Ssw_ClassesCheck( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if the node appears to be constant 1 candidate.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ssw_NodeIsConstCex( void * p, Aig_Obj_t * pObj )
+{
+    return pObj->fPhase == pObj->fMarkB;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if the nodes appear equal.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ssw_NodesAreEqualCex( void * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
+{
+    return (pObj0->fPhase == pObj1->fPhase) == (pObj0->fMarkB == pObj1->fMarkB);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates initial simulation classes.]
+
+  Description [Assumes that simulation info is assigned.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ssw_Cla_t * Ssw_ClassesPrepareSimple( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs )
+{
+    Ssw_Cla_t * p;
+    Aig_Obj_t * pObj;
+    int i;
+    // start the classes
+    p = Ssw_ClassesStart( pAig );
+    // go through the nodes
+    p->nCands1 = 0;
+    Aig_ManForEachObj( p->pAig, pObj, i )
+    {
+        if ( fLatchCorr )
+        {
+            if ( !Saig_ObjIsLo(pAig, pObj) )
+                continue;
+        }
+        else
+        {
+            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 )
+                continue;
+        }
+        Ssw_ObjSetConst1Cand( p->pAig, pObj );
+        p->nCands1++;
+    }
+    // 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;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Iteratively refines the classes after simulation.]
+
+  Description [Returns the number of refinements performed.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ssw_ClassesRefineOneClass( Ssw_Cla_t * p, Aig_Obj_t * pReprOld, int fRecursive )
+{
+    Aig_Obj_t ** pClassOld, ** pClassNew;
+    Aig_Obj_t * pObj, * pReprNew;
+    int i;
+
+    // split the class
+    Vec_PtrClear( p->vClassOld );
+    Vec_PtrClear( p->vClassNew );
+    Ssw_ClassForEachNode( p, pReprOld, pObj, i )
+        if ( p->pFuncNodesAreEqual(p->pManData, pReprOld, pObj) )
+            Vec_PtrPush( p->vClassOld, pObj );
+        else
+            Vec_PtrPush( p->vClassNew, pObj );
+    // check if splitting happened
+    if ( Vec_PtrSize(p->vClassNew) == 0 )
+        return 0;
+
+    // get the new representative
+    pReprNew = Vec_PtrEntry( p->vClassNew, 0 );
+    assert( Vec_PtrSize(p->vClassOld) > 0 );
+    assert( Vec_PtrSize(p->vClassNew) > 0 );
+
+    // create old class
+    pClassOld = Ssw_ObjRemoveClass( p, pReprOld );
+    Vec_PtrForEachEntry( p->vClassOld, pObj, i )
+    {
+        pClassOld[i] = pObj;
+        Aig_ObjSetRepr( p->pAig, pObj, i? pReprOld : NULL );
+    }
+    // create new class
+    pClassNew = pClassOld + i;
+    Vec_PtrForEachEntry( p->vClassNew, pObj, i )
+    {
+        pClassNew[i] = pObj;
+        Aig_ObjSetRepr( p->pAig, pObj, i? pReprNew : NULL );
+    }
+
+    // put classes back
+    if ( Vec_PtrSize(p->vClassOld) > 1 )
+        Ssw_ObjAddClass( p, pReprOld, pClassOld, Vec_PtrSize(p->vClassOld) );
+    if ( Vec_PtrSize(p->vClassNew) > 1 )
+        Ssw_ObjAddClass( p, pReprNew, pClassNew, Vec_PtrSize(p->vClassNew) );
+
+    // check if the class should be recursively refined
+    if ( fRecursive && Vec_PtrSize(p->vClassNew) > 1 )
+        return 1 + Ssw_ClassesRefineOneClass( p, pReprNew, 1 );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Refines the classes after simulation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ssw_ClassesRefine( Ssw_Cla_t * p )
+{
+    Aig_Obj_t ** ppClass;
+    int i, nRefis = 0;
+    Ssw_ManForEachClass( p, ppClass, i )
+        nRefis += Ssw_ClassesRefineOneClass( p, ppClass[0], 0 );
+    return nRefis;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Refine the group of constant 1 nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ssw_ClassesRefineConst1Group( Ssw_Cla_t * p, Vec_Ptr_t * vRoots, int fRecursive )
+{
+    Aig_Obj_t * pObj, * pReprNew, ** ppClassNew;
+    int i;
+    if ( Vec_PtrSize(vRoots) == 0 )
+        return 0;
+    // collect the nodes to be refined
+    Vec_PtrClear( p->vClassNew );
+    Vec_PtrForEachEntry( vRoots, pObj, 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/sswCnf.c b/src/aig/ssw/sswCnf.c
new file mode 100644
index 00000000..f5047400
--- /dev/null
+++ b/src/aig/ssw/sswCnf.c
@@ -0,0 +1,329 @@
+/**CFile****************************************************************
+
+  FileName    [sswCnf.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Inductive prover with constraints.]
+
+  Synopsis    [Computation of CNF.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - September 1, 2008.]
+
+  Revision    [$Id: sswCnf.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "sswInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Addes clauses to the solver.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_AddClausesMux( Ssw_Man_t * p, Aig_Obj_t * pNode )
+{
+    Aig_Obj_t * pNodeI, * pNodeT, * pNodeE;
+    int pLits[4], RetValue, VarF, VarI, VarT, VarE, fCompT, fCompE;
+
+    assert( !Aig_IsComplement( pNode ) );
+    assert( Aig_ObjIsMuxType( pNode ) );
+    // get nodes (I = if, T = then, E = else)
+    pNodeI = Aig_ObjRecognizeMux( pNode, &pNodeT, &pNodeE );
+    // get the variable numbers
+    VarF = Ssw_ObjSatNum(p,pNode);
+    VarI = Ssw_ObjSatNum(p,pNodeI);
+    VarT = Ssw_ObjSatNum(p,Aig_Regular(pNodeT));
+    VarE = Ssw_ObjSatNum(p,Aig_Regular(pNodeE));
+    // get the complementation flags
+    fCompT = Aig_IsComplement(pNodeT);
+    fCompE = Aig_IsComplement(pNodeE);
+
+    // f = ITE(i, t, e)
+
+    // i' + t' + f
+    // i' + t  + f'
+    // i  + e' + f
+    // i  + e  + f'
+
+    // create four clauses
+    pLits[0] = toLitCond(VarI, 1);
+    pLits[1] = toLitCond(VarT, 1^fCompT);
+    pLits[2] = toLitCond(VarF, 0);
+    if ( p->pPars->fPolarFlip )
+    {
+        if ( pNodeI->fPhase )               pLits[0] = lit_neg( pLits[0] );
+        if ( Aig_Regular(pNodeT)->fPhase )  pLits[1] = lit_neg( pLits[1] );
+        if ( pNode->fPhase )                pLits[2] = lit_neg( pLits[2] );
+    }
+    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
+    assert( RetValue );
+    pLits[0] = toLitCond(VarI, 1);
+    pLits[1] = toLitCond(VarT, 0^fCompT);
+    pLits[2] = toLitCond(VarF, 1);
+    if ( p->pPars->fPolarFlip )
+    {
+        if ( pNodeI->fPhase )               pLits[0] = lit_neg( pLits[0] );
+        if ( Aig_Regular(pNodeT)->fPhase )  pLits[1] = lit_neg( pLits[1] );
+        if ( pNode->fPhase )                pLits[2] = lit_neg( pLits[2] );
+    }
+    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
+    assert( RetValue );
+    pLits[0] = toLitCond(VarI, 0);
+    pLits[1] = toLitCond(VarE, 1^fCompE);
+    pLits[2] = toLitCond(VarF, 0);
+    if ( p->pPars->fPolarFlip )
+    {
+        if ( pNodeI->fPhase )               pLits[0] = lit_neg( pLits[0] );
+        if ( Aig_Regular(pNodeE)->fPhase )  pLits[1] = lit_neg( pLits[1] );
+        if ( pNode->fPhase )                pLits[2] = lit_neg( pLits[2] );
+    }
+    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
+    assert( RetValue );
+    pLits[0] = toLitCond(VarI, 0);
+    pLits[1] = toLitCond(VarE, 0^fCompE);
+    pLits[2] = toLitCond(VarF, 1);
+    if ( p->pPars->fPolarFlip )
+    {
+        if ( pNodeI->fPhase )               pLits[0] = lit_neg( pLits[0] );
+        if ( Aig_Regular(pNodeE)->fPhase )  pLits[1] = lit_neg( pLits[1] );
+        if ( pNode->fPhase )                pLits[2] = lit_neg( pLits[2] );
+    }
+    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
+    assert( RetValue );
+
+    // two additional clauses
+    // t' & e' -> f'
+    // t  & e  -> f 
+
+    // t  + e   + f'
+    // t' + e'  + f 
+
+    if ( VarT == VarE )
+    {
+//        assert( fCompT == !fCompE );
+        return;
+    }
+
+    pLits[0] = toLitCond(VarT, 0^fCompT);
+    pLits[1] = toLitCond(VarE, 0^fCompE);
+    pLits[2] = toLitCond(VarF, 1);
+    if ( p->pPars->fPolarFlip )
+    {
+        if ( Aig_Regular(pNodeT)->fPhase )  pLits[0] = lit_neg( pLits[0] );
+        if ( Aig_Regular(pNodeE)->fPhase )  pLits[1] = lit_neg( pLits[1] );
+        if ( pNode->fPhase )                pLits[2] = lit_neg( pLits[2] );
+    }
+    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
+    assert( RetValue );
+    pLits[0] = toLitCond(VarT, 1^fCompT);
+    pLits[1] = toLitCond(VarE, 1^fCompE);
+    pLits[2] = toLitCond(VarF, 0);
+    if ( p->pPars->fPolarFlip )
+    {
+        if ( Aig_Regular(pNodeT)->fPhase )  pLits[0] = lit_neg( pLits[0] );
+        if ( Aig_Regular(pNodeE)->fPhase )  pLits[1] = lit_neg( pLits[1] );
+        if ( pNode->fPhase )                pLits[2] = lit_neg( pLits[2] );
+    }
+    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
+    assert( RetValue );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Addes clauses to the solver.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_AddClausesSuper( Ssw_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper )
+{
+    Aig_Obj_t * pFanin;
+    int * pLits, nLits, RetValue, i;
+    assert( !Aig_IsComplement(pNode) );
+    assert( Aig_ObjIsNode( pNode ) );
+    // create storage for literals
+    nLits = Vec_PtrSize(vSuper) + 1;
+    pLits = ALLOC( int, nLits );
+    // suppose AND-gate is A & B = C
+    // add !A => !C   or   A + !C
+    Vec_PtrForEachEntry( vSuper, pFanin, i )
+    {
+        pLits[0] = toLitCond(Ssw_ObjSatNum(p,Aig_Regular(pFanin)), Aig_IsComplement(pFanin));
+        pLits[1] = toLitCond(Ssw_ObjSatNum(p,pNode), 1);
+        if ( p->pPars->fPolarFlip )
+        {
+            if ( Aig_Regular(pFanin)->fPhase )  pLits[0] = lit_neg( pLits[0] );
+            if ( pNode->fPhase )                pLits[1] = lit_neg( pLits[1] );
+        }
+        RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
+        assert( RetValue );
+    }
+    // add A & B => C   or   !A + !B + C
+    Vec_PtrForEachEntry( vSuper, pFanin, i )
+    {
+        pLits[i] = toLitCond(Ssw_ObjSatNum(p,Aig_Regular(pFanin)), !Aig_IsComplement(pFanin));
+        if ( p->pPars->fPolarFlip )
+        {
+            if ( Aig_Regular(pFanin)->fPhase )  pLits[i] = lit_neg( pLits[i] );
+        }
+    }
+    pLits[nLits-1] = toLitCond(Ssw_ObjSatNum(p,pNode), 0);
+    if ( p->pPars->fPolarFlip )
+    {
+        if ( pNode->fPhase )  pLits[nLits-1] = lit_neg( pLits[nLits-1] );
+    }
+    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + nLits );
+    assert( RetValue );
+    free( pLits );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the supergate.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_CollectSuper_rec( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int fUseMuxes )
+{
+    // if the new node is complemented or a PI, another gate begins
+    if ( Aig_IsComplement(pObj) || Aig_ObjIsPi(pObj) || 
+         (!fFirst && Aig_ObjRefs(pObj) > 1) || 
+         (fUseMuxes && Aig_ObjIsMuxType(pObj)) )
+    {
+        Vec_PtrPushUnique( vSuper, pObj );
+        return;
+    }
+    // go through the branches
+    Ssw_CollectSuper_rec( Aig_ObjChild0(pObj), vSuper, 0, fUseMuxes );
+    Ssw_CollectSuper_rec( Aig_ObjChild1(pObj), vSuper, 0, fUseMuxes );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the supergate.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_CollectSuper( Aig_Obj_t * pObj, int fUseMuxes, Vec_Ptr_t * vSuper )
+{
+    assert( !Aig_IsComplement(pObj) );
+    assert( !Aig_ObjIsPi(pObj) );
+    Vec_PtrClear( vSuper );
+    Ssw_CollectSuper_rec( pObj, vSuper, 1, fUseMuxes );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Updates the solver clause database.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_ObjAddToFrontier( Ssw_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vFrontier )
+{
+    assert( !Aig_IsComplement(pObj) );
+    if ( Ssw_ObjSatNum(p,pObj) )
+        return;
+    assert( Ssw_ObjSatNum(p,pObj) == 0 );
+    if ( Aig_ObjIsConst1(pObj) )
+        return;
+//    Vec_PtrPush( p->vUsedNodes, pObj );
+    Ssw_ObjSetSatNum( p, pObj, p->nSatVars++ );
+    if ( Aig_ObjIsNode(pObj) )
+        Vec_PtrPush( vFrontier, pObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Updates the solver clause database.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_CnfNodeAddToSolver( Ssw_Man_t * p, Aig_Obj_t * pObj )
+{ 
+    Vec_Ptr_t * vFrontier;
+    Aig_Obj_t * pNode, * pFanin;
+    int i, k, fUseMuxes = 1;
+    // quit if CNF is ready
+    if ( Ssw_ObjSatNum(p,pObj) )
+        return;
+    // start the frontier
+    vFrontier = Vec_PtrAlloc( 100 );
+    Ssw_ObjAddToFrontier( p, pObj, vFrontier );
+    // explore nodes in the frontier
+    Vec_PtrForEachEntry( vFrontier, pNode, i )
+    {
+        // create the supergate
+        assert( Ssw_ObjSatNum(p,pNode) );
+        if ( fUseMuxes && Aig_ObjIsMuxType(pNode) )
+        {
+            Vec_PtrClear( p->vFanins );
+            Vec_PtrPushUnique( p->vFanins, Aig_ObjFanin0( Aig_ObjFanin0(pNode) ) );
+            Vec_PtrPushUnique( p->vFanins, Aig_ObjFanin0( Aig_ObjFanin1(pNode) ) );
+            Vec_PtrPushUnique( p->vFanins, Aig_ObjFanin1( Aig_ObjFanin0(pNode) ) );
+            Vec_PtrPushUnique( p->vFanins, Aig_ObjFanin1( Aig_ObjFanin1(pNode) ) );
+            Vec_PtrForEachEntry( p->vFanins, pFanin, k )
+                Ssw_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier );
+            Ssw_AddClausesMux( p, pNode );
+        }
+        else
+        {
+            Ssw_CollectSuper( pNode, fUseMuxes, p->vFanins );
+            Vec_PtrForEachEntry( p->vFanins, pFanin, k )
+                Ssw_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier );
+            Ssw_AddClausesSuper( p, pNode, p->vFanins );
+        }
+        assert( Vec_PtrSize(p->vFanins) > 1 );
+    }
+    Vec_PtrFree( vFrontier );
+}
+
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/ssw/sswCore.c b/src/aig/ssw/sswCore.c
new file mode 100644
index 00000000..1e314b78
--- /dev/null
+++ b/src/aig/ssw/sswCore.c
@@ -0,0 +1,105 @@
+/**CFile****************************************************************
+
+  FileName    [sswCore.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Inductive prover with constraints.]
+
+  Synopsis    [The core procedures.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - September 1, 2008.]
+
+  Revision    [$Id: sswCore.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "sswInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [This procedure sets default parameters.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_ManSetDefaultParams( Ssw_Pars_t * p )
+{
+    memset( p, 0, sizeof(Ssw_Pars_t) );
+    p->nPartSize      =     0;  // size of the partition
+    p->nOverSize      =     0;  // size of the overlap between partitions
+    p->nFramesK       =     1;  // the induction depth
+    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->fVerbose       =     1;  // verbose stats
+    p->nIters         =     0;  // the number of iterations performed
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs computation of signal correspondence with constraints.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
+{
+    Ssw_Man_t * p;
+    int RetValue, nIter, clk, clkTotal = clock();
+    // reset random numbers
+    Aig_ManRandom(1);
+    // start the choicing manager
+    p = Ssw_ManCreate( pAig, pPars );
+    // compute candidate equivalence classes
+    p->ppClasses = Ssw_ClassesPrepareSimple( pAig, pPars->fLatchCorr, pPars->nMaxLevs );
+    // refine classes using BMC
+    Ssw_ClassesPrint( p->ppClasses, 0 );
+    Ssw_ManSweepBmc( p );
+    Ssw_ClassesPrint( p->ppClasses, 0 );
+    // refine classes using induction
+    for ( nIter = 0; ; nIter++ )
+    {
+clk = clock();
+        RetValue = Ssw_ManSweep(p);
+        if ( pPars->fVerbose )
+        {
+            printf( "%3d : Const = %6d. Class = %6d.  L = %6d. LR = %6d.  NR = %6d. ", 
+                nIter, Ssw_ClassesCand1Num(p->ppClasses), Ssw_ClassesClassNum(p->ppClasses), 
+                p->nConstrTotal, p->nConstrReduced, p->nFrameNodes );
+            PRT( "T", clock() - clk );
+        } 
+        if ( !RetValue )
+            break;
+    }
+p->timeTotal = clock() - clkTotal;
+    Ssw_ManStop( p );
+    return Aig_ManDupRepr( pAig, 0 );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/ssw/sswInt.h b/src/aig/ssw/sswInt.h
new file mode 100644
index 00000000..0e54af32
--- /dev/null
+++ b/src/aig/ssw/sswInt.h
@@ -0,0 +1,164 @@
+/**CFile****************************************************************
+
+  FileName    [sswInt.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Inductive prover with constraints.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - September 1, 2008.]
+
+  Revision    [$Id: sswInt.h,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef __SSW_INT_H__
+#define __SSW_INT_H__
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include "saig.h"
+#include "satSolver.h"
+#include "ssw.h"
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+// equivalence classes
+typedef struct Ssw_Cla_t_ Ssw_Cla_t;
+
+// manager
+typedef struct Ssw_Man_t_ Ssw_Man_t;
+struct Ssw_Man_t_
+{
+    // parameters
+    Ssw_Pars_t *     pPars;          // parameters
+    int              nFrames;        // for quick lookup
+    // AIGs used in the package
+    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
+    int              fRefined;       // is set to 1 when refinement happens
+    // SAT solving
+    sat_solver *     pSat;           // recyclable SAT solver
+    int              nSatVars;       // the counter of SAT variables
+    int *            pSatVars;       // mapping of each node into its SAT var
+    Vec_Ptr_t *      vFanins;        // fanins of the CNF node
+    Vec_Ptr_t *      vSimRoots;      // the roots of cand const 1 nodes to simulate
+    Vec_Ptr_t *      vSimClasses;    // the roots of cand equiv classes to simulate
+    // constraints
+    int              nConstrTotal;   // the number of total constraints
+    int              nConstrReduced; // the number of reduced constraints
+    // SAT calls statistics
+    int              nSatCalls;      // the number of SAT calls
+    int              nSatProof;      // the number of proofs
+    int              nSatFailsReal;  // the number of timeouts
+    int              nSatCallsUnsat; // the number of unsat SAT calls
+    int              nSatCallsSat;   // the number of sat SAT calls
+    // runtime stats
+    int              timeBmc;        // bounded model checking
+    int              timeReduce;     // speculative reduction
+    int              timeSimSat;     // simulation of the counter-examples
+    int              timeSat;        // solving SAT
+    int              timeSatSat;     // sat
+    int              timeSatUnsat;   // unsat
+    int              timeSatUndec;   // undecided
+    int              timeOther;      // other runtime
+    int              timeTotal;      // total runtime
+};
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+static inline int  Ssw_ObjSatNum( Ssw_Man_t * p, Aig_Obj_t * pObj )             { return p->pSatVars[pObj->Id]; }
+static inline void Ssw_ObjSetSatNum( Ssw_Man_t * p, Aig_Obj_t * pObj, int Num ) { p->pSatVars[pObj->Id] = Num;  }
+
+static inline int  Ssw_ObjIsConst1Cand( Aig_Man_t * pAig, Aig_Obj_t * pObj ) 
+{
+    return Aig_ObjRepr(pAig, pObj) == Aig_ManConst1(pAig);
+}
+static inline void Ssw_ObjSetConst1Cand( Aig_Man_t * pAig, Aig_Obj_t * pObj ) 
+{
+    assert( !Ssw_ObjIsConst1Cand( pAig, pObj ) );
+    Aig_ObjSetRepr( pAig, pObj, Aig_ManConst1(pAig) );
+}
+
+static inline Aig_Obj_t * Ssw_ObjFraig( Ssw_Man_t * p, Aig_Obj_t * pObj, int i )                       { return p->pNodeToFraig[p->nFrames*pObj->Id + i];  }
+static inline void        Ssw_ObjSetFraig( Ssw_Man_t * p, Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { p->pNodeToFraig[p->nFrames*pObj->Id + i] = pNode; }
+
+static inline Aig_Obj_t * Ssw_ObjChild0Fra( Ssw_Man_t * p, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Ssw_ObjFraig(p, Aig_ObjFanin0(pObj), i), Aig_ObjFaninC0(pObj)) : NULL;  }
+static inline Aig_Obj_t * Ssw_ObjChild1Fra( Ssw_Man_t * p, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Ssw_ObjFraig(p, Aig_ObjFanin1(pObj), i), Aig_ObjFaninC1(pObj)) : NULL;  }
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== sswAig.c ===================================================*/
+extern Aig_Man_t *   Ssw_FramesWithClasses( Ssw_Man_t * p );
+/*=== sswClass.c =================================================*/
+extern Ssw_Cla_t *   Ssw_ClassesStart( Aig_Man_t * pAig );
+extern void          Ssw_ClassesSetData( Ssw_Cla_t * p, void * pManData,
+                         unsigned (*pFuncNodeHash)(void *,Aig_Obj_t *),
+                         int (*pFuncNodeIsConst)(void *,Aig_Obj_t *),
+                         int (*pFuncNodesAreEqual)(void *,Aig_Obj_t *, Aig_Obj_t *) );
+extern void          Ssw_ClassesStop( 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 );
+extern Aig_Obj_t **  Ssw_ClassesReadClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, int * pnSize );
+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 void          Ssw_ClassesPrepare( Ssw_Cla_t * p, int fLatchCorr, int nMaxLevs );
+extern Ssw_Cla_t *   Ssw_ClassesPrepareSimple( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs );
+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 );
+/*=== sswCnf.c ===================================================*/
+extern void          Ssw_CnfNodeAddToSolver( Ssw_Man_t * p, Aig_Obj_t * pObj );
+/*=== sswMan.c ===================================================*/
+extern Ssw_Man_t *   Ssw_ManCreate( Aig_Man_t * pAig, Ssw_Pars_t * pPars );
+extern void          Ssw_ManCleanup( Ssw_Man_t * p );
+extern void          Ssw_ManStop( Ssw_Man_t * p );
+extern void          Ssw_ManStartSolver( Ssw_Man_t * p );
+/*=== sswSat.c ===================================================*/
+extern int           Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
+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 );
+/*=== sswSweep.c ===================================================*/
+extern int           Ssw_ManSweepBmc( Ssw_Man_t * p );
+extern int           Ssw_ManSweep( Ssw_Man_t * p );
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/aig/ssw/sswMan.c b/src/aig/ssw/sswMan.c
new file mode 100644
index 00000000..86144ebb
--- /dev/null
+++ b/src/aig/ssw/sswMan.c
@@ -0,0 +1,206 @@
+/**CFile****************************************************************
+
+  FileName    [sswMan.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Inductive prover with constraints.]
+
+  Synopsis    [Calls to the SAT solver.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - September 1, 2008.]
+
+  Revision    [$Id: sswMan.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "sswInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Ssw_Man_t * Ssw_ManCreate( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
+{
+    Ssw_Man_t * p;
+    // 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 );
+    // SAT solving
+    p->nSatVars     = 1;
+    p->pSatVars     = CALLOC( int, Aig_ManObjNumMax(p->pAig) );
+    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;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints stats of the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ssw_ManCountEquivs( Ssw_Man_t * p )
+{
+    Aig_Obj_t * pObj;
+    int i, nEquivs = 0;
+    Aig_ManForEachObj( p->pAig, pObj, i )
+//        nEquivs += ( p->pReprsProved[i] != NULL );
+        nEquivs += ( Aig_ObjRepr(p->pAig, pObj) != NULL );
+    return nEquivs;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints stats of the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+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", 
+        p->nSatCalls, p->nSatCalls-p->nSatCallsSat-p->nSatFailsReal, 
+        p->nSatCallsSat, p->nSatFailsReal );
+    printf( "Equivs    : All = %6d.\n", Ssw_ManCountEquivs(p) );
+    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( "  undecided", p->timeSatUndec, p->timeTotal );
+    PRTP( "Other      ", p->timeOther,    p->timeTotal );
+    PRTP( "TOTAL      ", p->timeTotal,    p->timeTotal );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Frees the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_ManCleanup( Ssw_Man_t * p )
+{
+    Aig_ManCleanMarkB( p->pAig );
+    if ( p->pFrames )
+    {
+        Aig_ManStop( p->pFrames );
+        p->pFrames = NULL;
+    }
+    if ( p->pSat )
+    {
+        sat_solver_delete( p->pSat );
+        p->pSat = NULL;
+        p->nSatVars = 0;
+    }
+    memset( p->pNodeToFraig, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p->pAig) * p->nFrames );
+    p->nConstrTotal = 0;
+    p->nConstrReduced = 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Frees the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_ManStop( Ssw_Man_t * p )
+{
+    if ( p->pPars->fVerbose )
+        Ssw_ManPrintStats( p );
+    if ( p->ppClasses )
+        Ssw_ClassesStop( p->ppClasses );
+    Vec_PtrFree( p->vFanins );
+    Vec_PtrFree( p->vSimRoots );
+    Vec_PtrFree( p->vSimClasses );
+    FREE( p->pNodeToFraig );
+//    FREE( p->pReprsProved );
+    FREE( p->pSatVars );
+    free( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the SAT solver.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_ManStartSolver( Ssw_Man_t * p )
+{
+    int Lit;
+    assert( p->pSat == NULL );
+    p->pSat = sat_solver_new();
+    sat_solver_setnvars( p->pSat, 10000 );
+    // var 0 is not used
+    // var 1 is reserved for const1 node - add the clause
+    Lit = toLit( 1 );
+    if ( p->pPars->fPolarFlip )
+        Lit = lit_neg( Lit );
+    sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
+    p->nSatVars = 2;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/ssw/sswSat.c b/src/aig/ssw/sswSat.c
new file mode 100644
index 00000000..06abd2c9
--- /dev/null
+++ b/src/aig/ssw/sswSat.c
@@ -0,0 +1,234 @@
+/**CFile****************************************************************
+
+  FileName    [sswSat.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Inductive prover with constraints.]
+
+  Synopsis    [Calls to the SAT solver.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - September 1, 2008.]
+
+  Revision    [$Id: sswSat.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "sswInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Runs equivalence test for the two nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+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;
+    p->nSatCalls++;
+
+    // sanity checks
+    assert( !Aig_IsComplement(pNew) );
+    assert( !Aig_IsComplement(pOld) );
+    assert( pNew != pOld );
+
+    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 );
+
+    // 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 );
+    pLits[1] = toLitCond( Ssw_ObjSatNum(p,pNew), pOld->fPhase == pNew->fPhase );
+    if ( p->pPars->fPolarFlip )
+    {
+        if ( pOld->fPhase )  pLits[0] = lit_neg( pLits[0] );
+        if ( pNew->fPhase )  pLits[1] = lit_neg( pLits[1] );
+    }
+//Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
+clk = clock();
+    RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, 
+        (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+p->timeSat += clock() - clk;
+    if ( RetValue1 == l_False )
+    {
+p->timeSatUnsat += clock() - clk;
+        pLits[0] = lit_neg( pLits[0] );
+        pLits[1] = lit_neg( pLits[1] );
+        RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
+        assert( RetValue );
+        p->nSatCallsUnsat++;
+    }
+    else if ( RetValue1 == l_True )
+    {
+p->timeSatSat += clock() - clk;
+        p->nSatCallsSat++;
+        return 0;
+    }
+    else // if ( RetValue1 == l_Undef )
+    {
+p->timeSatUndec += clock() - clk;
+        p->nSatFailsReal++;
+        return -1;
+    }
+
+    // if the old node was constant 0, we already know the answer
+    if ( pOld == Aig_ManConst1(p->pFrames) )
+    {
+        p->nSatProof++;
+        return 1;
+    }
+
+    // solve under assumptions
+    // A = 0; B = 1     OR     A = 0; B = 0 
+    pLits[0] = toLitCond( Ssw_ObjSatNum(p,pOld), 1 );
+    pLits[1] = toLitCond( Ssw_ObjSatNum(p,pNew), pOld->fPhase ^ pNew->fPhase );
+    if ( p->pPars->fPolarFlip )
+    {
+        if ( pOld->fPhase )  pLits[0] = lit_neg( pLits[0] );
+        if ( pNew->fPhase )  pLits[1] = lit_neg( pLits[1] );
+    }
+clk = clock();
+    RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, 
+        (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+p->timeSat += clock() - clk;
+    if ( RetValue1 == l_False )
+    {
+p->timeSatUnsat += clock() - clk;
+        pLits[0] = lit_neg( pLits[0] );
+        pLits[1] = lit_neg( pLits[1] );
+        RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
+        assert( RetValue );
+        p->nSatCallsUnsat++;
+    }
+    else if ( RetValue1 == l_True )
+    {
+p->timeSatSat += clock() - clk;
+        p->nSatCallsSat++;
+        return 0;
+    }
+    else // if ( RetValue1 == l_Undef )
+    {
+p->timeSatUndec += clock() - clk;
+        p->nSatFailsReal++;
+        return -1;
+    }
+    // return SAT proof
+    p->nSatProof++;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Constrains two nodes to be equivalent in the SAT solver.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
+{
+    int pLits[2], RetValue;
+
+    // sanity checks
+    assert( !Aig_IsComplement(pNew) );
+    assert( !Aig_IsComplement(pOld) );
+    assert( pNew != pOld );
+
+    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 );
+
+    if ( pOld == Aig_ManConst1(p->pFrames) )
+    {
+        pLits[0] = toLitCond( Ssw_ObjSatNum(p,pOld), !pNew->fPhase );
+        if ( p->pPars->fPolarFlip )
+        {
+            if ( pNew->fPhase )  pLits[0] = lit_neg( pLits[0] );
+        }
+        RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 1 );
+        assert( RetValue );
+    }
+    else
+    {
+        // solve under assumptions
+        // A = 1; B = 0     OR     A = 1; B = 1 
+        pLits[0] = toLitCond( Ssw_ObjSatNum(p,pOld), 0 );
+        pLits[1] = toLitCond( Ssw_ObjSatNum(p,pNew), pOld->fPhase == pNew->fPhase );
+        if ( p->pPars->fPolarFlip )
+        {
+            if ( pOld->fPhase )  pLits[0] = lit_neg( pLits[0] );
+            if ( pNew->fPhase )  pLits[1] = lit_neg( pLits[1] );
+        }
+        pLits[0] = lit_neg( pLits[0] );
+        pLits[1] = lit_neg( pLits[1] );
+        RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
+        assert( RetValue );
+
+        // solve under assumptions
+        // A = 0; B = 1     OR     A = 0; B = 0 
+        pLits[0] = toLitCond( Ssw_ObjSatNum(p,pOld), 1 );
+        pLits[1] = toLitCond( Ssw_ObjSatNum(p,pNew), pOld->fPhase ^ pNew->fPhase );
+        if ( p->pPars->fPolarFlip )
+        {
+            if ( pOld->fPhase )  pLits[0] = lit_neg( pLits[0] );
+            if ( pNew->fPhase )  pLits[1] = lit_neg( pLits[1] );
+        }
+        pLits[0] = lit_neg( pLits[0] );
+        pLits[1] = lit_neg( pLits[1] );
+        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;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/ssw/sswSimSat.c b/src/aig/ssw/sswSimSat.c
new file mode 100644
index 00000000..5986c27a
--- /dev/null
+++ b/src/aig/ssw/sswSimSat.c
@@ -0,0 +1,202 @@
+/**CFile****************************************************************
+
+  FileName    [sswSimSat.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Inductive prover with constraints.]
+
+  Synopsis    [Performs resimulation using counter-examples.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - September 1, 2008.]
+
+  Revision    [$Id: sswSimSat.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "sswInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Collects internal nodes in the reverse DFS order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_ManCollectTfoCands_rec( Ssw_Man_t * p, Aig_Obj_t * pObj )
+{
+    Aig_Obj_t * pFanout, * pRepr;
+    int iFanout = -1, i;
+    assert( !Aig_IsComplement(pObj) );
+    if ( Aig_ObjIsTravIdCurrent(p->pAig, pObj) )
+        return;
+    Aig_ObjSetTravIdCurrent(p->pAig, pObj);
+    // traverse the fanouts
+    Aig_ObjForEachFanout( p->pAig, pObj, pFanout, iFanout, i )
+        Ssw_ManCollectTfoCands_rec( p, pFanout );
+    // check if the given node has a representative
+    pRepr = Aig_ObjRepr( p->pAig, pObj );
+    if ( pRepr == NULL )
+        return;
+    // pRepr is the constant 1 node
+    if ( pRepr == Aig_ManConst1(p->pAig) )
+    {
+        Vec_PtrPush( p->vSimRoots, pObj );
+        return;
+    }
+    // pRepr is the representative of the equivalence class
+    if ( Aig_ObjIsTravIdCurrent(p->pAig, pRepr) )
+        return;
+    Aig_ObjSetTravIdCurrent(p->pAig, pRepr);
+    Vec_PtrPush( p->vSimClasses, pRepr );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collect equivalence classes and const1 cands in the TFO.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+ 
+***********************************************************************/
+void Ssw_ManCollectTfoCands( Ssw_Man_t * p, Aig_Obj_t * pObj1, Aig_Obj_t * pObj2 )
+{
+    Vec_PtrClear( p->vSimRoots );
+    Vec_PtrClear( p->vSimClasses );
+    Aig_ManIncrementTravId( p->pAig );
+    Aig_ObjSetTravIdCurrent( p->pAig, Aig_ManConst1(p->pAig) );    
+    Ssw_ManCollectTfoCands_rec( p, pObj1 );
+    Ssw_ManCollectTfoCands_rec( p, pObj2 );
+    Vec_PtrSort( p->vSimRoots,   Aig_ObjCompareIdIncrease );
+    Vec_PtrSort( p->vSimClasses, Aig_ObjCompareIdIncrease );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Resimulates the cone of influence of the solved nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+ 
+***********************************************************************/
+void Ssw_ManResimulateSolved_rec( Ssw_Man_t * p, Aig_Obj_t * pObj, int f )
+{
+    if ( Aig_ObjIsTravIdCurrent(p->pAig, pObj) )
+        return;
+    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 );
+        return;
+    }
+    Ssw_ManResimulateSolved_rec( p, Aig_ObjFanin0(pObj), f );
+    Ssw_ManResimulateSolved_rec( p, Aig_ObjFanin1(pObj), f );
+    pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) )
+                 & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Resimulates the cone of influence of the other nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_ManResimulateOther_rec( Ssw_Man_t * p, Aig_Obj_t * pObj )
+{
+    if ( Aig_ObjIsTravIdCurrent(p->pAig, pObj) )
+        return;
+    Aig_ObjSetTravIdCurrent(p->pAig, pObj);
+    if ( Aig_ObjIsPi(pObj) )
+    {
+        // set random value
+        pObj->fMarkB = Aig_ManRandom(0) & 1;
+        return;
+    }
+    Ssw_ManResimulateOther_rec( p, Aig_ObjFanin0(pObj) );
+    Ssw_ManResimulateOther_rec( p, Aig_ObjFanin1(pObj) );
+    pObj->fMarkB = ( Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj) )
+                 & ( Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Handle the counter-example.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_ManResimulateCex( Ssw_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr, int f )
+{
+    Aig_Obj_t * pRoot, ** ppClass;
+    int i, k, nSize, RetValue1, RetValue2, clk = clock();
+    // get the equivalence classes
+    Ssw_ManCollectTfoCands( p, pObj, pRepr );
+    // resimulate the cone of influence of the solved nodes
+    Aig_ManIncrementTravId( p->pAig );
+    Aig_ObjSetTravIdCurrent( p->pAig, Aig_ManConst1(p->pAig) );
+    Ssw_ManResimulateSolved_rec( p, pObj, f );
+    Ssw_ManResimulateSolved_rec( p, pRepr, f );
+    // resimulate the cone of influence of the other nodes
+    Vec_PtrForEachEntry( p->vSimRoots, pRoot, i )
+        Ssw_ManResimulateOther_rec( p, pRoot );
+    // refine these nodes
+    RetValue1 = Ssw_ClassesRefineConst1Group( p->ppClasses, p->vSimRoots, 0 );
+    // resimulate the cone of influence of the cand classes
+    RetValue2 = 0;
+    Vec_PtrForEachEntry( p->vSimClasses, pRoot, i )
+    {
+        ppClass = Ssw_ClassesReadClass( p->ppClasses, pRoot, &nSize );
+        for ( k = 0; k < nSize; k++ )
+            Ssw_ManResimulateOther_rec( p, ppClass[k] );
+        // refine this class
+        RetValue2 += Ssw_ClassesRefineOneClass( p->ppClasses, pRoot, 0 );
+    }
+    // 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
new file mode 100644
index 00000000..18796b20
--- /dev/null
+++ b/src/aig/ssw/sswSweep.c
@@ -0,0 +1,204 @@
+/**CFile****************************************************************
+
+  FileName    [sswSweep.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Inductive prover with constraints.]
+
+  Synopsis    [One round of SAT sweeping.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - September 1, 2008.]
+
+  Revision    [$Id: sswSweep.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "sswInt.h"
+#include "bar.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Performs fraiging for one node.]
+
+  Description [Returns the fraiged node.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_ManSweepNode( Ssw_Man_t * p, Aig_Obj_t * pObj, int f )
+{ 
+    Aig_Obj_t * pObjRepr, * pObjFraig, * pObjFraig2, * pObjReprFraig;
+    int RetValue;
+    // get representative of this class
+    pObjRepr = Aig_ObjRepr( p->pAig, pObj );
+    if ( pObjRepr == NULL )
+        return;
+    // get the fraiged node
+    pObjFraig = Ssw_ObjFraig( p, pObj, f );
+    if ( pObjFraig == NULL )
+        return;
+    // get the fraiged representative
+    pObjReprFraig = Ssw_ObjFraig( p, pObjRepr, f );
+    if ( pObjReprFraig == NULL )
+        return;
+    // if the fraiged nodes are the same, return
+    if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) )
+    {
+        // remember the proved equivalence
+//        p->pReprsProved[ pObj->Id ] = pObjRepr;
+        return;
+    }
+    assert( Aig_Regular(pObjFraig) != Aig_ManConst1(p->pFrames) );
+    RetValue = Ssw_NodesAreEquiv( p, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) );
+    if ( RetValue == -1 ) // timed out
+    {
+        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 );
+        // remember the proved equivalence
+//        p->pReprsProved[ pObj->Id ] = pObjRepr;
+        return;
+    }
+    // disproved the equivalence
+    Ssw_ManResimulateCex( p, pObj, pObjRepr, f );
+    assert( Aig_ObjRepr( p->pAig, pObj ) != pObjRepr );
+    p->fRefined = 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs fraiging for the internal nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ssw_ManSweepBmc( Ssw_Man_t * p )
+{
+    Bar_Progress_t * pProgress = NULL;
+    Aig_Obj_t * pObj, * pObjNew;
+    int i, f, clk;
+clk = clock();
+
+    // start initialized timeframes
+    p->pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->pPars->nFramesK );
+    Saig_ManForEachLo( p->pAig, pObj, i )
+        Ssw_ObjSetFraig( p, pObj, 0, Aig_ManConst0(p->pFrames) );
+
+    // sweep internal nodes
+    p->fRefined = 0;
+    pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) * p->pPars->nFramesK );
+    for ( f = 0; f < p->pPars->nFramesK; f++ )
+    {
+        // map constants and PIs
+        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) );
+        // sweep internal nodes
+        Aig_ManForEachNode( p->pAig, pObj, i )
+        {
+            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 );
+
+    // cleanup
+    Ssw_ClassesCheck( p->ppClasses );
+    Ssw_ManCleanup( p );
+p->timeBmc += clock() - clk;
+    return p->fRefined;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs fraiging for the internal nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ssw_ManSweep( Ssw_Man_t * p )
+{
+    Bar_Progress_t * pProgress = NULL;
+    Aig_Obj_t * pObj, * pObj2, * pObjNew;
+    int nConstrPairs, clk, i, f = p->pPars->nFramesK;
+
+    // perform speculative reduction
+clk = clock();
+    // create timeframes
+    p->pFrames = Ssw_FramesWithClasses( p );
+    p->nFrameNodes = Aig_ManNodeNum( p->pFrames );
+    // add constraints
+    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) );
+    }
+    // build logic cones for register inputs
+    for ( i = 0; i < Aig_ManRegNum(p->pAig); i++ )
+    {
+        pObj  = Aig_ManPo( p->pFrames, nConstrPairs + i );
+        Ssw_CnfNodeAddToSolver( p, Aig_ObjFanin0(pObj) );
+    }
+    sat_solver_simplify( p->pSat );
+p->timeReduce += clock() - clk;
+
+    // map constants and PIs
+    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) );
+    // sweep internal nodes
+    p->fRefined = 0;
+    pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) );
+    Aig_ManForEachNode( 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 );
+    }
+    Bar_ProgressStop( pProgress );
+
+    // cleanup
+    Ssw_ClassesCheck( p->ppClasses );
+    Ssw_ManCleanup( p );
+    return p->fRefined;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 26f97b78..90ee04b2 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -36,6 +36,7 @@
 #include "nwkMerge.h"
 #include "int.h"
 #include "dch.h"
+#include "ssw.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -190,6 +191,7 @@ static int Abc_CommandFlowRetime     ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandSeqFpga        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSeqMap         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSeqSweep       ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandSeqSweep2      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSeqSweepTest   ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandLcorr          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSeqCleanup     ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -451,7 +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",   "ssweep",        Abc_CommandSeqSweep,         1 );
+    Cmd_CommandAdd( pAbc, "Sequential",   "ssw",           Abc_CommandSeqSweep,         1 );
+    Cmd_CommandAdd( pAbc, "Sequential",   "ssw2",          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 );
@@ -13479,7 +13482,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: ssw [-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 );
@@ -13509,6 +13512,175 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk, * pNtkRes;
+    Ssw_Pars_t Pars, * pPars = &Pars;
+    int c;
+    extern Abc_Ntk_t * Abc_NtkDarSeqSweep2( Abc_Ntk_t * pNtk, Ssw_Pars_t * pPars );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    Ssw_ManSetDefaultParams( pPars );
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "PQFCLNplvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'P':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "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( pErr, "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( pErr, "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( pErr, "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( pErr, "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( pErr, "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 'p':
+            pPars->fPolarFlip ^= 1;
+            break;
+        case 'l':
+            pPars->fLatchCorr ^= 1;
+            break;
+        case 'v':
+            pPars->fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+
+    if ( Abc_NtkIsComb(pNtk) )
+    {
+        fprintf( pErr, "The network is combinational (run \"fraig\" or \"fraig_sweep\").\n" );
+        return 0;
+    }
+
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        printf( "This command works only for structrally hashed networks. Run \"st\".\n" );
+        return 0;
+    }
+/*
+    if ( pPars->nFramesK > 1 && pPars->fUse1Hot )
+    {
+        printf( "Currrently can only use one-hotness for simple induction (K=1).\n" );
+        return 0;
+    }
+
+    if ( pPars->nFramesP && pPars->fUse1Hot )
+    {
+        printf( "Currrently can only use one-hotness without prefix.\n" );
+        return 0;
+    }
+*/
+    // get the new network
+    pNtkRes = Abc_NtkDarSeqSweep2( pNtk, pPars );
+    if ( pNtkRes == NULL )
+    {
+        fprintf( pErr, "Sequential sweeping has failed.\n" );
+        return 1;
+    }
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: ssw2 [-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 );
+    fprintf( pErr, "\t-F num : number of time frames for induction (1=simple) [default = %d]\n", pPars->nFramesK );
+    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-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-v     : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandSeqSweepTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     char * pFileName;
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 16215a64..a0284a17 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -27,6 +27,7 @@
 #include "fraig.h"
 #include "int.h"
 #include "dch.h"
+#include "ssw.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -1238,6 +1239,45 @@ PRT( "Initial fraiging time", clock() - clk );
 
 /**Function*************************************************************
 
+  Synopsis    [Gives the current ABC network to AIG manager for processing.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkDarSeqSweep2( Abc_Ntk_t * pNtk, Ssw_Pars_t * pPars )
+{
+    Abc_Ntk_t * pNtkAig;
+    Aig_Man_t * pMan, * pTemp;
+
+    pMan = Abc_NtkToDar( pNtk, 0, 1 );
+    if ( pMan == NULL )
+        return NULL;
+
+    pMan = Ssw_SignalCorrespondence( pTemp = pMan, pPars );
+    Aig_ManStop( pTemp );
+    if ( pMan == NULL )
+        return NULL;
+
+    if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) )
+        pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
+    else
+    {
+        Abc_Obj_t * pObj;
+        int i;
+        pNtkAig = Abc_NtkFromDar( pNtk, pMan );
+        Abc_NtkForEachLatch( pNtkAig, pObj, i )
+            Abc_LatchSetInit0( pObj );
+    }
+    Aig_ManStop( pMan );
+    return pNtkAig;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Computes latch correspondence.]
 
   Description [] 
diff --git a/src/map/if/ifMan.c b/src/map/if/ifMan.c
index 015e3d31..35b0cccc 100644
--- a/src/map/if/ifMan.c
+++ b/src/map/if/ifMan.c
@@ -524,7 +524,7 @@ void If_ManDerefChoiceCutSet( If_Man_t * p, If_Obj_t * pObj )
     // consider the nodes in the choice class
     for ( pTemp = pObj; pTemp; pTemp = pTemp->pEquiv )
     {
-        assert( pTemp == pObj || pTemp->nVisits == 1 );
+//        assert( pTemp == pObj || pTemp->nVisits == 1 );
         if ( --pTemp->nVisits == 0 )
         {
 //            Mem_FixedEntryRecycle( p->pMemSet, (char *)pTemp->pCutSet );