diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-09-09 20:46:34 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-09-09 20:46:34 -0700 |
| commit | d40af538e2b7dc644fa427c37965a9721b64b12d (patch) | |
| tree | c8e0c6851bea42bc05f0f39743f6a823afb3fe74 /src/aig/saig | |
| parent | 71d7c9e66df28f0916e21b5d0e9daaa83fd6eedc (diff) | |
| download | abc-d40af538e2b7dc644fa427c37965a9721b64b12d.tar.gz abc-d40af538e2b7dc644fa427c37965a9721b64b12d.tar.bz2 abc-d40af538e2b7dc644fa427c37965a9721b64b12d.zip | |
Unified print-out of property failures produced by all engines.
Diffstat (limited to 'src/aig/saig')
| -rw-r--r-- | src/aig/saig/saigAbs.c | 4 | ||||
| -rw-r--r-- | src/aig/saig/saigBmc2.c | 6 | ||||
| -rw-r--r-- | src/aig/saig/saigBmc3.c | 4 |
3 files changed, 7 insertions, 7 deletions
diff --git a/src/aig/saig/saigAbs.c b/src/aig/saig/saigAbs.c index ffb17db8..f30963a8 100644 --- a/src/aig/saig/saigAbs.c +++ b/src/aig/saig/saigAbs.c @@ -118,8 +118,8 @@ Abc_Cex_t * Saig_ManCexRemap( Aig_Man_t * p, Aig_Man_t * pAbs, Abc_Cex_t * pCexA } else { - printf( "Counter-example verification is successful.\n" ); - printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). \n", pCex->iPo, pCex->iFrame ); + Abc_Print( 1, "Counter-example verification is successful.\n" ); + Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. \n", pCex->iPo, p->pName, pCex->iFrame ); } return pCex; } diff --git a/src/aig/saig/saigBmc2.c b/src/aig/saig/saigBmc2.c index f70a0015..ed15c635 100644 --- a/src/aig/saig/saigBmc2.c +++ b/src/aig/saig/saigBmc2.c @@ -829,8 +829,8 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax { assert( p->iFrameFail * Saig_ManPoNum(p->pAig) + p->iOutputFail + 1 == nOutsSolved ); if ( !fSilent ) - printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", - p->iOutputFail, p->iFrameFail ); + Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", + p->iOutputFail, p->pAig->pName, p->iFrameFail ); Status = 0; if ( piFrames ) *piFrames = p->iFrameFail; @@ -838,7 +838,7 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax else // if ( RetValue == l_False || RetValue == l_Undef ) { if ( !fSilent ) - printf( "No output was asserted in %d frames. ", Abc_MaxInt(p->iFramePrev-1, 0) ); + Abc_Print( 1, "No output failed in %d frames. ", Abc_MaxInt(p->iFramePrev-1, 0) ); if ( piFrames ) { if ( p->iOutputLast > 0 ) diff --git a/src/aig/saig/saigBmc3.c b/src/aig/saig/saigBmc3.c index bb59f677..75014158 100644 --- a/src/aig/saig/saigBmc3.c +++ b/src/aig/saig/saigBmc3.c @@ -1413,7 +1413,7 @@ clkOther += clock() - clk2; return 0; } pPars->nFailOuts++; - printf( "Output %*d was asserted in frame %2d (solved %*d out of %*d outputs).\n", + Abc_Print( 1, "Output %*d was asserted in frame %2d (solved %*d out of %*d outputs).\n", nOutDigits, i, f, nOutDigits, pPars->nFailOuts, nOutDigits, Saig_ManPoNum(pAig) ); if ( p->vCexes == NULL ) p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) ); @@ -1486,7 +1486,7 @@ clkOther += clock() - clk2; return 0; } pPars->nFailOuts++; - printf( "Output %*d was asserted in frame %2d (solved %*d out of %*d outputs).\n", + Abc_Print( 1, "Output %*d was asserted in frame %2d (solved %*d out of %*d outputs).\n", nOutDigits, i, f, nOutDigits, pPars->nFailOuts, nOutDigits, Saig_ManPoNum(pAig) ); if ( p->vCexes == NULL ) p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) ); |