diff options
Diffstat (limited to 'src/proof')
| -rw-r--r-- | src/proof/pdr/pdrInv.c | 4 | ||||
| -rw-r--r-- | src/proof/ssw/sswRarity.c | 5 |
2 files changed, 6 insertions, 3 deletions
diff --git a/src/proof/pdr/pdrInv.c b/src/proof/pdr/pdrInv.c index c4a85875..f9b4a55d 100644 --- a/src/proof/pdr/pdrInv.c +++ b/src/proof/pdr/pdrInv.c @@ -50,6 +50,8 @@ void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, clock_t Time ) int i, ThisSize, Length, LengthStart; if ( Vec_PtrSize(p->vSolvers) < 2 ) return; + if ( Abc_FrameIsBatchMode() && !fClose ) + return; // count the total length of the printout Length = 0; Vec_VecForEachLevel( p->vClauses, vVec, i ) @@ -78,7 +80,7 @@ void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, clock_t Time ) for ( i = ThisSize; i < 70; i++ ) Abc_Print( 1, " " ); Abc_Print( 1, "%6d", p->nQueMax ); - Abc_Print( 1, " %8.2f sec", (float)(Time)/(float)(CLOCKS_PER_SEC) ); + Abc_Print( 1, "%10.2f sec", 1.0*Time/CLOCKS_PER_SEC ); Abc_Print( 1, "%s", fClose ? "\n":"\r" ); if ( fClose ) p->nQueMax = 0; diff --git a/src/proof/ssw/sswRarity.c b/src/proof/ssw/sswRarity.c index 445dda84..032bc5ba 100644 --- a/src/proof/ssw/sswRarity.c +++ b/src/proof/ssw/sswRarity.c @@ -20,6 +20,7 @@ #include "sswInt.h" #include "src/aig/gia/giaAig.h" +#include "src/base/main/main.h" ABC_NAMESPACE_IMPL_START @@ -1074,7 +1075,7 @@ int Ssw_RarSignalFilter( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize if ( fMiter && Ssw_RarManCheckNonConstOutputs(p) ) { if ( !fVerbose ) - printf( "\r" ); + printf( "%s", Abc_FrameIsBatchMode() ? "\n" : "\r" ); // printf( "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames ); Ssw_RarManPrepareRandom( nRandSeed ); Abc_CexFree( pAig->pSeqModel ); @@ -1108,7 +1109,7 @@ finish: if ( r == nRounds && f == nFrames ) { if ( !fVerbose ) - printf( "\r" ); + printf( "%s", Abc_FrameIsBatchMode() ? "\n" : "\r" ); printf( "Simulation did not assert POs in the first %d frames. ", nRounds * nFrames ); Abc_PrintTime( 1, "Time", clock() - clkTotal ); } |