From 81b51657f5c502e45418630614fd56e5e1506230 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 13 Mar 2009 08:01:00 -0700 Subject: Version abc90313 --- src/aig/ssw/sswCore.c | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) (limited to 'src/aig/ssw/sswCore.c') diff --git a/src/aig/ssw/sswCore.c b/src/aig/ssw/sswCore.c index 9d09d4e7..03df38e1 100644 --- a/src/aig/ssw/sswCore.c +++ b/src/aig/ssw/sswCore.c @@ -146,6 +146,18 @@ Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p ) nSatProof = nSatCallsSat = nRecycles = nSatFailsReal = nUniques = 0; for ( nIter = 0; ; nIter++ ) { + if ( p->pPars->nItersStop >= 0 && p->pPars->nItersStop == nIter ) + { + Aig_Man_t * pSRed = Ssw_SpeculativeReduction( p ); + Aig_ManDumpBlif( pSRed, "srm.blif", NULL, NULL ); + Aig_ManStop( pSRed ); + printf( "Iterative refinement is stopped before iteration %d.\n", nIter ); + printf( "The network is reduced using candidate equivalences.\n" ); + printf( "Speculatively reduced miter is saved in file \"%s\".\n", "srm.blif" ); + printf( "If the miter is SAT, the reduced result is incorrect.\n" ); + break; + } + clk = clock(); p->pMSat = Ssw_SatStart( 0 ); if ( p->pPars->fLatchCorrOpt ) @@ -199,18 +211,6 @@ clk = clock(); Ssw_ManCleanup( p ); if ( !RetValue ) break; - - if ( p->pPars->nItersStop >= 0 && p->pPars->nItersStop == nIter ) - { - Aig_Man_t * pSRed = Ssw_SpeculativeReduction( p ); - Aig_ManDumpBlif( pSRed, "srm.blif", NULL, NULL ); - Aig_ManStop( pSRed ); - printf( "Iterative refinement is stopped after iteration %d.\n", nIter ); - printf( "The network is reduced using candidate equivalences.\n" ); - printf( "Speculatively reduced miter is saved in file \"%s\".\n", "srm.blif" ); - printf( "If the miter is SAT, the reduced result is incorrect.\n" ); - break; - } } p->pPars->nIters = nIter + 1; p->timeTotal = clock() - clkTotal; -- cgit v1.2.3