diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 564cb399b..baf0d7eec 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -37232,13 +37232,15 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     extern Gia_Man_t * Cec_ManScorrCorrespondence( Gia_Man_t * p, Cec_ParCor_t * pPars );
     extern Gia_Man_t * Gia_ManScorrDivideTest( Gia_Man_t * p, Cec_ParCor_t * pPars );
+    extern Gia_Man_t * Gia_SignalCorrespondencePart( Gia_Man_t * p, Cec_ParCor_t * pPars );
     Cec_ParCor_t Pars, * pPars = &Pars;
     Gia_Man_t * pTemp;
     int fPartition = 0;
     int fUseOld = 0, c;
     Cec_ManCorSetDefaultParams( pPars );
+    pPars->nProcs = 1;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "FCPXpkrecqowvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "FCGXPSpkrecqowvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -37264,7 +37266,7 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nBTLimit < 0 )
                 goto usage;
             break;
-        case 'P':
+        case 'G':
             if ( globalUtilOptind >= argc )
             {
                 Abc_Print( -1, "Command line switch \"-P\" should be followed by an integer.\n" );
@@ -37286,6 +37288,28 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nLimitMax < 0 )
                 goto usage;
             break;
+        case 'P':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-P\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nProcs = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nProcs < 0 )
+                goto usage;
+            break;
+        case 'S':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nPartSize = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nPartSize < 0 )
+                goto usage;
+            break;            
         case 'p':
             fPartition ^= 1;
             break;
@@ -37338,7 +37362,9 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( 0, "The network is combinational.\n" );
         return 0;
     }
-    if ( fUseOld )
+    if ( pPars->nPartSize > 0 )
+        pTemp = Gia_SignalCorrespondencePart( pAbc->pGia, pPars );
+    else if ( fUseOld )
         pTemp = Cec_ManScorrCorrespondence( pAbc->pGia, pPars );
     else if ( fPartition )
         pTemp = Gia_ManScorrDivideTest( pAbc->pGia, pPars );
@@ -37348,12 +37374,14 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &scorr [-FCPX num] [-pkrecqowvh]\n" );
+    Abc_Print( -2, "usage: &scorr [-FCGXPS num] [-pkrecqowvh]\n" );
     Abc_Print( -2, "\t         performs signal correpondence computation\n" );
     Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
     Abc_Print( -2, "\t-F num : the number of timeframes in inductive case [default = %d]\n", pPars->nFrames );
-    Abc_Print( -2, "\t-P num : the number of timeframes in the prefix [default = %d]\n", pPars->nPrefix );
+    Abc_Print( -2, "\t-G num : the number of timeframes in the prefix [default = %d]\n", pPars->nPrefix );
     Abc_Print( -2, "\t-X num : the number of iterations of little or no improvement [default = %d]\n", pPars->nLimitMax );
+    Abc_Print( -2, "\t-P num : the number of concurrent processes [default = %d]\n", pPars->nProcs );
+    Abc_Print( -2, "\t-S num : the number of flops in one partition [default = %d]\n", pPars->nPartSize );
     Abc_Print( -2, "\t-p     : toggle using partitioning for the input AIG [default = %s]\n", fPartition? "yes": "no" );
     Abc_Print( -2, "\t-k     : toggle using constant correspondence [default = %s]\n", pPars->fConstCorr? "yes": "no" );
     Abc_Print( -2, "\t-r     : toggle using implication rings during refinement [default = %s]\n", pPars->fUseRings? "yes": "no" );
diff --git a/src/proof/cec/cec.h b/src/proof/cec/cec.h
index 92a08b3ef..d11bca3c3 100644
--- a/src/proof/cec/cec.h
+++ b/src/proof/cec/cec.h
@@ -147,6 +147,8 @@ struct Cec_ParCor_t_
     int              nFrames;       // the number of time frames
     int              nPrefix;       // the number of time frames in the prefix
     int              nBTLimit;      // conflict limit at a node
+    int              nProcs;        // the number of processes
+    int              nPartSize;     // the partition size
     int              nLevelMax;     // (scorr only) the max number of levels
     int              nStepsMax;     // (scorr only) the max number of induction steps
     int              nLimitMax;     // (scorr only) stop after this many iterations if little or no improvement
diff --git a/src/proof/ssw/ssw.h b/src/proof/ssw/ssw.h
index c8275b7a3..7299e37d1 100644
--- a/src/proof/ssw/ssw.h
+++ b/src/proof/ssw/ssw.h
@@ -42,6 +42,7 @@ struct Ssw_Pars_t_
 {
     int              nPartSize;     // size of the partition
     int              nOverSize;     // size of the overlap between partitions
+    int              nProcs;        // the number of processors
     int              nFramesK;      // the induction depth
     int              nFramesAddSim; // the number of additional frames to simulate
     int              fConstrs;      // treat the last nConstrs POs as seq constraints
diff --git a/src/proof/ssw/sswPart.c b/src/proof/ssw/sswPart.c
index 30afddcae..0c6e54cef 100644
--- a/src/proof/ssw/sswPart.c
+++ b/src/proof/ssw/sswPart.c
@@ -20,10 +20,23 @@
 
 #include "sswInt.h"
 #include "aig/ioa/ioa.h"
+#include "aig/gia/giaAig.h"
+#include "proof/cec/cec.h"
+
+#ifdef ABC_USE_PTHREADS
+
+#ifdef _WIN32
+#include "../lib/pthread.h"
+#else
+#include <pthread.h>
+#include <unistd.h>
+#endif
+
+#endif
+
 
 ABC_NAMESPACE_IMPL_START
 
-
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -32,6 +45,141 @@ ABC_NAMESPACE_IMPL_START
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+/**Function*************************************************************
+
+  Synopsis    [Performing SAT sweeping for the array of AIGs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ssw_SignalCorrespondenceArray1( Vec_Ptr_t * vGias, Ssw_Pars_t * pPars )
+{
+    Gia_Man_t * pGia; int i;
+    Cec_ParCor_t CorPars, * pCorPars = &CorPars;
+    Cec_ManCorSetDefaultParams( pCorPars );
+    pCorPars->nBTLimit  = pPars->nBTLimit;
+    pCorPars->fVerbose  = pPars->fVerbose;
+    pCorPars->fUseCSat  = 1; 
+    Vec_PtrForEachEntry( Gia_Man_t *, vGias, pGia, i )
+        if ( Gia_ManPiNum(pGia) > 0 )
+            Cec_ManLSCorrespondenceClasses( pGia, pCorPars );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performing SAT sweeping for the array of AIGs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+#ifndef ABC_USE_PTHREADS
+
+void Ssw_SignalCorrespondenceArray( Vec_Ptr_t * vGias, Ssw_Pars_t * pPars )
+{
+    Ssw_SignalCorrespondenceArray1( vGias, pPars );
+}
+
+#else // pthreads are used
+
+
+#define PAR_THR_MAX 100
+typedef struct Par_ScorrThData_t_
+{
+    Cec_ParCor_t CorPars;
+    Gia_Man_t *  p;
+    int *        pMap;
+    int          iThread;
+    int          nTimeOut;
+    int          fWorking;
+} Par_ScorrThData_t;
+
+void * Ssw_GiaWorkerThread( void * pArg )
+{
+    Par_ScorrThData_t * pThData = (Par_ScorrThData_t *)pArg;
+    volatile int * pPlace = &pThData->fWorking;
+    while ( 1 )
+    {
+        while ( *pPlace == 0 );
+        assert( pThData->fWorking );
+        if ( pThData->p == NULL )
+        {
+            pthread_exit( NULL );
+            assert( 0 );
+            return NULL;
+        }
+        Cec_ManLSCorrespondenceClasses( pThData->p, &pThData->CorPars );
+        pThData->fWorking = 0;
+    }
+    assert( 0 );
+    return NULL;
+}
+
+void Ssw_SignalCorrespondenceArray( Vec_Ptr_t * vGias, Ssw_Pars_t * pPars )
+{
+    //abctime clkTotal = Abc_Clock();
+    Par_ScorrThData_t ThData[PAR_THR_MAX];
+    pthread_t WorkerThread[PAR_THR_MAX];
+    int i, status, nProcs = pPars->nProcs;
+    Vec_Ptr_t * vStack;
+    Cec_ParCor_t CorPars, * pCorPars = &CorPars;
+    Cec_ManCorSetDefaultParams( pCorPars );
+    if ( pPars->fVerbose )
+        printf( "Running concurrent &scorr with %d processes.\n", nProcs );
+    fflush( stdout );
+    if ( pPars->nProcs < 2 )
+        return Ssw_SignalCorrespondenceArray1( vGias, pPars );
+    // subtract manager thread
+    nProcs--;
+    assert( nProcs >= 1 && nProcs <= PAR_THR_MAX );
+    // start threads
+    for ( i = 0; i < nProcs; i++ )
+    {
+        ThData[i].CorPars  = *pCorPars;
+        ThData[i].iThread  = i;
+        //ThData[i].nTimeOut = pPars->nTimeOut;
+        ThData[i].fWorking = 0;
+        status = pthread_create( WorkerThread + i, NULL, Ssw_GiaWorkerThread, (void *)(ThData + i) );  assert( status == 0 );
+    }
+    // look at the threads
+    vStack = Vec_PtrDup( vGias );
+    while ( Vec_PtrSize(vStack) > 0 )
+    {
+        for ( i = 0; i < nProcs; i++ )
+        {
+            if ( ThData[i].fWorking )
+                continue;
+            ThData[i].p = (Gia_Man_t*)Vec_PtrPop( vStack );
+            ThData[i].fWorking = 1;   
+            break;
+        }
+    }
+    Vec_PtrFree( vStack );    
+    // wait till threads finish
+    for ( i = 0; i < nProcs; i++ )
+        if ( ThData[i].fWorking )
+            i = -1;
+    // stop threads
+    for ( i = 0; i < nProcs; i++ )
+    {
+        assert( !ThData[i].fWorking );
+        // stop
+        ThData[i].p = NULL;
+        ThData[i].fWorking = 1;
+    }
+
+}
+
+#endif // pthreads are used
+
+
 /**Function*************************************************************
 
   Synopsis    [Performs partitioned sequential SAT sweeping.]
@@ -45,7 +193,7 @@ ABC_NAMESPACE_IMPL_START
 ***********************************************************************/
 Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
 {
-    int fPrintParts = 0;
+    int fPrintParts = 1;
     char Buffer[100];
     Aig_Man_t * pTemp, * pNew;
     Vec_Ptr_t * vResult;
@@ -132,6 +280,143 @@ Aig_Man_t * Ssw_SignalCorrespondencePart( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    [Performs partitioned sequential SAT sweeping.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Ssw_SignalCorrespondencePart2( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
+{
+    int fPrintParts = 1;
+    //char Buffer[100];
+    Aig_Man_t * pTemp, * pNew;
+    Vec_Ptr_t * vAigs;    
+    Vec_Ptr_t * vGias;
+    Vec_Ptr_t * vMaps;
+    Vec_Ptr_t * vResult;
+    Vec_Int_t * vPart;
+    int * pMapBack = NULL;
+    int i, nCountPis, nCountRegs;
+    int nClasses, nPartSize, fVerbose;
+    abctime clk = Abc_Clock();
+    if ( pPars->fConstrs )
+    {
+        Abc_Print( 1, "Cannot use partitioned computation with constraints.\n" );
+        return NULL;
+    }
+    // save parameters
+    nPartSize = pPars->nPartSize; pPars->nPartSize = 0;
+    fVerbose  = pPars->fVerbose;  pPars->fVerbose  = 0;
+    // generate partitions
+    if ( pAig->vClockDoms )
+    {
+        // divide large clock domains into separate partitions
+        vResult = Vec_PtrAlloc( 100 );
+        Vec_PtrForEachEntry( Vec_Int_t *, (Vec_Ptr_t *)pAig->vClockDoms, vPart, i )
+        {
+            if ( nPartSize && Vec_IntSize(vPart) > nPartSize )
+                Aig_ManPartDivide( vResult, vPart, nPartSize, pPars->nOverSize );
+            else
+                Vec_PtrPush( vResult, Vec_IntDup(vPart) );
+        }
+    }
+    else
+        vResult = Aig_ManRegPartitionSimple( pAig, nPartSize, pPars->nOverSize );
+//    vResult = Aig_ManPartitionSmartRegisters( pAig, nPartSize, 0 ); 
+//    vResult = Aig_ManRegPartitionSmart( pAig, nPartSize );
+    // collect partitions
+    vAigs = Vec_PtrAlloc( 100 );
+    vGias = Vec_PtrAlloc( 100 );
+    vMaps = Vec_PtrAlloc( 100 );
+    if ( fPrintParts )
+        Abc_Print( 1, "Simple partitioning. %d partitions are saved:\n", Vec_PtrSize(vResult) );
+    Vec_PtrForEachEntry( Vec_Int_t *, vResult, vPart, i )
+    {
+        pTemp = Aig_ManRegCreatePart( pAig, vPart, &nCountPis, &nCountRegs, &pMapBack );
+        Aig_ManSetRegNum( pTemp, pTemp->nRegs );
+        Vec_PtrPush( vAigs, pTemp );
+        Vec_PtrPush( vGias, Gia_ManFromAigSimple(pTemp) );
+        Vec_PtrPush( vMaps, pMapBack );
+        //sprintf( Buffer, "part%03d.aig", i );
+        //Ioa_WriteAiger( pTemp, Buffer, 0, 0 );
+        if ( fPrintParts )
+            Abc_Print( 1, "part%03d.aig : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d.\n",
+                i, Vec_IntSize(vPart), Aig_ManCiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Aig_ManNodeNum(pTemp) );
+    }
+    // solve partitions
+    Ssw_SignalCorrespondenceArray( vGias, pPars );
+    // collect the results
+    Aig_ManReprStart( pAig, Aig_ManObjNumMax(pAig) );
+    Vec_PtrForEachEntry( Vec_Int_t *, vResult, vPart, i )
+    {
+        int * pMapBack = (int *)Vec_PtrEntry( vMaps, i );
+        Gia_Man_t * pGia = (Gia_Man_t *)Vec_PtrEntry( vGias, i );
+        Aig_Man_t * pTemp2 = Gia_ManToAigSimple( pGia );
+        pTemp = (Aig_Man_t *)Vec_PtrEntry( vAigs, i );
+        Gia_ManReprToAigRepr2( pTemp2, pGia );
+        // remap back
+        nClasses = Aig_TransferMappedClasses( pAig, pTemp2, pMapBack );
+        if ( fVerbose )
+            Abc_Print( 1, "%3d : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d. It = %3d. Cl = %5d.\n",
+                i, Vec_IntSize(vPart), Aig_ManCiNum(pTemp)-Vec_IntSize(vPart), 0, 0, Aig_ManNodeNum(pTemp), 0, nClasses );
+        Aig_ManStop( pTemp );
+        Aig_ManStop( pTemp2 );
+        Gia_ManStop( pGia );
+        ABC_FREE( pMapBack );
+    }
+    Vec_PtrFree( vAigs );
+    Vec_PtrFree( vGias );
+    Vec_PtrFree( vMaps );
+
+    // remap the AIG
+    pNew = Aig_ManDupRepr( pAig, 0 );
+    Aig_ManSeqCleanup( pNew );
+//    Aig_ManPrintStats( pAig );
+//    Aig_ManPrintStats( pNew );
+    Vec_VecFree( (Vec_Vec_t *)vResult );
+    pPars->nPartSize = nPartSize;
+    pPars->fVerbose = fVerbose;
+    if ( fVerbose )
+    {
+        ABC_PRT( "Total time", Abc_Clock() - clk );
+    }
+    return pNew;
+}
+void Gia_ManRestoreNodeMapping( Aig_Man_t * pAig, Gia_Man_t * pGia )
+{
+    Aig_Obj_t * pObjAig; int i;
+    assert( Gia_ManObjNum(pGia) == Aig_ManObjNum(pAig) );
+    Aig_ManForEachObj( pAig, pObjAig, i )
+        pObjAig->iData = Abc_Var2Lit(i, 0);
+}
+Gia_Man_t * Gia_SignalCorrespondencePart( Gia_Man_t * p, Cec_ParCor_t * pPars )
+{
+    Gia_Man_t * pRes = NULL;
+    Aig_Man_t * pNew = NULL;
+    Aig_Man_t * pAig = Gia_ManToAigSimple(p);
+    Ssw_Pars_t SswPars, * pSswPars = &SswPars;
+    assert( pPars->nProcs > 0 );
+    assert( pPars->nPartSize > 0 );
+    Ssw_ManSetDefaultParams( pSswPars ); 
+    pSswPars->nBTLimit  = pPars->nBTLimit;
+    pSswPars->nProcs    = pPars->nProcs;
+    pSswPars->nPartSize = pPars->nPartSize;
+    pSswPars->fVerbose  = pPars->fVerbose;
+    pNew = Ssw_SignalCorrespondencePart2( pAig, pSswPars );
+    Gia_ManRestoreNodeMapping( pAig, p );
+    Gia_ManReprFromAigRepr2( pAig, p );
+    pRes = Gia_ManFromAigSimple(pNew);
+    Aig_ManStop( pNew );
+    Aig_ManStop( pAig );
+    return pRes;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////