diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index fc75642d8..b73732c62 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -37280,12 +37280,13 @@ int Abc_CommandAbc9Fraig( 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_ManSimulateTest5( Gia_Man_t * p, int nConfs, int fVerbose );
     extern Gia_Man_t * Cec5_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars, int fCbs, int approxLim, int subBatchSz, int adaRecycle );
+    extern Gia_Man_t * Gia_ManIvyFraig( Gia_Man_t * p, int nConfLimit, int fUseProve, int fVerbose );
     Cec_ParFra_t ParsFra, * pPars = &ParsFra; Gia_Man_t * pTemp;
-    int c, fUseAlgo = 0, fUseAlgoG = 0, fUseAlgoX = 0, fUseAlgoY = 0, fUseSave = 0;
-    int fCbs = 1, approxLim = 600, subBatchSz = 1, adaRecycle = 500;
+    int c, fUseAlgo = 0, fUseAlgoG = 0, fUseAlgoX = 0, fUseAlgoY = 0, fUseSave = 0, fUseIvy = 0, fUseProve = 0;
+    int fCbs = 1, approxLim = 600, subBatchSz = 1, adaRecycle = 500, nMaxNodes = 0;
     Cec4_ManSetParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "JWRILDCNPrmdckngxyswvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "JWRILDCNPMrmdckngxysopwvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -37388,6 +37389,17 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nGenIters < 0 )
                 goto usage;
             break;
+        case 'M':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nMaxNodes = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nMaxNodes < 0 )
+                goto usage;
+            break;
         case 'r':
             pPars->fRewriting ^= 1;
             break;
@@ -37418,6 +37430,12 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 's':
             fUseSave ^= 1;
             break;
+        case 'o':
+            fUseIvy ^= 1;
+            break;
+        case 'p':
+            fUseProve ^= 1;
+            break;
         case 'w':
             pPars->fVeryVerbose ^= 1;
             break;
@@ -37438,6 +37456,8 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
         Cec4_ManSimulateTest5( pAbc->pGia, pPars->nBTLimit, pPars->fVerbose );
         return 0;
     }
+    else if ( fUseIvy && (!nMaxNodes || Gia_ManAndNum(pAbc->pGia) < nMaxNodes) )
+        pTemp = Gia_ManIvyFraig( pAbc->pGia, pPars->nBTLimit, fUseProve, pPars->fVerbose );
     else if ( fUseAlgo )
         pTemp = Cec2_ManSimulateTest( pAbc->pGia, pPars );
     else if ( fUseAlgoG )
@@ -37458,7 +37478,7 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &fraig [-JWRILDCNP <num>] [-rmdckngxyswvh]\n" );
+    Abc_Print( -2, "usage: &fraig [-JWRILDCNPM <num>] [-rmdckngxysopwvh]\n" );
     Abc_Print( -2, "\t         performs combinational SAT sweeping\n" );
     Abc_Print( -2, "\t-J num : the solver type [default = %d]\n", pPars->jType );
     Abc_Print( -2, "\t-W num : the number of simulation words [default = %d]\n", pPars->nWords );
@@ -37469,6 +37489,7 @@ usage:
     Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
     Abc_Print( -2, "\t-N num : the min number of calls to recycle the solver [default = %d]\n", pPars->nCallsRecycle );
     Abc_Print( -2, "\t-P num : the number of pattern generation iterations [default = %d]\n", pPars->nGenIters );
+    Abc_Print( -2, "\t-M num : the node count limit to call the old sweeper [default = %d]\n", nMaxNodes );
     Abc_Print( -2, "\t-r     : toggle the use of AIG rewriting [default = %s]\n", pPars->fRewriting? "yes": "no" );
     Abc_Print( -2, "\t-m     : toggle miter vs. any circuit [default = %s]\n", pPars->fCheckMiter? "miter": "circuit" );
     Abc_Print( -2, "\t-d     : toggle using double output miters [default = %s]\n", pPars->fDualOut? "yes": "no" );
@@ -37479,6 +37500,8 @@ usage:
     Abc_Print( -2, "\t-x     : toggle using another new implementation [default = %s]\n", fUseAlgoX? "yes": "no" );
     Abc_Print( -2, "\t-y     : toggle using another new implementation [default = %s]\n", fUseAlgoY? "yes": "no" );
     Abc_Print( -2, "\t-s     : toggle dumping equivalences into a file [default = %s]\n", fUseSave? "yes": "no" );
+    Abc_Print( -2, "\t-o     : toggle using the old SAT sweeper [default = %s]\n", fUseIvy? "yes": "no" );
+    Abc_Print( -2, "\t-p     : toggle trying to prove when running the old SAT sweeper [default = %s]\n", fUseProve? "yes": "no" );
     Abc_Print( -2, "\t-w     : toggle printing even more verbose information [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
diff --git a/src/base/abci/abcIvy.c b/src/base/abci/abcIvy.c
index c680f85a7..552370aa1 100644
--- a/src/base/abci/abcIvy.c
+++ b/src/base/abci/abcIvy.c
@@ -25,6 +25,7 @@
 #include "proof/fraig/fraig.h"
 #include "map/mio/mio.h"
 #include "aig/aig/aig.h"
+#include "aig/gia/gia.h"
 
 #ifdef ABC_USE_CUDD
 #include "bdd/extrab/extraBdd.h"
@@ -1141,6 +1142,105 @@ Vec_Int_t * Abc_NtkCollectLatchValuesIvy( Abc_Ntk_t * pNtk, int fUseDcs )
     return vArray;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Convert Ivy into Gia.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Ivy_Obj_t * Gia_ObjChild0Copy3( Ivy_Obj_t ** ppNodes, Gia_Obj_t * pObj, int Id )  { return Ivy_NotCond( ppNodes[Gia_ObjFaninId0(pObj, Id)], Gia_ObjFaninC0(pObj) ); }
+static inline Ivy_Obj_t * Gia_ObjChild1Copy3( Ivy_Obj_t ** ppNodes, Gia_Obj_t * pObj, int Id )  { return Ivy_NotCond( ppNodes[Gia_ObjFaninId1(pObj, Id)], Gia_ObjFaninC1(pObj) ); }
+
+Ivy_Man_t * Gia_ManToIvySimple( Gia_Man_t * p )
+{
+    Ivy_Man_t * pNew;
+    Gia_Obj_t * pObj; int i;
+    Ivy_Obj_t ** ppNodes = ABC_FALLOC( Ivy_Obj_t *, Gia_ManObjNum(p) );
+    // create the new manager
+    pNew = Ivy_ManStart( Gia_ManObjNum(p) );
+    // create the PIs
+    Gia_ManForEachObj( p, pObj, i )
+    {
+        if ( Gia_ObjIsAnd(pObj) )
+            ppNodes[i] = Ivy_And( pNew, Gia_ObjChild0Copy3(ppNodes, pObj, i), Gia_ObjChild1Copy3(ppNodes, pObj, i) );
+        else if ( Gia_ObjIsCi(pObj) )
+            ppNodes[i] = Ivy_ObjCreatePi( pNew );
+        else if ( Gia_ObjIsCo(pObj) )
+            ppNodes[i] = Ivy_ObjCreatePo( pNew, Gia_ObjChild0Copy3(ppNodes, pObj, Gia_ObjId(p, pObj)) );
+        else if ( Gia_ObjIsConst0(pObj) )
+            ppNodes[i] = Ivy_Not(Ivy_ManConst1(pNew));
+        else
+            assert( 0 );
+        assert( i == 0 || Ivy_ObjId(ppNodes[i]) == i );
+    }
+    ABC_FREE( ppNodes );
+    return pNew;
+}
+static inline int Gia_ObjChild0Copy4( int * pNodes, Ivy_Obj_t * pObj )  { return Abc_LitNotCond( pNodes[Ivy_Regular(pObj->pFanin0)->Id], Ivy_IsComplement(pObj->pFanin0) ); }
+static inline int Gia_ObjChild1Copy4( int * pNodes, Ivy_Obj_t * pObj )  { return Abc_LitNotCond( pNodes[Ivy_Regular(pObj->pFanin1)->Id], Ivy_IsComplement(pObj->pFanin1) ); }
+
+Gia_Man_t * Gia_ManFromIvySimple( Ivy_Man_t * p )
+{
+    Gia_Man_t * pNew;
+    Ivy_Obj_t * pObj;
+    int i, * pNodes = ABC_FALLOC( int, Ivy_ManObjIdMax(p) + 1 );
+    pNew = Gia_ManStart( Ivy_ManObjIdMax(p) );
+    pNew->pName = Abc_UtilStrsav( "from_ivy" );
+    Ivy_ManForEachObj( p, pObj, i )
+    {
+        if ( Ivy_ObjIsAnd(pObj) )
+            pNodes[pObj->Id] = Gia_ManAppendAnd( pNew, Gia_ObjChild0Copy4(pNodes, pObj), Gia_ObjChild1Copy4(pNodes, pObj) );
+        else if ( Ivy_ObjIsCi(pObj) )
+            pNodes[pObj->Id] = Gia_ManAppendCi( pNew );
+        else if ( Ivy_ObjIsCo(pObj) )
+            pNodes[pObj->Id] = Gia_ManAppendCo( pNew, Gia_ObjChild0Copy4(pNodes, pObj) );
+        else if ( Ivy_ObjIsConst1(pObj) )
+            pNodes[pObj->Id] = 1;
+        else
+            assert( 0 );
+    }
+    ABC_FREE( pNodes );
+    return pNew;
+}
+Gia_Man_t * Gia_ManIvyFraig( Gia_Man_t * p, int nConfLimit, int fUseProve, int fVerbose )
+{
+    Ivy_FraigParams_t Params, * pParams = &Params; 
+    Gia_Man_t * pNew;
+    Ivy_Man_t * pMan, * pTemp;
+    pMan = Gia_ManToIvySimple( p );
+    if ( pMan == NULL )
+        return NULL;
+    Ivy_FraigParamsDefault( pParams );
+    pParams->nBTLimitNode = nConfLimit;
+    pParams->fVerbose     = fVerbose;
+    pParams->fProve       = fUseProve;
+    pParams->fDoSparse    = 1;
+    pMan = Ivy_FraigPerform( pTemp = pMan, pParams );
+    pNew = Gia_ManFromIvySimple( pMan );
+    if ( pMan->pData )
+    {
+        p->pCexSeq = Abc_CexDeriveFromCombModel( (int *)pMan->pData, Ivy_ManPiNum(pMan), 0, -1 );
+        p->pCexSeq->iPo = Gia_ManFindFailedPoCex( p, p->pCexSeq, 0 );
+        ABC_FREE( pMan->pData );
+    }
+    Ivy_ManStop( pTemp );
+    Ivy_ManStop( pMan );
+    return pNew;
+}
+Gia_Man_t * Gia_ManIvyFraigTest( Gia_Man_t * p, int nConfLimit, int fVerbose )
+{
+    Ivy_Man_t * pMan = Gia_ManToIvySimple( p );
+    Gia_Man_t * pNew = Gia_ManFromIvySimple( pMan );
+    Ivy_ManStop( pMan );
+    return pNew;
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////