5 files changed, 37 insertions, 3 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 3358ca76..e3546686 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -179,6 +179,7 @@ struct Gia_ParSim_t_
     // user-controlled parameters
     int            nWords;        // the number of machine words
     int            nIters;        // the number of timeframes
+    int            RandSeed;      // seed to generate random numbers
     int            TimeLimit;     // time limit in seconds
     int            fCheckMiter;   // check if miter outputs are non-zero
     int            fVerbose;      // enables verbose output
diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c
index 4c19b4f5..581383ea 100644
--- a/src/aig/gia/giaEquiv.c
+++ b/src/aig/gia/giaEquiv.c
@@ -1049,6 +1049,11 @@ Gia_Man_t * Gia_ManSpecReduceInitFrames( Gia_Man_t * p, Abc_Cex_t * pInit, int n
             break;
         if ( f == nFramesMax )
             break;
+        if ( Gia_ManAndNum(pFrames) > 500000 )
+        {
+            Gia_ManStop( pFrames );
+            return NULL;
+        }
         Gia_ManStop( pFrames );
         pFrames = NULL;
     }
diff --git a/src/aig/gia/giaSim.c b/src/aig/gia/giaSim.c
index 68b50fb6..1de1a2d4 100644
--- a/src/aig/gia/giaSim.c
+++ b/src/aig/gia/giaSim.c
@@ -65,6 +65,7 @@ void Gia_ManSimSetDefaultParams( Gia_ParSim_t * p )
     // user-controlled parameters
     p->nWords       =   8;    // the number of machine words
     p->nIters       =  32;    // the number of timeframes
+    p->RandSeed     =   0;    // the seed to generate random numbers
     p->TimeLimit    =  60;    // time limit in seconds
     p->fCheckMiter  =   0;    // check if miter outputs are non-zero 
     p->fVerbose     =   0;    // enables verbose output
@@ -437,9 +438,8 @@ Abc_Cex_t * Gia_ManGenerateCounter( Gia_Man_t * pAig, int iFrame, int iOut, int
     int f, i, w, iPioId, Counter;
     p = Gia_ManAllocCounterExample( Gia_ManRegNum(pAig), Gia_ManPiNum(pAig), iFrame+1 );
     p->iFrame = iFrame;
-    p->iPo = iOut;
+    p->iPo    = iOut;
     // fill in the binary data
-    Gia_ManRandom( 1 );
     Counter = p->nRegs;
     pData = ABC_ALLOC( unsigned, nWords );
     for ( f = 0; f <= iFrame; f++, Counter += p->nPis )
@@ -468,14 +468,36 @@ Abc_Cex_t * Gia_ManGenerateCounter( Gia_Man_t * pAig, int iFrame, int iOut, int
   SeeAlso     []
 
 ***********************************************************************/
+void Gia_ManResetRandom( Gia_ParSim_t * pPars )
+{
+    int i;
+    Gia_ManRandom( 1 );
+    for ( i = 0; i < pPars->RandSeed; i++ )
+        Gia_ManRandom( 0 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Gia_ManSimSimulate( Gia_Man_t * pAig, Gia_ParSim_t * pPars )
 {
+    extern int Gia_ManSimSimulateEquiv( Gia_Man_t * pAig, Gia_ParSim_t * pPars );
     Gia_ManSim_t * p;
     int i, clkTotal = clock();
     int iOut, iPat, RetValue = 0;
+    if ( pAig->pReprs && pAig->pNexts )
+        return Gia_ManSimSimulateEquiv( pAig, pPars );
     ABC_FREE( pAig->pCexSeq );
     p = Gia_ManSimCreate( pAig, pPars );
-    Gia_ManRandom( 1 );
+    Gia_ManResetRandom( pPars );
     Gia_ManSimInfoInit( p );
     for ( i = 0; i < pPars->nIters; i++ )
     {
@@ -487,6 +509,7 @@ int Gia_ManSimSimulate( Gia_Man_t * pAig, Gia_ParSim_t * pPars )
         }
         if ( pPars->fCheckMiter && Gia_ManCheckPos( p, &iOut, &iPat ) )
         {
+            Gia_ManResetRandom( pPars );
             pPars->iOutFail = iOut;
             pAig->pCexSeq = Gia_ManGenerateCounter( pAig, i, iOut, p->nWords, iPat, p->vCis2Ids );
             Abc_Print( 1, "Networks are NOT EQUIVALENT.   Output %d was asserted in frame %d.  ", iOut, i );
diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c
index 002e766d..82bdb367 100644
--- a/src/aig/gia/giaUtil.c
+++ b/src/aig/gia/giaUtil.c
@@ -952,8 +952,12 @@ int Gia_ManVerifyCounterExample( Gia_Man_t * pAig, Abc_Cex_t * p, int fDualOut )
                            (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
         Gia_ManForEachCo( pAig, pObj, k )
             pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
+        if ( i == p->iFrame )
+            break;
         Gia_ManForEachRiRo( pAig, pObjRi, pObjRo, k )
+        {
             pObjRo->fMark0 = pObjRi->fMark0;
+        }
     }
     assert( iBit == p->nBits );
     if ( fDualOut )
diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make
index fc1c5c73..fd0e0a5e 100644
--- a/src/aig/gia/module.make
+++ b/src/aig/gia/module.make
@@ -29,6 +29,7 @@ SRC +=    src/aig/gia/gia.c \
     src/aig/gia/giaScl.c \
     src/aig/gia/giaShrink.c \
     src/aig/gia/giaSim.c \
+    src/aig/gia/giaSim2.c \
     src/aig/gia/giaSort.c \
     src/aig/gia/giaSpeedup.c \
     src/aig/gia/giaSupMin.c \