Added new command &gla_shrink.

10 files changed, 278 insertions, 29 deletions

diff --git a/src/aig/gia/giaAbsIter.c b/src/aig/gia/giaAbsIter.c
new file mode 100644
index 00000000..4600530b
--- /dev/null
+++ b/src/aig/gia/giaAbsIter.c
@@ -0,0 +1,149 @@
+/**CFile****************************************************************
+
+  FileName    [giaIter.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Scalable AIG package.]
+
+  Synopsis    [Iterative improvement of abstraction.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: giaIter.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "gia.h"
+#include "giaAig.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static inline int  Gia_ObjIsInGla( Gia_Man_t * p, Gia_Obj_t * pObj )    { return Vec_IntEntry(p->vGateClasses, Gia_ObjId(p, pObj));  }
+static inline void Gia_ObjAddToGla( Gia_Man_t * p, Gia_Obj_t * pObj )   { Vec_IntWriteEntry(p->vGateClasses, Gia_ObjId(p, pObj), 1); }
+static inline void Gia_ObjRemFromGla( Gia_Man_t * p, Gia_Obj_t * pObj ) { Vec_IntWriteEntry(p->vGateClasses, Gia_ObjId(p, pObj), 0); }
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_IterTryImprove( Gia_Man_t * p, int nTimeOut, int iFrame0 )
+{
+    extern int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite, int * piFrames, int fSilent );
+    Gia_Man_t * pAbs = Gia_ManDupAbsGates( p, p->vGateClasses );
+    Aig_Man_t * pAig = Gia_ManToAigSimple( pAbs );
+    int nStart      =            0;
+    int nFrames     =  iFrame0 ? iFrame0 + 1 : 10000000;
+    int nNodeDelta  =         2000;
+    int nBTLimit    =            0;
+    int nBTLimitAll =            0;
+    int fVerbose    =            0;
+    int RetValue, iFrame; 
+    RetValue = Saig_BmcPerform( pAig, nStart, nFrames, nNodeDelta, nTimeOut, nBTLimit, nBTLimitAll, fVerbose, 0, &iFrame, 1 );
+    assert( RetValue == 0 || RetValue == -1 );
+    Aig_ManStop( pAig );
+    Gia_ManStop( pAbs );
+    return iFrame;
+}
+Gia_Man_t * Gia_IterImprove( Gia_Man_t * p, int nFrameMax, int nTimeOut, int fUsePdr, int fUseSat, int fUseBdd, int fVerbose )
+{
+    Gia_Obj_t * pObj;
+    int i, iFrame0, iFrame;
+    int nTotal = 0, nRemoved = 0;
+    Vec_Int_t * vGScopy;
+    clock_t clk, clkTotal = clock();
+    assert( Gia_ManPoNum(p) == 1 );
+    assert( p->vGateClasses != NULL );
+    vGScopy = Vec_IntDup( p->vGateClasses );
+    if ( nFrameMax == 0 )
+        iFrame0 = Gia_IterTryImprove( p, 0, 0 );
+    else
+        iFrame0 = nFrameMax - 1;
+    while ( 1 )
+    {
+        int fChanges = 0;
+        Gia_ManForEachObj1( p, pObj, i )
+        {
+            if ( pObj->fMark0 )
+                continue;
+            if ( !Gia_ObjIsInGla(p, pObj) )
+                continue;
+            if ( pObj == Gia_ObjFanin0( Gia_ManPo(p, 0) ) )
+                continue;
+            if ( Gia_ObjIsAnd(pObj) )
+            {
+                if ( Gia_ObjIsInGla(p, Gia_ObjFanin0(pObj)) && Gia_ObjIsInGla(p, Gia_ObjFanin1(pObj)) )
+                    continue;
+            }
+            if ( Gia_ObjIsRo(p, pObj) )
+            {
+                if ( Gia_ObjIsInGla(p, Gia_ObjRoToRi(p, pObj)) )
+                    continue;
+            }        
+            clk = clock();
+            printf( "%5d : ", nTotal );
+            printf( "Obj =%7d   ", i );
+            Gia_ObjRemFromGla( p, pObj );
+            iFrame = Gia_IterTryImprove( p, nTimeOut, iFrame0 );
+            if ( nFrameMax )
+                assert( iFrame <= nFrameMax );
+            else
+                assert( iFrame <= iFrame0 );
+            printf( "Frame =%6d   ", iFrame );
+            if ( iFrame < iFrame0 )
+            {
+                pObj->fMark0 = 1;
+                Gia_ObjAddToGla( p, pObj );
+                printf( "           " );
+            }
+            else
+            {
+                fChanges = 1;
+                nRemoved++;
+                printf( "Removing   " );
+                Vec_IntWriteEntry( vGScopy, Gia_ObjId(p, pObj), 0 );
+            }
+            Abc_PrintTime( 1, "Time", clock() - clk );
+            nTotal++;
+            // update the classes
+            Vec_IntFreeP( &p->vGateClasses );
+            p->vGateClasses = Vec_IntDup(vGScopy);
+        }
+        if ( !fChanges )
+            break;
+    }
+    Gia_ManCleanMark0(p);
+    Vec_IntFree( vGScopy );
+    printf( "Tried = %d.  ",     nTotal );
+    printf( "Removed = %d. (%.2f %%)  ",  nRemoved, 100.0 * nRemoved / Vec_IntCountPositive(p->vGateClasses) );
+    Abc_PrintTime( 1, "Time",  clock() - clkTotal );
+    return NULL;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c
index bf1e4c06..62afe26c 100644
--- a/src/aig/gia/giaEquiv.c
+++ b/src/aig/gia/giaEquiv.c
@@ -1723,7 +1723,7 @@ int Gia_CommandSpecI( Gia_Man_t * pGia, int nFramesInit, int nBTLimitInit, int f
             pTemp = Gia_ManToAig( pSrm, 0 );
 //            Aig_ManPrintStats( pTemp );
             Gia_ManStop( pSrm );
-            Saig_BmcPerform( pTemp, nStart, nFrames, nNodeDelta, 0, nBTLimit, nBTLimitAll, fVerbose, 0, NULL );
+            Saig_BmcPerform( pTemp, nStart, nFrames, nNodeDelta, 0, nBTLimit, nBTLimitAll, fVerbose, 0, NULL, 0 );
             pCex = pTemp->pSeqModel; pTemp->pSeqModel = NULL;
             Aig_ManStop( pTemp );
             if ( pCex == NULL )
diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make
index 83399eb8..cac2986e 100644
--- a/src/aig/gia/module.make
+++ b/src/aig/gia/module.make
@@ -2,6 +2,7 @@ SRC +=    src/aig/gia/gia.c \
     src/aig/gia/giaAbs.c \
     src/aig/gia/giaAbsGla.c \
     src/aig/gia/giaAbsGla2.c \
+    src/aig/gia/giaAbsIter.c \
     src/aig/gia/giaAbsRef.c \
     src/aig/gia/giaAbsRef2.c \
     src/aig/gia/giaAbsVta.c \
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index ec33b3eb..e7cdea90 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -147,7 +147,7 @@ extern int               Saig_ManCexRefineStep( Aig_Man_t * p, Vec_Int_t * vFlop
 extern Vec_Int_t *       Saig_ManCexAbstractionFlops( Aig_Man_t * p, Gia_ParAbs_t * pPars );
 /*=== saigBmc.c ==========================================================*/
 extern int               Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fVerbose, int * piFrame, int nCofFanLit );
-extern int               Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite, int * piFrames );
+extern int               Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite, int * piFrames, int fSilent );
 /*=== saigBmc3.c ==========================================================*/
 extern void              Saig_ParBmcSetDefaultParams( Saig_ParBmc_t * p );
 extern int               Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars );
diff --git a/src/aig/saig/saigAbsStart.c b/src/aig/saig/saigAbsStart.c
index 51033dee..90efef26 100644
--- a/src/aig/saig/saigAbsStart.c
+++ b/src/aig/saig/saigAbsStart.c
@@ -72,7 +72,7 @@ int Saig_ManCexFirstFlopPi( Aig_Man_t * p, Aig_Man_t * pAbs )
 ***********************************************************************/
 Aig_Man_t * Saig_ManCexRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlops, int nFrames, int nConfMaxOne, int fUseBdds, int fUseDprove, int fVerbose, int * pnUseStart, int * piRetValue, int * pnFrames )
 { 
-    extern int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite, int * piFrames );
+    extern int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite, int * piFrames, int fSilent );
     Vec_Int_t * vFlopsNew;
     int i, Entry, RetValue;
     *piRetValue = -1;
@@ -119,7 +119,7 @@ Aig_Man_t * Saig_ManCexRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlo
     }
     else 
     {
-        Saig_BmcPerform( pAbs, pnUseStart? *pnUseStart: 0, nFrames, 2000, 0, nConfMaxOne, 0, fVerbose, 0, pnFrames );
+        Saig_BmcPerform( pAbs, pnUseStart? *pnUseStart: 0, nFrames, 2000, 0, nConfMaxOne, 0, fVerbose, 0, pnFrames, 0 );
     }
     if ( pAbs->pSeqModel == NULL )
         return NULL;
diff --git a/src/aig/saig/saigBmc2.c b/src/aig/saig/saigBmc2.c
index a1dee6e4..f70a0015 100644
--- a/src/aig/saig/saigBmc2.c
+++ b/src/aig/saig/saigBmc2.c
@@ -754,7 +754,7 @@ void Saig_BmcAddTargetsAsPos( Saig_Bmc_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite, int * piFrames )
+int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite, int * piFrames, int fSilent )
 {
     Saig_Bmc_t * p;
     Aig_Man_t * pNew;
@@ -817,7 +817,8 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax
         // check the timeout
         if ( nTimeOut && clock() > nTimeToStop )
         {
-            printf( "Reached timeout (%d seconds).\n",  nTimeOut );
+            if ( !fSilent )
+                printf( "Reached timeout (%d seconds).\n",  nTimeOut );
             if ( piFrames )
                 *piFrames = p->iFrameLast-1;
             Saig_BmcManStop( p );
@@ -827,15 +828,17 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax
     if ( RetValue == l_True )
     {
         assert( p->iFrameFail * Saig_ManPoNum(p->pAig) + p->iOutputFail + 1 == nOutsSolved );
-        printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", 
-            p->iOutputFail, p->iFrameFail );
+        if ( !fSilent )
+            printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", 
+                p->iOutputFail, p->iFrameFail );
         Status = 0;
         if ( piFrames )
             *piFrames = p->iFrameFail;
     }
     else // if ( RetValue == l_False || RetValue == l_Undef )
     {
-        printf( "No output was asserted in %d frames.  ", Abc_MaxInt(p->iFramePrev-1, 0) );
+        if ( !fSilent )
+            printf( "No output was asserted in %d frames.  ", Abc_MaxInt(p->iFramePrev-1, 0) );
         if ( piFrames )
         {
             if ( p->iOutputLast > 0 )
@@ -844,24 +847,27 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax
                 *piFrames = p->iFramePrev;
         }
     }
-    if ( fVerbOverwrite )
+    if ( !fSilent )
     {
-        ABC_PRTr( "Time", clock() - clk );
-    }
-    else
-    {
-        ABC_PRT( "Time", clock() - clk );
-    }
-    if ( RetValue != l_True )
-    {
-        if ( p->iFrameLast >= p->nFramesMax )
-            printf( "Reached limit on the number of timeframes (%d).\n", p->nFramesMax );
-        else if ( p->nConfMaxAll && p->pSat->stats.conflicts > p->nConfMaxAll )
-            printf( "Reached global conflict limit (%d).\n", p->nConfMaxAll );
-        else if ( nTimeOut && clock() > nTimeToStop )
-            printf( "Reached timeout (%d seconds).\n", nTimeOut );
+        if ( fVerbOverwrite )
+        {
+            ABC_PRTr( "Time", clock() - clk );
+        }
         else
-            printf( "Reached local conflict limit (%d).\n", p->nConfMaxOne );
+        {
+            ABC_PRT( "Time", clock() - clk );
+        }
+        if ( RetValue != l_True )
+        {
+            if ( p->iFrameLast >= p->nFramesMax )
+                printf( "Reached limit on the number of timeframes (%d).\n", p->nFramesMax );
+            else if ( p->nConfMaxAll && p->pSat->stats.conflicts > p->nConfMaxAll )
+                printf( "Reached global conflict limit (%d).\n", p->nConfMaxAll );
+            else if ( nTimeOut && clock() > nTimeToStop )
+                printf( "Reached timeout (%d seconds).\n", nTimeOut );
+            else
+                printf( "Reached local conflict limit (%d).\n", p->nConfMaxOne );
+        }
     }
     Saig_BmcManStop( p );
     fflush( stdout );
diff --git a/src/aig/saig/saigTempor.c b/src/aig/saig/saigTempor.c
index c8c33680..040df1f9 100644
--- a/src/aig/saig/saigTempor.c
+++ b/src/aig/saig/saigTempor.c
@@ -222,7 +222,7 @@ Aig_Man_t * Saig_ManTempor( Aig_Man_t * pAig, int nFrames, int TimeOut, int nCon
     // run BMC2
     if ( fUseBmc )
     {
-        RetValue = Saig_BmcPerform( pAig, 0, nFrames, 2000, TimeOut, nConfLimit, 0, fVerbose, 0, &nFramesFinished );
+        RetValue = Saig_BmcPerform( pAig, 0, nFrames, 2000, TimeOut, nConfLimit, 0, fVerbose, 0, &nFramesFinished, 0 );
         if ( RetValue == 0 )
         {
             Vec_IntFreeP( &vTransSigs );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index ddce0cf5..874a1057 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -358,6 +358,7 @@ static int Abc_CommandAbc9AbsRefine          ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandAbc9GlaDerive          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9GlaRefine          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9GlaPurify          ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9GlaShrink          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 //static int Abc_CommandAbc9GlaCba             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 //static int Abc_CommandAbc9GlaPba             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Gla                ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -817,6 +818,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC9",         "&gla_derive",   Abc_CommandAbc9GlaDerive,    0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&gla_refine",   Abc_CommandAbc9GlaRefine,    0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&gla_purify",   Abc_CommandAbc9GlaPurify,    0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&gla_shrink",   Abc_CommandAbc9GlaShrink,    0 );
 //    Cmd_CommandAdd( pAbc, "ABC9",         "&gla_cba",      Abc_CommandAbc9GlaCba,       0 );
 //    Cmd_CommandAdd( pAbc, "ABC9",         "&gla_pba",      Abc_CommandAbc9GlaPba,       0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&gla",          Abc_CommandAbc9Gla,          0 );
@@ -27941,6 +27943,97 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandAbc9GlaShrink( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern Gia_Man_t * Gia_IterImprove( Gia_Man_t * p, int nFrameMax, int nTimeOut, int fUsePdr, int fUseSat, int fUseBdd, int fVerbose );
+    int fUsePdr = 0;
+    int fUseSat = 1;
+    int fUseBdd = 0;
+    int nFrameMax = 0;
+    int nTimeOut = 0;
+    int c, fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "FTpsbvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'F':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nFrameMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nFrameMax < 0 ) 
+                goto usage;
+            break;
+        case 'T':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nTimeOut = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nTimeOut < 0 ) 
+                goto usage;
+            break;
+        case 'p':
+            fUsePdr ^= 1;
+            break;
+        case 's':
+            fUseSat ^= 1;
+            break;
+        case 'b':
+            fUseBdd ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9GlaShrink(): There is no AIG.\n" );
+        return 1;
+    } 
+    if ( pAbc->pGia->vGateClasses == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9GlaShrink(): There is no gate-level abstraction.\n" );
+        return 0;
+    }
+    Gia_IterImprove( pAbc->pGia, nFrameMax, nTimeOut, fUsePdr, fUseSat, fUseBdd, fVerbose );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &gla_shrink [-FT num] [-psbvh]\n" );
+    Abc_Print( -2, "\t         shrinks the abstraction by removing redundant objects\n" );
+    Abc_Print( -2, "\t-F num : the maximum timeframe to check to [default = %d]\n", nFrameMax );
+    Abc_Print( -2, "\t-T num : the timeout per call, in seconds [default = %d]\n", nTimeOut );
+    Abc_Print( -2, "\t-p     : toggle using PDR for checking [default = %s]\n", fUsePdr? "yes": "no" );
+    Abc_Print( -2, "\t-s     : toggle using BMC for checking [default = %s]\n", fUseSat? "yes": "no" );
+    Abc_Print( -2, "\t-b     : toggle using BDDs for checking [default = %s]\n", fUseBdd? "yes": "no" );
+    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;
+} 
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandAbc9GlaCba( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Saig_ParBmc_t Pars, * pPars = &Pars;
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index bea8e6b9..97385b91 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -1905,7 +1905,7 @@ ABC_PRT( "Time", clock() - clk );
     }
     else
     { 
-        RetValue = Saig_BmcPerform( pMan, nStart, nFrames, nNodeDelta, nTimeOut, nBTLimit, nBTLimitAll, fVerbose, 0, piFrames );
+        RetValue = Saig_BmcPerform( pMan, nStart, nFrames, nNodeDelta, nTimeOut, nBTLimit, nBTLimitAll, fVerbose, 0, piFrames, 0 );
         ABC_FREE( pNtk->pModel );
         ABC_FREE( pNtk->pSeqModel );
         pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
@@ -2414,7 +2414,7 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar, int nBmcFramesMax, i
 
     if ( pSecPar->fTryBmc )
     {
-        RetValue = Saig_BmcPerform( pMan, 0, nBmcFramesMax, 2000, 0, nBmcConfMax, 0, pSecPar->fVerbose, 0, &iFrame );
+        RetValue = Saig_BmcPerform( pMan, 0, nBmcFramesMax, 2000, 0, nBmcConfMax, 0, pSecPar->fVerbose, 0, &iFrame, 0 );
         if ( RetValue == 0 )
         {
             Abc_Print( 1, "Networks are not equivalent.\n" );
diff --git a/src/proof/ssw/sswRarity.c b/src/proof/ssw/sswRarity.c
index 7d12b724..d13e82ee 100644
--- a/src/proof/ssw/sswRarity.c
+++ b/src/proof/ssw/sswRarity.c
@@ -927,7 +927,7 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in
         if ( fTryBmc )
         {
             Aig_Man_t * pNewAig = Saig_ManDupWithPhase( pAig, p->vInits );
-            Saig_BmcPerform( pNewAig, 0, 100, 2000, 3, 0, 0, 1 /*fVerbose*/, 0, &iFrameFail );
+            Saig_BmcPerform( pNewAig, 0, 100, 2000, 3, 0, 0, 1 /*fVerbose*/, 0, &iFrameFail, 0 );
 //            if ( pNewAig->pSeqModel != NULL )
 //                printf( "BMC has found a counter-example in frame %d.\n", iFrameFail );
             Aig_ManStop( pNewAig );