4 files changed, 71 insertions, 7 deletions

diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index a0216f37..e614d58f 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -154,7 +154,7 @@ struct Aig_Man_t_
     Vec_Int_t *      vFlopNums;      
     Vec_Int_t *      vFlopReprs;      
     Abc_Cex_t *      pSeqModel;
-    Vec_Ptr_t *      pSeqModelVec;   // vector of counter-examples (for sequential miters)
+    Vec_Ptr_t *      vSeqModelVec;   // vector of counter-examples (for sequential miters)
     Aig_Man_t *      pManExdc;
     Vec_Ptr_t *      vOnehots;
     Aig_Man_t *      pManHaig;
diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c
index bce56424..b0544c90 100644
--- a/src/aig/aig/aigMan.c
+++ b/src/aig/aig/aigMan.c
@@ -211,8 +211,8 @@ void Aig_ManStop( Aig_Man_t * p )
     Vec_IntFreeP( &p->vProbs );
     Vec_IntFreeP( &p->vCiNumsOrig );
     Vec_PtrFreeP( &p->vMapped );
-    if ( p->pSeqModelVec )
-        Vec_PtrFreeFree( p->pSeqModelVec );
+    if ( p->vSeqModelVec )
+        Vec_PtrFreeFree( p->vSeqModelVec );
     ABC_FREE( p->pTerSimData );
     ABC_FREE( p->pFastSim );
     ABC_FREE( p->pData );
diff --git a/src/aig/saig/saigBmc3.c b/src/aig/saig/saigBmc3.c
index b984844e..4dc0c714 100644
--- a/src/aig/saig/saigBmc3.c
+++ b/src/aig/saig/saigBmc3.c
@@ -612,8 +612,8 @@ void Saig_Bmc3ManStop( Gia_ManBmc_t * p )
     Aig_ManCleanMarkA( p->pAig );
     if ( p->vCexes )
     {
-        assert( p->pAig->pSeqModelVec == NULL );
-        p->pAig->pSeqModelVec = p->vCexes;
+        assert( p->pAig->vSeqModelVec == NULL );
+        p->pAig->vSeqModelVec = p->vCexes;
         p->vCexes = NULL;
     }
 //    Vec_PtrFreeFree( p->vCexes );
@@ -1133,7 +1133,8 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
             return 0;
         }
         // consider the next timeframe
-        pPars->iFrame = f;
+        if ( RetValue == -1 && pPars->nStart == 0 )
+            pPars->iFrame = f;
         // resize the array
         Vec_IntFillExtra( p->vPiVars, (f+1)*Saig_ManPiNum(p->pAig), 0 );
         // map nodes of this section
@@ -1206,6 +1207,7 @@ clkOther += clock() - clk2;
                 if ( p->vCexes == NULL )
                     p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) );
                 Vec_PtrWriteEntry( p->vCexes, i, pCex );
+                RetValue = 0;
                 continue;
             }
             // solve this output
@@ -1254,6 +1256,7 @@ clkOther += clock() - clk2;
                 if ( p->vCexes == NULL )
                     p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) );
                 Vec_PtrWriteEntry( p->vCexes, i, pCex );
+                RetValue = 0;
             }
             else 
             {
diff --git a/src/aig/saig/saigCexMin.c b/src/aig/saig/saigCexMin.c
index dd88fb70..824f9eb3 100644
--- a/src/aig/saig/saigCexMin.c
+++ b/src/aig/saig/saigCexMin.c
@@ -252,7 +252,7 @@ void Saig_ManCexMinDerivePhasePriority( Aig_Man_t * pAig, Abc_Cex_t * pCex, Vec_
   SeeAlso     []
  
 ***********************************************************************/
-Vec_Vec_t * Saig_ManCexMinCollectPhasePriority( Aig_Man_t * pAig, Abc_Cex_t * pCex, Vec_Vec_t * vFrameCis )
+Vec_Vec_t * Saig_ManCexMinCollectPhasePriority_( Aig_Man_t * pAig, Abc_Cex_t * pCex, Vec_Vec_t * vFrameCis )
 {
     Vec_Vec_t * vFramePPs;
     Vec_Int_t * vRoots, * vFramePPsOne, * vFrameCisOne;
@@ -302,6 +302,67 @@ Vec_Vec_t * Saig_ManCexMinCollectPhasePriority( Aig_Man_t * pAig, Abc_Cex_t * pC
     return vFramePPs;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Collects phase and priority of all timeframes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+ 
+***********************************************************************/
+Vec_Vec_t * Saig_ManCexMinCollectPhasePriority( Aig_Man_t * pAig, Abc_Cex_t * pCex, Vec_Vec_t * vFrameCis )
+{
+    Vec_Vec_t * vFramePPs;
+    Vec_Int_t * vRoots, * vFramePPsOne, * vFrameCisOne;
+    Aig_Obj_t * pObj;
+    int i, f, nPrioOffset;
+
+    // initialize phase and priority
+    Aig_ManForEachObj( pAig, pObj, i )
+        pObj->iData = -1;
+
+    // set the constant node to higher priority than the flops
+    vFramePPs = Vec_VecStart( pCex->iFrame+1 );
+    nPrioOffset = pCex->nRegs;
+    Aig_ManConst1(pAig)->iData = Aig_Var2Lit( nPrioOffset + (pCex->iFrame + 1) * pCex->nPis, 1 );
+    vRoots = Vec_IntAlloc( 1000 );
+//printf( "Const1 = %d  Offset = %d\n", Aig_ManConst1(pAig)->iData, nPrioOffset ); 
+    for ( f = 0; f <= pCex->iFrame; f++ )
+    {
+        int nPiCount = 0;
+        // fill in PP for the CIs
+        vFrameCisOne = Vec_VecEntryInt( vFrameCis, f );
+        vFramePPsOne = Vec_VecEntryInt( vFramePPs, f );
+        assert( Vec_IntSize(vFramePPsOne) == 0 );
+        Aig_ManForEachObjVec( vFrameCisOne, pAig, pObj, i )
+        {
+            assert( Aig_ObjIsPi(pObj) );
+            if ( Saig_ObjIsPi(pAig, pObj) )
+                Vec_IntPush( vFramePPsOne, Aig_Var2Lit( nPrioOffset + (f+1) * pCex->nPis - 1 - nPiCount++, Aig_InfoHasBit(pCex->pData, pCex->nRegs + f * pCex->nPis + Aig_ObjPioNum(pObj)) ) );
+            else if ( f == 0 )
+                Vec_IntPush( vFramePPsOne, Aig_Var2Lit( Saig_ObjRegId(pAig, pObj), 0 ) );
+            else
+            {
+                Aig_Obj_t * pObj0 = Saig_ObjLoToLi(pAig, pObj);
+                int Value = Saig_ObjLoToLi(pAig, pObj)->iData;
+                Vec_IntPush( vFramePPsOne, Saig_ObjLoToLi(pAig, pObj)->iData );
+            }
+//printf( "%d ", Vec_IntEntryLast(vFramePPsOne) );
+        }
+//printf( "\n" );
+        // compute the PP info
+        Saig_ManCexMinDerivePhasePriority( pAig, pCex, vFrameCis, vFramePPs, f, vRoots );
+    }
+    Vec_IntFree( vRoots );
+    // check the output
+    pObj = Aig_ManPo( pAig, pCex->iPo );
+    assert( Aig_LitIsCompl(pObj->iData) );
+    return vFramePPs;
+}
+
 
 /**Function*************************************************************