Fixed several important problems in choice computation (command 'dch').

3 files changed, 216 insertions, 1232 deletions

diff --git a/src/proof/cec/cecCorr_updated.c b/src/proof/cec/cecCorr_updated.c
deleted file mode 100644
index 0d441629..00000000
--- a/src/proof/cec/cecCorr_updated.c
+++ /dev/null
@@ -1,1028 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [cecCorr.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Combinational equivalence checking.]
-
-  Synopsis    [Latch/signal correspondence computation.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: cecCorr.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "cecInt.h"
-
-ABC_NAMESPACE_IMPL_START
-
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-static void Gia_ManCorrSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, int f, int nPrefix );
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Computes the real value of the literal w/o spec reduction.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-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, 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 )
-    {
-        assert( Gia_ObjIsRo(p, pObj) );
-        return Gia_ObjCopyF(p, f, pObj);
-    }
-    assert( f && Gia_ObjIsRo(p, pObj) );
-    pObj = Gia_ObjRoToRi( p, pObj );
-    Gia_ManCorrSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), f-1, nPrefix );
-    return Gia_ObjFanin0CopyF( p, f-1, pObj );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Recursively performs speculative reduction for the object.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-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 ( f >= nPrefix && (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) )
-    {
-        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, nPrefix );
-    Gia_ObjSetCopyF( p, f, pObj, iLitNew );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Derives SRM for signal correspondence.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Gia_Man_t * Gia_ManCorrSpecReduce( Gia_Man_t * p, int nFrames, 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, iPrev, iObj, iPrevNew, iObjNew;
-    assert( nFrames > 0 );
-    assert( Gia_ManRegNum(p) > 0 );
-    assert( p->pReprs != NULL );
-    p->pCopies = ABC_FALLOC( int, (nFrames+fScorr)*Gia_ManObjNum(p) );
-    Gia_ManSetPhase( p );
-    pNew = Gia_ManStart( nFrames * Gia_ManObjNum(p) );
-    pNew->pName = Gia_UtilStrsav( p->pName );
-    Gia_ManHashAlloc( pNew );
-    Gia_ObjSetCopyF( p, 0, Gia_ManConst0(p), 0 );
-    Gia_ManForEachRo( p, pObj, i )
-        Gia_ObjSetCopyF( p, 0, pObj, Gia_ManAppendCi(pNew) );
-    Gia_ManForEachRo( p, pObj, i )
-        if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) )
-            Gia_ObjSetCopyF( p, 0, pObj, Gia_ObjCopyF(p, 0, pRepr) );
-    for ( f = 0; f < nFrames+fScorr; f++ )
-    { 
-        Gia_ObjSetCopyF( p, f, Gia_ManConst0(p), 0 );
-        Gia_ManForEachPi( p, pObj, i )
-            Gia_ObjSetCopyF( p, f, pObj, Gia_ManAppendCi(pNew) );
-    }
-    *pvOutputs = Vec_IntAlloc( 1000 );
-    vXorLits = Vec_IntAlloc( 1000 );
-    if ( fRings )
-    {
-        Gia_ManForEachObj1( p, pObj, i )
-        {
-            if ( Gia_ObjIsConst( p, i ) )
-            {
-                iObjNew = Gia_ManCorrSpecReal( pNew, p, pObj, nFrames, 0 );
-                iObjNew = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pObj) );
-                if ( iObjNew != 0 )
-                {
-                    Vec_IntPush( *pvOutputs, 0 );
-                    Vec_IntPush( *pvOutputs, i );
-                    Vec_IntPush( vXorLits, iObjNew );
-                }
-            }
-            else if ( Gia_ObjIsHead( p, i ) )
-            {
-                iPrev = i;
-                Gia_ClassForEachObj1( p, i, iObj )
-                {
-                    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 )
-                    {
-                        Vec_IntPush( *pvOutputs, iPrev );
-                        Vec_IntPush( *pvOutputs, iObj );
-                        Vec_IntPush( vXorLits, Gia_ManHashAnd(pNew, iPrevNew, Gia_LitNot(iObjNew)) );
-                    }
-                    iPrev = iObj;
-                }
-                iObj = i;
-                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 )
-                {
-                    Vec_IntPush( *pvOutputs, iPrev );
-                    Vec_IntPush( *pvOutputs, iObj );
-                    Vec_IntPush( vXorLits, Gia_ManHashAnd(pNew, iPrevNew, Gia_LitNot(iObjNew)) );
-                }
-            }
-        }
-    }
-    else
-    {
-        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, nFrames, 0 );
-            iObjNew  = Gia_ManCorrSpecReal( pNew, p, pObj, nFrames, 0 );
-            iObjNew  = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );
-            if ( iPrevNew != iObjNew )
-            {
-                Vec_IntPush( *pvOutputs, Gia_ObjId(p, pRepr) );
-                Vec_IntPush( *pvOutputs, Gia_ObjId(p, pObj) );
-                Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, iPrevNew, iObjNew) );
-            }
-        }
-    }
-    Vec_IntForEachEntry( vXorLits, iObjNew, i )
-        Gia_ManAppendCo( pNew, iObjNew );
-    Vec_IntFree( vXorLits );
-    Gia_ManHashStop( pNew );
-    ABC_FREE( p->pCopies );
-//printf( "Before sweeping = %d\n", Gia_ManAndNum(pNew) );
-    pNew = Gia_ManCleanup( pTemp = pNew );
-//printf( "After sweeping = %d\n", Gia_ManAndNum(pNew) );
-    Gia_ManStop( pTemp );
-    return pNew;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Derives SRM for signal correspondence.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-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) || nPrefix );
-    assert( Gia_ManRegNum(p) > 0 );
-    assert( p->pReprs != NULL );
-    p->pCopies = ABC_FALLOC( int, (nFrames+nPrefix+fScorr)*Gia_ManObjNum(p) );
-    Gia_ManSetPhase( p );
-    pNew = Gia_ManStart( (nFrames+nPrefix) * Gia_ManObjNum(p) );
-    pNew->pName = Gia_UtilStrsav( p->pName );
-    Gia_ManHashAlloc( pNew );
-    Gia_ManForEachRo( p, pObj, i )
-    {
-        Gia_ManAppendCi(pNew);
-        Gia_ObjSetCopyF( p, 0, pObj, 0 );
-    }
-    for ( f = 0; f < nFrames+nPrefix+fScorr; f++ )
-    { 
-        Gia_ObjSetCopyF( p, f, Gia_ManConst0(p), 0 );
-        Gia_ManForEachPi( p, pObj, i )
-            Gia_ObjSetCopyF( p, f, pObj, Gia_ManAppendCi(pNew) );
-    }
-    *pvOutputs = Vec_IntAlloc( 1000 );
-    vXorLits = Vec_IntAlloc( 1000 );
-    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, nPrefix );
-            iObjNew  = Gia_ManCorrSpecReal( pNew, p, pObj, f, nPrefix );
-            iObjNew  = Gia_LitNotCond( iObjNew, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );
-            if ( iPrevNew != iObjNew )
-            {
-                Vec_IntPush( *pvOutputs, Gia_ObjId(p, pRepr) );
-                Vec_IntPush( *pvOutputs, Gia_ObjId(p, pObj) );
-                Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, iPrevNew, iObjNew) );
-            }
-        }
-    }
-    Vec_IntForEachEntry( vXorLits, iObjNew, i )
-        Gia_ManAppendCo( pNew, iObjNew );
-    Vec_IntFree( vXorLits );
-    Gia_ManHashStop( pNew );
-    ABC_FREE( p->pCopies );
-//printf( "Before sweeping = %d\n", Gia_ManAndNum(pNew) );
-    pNew = Gia_ManCleanup( pTemp = pNew );
-//printf( "After sweeping = %d\n", Gia_ManAndNum(pNew) );
-    Gia_ManStop( pTemp );
-    return pNew;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Initializes simulation info for lcorr/scorr counter-examples.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cec_ManStartSimInfo( Vec_Ptr_t * vInfo, int nFlops, int * pInitState )
-{
-    unsigned * pInfo;
-    int k, w, nWords;
-    nWords = Vec_PtrReadWordsSimInfo( vInfo );
-    assert( nFlops <= Vec_PtrSize(vInfo) );
-    for ( k = 0; k < nFlops; k++ )
-    {
-        pInfo = Vec_PtrEntry( vInfo, k );
-        if ( pInitState && Gia_InfoHasBit(pInitState, k) )
-        {
-            for ( w = 0; w < nWords; w++ )
-                pInfo[w] = ~0;
-//            pInfo[0] <<= 1;
-        }
-        else
-        {
-            for ( w = 0; w < nWords; w++ )
-                pInfo[w] = 0;
-        }
-    }
-    for ( k = nFlops; k < Vec_PtrSize(vInfo); k++ )
-    {
-        pInfo = Vec_PtrEntry( vInfo, k );
-        for ( w = 0; w < nWords; w++ )
-            pInfo[w] = Gia_ManRandom( 0 );
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Remaps simulation info from SRM to the original AIG.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Gia_ManCorrRemapSimInfo( Gia_Man_t * p, Vec_Ptr_t * vInfo )
-{
-    Gia_Obj_t * pObj, * pRepr;
-    unsigned * pInfoObj, * pInfoRepr;
-    int i, w, nWords;
-    nWords = Vec_PtrReadWordsSimInfo( vInfo );
-    Gia_ManForEachRo( p, pObj, i )
-    {
-        // skip ROs without representatives
-        pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) );
-        if ( pRepr == NULL || Gia_ObjFailed(p, Gia_ObjId(p,pObj)) )
-            continue;
-        pInfoObj = Vec_PtrEntry( vInfo, i );
-        for ( w = 0; w < nWords; w++ )
-            assert( pInfoObj[w] == 0 );
-        // skip ROs with constant representatives
-        if ( Gia_ObjIsConst0(pRepr) )
-            continue;
-        assert( Gia_ObjIsRo(p, pRepr) );
-//        printf( "%d -> %d    ", i, Gia_ObjId(p, pRepr) );
-        // transfer info from the representative
-        pInfoRepr = Vec_PtrEntry( vInfo, Gia_ObjCioId(pRepr) - Gia_ManPiNum(p) );
-        for ( w = 0; w < nWords; w++ )
-            pInfoObj[w] = pInfoRepr[w];
-    }
-//    printf( "\n" );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Collects information about remapping.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Int_t * Gia_ManCorrCreateRemapping( Gia_Man_t * p )
-{
-    Vec_Int_t * vPairs;
-    Gia_Obj_t * pObj, * pRepr;
-    int i;
-    vPairs = Vec_IntAlloc( 100 );
-    Gia_ManForEachRo( p, pObj, i )
-    {
-        // skip ROs without representatives
-        pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) );
-        if ( pRepr == NULL || Gia_ObjIsConst0(pRepr) || Gia_ObjFailed(p, Gia_ObjId(p,pObj)) )
-//        if ( pRepr == NULL || Gia_ObjIsConst0(pRepr) || Gia_ObjIsFailedPair(p, Gia_ObjId(p, pRepr), Gia_ObjId(p, pObj)) )
-            continue;
-        assert( Gia_ObjIsRo(p, pRepr) );
-//        printf( "%d -> %d    ", Gia_ObjId(p,pObj), Gia_ObjId(p, pRepr) );
-        // remember the pair
-        Vec_IntPush( vPairs, Gia_ObjCioId(pRepr) - Gia_ManPiNum(p) );
-        Vec_IntPush( vPairs, i );
-    }
-    return vPairs;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Remaps simulation info from SRM to the original AIG.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Gia_ManCorrPerformRemapping( Vec_Int_t * vPairs, Vec_Ptr_t * vInfo, int * pInitState )
-{
-    unsigned * pInfoObj, * pInfoRepr;
-    int w, i, iObj, iRepr, nWords;
-    nWords = Vec_PtrReadWordsSimInfo( vInfo );
-    Vec_IntForEachEntry( vPairs, iRepr, i )
-    {
-        iObj = Vec_IntEntry( vPairs, ++i );
-        pInfoObj = Vec_PtrEntry( vInfo, iObj );
-        pInfoRepr = Vec_PtrEntry( vInfo, iRepr );
-        for ( w = 0; w < nWords; w++ )
-        {
-            assert( pInitState || pInfoObj[w] == 0 );
-            pInfoObj[w] = pInfoRepr[w];
-        }
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Packs one counter-examples into the array of simulation info.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-*************************************`**********************************/
-int Cec_ManLoadCounterExamplesTry( Vec_Ptr_t * vInfo, Vec_Ptr_t * vPres, int iBit, int * pLits, int nLits )
-{
-    unsigned * pInfo, * pPres;
-    int i;
-    for ( i = 0; i < nLits; i++ )
-    {
-        pInfo = Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i]));
-        pPres = Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i]));
-        if ( Gia_InfoHasBit( pPres, iBit ) && 
-             Gia_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) )
-             return 0;
-    }
-    for ( i = 0; i < nLits; i++ )
-    {
-        pInfo = Vec_PtrEntry(vInfo, Gia_Lit2Var(pLits[i]));
-        pPres = Vec_PtrEntry(vPres, Gia_Lit2Var(pLits[i]));
-        Gia_InfoSetBit( pPres, iBit );
-        if ( Gia_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(pLits[i]) )
-            Gia_InfoXorBit( pInfo, iBit );
-    }
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs bitpacking of counter-examples.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Cec_ManLoadCounterExamples( Vec_Ptr_t * vInfo, Vec_Int_t * vCexStore, int iStart )
-{ 
-    Vec_Int_t * vPat;
-    Vec_Ptr_t * vPres;
-    int nWords = Vec_PtrReadWordsSimInfo(vInfo);
-    int nBits = 32 * nWords; 
-    int k, nSize, iBit = 1, kMax = 0;
-    vPat  = Vec_IntAlloc( 100 );
-    vPres = Vec_PtrAllocSimInfo( Vec_PtrSize(vInfo), nWords );
-    Vec_PtrCleanSimInfo( vPres, 0, nWords );
-    while ( iStart < Vec_IntSize(vCexStore) )
-    {
-        // skip the output number
-        iStart++;
-        // get the number of items
-        nSize = Vec_IntEntry( vCexStore, iStart++ );
-        if ( nSize <= 0 )
-            continue;
-        // extract pattern
-        Vec_IntClear( vPat );
-        for ( k = 0; k < nSize; k++ )
-            Vec_IntPush( vPat, Vec_IntEntry( vCexStore, iStart++ ) );
-        // add pattern to storage
-        for ( k = 1; k < nBits; k++ )
-            if ( Cec_ManLoadCounterExamplesTry( vInfo, vPres, k, (int *)Vec_IntArray(vPat), Vec_IntSize(vPat) ) )
-                break;
-        kMax = Abc_MaxInt( kMax, k );
-        if ( k == nBits-1 )
-            break;
-    }
-    Vec_PtrFree( vPres );
-    Vec_IntFree( vPat );
-    return iStart;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs bitpacking of counter-examples.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Cec_ManLoadCounterExamples2( Vec_Ptr_t * vInfo, Vec_Int_t * vCexStore, int iStart )
-{ 
-    unsigned * pInfo;
-    int nBits = 32 * Vec_PtrReadWordsSimInfo(vInfo); 
-    int k, iLit, nLits, Out, iBit = 1;
-    while ( iStart < Vec_IntSize(vCexStore) )
-    {
-        // skip the output number
-//        iStart++;
-        Out = Vec_IntEntry( vCexStore, iStart++ );
-//        printf( "iBit = %d. Out = %d.\n", iBit, Out );
-        // get the number of items
-        nLits = Vec_IntEntry( vCexStore, iStart++ );
-        if ( nLits <= 0 )
-            continue;
-        // add pattern to storage
-        for ( k = 0; k < nLits; k++ )
-        {
-            iLit = Vec_IntEntry( vCexStore, iStart++ );
-            pInfo = Vec_PtrEntry( vInfo, Gia_Lit2Var(iLit) );
-            if ( Gia_InfoHasBit( pInfo, iBit ) == Gia_LitIsCompl(iLit) )
-                Gia_InfoXorBit( pInfo, iBit );
-        }
-        if ( ++iBit == nBits )
-            break;
-    }
-//    printf( "added %d bits\n", iBit-1 );
-    return iStart;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Resimulates counter-examples derived by the SAT solver.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Cec_ManResimulateCounterExamples( Cec_ManSim_t * pSim, Vec_Int_t * vCexStore, int nFrames, int * pInitState )
-{ 
-    Vec_Int_t * vPairs;
-    Vec_Ptr_t * vSimInfo; 
-    int RetValue = 0, iStart = 0;
-    vPairs = Gia_ManCorrCreateRemapping( pSim->pAig );
-    Gia_ManSetRefs( pSim->pAig );
-//    pSim->pPars->nWords  = 63;
-    pSim->pPars->nRounds = nFrames;
-    vSimInfo = Vec_PtrAllocSimInfo( Gia_ManRegNum(pSim->pAig) + Gia_ManPiNum(pSim->pAig) * nFrames, pSim->pPars->nWords );
-    while ( iStart < Vec_IntSize(vCexStore) )
-    {
-        Cec_ManStartSimInfo( vSimInfo, Gia_ManRegNum(pSim->pAig), pInitState );
-        iStart = Cec_ManLoadCounterExamples( vSimInfo, vCexStore, iStart );
-//        iStart = Cec_ManLoadCounterExamples2( vSimInfo, vCexStore, iStart );
-//        Gia_ManCorrRemapSimInfo( pSim->pAig, vSimInfo );
-        Gia_ManCorrPerformRemapping( vPairs, vSimInfo, pInitState );
-        RetValue |= Cec_ManSeqResimulate( pSim, vSimInfo );
-//        Cec_ManSeqResimulateInfo( pSim->pAig, vSimInfo, NULL );
-    }
-//Gia_ManEquivPrintOne( pSim->pAig, 85, 0 );
-    assert( iStart == Vec_IntSize(vCexStore) );
-    Vec_PtrFree( vSimInfo );
-    Vec_IntFree( vPairs );
-    return RetValue;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Resimulates counter-examples derived by the SAT solver.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Cec_ManResimulateCounterExamplesComb( Cec_ManSim_t * pSim, Vec_Int_t * vCexStore )
-{ 
-    Vec_Ptr_t * vSimInfo; 
-    int RetValue = 0, iStart = 0;
-    Gia_ManSetRefs( pSim->pAig );
-    pSim->pPars->nRounds = 1;
-    vSimInfo = Vec_PtrAllocSimInfo( Gia_ManCiNum(pSim->pAig), pSim->pPars->nWords );
-    while ( iStart < Vec_IntSize(vCexStore) )
-    {
-        Cec_ManStartSimInfo( vSimInfo, 0, NULL );
-        iStart = Cec_ManLoadCounterExamples( vSimInfo, vCexStore, iStart );
-        RetValue |= Cec_ManSeqResimulate( pSim, vSimInfo );
-    }
-    assert( iStart == Vec_IntSize(vCexStore) );
-    Vec_PtrFree( vSimInfo );
-    return RetValue;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Updates equivalence classes by marking those that timed out.]
-
-  Description [Returns 1 if all ndoes are proved.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Gia_ManCheckRefinements( Gia_Man_t * p, Vec_Str_t * vStatus, Vec_Int_t * vOutputs, Cec_ManSim_t * pSim, int fRings )
-{
-    int i, status, iRepr, iObj;
-    int Counter = 0;
-    assert( 2 * Vec_StrSize(vStatus) == Vec_IntSize(vOutputs) );
-    Vec_StrForEachEntry( vStatus, status, i )
-    {
-        iRepr = Vec_IntEntry( vOutputs, 2*i );
-        iObj  = Vec_IntEntry( vOutputs, 2*i+1 );
-        if ( status == 1 )
-            continue;
-        if ( status == 0 )
-        {
-            if ( Gia_ObjHasSameRepr(p, iRepr, iObj) )
-                Counter++;
-//            if ( Gia_ObjHasSameRepr(p, iRepr, iObj) )
-//                printf( "Gia_ManCheckRefinements(): Disproved equivalence (%d,%d) is not refined!\n", iRepr, iObj );
-//            if ( Gia_ObjHasSameRepr(p, iRepr, iObj) )
-//                Cec_ManSimClassRemoveOne( pSim, iObj );
-            continue;
-        }
-        if ( status == -1 )
-        {
-//            if ( !Gia_ObjFailed( p, iObj ) )
-//                printf( "Gia_ManCheckRefinements(): Failed equivalence is not marked as failed!\n" );
-//            Gia_ObjSetFailed( p, iRepr );
-//            Gia_ObjSetFailed( p, iObj );        
-//            if ( fRings )
-//            Cec_ManSimClassRemoveOne( pSim, iRepr );
-            Cec_ManSimClassRemoveOne( pSim, iObj );
-            continue;
-        }
-    }
-//    if ( Counter )
-//    printf( "Gia_ManCheckRefinements(): Could not refine %d nodes.\n", Counter );
-    return 1;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Duplicates the AIG in the DFS order.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Gia_ManCorrReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
-{
-    Gia_Obj_t * pRepr;
-    if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) )
-    {
-        Gia_ManCorrReduce_rec( pNew, p, pRepr );
-        pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
-        return;
-    }
-    if ( ~pObj->Value )
-        return;
-    assert( Gia_ObjIsAnd(pObj) );
-    Gia_ManCorrReduce_rec( pNew, p, Gia_ObjFanin0(pObj) );
-    Gia_ManCorrReduce_rec( pNew, p, Gia_ObjFanin1(pObj) );
-    pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Reduces AIG using equivalence classes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Gia_Man_t * Gia_ManCorrReduce( Gia_Man_t * p )
-{
-    Gia_Man_t * pNew;
-    Gia_Obj_t * pObj;
-    int i;
-    Gia_ManSetPhase( p );
-    pNew = Gia_ManStart( Gia_ManObjNum(p) );
-    pNew->pName = Gia_UtilStrsav( p->pName );
-    Gia_ManFillValue( p );
-    Gia_ManConst0(p)->Value = 0;
-    Gia_ManForEachCi( p, pObj, i )
-        pObj->Value = Gia_ManAppendCi(pNew);
-    Gia_ManHashAlloc( pNew );
-    Gia_ManForEachCo( p, pObj, i )
-        Gia_ManCorrReduce_rec( pNew, p, Gia_ObjFanin0(pObj) );
-    Gia_ManForEachCo( p, pObj, i )
-        Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
-    Gia_ManHashStop( pNew );
-    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
-    return pNew;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Prints statistics during solving.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Cec_ManRefinedClassPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIter, clock_t Time )
-{ 
-    int nLits, CounterX = 0, Counter0 = 0, Counter = 0;
-    int i, Entry, nProve = 0, nDispr = 0, nFail = 0;
-    for ( i = 1; i < Gia_ManObjNum(p); i++ )
-    {
-        if ( Gia_ObjIsNone(p, i) )
-            CounterX++;
-        else if ( Gia_ObjIsConst(p, i) )
-            Counter0++;
-        else if ( Gia_ObjIsHead(p, i) )
-            Counter++;
-    }
-    CounterX -= Gia_ManCoNum(p);
-    nLits = Gia_ManCiNum(p) + Gia_ManAndNum(p) - Counter - CounterX;
-    if ( iIter == -1 )
-        printf( "BMC : " );
-    else
-        printf( "%3d : ", iIter );
-    printf( "c =%8d  cl =%7d  lit =%8d  ", Counter0, Counter, nLits );
-    if ( vStatus )
-    Vec_StrForEachEntry( vStatus, Entry, i )
-    {
-        if ( Entry == 1 )
-            nProve++;
-        else if ( Entry == 0 )
-            nDispr++;
-        else if ( Entry == -1 )
-            nFail++;
-    }
-    printf( "p =%6d  d =%6d  f =%6d  ", nProve, nDispr, nFail );
-    ABC_PRT( "T", Time );
-}
-
-/**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; 
-    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;
-//            pObj->fMark1 = 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    [Internal procedure for register correspondence.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
-{  
-    int nIterMax = 100000;
-    int nAddFrames = 1; // additional timeframes to simulate
-    Vec_Str_t * vStatus;
-    Vec_Int_t * vOutputs;
-    Vec_Int_t * vCexStore;
-    Cec_ParSim_t ParsSim, * pParsSim = &ParsSim;
-    Cec_ParSat_t ParsSat, * pParsSat = &ParsSat;
-    Cec_ManSim_t * pSim;
-    Gia_Man_t * pSrm;
-    unsigned * pInitState = NULL;
-    int r, RetValue;
-    clock_t clkTotal = clock();
-    clock_t clkSat = 0, clkSim = 0, clkSrm = 0;
-    clock_t clk2, clk = clock();
-    ABC_FREE( pAig->pReprs );
-    ABC_FREE( pAig->pNexts );
-    if ( Gia_ManRegNum(pAig) == 0 )
-    {
-        printf( "Cec_ManLatchCorrespondence(): Not a sequential AIG.\n" );
-        return 0;
-    }
-    Gia_ManRandom( 1 );
-    // derive initial state for resimulation
-    if ( pPars->nPrefix )
-//        pInitState = Cec_ManComputeInitState( pAig, 5+(1<<20)/Gia_ManAndNum(pAig) );
-        pInitState = Cec_ManComputeInitState( pAig, 100 );
-    // 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;
-    // create equivalence classes of registers
-    pSim = Cec_ManSimStart( pAig, pParsSim, pInitState );
-    Cec_ManSimClassesPrepare( pSim );
-    Cec_ManSimClassesRefine( pSim );
-    // prepare SAT solving
-    Cec_ManSatSetDefaultParams( pParsSat );
-    pParsSat->nBTLimit = pPars->nBTLimit;
-    pParsSat->fVerbose = pPars->fVerbose;
-    if ( pPars->fVerbose )
-    {
-        printf( "Obj = %7d. And = %7d. Conf = %5d. Fr = %d. Lcorr = %d. Ring = %d. CSat = %d.\n",
-            Gia_ManObjNum(pAig), Gia_ManAndNum(pAig), 
-            pPars->nBTLimit, pPars->nFrames, pPars->fLatchCorr, pPars->fUseRings, pPars->fUseCSat );
-        Cec_ManRefinedClassPrintStats( pAig, NULL, 0, clock() - clk );
-    }
-    // perform refinement of equivalence classes
-    for ( r = 0; r < nIterMax; r++ )
-    { 
-        clk = clock();
-        // perform speculative reduction
-        clk2 = clock();
-        pSrm = Gia_ManCorrSpecReduce( pAig, pPars->nFrames, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings );
-        assert( Gia_ManRegNum(pSrm) == 0 && Gia_ManPiNum(pSrm) == Gia_ManRegNum(pAig)+(pPars->nFrames+!pPars->fLatchCorr)*Gia_ManPiNum(pAig) );
-        clkSrm += clock() - clk2;
-        if ( Gia_ManCoNum(pSrm) == 0 )
-        {
-            Vec_IntFree( vOutputs );
-            Gia_ManStop( pSrm );            
-            break;
-        }
-//Gia_DumpAiger( pSrm, "corrsrm", r, 2 );
-        // found counter-examples to speculation
-        clk2 = clock();
-        if ( pPars->fUseCSat )
-            vCexStore = Cbs_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0 );
-        else
-            vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus );
-        Gia_ManStop( pSrm );
-        clkSat += clock() - clk2;
-        if ( Vec_IntSize(vCexStore) == 0 )
-        {
-            Vec_IntFree( vCexStore );
-            Vec_StrFree( vStatus );
-            Vec_IntFree( vOutputs );
-            break;
-        }
-        // refine classes with these counter-examples
-        clk2 = clock();
-        RetValue = Cec_ManResimulateCounterExamples( pSim, vCexStore, pPars->nFrames + 1 + nAddFrames, pInitState );
-        Vec_IntFree( vCexStore );
-        clkSim += clock() - clk2;
-        Gia_ManCheckRefinements( pAig, vStatus, vOutputs, pSim, pPars->fUseRings );
-        if ( pPars->fVerbose )
-            Cec_ManRefinedClassPrintStats( pAig, vStatus, r+1, clock() - clk );
-        Vec_StrFree( vStatus );
-        Vec_IntFree( vOutputs );
-//Gia_ManEquivPrintClasses( pAig, 1, 0 );
-    }
-    ABC_FREE( pInitState );
-    // check the base case
-    if ( (!pPars->fLatchCorr || pPars->nFrames > 1) || pPars->nPrefix )
-    {
-        int fChanges = 1;
-        while ( fChanges )
-        {
-            clock_t clkBmc = clock();
-            fChanges = 0;
-            pSrm = Gia_ManCorrSpecReduceInit( pAig, pPars->nFrames, pPars->nPrefix, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings );
-            if ( Gia_ManPoNum(pSrm) == 0 )
-            {
-                Gia_ManStop( pSrm );
-                Vec_IntFree( vOutputs );
-                break;
-            }
-            pParsSat->nBTLimit *= 10;
-            if ( pPars->nPrefix )
-            {
-                pParsSat->nBTLimit = 10000;
-                vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus );
-            }
-            else 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 + pPars->nPrefix, NULL );
-                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 );
-    }
-    // check the overflow
-    if ( r == nIterMax )
-        printf( "The refinement was not finished. The result may be incorrect.\n" );
-    Cec_ManSimStop( pSim );
-    clkTotal = clock() - clkTotal;
-    // report the results
-    if ( pPars->fVerbose )
-    {
-        ABC_PRTP( "Srm  ", clkSrm,                        clkTotal );
-        ABC_PRTP( "Sat  ", clkSat,                        clkTotal );
-        ABC_PRTP( "Sim  ", clkSim,                        clkTotal );
-        ABC_PRTP( "Other", clkTotal-clkSat-clkSrm-clkSim, clkTotal );
-        ABC_PRT( "TOTAL",  clkTotal );
-    }
-    return 1;
-}    
-
-/**Function*************************************************************
-
-  Synopsis    [Top-level procedure for register correspondence.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
-{  
-    Gia_Man_t * pNew, * pTemp;
-    int RetValue;
-    RetValue = Cec_ManLSCorrespondenceClasses( pAig, pPars );
-    // derive reduced AIG
-    if ( pPars->fMakeChoices )
-    {
-        pNew = Gia_ManEquivToChoices( pAig, 1 );
-        Gia_ManHasChoices( pNew );
-    }
-    else
-    {
-        Gia_ManEquivImprove( pAig );
-        pNew = Gia_ManCorrReduce( pAig );
-        pNew = Gia_ManSeqCleanup( pTemp = pNew );
-        Gia_ManStop( pTemp );
-        //Gia_WriteAiger( pNew, "reduced.aig", 0, 0 );
-    }
-    // report the results
-    if ( pPars->fVerbose )
-    {
-        printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%).  RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n", 
-            Gia_ManAndNum(pAig), Gia_ManAndNum(pNew), 
-            100.0*(Gia_ManAndNum(pAig)-Gia_ManAndNum(pNew))/(Gia_ManAndNum(pAig)?Gia_ManAndNum(pAig):1), 
-            Gia_ManRegNum(pAig), Gia_ManRegNum(pNew), 
-            100.0*(Gia_ManRegNum(pAig)-Gia_ManRegNum(pNew))/(Gia_ManRegNum(pAig)?Gia_ManRegNum(pAig):1) );
-    }
-    return pNew;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
-ABC_NAMESPACE_IMPL_END
-
diff --git a/src/proof/dch/dchChoice.c b/src/proof/dch/dchChoice.c
index 8fc8192f..783202e2 100644
--- a/src/proof/dch/dchChoice.c
+++ b/src/proof/dch/dchChoice.c
@@ -33,6 +33,36 @@ ABC_NAMESPACE_IMPL_START
 
 /**Function*************************************************************
 
+  Synopsis    [Counts support nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Dch_ObjCountSupp_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+    int Count;
+    if ( Aig_ObjIsTravIdCurrent( p, pObj ) )
+        return 0;
+    Aig_ObjSetTravIdCurrent( p, pObj );
+    if ( Aig_ObjIsCi(pObj) )
+        return 1;
+    assert( Aig_ObjIsNode(pObj) );
+    Count  = Dch_ObjCountSupp_rec( p, Aig_ObjFanin0(pObj) );
+    Count += Dch_ObjCountSupp_rec( p, Aig_ObjFanin1(pObj) );
+    return Count;
+}
+int Dch_ObjCountSupp( Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+    Aig_ManIncrementTravId( p );
+    return Dch_ObjCountSupp_rec( p, pObj );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Counts the number of representatives.]
 
   Description []
@@ -56,54 +86,72 @@ int Dch_DeriveChoiceCountReprs( Aig_Man_t * pAig )
     }
     return nReprs;
 }
+int Dch_DeriveChoiceCountEquivs( Aig_Man_t * pAig )
+{
+    Aig_Obj_t * pObj, * pEquiv;
+    int i, nEquivs = 0;
+    Aig_ManForEachObj( pAig, pObj, i )
+    {
+        pEquiv = Aig_ObjEquiv( pAig, pObj );
+        if ( pEquiv == NULL )
+            continue;
+        assert( pEquiv->Id > pObj->Id );
+        nEquivs++;
+    }
+    return nEquivs;
+}
 
 /**Function*************************************************************
 
-  Synopsis    [Counts the number of equivalences.]
+  Synopsis    [Marks the TFI of the node.]
 
-  Description []
+  Description [Returns 1 if there is a CI not marked with previous ID.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-int Dch_DeriveChoiceCountEquivs( Aig_Man_t * pAig )
+int Dch_ObjMarkTfi_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
 {
-    Aig_Obj_t * pObj, * pTemp, * pPrev;
-    int i, nEquivs = 0, Counter = 0;
-    Aig_ManForEachObj( pAig, pObj, i )
+    int RetValue;
+    if ( pObj == NULL )
+        return 0;
+    if ( Aig_ObjIsTravIdCurrent( p, pObj ) )
+        return 0;
+    if ( Aig_ObjIsCi(pObj) )
     {
-        if ( !Aig_ObjIsChoice(pAig, pObj) )
-            continue;
-        for ( pPrev = pObj, pTemp = Aig_ObjEquiv(pAig, pObj); pTemp; 
-              pPrev = pTemp, pTemp = Aig_ObjEquiv(pAig, pTemp) )
-        {
-            if ( pTemp->nRefs > 0 )
-            {
-                // remove referenced node from equivalence class
-                assert( pAig->pEquivs[pPrev->Id] == pTemp );
-                pAig->pEquivs[pPrev->Id] = pAig->pEquivs[pTemp->Id];
-                pAig->pEquivs[pTemp->Id] = NULL;
-                // how about the need to continue iterating over the list?
-                // pPrev = pTemp ???
-                Counter++;
-            }
-            nEquivs++;
-        }
+        RetValue = !Aig_ObjIsTravIdPrevious( p, pObj );
+        Aig_ObjSetTravIdCurrent( p, pObj );
+        return RetValue;
     }
-//    printf( "Removed %d classes.\n", Counter );
-
-    if ( Counter )
-        Dch_DeriveChoiceCountEquivs( pAig );
-//    if ( Counter )
-//    printf( "Removed %d equiv nodes because of non-zero ref counter.\n", Counter );
-    return nEquivs;
+    assert( Aig_ObjIsNode(pObj) );
+    Aig_ObjSetTravIdCurrent( p, pObj );
+    RetValue  = Dch_ObjMarkTfi_rec( p, Aig_ObjFanin0(pObj) );
+    RetValue += Dch_ObjMarkTfi_rec( p, Aig_ObjFanin1(pObj) );
+//    RetValue += Dch_ObjMarkTfi_rec( p, Aig_ObjEquiv(p, pObj) );
+    return (RetValue > 0);
+}
+int Dch_ObjCheckSuppRed( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr )
+{
+    // mark support of the representative node (pRepr)
+    Aig_ManIncrementTravId( p );
+    Dch_ObjMarkTfi_rec( p, pRepr );
+    // detect if the new node (pObj) depends on additional variables
+    Aig_ManIncrementTravId( p );
+    if ( Dch_ObjMarkTfi_rec( p, pObj ) )
+        return 1;//, printf( "1" );
+    // detect if the representative node (pRepr) depends on additional variables
+    Aig_ManIncrementTravId( p );
+    if ( Dch_ObjMarkTfi_rec( p, pRepr ) )
+        return 1;//, printf( "2" );
+    // skip the choice if this is what is happening
+    return 0;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Returns representatives of fanin in approapriate polarity.]
+  Synopsis    [Make sure reprsentative nodes do not have representatives.]
 
   Description []
                
@@ -112,19 +160,88 @@ int Dch_DeriveChoiceCountEquivs( Aig_Man_t * pAig )
   SeeAlso     []
 
 ***********************************************************************/
-static inline Aig_Obj_t * Aig_ObjGetRepr( Aig_Man_t * p, Aig_Obj_t * pObj )
+void Aig_ManCheckReprs( Aig_Man_t * p )
 {
-    Aig_Obj_t * pRepr;
-    if ( (pRepr = Aig_ObjRepr(p, Aig_Regular(pObj))) )
-        return Aig_NotCond( pRepr, Aig_Regular(pObj)->fPhase ^ pRepr->fPhase ^ Aig_IsComplement(pObj) );
-    return pObj;
+    int fPrintConst = 0;
+    Aig_Obj_t * pObj;
+    int i, fProb = 0;
+    int Class0 = 0, ClassCi = 0;
+    Aig_ManForEachObj( p, pObj, i )
+    {
+        if ( Aig_ObjRepr(p, pObj) == NULL )
+            continue;
+        if ( !Aig_ObjIsNode(pObj) )
+            printf( "Obj %d is not an AND but it has a repr %d.\n", i, Aig_ObjId(Aig_ObjRepr(p, pObj)) ), fProb = 1;
+        else if ( Aig_ObjRepr(p, Aig_ObjRepr(p, pObj)) )
+            printf( "Obj %d has repr %d with a repr %d.\n", i, Aig_ObjId(Aig_ObjRepr(p, pObj)), Aig_ObjId(Aig_ObjRepr(p, Aig_ObjRepr(p, pObj))) ), fProb = 1;
+    }
+    if ( !fProb )
+        printf( "Representive verification successful.\n" );
+    else
+        printf( "Representive verification FAILED.\n" );
+    if ( !fPrintConst )
+        return;
+    // count how many representatives are const0 or a CI
+    Aig_ManForEachObj( p, pObj, i )
+    {
+        if ( Aig_ObjRepr(p, pObj) == Aig_ManConst1(p) )
+            Class0++;
+        if ( Aig_ObjRepr(p, pObj) && Aig_ObjIsCi(Aig_ObjRepr(p, pObj)) )
+            ClassCi++;
+    }
+    printf( "Const0 nodes = %d.  ConstCI nodes = %d.\n", Class0, ClassCi );
 }
 
-static inline Aig_Obj_t * Aig_ObjChild0CopyRepr( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_ObjGetRepr( p, Aig_ObjChild0Copy(pObj) ); }
-static inline Aig_Obj_t * Aig_ObjChild1CopyRepr( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_ObjGetRepr( p, Aig_ObjChild1Copy(pObj) ); }
+/**Function*************************************************************
 
+  Synopsis    [Verify correctness of choices.]
 
+  Description []
+               
+  SideEffects []
 
+  SeeAlso     []
+
+***********************************************************************/
+void Dch_CheckChoices( Aig_Man_t * p, int fSkipRedSupps )
+{
+    Aig_Obj_t * pObj;
+    int i, fProb = 0;
+    Aig_ManCleanMarkA( p );
+    Aig_ManForEachNode( p, pObj, i )
+    {
+        if ( p->pEquivs[i] != NULL )
+        {
+            if ( pObj->fMarkA == 1 )
+                printf( "node %d participates in more than one choice class\n", i ), fProb = 1;
+            pObj->fMarkA = 1;
+            // check redundancy
+            if ( fSkipRedSupps && Dch_ObjCheckSuppRed( p, pObj, p->pEquivs[i]) )
+                printf( "node %d and repr %d have diff supports\n", pObj->Id, p->pEquivs[i]->Id );
+            // consider the next one
+            pObj = p->pEquivs[i];
+            if ( p->pEquivs[Aig_ObjId(pObj)] == NULL )
+            {
+                if ( pObj->fMarkA == 1 )
+                    printf( "repr %d has final node %d participates in more than one choice class\n", i, pObj->Id ), fProb = 1;
+                pObj->fMarkA = 1;
+            }
+            // consider the non-head ones
+            if ( pObj->nRefs > 0 )
+                printf( "node %d belonging to choice has fanout %d\n", pObj->Id, pObj->nRefs );
+        }
+        if ( p->pReprs && p->pReprs[i] != NULL )
+        {
+            if ( pObj->nRefs > 0 )
+                printf( "node %d has representative %d and fanout count %d\n", pObj->Id, p->pReprs[i]->Id, pObj->nRefs ), fProb = 1;
+        }
+    }
+    Aig_ManCleanMarkA( p );
+    if ( !fProb )
+        printf( "Verification of choice AIG succeeded.\n" );
+    else
+        printf( "Verification of choice AIG FAILED.\n" );
+}
 
 /**Function*************************************************************
 
@@ -240,104 +357,6 @@ int Aig_ManCheckAcyclic( Aig_Man_t * p, int fVerbose )
     return fAcyclic;
 }
 
-/**Function*************************************************************
-
-  Synopsis    [Removes combinational loop.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_ManFixLoopProblem( Aig_Man_t * p, int fVerbose )
-{
-    Aig_Obj_t * pObj;
-    int i, Counter = 0, Counter2 = 0;
-    Aig_ManForEachObj( p, pObj, i )
-    {
-        if ( !Aig_ObjIsTravIdCurrent(p, pObj) )
-            continue;
-        Counter2++;
-        if ( Aig_ObjRepr(p, pObj) == NULL && Aig_ObjEquiv(p, pObj) != NULL )
-        {
-            Aig_ObjSetEquiv(p, pObj, NULL);
-            Counter++;
-        }
-    }
-    if ( fVerbose )
-    Abc_Print( 1, "Fixed %d choice nodes on the path with %d objects.\n", Counter, Counter2 );
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Verify correctness of choices.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Dch_CheckChoices( Aig_Man_t * p )
-{
-    Aig_Obj_t * pObj;
-    int i, fProb = 0;
-    Aig_ManCleanMarkA( p );
-    Aig_ManForEachNode( p, pObj, i )
-        if ( p->pEquivs[i] != NULL )
-        {
-            if ( pObj->fMarkA == 1 )
-                printf( "node %d participates in more than one choice class\n", i ), fProb = 1;
-            pObj->fMarkA = 1;
-            // consider the last one
-            pObj = p->pEquivs[i];
-            if ( p->pEquivs[Aig_ObjId(pObj)] == NULL )
-            {
-                if ( pObj->fMarkA == 1 )
-                    printf( "repr %d has final node %d participates in more than one choice class\n", i, pObj->Id ), fProb = 1;
-                pObj->fMarkA = 1;
-            }
-        }
-    Aig_ManCleanMarkA( p );
-    if ( !fProb )
-        printf( "Verification of choice AIG succeeded.\n" );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Marks the TFI of the node.]
-
-  Description [Returns 1 if there is a CI not marked with previous ID.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Dch_ObjMarkTfi_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
-{
-    int RetValue;
-    if ( pObj == NULL )
-        return 0;
-    if ( Aig_ObjIsTravIdCurrent( p, pObj ) )
-        return 0;
-    if ( Aig_ObjIsCi(pObj) )
-    {
-        RetValue = !Aig_ObjIsTravIdPrevious( p, pObj );
-        Aig_ObjSetTravIdCurrent( p, pObj );
-        return RetValue;
-    }
-    assert( Aig_ObjIsNode(pObj) );
-    Aig_ObjSetTravIdCurrent( p, pObj );
-    RetValue  = Dch_ObjMarkTfi_rec( p, Aig_ObjFanin0(pObj) );
-    RetValue += Dch_ObjMarkTfi_rec( p, Aig_ObjFanin1(pObj) );
-//    RetValue += Dch_ObjMarkTfi_rec( p, Aig_ObjEquiv(p, pObj) );
-    return (RetValue > 0);
-}
 
 /**Function*************************************************************
 
@@ -391,6 +410,27 @@ int Dch_ObjCheckTfi( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr )
 
 /**Function*************************************************************
 
+  Synopsis    [Returns representatives of fanin in approapriate polarity.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Aig_Obj_t * Aig_ObjGetRepr( Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+    Aig_Obj_t * pRepr;
+    if ( (pRepr = Aig_ObjRepr(p, Aig_Regular(pObj))) )
+        return Aig_NotCond( pRepr, Aig_Regular(pObj)->fPhase ^ pRepr->fPhase ^ Aig_IsComplement(pObj) );
+    return pObj;
+}
+static inline Aig_Obj_t * Aig_ObjChild0CopyRepr( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_ObjGetRepr( p, Aig_ObjChild0Copy(pObj) ); }
+static inline Aig_Obj_t * Aig_ObjChild1CopyRepr( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_ObjGetRepr( p, Aig_ObjChild1Copy(pObj) ); }
+
+/**Function*************************************************************
+
   Synopsis    [Derives the AIG with choices from representatives.]
 
   Description []
@@ -403,22 +443,34 @@ int Dch_ObjCheckTfi( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr )
 void Dch_DeriveChoiceAigNode( Aig_Man_t * pAigNew, Aig_Man_t * pAigOld, Aig_Obj_t * pObj, int fSkipRedSupps )
 {
     Aig_Obj_t * pRepr, * pObjNew, * pReprNew;
+    assert( !Aig_IsComplement(pObj) );
+    // get the representative
+    pRepr = Aig_ObjRepr( pAigOld, pObj );
+    if ( pRepr != NULL && (Aig_ObjIsConst1(pRepr) || Aig_ObjIsCi(pRepr)) )
+    {
+        assert( pRepr->pData != NULL );
+        pObj->pData = Aig_NotCond( (Aig_Obj_t *)pRepr->pData, pObj->fPhase ^ pRepr->fPhase );
+        return;
+    }
     // get the new node
-    assert( pObj->pData == NULL );
-    pObj->pData = Aig_And( pAigNew, 
+    pObjNew = Aig_And( pAigNew, 
         Aig_ObjChild0CopyRepr(pAigNew, pObj), 
         Aig_ObjChild1CopyRepr(pAigNew, pObj) );
-    pRepr = Aig_ObjRepr( pAigOld, pObj );
+    pObjNew = Aig_ObjGetRepr( pAigNew, pObjNew );
+    assert( Aig_ObjRepr( pAigNew, pObjNew ) == NULL );
+    // assign the copy
+    assert( pObj->pData == NULL );
+    pObj->pData = pObjNew;
+    // skip those without reprs
     if ( pRepr == NULL )
         return;
     assert( pRepr->Id < pObj->Id );
+    assert( Aig_ObjIsNode(pRepr) );
     // get the corresponding new nodes
     pObjNew  = Aig_Regular((Aig_Obj_t *)pObj->pData);
     pReprNew = Aig_Regular((Aig_Obj_t *)pRepr->pData);
-    if ( pObjNew == pReprNew )
-        return;
-    // skip the earlier nodes
-    if ( pReprNew->Id > pObjNew->Id )
+    // skip earlier nodes
+    if ( pReprNew->Id >= pObjNew->Id )
         return;
     assert( pReprNew->Id < pObjNew->Id );
     // set the representatives
@@ -427,33 +479,16 @@ void Dch_DeriveChoiceAigNode( Aig_Man_t * pAigNew, Aig_Man_t * pAigOld, Aig_Obj_
     if ( pObjNew->nRefs > 0 )
         return;
     assert( pObjNew->nRefs == 0 );
-    // update new nodes of the object
-    if ( !Aig_ObjIsNode(pRepr) )
-        return;
-    // skip choices with combinational loops
+    // skip choices that can lead to combo loops
     if ( Dch_ObjCheckTfi( pAigNew, pObjNew, pReprNew ) )
         return;
     // don't add choice if structural support of pObjNew and pReprNew differ
-    if ( fSkipRedSupps )
-    {
-        int fSkipChoice = 0;
-        // mark support of the representative node (pReprNew)
-        Aig_ManIncrementTravId( pAigNew );
-        Dch_ObjMarkTfi_rec( pAigNew, pReprNew );
-        // detect if the new node (pObjNew) depends on any additional variables
-        Aig_ManIncrementTravId( pAigNew );
-        if ( Dch_ObjMarkTfi_rec( pAigNew, pObjNew ) )
-            fSkipChoice = 1;//, printf( "1" );
-        // detect if the representative node (pReprNew) depends on any additional variables
-        Aig_ManIncrementTravId( pAigNew );
-        if ( Dch_ObjMarkTfi_rec( pAigNew, pReprNew ) )
-            fSkipChoice = 1;//, printf( "2" );
-        // skip the choice if this is what is happening
-        if ( fSkipChoice )
-            return;
-    }
-    // add choice
-    pAigNew->pEquivs[pObjNew->Id]  = pAigNew->pEquivs[pReprNew->Id];
+    if ( fSkipRedSupps && Dch_ObjCheckSuppRed(pAigNew, pObjNew, pReprNew) )
+        return;
+    // add choice to the end of the list
+    while ( pAigNew->pEquivs[pReprNew->Id] != NULL )
+        pReprNew = pAigNew->pEquivs[pReprNew->Id];
+    assert( pAigNew->pEquivs[pReprNew->Id] == NULL );
     pAigNew->pEquivs[pReprNew->Id] = pObjNew;
 }
 Aig_Man_t * Dch_DeriveChoiceAigInt( Aig_Man_t * pAig, int fSkipRedSupps )
@@ -461,10 +496,6 @@ Aig_Man_t * Dch_DeriveChoiceAigInt( Aig_Man_t * pAig, int fSkipRedSupps )
     Aig_Man_t * pChoices;
     Aig_Obj_t * pObj;
     int i;
-    // make sure reprsentative nodes do not have representatives
-    Aig_ManForEachNode( pAig, pObj, i )
-        if ( pAig->pReprs[i] != NULL && pAig->pReprs[pAig->pReprs[i]->Id] != NULL )
-            printf( "Node %d: repr %d has repr %d.\n", i, Aig_ObjId(pAig->pReprs[i]), Aig_ObjId(pAig->pReprs[pAig->pReprs[i]->Id]) );
     // start recording equivalences
     pChoices = Aig_ManStart( Aig_ManObjNumMax(pAig) );
     pChoices->pEquivs = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) );
@@ -476,45 +507,32 @@ Aig_Man_t * Dch_DeriveChoiceAigInt( Aig_Man_t * pAig, int fSkipRedSupps )
         pObj->pData = Aig_ObjCreateCi( pChoices );
     // construct choices for the internal nodes
     assert( pAig->pReprs != NULL );
-    Aig_ManForEachNode( pAig, pObj, i )
+    Aig_ManForEachNode( pAig, pObj, i ) 
         Dch_DeriveChoiceAigNode( pChoices, pAig, pObj, fSkipRedSupps );
     Aig_ManForEachCo( pAig, pObj, i )
         Aig_ObjCreateCo( pChoices, Aig_ObjChild0CopyRepr(pChoices, pObj) );
-    Dch_DeriveChoiceCountEquivs( pChoices );
     Aig_ManSetRegNum( pChoices, Aig_ManRegNum(pAig) );
-//Dch_CheckChoices( pChoices );
     return pChoices;
 }
-
-/**Function*************************************************************
-
-  Synopsis    [Derives the AIG with choices from representatives.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
 Aig_Man_t * Dch_DeriveChoiceAig( Aig_Man_t * pAig, int fSkipRedSupps )
 {
-    extern int Aig_ManCheckAcyclic( Aig_Man_t * pAig, int fVerbose );
+    int fCheck = 0;
     Aig_Man_t * pChoices, * pTemp;
-    int fVerbose = 0;
+    // verify
+    if ( fCheck )
+        Aig_ManCheckReprs( pAig ); 
+    // compute choices
     pChoices = Dch_DeriveChoiceAigInt( pAig, fSkipRedSupps );
-//    pChoices = Dch_DeriveChoiceAigInt( pTemp = pChoices );
-//    Aig_ManStop( pTemp );
-    // there is no need for cleanup
     ABC_FREE( pChoices->pReprs );
-    while ( !Aig_ManCheckAcyclic( pChoices, fVerbose ) )
-    {
-        if ( fVerbose )
-        Abc_Print( 1, "There is a loop!\n" );
-        Aig_ManFixLoopProblem( pChoices, fVerbose );
-    }
+    // verify
+    if ( fCheck )
+        Dch_CheckChoices( pChoices, fSkipRedSupps ); 
+    // find correct topo order with choices
     pChoices = Aig_ManDupDfs( pTemp = pChoices );
     Aig_ManStop( pTemp );
+    // verify
+    if ( fCheck )
+        Dch_CheckChoices( pChoices, fSkipRedSupps ); 
     return pChoices;
 }
 
diff --git a/src/proof/dch/dchCore.c b/src/proof/dch/dchCore.c
index 654ed359..da103e0e 100644
--- a/src/proof/dch/dchCore.c
+++ b/src/proof/dch/dchCore.c
@@ -106,19 +106,13 @@ p->timeSimInit = clock() - clk;
     // free memory ahead of time
 p->timeTotal = clock() - clkTotal;
     Dch_ManStop( p );
-    // try something different
-    {
-//    extern void Gia_ManNormalizeChoicesTest( Aig_Man_t * pAig );
-//    Gia_ManNormalizeChoicesTest( pAig );
-    }
-
     // create choices
     ABC_FREE( pAig->pTable );
     pResult = Dch_DeriveChoiceAig( pAig, pPars->fSkipRedSupp );
     // count the number of representatives
     if ( pPars->fVerbose ) 
         Abc_Print( 1, "STATS:  Reprs = %6d.  Equivs = %6d.  Choices = %6d.\n", 
-               Dch_DeriveChoiceCountReprs( pAig ),
+               Dch_DeriveChoiceCountReprs( pResult ),
                Dch_DeriveChoiceCountEquivs( pResult ),
                Aig_ManChoiceNum( pResult ) );
     return pResult;