summaryrefslogtreecommitdiffstats
path: root/src/proof
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof')
-rw-r--r--src/proof/int/intCore.c4
-rw-r--r--src/proof/pdr/pdrCore.c1
2 files changed, 3 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
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c
index 5cb05143..ca2ca5a0 100644
--- a/src/proof/pdr/pdrCore.c
+++ b/src/proof/pdr/pdrCore.c
@@ -709,6 +709,7 @@ int Pdr_ManSolve_( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t ** pvPrioInit,
p->vPrio = NULL;
}
Pdr_ManStop( p );
+ pPars->iFrame--;
return RetValue;
}