diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-06-28 10:42:31 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-06-28 10:42:31 -0700 |
| commit | 184c5d4ea467731005c92bc159c68d57c83c6c6a (patch) | |
| tree | ec585fa6f993ed00851000069887812a4734d678 /src/proof/int | |
| parent | e93cfb18ee42e75e6d55c4fd02e5455c4ec16cc8 (diff) | |
| download | abc-184c5d4ea467731005c92bc159c68d57c83c6c6a.tar.gz abc-184c5d4ea467731005c92bc159c68d57c83c6c6a.tar.bz2 abc-184c5d4ea467731005c92bc159c68d57c83c6c6a.zip | |
Adding timeout to the interpolant computation procedure.
Diffstat (limited to 'src/proof/int')
| -rw-r--r-- | src/proof/int/intM114.c | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/proof/int/intM114.c b/src/proof/int/intM114.c index 64b18ae0..e5da012a 100644 --- a/src/proof/int/intM114.c +++ b/src/proof/int/intM114.c @@ -304,11 +304,13 @@ clk = Abc_Clock(); */ pManInterA = Inta_ManAlloc(); - p->pInterNew = (Aig_Man_t *)Inta_ManInterpolate( pManInterA, (Sto_Man_t *)pSatCnf, p->vVarsAB, 0 ); + p->pInterNew = (Aig_Man_t *)Inta_ManInterpolate( pManInterA, (Sto_Man_t *)pSatCnf, nTimeNewOut, p->vVarsAB, 0 ); Inta_ManFree( pManInterA ); p->timeInt += Abc_Clock() - clk; Sto_ManFree( (Sto_Man_t *)pSatCnf ); + if ( p->pInterNew == NULL ) + RetValue = -1; return RetValue; } |