Updating printouts.

schnrj · Oct 23, 2023 · 538ecb4 · 538ecb4
1 parent 01ad71b
commit 538ecb4
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 5 deletions.
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c
@@ -1149,7 +1149,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
                 {
                     if ( p->pPars->fVerbose )
                         Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
-                    if ( p->timeToStop && Abc_Clock() > p->timeToStop )
+                    if ( p->timeToStop && Abc_Clock() > p->timeToStop && !p->pPars->fSilent )
                         Abc_Print( 1, "Reached timeout (%d seconds) in frame %d.\n",  p->pPars->nTimeOut, iFrame );
                     else if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && Abc_Clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC )
                         Abc_Print( 1, "Reached gap timeout (%d seconds) in frame %d.\n",  p->pPars->nTimeOutGap, iFrame );
@@ -1173,7 +1173,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
                     {
                         if ( p->pPars->fVerbose )
                             Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
-                        if ( p->timeToStop && Abc_Clock() > p->timeToStop )
+                        if ( p->timeToStop && Abc_Clock() > p->timeToStop && !p->pPars->fSilent )
                             Abc_Print( 1, "Reached timeout (%d seconds) in frame %d.\n",  p->pPars->nTimeOut, iFrame );
                         else if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && Abc_Clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC )
                             Abc_Print( 1, "Reached gap timeout (%d seconds) in frame %d.\n",  p->pPars->nTimeOutGap, iFrame );

diff --git a/src/sat/bmc/bmcBmcG.c b/src/sat/bmc/bmcBmcG.c
@@ -421,9 +421,11 @@ int Bmcg_ManPerformOne( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
             break;
     }
     p->timeOth = Abc_Clock() - clkStart - p->timeUnf - p->timeCnf - p->timeSmp - p->timeSat;
-    if ( RetValue == -1 && !pPars->fNotVerbose )
-        printf( "No output failed in %d frames.  ", f + (k < pPars->nFramesAdd ? k+1 : 0) );
-    Abc_PrintTime( 1, "Time", Abc_Clock() - clkStart );
+    if ( !pPars->fNotVerbose ) {
+        if ( RetValue == -1 && !pPars->fNotVerbose )
+            printf( "No output failed in %d frames.  ", f + (k < pPars->nFramesAdd ? k+1 : 0) );
+        Abc_PrintTime( 1, "Time", Abc_Clock() - clkStart );
+    }
     Bmcg_ManPrintTime( p );
     Bmcg_ManStop( p );
     return RetValue;