summaryrefslogtreecommitdiffstats
path: root/src/sat/bmc/bmcBmcG.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/sat/bmc/bmcBmcG.c')
-rw-r--r--src/sat/bmc/bmcBmcG.c5
1 files changed, 3 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;