Unified print-out of property failures produced by all engines.

14 files changed, 28 insertions, 29 deletions

diff --git a/src/aig/gia/giaAbsOut.c b/src/aig/gia/giaAbsOut.c
index f7204307..0b303355 100644
--- a/src/aig/gia/giaAbsOut.c
+++ b/src/aig/gia/giaAbsOut.c
@@ -73,7 +73,7 @@ Abc_Cex_t * Gia_ManCexRemap( Gia_Man_t * p, Abc_Cex_t * pCexAbs, Vec_Int_t * vPi
     else
     {
         Abc_Print( 1, "Counter-example verification is successful.\n" );
-        Abc_Print( 1, "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). \n", pCex->iPo, pCex->iFrame );
+        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/gia/giaEra2.c b/src/aig/gia/giaEra2.c
index b0823ee8..060c83a5 100644
--- a/src/aig/gia/giaEra2.c
+++ b/src/aig/gia/giaEra2.c
@@ -1736,9 +1736,8 @@ int Gia_ManArePerform( Gia_Man_t * pAig, int nStatesMax, int fMiter, int fVerbos
         Gia_ManAreDepth(p, p->iStaCur-1) );
     ABC_PRT( "Time", clock() - clk );
     if ( pAig->pCexSeq != NULL )
-//        printf( "Miter FAILED in state %d at frame %d (use \"&write_counter\" to dump a witness)\n", 
-        printf( "Miter FAILED in state %d at frame %d (the cex is available for refinement)\n", 
-            p->iStaCur, Gia_ManAreDepth(p, p->iStaCur)-1 );
+        Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d.\n", 
+            p->iStaCur, pAig->pName, Gia_ManAreDepth(p, p->iStaCur)-1 );
     if ( fVerbose )
     {
         ABC_PRTP( "Cofactoring", p->timeAig - p->timeCube,    clock() - clk );
diff --git a/src/aig/gia/giaSim.c b/src/aig/gia/giaSim.c
index 8d22e699..da6ac33e 100644
--- a/src/aig/gia/giaSim.c
+++ b/src/aig/gia/giaSim.c
@@ -631,7 +631,7 @@ int Gia_ManSimSimulate( Gia_Man_t * pAig, Gia_ParSim_t * pPars )
             Gia_ManResetRandom( pPars );
             pPars->iOutFail = iOut;
             pAig->pCexSeq = Gia_ManGenerateCounter( pAig, i, iOut, p->nWords, iPat, p->vCis2Ids );
-            Abc_Print( 1, "Networks are NOT EQUIVALENT.   Output %d was asserted in frame %d.  ", iOut, i );
+            Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d.  ", iOut, pAig->pName, i );
             if ( !Gia_ManVerifyCex( pAig, pAig->pCexSeq, 0 ) )
             {
 //                Abc_Print( 1, "\n" );
diff --git a/src/aig/gia/giaSim2.c b/src/aig/gia/giaSim2.c
index 897eff98..85428769 100644
--- a/src/aig/gia/giaSim2.c
+++ b/src/aig/gia/giaSim2.c
@@ -663,7 +663,7 @@ int Gia_ManSimSimulateEquiv( Gia_Man_t * pAig, Gia_ParSim_t * pPars )
             Gia_ManResetRandom( pPars );
             pPars->iOutFail = iOut;
             pAig->pCexSeq = Gia_Sim2GenerateCounter( pAig, i, iOut, p->nWords, iPat );
-            Abc_Print( 1, "Networks are NOT EQUIVALENT.   Output %d was asserted in frame %d.  ", iOut, i );
+            Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d.  ", iOut, pAig->pName, i );
             if ( !Gia_ManVerifyCex( pAig, pAig->pCexSeq, 0 ) )
             {
 //                Abc_Print( 1, "\n" );
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) );
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 97385b91..85377956 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -1899,7 +1899,7 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nStart, int nFrames, int nSizeMax, int
         else // if ( RetValue == 0 )
         {
             Abc_Cex_t * pCex = pNtk->pSeqModel;
-            Abc_Print( 1, "Output %d asserted in frame %d (use \"write_counter\" to dump a witness). ", pCex->iPo, pCex->iFrame );
+            Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", pCex->iPo, pNtk->pName, pCex->iFrame );
         }
 ABC_PRT( "Time", clock() - clk );
     }
@@ -1988,7 +1988,7 @@ int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars, int fOrDecomp )
         if ( !pPars->fSolveAll )
         {
             Abc_Cex_t * pCex = pNtk->pSeqModel;
-            Abc_Print( 1, "Output %d asserted in frame %d (use \"write_counter\" to dump a witness). ", pCex->iPo, pCex->iFrame );
+            Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", pCex->iPo, pNtk->pName, pCex->iFrame );
         }
         else
         {
@@ -2120,7 +2120,7 @@ int Abc_NtkDarBmcInter_int( Aig_Man_t * pMan, Inter_ManParams_t * pPars, Aig_Man
     if ( RetValue == 1 )
         Abc_Print( 1, "Property proved.  " );
     else if ( RetValue == 0 )
-        Abc_Print( 1, "Property DISPROVED in frame %d (use \"write_counter\" to dump a witness).  ", iFrame );
+        Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d.  ", pMan->pSeqModel ? pMan->pSeqModel->iPo : -1, pMan->pName, iFrame );
     else if ( RetValue == -1 )
         Abc_Print( 1, "Property UNDECIDED.  " );
     else
@@ -2445,7 +2445,7 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, Fra_Sec_t * pSecPar, int nBmcFramesMax, i
         if ( pNtk->pSeqModel )
         {
             Abc_Cex_t * pCex = pNtk->pSeqModel;
-            Abc_Print( 1, "Output %d asserted in frame %d (use \"write_counter\" to dump a witness).\n", pCex->iPo, pCex->iFrame );
+            Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d.\n", pCex->iPo, pNtk->pName, pCex->iFrame );
             if ( !Saig_ManVerifyCex( pMan, pNtk->pSeqModel ) )
                 Abc_Print( 1, "Abc_NtkDarProve(): Counter-example verification has FAILED.\n" );
         }
@@ -2580,7 +2580,7 @@ int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex )
     if ( RetValue == 1 )
         Abc_Print( 1, "Property proved.  " );
     else if ( RetValue == 0 )
-        Abc_Print( 1, "Property DISPROVED in frame %d (use \"write_counter\" to dump a witness).  ", ppCex? (*ppCex)->iFrame : -1 );
+        Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d.  ", (*ppCex)->iPo, pNtk->pName, ppCex? (*ppCex)->iFrame : -1 );
     else if ( RetValue == -1 )
         Abc_Print( 1, "Property UNDECIDED.  " );
     else
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;