luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Fix mismatch in output formatting.

This commit is contained in:
Alan Mishchenko 2017-01-21 12:48:40 +08:00
parent a28be94ac7
commit cf539dcca4
5 changed files with 16 additions and 16 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
src/aig/saig/saigMiter.c
View File

@ -1111,12 +1111,12 @@ int Ssw_SecSpecial( Aig_Man_t * pPart0, Aig_Man_t * pPart1, int nFrames, int fVe
// report the miter
if ( RetValue == 1 )
{
printf( "Networks are equivalent. " );
printf( "Networks are equivalent. " );
ABC_PRT( "Time", Abc_Clock() - clkTotal );
}
else if ( RetValue == 0 )
{
printf( "Networks are NOT EQUIVALENT. " );
printf( "Networks are NOT EQUIVALENT. " );
ABC_PRT( "Time", Abc_Clock() - clkTotal );
if ( pMiterCec->pData == NULL )
printf( "Counter-example is not available.\n" );

12
src/base/abci/abcDar.c
View File

@ -1946,17 +1946,17 @@ finish:
// report the miter
if ( RetValue == 1 )
{
Abc_Print( 1, "Networks are equivalent. " );
Abc_Print( 1, "Networks are equivalent. " );
ABC_PRT( "Time", Abc_Clock() - clkTotal );
}
else if ( RetValue == 0 )
{
Abc_Print( 1, "Networks are NOT EQUIVALENT. " );
Abc_Print( 1, "Networks are NOT EQUIVALENT. " );
ABC_PRT( "Time", Abc_Clock() - clkTotal );
}
else
{
Abc_Print( 1, "Networks are UNDECIDED. " );
Abc_Print( 1, "Networks are UNDECIDED. " );
ABC_PRT( "Time", Abc_Clock() - clkTotal );
}
fflush( stdout );
@ -3695,17 +3695,17 @@ int Abc_NtkDarInduction( Abc_Ntk_t * pNtk, int nTimeOut, int nFramesMax, int nCo
RetValue = Saig_ManInduction( pMan, nTimeOut, nFramesMax, nConfMax, fUnique, fUniqueAll, fGetCex, fVerbose, fVeryVerbose );
if ( RetValue == 1 )
{
Abc_Print( 1, "Networks are equivalent. " );
Abc_Print( 1, "Networks are equivalent. " );
ABC_PRT( "Time", Abc_Clock() - clkTotal );
}
else if ( RetValue == 0 )
{
Abc_Print( 1, "Networks are NOT EQUIVALENT. " );
Abc_Print( 1, "Networks are NOT EQUIVALENT. " );
ABC_PRT( "Time", Abc_Clock() - clkTotal );
}
else
{
Abc_Print( 1, "Networks are UNDECIDED. " );
Abc_Print( 1, "Networks are UNDECIDED. " );
ABC_PRT( "Time", Abc_Clock() - clkTotal );
}
if ( fGetCex )

6
src/proof/cec/cecCec.c
View File

@ -85,7 +85,7 @@ int Cec_ManVerifyOld( Gia_Man_t * pMiter, int fVerbose, int * piOutFail, abctime
{
if ( !fSilent )
{
Abc_Print( 1, "Networks are equivalent. " );
Abc_Print( 1, "Networks are equivalent. " );
Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
}
}
@ -93,7 +93,7 @@ int Cec_ManVerifyOld( Gia_Man_t * pMiter, int fVerbose, int * piOutFail, abctime
{
if ( !fSilent )
{
Abc_Print( 1, "Networks are NOT EQUIVALENT. " );
Abc_Print( 1, "Networks are NOT EQUIVALENT. " );
Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
}
if ( pMiterCec->pData == NULL )
@ -120,7 +120,7 @@ int Cec_ManVerifyOld( Gia_Man_t * pMiter, int fVerbose, int * piOutFail, abctime
}
else if ( !fSilent )
{
Abc_Print( 1, "Networks are UNDECIDED. " );
Abc_Print( 1, "Networks are UNDECIDED. " );
Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
}
fflush( stdout );

6
src/proof/fra/fraCec.c
View File

@ -547,17 +547,17 @@ int Fra_FraigCecTop( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int n
// report the miter
if ( RetValue == 1 )
{
printf( "Networks are equivalent. " );
printf( "Networks are equivalent. " );
ABC_PRT( "Time", Abc_Clock() - clkTotal );
}
else if ( RetValue == 0 )
{
printf( "Networks are NOT EQUIVALENT. " );
printf( "Networks are NOT EQUIVALENT. " );
ABC_PRT( "Time", Abc_Clock() - clkTotal );
}
else
{
printf( "Networks are UNDECIDED. " );
printf( "Networks are UNDECIDED. " );
ABC_PRT( "Time", Abc_Clock() - clkTotal );
}
fflush( stdout );

4
src/proof/fra/fraSec.c
View File

@ -606,7 +606,7 @@ finish:
{
if ( !pParSec->fSilent )
{
printf( "Networks are equivalent. " );
printf( "Networks are equivalent. " );
ABC_PRT( "Time", Abc_Clock() - clkTotal );
}
if ( pParSec->fReportSolution && !pParSec->fRecursive )
@ -630,7 +630,7 @@ ABC_PRT( "Time", Abc_Clock() - clkTotal );
}
if ( !pParSec->fSilent )
{
printf( "Networks are NOT EQUIVALENT. " );
printf( "Networks are NOT EQUIVALENT. " );
ABC_PRT( "Time", Abc_Clock() - clkTotal );
}
if ( pParSec->fReportSolution && !pParSec->fRecursive )