diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 5e8f5f36d..f12ab35df 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -1793,21 +1793,26 @@ extern int                 Tas_ManSolveArray( Tas_Man_t * p, Vec_Ptr_t * vObjs )
 /*=== giaBound.c ===========================================================*/
 typedef struct Bnd_Man_t_  Bnd_Man_t;
 
-extern Bnd_Man_t*           Bnd_ManStart( Gia_Man_t *pSpec, Gia_Man_t *pImpl );
+extern Bnd_Man_t*           Bnd_ManStart( Gia_Man_t *pSpec, Gia_Man_t *pImpl, int fVerbose );
 extern void                 Bnd_ManStop();
+
+// getter
+extern int                  Bnd_ManGetNInternal();
+extern int                  Bnd_ManGetNExtra();
+
 //for fraig
 extern void                 Bnd_ManMap( int iLit, int id, int spec );
 extern void                 Bnd_ManMerge( int id1, int id2, int phaseDiff );
 extern void                 Bnd_ManFinalizeMappings();
 extern void                 Bnd_ManPrintMappings();
 // for eco
-extern int                  Bnd_ManCheckBound( Gia_Man_t *p );
+extern int                  Bnd_ManCheckBound( Gia_Man_t *p, int fVerbose );
 extern void                 Bnd_ManFindBound( Gia_Man_t *p );
 extern Gia_Man_t*           Bnd_ManGenSpecOut( Gia_Man_t *p );
 extern Gia_Man_t*           Bnd_ManGenImplOut( Gia_Man_t *p );
 extern Gia_Man_t*           Bnd_ManGenPatched( Gia_Man_t *pOut, Gia_Man_t *pSpec, Gia_Man_t *pPatch );
 extern Gia_Man_t*           Bnd_ManGenPatched1( Gia_Man_t *pOut, Gia_Man_t *pSpec );
-extern Gia_Man_t*           Bnd_ManGenPatched2( Gia_Man_t *p, Gia_Man_t *pPatch );
+extern Gia_Man_t*           Bnd_ManGenPatched2( Gia_Man_t *pImpl, Gia_Man_t *pPatch, int fSkiptStrash, int fVerbose );
 extern void                 Bnd_ManSetEqOut( int eq );
 extern void                 Bnd_ManSetEqRes( int eq );
 extern void                 Bnd_ManPrintStats();
diff --git a/src/aig/gia/giaBound.c b/src/aig/gia/giaBound.c
index a3a298e35..a420b818d 100644
--- a/src/aig/gia/giaBound.c
+++ b/src/aig/gia/giaBound.c
@@ -29,6 +29,7 @@ struct Bnd_Man_t_
     int nNode_patched;
 
     int status; // 0: init 1: boundary found 2: out generated 3: patched generated
+    int fVerbose;
 
     int combLoop_spec;
     int combLoop_impl;
@@ -57,7 +58,7 @@ struct Bnd_Man_t_
 
 };
 
-Bnd_Man_t* pBnd;
+Bnd_Man_t* pBnd = 0;
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -78,7 +79,7 @@ void Bnd_ManSetEqRes( int eq ) { pBnd -> eq_res = eq;}
 
 ***********************************************************************/
 
-Bnd_Man_t* Bnd_ManStart( Gia_Man_t *pSpec, Gia_Man_t *pImpl )
+Bnd_Man_t* Bnd_ManStart( Gia_Man_t *pSpec, Gia_Man_t *pImpl, int fVerbose )
 {
     int i;
     Bnd_Man_t* p = ABC_CALLOC( Bnd_Man_t, 1 );
@@ -113,6 +114,8 @@ Bnd_Man_t* Bnd_ManStart( Gia_Man_t *pSpec, Gia_Man_t *pImpl )
     p -> nNode_patched = 0;
 
     p -> status = 0;
+    p -> fVerbose = fVerbose;
+
     p -> combLoop_spec = 0;
     p -> combLoop_impl = 0;
     p -> eq_out = 0;
@@ -166,6 +169,8 @@ void Bnd_ManStop()
     ABC_FREE( pBnd );
 }
 
+int Bnd_ManGetNInternal() { assert(pBnd); return pBnd -> nInternal; }
+int Bnd_ManGetNExtra() { assert(pBnd); return pBnd -> nExtra; }
 
 void Bnd_ManMap( int iLit, int id, int spec )
 {
@@ -370,23 +375,22 @@ void Bnd_ManPrintStats()
 
   Description [check if the given boundary is valid. Return 0 if
   the boundary is invalid. Return k if the boundary is valid and
-  there're k boundary inputs. ]
+  there're k boundary inputs. 
+  Can be called even if Bnd_Man_t is not created]
 
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-int Bnd_ManCheckBound( Gia_Man_t * p )
+int Bnd_ManCheckBound( Gia_Man_t * p, int fVerbose )
 {
     int i;
     Gia_Obj_t *pObj;
     int valid = 1;
-    pBnd -> nBI = 0;
-    pBnd -> nBO = 0;
-    pBnd -> nInternal = 0;
+    int nBI = 0, nBO = 0, nInternal = 0;
 
-    printf( "Checking boundary... \n");
+    if ( fVerbose ) printf( "Checking boundary... \n");
 
     Vec_Int_t *vPath;
     vPath = Vec_IntAlloc( Gia_ManObjNum(p) );
@@ -417,7 +421,7 @@ int Bnd_ManCheckBound( Gia_Man_t * p )
             if ( path == 1 )  // boundary input
             {
                 // TODO: record BIs here since they may not be in the first n buffers
-                pBnd -> nBO ++;
+                nBO ++;
             }
         }
         else if ( Gia_ObjFaninNum( p, pObj ) >= 1 )
@@ -431,7 +435,7 @@ int Bnd_ManCheckBound( Gia_Man_t * p )
             if ( path == 2 )  // inside boundary
             {
                 // TODO: record BIs here since they may not be in the first n buffers
-                pBnd -> nInternal ++;
+                nInternal ++;
             }
         }
         else // PI or const, check validity
@@ -445,20 +449,33 @@ int Bnd_ManCheckBound( Gia_Man_t * p )
         }
     }
 
-    pBnd -> nBI = Gia_ManBufNum(p) - pBnd -> nBO;
+    nBI = Gia_ManBufNum(p) - nBO;
 
     if ( !valid ) 
     {
         printf("invalid boundary\n");
         return 0;
     }
+    else if ( nBI == 0 )
+    {
+        printf("no boundary\n");
+        return 0;
+    }
     else 
     {
-        printf("valid boundary (");
-        printf("#BI = %d\t#BO = %d\t", pBnd -> nBI, Gia_ManBufNum(p)- pBnd -> nBI);
-        printf("#Internal = %d)\n", pBnd -> nInternal );
-        assert( pBnd -> nBI > 0 );
-        return pBnd -> nBI;
+        if ( fVerbose )
+        {
+            printf("valid boundary (");
+            printf("#BI = %d\t#BO = %d\t", nBI, Gia_ManBufNum(p)- nBI);
+            printf("#Internal = %d)\n", nInternal );
+        }
+        if ( pBnd )
+        {
+            pBnd -> nBI = nBI;
+            pBnd -> nBO = nBO;
+            pBnd -> nInternal = nInternal;
+        }
+        return nBI;
     }
 }
 
@@ -593,7 +610,7 @@ void Bnd_ManFindBound( Gia_Man_t * p )
             Vec_IntPush(vEO_spec, id);
         }
     }
-    printf("%d BO doesn't match. ", Vec_PtrSize(vQ) );
+    if ( pBnd -> fVerbose )  printf("%d BO doesn't match. ", Vec_PtrSize(vQ) );
     pBnd -> nBO_miss = Vec_PtrSize(vQ);
 
     int cnt_extra = - Vec_PtrSize(vQ);
@@ -622,7 +639,7 @@ void Bnd_ManFindBound( Gia_Man_t * p )
         }
     }
     // printf("%d AO found with %d extra nodes\n", Vec_IntSize(vAO) , cnt_extra );
-     printf("%d AO found\n", Vec_IntSize(vAO) );
+    if ( pBnd -> fVerbose ) printf("%d AO found\n", Vec_IntSize(vAO) );
 
 
     // mark TFOC of BO with flag 1 to prevent them from being selected into EI
@@ -665,7 +682,7 @@ void Bnd_ManFindBound( Gia_Man_t * p )
             Vec_IntPush(vEI_spec, id);
         }
     }
-    printf("%d BI doesn't match. ", Vec_PtrSize(vQ) );
+    if ( pBnd -> fVerbose ) printf("%d BI doesn't match. ", Vec_PtrSize(vQ) );
     pBnd -> nBI_miss = Vec_PtrSize(vQ);
     cnt_extra -= Vec_PtrSize(vQ);
 
@@ -708,7 +725,7 @@ void Bnd_ManFindBound( Gia_Man_t * p )
 
         Vec_IntSetEntry( vFlag, id, 2 );
     }
-    printf("%d AI found with %d extra nodes in total\n", Vec_IntSize(vAI) , cnt_extra );
+    if ( pBnd -> fVerbose ) printf("%d AI found with %d extra nodes in total\n", Vec_IntSize(vAI) , cnt_extra );
     pBnd -> nExtra = cnt_extra;
 
 
@@ -738,8 +755,11 @@ void Bnd_ManFindBound( Gia_Man_t * p )
 
     // print
     pBnd -> status = 1;
-    printf("#EI = %d\t#EO = %d\t#Extra Node = %d\n", Vec_IntSize(vEI_spec) , Vec_IntSize(vEO_spec), cnt_extra );
-    Bnd_ManPrintBound();
+    if ( pBnd -> fVerbose )
+    {
+        printf("#EI = %d\t#EO = %d\t#Extra Node = %d\n", Vec_IntSize(vEI_spec) , Vec_IntSize(vEO_spec), cnt_extra );
+        Bnd_ManPrintBound();
+    }
 
     // check boundary has comb loop
     if ( !Bnd_ManCheckExtBound( p, vEI_spec, vEO_spec ) )
@@ -869,15 +889,15 @@ Gia_Man_t* Bnd_ManCutBoundary( Gia_Man_t *p, Vec_Int_t* vEI, Vec_Int_t* vEO, Vec
 
 }
 
-Gia_Man_t* Bnd_ManGenSpecOut( Gia_Man_t* p )
+Gia_Man_t* Bnd_ManGenSpecOut( Gia_Man_t* p  )
 {
-    printf("Generating spec_out with given boundary.\n");
+    if ( pBnd -> fVerbose ) printf("Generating spec_out with given boundary.\n");
     Gia_Man_t *pNew = Bnd_ManCutBoundary( p, pBnd->vEI_spec, pBnd->vEO_spec, 0, 0 );
     return pNew;
 }
-Gia_Man_t* Bnd_ManGenImplOut( Gia_Man_t* p )
+Gia_Man_t* Bnd_ManGenImplOut( Gia_Man_t* p)
 {
-    printf("Generating impl_out with given boundary.\n");
+    if ( pBnd -> fVerbose ) printf("Generating impl_out with given boundary.\n");
     Gia_Man_t *pNew = Bnd_ManCutBoundary( p, pBnd->vEI_impl, pBnd->vEO_impl, pBnd->vEI_phase, pBnd->vEO_phase );
     if ( pNew ) pBnd -> status = 2;
     else pBnd -> combLoop_impl = 1;
@@ -1066,7 +1086,7 @@ Gia_Man_t* Bnd_ManGenPatched1( Gia_Man_t *pOut, Gia_Man_t *pSpec )
     }
 
     // add Impl EI to CI
-    printf("adding EI to CI in Impl\n");
+    // printf("adding EI to CI in Impl\n");
     for ( i = 0; i < Vec_IntSize( pBnd -> vEI_spec ); i++ )
     {
         pObj = Gia_ManCo(pOut, i + Gia_ManCoNum(pSpec) );
@@ -1074,20 +1094,24 @@ Gia_Man_t* Bnd_ManGenPatched1( Gia_Man_t *pOut, Gia_Man_t *pSpec )
 
         // set Spec EI
         Gia_ManObj( pSpec, Vec_IntEntry(pBnd -> vEI_spec, i) ) -> Value = pObj -> Value;
-        printf(" %d",pObj -> Value);
+        // printf(" %d",pObj -> Value);
     }
-    printf("\n");
+    // printf("\n");
 
     // add Spec EO to EI
     // add BI -> BO -> EO to maintain the order of bufs
-    Vec_IntForEachEntry( pBnd -> vBI, id, i )
+    // Vec_IntForEachEntry( pBnd -> vBI, id, i )
+    // {
+    //     pObj = Gia_ManObj( pSpec, id );
+    //     Bnd_AddNodeRec( pSpec, pNew, pObj, 1 );
+    // }
+    // Vec_IntForEachEntry( pBnd -> vBO, id, i )
+    // {
+    //     pObj = Gia_ManObj( pSpec, id );
+    //     Bnd_AddNodeRec( pSpec, pNew, pObj, 1 );
+    // }
+    Gia_ManForEachBuf( pSpec, pObj, i )
     {
-        pObj = Gia_ManObj( pSpec, id );
-        Bnd_AddNodeRec( pSpec, pNew, pObj, 1 );
-    }
-    Vec_IntForEachEntry( pBnd -> vBO, id, i )
-    {
-        pObj = Gia_ManObj( pSpec, id );
         Bnd_AddNodeRec( pSpec, pNew, pObj, 1 );
     }
     Vec_IntForEachEntry( pBnd -> vEO_spec, id, i )
@@ -1123,6 +1147,100 @@ Gia_Man_t* Bnd_ManGenPatched1( Gia_Man_t *pOut, Gia_Man_t *pSpec )
     return pNew;
 }
 
+Gia_Man_t* Bnd_ManGenPatched2( Gia_Man_t *pImpl, Gia_Man_t *pPatch, int fSkipStrash, int fVerbose )
+{
+
+    Gia_Man_t * pNew, * pTemp;
+    Gia_Obj_t * pObj;
+    int i, nBI, nBI_patch, cnt;
+    Vec_Int_t* vLit;
+
+
+    // check boundary first
+    nBI = Bnd_ManCheckBound( pImpl, fVerbose );
+    nBI_patch = Bnd_ManCheckBound( pPatch, fVerbose );
+    if ( 0 == nBI_patch || Gia_ManBufNum(pImpl) != Gia_ManBufNum(pPatch) || nBI != nBI_patch )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9StrEco(): The given boundary is invalid.\n" );
+        return 0; 
+    }
+
+    // prepare new network
+    pNew = Gia_ManStart( Gia_ManObjNum(pImpl) + Gia_ManObjNum( pPatch ) );
+    pNew -> pName = ABC_ALLOC( char, strlen(pImpl->pName)+3);
+    sprintf( pNew -> pName, "%s_p", pImpl -> pName );
+    if ( !fSkipStrash )
+    {
+        Gia_ManHashAlloc( pNew );
+    }
+    Gia_ManFillValue(pImpl);
+    Gia_ManFillValue(pPatch);
+    Gia_ManConst0(pImpl)->Value = 0;
+    Gia_ManConst0(pPatch)->Value = 0;
+
+    vLit = Vec_IntAlloc( Gia_ManBufNum(pImpl) );
+
+    // add Impl (real) CI
+    Gia_ManForEachCi( pImpl, pObj, i )
+    {
+        pObj -> Value = Gia_ManAppendCi( pNew );
+    }
+
+    // add Impl BI to CI
+    cnt = 0;
+    Gia_ManForEachBuf( pImpl, pObj, i )
+    {
+        Bnd_AddNodeRec( pImpl, pNew, pObj, fSkipStrash );
+        Vec_IntPush( vLit, pObj -> Value );
+        cnt ++;
+        if ( cnt >= nBI ) break;
+    }
+    
+    // set BI in patch
+    // add patch BO to BI
+    cnt = 0;
+    Gia_ManForEachBuf( pPatch, pObj, i )
+    {
+        if ( cnt < nBI ) 
+        {
+            pObj -> Value = Vec_IntEntry( vLit, cnt );
+        }
+        else
+        {
+            Bnd_AddNodeRec( pPatch, pNew, pObj, fSkipStrash );
+            Vec_IntPush( vLit, pObj -> Value );
+        }
+        cnt ++;
+        if ( cnt == nBI ) Vec_IntClear( vLit );
+    }
+
+    // set BO in impl
+    cnt = 0;
+    Gia_ManForEachBuf( pImpl, pObj, i )
+    {
+        cnt ++;
+        if ( cnt <= nBI) continue;
+        pObj -> Value = Vec_IntEntry( vLit, cnt-nBI-1 );
+    }
+
+    // add impl CO to BO
+    Gia_ManForEachCo( pImpl, pObj, i )
+    {
+        Bnd_AddNodeRec( pImpl, pNew, pObj, fSkipStrash );
+        Gia_ManAppendCo( pNew, pObj -> Value );
+    }
+
+    // clean up
+    if ( !fSkipStrash ) 
+    {
+        Gia_ManHashStop( pNew );
+    }
+    Vec_IntFree( vLit );
+    pNew = Gia_ManCleanup( pTemp = pNew );
+    Gia_ManStop( pTemp );
+
+    return pNew;
+}
 
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 60aa58c08..d6363a0cc 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -52099,7 +52099,7 @@ int Abc_CommandAbc9BRecover( Abc_Frame_t * pAbc, int argc, char ** argv )
     extern Gia_Man_t * Cec4_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars );
     extern void Cec4_ManSetParams( Cec_ParFra_t * pPars );
     extern Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose );
-    Gia_Man_t *pSpec, *pImpl_out = 0, *pSpec_out = 0, *pMiter, *pPatched, *pTemp, *pBmiter;
+    Gia_Man_t *pSpec, *pImpl_out = 0, *pSpec_out = 0, *pMiter, *pPatched = 0, *pTemp, *pBmiter;
     char * FileName = NULL;
     FILE * pFile = NULL;
     int c, fVerbose = 0, success = 1;
@@ -52165,7 +52165,7 @@ int Abc_CommandAbc9BRecover( Abc_Frame_t * pAbc, int argc, char ** argv )
     }    
 
     // start boundary manager
-    pBnd = Bnd_ManStart( pSpec, pAbc->pGia );
+    pBnd = Bnd_ManStart( pSpec, pAbc->pGia, fVerbose );
 
     // verify if spec eq impl
     pMiter = Gia_ManMiter( pAbc->pGia, pSpec, 0, 1, 0, 0, 0 );
@@ -52179,7 +52179,7 @@ int Abc_CommandAbc9BRecover( Abc_Frame_t * pAbc, int argc, char ** argv )
     // check boundary
     if ( success )
     {
-        if ( 0 == Bnd_ManCheckBound( pSpec ) )
+        if ( 0 == Bnd_ManCheckBound( pSpec, fVerbose ) )
         {
             Abc_Print( -1, "Abc_CommandAbc9BRecover(): The given spec has invalid boundary.\n" );
             success = 0;
@@ -52209,17 +52209,24 @@ int Abc_CommandAbc9BRecover( Abc_Frame_t * pAbc, int argc, char ** argv )
         // Gia_ManPrintStats( pImpl_out, pPars );
     }
 
-    if ( success )
+    if ( !success )
+    {
+        printf("Abc_CommandAbc9BRecover(): The generated boundary is invalid. The circuit is not changed.\n");
+    }
+    else
     {
 
         // check if spec_out and imnpl_out are equivalent
-        printf("Checking the equivalence of spec_out and impl_out\n");
-        pMiter = Gia_ManMiter( pSpec_out, pImpl_out, 0, 1, 0, 0, 0 );
-        Bnd_ManSetEqOut( Cec_ManVerify( pMiter, pParsCec ) );
-        Gia_ManStop( pMiter );
+        if ( fVerbose ) 
+        {
+            printf("Checking the equivalence of spec_out and impl_out\n");
+            pMiter = Gia_ManMiter( pSpec_out, pImpl_out, 0, 1, 0, 0, 0 );
+            Bnd_ManSetEqOut( Cec_ManVerify( pMiter, pParsCec ) );
+            Gia_ManStop( pMiter );
+        }
 
         // generate patched impl
-        printf("Generating patched impl\n");
+        if ( fVerbose ) printf("Generating patched impl\n");
         pPatched = Bnd_ManGenPatched1( pImpl_out, pSpec );
 
         // // generate patched spec just for debugging
@@ -52237,29 +52244,35 @@ int Abc_CommandAbc9BRecover( Abc_Frame_t * pAbc, int argc, char ** argv )
         // Gia_ManStop( pTemp );
 
         // check if patched is equiv to spec
-        printf("Checking the equivalence of patched impl and patch\n");
+        if ( fVerbose ) printf("Checking the equivalence of patched impl and spec\n");
         pMiter = Gia_ManMiter( pSpec, pPatched, 0, 1, 0, 0, 0 );
-        Bnd_ManSetEqRes( Cec_ManVerify( pMiter, pParsCec ) );
+        success = Cec_ManVerify( pMiter, pParsCec );
+        Bnd_ManSetEqRes( success );
+        if ( !success )
+        {
+            printf("Failed. The generated AIG is not equivalent.\n");
+        }
         Gia_ManStop( pMiter );
 
     }
 
-    Bnd_ManPrintStats();
+    if ( fVerbose ) Bnd_ManPrintStats();
 
     Gia_ManStop( pSpec );
     if ( pSpec_out ) Gia_ManStop( pSpec_out );
     if ( pImpl_out ) Gia_ManStop( pImpl_out );
     if ( success )
     {
-        Abc_FrameUpdateGia( pAbc, pPatched );
+        printf("Success. The generated hierarchical impl is equivalent. (box size: %d -> %d)\n", Bnd_ManGetNInternal(), Bnd_ManGetNInternal() + Bnd_ManGetNExtra() );
     }
+    if (pPatched) Abc_FrameUpdateGia( pAbc, pPatched );
     Bnd_ManStop();
 
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &str_eco -I <biNum> [-vh] <impl> <patch>\n" );
-    Abc_Print( -2, "\t         SAT-sweeping-based ECO\n" );
+    Abc_Print( -2, "usage: &brecover -I <biNum> [-vh] <impl> <patch>\n" );
+    Abc_Print( -2, "\t         recover boundary using SAT-Sweeping\n" );
     Abc_Print( -2, "\t-v     : toggles printing verbose information [default = %s]\n",  fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     Abc_Print( -2, "\t<impl> : the implementation aig. (should be equivalent to spec)\n");    
@@ -52283,11 +52296,11 @@ int Abc_CommandAbc9StrEco( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     extern Gia_Man_t * Cec4_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars );
     extern void Cec4_ManSetParams( Cec_ParFra_t * pPars );
-    extern Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose );
-    Gia_Man_t *pImpl, *pImpl_out = 0, *pSpec_out = 0, *pMiter, *pPatch, *pPatched, *pTemp, *pBmiter;;
+    Gia_Man_t *pMiter, *pPatch, *pPatched;
     char * FileName = NULL;
     FILE * pFile = NULL;
-    int c, fVerbose = 0, success = 1;
+    int c, success = 1;
+    int fVerbose = 0, fSkipStrash = 0;
 
     // params
     Gps_Par_t Pars, * pPars = &Pars;
@@ -52300,13 +52313,16 @@ int Abc_CommandAbc9StrEco( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // parse options
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "vsh" ) ) != EOF )
     {
         switch ( c )
         {
         case 'v':
             fVerbose ^= 1;
             break;
+        case 's':
+            fSkipStrash ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -52318,33 +52334,15 @@ int Abc_CommandAbc9StrEco( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Abc_CommandAbc9StrEco(): There is no AIG.\n" );
         return 0;
     }
-    if ( argc != globalUtilOptind + 2 )
+    if ( argc != globalUtilOptind + 1 )
     {
         printf("%d\n", argc-globalUtilOptind);
         Abc_Print( -1, "Abc_CommandAbc9StrEco(): AIG should be given on the command line.\n" );
         return 0;
     }
 
-    // read impl
-    FileName = argv[globalUtilOptind];
-    if ( (pFile = fopen( FileName, "r" )) == NULL )
-    {
-        Abc_Print( -1, "Cannot open input file \"%s\". ", FileName );
-        if ( (FileName = Extra_FileGetSimilarName( FileName, ".aig", ".blif", ".pla", ".eqn", ".bench" )) )
-            Abc_Print( 1, "Did you mean \"%s\"?", FileName );
-        Abc_Print( 1, "\n" );
-        return 1;
-    }
-    fclose( pFile );
-    pImpl = Gia_AigerRead( FileName, 0, 0, 0 );
-    if ( pImpl == NULL )
-    {
-        Abc_Print( -1, "Abc_CommandAbc9StrEco(): Cannot read the file name on the command line.\n" );
-        return 0;
-    }    
-
     // read patch
-    FileName = argv[globalUtilOptind+1];
+    FileName = argv[globalUtilOptind];
     if ( (pFile = fopen( FileName, "r" )) == NULL )
     {
         Abc_Print( -1, "Cannot open input file \"%s\". ", FileName );
@@ -52361,98 +52359,29 @@ int Abc_CommandAbc9StrEco( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 0;
     }    
 
-    // start boundary manager
-    pBnd = Bnd_ManStart( pAbc->pGia, pImpl );
+    // generate patched impl
+    if ( fVerbose ) printf("Generating patched impl\n");
+    pPatched = Bnd_ManGenPatched2( pAbc->pGia, pPatch, fSkipStrash, fVerbose );
 
-    // verify if spec eq impl
-    pMiter = Gia_ManMiter( pAbc->pGia, pImpl, 0, 1, 0, 0, 0 );
-    if ( !Cec_ManVerify( pMiter, pParsCec ) )
+    if ( pPatched )
     {
-        Abc_Print( -1, "Abc_CommandAbc9StrEco(): The given impl is not equivalent to spec.\n" );
-        success = 0;
-    }
-    Gia_ManStop(pMiter);
-
-    // check boundary
-    if ( success )
-    {
-        if ( 0 == Bnd_ManCheckBound( pPatch ) || 0 == Bnd_ManCheckBound( pAbc -> pGia ) )
-        {
-            Abc_Print( -1, "Abc_CommandAbc9StrEco(): The given boundary is invalid.\n" );
-            success = 0;
-        }
-    }
-
-    if ( success )
-    {
-        // create bmiter, run fraig
-        pBmiter = Gia_ManBoundaryMiter( pAbc -> pGia, pImpl, 0 );
-        pTemp = Cec4_ManSimulateTest( pBmiter, pParsFra );
-        Gia_ManStop(pBmiter);
-        Gia_ManStop(pTemp);
-
-        // find 
-        Bnd_ManFindBound( pAbc -> pGia );
-
-        // create spec_out and 
-        pSpec_out = Bnd_ManGenSpecOut( pAbc -> pGia );
-        if ( !pSpec_out ) success = 0;
-        pImpl_out = Bnd_ManGenImplOut( pImpl );
-        if ( !pImpl_out ) success = 0;
-
-        // Gia_AigerWrite( pSpec_out, "spec_out.aig", 0, 0, 0 );
-        // Gia_AigerWrite( pImpl_out, "impl_out.aig", 0, 0, 0 );
-        // Gia_ManPrintStats( pSpec_out, pPars );
-        // Gia_ManPrintStats( pImpl_out, pPars );
-
-    }
-
-    if ( success )
-    {
-
-        // check if spec_out and imnpl_out are equivalent
-        printf("Checking the equivalence of spec_out and impl_out\n");
-        pMiter = Gia_ManMiter( pSpec_out, pImpl_out, 0, 1, 0, 0, 0 );
-        Bnd_ManSetEqOut( Cec_ManVerify( pMiter, pParsCec ) );
-        Gia_ManStop( pMiter );
-
-        // generate patched impl
-        printf("Generating patched impl\n");
-        pPatched = Bnd_ManGenPatched( pImpl_out, pAbc->pGia, pPatch );
-
-        // generate patched spec just for debugging
-        printf("Generating patched spec\n");
-        pTemp = Bnd_ManGenPatched( pSpec_out, pAbc->pGia, pPatch );
-        printf("Checking the equivalence of patched spec and patched impl\n");
-        pMiter = Gia_ManMiter( pTemp, pPatched, 0, 1, 0, 0, 0 );
-        Cec_ManVerify( pMiter, pParsCec );
-        Gia_ManStop( pMiter );
-        printf("Checking the equivalence of patched spec and patch\n");
-        pMiter = Gia_ManMiter( pTemp, pPatch, 0, 1, 0, 0, 0 );
-        Cec_ManVerify( pMiter, pParsCec );
-        Gia_ManStop( pMiter );
-
-        Gia_ManStop( pTemp );
-
         // check if patched is equiv to patch
-        printf("Checking the equivalence of patched impl and patch\n");
+        if ( fVerbose ) printf("Checking the equivalence of patched impl and patch\n");
         pMiter = Gia_ManMiter( pPatch, pPatched, 0, 1, 0, 0, 0 );
-        Bnd_ManSetEqRes( Cec_ManVerify( pMiter, pParsCec ) );
+        success = Cec_ManVerify( pMiter, pParsCec );
+        if( !success ) 
+        {
+            printf("Failed. The patched circuit is not equivalent.\n");
+        }
         Gia_ManStop( pMiter );
-
-    }
-
-    Bnd_ManPrintStats();
-
-    Gia_ManStop( pImpl );
-    Gia_ManStop( pPatch );
-    if ( pSpec_out ) Gia_ManStop( pSpec_out );
-    if ( pImpl_out ) Gia_ManStop( pImpl_out );
-    if ( success )
-    {
         Abc_FrameUpdateGia( pAbc, pPatched );
     }
-    Bnd_ManStop();
+
+    Gia_ManStop( pPatch );
+    if ( success )
+    {
+        printf("Success. The patched circuit is equivalent.\n");
+    }
 
     return 0;
 
@@ -52460,6 +52389,7 @@ usage:
     Abc_Print( -2, "usage: &str_eco -I <biNum> [-vh] <impl> <patch>\n" );
     Abc_Print( -2, "\t         SAT-sweeping-based ECO\n" );
     Abc_Print( -2, "\t-v     : toggles printing verbose information [default = %s]\n",  fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-s     : toggles skipping structural hash [default = %s]\n",  fSkipStrash? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     Abc_Print( -2, "\t<impl> : the implementation aig. (should be equivalent to spec)\n");    
     Abc_Print( -2, "\t<patch> : the modified spec. (should be a hierarchical AIG)\n");