diff options
Diffstat (limited to 'src/proof/int')
| -rw-r--r-- | src/proof/int/intCore.c | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/proof/int/intCore.c b/src/proof/int/intCore.c index 7891fa69..f563eea2 100644 --- a/src/proof/int/intCore.c +++ b/src/proof/int/intCore.c @@ -97,7 +97,7 @@ int Inter_ManPerformInterpolation( Aig_Man_t * pAig, Inter_ManParams_t * pPars, if ( Inter_ManCheckInitialState(pAig) ) { - *piFrame = 0; + *piFrame = -1; printf( "Property trivially fails in the initial state.\n" ); return 0; } @@ -223,7 +223,7 @@ p->timeEqu += clock() - clk; ABC_PRT( "Time", clock() - clk ); } // remember the number of timeframes completed - pPars->iFrameMax = i + 1 + p->nFrames; + pPars->iFrameMax = i - 1 + p->nFrames; if ( RetValue == 0 ) // found a (spurious?) counter-example { if ( i == 0 ) // real counterexample |