From daeffe791cb2f6690a23f4cf4d0d3101a5ac54b5 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Tue, 9 Oct 2012 15:42:25 -0700
Subject: Making report about the number of correcty covered frames consistent
 across the engines.

---
 src/proof/int/intCore.c | 4 ++--
 src/proof/pdr/pdrCore.c | 1 +
 2 files changed, 3 insertions(+), 2 deletions(-)

(limited to 'src/proof')

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;
 }
 
-- 
cgit v1.2.3