diff --git a/abclib.dsp b/abclib.dsp
index 7433c5139..3255424db 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -5627,6 +5627,10 @@ SOURCE=.\src\proof\cec\cecPat.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\proof\cec\cecProve.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\proof\cec\cecSat.c
 # End Source File
 # Begin Source File
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index dab6770bb..654f2faa5 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -1530,7 +1530,7 @@ extern void                Gia_ManPrintStatsMiter( Gia_Man_t * p, int fVerbose )
 extern void                Gia_ManSetRegNum( Gia_Man_t * p, int nRegs );
 extern void                Gia_ManReportImprovement( Gia_Man_t * p, Gia_Man_t * pNew );
 extern void                Gia_ManPrintNpnClasses( Gia_Man_t * p );
-extern void                Gia_ManDumpVerilog( Gia_Man_t * p, char * pFileName, Vec_Int_t * vObjs, int fVerBufs, int fInter, int fInterComb );
+extern void                Gia_ManDumpVerilog( Gia_Man_t * p, char * pFileName, Vec_Int_t * vObjs, int fVerBufs, int fInter, int fInterComb, int fAssign );
 /*=== giaMem.c ===========================================================*/
 extern Gia_MmFixed_t *     Gia_MmFixedStart( int nEntrySize, int nEntriesMax );
 extern void                Gia_MmFixedStop( Gia_MmFixed_t * p, int fVerbose );
diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c
index 2449b5df7..e771f99cc 100644
--- a/src/aig/gia/giaMan.c
+++ b/src/aig/gia/giaMan.c
@@ -1408,7 +1408,32 @@ void Gia_ManWriteNames( FILE * pFile, char c, int n, Vec_Ptr_t * vNames, int Sta
         fFirst = 0;
     }
 }
-void Gia_ManDumpVerilog( Gia_Man_t * p, char * pFileName, Vec_Int_t * vObjs, int fVerBufs, int fInter, int fInterComb )
+void Gia_ManDumpVerilog( Gia_Man_t * p, char * pFileName, Vec_Int_t * vObjs, int fVerBufs, int fInter, int fInterComb, int fAssign )
+{
+    if ( fInterComb ) 
+    {
+        if ( fAssign ) {
+            extern void Gia_ManDumpInterfaceAssign( Gia_Man_t * p, char * pFileName );
+            Gia_ManDumpInterfaceAssign( p, pFileName );
+        }
+        else {
+            extern void Gia_ManDumpInterface( Gia_Man_t * p, char * pFileName );
+            Gia_ManDumpInterface( p, pFileName );
+        }
+    }
+    else
+    {
+        if ( fAssign ) {
+            extern void Gia_ManDumpVerilogNoInterAssign( Gia_Man_t * p, char * pFileName, Vec_Int_t * vObjs, int fVerBufs, int fInter );
+            Gia_ManDumpVerilogNoInterAssign( p, pFileName, vObjs, fVerBufs, fInter );
+        }
+        else {
+            extern void Gia_ManDumpVerilogNoInter( Gia_Man_t * p, char * pFileName, Vec_Int_t * vObjs, int fVerBufs, int fInter );
+            Gia_ManDumpVerilogNoInter( p, pFileName, vObjs, fVerBufs, fInter );
+        }
+    }
+}
+void Gia_ManDumpVerilogNoInter( Gia_Man_t * p, char * pFileName, Vec_Int_t * vObjs, int fVerBufs, int fInter )
 {
     Gia_Obj_t * pObj;
     Vec_Bit_t * vInvs, * vUsed;
@@ -1416,13 +1441,6 @@ void Gia_ManDumpVerilog( Gia_Man_t * p, char * pFileName, Vec_Int_t * vObjs, int
     int nDigitsI = Abc_Base10Log( Gia_ManPiNum(p) );
     int nDigitsO = Abc_Base10Log( Gia_ManPoNum(p) );
     int i, k, iObj, nRegs = Gia_ManRegNum(p);
-    if ( fInterComb ) 
-    {
-        extern void Gia_ManDumpInterface( Gia_Man_t * p, char * pFileName );
-        Gia_ManDumpInterface( p, pFileName );
-        return;
-    }
-
     FILE * pFile = fopen( pFileName, "wb" );
     if ( pFile == NULL )
     {
@@ -1595,6 +1613,179 @@ void Gia_ManDumpVerilog( Gia_Man_t * p, char * pFileName, Vec_Int_t * vObjs, int
 
     Gia_ManSetRegNum( p, nRegs );
 }
+void Gia_ManDumpVerilogNoInterAssign( Gia_Man_t * p, char * pFileName, Vec_Int_t * vObjs, int fVerBufs, int fInter )
+{
+    Gia_Obj_t * pObj;
+    Vec_Bit_t * vInvs, * vUsed;
+    int nDigits  = Abc_Base10Log( Gia_ManObjNum(p) );
+    int nDigitsI = Abc_Base10Log( Gia_ManPiNum(p) );
+    int nDigitsO = Abc_Base10Log( Gia_ManPoNum(p) );
+    int i, k, iObj, nRegs = Gia_ManRegNum(p);
+    FILE * pFile = fopen( pFileName, "wb" );
+    if ( pFile == NULL )
+    {
+        printf( "Cannot open output file \"%s\".\n", pFileName );
+        return;
+    }
+
+    if ( fInter || nRegs ) 
+        Gia_ManDumpInterface2( p, pFile );
+    //Gia_ManSetRegNum( p, 0 );
+    p->nRegs = 0;
+
+    vInvs = Gia_ManGenUsed( p, 0 );
+    vUsed = Gia_ManGenUsed( p, 1 );
+
+    //fprintf( pFile, "// This Verilog file is written by ABC on %s\n\n", Extra_TimeStamp() );
+
+    fprintf( pFile, "module " );
+    Gia_ManDumpModuleName( pFile, p->pName );
+
+    if ( fVerBufs )
+    {
+        fprintf( pFile, " (\n    " );
+        Gia_ManWriteNames( pFile, 'a', Gia_ManPiNum(p), NULL, 4, 4, NULL );
+        fprintf( pFile, ",\n    " );
+
+        Gia_ManWriteNames( pFile, 'y', Gia_ManPoNum(p), NULL, 4, 4, NULL );
+        fprintf( pFile, "\n  );\n\n" );
+
+        fprintf( pFile, "  input " );
+        Gia_ManWriteNames( pFile, 'a', Gia_ManPiNum(p), NULL, 8, 4, NULL );
+        fprintf( pFile, ";\n\n" );
+
+        fprintf( pFile, "  output " );
+        Gia_ManWriteNames( pFile, 'y', Gia_ManPoNum(p), NULL, 9, 4, NULL );
+        fprintf( pFile, ";\n\n" );
+
+        fprintf( pFile, "  wire " );
+        Gia_ManWriteNames( pFile, 'x', Gia_ManPiNum(p), p->vNamesIn, 8, 4, NULL );
+        fprintf( pFile, ";\n\n" );
+
+        fprintf( pFile, "  wire " );
+        Gia_ManWriteNames( pFile, 'z', Gia_ManPoNum(p), p->vNamesOut, 9, 4, NULL );
+        fprintf( pFile, ";\n\n" );
+
+        Gia_ManForEachPi( p, pObj, i )
+        {
+            fprintf( pFile, "  assign %s =", Gia_ObjGetDumpName(p->vNamesIn, 'x', i, nDigitsI) );
+            fprintf( pFile, " %s;\n", Gia_ObjGetDumpName(NULL, 'a', i, nDigitsI) );
+        }
+        fprintf( pFile, "\n" );
+
+        Gia_ManForEachPo( p, pObj, i )
+        {
+            fprintf( pFile, "  assign %s =", Gia_ObjGetDumpName(NULL, 'y', i, nDigitsO) );
+            fprintf( pFile, " %s;\n", Gia_ObjGetDumpName(p->vNamesOut, 'z', i, nDigitsO) );
+        }
+        fprintf( pFile, "\n" );
+    }
+    else
+    {
+        fprintf( pFile, " (\n    " );
+        Gia_ManWriteNames( pFile, 'x', Gia_ManPiNum(p), p->vNamesIn, 4, 4, NULL );
+        fprintf( pFile, ",\n    " );
+
+        Gia_ManWriteNames( pFile, 'z', Gia_ManPoNum(p), p->vNamesOut, 4, 4, NULL );
+        fprintf( pFile, "\n  );\n\n" );
+
+        fprintf( pFile, "  input " );
+        Gia_ManWriteNames( pFile, 'x', Gia_ManPiNum(p), p->vNamesIn, 8, 4, NULL );
+        fprintf( pFile, ";\n\n" );
+
+        fprintf( pFile, "  output " );
+        Gia_ManWriteNames( pFile, 'z', Gia_ManPoNum(p), p->vNamesOut, 9, 4, NULL );
+        fprintf( pFile, ";\n\n" );
+    }
+
+    if ( Vec_BitCount(vUsed) )
+    {
+        fprintf( pFile, "  wire " );
+        Gia_ManWriteNames( pFile, 'n', Gia_ManObjNum(p), NULL, 7, 4, vUsed );
+        fprintf( pFile, ";\n\n" );
+    }
+
+    if ( Vec_BitCount(vInvs) )
+    {
+        fprintf( pFile, "  wire " );
+        Gia_ManWriteNames( pFile, 'i', Gia_ManObjNum(p), NULL, 7, 4, vInvs );
+        fprintf( pFile, ";\n\n" );
+    }
+
+    if ( vObjs )
+    {
+        fprintf( pFile, "  wire " );
+        Vec_IntForEachEntry( vObjs, iObj, i )
+            fprintf( pFile, " t_%d%s", i, i==Vec_IntSize(vObjs)-1 ? "" : "," ); 
+        fprintf( pFile, ";\n\n" );
+        Vec_IntForEachEntry( vObjs, iObj, i )
+        {
+            fprintf( pFile, "  assign %s =", Gia_ObjGetDumpName(NULL, 'n', iObj, nDigits) );
+            fprintf( pFile, " t_%d;\n", i );
+        }
+        fprintf( pFile, "\n" );
+    }
+
+    // input inverters
+    Gia_ManForEachPi( p, pObj, i )
+    {
+        if ( Vec_BitEntry(vUsed, Gia_ObjId(p, pObj)) )
+        {
+            fprintf( pFile, "  assign %s =", Gia_ObjGetDumpName(NULL, 'n', Gia_ObjId(p, pObj), nDigits) );
+            fprintf( pFile, " %s;\n",   Gia_ObjGetDumpName(p->vNamesIn, 'x', i, nDigitsI) );
+        }
+        if ( Vec_BitEntry(vInvs, Gia_ObjId(p, pObj)) )
+        {
+            fprintf( pFile, "  assign %s =", Gia_ObjGetDumpName(NULL, 'i', Gia_ObjId(p, pObj), nDigits) );
+            fprintf( pFile, " ~%s;\n",   Gia_ObjGetDumpName(p->vNamesIn, 'x', i, nDigitsI) );
+        }
+    }
+
+    // internal nodes and their inverters
+    fprintf( pFile, "\n" );
+    Gia_ManForEachAnd( p, pObj, i )
+    {
+        int fSkip = 0;
+        if ( vObjs )
+        {
+            Vec_IntForEachEntry( vObjs, iObj, k )
+                if ( iObj == i )
+                    break;
+            if ( k < Vec_IntSize(vObjs) )
+                fSkip = 1;
+        }
+        if ( !fSkip )
+        {
+            fprintf( pFile, "  assign %s =", Gia_ObjGetDumpName(NULL, 'n', i, nDigits) );
+            fprintf( pFile, " %s &",       Gia_ObjGetDumpName(NULL, (char)(Gia_ObjFaninC0(pObj)? 'i':'n'), Gia_ObjFaninId0(pObj, i), nDigits) );
+            fprintf( pFile, " %s;\n",   Gia_ObjGetDumpName(NULL, (char)(Gia_ObjFaninC1(pObj)? 'i':'n'), Gia_ObjFaninId1(pObj, i), nDigits) );
+        }
+        if ( Vec_BitEntry(vInvs, i) )
+        {
+            fprintf( pFile, "  assign %s =", Gia_ObjGetDumpName(NULL, 'i', i, nDigits) );
+            fprintf( pFile, " ~%s;\n",   Gia_ObjGetDumpName(NULL, 'n', i, nDigits) );
+        }
+    }
+    
+    // output drivers
+    fprintf( pFile, "\n" );
+    Gia_ManForEachPo( p, pObj, i )
+    {
+        fprintf( pFile, "  assign %s = ", Gia_ObjGetDumpName(p->vNamesOut, 'z', i, nDigitsO) );
+        if ( Gia_ObjIsConst0(Gia_ObjFanin0(pObj)) )
+            fprintf( pFile, "1\'b%d;\n", Gia_ObjFaninC0(pObj) );
+        else 
+            fprintf( pFile, "%s;\n", Gia_ObjGetDumpName(NULL, (char)(Gia_ObjFaninC0(pObj)? 'i':'n'), Gia_ObjFaninId0p(p, pObj), nDigits) );
+    }
+
+    fprintf( pFile, "\nendmodule\n\n" );
+    fclose( pFile );
+
+    Vec_BitFree( vInvs );
+    Vec_BitFree( vUsed );
+
+    Gia_ManSetRegNum( p, nRegs );
+}
 
 /**Function*************************************************************
 
@@ -1709,6 +1900,108 @@ void Gia_ManDumpInterface( Gia_Man_t * p, char * pFileName )
     Vec_BitFree( vInvs );
     Vec_BitFree( vUsed );
 }
+void Gia_ManDumpInterfaceAssign( Gia_Man_t * p, char * pFileName )
+{
+    Gia_Obj_t * pObj;
+    Vec_Bit_t * vInvs, * vUsed;
+    int nDigits  = Abc_Base10Log( Gia_ManObjNum(p) );
+    int nDigitsI = Abc_Base10Log( Gia_ManPiNum(p) );
+    int nDigitsO = Abc_Base10Log( Gia_ManPoNum(p) );
+    int i;
+
+    FILE * pFile = fopen( pFileName, "wb" );
+    if ( pFile == NULL )
+    {
+        printf( "Cannot open output file \"%s\".\n", pFileName );
+        return;
+    }
+
+    vInvs = Gia_ManGenUsed( p, 0 );
+    vUsed = Gia_ManGenUsed( p, 1 );
+
+    fprintf( pFile, "module " );
+    Gia_ManDumpModuleName( pFile, p->pName );
+    fprintf( pFile, "_wrapper" );
+    fprintf( pFile, " ( _i_, _o_ );\n\n" );
+    fprintf( pFile, "  input  [%d:0] _i_;\n",   Gia_ManCiNum(p)-1 );
+    fprintf( pFile, "  output [%d:0] _o_;\n\n", Gia_ManCoNum(p)-1 );
+
+    fprintf( pFile, "  wire " );
+    Gia_ManWriteNames( pFile, 'x', Gia_ManPiNum(p), p->vNamesIn, 8, 4, NULL );
+    fprintf( pFile, ";\n\n" );
+
+    fprintf( pFile, "  wire " );
+    Gia_ManWriteNames( pFile, 'z', Gia_ManPoNum(p), p->vNamesOut, 9, 4, NULL );
+    fprintf( pFile, ";\n\n" );
+
+    fprintf( pFile, "  assign { " );
+    Gia_ManWriteNames( pFile, 'x', Gia_ManCiNum(p), p->vNamesIn, 8, 4, NULL );
+    fprintf( pFile, " } = _i_;\n\n" );
+
+    fprintf( pFile, "  assign _o_ = { " );
+    Gia_ManWriteNames( pFile, 'z', Gia_ManCoNum(p), p->vNamesOut, 9, 4, NULL );
+    fprintf( pFile, " };\n\n" );
+
+    if ( Vec_BitCount(vUsed) )
+    {
+        fprintf( pFile, "  wire " );
+        Gia_ManWriteNames( pFile, 'n', Gia_ManObjNum(p), NULL, 7, 4, vUsed );
+        fprintf( pFile, ";\n\n" );
+    }
+
+    if ( Vec_BitCount(vInvs) )
+    {
+        fprintf( pFile, "  wire " );
+        Gia_ManWriteNames( pFile, 'i', Gia_ManObjNum(p), NULL, 7, 4, vInvs );
+        fprintf( pFile, ";\n\n" );
+    }
+
+    // input inverters
+    Gia_ManForEachCi( p, pObj, i )
+    {
+        if ( Vec_BitEntry(vUsed, Gia_ObjId(p, pObj)) )
+        {
+            fprintf( pFile, "  assign %s =", Gia_ObjGetDumpName(NULL, 'n', Gia_ObjId(p, pObj), nDigits) );
+            fprintf( pFile, " %s;\n",   Gia_ObjGetDumpName(p->vNamesIn, 'x', i, nDigitsI) );
+        }
+        if ( Vec_BitEntry(vInvs, Gia_ObjId(p, pObj)) )
+        {
+            fprintf( pFile, "  assign %s =", Gia_ObjGetDumpName(NULL, 'i', Gia_ObjId(p, pObj), nDigits) );
+            fprintf( pFile, " ~%s;\n",   Gia_ObjGetDumpName(p->vNamesIn, 'x', i, nDigitsI) );
+        }
+    }
+
+    // internal nodes and their inverters
+    fprintf( pFile, "\n" );
+    Gia_ManForEachAnd( p, pObj, i )
+    {
+        fprintf( pFile, "  assign %s =", Gia_ObjGetDumpName(NULL, 'n', i, nDigits) );
+        fprintf( pFile, " %s &",       Gia_ObjGetDumpName(NULL, (char)(Gia_ObjFaninC0(pObj)? 'i':'n'), Gia_ObjFaninId0(pObj, i), nDigits) );
+        fprintf( pFile, " %s;\n",   Gia_ObjGetDumpName(NULL, (char)(Gia_ObjFaninC1(pObj)? 'i':'n'), Gia_ObjFaninId1(pObj, i), nDigits) );
+        if ( Vec_BitEntry(vInvs, i) )
+        {
+            fprintf( pFile, "  assign %s =", Gia_ObjGetDumpName(NULL, 'i', i, nDigits) );
+            fprintf( pFile, " ~%s;\n",   Gia_ObjGetDumpName(NULL, 'n', i, nDigits) );
+        }
+    }
+    
+    // output drivers
+    fprintf( pFile, "\n" );
+    Gia_ManForEachCo( p, pObj, i )
+    {
+        fprintf( pFile, "  assign %s = ", Gia_ObjGetDumpName(p->vNamesOut, 'z', i, nDigitsO) );
+        if ( Gia_ObjIsConst0(Gia_ObjFanin0(pObj)) )
+            fprintf( pFile, "1\'b%d;\n", Gia_ObjFaninC0(pObj) );
+        else 
+            fprintf( pFile, "%s;\n", Gia_ObjGetDumpName(NULL, (char)(Gia_ObjFaninC0(pObj)? 'i':'n'), Gia_ObjFaninId0p(p, pObj), nDigits) );
+    }
+
+    fprintf( pFile, "\nendmodule\n\n" );
+    fclose( pFile );
+
+    Vec_BitFree( vInvs );
+    Vec_BitFree( vUsed );
+}
 
 
 /**Function*************************************************************
@@ -1783,7 +2076,7 @@ void Gia_GenSandwich( char ** pFNames, int nFNames, char * pFileName )
     fprintf( pFile, "endmodule\n" );
     fclose( pFile );
     for ( i = 0; i < nFNames; i++ ) {
-        Gia_ManDumpVerilog( pGias[i], Extra_FileNameGenericAppend(pGias[i]->pSpec, ".v"), NULL, 0, 0, 1 );
+        Gia_ManDumpVerilog( pGias[i], Extra_FileNameGenericAppend(pGias[i]->pSpec, ".v"), NULL, 0, 0, 1, 0 );
         printf( "Dumped Verilog file \"%s\"\n", Extra_FileNameGenericAppend(pGias[i]->pSpec, ".v") );        
     }
     Gia_FreeMany( pGias, nFNames );
diff --git a/src/aig/gia/giaMini.c b/src/aig/gia/giaMini.c
index 85647eac5..2fce5d0d4 100644
--- a/src/aig/gia/giaMini.c
+++ b/src/aig/gia/giaMini.c
@@ -1257,7 +1257,7 @@ Vec_Str_t * Gia_ManRetimableF( Gia_Man_t * p, int * pRst, int * pSet, int * pEna
         int * pNode = Vec_IntEntryP( vTemps, 3*i );
         pStops[i] = (char)1;
         if ( pFan0[0] != -1 && pFan0[0] == pFan1[0] && pFan0[1] == pFan1[1] && pFan0[2] == pFan1[2] )
-            pStops[i] = (char)0, pNode[0] = pFan0[0], pNode[1] = pFan0[1], pNode[2] = pFan0[2]; 
+            pStops[i] = (char)0, pNode[0] = pFan0[0], pNode[1] = pFan0[1], pNode[2] = pFan0[2];
     }
     Vec_IntFree( vTemps );
     return vStops;
@@ -1266,32 +1266,37 @@ Vec_Str_t * Gia_ManRetimableB( Gia_Man_t * p, int * pRst, int * pSet, int * pEna
 {
     Vec_Str_t * vStops = Vec_StrStart( Gia_ManObjNum(p) );
     Vec_Int_t * vTemps = Vec_IntStartFull( 3*Gia_ManObjNum(p) );
-    Gia_Obj_t * pObj, * pObjRi, * pObjRo; int i, n;
+    Gia_Obj_t * pObj, * pObjRi, * pObjRo; int i, n, iFanout;
     char * pStops = Vec_StrArray(vStops);
     assert( Gia_ManRegNum(p) > 0 );
     Gia_ManForEachRiRo( p, pObjRi, pObjRo, i ) {
-        Vec_IntWriteEntry( vTemps, 3*Gia_ObjFaninId0p(p, pObjRi) + 0, pRst[i] );
-        Vec_IntWriteEntry( vTemps, 3*Gia_ObjFaninId0p(p, pObjRi) + 1, pSet[i] );
-        Vec_IntWriteEntry( vTemps, 3*Gia_ObjFaninId0p(p, pObjRi) + 2, pEna[i] );        
+        Vec_IntWriteEntry( vTemps, 3*Gia_ObjId(p, pObjRi) + 0, pRst[i] );
+        Vec_IntWriteEntry( vTemps, 3*Gia_ObjId(p, pObjRi) + 1, pSet[i] );
+        Vec_IntWriteEntry( vTemps, 3*Gia_ObjId(p, pObjRi) + 2, pEna[i] );        
     }
+    Gia_ManStaticFanoutStart( p );
     Gia_ManForEachAndReverse( p, pObj, i ) {
-        int   iFans[2] = { Gia_ObjFaninId0(pObj, i), Gia_ObjFaninId1(pObj, i) };
-        int * pFans[2] = { Vec_IntEntryP( vTemps, 3*iFans[0] ), Vec_IntEntryP( vTemps, 3*iFans[1] ) };
+        int * pFan0 = Vec_IntEntryP( vTemps, 3*Gia_ObjFanoutId(p, i, 0) );
         int * pNode = Vec_IntEntryP( vTemps, 3*i );
-        if ( pNode[0] == -1 )
+        pStops[i] = (char)1;        
+        if ( pFan0[0] == -1 )
             continue;
-        for ( n = 0; n < 2; n++ )
-            if ( pFans[n][0] == -1 )
-                pStops[iFans[n]] = (char)1, pFans[n][0] = pNode[0], pFans[n][1] = pNode[1], pFans[n][2] = pNode[2];
-            else if ( pFans[n][0] != pNode[0] || pFans[n][1] != pNode[1] || pFans[n][2] != pNode[2] )
-                pStops[iFans[n]] = (char)0;
+        Gia_ObjForEachFanoutStaticId( p, i, iFanout, n ) {
+            int * pFan1 = Vec_IntEntryP( vTemps, 3*iFanout );
+            if ( pFan1[0] == -1 || pFan0[0] != pFan1[0] || pFan0[1] != pFan1[1] || pFan0[2] != pFan1[2] )
+                break;
+        }
+        if ( n < Gia_ObjFanoutNum(p, pObj) )
+            continue;
+        pStops[i] = (char)0, pNode[0] = pFan0[0], pNode[1] = pFan0[1], pNode[2] = pFan0[2];
     }
-    pStops[0] = (char)0;
-    Gia_ManForEachCi( p, pObj, i )
-        pStops[Gia_ObjId(p, pObj)] = (char)0;
-    Gia_ManForEachAnd( p, pObj, i )
-        pStops[i] = (char)!pStops[i];      
-    Vec_IntFree( vTemps );    
+    Gia_ManStaticFanoutStop( p );
+    Vec_IntFree( vTemps );
+    Gia_ManForEachRiRo( p, pObjRi, pObjRo, i ) {
+        if ( Gia_ObjIsAnd(Gia_ManObj(p, Abc_Lit2Var(pRst[i]))) ) pStops[Abc_Lit2Var(pRst[i])] = 1;
+        if ( Gia_ObjIsAnd(Gia_ManObj(p, Abc_Lit2Var(pSet[i]))) ) pStops[Abc_Lit2Var(pSet[i])] = 1;
+        if ( Gia_ObjIsAnd(Gia_ManObj(p, Abc_Lit2Var(pEna[i]))) ) pStops[Abc_Lit2Var(pEna[i])] = 1;                
+    }    
     return vStops;
 }
 
@@ -1306,18 +1311,42 @@ Vec_Str_t * Gia_ManRetimableB( Gia_Man_t * p, int * pRst, int * pSet, int * pEna
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_FrameSetRetimingData( Abc_Frame_t * pAbc, int * pRst, int * pSet, int * pEna )
+void Abc_FrameRemapLits( int * pLits, int nLits, Vec_Int_t * vMap )
+{
+    for ( int i = 0; i < nLits; i++ )
+        pLits[i] = Abc_Lit2LitL( Vec_IntArray(vMap), pLits[i] );
+}
+void Abc_FrameSetRetimingData( Abc_Frame_t * pAbc, int * pRst, int * pSet, int * pEna, int nRegs )
 {
     Gia_Man_t * pGia;
+    int * pRstNew = ABC_CALLOC( int, nRegs );
+    int * pSetNew = ABC_CALLOC( int, nRegs );
+    int * pEnaNew = ABC_CALLOC( int, nRegs );
     if ( pAbc == NULL )
         printf( "ABC framework is not initialized by calling Abc_Start()\n" );
     pGia = Abc_FrameReadGia( pAbc );
     if ( pGia == NULL )
         printf( "Current network in ABC framework is not defined.\n" );
+    else {
+        assert( nRegs == Gia_ManRegNum(pGia) );
+        memmove( pRstNew, pRst, sizeof(int)*nRegs ); 
+        memmove( pSetNew, pSet, sizeof(int)*nRegs ); 
+        memmove( pEnaNew, pEna, sizeof(int)*nRegs ); 
+    }
+    if ( pAbc->vCopyMiniAig == NULL )
+        printf( "Mapping of MiniAig nodes is not available.\n" );
+    else {
+        Abc_FrameRemapLits( pRstNew, nRegs, pAbc->vCopyMiniAig );
+        Abc_FrameRemapLits( pSetNew, nRegs, pAbc->vCopyMiniAig );
+        Abc_FrameRemapLits( pEnaNew, nRegs, pAbc->vCopyMiniAig );        
+    }      
     assert( pGia->vStopsF == NULL );
     assert( pGia->vStopsB == NULL );
-    pGia->vStopsF = Gia_ManRetimableF( pGia, pRst, pSet, pEna );
-    pGia->vStopsB = Gia_ManRetimableB( pGia, pRst, pSet, pEna );    
+    pGia->vStopsF = Gia_ManRetimableF( pGia, pRstNew, pSetNew, pEnaNew );
+    pGia->vStopsB = Gia_ManRetimableB( pGia, pRstNew, pSetNew, pEnaNew );
+    ABC_FREE( pRstNew );
+    ABC_FREE( pSetNew );
+    ABC_FREE( pEnaNew );
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 70f83bf62..c3afa1c72 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -541,6 +541,7 @@ static int Abc_CommandAbc9PoPart             ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandAbc9GroupProve         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9MultiProve         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9SplitProve         ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9SProve             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9SplitSat           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Bmc                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9SBmc               ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -844,14 +845,18 @@ Gia_Man_t * Abc_FrameGetGia( Abc_Frame_t * pAbc )
 ***********************************************************************/
 void Abc_Init( Abc_Frame_t * pAbc )
 {
+    Cmd_CommandAdd( pAbc, "Printing",     "ps",            Abc_CommandPrintStats,       0 );
     Cmd_CommandAdd( pAbc, "Printing",     "print_stats",   Abc_CommandPrintStats,       0 );
     Cmd_CommandAdd( pAbc, "Printing",     "print_exdc",    Abc_CommandPrintExdc,        0 );
     Cmd_CommandAdd( pAbc, "Printing",     "print_io",      Abc_CommandPrintIo,          0 );
     Cmd_CommandAdd( pAbc, "Printing",     "print_latch",   Abc_CommandPrintLatch,       0 );
+    Cmd_CommandAdd( pAbc, "Printing",     "pfan",          Abc_CommandPrintFanio,       0 );
     Cmd_CommandAdd( pAbc, "Printing",     "print_fanio",   Abc_CommandPrintFanio,       0 );
     Cmd_CommandAdd( pAbc, "Printing",     "print_mffc",    Abc_CommandPrintMffc,        0 );
+    Cmd_CommandAdd( pAbc, "Printing",     "pf",            Abc_CommandPrintFactor,      0 );
     Cmd_CommandAdd( pAbc, "Printing",     "print_factor",  Abc_CommandPrintFactor,      0 );
     Cmd_CommandAdd( pAbc, "Printing",     "print_level",   Abc_CommandPrintLevel,       0 );
+    Cmd_CommandAdd( pAbc, "Printing",     "psu",           Abc_CommandPrintSupport,     0 );
     Cmd_CommandAdd( pAbc, "Printing",     "print_supp",    Abc_CommandPrintSupport,     0 );
 #ifdef ABC_USE_CUDD
     Cmd_CommandAdd( pAbc, "Printing",     "print_mint",    Abc_CommandPrintMint,        0 );
@@ -860,6 +865,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Printing",     "print_unate",   Abc_CommandPrintUnate,       0 );
     Cmd_CommandAdd( pAbc, "Printing",     "print_auto",    Abc_CommandPrintAuto,        0 );
     Cmd_CommandAdd( pAbc, "Printing",     "print_kmap",    Abc_CommandPrintKMap,        0 );
+    Cmd_CommandAdd( pAbc, "Printing",     "pg",            Abc_CommandPrintGates,       0 );
     Cmd_CommandAdd( pAbc, "Printing",     "print_gates",   Abc_CommandPrintGates,       0 );
     Cmd_CommandAdd( pAbc, "Printing",     "print_sharing", Abc_CommandPrintSharing,     0 );
     Cmd_CommandAdd( pAbc, "Printing",     "print_xcut",    Abc_CommandPrintXCut,        0 );
@@ -873,9 +879,12 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Printing",     "show_bdd",      Abc_CommandShowBdd,          0 );
     Cmd_CommandAdd( pAbc, "Printing",     "show_cut",      Abc_CommandShowCut,          0 );
 
+    Cmd_CommandAdd( pAbc, "Synthesis",    "clp",           Abc_CommandCollapse,         1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "collapse",      Abc_CommandCollapse,         1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "satclp",        Abc_CommandSatClp,           1 );
+    Cmd_CommandAdd( pAbc, "Synthesis",    "st",            Abc_CommandStrash,           1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "strash",        Abc_CommandStrash,           1 );
+    Cmd_CommandAdd( pAbc, "Synthesis",    "b",             Abc_CommandBalance,          1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "balance",       Abc_CommandBalance,          1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "mux_struct",    Abc_CommandMuxStruct,        1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "multi",         Abc_CommandMulti,            1 );
@@ -1306,6 +1315,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC9",         "&gprove",       Abc_CommandAbc9GroupProve,   0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&mprove",       Abc_CommandAbc9MultiProve,   0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&splitprove",   Abc_CommandAbc9SplitProve,   0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&sprove",       Abc_CommandAbc9SProve,       0 );    
     Cmd_CommandAdd( pAbc, "ABC9",         "&splitsat",     Abc_CommandAbc9SplitSat,     0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&bmc",          Abc_CommandAbc9Bmc,          0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&bmcs",         Abc_CommandAbc9SBmc,         0 );
@@ -31929,13 +31939,14 @@ int Abc_CommandAbc9Write( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fVerilog = 0;
     int fInter   = 0;
     int fInterComb = 0;
+    int fAssign  = 0;
     int fVerBufs = 0;
     int fMiniAig = 0;
     int fMiniLut = 0;
     int fWriteNewLine = 0;
     int fVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "upicbmlnvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "upicabmlnvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -31950,7 +31961,10 @@ int Abc_CommandAbc9Write( Abc_Frame_t * pAbc, int argc, char ** argv )
             break;
         case 'c':
             fInterComb ^= 1;
-            break;            
+            break;      
+        case 'a':
+            fAssign ^= 1;
+            break;                        
         case 'b':
             fVerBufs ^= 1;
             break;
@@ -31992,7 +32006,7 @@ int Abc_CommandAbc9Write( Abc_Frame_t * pAbc, int argc, char ** argv )
         Gia_ManStop( pGia );
     }
     else if ( fVerilog )
-        Gia_ManDumpVerilog( pAbc->pGia, pFileName, NULL, fVerBufs, fInter, fInterComb );
+        Gia_ManDumpVerilog( pAbc->pGia, pFileName, NULL, fVerBufs, fInter, fInterComb, fAssign );
     else if ( fMiniAig )
         Gia_ManWriteMiniAig( pAbc->pGia, pFileName );
     else if ( fMiniLut )
@@ -32002,12 +32016,13 @@ int Abc_CommandAbc9Write( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &w [-upicbmlnvh] <file>\n" );
+    Abc_Print( -2, "usage: &w [-upicabmlnvh] <file>\n" );
     Abc_Print( -2, "\t         writes the current AIG into the AIGER file\n" );
     Abc_Print( -2, "\t-u     : toggle writing canonical AIG structure [default = %s]\n", fUnique? "yes" : "no" );
     Abc_Print( -2, "\t-p     : toggle writing Verilog with 'and' and 'not' [default = %s]\n", fVerilog? "yes" : "no" );
     Abc_Print( -2, "\t-i     : toggle writing the interface module in Verilog [default = %s]\n", fInter? "yes" : "no" );
     Abc_Print( -2, "\t-c     : toggle writing the interface module in Verilog [default = %s]\n", fInterComb? "yes" : "no" );
+    Abc_Print( -2, "\t-a     : toggle writing the interface module with assign-statements [default = %s]\n", fAssign? "yes" : "no" );
     Abc_Print( -2, "\t-b     : toggle writing additional buffers in Verilog [default = %s]\n", fVerBufs? "yes" : "no" );
     Abc_Print( -2, "\t-m     : toggle writing MiniAIG rather than AIGER [default = %s]\n", fMiniAig? "yes" : "no" );
     Abc_Print( -2, "\t-l     : toggle writing MiniLUT rather than AIGER [default = %s]\n", fMiniLut? "yes" : "no" );
@@ -46264,6 +46279,89 @@ usage:
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc9SProve( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int fVerbose, int fVeryVerbose, int fSilent );
+    int c, nProcs = 5, nTimeOut = 3, fVerbose = 0, fVeryVerbose = 0, fSilent = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "PTsvwh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'P':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-P\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            nProcs = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nProcs <= 0 )
+                goto usage;
+            break;
+        case 'T':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-T\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            nTimeOut = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nTimeOut <= 0 )
+                goto usage;
+            break;
+        case 's':
+            fSilent ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'w':
+            fVeryVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9SProve(): There is no AIG.\n" );
+        return 1;
+    }
+    if ( Gia_ManRegNum(pAbc->pGia) == 0 )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9SProve(): The problem is combinational.\n" );
+        return 1;
+    }
+    pAbc->Status = Cec_GiaProveTest( pAbc->pGia, nProcs, nTimeOut, fVerbose, fVeryVerbose, fSilent );
+    Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexSeq ); 
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &sprove [-PT num] [-svwh]\n" );
+    Abc_Print( -2, "\t         proves CEC problem by case-splitting\n" );
+    Abc_Print( -2, "\t-P num : the number of concurrent processes [default = %d]\n",          nProcs );
+    Abc_Print( -2, "\t-T num : runtime limit in seconds per subproblem [default = %d]\n",     nTimeOut );
+    Abc_Print( -2, "\t-s     : enable silent computation (no reporting) [default = %s]\n",    fSilent? "yes": "no" );
+    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n",         fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-w     : toggle printing more verbose information [default = %s]\n",    fVeryVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
+    return 1;
+}
+
 /**Function*************************************************************
 
   Synopsis    []
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index 7b566b79d..e90159d2a 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -224,6 +224,37 @@ float Abc_NtkGetArea( Abc_Ntk_t * pNtk )
     return Counter;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+float Abc_NtkGetAreaSpecial( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj; int i, Count = 0;    
+    Abc_NtkForEachNode( pNtk, pObj, i )
+        if ( !strncmp( Mio_GateReadName((Mio_Gate_t*)pObj->pData), "mm", 2 ) )
+           Count++;
+    return 1.0*Count/Abc_NtkNodeNum(pNtk);
+}
+float Abc_NtkGetAreaSpecial2( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj; int i; 
+    float Count = 0, CountAll = 0;    
+    Abc_NtkForEachNode( pNtk, pObj, i ) {
+        if ( !strncmp( Mio_GateReadName((Mio_Gate_t*)pObj->pData), "mm", 2 ) )
+           Count += Mio_GateReadArea((Mio_Gate_t*)pObj->pData);
+        CountAll += Mio_GateReadArea((Mio_Gate_t*)pObj->pData);
+    }
+    return 1.0*Count/CountAll;
+}
+
 /**Function*************************************************************
 
   Synopsis    [Print the vital stats of the network.]
@@ -360,7 +391,7 @@ void Abc_NtkPrintStats( Abc_Ntk_t * pNtk, int fFactored, int fSaveBest, int fDum
     if ( fPrintMem )
         Abc_Print( 1,"  mem =%5.2f MB", Abc_NtkMemory(pNtk)/(1<<20) );
     Abc_Print( 1,"\n" );
-
+/*
     // print the statistic into a file
     if ( fDumpResult )
     {
@@ -374,6 +405,8 @@ void Abc_NtkPrintStats( Abc_Ntk_t * pNtk, int fFactored, int fSaveBest, int fDum
         fprintf( pTable, "\n" );
         fclose( pTable );
     }
+*/
+
 /*
     {
         FILE * pTable;
@@ -389,21 +422,6 @@ void Abc_NtkPrintStats( Abc_Ntk_t * pNtk, int fFactored, int fSaveBest, int fDum
     }
 */
 
-/*
-    // print the statistic into a file
-    {
-        FILE * pTable;
-        pTable = fopen( "ucsb/stats.txt", "a+" );
-//        fprintf( pTable, "%s ",  pNtk->pSpec );
-        fprintf( pTable, "%d ",  Abc_NtkNodeNum(pNtk) );
-//        fprintf( pTable, "%d ",  Abc_NtkLevel(pNtk) );
-//        fprintf( pTable, "%.0f ", Abc_NtkGetMappedArea(pNtk) );
-//        fprintf( pTable, "%.2f ", Abc_NtkDelayTrace(pNtk) );
-        fprintf( pTable, "\n" );
-        fclose( pTable );
-    }
-*/
-
 /*
     // print the statistic into a file
     {
diff --git a/src/base/cmd/cmd.c b/src/base/cmd/cmd.c
index 67c02cab8..80ba52612 100644
--- a/src/base/cmd/cmd.c
+++ b/src/base/cmd/cmd.c
@@ -22,6 +22,7 @@
 #include <process.h>
 #else
 #include <unistd.h>
+#include <dirent.h>
 #endif
 
 #include "base/abc/abc.h"
@@ -54,8 +55,11 @@ static int CmdCommandScanDir       ( Abc_Frame_t * pAbc, int argc, char ** argv
 static int CmdCommandRenameFiles   ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int CmdCommandLs            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int CmdCommandScrGen        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+#else
+static int CmdCommandScrGenLinux   ( Abc_Frame_t * pAbc, int argc, char ** argv );
 #endif
 static int CmdCommandVersion       ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int CmdCommandSGen          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int CmdCommandSis           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int CmdCommandMvsis         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int CmdCommandCapo          ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -104,8 +108,11 @@ void Cmd_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Basic", "renamefiles",   CmdCommandRenameFiles,     0 );
     Cmd_CommandAdd( pAbc, "Basic", "ls",            CmdCommandLs,              0 );
     Cmd_CommandAdd( pAbc, "Basic", "scrgen",        CmdCommandScrGen,          0 );
+#else
+    Cmd_CommandAdd( pAbc, "Basic", "scrgen",        CmdCommandScrGenLinux,     0 );
 #endif
     Cmd_CommandAdd( pAbc, "Basic", "version",       CmdCommandVersion,         0 );
+    Cmd_CommandAdd( pAbc, "Basic", "sgen",          CmdCommandSGen,            0 );
 
     Cmd_CommandAdd( pAbc, "Various", "sis",         CmdCommandSis,             1 );
     Cmd_CommandAdd( pAbc, "Various", "mvsis",       CmdCommandMvsis,           1 );
@@ -1628,11 +1635,11 @@ int CmdCommandScrGen( Abc_Frame_t * pAbc, int argc, char **argv )
     int    nFileNameMax, nFileNameCur;
     int    Counter = 0;
     int    fUseCurrent;
-    char   c;
+    int    c;
 
     fUseCurrent = 0;
     Extra_UtilGetoptReset();
-    while ( (c = Extra_UtilGetopt(argc, argv, "FDCWch") ) != EOF )
+    while ( (c = Extra_UtilGetopt(argc, argv, "FRCWch") ) != EOF )
     {
         switch (c)
         {
@@ -1645,7 +1652,7 @@ int CmdCommandScrGen( Abc_Frame_t * pAbc, int argc, char **argv )
             pFileStr = argv[globalUtilOptind];
             globalUtilOptind++;
             break;
-        case 'D':
+        case 'R':
             if ( globalUtilOptind >= argc )
             {
                 fprintf( pAbc->Err, "Command line switch \"-D\" should be followed by a string.\n" );
@@ -1795,7 +1802,7 @@ int CmdCommandScrGen( Abc_Frame_t * pAbc, int argc, char **argv )
                         Line[c] = '/';
                 fprintf( pFile, "%s", Line );
             }
-            fprintf( pFile, "\n", Line );
+            fprintf( pFile, "\n" );
         }
         while( _findnext( hFile, &c_file ) == 0 );
         _findclose( hFile );
@@ -1815,17 +1822,171 @@ int CmdCommandScrGen( Abc_Frame_t * pAbc, int argc, char **argv )
     return 0;
 
 usage:
-    fprintf( pAbc->Err, "usage: scrgen -F <str> -D <str> -C <str> -W <str> -ch\n" );
+    fprintf( pAbc->Err, "usage: scrgen -F <str> -R <str> -C <str> -W <str> -ch\n" );
     fprintf( pAbc->Err, "\t          generates script for running ABC\n" );
     fprintf( pAbc->Err, "\t-F str  : the name of the script file [default = \"test.s\"]\n" );
-    fprintf( pAbc->Err, "\t-D str  : the directory to read files from [default = current]\n" );
+    fprintf( pAbc->Err, "\t-R str  : the directory to read files from [default = current]\n" );
     fprintf( pAbc->Err, "\t-C str  : the sequence of commands to run [default = \"ps\"]\n" );
     fprintf( pAbc->Err, "\t-W str  : the directory to write the resulting files [default = no writing]\n" );
     fprintf( pAbc->Err, "\t-c      : toggle placing file in current/target dir [default = %s]\n", fUseCurrent? "current": "target" );
     fprintf( pAbc->Err, "\t-h      : print the command usage\n\n");
-    fprintf( pAbc->Err, "\tExample : scrgen -F test1.s -D a/in -C \"ps; st; ps\" -W a/out\n" );
+    fprintf( pAbc->Err, "\tExample : scrgen -F test1.s -R a/in -C \"ps; st; ps\" -W a/out\n" );
     return 1;
 }
+
+#else
+
+Vec_Ptr_t * CmdReturnFileNames( char * pDirStr ) 
+{
+    Vec_Ptr_t * vRes = Vec_PtrAlloc( 100 );
+    struct dirent **namelist;
+    int num_files = scandir(pDirStr, &namelist, NULL, alphasort);
+    if (num_files == -1) {
+        printf("Error opening directory.\n");
+        return NULL;
+    }
+    for (int i = 0; i < num_files; i++) {
+        char * pExt = strstr(namelist[i]->d_name, ".");
+        if ( !pExt || !strcmp(pExt, ".") || !strcmp(pExt, "..") || !strcmp(pExt, ".s") || !strcmp(pExt, ".txt") )
+            continue;    
+        Vec_PtrPush( vRes, Abc_UtilStrsav(namelist[i]->d_name) );
+        free(namelist[i]);
+    }
+    free(namelist);
+    return vRes;
+}
+
+int CmdCommandScrGenLinux( Abc_Frame_t * pAbc, int argc, char **argv )
+{
+    Vec_Ptr_t * vNames = NULL;
+    FILE * pFile = NULL;
+    char * pFileStr = (char *)"test.s";
+    char * pDirStr = (char *)".";
+    char * pComStr = (char *)"ps";
+    char * pWriteStr = NULL;
+    char * pWriteExt = NULL;    
+    char   Line[2000], * pName;
+    int    nFileNameMax;
+    int    c, k;
+
+    Extra_UtilGetoptReset();
+    while ( (c = Extra_UtilGetopt(argc, argv, "FRCWEh") ) != EOF )
+    {
+        switch (c)
+        {
+        case 'F':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pAbc->Err, "Command line switch \"-F\" should be followed by a string.\n" );
+                goto usage;
+            }
+            pFileStr = argv[globalUtilOptind];
+            globalUtilOptind++;
+            break;
+        case 'R':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pAbc->Err, "Command line switch \"-D\" should be followed by a string.\n" );
+                goto usage;
+            }
+            pDirStr = argv[globalUtilOptind];
+            globalUtilOptind++;
+            break;
+        case 'C':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pAbc->Err, "Command line switch \"-C\" should be followed by a string.\n" );
+                goto usage;
+            }
+            pComStr = argv[globalUtilOptind];
+            globalUtilOptind++;
+            break;
+        case 'W':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pAbc->Err, "Command line switch \"-W\" should be followed by a string.\n" );
+                goto usage;
+            }
+            pWriteStr = argv[globalUtilOptind];
+            globalUtilOptind++;
+            break;
+        case 'E':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pAbc->Err, "Command line switch \"-E\" should be followed by a string.\n" );
+                goto usage;
+            }
+            pWriteExt = argv[globalUtilOptind];
+            globalUtilOptind++;
+            break;            
+        default:
+            goto usage;
+        }
+    }
+    pFile = fopen( pFileStr, "w" );
+    if ( pFile == NULL )
+    {
+        printf( "Cannot open output file %s.\n", pFileStr );
+        return 0;
+    }
+    vNames = CmdReturnFileNames( pDirStr );
+    if ( !vNames || !Vec_PtrSize(vNames) )
+    {
+        if ( vNames )
+            printf( "It looks like the directory \"%s\" does not contain any relevant files.\n", pDirStr );
+        Vec_PtrFreeP(&vNames);
+        return 0;
+    }
+    nFileNameMax = 0;
+    Vec_PtrForEachEntry( char *, vNames, pName, k )
+        if ( nFileNameMax < strlen(pName) )
+            nFileNameMax = strlen(pName);
+    {
+        int fAndSpace = pComStr[0] == '&';
+        fprintf( pFile, "# Script file produced by ABC on %s\n", Extra_TimeStamp() );
+        fprintf( pFile, "# Command line was: scrgen -F %s -D %s -C \"%s\"%s%s%s%s\n",
+            pFileStr, pDirStr, pComStr, 
+            pWriteStr?" -W ":"", pWriteStr?pWriteStr:"", 
+            pWriteExt?" -E ":"", pWriteExt?pWriteExt:"" );
+        Vec_PtrForEachEntry( char *, vNames, pName, k ) {
+            char * pExt = strstr(pName, ".");
+            if ( !pExt || !strcmp(pExt, ".") || !strcmp(pExt, "..") || !strcmp(pExt, ".s") || !strcmp(pExt, ".txt") )
+                continue;
+            sprintf( Line, "%sread %s%s%-*s ; %s", fAndSpace ? "&" : "", pDirStr?pDirStr:"", pDirStr?"/":"", nFileNameMax, pName, pComStr );
+            for ( c = (int)strlen(Line)-1; c >= 0; c-- )
+                if ( Line[c] == '\\' )
+                    Line[c] = '/';
+            fprintf( pFile, "%s", Line );
+            if ( pWriteStr )
+            {
+                char * pFNameOut = pWriteExt ? Extra_FileNameGenericAppend(pName, pWriteExt) : pName;
+                sprintf( Line, " ; %swrite %s/%-*s", fAndSpace ? "&" : "", pWriteStr, nFileNameMax, pFNameOut );
+                for ( c = (int)strlen(Line)-1; c >= 0; c-- )
+                    if ( Line[c] == '\\' )
+                        Line[c] = '/';
+                fprintf( pFile, "%s", Line );
+            }
+            fprintf( pFile, "\n" );
+        }
+    }
+    fclose( pFile );
+    printf( "Script file \"%s\" with command lines for %d files.\n", pFileStr, Vec_PtrSize(vNames) );
+    Vec_PtrFreeFree( vNames );
+    return 0;
+
+usage:
+    fprintf( pAbc->Err, "usage: scrgen -F <str> -R <str> -C <str> -W <str> -E <str> -h\n" );
+    fprintf( pAbc->Err, "\t          generates script for running ABC\n" );
+    fprintf( pAbc->Err, "\t-F str  : the name of the script file [default = \"test.s\"]\n" );
+    fprintf( pAbc->Err, "\t-R str  : the directory to read files from [default = current]\n" );
+    fprintf( pAbc->Err, "\t-C str  : the sequence of commands to run [default = \"ps\"]\n" );
+    fprintf( pAbc->Err, "\t-W str  : the directory to write the resulting files [default = no writing]\n" );
+    fprintf( pAbc->Err, "\t-E str  : the output files extension (with \".\") [default = the same as input files]\n" );
+    fprintf( pAbc->Err, "\t-h      : print the command usage\n\n");
+    fprintf( pAbc->Err, "\tExample : scrgen -F test1.s -R a/in -C \"ps; st; ps\" -W a/out -E .blif\n" );
+    return 1;
+}
+
 #endif
 
 
@@ -2602,6 +2763,79 @@ usage:
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int CmdCommandSGen( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern void Cmd_CommandSGen( Abc_Frame_t * pAbc, int nParts, int nIters, int fVerbose );
+    int c, nParts    = 10;
+    int nIters       = 10;
+    int fVerbose     =  0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "NIvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'N':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nParts = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nParts < 0 ) 
+                goto usage;
+            break;
+        case 'I':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-I\" should be followed by a string (possibly in quotes).\n" );
+                goto usage;
+            }
+            nIters = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( Abc_FrameReadNtk(pAbc) == NULL )
+    {
+        Abc_Print( -2, "There is no current network.\n" );
+        return 1;
+    }
+    if ( !Abc_NtkIsStrash(Abc_FrameReadNtk(pAbc)) )    
+    {
+        Abc_Print( -2, "The current network is not an AIG.\n" );
+        return 1;
+    }
+    Cmd_CommandSGen( pAbc, nParts, nIters, fVerbose );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: sgen [-N num] [-I num] [-vh]\n" );
+    Abc_Print( -2, "\t         experiment with script generation\n" );
+    Abc_Print( -2, "\t-N num : the number of commands to use [default = %d]\n", nParts );
+    Abc_Print( -2, "\t-I num : the number of iterations to perform [default = %d]\n", nIters );
+    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
+    return 1;
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/base/cmd/cmdUtils.c b/src/base/cmd/cmdUtils.c
index 2158f8e97..a5dc6972b 100644
--- a/src/base/cmd/cmdUtils.c
+++ b/src/base/cmd/cmdUtils.c
@@ -833,6 +833,70 @@ void Gia_ManKissatCall( Abc_Frame_t * pAbc, char * pFileName, char * pArgs, int
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+                
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Cmd_GenScript( char ** pComms, int nComms, int nParts )
+{
+    static char pScript[1000]; int c;
+    pScript[0] = 0;
+    for ( c = 0; c < nParts; c++ ) {
+        strcat( pScript, pComms[rand() % nComms] );
+        strcat( pScript, "; " );
+    }
+    strcat( pScript, "print_stats" );    
+    return pScript;
+}
+void Cmd_CommandSGen( Abc_Frame_t * pAbc, int nParts, int nIters, int fVerbose )
+{
+    Abc_Ntk_t * pCopy = Abc_NtkDup( Abc_FrameReadNtk(pAbc) );
+    Abc_Ntk_t * pBest = Abc_NtkDup( Abc_FrameReadNtk(pAbc) );
+    Abc_Ntk_t * pCur = NULL;  int i;
+    char * pComms[6] = { "balance", "rewrite", "rewrite -z", "refactor", "refactor -z", "resub" };
+    srand( time(NULL) );
+    for ( i = 0; i < nIters; i++ )
+    {
+        char * pScript = Cmd_GenScript( pComms, 6, nParts );
+        Abc_FrameSetCurrentNetwork( pAbc, Abc_NtkDup(pCopy) );
+        if ( Abc_FrameIsBatchMode() )
+        {
+            if ( Cmd_CommandExecute(pAbc, pScript) )
+            {
+                Abc_Print( 1, "Something did not work out with the command \"%s\".\n", pScript );
+                return;
+            }
+        }
+        else
+        {
+            Abc_FrameSetBatchMode( 1 );
+            if ( Cmd_CommandExecute(pAbc, pScript) )
+            {
+                Abc_Print( 1, "Something did not work out with the command \"%s\".\n", pScript );
+                Abc_FrameSetBatchMode( 0 );
+                return;
+            }
+            Abc_FrameSetBatchMode( 0 );
+        }
+        pCur = Abc_FrameReadNtk(pAbc);
+        if ( Abc_NtkNodeNum(pCur) < Abc_NtkNodeNum(pBest) ) {
+            Abc_Obj_t * pObj; int k;
+            Abc_NtkForEachObj( pBest, pObj, k )
+                pObj->fMarkA = pObj->fMarkB = pObj->fMarkC = 0;
+            Abc_NtkDelete( pBest );
+            pBest = Abc_NtkDup( pCur );
+        }
+    }
+    Abc_FrameSetCurrentNetwork( pAbc, pBest );
+    Abc_NtkDelete( pCopy );
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/base/io/io.c b/src/base/io/io.c
index 7b8ca184e..e808d1d0b 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -276,6 +276,18 @@ int IoCommandRead( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 0;
     }
     // read the file using the corresponding file reader
+    if ( strstr(pFileName, ".") && !strcmp(strstr(pFileName, "."), ".s") ) 
+    {
+        char Command[1000];
+        assert( strlen(pFileName) < 980 );
+        sprintf( Command, "source -x %s", pFileName );
+        if ( Cmd_CommandExecute( pAbc, Command ) )
+        {
+            fprintf( stdout, "Cannot execute command \"%s\".\n", Command );
+            return 1;
+        }
+        return 0;
+    }
     pNtk = Io_Read( pFileName, Io_ReadFileType(pFileName), fCheck, fBarBufs );
     if ( pNtk == NULL )
         return 0;
diff --git a/src/base/main/abcapis.h b/src/base/main/abcapis.h
index e1e05f4c7..30494f77c 100644
--- a/src/base/main/abcapis.h
+++ b/src/base/main/abcapis.h
@@ -107,7 +107,7 @@ extern ABC_DLL int    Abc_FrameReadProbStatus( Abc_Frame_t * pAbc );
 extern ABC_DLL void * Abc_FrameReadCex( Abc_Frame_t * pAbc );    
 
 // procedure to set retiming data
-extern ABC_DLL void   Abc_FrameSetRetimingData( Abc_Frame_t * pAbc, int * pRst, int * pSet, int * pEna );
+extern ABC_DLL void   Abc_FrameSetRetimingData( Abc_Frame_t * pAbc, int * pRst, int * pSet, int * pEna, int nRegs );
 
 // procedure to return sequential equivalences
 extern ABC_DLL int *  Abc_FrameReadMiniAigEquivClasses( Abc_Frame_t * pAbc );
diff --git a/src/map/scl/sclLiberty.c b/src/map/scl/sclLiberty.c
index 674f65549..3d62b68e5 100644
--- a/src/map/scl/sclLiberty.c
+++ b/src/map/scl/sclLiberty.c
@@ -83,7 +83,7 @@ struct Scl_Tree_t_
 
 static inline int          Scl_LibertyGlobMatch(const char * pattern, const char * string) {
     #ifdef _WIN32
-    return PathMatchSpec(string, pattern);
+    return PathMatchSpec(string, pattern); // if the compiler complains, add "-lshlwapi"
     #else
     return fnmatch(pattern, string, 0) == 0;
     #endif
diff --git a/src/proof/cec/cecProve.c b/src/proof/cec/cecProve.c
new file mode 100644
index 000000000..748f506f9
--- /dev/null
+++ b/src/proof/cec/cecProve.c
@@ -0,0 +1,205 @@
+/**CFile****************************************************************
+
+  FileName    [cecSplit.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Combinational equivalence checking.]
+
+  Synopsis    [Cofactoring for combinational miters.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: cecSplit.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include <math.h>
+#include "aig/gia/gia.h"
+#include "aig/gia/giaAig.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                              ///
+////////////////////////////////////////////////////////////////////////
+
+#ifndef ABC_USE_PTHREADS
+
+int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int fVerbose, int fVeryVerbose, int fSilent ) { return -1; }
+
+#else // pthreads are used
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cec_GiaProveOne( Gia_Man_t * p, int iEngine, int nTimeOut, Abc_Cex_t ** ppCex )
+{
+    abctime clk = Abc_Clock();
+    //abctime clkStop = nTimeOut * CLOCKS_PER_SEC + Abc_Clock();
+    printf( "Calling engine %d with timeout %d sec.\n", iEngine, nTimeOut );
+    if ( iEngine == 0 )
+    {
+    }
+    else if ( iEngine == 1 )
+    {
+    }    
+    else if ( iEngine == 2 )
+    {
+    }    
+    else if ( iEngine == 3 )
+    {
+    }
+    else assert( 0 );
+    //while ( Abc_Clock() < clkStop );
+    printf( "Engine %d finished.   ", iEngine );
+    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );    
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+#define PAR_THR_MAX 8
+typedef struct Par_ThData_t_
+{
+    Gia_Man_t * p;
+    Abc_Cex_t * pCex;
+    int         iEngine;
+    int         fWorking;
+    int         nTimeOut;
+    int         Result;
+} Par_ThData_t;
+void * Cec_GiaProveWorkerThread( void * pArg )
+{
+    Par_ThData_t * pThData = (Par_ThData_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;
+        }
+        pThData->Result = Cec_GiaProveOne( pThData->p, pThData->iEngine, pThData->nTimeOut, &pThData->pCex );
+        pThData->fWorking = 0;
+    }
+    assert( 0 );
+    return NULL;
+}
+int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int fVerbose, int fVeryVerbose, int fSilent )
+{
+    abctime clkTotal = Abc_Clock();
+    Par_ThData_t ThData[PAR_THR_MAX];
+    pthread_t WorkerThread[PAR_THR_MAX];
+    int i, status, RetValue = -1;
+    Abc_CexFreeP( &p->pCexComb );
+    Abc_CexFreeP( &p->pCexSeq );        
+    if ( fVerbose )
+        printf( "Solving verification problem with the following parameters:\n" );
+    if ( fVerbose )
+        printf( "Processes = %d   TimeOut = %d sec   Verbose = %d.\n", nProcs, nTimeOut, fVerbose );
+    fflush( stdout );
+    if ( nProcs == 1 )
+        return -1;
+    // subtract manager thread
+    nProcs--;
+    assert( (nProcs == 4 || nProcs == 8) && nProcs <= PAR_THR_MAX );
+    // start threads
+    for ( i = 0; i < nProcs; i++ )
+    {
+        ThData[i].p        = Gia_ManDup(p);
+        ThData[i].pCex     = NULL;
+        ThData[i].iEngine  = i;
+        ThData[i].nTimeOut = nTimeOut;
+        ThData[i].fWorking = 0;
+        ThData[i].Result   = -1;
+        status = pthread_create( WorkerThread + i, NULL,Cec_GiaProveWorkerThread, (void *)(ThData + i) );  assert( status == 0 );
+    }
+
+    for ( i = 0; i < nProcs; i++ )
+        ThData[i].fWorking = 1;
+    
+    // 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 );
+        // cleanup
+        Gia_ManStopP( &ThData[i].p );        
+        if ( !p->pCexSeq && ThData[i].pCex )
+            p->pCexSeq = Abc_CexDup( ThData[i].pCex, -1 );
+        Abc_CexFreeP( &ThData[i].pCex );
+        // stop
+        ThData[i].p = NULL;
+        ThData[i].fWorking = 1;
+    }
+    if ( !fSilent )
+    {
+        if ( RetValue == 0 )
+            printf( "Problem is SAT " );
+        else if ( RetValue == 1 )
+            printf( "Problem is UNSAT " );
+        else if ( RetValue == -1 )
+            printf( "Problem is UNDECIDED " );
+        else assert( 0 );
+        printf( ".  " );
+        Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
+        fflush( stdout );
+    }
+    return RetValue;
+}
+
+#endif // pthreads are used
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/proof/cec/module.make b/src/proof/cec/module.make
index ed3dac110..ed8deba98 100644
--- a/src/proof/cec/module.make
+++ b/src/proof/cec/module.make
@@ -6,6 +6,7 @@ SRC +=    src/proof/cec/cecCec.c \
     src/proof/cec/cecIso.c \
     src/proof/cec/cecMan.c \
     src/proof/cec/cecPat.c \
+    src/proof/cec/cecProve.c \
     src/proof/cec/cecSat.c \
     src/proof/cec/cecSatG.c \
     src/proof/cec/cecSatG2.c \