diff options
Diffstat (limited to 'src/aig/saig')
-rw-r--r-- | src/aig/saig/saigBmc.c | 2 | ||||
-rw-r--r-- | src/aig/saig/saigInter.c | 5 |
2 files changed, 4 insertions, 3 deletions
diff --git a/src/aig/saig/saigBmc.c b/src/aig/saig/saigBmc.c index f6a42c8b..952094ce 100644 --- a/src/aig/saig/saigBmc.c +++ b/src/aig/saig/saigBmc.c @@ -182,7 +182,6 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim Aig_Man_t * pFrames, * pAigTemp; Aig_Obj_t * pObj; int status, clk, Lit, i, RetValue = 1; - *piFrame = -1; // derive the timeframes clk = clock(); if ( nSizeMax > 0 ) @@ -192,6 +191,7 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim } else pFrames = Saig_ManFramesBmc( pAig, nFrames ); + *piFrame = nFrames; if ( fVerbose ) { printf( "AIG: PI/PO/Reg = %d/%d/%d. Node = %6d. Lev = %5d.\n", diff --git a/src/aig/saig/saigInter.c b/src/aig/saig/saigInter.c index 3adcc568..889e6298 100644 --- a/src/aig/saig/saigInter.c +++ b/src/aig/saig/saigInter.c @@ -178,6 +178,7 @@ Aig_Man_t * Saig_ManTransformed( Aig_Man_t * p ) Saig_ManForEachLiLo( p, pObjLi, pObjLo, i ) { pObj = Aig_Mux( pNew, pCtrl, pObjLo->pData, Aig_ObjChild0Copy(pObjLi) ); +// pObj = Aig_Mux( pNew, pCtrl, Aig_ManConst0(pNew), Aig_ObjChild0Copy(pObjLi) ); Aig_ObjCreatePo( pNew, pObj ); } Aig_ManCleanup( pNew ); @@ -566,10 +567,10 @@ p->timeCnf += clock() - clk; // iterate the interpolation procedure for ( i = 0; ; i++ ) { - if ( p->nFrames + i >= 100 ) + if ( p->nFrames + i >= 75 ) { if ( fVerbose ) - printf( "Reached limit (%d) on the number of timeframes.\n", 100 ); + printf( "Reached limit (%d) on the number of timeframes.\n", 75 ); p->timeTotal = clock() - clkTotal; Saig_ManagerFree( p ); return -1; |