diff options
Diffstat (limited to 'src/proof')
-rw-r--r-- | src/proof/bbr/bbrReach.c | 4 | ||||
-rw-r--r-- | src/proof/llb/llb1Reach.c | 4 | ||||
-rw-r--r-- | src/proof/llb/llb2Core.c | 4 | ||||
-rw-r--r-- | src/proof/llb/llb3Nonlin.c | 4 | ||||
-rw-r--r-- | src/proof/llb/llb4Nonlin.c | 2 | ||||
-rw-r--r-- | src/proof/ssw/sswRarity.c | 4 |
6 files changed, 11 insertions, 11 deletions
diff --git a/src/proof/bbr/bbrReach.c b/src/proof/bbr/bbrReach.c index 19d87bc2..13f4f558 100644 --- a/src/proof/bbr/bbrReach.c +++ b/src/proof/bbr/bbrReach.c @@ -336,7 +336,7 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D vOnionRings, bIntersect, i, pPars->fVerbose, pPars->fSilent ); Cudd_RecursiveDeref( dd, bIntersect ); if ( !pPars->fSilent ) - printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", i, Vec_PtrSize(vOnionRings) ); + Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", i, p->pName, Vec_PtrSize(vOnionRings) ); Cudd_RecursiveDeref( dd, bReached ); bReached = NULL; pPars->iFrame = nIters; @@ -488,7 +488,7 @@ int Aig_ManVerifyUsingBdds_int( Aig_Man_t * p, Saig_ParBbr_t * pPars ) vOnionRings, bIntersect, i, pPars->fVerbose, pPars->fSilent ); Cudd_RecursiveDeref( dd, bIntersect ); if ( !pPars->fSilent ) - printf( "The miter output %d is proved REACHABLE in the initial state (use \"write_counter\" to dump a witness). ", i ); + Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", i, p->pName, -1 ); RetValue = 0; break; } diff --git a/src/proof/llb/llb1Reach.c b/src/proof/llb/llb1Reach.c index fed0389a..b7d79994 100644 --- a/src/proof/llb/llb1Reach.c +++ b/src/proof/llb/llb1Reach.c @@ -699,9 +699,9 @@ int Llb_ManReachability( Llb_Man_t * p, Vec_Int_t * vHints, DdManager ** pddGlo if ( !p->pPars->fSilent ) { if ( !p->pPars->fBackward ) - printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", p->pAigGlo->pSeqModel->iPo, nIters ); + Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", p->pAigGlo->pSeqModel->iPo, p->pAigGlo->pName, p->pAigGlo->pName, nIters ); else - printf( "Output ??? was asserted in frame %d (counter-example is not produced). ", nIters ); + Abc_Print( 1, "Output ??? of miter \"%s\" was asserted in frame %d (counter-example is not produced). ", p->pAigGlo->pName, nIters ); Abc_PrintTime( 1, "Time", clock() - clk ); } p->pPars->iFrame = nIters - 1; diff --git a/src/proof/llb/llb2Core.c b/src/proof/llb/llb2Core.c index f19f757e..a6f16aeb 100644 --- a/src/proof/llb/llb2Core.c +++ b/src/proof/llb/llb2Core.c @@ -323,9 +323,9 @@ int Llb_CoreReachability_int( Llb_Img_t * p, Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQ if ( !p->pPars->fSilent ) { if ( !p->pPars->fBackward ) - printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", p->pInit->pSeqModel->iPo, nIters ); + Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", p->pInit->pSeqModel->iPo, p->pInit->pName, nIters ); else - printf( "Output ??? was asserted in frame %d (counter-example is not produced). ", nIters ); + Abc_Print( 1, "Output ??? was asserted in frame %d (counter-example is not produced). ", nIters ); Abc_PrintTime( 1, "Time", clock() - clk ); } p->pPars->iFrame = nIters - 1; diff --git a/src/proof/llb/llb3Nonlin.c b/src/proof/llb/llb3Nonlin.c index 8badc61d..22e23337 100644 --- a/src/proof/llb/llb3Nonlin.c +++ b/src/proof/llb/llb3Nonlin.c @@ -504,9 +504,9 @@ int Llb_NonlinReachability( Llb_Mnn_t * p ) if ( !p->pPars->fSilent ) { if ( !p->pPars->fBackward ) - printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", p->pInit->pSeqModel->iPo, nIters ); + Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", p->pInit->pSeqModel->iPo, nIters ); else - printf( "Output ??? was asserted in frame %d (counter-example is not produced). ", nIters ); + Abc_Print( 1, "Output ??? was asserted in frame %d (counter-example is not produced). ", nIters ); Abc_PrintTime( 1, "Time", clock() - clk ); } p->pPars->iFrame = nIters - 1; diff --git a/src/proof/llb/llb4Nonlin.c b/src/proof/llb/llb4Nonlin.c index f2973922..51f9d602 100644 --- a/src/proof/llb/llb4Nonlin.c +++ b/src/proof/llb/llb4Nonlin.c @@ -759,7 +759,7 @@ int Llb_Nonlin4Reachability( Llb_Mnx_t * p ) Vec_PtrFreeP( &vStates ); if ( !p->pPars->fSilent ) { - printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", p->pAig->pSeqModel->iPo, nIters ); + Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", p->pAig->pSeqModel->iPo, p->pAig->pName, nIters ); Abc_PrintTime( 1, "Time", clock() - clk ); } p->pPars->iFrame = nIters - 1; diff --git a/src/proof/ssw/sswRarity.c b/src/proof/ssw/sswRarity.c index d13e82ee..73a65d88 100644 --- a/src/proof/ssw/sswRarity.c +++ b/src/proof/ssw/sswRarity.c @@ -946,7 +946,7 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in printf( "Simulated %d frames for %d rounds with %d restarts.\n", nFrames, nNumRestart * nRestart + r, nNumRestart ); pAig->pSeqModel = Ssw_RarDeriveCex( p, r * p->nFrames + f, p->iFailPo, p->iFailPat, fVerbose ); // print final report - printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", pAig->pSeqModel->iPo, pAig->pSeqModel->iFrame ); + Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", pAig->pSeqModel->iPo, pAig->pName, pAig->pSeqModel->iFrame ); Abc_PrintTime( 1, "Time", clock() - clkTotal ); RetValue = 0; goto finish; @@ -1106,7 +1106,7 @@ int Ssw_RarSignalFilter( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize Abc_CexFree( pAig->pSeqModel ); pAig->pSeqModel = Ssw_RarDeriveCex( p, r * p->nFrames + f, p->iFailPo, p->iFailPat, 1 ); // print final report - printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", pAig->pSeqModel->iPo, pAig->pSeqModel->iFrame ); + Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", pAig->pSeqModel->iPo, pAig->pName, pAig->pSeqModel->iFrame ); Abc_PrintTime( 1, "Time", clock() - clkTotal ); RetValue = 0; goto finish; |