Version abc90424

1 files changed, 182 insertions, 73 deletions

diff --git a/src/aig/cec/cecCorr.c b/src/aig/cec/cecCorr.c
index 8e97e207..b4076916 100644
--- a/src/aig/cec/cecCorr.c
+++ b/src/aig/cec/cecCorr.c
@@ -24,7 +24,7 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static void Gia_ManCorrSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f );
+static void Gia_ManCorrSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -41,12 +41,12 @@ static void Gia_ManCorrSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_
   SeeAlso     []
 
 ***********************************************************************/
-static inline int Gia_ManCorrSpecReal( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f )
+static inline int Gia_ManCorrSpecReal( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix )
 {
     if ( Gia_ObjIsAnd(pObj) )
     {
-        Gia_ManCorrSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), f );
-        Gia_ManCorrSpecReduce_rec( pNew, p, Gia_ObjFanin1(pObj), f );
+        Gia_ManCorrSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), f, nPrefix );
+        Gia_ManCorrSpecReduce_rec( pNew, p, Gia_ObjFanin1(pObj), f, nPrefix );
         return Gia_ManHashAnd( pNew, Gia_ObjFanin0CopyF(p, f, pObj), Gia_ObjFanin1CopyF(p, f, pObj) );
     }
     if ( f == 0 )
@@ -56,7 +56,7 @@ static inline int Gia_ManCorrSpecReal( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_
     }
     assert( f && Gia_ObjIsRo(p, pObj) );
     pObj = Gia_ObjRoToRi( p, pObj );
-    Gia_ManCorrSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), f-1 );
+    Gia_ManCorrSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), f-1, nPrefix );
     return Gia_ObjFanin0CopyF( p, f-1, pObj );
 }
 
@@ -71,21 +71,21 @@ static inline int Gia_ManCorrSpecReal( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_
   SeeAlso     []
 
 ***********************************************************************/
-void Gia_ManCorrSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f )
+void Gia_ManCorrSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix )
 {
     Gia_Obj_t * pRepr;
     int iLitNew;
     if ( ~Gia_ObjCopyF(p, f, pObj) )
         return;
-    if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) )
+    if ( f >= nPrefix && (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) )
     {
-        Gia_ManCorrSpecReduce_rec( pNew, p, pRepr, f );
+        Gia_ManCorrSpecReduce_rec( pNew, p, pRepr, f, nPrefix );
         iLitNew = Gia_LitNotCond( Gia_ObjCopyF(p, f, pRepr), Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );
         Gia_ObjSetCopyF( p, f, pObj, iLitNew );
         return;
     }
     assert( Gia_ObjIsCand(pObj) );
-    iLitNew = Gia_ManCorrSpecReal( pNew, p, pObj, f );
+    iLitNew = Gia_ManCorrSpecReal( pNew, p, pObj, f, nPrefix );
     Gia_ObjSetCopyF( p, f, pObj, iLitNew );
 }
 
@@ -134,7 +134,7 @@ Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_I
         {
             if ( Gia_ObjIsConst( p, i ) )
             {
-                iObjNew = Gia_ManCorrSpecReal( pNew, p, pObj, nFrames );
+                iObjNew = Gia_ManCorrSpecReal( pNew, p, pObj, nFrames, 0 );
                 iObjNew = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pObj) );
                 if ( iObjNew != 0 )
                 {
@@ -148,8 +148,8 @@ Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_I
                 iPrev = i;
                 Gia_ClassForEachObj1( p, i, iObj )
                 {
-                    iPrevNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iPrev), nFrames );
-                    iObjNew  = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iObj), nFrames );
+                    iPrevNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iPrev), nFrames, 0 );
+                    iObjNew  = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iObj), nFrames, 0 );
                     iPrevNew = Gia_LitNotCond( iPrevNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iPrev)) );
                     iObjNew  = Gia_LitNotCond( iObjNew,  Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iObj)) );
                     if ( iPrevNew != iObjNew && iPrevNew != 0 && iObjNew != 1 )
@@ -161,8 +161,8 @@ Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_I
                     iPrev = iObj;
                 }
                 iObj = i;
-                iPrevNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iPrev), nFrames );
-                iObjNew  = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iObj), nFrames );
+                iPrevNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iPrev), nFrames, 0 );
+                iObjNew  = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iObj), nFrames, 0 );
                 iPrevNew = Gia_LitNotCond( iPrevNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iPrev)) );
                 iObjNew  = Gia_LitNotCond( iObjNew,  Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iObj)) );
                 if ( iPrevNew != iObjNew && iPrevNew != 0 && iObjNew != 1 )
@@ -181,8 +181,8 @@ Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_I
             pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) );
             if ( pRepr == NULL )
                 continue;
-            iPrevNew = Gia_ObjIsConst(p, i)? 0 : Gia_ManCorrSpecReal( pNew, p, pRepr, nFrames );
-            iObjNew  = Gia_ManCorrSpecReal( pNew, p, pObj, nFrames );
+            iPrevNew = Gia_ObjIsConst(p, i)? 0 : Gia_ManCorrSpecReal( pNew, p, pRepr, nFrames, 0 );
+            iObjNew  = Gia_ManCorrSpecReal( pNew, p, pObj, nFrames, 0 );
             iObjNew  = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );
             if ( iPrevNew != iObjNew )
             {
@@ -216,18 +216,18 @@ Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, int fScorr, Vec_I
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Gia_ManCorrSpecReduceInit( Gia_Man_t * p, int nFrames, int fScorr, Vec_Int_t ** pvOutputs, int fRings )
+Gia_Man_t * Gia_ManCorrSpecReduceInit( Gia_Man_t * p, int nFrames, int nPrefix, int fScorr, Vec_Int_t ** pvOutputs, int fRings )
 {
     Gia_Man_t * pNew, * pTemp;
     Gia_Obj_t * pObj, * pRepr;
     Vec_Int_t * vXorLits;
     int f, i, iPrevNew, iObjNew;
-    assert( (!fScorr && nFrames > 1) || (fScorr && nFrames > 0) );
+    assert( (!fScorr && nFrames > 1) || (fScorr && nFrames > 0) || nPrefix );
     assert( Gia_ManRegNum(p) > 0 );
     assert( p->pReprs != NULL );
-    p->pCopies = ABC_FALLOC( int, (nFrames+fScorr)*Gia_ManObjNum(p) );
+    p->pCopies = ABC_FALLOC( int, (nFrames+nPrefix+fScorr)*Gia_ManObjNum(p) );
     Gia_ManSetPhase( p );
-    pNew = Gia_ManStart( nFrames * Gia_ManObjNum(p) );
+    pNew = Gia_ManStart( (nFrames+nPrefix) * Gia_ManObjNum(p) );
     pNew->pName = Gia_UtilStrsav( p->pName );
     Gia_ManHashAlloc( pNew );
     Gia_ManForEachRo( p, pObj, i )
@@ -235,7 +235,7 @@ Gia_Man_t * Gia_ManCorrSpecReduceInit( Gia_Man_t * p, int nFrames, int fScorr, V
         Gia_ManAppendCi(pNew);
         Gia_ObjSetCopyF( p, 0, pObj, 0 );
     }
-    for ( f = 0; f < nFrames+fScorr; f++ )
+    for ( f = 0; f < nFrames+nPrefix+fScorr; f++ )
     { 
         Gia_ObjSetCopyF( p, f, Gia_ManConst0(p), 0 );
         Gia_ManForEachPi( p, pObj, i )
@@ -243,15 +243,15 @@ Gia_Man_t * Gia_ManCorrSpecReduceInit( Gia_Man_t * p, int nFrames, int fScorr, V
     }
     *pvOutputs = Vec_IntAlloc( 1000 );
     vXorLits = Vec_IntAlloc( 1000 );
-    for ( f = 0; f < nFrames; f++ )
+    for ( f = nPrefix; f < nFrames+nPrefix; f++ )
     {
         Gia_ManForEachObj1( p, pObj, i )
         {
             pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) );
             if ( pRepr == NULL )
                 continue;
-            iPrevNew = Gia_ObjIsConst(p, i)? 0 : Gia_ManCorrSpecReal( pNew, p, pRepr, f );
-            iObjNew  = Gia_ManCorrSpecReal( pNew, p, pObj, f );
+            iPrevNew = Gia_ObjIsConst(p, i)? 0 : Gia_ManCorrSpecReal( pNew, p, pRepr, f, nPrefix );
+            iObjNew  = Gia_ManCorrSpecReal( pNew, p, pObj, f, nPrefix );
             iObjNew  = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );
             if ( iPrevNew != iObjNew )
             {
@@ -752,6 +752,74 @@ void Cec_ManRefinedClassPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIte
 
 /**Function*************************************************************
 
+  Synopsis    [Runs BMC for the equivalence classes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_ManLSCorrespondenceBmc( Gia_Man_t * pAig, Cec_ParCor_t * pPars, int nPrefs )
+{  
+    Cec_ParSim_t ParsSim, * pParsSim = &ParsSim;
+    Cec_ParSat_t ParsSat, * pParsSat = &ParsSat;
+    Vec_Str_t * vStatus;
+    Vec_Int_t * vOutputs;
+    Vec_Int_t * vCexStore;
+    Cec_ManSim_t * pSim;
+    Gia_Man_t * pSrm;
+    int fChanges, RetValue;
+    // prepare simulation manager
+    Cec_ManSimSetDefaultParams( pParsSim );
+    pParsSim->nWords     = pPars->nWords;
+    pParsSim->nRounds    = pPars->nRounds;
+    pParsSim->fVerbose   = pPars->fVerbose;
+    pParsSim->fLatchCorr = pPars->fLatchCorr;
+    pParsSim->fSeqSimulate = 1;
+    pSim = Cec_ManSimStart( pAig, pParsSim );
+    // prepare SAT solving
+    Cec_ManSatSetDefaultParams( pParsSat );
+    pParsSat->nBTLimit = pPars->nBTLimit;
+    pParsSat->fVerbose = pPars->fVerbose;
+    fChanges = 1;
+    while ( fChanges )
+    {
+        int clkBmc = clock();
+        fChanges = 0;
+        pSrm = Gia_ManCorrSpecReduceInit( pAig, pPars->nFrames, nPrefs, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings );
+        if ( Gia_ManPoNum(pSrm) == 0 )
+        {
+            Gia_ManStop( pSrm );
+            Vec_IntFree( vOutputs );
+            break;
+        } 
+        pParsSat->nBTLimit *= 10;
+        if ( pPars->fUseCSat )
+            vCexStore = Cbs_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0 );
+        else
+            vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus );
+        // refine classes with these counter-examples
+        if ( Vec_IntSize(vCexStore) )
+        {
+            RetValue = Cec_ManResimulateCounterExamples( pSim, vCexStore, pPars->nFrames + 1 + nPrefs );
+            Gia_ManCheckRefinements( pAig, vStatus, vOutputs, pSim, pPars->fUseRings );
+            fChanges = 1;
+        }
+        if ( pPars->fVerbose )
+            Cec_ManRefinedClassPrintStats( pAig, vStatus, -1, clock() - clkBmc );
+        // recycle
+        Vec_IntFree( vCexStore );
+        Vec_StrFree( vStatus );
+        Gia_ManStop( pSrm );
+        Vec_IntFree( vOutputs );
+    }
+    Cec_ManSimStop( pSim );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Internal procedure for register correspondence.]
 
   Description []
@@ -775,8 +843,6 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
     int r, RetValue, clkTotal = clock();
     int clkSat = 0, clkSim = 0, clkSrm = 0;
     int clk2, clk = clock();
-    ABC_FREE( pAig->pReprs );
-    ABC_FREE( pAig->pNexts );
     if ( Gia_ManRegNum(pAig) == 0 )
     {
         printf( "Cec_ManLatchCorrespondence(): Not a sequential AIG.\n" );
@@ -792,8 +858,11 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
     pParsSim->fSeqSimulate = 1;
     // create equivalence classes of registers
     pSim = Cec_ManSimStart( pAig, pParsSim );
-    Cec_ManSimClassesPrepare( pSim );
-    Cec_ManSimClassesRefine( pSim );
+    if ( pAig->pReprs == NULL )
+    {
+        Cec_ManSimClassesPrepare( pSim );
+        Cec_ManSimClassesRefine( pSim );
+    }
     // prepare SAT solving
     Cec_ManSatSetDefaultParams( pParsSat );
     pParsSat->nBTLimit = pPars->nBTLimit;
@@ -805,6 +874,9 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
             pPars->nBTLimit, pPars->nFrames, pPars->fLatchCorr, pPars->fUseRings, pPars->fUseCSat );
         Cec_ManRefinedClassPrintStats( pAig, NULL, 0, clock() - clk );
     }
+    // check the base case
+    if ( !pPars->fLatchCorr || pPars->nFrames > 1 )
+            Cec_ManLSCorrespondenceBmc( pAig, pPars, 0 );
     // perform refinement of equivalence classes
     for ( r = 0; r < nIterMax; r++ )
     { 
@@ -848,49 +920,8 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
         Vec_IntFree( vOutputs );
 //Gia_ManEquivPrintClasses( pAig, 1, 0 );
     }
-    // check the base case
-    if ( !pPars->fLatchCorr || pPars->nFrames > 1 )
-    {
-        int fChanges = 1;
-        while ( fChanges )
-        {
-            int clkBmc = clock();
-            fChanges = 0;
-            pSrm = Gia_ManCorrSpecReduceInit( pAig, pPars->nFrames, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings );
-            if ( Gia_ManPoNum(pSrm) == 0 )
-            {
-                Gia_ManStop( pSrm );
-                Vec_IntFree( vOutputs );
-                break;
-            }
-            pParsSat->nBTLimit *= 10;
-            if ( pPars->fUseCSat )
-                vCexStore = Cbs_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0 );
-            else
-                vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus );
-            // refine classes with these counter-examples
-            if ( Vec_IntSize(vCexStore) )
-            {
-                clk2 = clock();
-                RetValue = Cec_ManResimulateCounterExamples( pSim, vCexStore, pPars->nFrames + 1 + nAddFrames );
-                clkSim += clock() - clk2;
-                Gia_ManCheckRefinements( pAig, vStatus, vOutputs, pSim, pPars->fUseRings );
-                fChanges = 1;
-            }
-            if ( pPars->fVerbose )
-                Cec_ManRefinedClassPrintStats( pAig, vStatus, -1, clock() - clkBmc );
-            // recycle
-            Vec_IntFree( vCexStore );
-            Vec_StrFree( vStatus );
-            Gia_ManStop( pSrm );
-            Vec_IntFree( vOutputs );
-        }
-    }
-    else
-    {
-        if ( pPars->fVerbose )
-            Cec_ManRefinedClassPrintStats( pAig, NULL, r+1, clock() - clk );
-    }
+    if ( pPars->fVerbose )
+        Cec_ManRefinedClassPrintStats( pAig, NULL, r+1, clock() - clk );
     // check the overflow
     if ( r == nIterMax )
         printf( "The refinement was not finished. The result may be incorrect.\n" );
@@ -910,6 +941,51 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
 
 /**Function*************************************************************
 
+  Synopsis    [Computes new initial state.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned * Cec_ManComputeInitState( Gia_Man_t * pAig, int nFrames )
+{  
+    Gia_Obj_t * pObj, * pObjRo, * pObjRi;
+    unsigned * pInitState;
+    int i, f; 
+    Gia_ManRandom( 1 );
+//    printf( "Simulating %d timeframes.\n", nFrames );
+    Gia_ManForEachRo( pAig, pObj, i )
+        pObj->fMark1 = 0;
+    for ( f = 0; f < nFrames; f++ )
+    {
+        Gia_ManConst0(pAig)->fMark1 = 0;
+        Gia_ManForEachPi( pAig, pObj, i )
+            pObj->fMark1 = Gia_ManRandom(0) & 1;
+        Gia_ManForEachAnd( pAig, pObj, i )
+            pObj->fMark1 = (Gia_ObjFanin0(pObj)->fMark1 ^ Gia_ObjFaninC0(pObj)) & 
+                (Gia_ObjFanin1(pObj)->fMark1 ^ Gia_ObjFaninC1(pObj));
+        Gia_ManForEachRi( pAig, pObj, i )
+            pObj->fMark1 = (Gia_ObjFanin0(pObj)->fMark1 ^ Gia_ObjFaninC0(pObj));
+        Gia_ManForEachRiRo( pAig, pObjRi, pObjRo, i )
+            pObjRo->fMark1 = pObjRi->fMark1;
+    }
+    pInitState = ABC_CALLOC( unsigned, Gia_BitWordNum(Gia_ManRegNum(pAig)) );
+    Gia_ManForEachRo( pAig, pObj, i )
+    {
+        if ( pObj->fMark1 )
+            Gia_InfoSetBit( pInitState, i );
+//        printf( "%d", pObj->fMark1 );
+    }
+//    printf( "\n" );
+    Gia_ManCleanMark1( pAig );
+    return pInitState;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Top-level procedure for register correspondence.]
 
   Description []
@@ -922,8 +998,39 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
 Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
 {  
     Gia_Man_t * pNew, * pTemp;
+    unsigned * pInitState;
     int RetValue;
-    RetValue = Cec_ManLSCorrespondenceClasses( pAig, pPars );
+    ABC_FREE( pAig->pReprs );
+    ABC_FREE( pAig->pNexts );
+    if ( pPars->nPrefix == 0 )
+        RetValue = Cec_ManLSCorrespondenceClasses( pAig, pPars );
+    else
+    {
+        // compute the cycles AIG
+        pInitState = Cec_ManComputeInitState( pAig, pPars->nPrefix );
+        pTemp = Gia_ManDupFlip( pAig, pInitState );
+        ABC_FREE( pInitState );
+        // compute classes of this AIG
+        RetValue = Cec_ManLSCorrespondenceClasses( pTemp, pPars );
+        // transfer the class info
+        pAig->pReprs = pTemp->pReprs; pTemp->pReprs = NULL;
+        pAig->pNexts = pTemp->pNexts; pTemp->pNexts = NULL;
+        // perform additional BMC
+        pPars->fUseCSat = 0;
+        pPars->nBTLimit = ABC_MAX( pPars->nBTLimit, 1000 );
+        Cec_ManLSCorrespondenceBmc( pAig, pPars, pPars->nPrefix );
+/*
+        // transfer the class info back
+        pTemp->pReprs = pAig->pReprs; pAig->pReprs = NULL;
+        pTemp->pNexts = pAig->pNexts; pAig->pNexts = NULL;
+        // continue refining
+        RetValue = Cec_ManLSCorrespondenceClasses( pTemp, pPars );
+        // transfer the class info
+        pAig->pReprs = pTemp->pReprs; pTemp->pReprs = NULL;
+        pAig->pNexts = pTemp->pNexts; pTemp->pNexts = NULL;
+*/
+        Gia_ManStop( pTemp );
+    }
     // derive reduced AIG
     if ( pPars->fMakeChoices )
     {
@@ -932,7 +1039,7 @@ Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
     }
     else
     {
-        Gia_ManEquivImprove( pAig );
+//        Gia_ManEquivImprove( pAig );
         pNew = Gia_ManCorrReduce( pAig );
         pNew = Gia_ManSeqCleanup( pTemp = pNew );
         Gia_ManStop( pTemp );
@@ -947,6 +1054,8 @@ Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
             Gia_ManRegNum(pAig), Gia_ManRegNum(pNew), 
             100.0*(Gia_ManRegNum(pAig)-Gia_ManRegNum(pNew))/(Gia_ManRegNum(pAig)?Gia_ManRegNum(pAig):1) );
     }
+    if ( pPars->nPrefix && (Gia_ManAndNum(pNew) < Gia_ManAndNum(pAig) || Gia_ManRegNum(pNew) < Gia_ManRegNum(pAig)) )
+        printf( "The reduced AIG was produced using %d-th invariants and will not verify.\n", pPars->nPrefix );
     return pNew;
 }