diff options
Diffstat (limited to 'src/sat/bmc')
-rw-r--r-- | src/sat/bmc/bmcBmcG.c | 5 | ||||
-rw-r--r-- | src/sat/bmc/bmcBmcS.c | 2 |
2 files changed, 5 insertions, 2 deletions
diff --git a/src/sat/bmc/bmcBmcG.c b/src/sat/bmc/bmcBmcG.c index 3dadfb20..8fef2ef6 100644 --- a/src/sat/bmc/bmcBmcG.c +++ b/src/sat/bmc/bmcBmcG.c @@ -337,7 +337,7 @@ int Bmcg_ManPerformOne( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) if ( pCnf == NULL ) { Bmcg_ManPrintFrame( p, f, nClauses, -1, clkStart ); - if( pPars->pFuncOnFrameDone) + if( pPars->pFuncOnFrameDone ) for ( k = 0; k < pPars->nFramesAdd; k++ ) for ( i = 0; i < Gia_ManPoNum(pGia); i++ ) pPars->pFuncOnFrameDone(f+k, i, 0); @@ -372,6 +372,7 @@ int Bmcg_ManPerformOne( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) pPars->iFrame = f+k; pGia->pCexSeq = Bmcg_ManGenerateCex( p, i, f+k, 0 ); pPars->nFailOuts++; + Bmcg_ManPrintFrame( p, f+k, nClauses, -1, clkStart ); if ( !pPars->fNotVerbose ) { int nOutDigits = Abc_Base10Log( Gia_ManPoNum(pGia) ); @@ -379,7 +380,7 @@ int Bmcg_ManPerformOne( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) nOutDigits, i, f+k, nOutDigits, pPars->nFailOuts, nOutDigits, Gia_ManPoNum(pGia) ); fflush( stdout ); } - if( pPars->pFuncOnFrameDone) + if( pPars->pFuncOnFrameDone ) pPars->pFuncOnFrameDone(f+k, i, 1); } break; diff --git a/src/sat/bmc/bmcBmcS.c b/src/sat/bmc/bmcBmcS.c index 6a5c2a85..8bfda56b 100644 --- a/src/sat/bmc/bmcBmcS.c +++ b/src/sat/bmc/bmcBmcS.c @@ -682,6 +682,7 @@ int Bmcs_ManPerformOne( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) pPars->iFrame = f+k; pGia->pCexSeq = Bmcs_ManGenerateCex( p, i, f+k, 0 ); pPars->nFailOuts++; + Bmcs_ManPrintFrame( p, f+k, nClauses, -1, clkStart ); if ( !pPars->fNotVerbose ) { int nOutDigits = Abc_Base10Log( Gia_ManPoNum(pGia) ); @@ -872,6 +873,7 @@ int Bmcs_ManPerformMulti( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) pPars->iFrame = f+k; pGia->pCexSeq = Bmcs_ManGenerateCex( p, i, f+k, Solver ); pPars->nFailOuts++; + Bmcs_ManPrintFrame( p, f+k, nClauses, Solver, clkStart ); if ( !pPars->fNotVerbose ) { int nOutDigits = Abc_Base10Log( Gia_ManPoNum(pGia) ); |