Fixing gap timeout in 'pdr'.

src/proof/pdr/pdrCore.c

@@ -599,6 +599,15 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
             // try to solve this output
             while ( 1 )
             {
+                if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC )
+                {
+                    if ( p->pPars->fVerbose ) 
+                        Pdr_ManPrintProgress( p, 1, clock() - clkStart );
+                    if ( !p->pPars->fSilent )
+                        Abc_Print( 1, "Reached gap timeout (%d seconds).\n",  p->pPars->nTimeOutGap );
+                    p->pPars->iFrame = k;
+                    return p->vCexes ? 0 : -1;
+                }
                 RetValue = Pdr_ManCheckCube( p, k, NULL, &pCube, p->pPars->nConfLimit );
                 if ( RetValue == 1 )
                     break;
@@ -606,10 +615,10 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
                 {
                     if ( p->pPars->fVerbose ) 
                         Pdr_ManPrintProgress( p, 1, clock() - clkStart );
-                        if ( p->pPars->nConfLimit )
-                            Abc_Print( 1, "Reached conflict limit (%d).\n",  p->pPars->nConfLimit );
-                        else if ( p->pPars->fVerbose ) 
-                            Abc_Print( 1, "Computation cancelled by the callback.\n" );
+                    if ( p->pPars->nConfLimit )
+                        Abc_Print( 1, "Reached conflict limit (%d).\n",  p->pPars->nConfLimit );
+                    else if ( p->pPars->fVerbose ) 
+                        Abc_Print( 1, "Computation cancelled by the callback.\n" );
                     p->pPars->iFrame = k;
                     return p->vCexes ? 0 : -1;
                 }
@@ -622,6 +631,8 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
                             Pdr_ManPrintProgress( p, 1, clock() - clkStart );
                         if ( p->pPars->nConfLimit )
                             Abc_Print( 1, "Reached conflict limit (%d).\n",  p->pPars->nConfLimit );
+                        else if ( p->timeToStop && clock() > p->timeToStop )
+                            Abc_Print( 1, "Reached timeout (%d seconds).\n",  p->pPars->nTimeOut );
                         else if ( p->pPars->fVerbose ) 
                             Abc_Print( 1, "Computation cancelled by the callback.\n" );
                         p->pPars->iFrame = k;
@@ -737,7 +748,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
             if ( p->pPars->fVerbose ) 
                 Pdr_ManPrintProgress( p, 1, clock() - clkStart );
             if ( !p->pPars->fSilent )
-                Abc_Print( 1, "Reached gap timeout (%d seconds).\n",  p->pPars->nTimeOut );
+                Abc_Print( 1, "Reached gap timeout (%d seconds).\n",  p->pPars->nTimeOutGap );
             p->pPars->iFrame = k;
             return p->vCexes ? 0 : -1;
         }