Adding timeout to AIG rewriting inside 'int'.

1 files changed, 12 insertions, 0 deletions

diff --git a/src/proof/int/intCore.c b/src/proof/int/intCore.c
index dedf987e..1418402c 100644
--- a/src/proof/int/intCore.c
+++ b/src/proof/int/intCore.c
@@ -280,10 +280,22 @@ p->timeEqu += Abc_Clock() - clk;
 clk = Abc_Clock();
             if ( p->pInterNew )
             {
+                Abc_PrintTime( 1, "Before time", clock() - clkTotal );
+                // save the timeout value
+                p->pInterNew->Time2Quit = nTimeNewOut;
 //                Ioa_WriteAiger( p->pInterNew, "interpol.aig", 0, 0 );
                 p->pInterNew = Dar_ManRwsat( pAigTemp = p->pInterNew, 1, 0 );
 //                p->pInterNew = Dar_ManRwsat( pAigTemp = p->pInterNew, 0, 0 );
+                Abc_PrintTime( 1, "After time", clock() - clkTotal );
                 Aig_ManStop( pAigTemp );
+                if ( p->pInterNew == NULL )
+                {
+                    printf( "Reached timeout (%d seconds) during rewriting.\n",  pPars->nSecLimit );
+                    p->timeTotal = Abc_Clock() - clkTotal;
+                    Inter_ManStop( p, 1 );
+                    Inter_CheckStop( pCheck );
+                    return -1;
+                }
             }
 p->timeRwr += Abc_Clock() - clk;