diff options
Diffstat (limited to 'src/sat/bmc/bmcBmcS.c')
| -rw-r--r-- | src/sat/bmc/bmcBmcS.c | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/sat/bmc/bmcBmcS.c b/src/sat/bmc/bmcBmcS.c index d6452340..e22796d3 100644 --- a/src/sat/bmc/bmcBmcS.c +++ b/src/sat/bmc/bmcBmcS.c @@ -551,6 +551,9 @@ int Bmcs_ManPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) if ( pCnf == NULL ) { Bmcs_ManPrintFrame( p, f, nClauses, clkStart ); + if( pPars->pFuncOnFrameDone) + for ( i = 0; i < Gia_ManPoNum(pGia); i++ ) + pPars->pFuncOnFrameDone(f, i, 0); continue; } nClauses += pCnf->nClauses; @@ -571,6 +574,8 @@ int Bmcs_ManPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) if ( status == SATOKO_UNSAT ) { Bmcs_ManPrintFrame( p, f, nClauses, clkStart ); + if( pPars->pFuncOnFrameDone) + pPars->pFuncOnFrameDone(f, i, 0); continue; } if ( status == SATOKO_SAT ) @@ -586,6 +591,8 @@ int Bmcs_ManPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) fflush( stdout ); pGia->pCexSeq = Bmcs_ManGenerateCex( p, i, f ); } + if( pPars->pFuncOnFrameDone) + pPars->pFuncOnFrameDone(f, i, 1); } break; } |