summaryrefslogtreecommitdiffstats
path: root/src/proof/int/intCore.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof/int/intCore.c')
-rw-r--r--src/proof/int/intCore.c12
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;