Version abc90410

27 files changed, 1112 insertions, 132 deletions

diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 1750a7b7..38ba167f 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -514,10 +514,10 @@ extern void            Aig_ManStopMemory( Aig_Man_t * p );
 /*=== aigMffc.c ==========================================================*/
 extern int             Aig_NodeRef_rec( Aig_Obj_t * pNode, unsigned LevelMin );
 extern int             Aig_NodeDeref_rec( Aig_Obj_t * pNode, unsigned LevelMin, float * pPower, float * pProbs );
-extern int             Aig_NodeMffsSupp( Aig_Man_t * p, Aig_Obj_t * pNode, int LevelMin, Vec_Ptr_t * vSupp );
-extern int             Aig_NodeMffsLabel( Aig_Man_t * p, Aig_Obj_t * pNode, float * pPower );
-extern int             Aig_NodeMffsLabelCut( Aig_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vLeaves );
-extern int             Aig_NodeMffsExtendCut( Aig_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vResult );
+extern int             Aig_NodeMffcSupp( Aig_Man_t * p, Aig_Obj_t * pNode, int LevelMin, Vec_Ptr_t * vSupp );
+extern int             Aig_NodeMffcLabel( Aig_Man_t * p, Aig_Obj_t * pNode, float * pPower );
+extern int             Aig_NodeMffcLabelCut( Aig_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vLeaves );
+extern int             Aig_NodeMffcExtendCut( Aig_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vResult );
 /*=== aigObj.c ==========================================================*/
 extern Aig_Obj_t *     Aig_ObjCreatePi( Aig_Man_t * p );
 extern Aig_Obj_t *     Aig_ObjCreatePo( Aig_Man_t * p, Aig_Obj_t * pDriver );
diff --git a/src/aig/aig/aigDup.c b/src/aig/aig/aigDup.c
index febe8a0c..eeaf4c91 100644
--- a/src/aig/aig/aigDup.c
+++ b/src/aig/aig/aigDup.c
@@ -476,15 +476,9 @@ Aig_Man_t * Aig_ManDupDfs( Aig_Man_t * p )
         pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
     // duplicate representation of choice nodes
     if ( p->pEquivs )
-    {
-        pNew->pEquivs = ABC_ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p) );
-        memset( pNew->pEquivs, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p) );
-    }
+        pNew->pEquivs = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p) );
     if ( p->pReprs )
-    {
-        pNew->pReprs = ABC_ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p) );
-        memset( pNew->pReprs, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p) );
-    }
+        pNew->pReprs = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p) );
     // create the PIs
     Aig_ManCleanData( p );
     // duplicate internal nodes
diff --git a/src/aig/aig/aigMffc.c b/src/aig/aig/aigMffc.c
index 2c648382..b902e609 100644
--- a/src/aig/aig/aigMffc.c
+++ b/src/aig/aig/aigMffc.c
@@ -144,7 +144,7 @@ int Aig_NodeRefLabel_rec( Aig_Man_t * p, Aig_Obj_t * pNode, unsigned LevelMin )
   SeeAlso     []
 
 ***********************************************************************/
-void Aig_NodeMffsSupp_rec( Aig_Man_t * p, Aig_Obj_t * pNode, unsigned LevelMin, Vec_Ptr_t * vSupp, int fTopmost, Aig_Obj_t * pObjSkip )
+void Aig_NodeMffcSupp_rec( Aig_Man_t * p, Aig_Obj_t * pNode, unsigned LevelMin, Vec_Ptr_t * vSupp, int fTopmost, Aig_Obj_t * pObjSkip )
 {
     // skip visited nodes
     if ( Aig_ObjIsTravIdCurrent(p, pNode) )
@@ -158,8 +158,8 @@ void Aig_NodeMffsSupp_rec( Aig_Man_t * p, Aig_Obj_t * pNode, unsigned LevelMin,
     }
     assert( Aig_ObjIsNode(pNode) );
     // recur on the children
-    Aig_NodeMffsSupp_rec( p, Aig_ObjFanin0(pNode), LevelMin, vSupp, 0, pObjSkip );
-    Aig_NodeMffsSupp_rec( p, Aig_ObjFanin1(pNode), LevelMin, vSupp, 0, pObjSkip );
+    Aig_NodeMffcSupp_rec( p, Aig_ObjFanin0(pNode), LevelMin, vSupp, 0, pObjSkip );
+    Aig_NodeMffcSupp_rec( p, Aig_ObjFanin1(pNode), LevelMin, vSupp, 0, pObjSkip );
 }
 
 /**Function*************************************************************
@@ -173,7 +173,7 @@ void Aig_NodeMffsSupp_rec( Aig_Man_t * p, Aig_Obj_t * pNode, unsigned LevelMin,
   SeeAlso     []
 
 ***********************************************************************/
-int Aig_NodeMffsSupp( Aig_Man_t * p, Aig_Obj_t * pNode, int LevelMin, Vec_Ptr_t * vSupp )
+int Aig_NodeMffcSupp( Aig_Man_t * p, Aig_Obj_t * pNode, int LevelMin, Vec_Ptr_t * vSupp )
 {
     int ConeSize1, ConeSize2;
     if ( vSupp ) Vec_PtrClear( vSupp );
@@ -187,7 +187,7 @@ int Aig_NodeMffsSupp( Aig_Man_t * p, Aig_Obj_t * pNode, int LevelMin, Vec_Ptr_t
     assert( Aig_ObjIsNode(pNode) );
     Aig_ManIncrementTravId( p );
     ConeSize1 = Aig_NodeDeref_rec( pNode, LevelMin, NULL, NULL );
-    Aig_NodeMffsSupp_rec( p, pNode, LevelMin, vSupp, 1, NULL );
+    Aig_NodeMffcSupp_rec( p, pNode, LevelMin, vSupp, 1, NULL );
     ConeSize2 = Aig_NodeRef_rec( pNode, LevelMin );
     assert( ConeSize1 == ConeSize2 );
     assert( ConeSize1 > 0 );
@@ -205,7 +205,7 @@ int Aig_NodeMffsSupp( Aig_Man_t * p, Aig_Obj_t * pNode, int LevelMin, Vec_Ptr_t
   SeeAlso     []
 
 ***********************************************************************/
-int Aig_NodeMffsLabel( Aig_Man_t * p, Aig_Obj_t * pNode, float * pPower )
+int Aig_NodeMffcLabel( Aig_Man_t * p, Aig_Obj_t * pNode, float * pPower )
 {
     int ConeSize1, ConeSize2;
     assert( (pPower != NULL) == (p->vProbs != NULL) );
@@ -230,7 +230,7 @@ int Aig_NodeMffsLabel( Aig_Man_t * p, Aig_Obj_t * pNode, float * pPower )
   SeeAlso     []
 
 ***********************************************************************/
-int Aig_NodeMffsLabelCut( Aig_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vLeaves )
+int Aig_NodeMffcLabelCut( Aig_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vLeaves )
 {
     Aig_Obj_t * pObj;
     int i, ConeSize1, ConeSize2;
@@ -259,7 +259,7 @@ int Aig_NodeMffsLabelCut( Aig_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vLeaves
   SeeAlso     []
 
 ***********************************************************************/
-int Aig_NodeMffsExtendCut( Aig_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vResult )
+int Aig_NodeMffcExtendCut( Aig_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vResult )
 {
     Aig_Obj_t * pObj, * pLeafBest;
     int i, LevelMax, ConeSize1, ConeSize2, ConeCur1, ConeCur2, ConeBest;
@@ -294,7 +294,7 @@ int Aig_NodeMffsExtendCut( Aig_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vLeaves
     // collect the cut nodes
     Vec_PtrClear( vResult );
     Aig_ManIncrementTravId( p );
-    Aig_NodeMffsSupp_rec( p, pNode, 0, vResult, 1, pLeafBest );
+    Aig_NodeMffcSupp_rec( p, pNode, 0, vResult, 1, pLeafBest );
     // ref the nodes
     ConeCur2 = Aig_NodeRef_rec( pLeafBest, 0 );
     assert( ConeCur1 == ConeCur2 );
diff --git a/src/aig/aig/aigPart.c b/src/aig/aig/aigPart.c
index 1fd85768..6e0cb3e8 100644
--- a/src/aig/aig/aigPart.c
+++ b/src/aig/aig/aigPart.c
@@ -1520,7 +1520,7 @@ void Aig_ManChoiceEval( Aig_Man_t * p )
         printf( "Choice node = %5d. Level = %2d. Choices = %d. { ", pNode->Id, pNode->Level, Counter );
         for ( pTemp = pNode; pTemp; pTemp = Aig_ObjEquiv(p, pTemp) )
         {
-            Counter = Aig_NodeMffsSupp( p, pTemp, 0, vSupp );
+            Counter = Aig_NodeMffcSupp( p, pTemp, 0, vSupp );
             printf( "S=%d N=%d L=%d  ", Vec_PtrSize(vSupp), Counter, pTemp->Level );
         }
         printf( "}\n" );
diff --git a/src/aig/cec/cec.h b/src/aig/cec/cec.h
index a965730f..5cb8d345 100644
--- a/src/aig/cec/cec.h
+++ b/src/aig/cec/cec.h
@@ -125,6 +125,7 @@ struct Cec_ParCor_t_
     int              nBTLimit;      // conflict limit at a node
     int              fLatchCorr;    // consider only latch outputs
     int              fUseRings;     // use rings
+    int              fMakeChoices;  // use equilvaences as choices
     int              fUseCSat;      // use circuit-based solver
     int              fFirstStop;    // stop on the first sat output
     int              fUseSmartCnf;  // use smart CNF computation
@@ -139,8 +140,8 @@ struct Cec_ParChc_t_
     int              nWords;        // the number of simulation words
     int              nRounds;       // the number of simulation rounds
     int              nBTLimit;      // conflict limit at a node
-    int              fFirstStop;    // stop on the first sat output
-    int              fUseSmartCnf;  // use smart CNF computation
+    int              fUseRings;     // use rings
+    int              fUseCSat;      // use circuit-based solver
     int              fVeryVerbose;  // verbose stats
     int              fVerbose;      // verbose stats
 };
diff --git a/src/aig/cec/cecCec.c b/src/aig/cec/cecCec.c
index ee9f6d3c..7ec3dad4 100644
--- a/src/aig/cec/cecCec.c
+++ b/src/aig/cec/cecCec.c
@@ -70,7 +70,7 @@ int Cec_ManVerifyOld( Gia_Man_t * pMiter, int fVerbose )
     extern int Fra_FraigCec( Aig_Man_t ** ppAig, int nConfLimit, int fVerbose );
     extern int Ssw_SecCexResimulate( Aig_Man_t * p, int * pModel, int * pnOutputs );
     Gia_Man_t * pTemp = Gia_ManTransformMiter( pMiter );
-    Aig_Man_t * pMiterCec = Gia_ManToAig( pTemp );
+    Aig_Man_t * pMiterCec = Gia_ManToAig( pTemp, 0 );
     int RetValue, iOut, nOuts, clkTotal = clock();
     Gia_ManStop( pTemp );
     // run CEC on this miter
diff --git a/src/aig/cec/cecChoice.c b/src/aig/cec/cecChoice.c
index 2a619e39..0662d73d 100644
--- a/src/aig/cec/cecChoice.c
+++ b/src/aig/cec/cecChoice.c
@@ -19,17 +19,172 @@
 ***********************************************************************/
 
 #include "cecInt.h"
+#include "giaAig.h"
+#include "dch.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+static void Cec_ManCombSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj );
+
+extern int Cec_ManResimulateCounterExamplesComb( Cec_ManSim_t * pSim, Vec_Int_t * vCexStore );
+extern int Gia_ManCheckRefinements( Gia_Man_t * p, Vec_Str_t * vStatus, Vec_Int_t * vOutputs, Cec_ManSim_t * pSim, int fRings );
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
+  Synopsis    [Computes the real value of the literal w/o spec reduction.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Cec_ManCombSpecReal( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
+{
+    assert( Gia_ObjIsAnd(pObj) );
+    Cec_ManCombSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj) );
+    Cec_ManCombSpecReduce_rec( pNew, p, Gia_ObjFanin1(pObj) );
+    return Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Recursively performs speculative reduction for the object.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_ManCombSpecReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
+{
+    Gia_Obj_t * pRepr;
+    if ( ~pObj->Value )
+        return;
+    if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) )
+    {
+        Cec_ManCombSpecReduce_rec( pNew, p, pRepr );
+        pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );
+        return;
+    }
+    pObj->Value = Cec_ManCombSpecReal( pNew, p, pObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives SRM for signal correspondence.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Cec_ManCombSpecReduce( Gia_Man_t * p, Vec_Int_t ** pvOutputs, int fRings )
+{
+    Gia_Man_t * pNew, * pTemp;
+    Gia_Obj_t * pObj, * pRepr;
+    Vec_Int_t * vXorLits;
+    int i, iPrev, iObj, iPrevNew, iObjNew;
+    assert( p->pReprs != NULL );
+    Gia_ManSetPhase( p );
+    Gia_ManFillValue( p );
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Gia_UtilStrsav( p->pName );
+    Gia_ManHashAlloc( pNew );
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManForEachCi( p, pObj, i )
+        pObj->Value = Gia_ManAppendCi(pNew);
+    *pvOutputs = Vec_IntAlloc( 1000 );
+    vXorLits = Vec_IntAlloc( 1000 );
+    if ( fRings )
+    {
+        Gia_ManForEachObj1( p, pObj, i )
+        {
+            if ( Gia_ObjIsConst( p, i ) )
+            {
+                iObjNew = Cec_ManCombSpecReal( pNew, p, pObj );
+                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 = Cec_ManCombSpecReal( pNew, p, Gia_ManObj(p, iPrev) );
+                    iObjNew  = Cec_ManCombSpecReal( pNew, p, Gia_ManObj(p, iObj) );
+                    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 = Cec_ManCombSpecReal( pNew, p, Gia_ManObj(p, iPrev) );
+                iObjNew  = Cec_ManCombSpecReal( pNew, p, Gia_ManObj(p, iObj) );
+                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 : Cec_ManCombSpecReal( pNew, p, pRepr );
+            iObjNew  = Cec_ManCombSpecReal( pNew, p, pObj );
+            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 );
+//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    []
 
   Description []
@@ -39,9 +194,293 @@
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Cec_ManChoiceComputation( Gia_Man_t * pAig, Cec_ParChc_t * pPars )
+int Cec_ManChoiceComputation_int( Gia_Man_t * pAig, Cec_ParChc_t * pPars )
+{
+    int nItersMax = 1000;
+    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;
+    int r, RetValue;
+    int clkSat = 0, clkSim = 0, clkSrm = 0, clkTotal = clock();
+    int clk2, clk = clock();
+    ABC_FREE( pAig->pReprs );
+    ABC_FREE( pAig->pNexts );
+    Gia_ManRandom( 1 );
+    // prepare simulation manager
+    Cec_ManSimSetDefaultParams( pParsSim );
+    pParsSim->nWords     = pPars->nWords;
+    pParsSim->nRounds    = pPars->nRounds;
+    pParsSim->fVerbose   = pPars->fVerbose;
+    pParsSim->fLatchCorr   = 0;
+    pParsSim->fSeqSimulate = 0;
+    // create equivalence classes of registers
+    pSim = Cec_ManSimStart( pAig, pParsSim );
+    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. Ring = %d. CSat = %d.\n",
+            Gia_ManObjNum(pAig), Gia_ManAndNum(pAig), pPars->nBTLimit, pPars->fUseRings, pPars->fUseCSat );
+        Cec_ManRefinedClassPrintStats( pAig, NULL, 0, clock() - clk );
+    }
+    // perform refinement of equivalence classes
+    for ( r = 0; r < nItersMax; r++ )
+    { 
+        clk = clock();
+        // perform speculative reduction
+        clk2 = clock();
+        pSrm = Cec_ManCombSpecReduce( pAig, &vOutputs, pPars->fUseRings );
+        assert( Gia_ManRegNum(pSrm) == 0 && Gia_ManCiNum(pSrm) == Gia_ManCiNum(pAig) );
+        clkSrm += clock() - clk2;
+        if ( Gia_ManCoNum(pSrm) == 0 )
+        {
+            if ( pPars->fVerbose )
+                Cec_ManRefinedClassPrintStats( pAig, NULL, r+1, clock() - clk );
+            Vec_IntFree( vOutputs );
+            Gia_ManStop( pSrm );            
+            break;
+        }
+//Gia_DumpAiger( pSrm, "choicesrm", 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 )
+        {
+            if ( pPars->fVerbose )
+                Cec_ManRefinedClassPrintStats( pAig, vStatus, r+1, clock() - clk );
+            Vec_IntFree( vCexStore );
+            Vec_StrFree( vStatus );
+            Vec_IntFree( vOutputs );
+            break;
+        }
+        // refine classes with these counter-examples
+        clk2 = clock();
+        RetValue = Cec_ManResimulateCounterExamplesComb( pSim, vCexStore );
+        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 );
+    }
+    // check the overflow
+    if ( r == nItersMax )
+        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 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates the AIG in the DFS order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManChoiceMiter_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
+{
+    if ( ~pObj->Value )
+        return pObj->Value;
+    Gia_ManChoiceMiter_rec( pNew, p, Gia_ObjFanin0(pObj) );
+    if ( Gia_ObjIsCo(pObj) )
+        return pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    Gia_ManChoiceMiter_rec( pNew, p, Gia_ObjFanin1(pObj) );
+    return pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+} 
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the miter of several AIGs for choice computation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManChoiceMiter( Vec_Ptr_t * vGias )
+{
+    Gia_Man_t * pNew, * pGia, * pGia0;
+    int i, k, iNode, nNodes;
+    // make sure they have equal parameters
+    assert( Vec_PtrSize(vGias) > 0 );
+    pGia0 = Vec_PtrEntry( vGias, 0 );
+    Vec_PtrForEachEntry( vGias, pGia, i )
+    {
+        assert( Gia_ManCiNum(pGia)  == Gia_ManCiNum(pGia0) );
+        assert( Gia_ManCoNum(pGia)  == Gia_ManCoNum(pGia0) );
+        assert( Gia_ManRegNum(pGia) == Gia_ManRegNum(pGia0) );
+        Gia_ManFillValue( pGia );
+        Gia_ManConst0(pGia)->Value = 0;
+    }
+    // start the new manager
+    pNew = Gia_ManStart( Vec_PtrSize(vGias) * Gia_ManObjNum(pGia0) );
+    pNew->pName = Gia_UtilStrsav( pGia0->pName );
+    // create new CIs and assign them to the old manager CIs
+    for ( k = 0; k < Gia_ManCiNum(pGia0); k++ )
+    {
+        iNode = Gia_ManAppendCi(pNew);
+        Vec_PtrForEachEntry( vGias, pGia, i )
+            Gia_ManCi( pGia, k )->Value = iNode; 
+    }
+    // create internal nodes
+    Gia_ManHashAlloc( pNew );
+    for ( k = 0; k < Gia_ManCoNum(pGia0); k++ )
+    {
+        Vec_PtrForEachEntry( vGias, pGia, i )
+            Gia_ManChoiceMiter_rec( pNew, pGia, Gia_ManCo( pGia, k ) );
+    }
+    Gia_ManHashStop( pNew );
+    // check the presence of dangling nodes
+    nNodes = Gia_ManHasDandling( pNew );
+    assert( nNodes == 0 );
+    // finalize
+//    Gia_ManSetRegNum( pNew, Gia_ManRegNum(pGia0) );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes choices for the vector of AIGs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Cec_ManChoiceComputationVec( Vec_Ptr_t * vGias, Cec_ParChc_t * pPars )
+{
+    Gia_Man_t * pMiter, * pNew;
+    int RetValue;
+    // compute equivalences of the miter
+    pMiter = Gia_ManChoiceMiter( vGias );
+    RetValue = Cec_ManChoiceComputation_int( pMiter, pPars );
+    // derive AIG with choices
+    pNew = Gia_ManEquivToChoices( pMiter, Vec_PtrSize(vGias) );
+    Gia_ManHasChoices( pNew );
+    Gia_ManStop( pMiter );
+    // 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;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes choices for one AIGs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Cec_ManChoiceComputation( Gia_Man_t * pAig, Cec_ParChc_t * pParsChc )
+{
+    extern Aig_Man_t * Dar_ManChoiceNew( Aig_Man_t * pAig, Dch_Pars_t * pPars );
+    Dch_Pars_t Pars, * pPars = &Pars;
+    Aig_Man_t * pMan, * pManNew;
+    Gia_Man_t * pGia;
+    if ( 0 ) 
+    {
+        Vec_Ptr_t * vGias;
+        vGias = Vec_PtrAlloc( 1 );
+        Vec_PtrPush( vGias, pAig );
+        pGia = Cec_ManChoiceComputationVec( vGias, pParsChc );
+        Vec_PtrFree( vGias );
+    }
+    else
+    {
+        pMan = Gia_ManToAig( pAig, 0 );
+        Dch_ManSetDefaultParams( pPars );
+        pPars->fUseGia  = 1;
+        pPars->nBTLimit = pParsChc->nBTLimit;
+        pPars->fUseCSat = pParsChc->fUseCSat;
+        pPars->fVerbose = pParsChc->fVerbose;
+        pManNew = Dar_ManChoiceNew( pMan, pPars );
+        pGia = Gia_ManFromAig( pManNew );
+        Aig_ManStop( pManNew );
+        Aig_ManStop( pMan );
+    }
+    return pGia;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs computation of AIGs with choices.]
+
+  Description [Takes several AIGs and performs choicing.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Cec_ComputeChoices( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars )
 {
-    return NULL;
+    Cec_ParChc_t ParsChc, * pParsChc = &ParsChc;
+    Vec_Ptr_t * vGias;
+    Gia_Man_t * pGia;
+    Aig_Man_t * pAig;
+    int i;
+    if ( pPars->fVerbose )
+        ABC_PRT( "Synthesis time", pPars->timeSynth );
+    Cec_ManChcSetDefaultParams( pParsChc );
+    pParsChc->nBTLimit = pPars->nBTLimit;
+    pParsChc->fUseCSat = pPars->fUseCSat;
+    if ( pParsChc->fUseCSat && pParsChc->nBTLimit > 100 )
+        pParsChc->nBTLimit = 100;
+    pParsChc->fVerbose = pPars->fVerbose;
+    vGias = Vec_PtrAlloc( 10 );
+    Vec_PtrForEachEntry( vAigs, pAig, i )
+        Vec_PtrPush( vGias, Gia_ManFromAig(pAig) );
+    pGia = Cec_ManChoiceComputationVec( vGias, pParsChc );
+    Gia_ManSetRegNum( pGia, Gia_ManRegNum(Vec_PtrEntry(vGias, 0)) );
+    Vec_PtrForEachEntry( vGias, pAig, i )
+        Gia_ManStop( (Gia_Man_t *)pAig );
+    Vec_PtrFree( vGias );
+    pAig = Gia_ManToAig( pGia, 1 );
+    Gia_ManStop( pGia );
+    return pAig;
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/cec/cecCore.c b/src/aig/cec/cecCore.c
index ca0a3665..dc0fc0d0 100644
--- a/src/aig/cec/cecCore.c
+++ b/src/aig/cec/cecCore.c
@@ -199,8 +199,8 @@ void Cec_ManChcSetDefaultParams( Cec_ParChc_t * p )
     p->nWords         =      15;  // the number of simulation words
     p->nRounds        =      15;  // the number of simulation rounds
     p->nBTLimit       =    1000;  // conflict limit at a node
-    p->fFirstStop     =       0;  // stop on the first sat output
-    p->fUseSmartCnf   =       0;  // use smart CNF computation
+    p->fUseRings      =       1;  // use rings
+    p->fUseCSat       =       0;  // use circuit-based solver
     p->fVeryVerbose   =       0;  // verbose stats
     p->fVerbose       =       0;  // verbose stats
 }  
diff --git a/src/aig/cec/cecCorr.c b/src/aig/cec/cecCorr.c
index dccd90b0..8e97e207 100644
--- a/src/aig/cec/cecCorr.c
+++ b/src/aig/cec/cecCorr.c
@@ -566,6 +566,35 @@ int Cec_ManResimulateCounterExamples( Cec_ManSim_t * pSim, Vec_Int_t * vCexStore
 
 /**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 );
+        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.]
@@ -613,9 +642,10 @@ int Gia_ManCheckRefinements( Gia_Man_t * p, Vec_Str_t * vStatus, Vec_Int_t * vOu
     return 1;
 }
 
+
 /**Function*************************************************************
 
-  Synopsis    [Marks all the nodes as proved.]
+  Synopsis    [Duplicates the AIG in the DFS order.]
 
   Description []
                
@@ -624,22 +654,59 @@ int Gia_ManCheckRefinements( Gia_Man_t * p, Vec_Str_t * vStatus, Vec_Int_t * vOu
   SeeAlso     []
 
 ***********************************************************************/
-void Gia_ManSetProvedNodes( Gia_Man_t * p )
+void Gia_ManCorrReduce_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
 {
-    Gia_Obj_t * pObj;
-    int i, nLits = 0;
-    Gia_ManForEachObj1( p, pObj, i )
+    Gia_Obj_t * pRepr;
+    if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) )
     {
-        if ( Gia_ObjRepr(p, i) == GIA_VOID )
-            continue;
-        Gia_ObjSetProved( p, i );
-        nLits++;
+        Gia_ManCorrReduce_rec( pNew, p, pRepr );
+        pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
+        return;
     }
-//    printf( "Identified %d proved literals.\n", nLits );
+    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 []
@@ -649,7 +716,7 @@ void Gia_ManSetProvedNodes( Gia_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Cec_ManLCorrPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIter, int Time )
+void Cec_ManRefinedClassPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIter, int Time )
 { 
     int nLits, CounterX = 0, Counter0 = 0, Counter = 0;
     int i, Entry, nProve = 0, nDispr = 0, nFail = 0;
@@ -685,7 +752,7 @@ void Cec_ManLCorrPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIter, int
 
 /**Function*************************************************************
 
-  Synopsis    [Top-level procedure for register correspondence.]
+  Synopsis    [Internal procedure for register correspondence.]
 
   Description []
                
@@ -694,26 +761,26 @@ void Cec_ManLCorrPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIter, int
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
+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;
-    Gia_Man_t * pNew, * pTemp;
     Cec_ParSim_t ParsSim, * pParsSim = &ParsSim;
     Cec_ParSat_t ParsSat, * pParsSat = &ParsSat;
     Cec_ManSim_t * pSim;
     Gia_Man_t * pSrm;
-    int r, RetValue;
-    int clkSat = 0, clkSim = 0, clkSrm = 0, clkTotal = clock();
+    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" );
-        return NULL;
+        return 0;
     }
     Gia_ManRandom( 1 );
     // prepare simulation manager
@@ -736,10 +803,10 @@ Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
         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_ManLCorrPrintStats( pAig, NULL, 0, clock() - clk );
+        Cec_ManRefinedClassPrintStats( pAig, NULL, 0, clock() - clk );
     }
     // perform refinement of equivalence classes
-    for ( r = 0; r < 100000; r++ )
+    for ( r = 0; r < nIterMax; r++ )
     { 
         clk = clock();
         // perform speculative reduction
@@ -776,7 +843,7 @@ Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
         clkSim += clock() - clk2;
         Gia_ManCheckRefinements( pAig, vStatus, vOutputs, pSim, pPars->fUseRings );
         if ( pPars->fVerbose )
-            Cec_ManLCorrPrintStats( pAig, vStatus, r+1, clock() - clk );
+            Cec_ManRefinedClassPrintStats( pAig, vStatus, r+1, clock() - clk );
         Vec_StrFree( vStatus );
         Vec_IntFree( vOutputs );
 //Gia_ManEquivPrintClasses( pAig, 1, 0 );
@@ -811,7 +878,7 @@ Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
                 fChanges = 1;
             }
             if ( pPars->fVerbose )
-                Cec_ManLCorrPrintStats( pAig, vStatus, -1, clock() - clkBmc );
+                Cec_ManRefinedClassPrintStats( pAig, vStatus, -1, clock() - clkBmc );
             // recycle
             Vec_IntFree( vCexStore );
             Vec_StrFree( vStatus );
@@ -822,20 +889,55 @@ Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
     else
     {
         if ( pPars->fVerbose )
-            Cec_ManLCorrPrintStats( pAig, NULL, r+1, clock() - clk );
+            Cec_ManRefinedClassPrintStats( pAig, NULL, r+1, clock() - clk );
     }
     // check the overflow
-    if ( r == 100000 )
+    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 0;
+}    
+
+/**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
-    Gia_ManSetProvedNodes( pAig );
-    Gia_ManEquivImprove( pAig );
-    pNew = Gia_ManEquivReduce( pAig, 0, 0, 0 );
-//Gia_WriteAiger( pNew, "reduced.aig", 0, 0 );
-    pNew = Gia_ManSeqCleanup( pTemp = pNew );
-    Gia_ManStop( pTemp );
+    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 )
     {
@@ -844,11 +946,6 @@ Gia_Man_t * Cec_ManLSCorrespondence( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
             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) );
-        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 pNew;
 }
diff --git a/src/aig/cec/cecInt.h b/src/aig/cec/cecInt.h
index 22bd292b..1fd48d55 100644
--- a/src/aig/cec/cecInt.h
+++ b/src/aig/cec/cecInt.h
@@ -166,7 +166,8 @@ struct Cec_ManFra_t_
 ///                    FUNCTION DECLARATIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
-/*=== cecCore.c ============================================================*/
+/*=== cecCorr.c ============================================================*/
+extern void                 Cec_ManRefinedClassPrintStats( Gia_Man_t * p, Vec_Str_t * vStatus, int iIter, int Time );
 /*=== cecClass.c ============================================================*/
 extern int                  Cec_ManSimClassRemoveOne( Cec_ManSim_t * p, int i );
 extern int                  Cec_ManSimClassesPrepare( Cec_ManSim_t * p );
diff --git a/src/aig/cec/cecSeq.c b/src/aig/cec/cecSeq.c
index 28f3a637..b19950b3 100644
--- a/src/aig/cec/cecSeq.c
+++ b/src/aig/cec/cecSeq.c
@@ -126,7 +126,7 @@ int Cec_ManSeqResimulate( Cec_ManSim_t * p, Vec_Ptr_t * vInfo )
 {
     unsigned * pInfo0, * pInfo1;
     int f, i, k, w, RetValue = 0;
-    assert( Gia_ManRegNum(p->pAig) > 0 );
+//    assert( Gia_ManRegNum(p->pAig) > 0 );
     assert( Vec_PtrSize(vInfo) == Gia_ManRegNum(p->pAig) + Gia_ManPiNum(p->pAig) * p->pPars->nRounds );
     for ( k = 0; k < Gia_ManRegNum(p->pAig); k++ )
     {
diff --git a/src/aig/dar/darLib.c b/src/aig/dar/darLib.c
index cfa4594d..7b23aa33 100644
--- a/src/aig/dar/darLib.c
+++ b/src/aig/dar/darLib.c
@@ -730,7 +730,7 @@ int Dar_LibCutMarkMffc( Aig_Man_t * p, Aig_Obj_t * pRoot, int nLeaves, float * p
     for ( i = 0; i < nLeaves; i++ )
         Aig_Regular(s_DarLib->pDatas[i].pFunc)->nRefs++;
     // label MFFC with current ID
-    nNodes = Aig_NodeMffsLabel( p, pRoot, pPower );
+    nNodes = Aig_NodeMffcLabel( p, pRoot, pPower );
     // unmark the cut leaves
     for ( i = 0; i < nLeaves; i++ )
         Aig_Regular(s_DarLib->pDatas[i].pFunc)->nRefs--;
diff --git a/src/aig/dar/darRefact.c b/src/aig/dar/darRefact.c
index 6118dd71..5f6c5520 100644
--- a/src/aig/dar/darRefact.c
+++ b/src/aig/dar/darRefact.c
@@ -376,14 +376,14 @@ int Dar_ManRefactorTryCuts( Ref_Man_t * p, Aig_Obj_t * pObj, int nNodesSaved, in
         pTruth = Aig_ManCutTruth( pObj, vCut, p->vCutNodes, p->vTruthElem, p->vTruthStore );
         if ( Kit_TruthIsConst0(pTruth, Vec_PtrSize(vCut)) )
         {
-            p->GainBest = Aig_NodeMffsSupp( p->pAig, pObj, 0, NULL );
+            p->GainBest = Aig_NodeMffcSupp( p->pAig, pObj, 0, NULL );
             p->pGraphBest = Kit_GraphCreateConst0();
             Vec_PtrCopy( p->vLeavesBest, vCut );
             return p->GainBest;
         }
         if ( Kit_TruthIsConst1(pTruth, Vec_PtrSize(vCut)) )
         {
-            p->GainBest = Aig_NodeMffsSupp( p->pAig, pObj, 0, NULL );
+            p->GainBest = Aig_NodeMffcSupp( p->pAig, pObj, 0, NULL );
             p->pGraphBest = Kit_GraphCreateConst1();
             Vec_PtrCopy( p->vLeavesBest, vCut );
             return p->GainBest;
@@ -528,7 +528,7 @@ int Dar_ManRefactor( Aig_Man_t * pAig, Dar_RefPar_t * pPars )
         // get the bounded MFFC size
 clk = clock();
         nLevelMin = ABC_MAX( 0, Aig_ObjLevel(pObj) - 10 );
-        nNodesSaved = Aig_NodeMffsSupp( pAig, pObj, nLevelMin, vCut );
+        nNodesSaved = Aig_NodeMffcSupp( pAig, pObj, nLevelMin, vCut );
         if ( nNodesSaved < p->pPars->nMffcMin ) // too small to consider
         {
 p->timeCuts += clock() - clk;
@@ -538,15 +538,15 @@ p->timeCuts += clock() - clk;
         if ( Vec_PtrSize(vCut) > p->pPars->nLeafMax ) // get one reconv-driven cut
         {
             Aig_ManFindCut( pObj, vCut, p->vCutNodes, p->pPars->nLeafMax, 50 );
-            nNodesSaved = Aig_NodeMffsLabelCut( p->pAig, pObj, vCut );
+            nNodesSaved = Aig_NodeMffcLabelCut( p->pAig, pObj, vCut );
         }
         else if ( Vec_PtrSize(vCut) < p->pPars->nLeafMax - 2 && p->pPars->fExtend )
         {
             if ( !Dar_ObjCutLevelAchieved(vCut, nLevelMin) )
             {
-                if ( Aig_NodeMffsExtendCut( pAig, pObj, vCut, vCut2 ) )
+                if ( Aig_NodeMffcExtendCut( pAig, pObj, vCut, vCut2 ) )
                 {
-                    nNodesSaved2 = Aig_NodeMffsLabelCut( p->pAig, pObj, vCut );
+                    nNodesSaved2 = Aig_NodeMffcLabelCut( p->pAig, pObj, vCut );
                     assert( nNodesSaved2 == nNodesSaved );
                 }
                 if ( Vec_PtrSize(vCut2) > p->pPars->nLeafMax )
diff --git a/src/aig/dar/darScript.c b/src/aig/dar/darScript.c
index 383b5b6b..66e6371d 100644
--- a/src/aig/dar/darScript.c
+++ b/src/aig/dar/darScript.c
@@ -435,6 +435,7 @@ ABC_PRT( "Choicing time ", clock() - clk );
 Aig_Man_t * Dar_ManChoiceNew( Aig_Man_t * pAig, Dch_Pars_t * pPars )
 {
     extern Aig_Man_t * Dch_ComputeChoices( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars );
+    extern Aig_Man_t * Cec_ComputeChoices( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars );
 
     int fVerbose = pPars->fVerbose;
     int fConstruct = 0;
@@ -444,7 +445,8 @@ Aig_Man_t * Dar_ManChoiceNew( Aig_Man_t * pAig, Dch_Pars_t * pPars )
 
 clk = clock();
 //    vAigs = Dar_ManChoiceSynthesisExt();
-    vAigs = Dar_ManChoiceSynthesis( pAig, 1, 1, pPars->fPower, fVerbose );
+//    vAigs = Dar_ManChoiceSynthesis( pAig, 1, 1, pPars->fPower, fVerbose );
+    vAigs = Dar_ManChoiceSynthesis( pAig, 1, 1, pPars->fPower, 0 );
 
     // swap the first and last network
     // this should lead to the primary choice being "better" because of synthesis
@@ -458,9 +460,9 @@ clk = clock();
 
 if ( fVerbose )
 {
-ABC_PRT( "Synthesis time", clock() - clk );
+//ABC_PRT( "Synthesis time", clock() - clk );
 }
-//    pPars->timeSynth = clock() - clk;
+    pPars->timeSynth = clock() - clk;
 
 clk = clock();
 /*
@@ -469,7 +471,11 @@ clk = clock();
     else
         pMan = Aig_ManChoicePartitioned( vAigs, 300, nConfMax, nLevelMax, fVerbose );
 */
-    pMan = Dch_ComputeChoices( vAigs, pPars );
+    // perform choice computation
+    if ( pPars->fUseGia )
+        pMan = Cec_ComputeChoices( vAigs, pPars );
+    else
+        pMan = Dch_ComputeChoices( vAigs, pPars );
 
     // reconstruct the network
     pMan = Aig_ManDupDfsGuided( pTemp = pMan, Vec_PtrEntry(vAigs,0) );
@@ -483,6 +489,8 @@ clk = clock();
     }
     // reset levels
     Aig_ManChoiceLevel( pMan );
+    ABC_FREE( pMan->pName );
+    ABC_FREE( pMan->pSpec );
     pMan->pName = Aig_UtilStrsav( pTemp->pName );
     pMan->pSpec = Aig_UtilStrsav( pTemp->pSpec );
 
diff --git a/src/aig/dch/dch.h b/src/aig/dch/dch.h
index a5a56da6..6157a811 100644
--- a/src/aig/dch/dch.h
+++ b/src/aig/dch/dch.h
@@ -46,8 +46,10 @@ struct Dch_Pars_t_
     int              nSatVarMax;    // the max number of SAT variables
     int              fSynthesis;    // set to 1 to perform synthesis
     int              fPolarFlip;    // uses polarity adjustment
-    int              fSimulateTfo;  // uses simulatin of TFO classes
+    int              fSimulateTfo;  // uses simulation of TFO classes
     int              fPower;        // uses power-aware rewriting
+    int              fUseGia;       // uses GIA package 
+    int              fUseCSat;      // uses circuit-based solver
     int              fVerbose;      // verbose stats
     int              timeSynth;     // synthesis runtime
     int              nNodesAhead;   // the lookahead in terms of nodes
diff --git a/src/aig/dch/dchAig.c b/src/aig/dch/dchAig.c
index 239ece18..d38a1304 100644
--- a/src/aig/dch/dchAig.c
+++ b/src/aig/dch/dchAig.c
@@ -72,7 +72,7 @@ Aig_Man_t * Dch_DeriveTotalAig( Vec_Ptr_t * vAigs )
     {
         assert( Aig_ManPiNum(pAig) == Aig_ManPiNum(pAig2) );
         assert( Aig_ManPoNum(pAig) == Aig_ManPoNum(pAig2) );
-        nNodes += Aig_ManNodeNum(pAig);
+        nNodes += Aig_ManNodeNum(pAig2);
         Aig_ManCleanData( pAig2 );
     }
     // map constant nodes
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index feee5472..2d633d5c 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -418,6 +418,7 @@ static inline int         Gia_ObjVisitColor( Gia_Man_t * p, int Id, int c )  { i
 static inline int         Gia_ObjDiffColors( Gia_Man_t * p, int i, int j )   { return (p->pReprs[i].fColorA ^ p->pReprs[j].fColorA) && (p->pReprs[i].fColorB ^ p->pReprs[j].fColorB); }
 static inline int         Gia_ObjDiffColors2( Gia_Man_t * p, int i, int j )  { return (p->pReprs[i].fColorA ^ p->pReprs[j].fColorA) || (p->pReprs[i].fColorB ^ p->pReprs[j].fColorB); }
 
+static inline Gia_Obj_t * Gia_ObjNextObj( Gia_Man_t * p, int Id )            { return p->pNexts[Id] == 0 ? NULL : Gia_ManObj( p, p->pNexts[Id] );}
 static inline int         Gia_ObjNext( Gia_Man_t * p, int Id )               { return p->pNexts[Id];               }
 static inline void        Gia_ObjSetNext( Gia_Man_t * p, int Id, int Num )   { p->pNexts[Id] = Num;                }
 
@@ -535,6 +536,8 @@ extern Gia_Man_t *         Gia_ManRemoveEnables( Gia_Man_t * p );
 /*=== giaEquiv.c ==========================================================*/
 extern int                 Gia_ManCheckTopoOrder( Gia_Man_t * p );
 extern int *               Gia_ManDeriveNexts( Gia_Man_t * p );
+extern void                Gia_ManDeriveReprs( Gia_Man_t * p );
+extern int                 Gia_ManEquivCountClasses( Gia_Man_t * p );
 extern void                Gia_ManEquivPrintOne( Gia_Man_t * p, int i, int Counter );
 extern void                Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem );
 extern Gia_Man_t *         Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fVerbose );
@@ -544,6 +547,7 @@ extern Gia_Man_t *         Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int f
 extern Gia_Man_t *         Gia_ManSpecReduceInit( Gia_Man_t * p, Gia_Cex_t * pInit, int nFrames, int fDualOut );
 extern void                Gia_ManEquivTransform( Gia_Man_t * p, int fVerbose );
 extern void                Gia_ManEquivImprove( Gia_Man_t * p );
+extern Gia_Man_t *         Gia_ManEquivToChoices( Gia_Man_t * p, int nSnapshots );
 /*=== giaFanout.c =========================================================*/
 extern void                Gia_ObjAddFanout( Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pFanout );
 extern void                Gia_ObjRemoveFanout( Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pFanout );
@@ -629,6 +633,8 @@ extern Gia_Cex_t *         Gia_ManAllocCounterExample( int nRegs, int nRealPis,
 extern int                 Gia_ManVerifyCounterExample( Gia_Man_t * pAig, Gia_Cex_t * p, int fDualOut );
 extern void                Gia_ManPrintCounterExample( Gia_Cex_t * p );
 extern int                 Gia_NodeMffcSize( Gia_Man_t * p, Gia_Obj_t * pNode );
+extern int                 Gia_ManHasChoices( Gia_Man_t * p );
+extern int                 Gia_ManHasDandling( Gia_Man_t * p );
  
 #ifdef __cplusplus
 }
diff --git a/src/aig/gia/giaAig.c b/src/aig/gia/giaAig.c
index 601b85af..a4f1ab44 100644
--- a/src/aig/gia/giaAig.c
+++ b/src/aig/gia/giaAig.c
@@ -45,19 +45,24 @@ static inline Aig_Obj_t * Gia_ObjChild1Copy2( Aig_Obj_t ** ppNodes, Gia_Obj_t *
   SeeAlso     []
 
 ***********************************************************************/
-void Gia_ManFromAig_rec( Gia_Man_t * pNew, Aig_Obj_t * pObj )
+void Gia_ManFromAig_rec( Gia_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
 {
-    if ( pObj->pData )
+    Aig_Obj_t * pNext;
+    if ( pObj->iData )
         return;
-    if ( Aig_ObjIsPi(pObj) )
-    {
-        pObj->iData = Gia_ManAppendCi( pNew );
-        return;
-    }
     assert( Aig_ObjIsNode(pObj) );
-    Gia_ManFromAig_rec( pNew, Aig_ObjFanin0(pObj) );
-    Gia_ManFromAig_rec( pNew, Aig_ObjFanin1(pObj) );
+    Gia_ManFromAig_rec( pNew, p, Aig_ObjFanin0(pObj) );
+    Gia_ManFromAig_rec( pNew, p, Aig_ObjFanin1(pObj) );
     pObj->iData = Gia_ManAppendAnd( pNew, Gia_ObjChild0Copy(pObj), Gia_ObjChild1Copy(pObj) );
+    if ( p->pEquivs && (pNext = Aig_ObjEquiv(p, pObj)) )
+    {
+        int iObjNew, iNextNew;
+        Gia_ManFromAig_rec( pNew, p, pNext );
+        iObjNew  = Gia_Lit2Var(pObj->iData);
+        iNextNew = Gia_Lit2Var(pNext->iData);
+        if ( pNew->pNexts )
+            pNew->pNexts[iObjNew] = iNextNew;        
+    }
 }
 
 /**Function*************************************************************
@@ -76,26 +81,25 @@ Gia_Man_t * Gia_ManFromAig( Aig_Man_t * p )
     Gia_Man_t * pNew;
     Aig_Obj_t * pObj;
     int i;
-    // add fake POs to all the dangling nodes (choices)
-    Aig_ManForEachNode( p, pObj, i )
-        assert( Aig_ObjRefs(pObj) > 0 );
     // create the new manager
     pNew = Gia_ManStart( Aig_ManObjNum(p) );
-    pNew->pName = Aig_UtilStrsav( p->pName );
+    pNew->pName = Gia_UtilStrsav( p->pName );
+    // create room to store equivalences
+    if ( p->pEquivs )
+        pNew->pNexts = ABC_CALLOC( int, Aig_ManObjNum(p) );
     // create the PIs
     Aig_ManCleanData( p );
     Aig_ManConst1(p)->iData = 1;
     Aig_ManForEachPi( p, pObj, i )
-    {
-//        if ( Aig_ObjRefs(pObj) == 0 )
-            pObj->iData = Gia_ManAppendCi( pNew );
-    }
+        pObj->iData = Gia_ManAppendCi( pNew );
     // add logic for the POs
     Aig_ManForEachPo( p, pObj, i )
-        Gia_ManFromAig_rec( pNew, Aig_ObjFanin0(pObj) );        
+        Gia_ManFromAig_rec( pNew, p, Aig_ObjFanin0(pObj) );        
     Aig_ManForEachPo( p, pObj, i )
         Gia_ManAppendCo( pNew, Gia_ObjChild0Copy(pObj) );
     Gia_ManSetRegNum( pNew, Aig_ManRegNum(p) );
+    if ( pNew->pNexts )
+        Gia_ManDeriveReprs( pNew );
     return pNew;
 }
 
@@ -117,7 +121,7 @@ Gia_Man_t * Gia_ManFromAigSwitch( Aig_Man_t * p )
     int i;
     // create the new manager
     pNew = Gia_ManStart( Aig_ManObjNum(p) );
-    pNew->pName = Aig_UtilStrsav( p->pName );
+    pNew->pName = Gia_UtilStrsav( p->pName );
     // create the PIs
     Aig_ManCleanData( p );
     Aig_ManConst1(p)->iData = 1;
@@ -127,12 +131,12 @@ Gia_Man_t * Gia_ManFromAigSwitch( Aig_Man_t * p )
     Aig_ManForEachNode( p, pObj, i )
         if ( Aig_ObjRefs(pObj) == 0 )
         {
-            Gia_ManFromAig_rec( pNew, pObj );        
+            Gia_ManFromAig_rec( pNew, p, pObj );        
             Gia_ManAppendCo( pNew, pObj->iData );
         }
     // add logic for the POs
     Aig_ManForEachPo( p, pObj, i )
-        Gia_ManFromAig_rec( pNew, Aig_ObjFanin0(pObj) );        
+        Gia_ManFromAig_rec( pNew, p, Aig_ObjFanin0(pObj) );        
     Aig_ManForEachPo( p, pObj, i )
         Gia_ManAppendCo( pNew, Gia_ObjChild0Copy(pObj) );
     Gia_ManSetRegNum( pNew, Aig_ManRegNum(p) );
@@ -152,17 +156,27 @@ Gia_Man_t * Gia_ManFromAigSwitch( Aig_Man_t * p )
 ***********************************************************************/
 void Gia_ManToAig_rec( Aig_Man_t * pNew, Aig_Obj_t ** ppNodes, Gia_Man_t * p, Gia_Obj_t * pObj )
 {
+    Gia_Obj_t * pNext;
     if ( ppNodes[Gia_ObjId(p, pObj)] )
         return;
     if ( Gia_ObjIsCi(pObj) )
-    {
         ppNodes[Gia_ObjId(p, pObj)] = Aig_ObjCreatePi( pNew );
-        return;
+    else
+    {
+        assert( Gia_ObjIsAnd(pObj) );
+        Gia_ManToAig_rec( pNew, ppNodes, p, Gia_ObjFanin0(pObj) );
+        Gia_ManToAig_rec( pNew, ppNodes, p, Gia_ObjFanin1(pObj) );
+        ppNodes[Gia_ObjId(p, pObj)] = Aig_And( pNew, Gia_ObjChild0Copy2(ppNodes, pObj, Gia_ObjId(p, pObj)), Gia_ObjChild1Copy2(ppNodes, pObj, Gia_ObjId(p, pObj)) );
+    }
+    if ( pNew->pEquivs && (pNext = Gia_ObjNextObj(p, Gia_ObjId(p, pObj))) )
+    {
+        Aig_Obj_t * pObjNew, * pNextNew;
+        Gia_ManToAig_rec( pNew, ppNodes, p, pNext );
+        pObjNew  = ppNodes[Gia_ObjId(p, pObj)];
+        pNextNew = ppNodes[Gia_ObjId(p, pNext)];
+        if ( pNew->pEquivs )
+            pNew->pEquivs[Aig_Regular(pObjNew)->Id] = Aig_Regular(pNextNew);        
     }
-    assert( Gia_ObjIsAnd(pObj) );
-    Gia_ManToAig_rec( pNew, ppNodes, p, Gia_ObjFanin0(pObj) );
-    Gia_ManToAig_rec( pNew, ppNodes, p, Gia_ObjFanin1(pObj) );
-    ppNodes[Gia_ObjId(p, pObj)] = Aig_And( pNew, Gia_ObjChild0Copy2(ppNodes, pObj, Gia_ObjId(p, pObj)), Gia_ObjChild1Copy2(ppNodes, pObj, Gia_ObjId(p, pObj)) );
 }
 
 /**Function*************************************************************
@@ -176,37 +190,31 @@ void Gia_ManToAig_rec( Aig_Man_t * pNew, Aig_Obj_t ** ppNodes, Gia_Man_t * p, Gi
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Gia_ManToAig( Gia_Man_t * p )
+Aig_Man_t * Gia_ManToAig( Gia_Man_t * p, int fChoices )
 {
     Aig_Man_t * pNew;
     Aig_Obj_t ** ppNodes;
     Gia_Obj_t * pObj;
     int i;
-
+    assert( !fChoices || (p->pNexts && p->pReprs) );
     // create the new manager
     pNew = Aig_ManStart( Gia_ManAndNum(p) );
-    pNew->pName = Aig_UtilStrsav( p->pName );
-    ppNodes = ABC_CALLOC( Aig_Obj_t *, Gia_ManObjNum(p) );
+    pNew->pName = Gia_UtilStrsav( p->pName );
+//    pNew->pSpec = Gia_UtilStrsav( p->pName );
+    // duplicate representation of choice nodes
+    if ( fChoices )
+        pNew->pEquivs = ABC_CALLOC( Aig_Obj_t *, Gia_ManObjNum(p) );
     // create the PIs
+    ppNodes = ABC_CALLOC( Aig_Obj_t *, Gia_ManObjNum(p) );
     ppNodes[0] = Aig_ManConst0(pNew);
     Gia_ManForEachCi( p, pObj, i )
-    {
-//        if ( Aig_ObjRefs(pObj) == 0 )
-            ppNodes[Gia_ObjId(p, pObj)] = Aig_ObjCreatePi( pNew );
-    }
-
+        ppNodes[Gia_ObjId(p, pObj)] = Aig_ObjCreatePi( pNew );
     // add logic for the POs
     Gia_ManForEachCo( p, pObj, i )
     {
         Gia_ManToAig_rec( pNew, ppNodes, p, Gia_ObjFanin0(pObj) );        
         ppNodes[Gia_ObjId(p, pObj)] = Aig_ObjCreatePo( pNew, Gia_ObjChild0Copy2(ppNodes, pObj, Gia_ObjId(p, pObj)) );
     }
-/*
-    Gia_ManForEachCo( p, pObj, i )
-        Gia_ManToAig_rec( pNew, ppNodes, p, Gia_ObjFanin0(pObj) );        
-    Gia_ManForEachCo( p, pObj, i )
-        ppNodes[Gia_ObjId(p, pObj)] = Aig_ObjCreatePo( pNew, Gia_ObjChild0Copy2(ppNodes, pObj, Gia_ObjId(p, pObj)) );
-*/
     Aig_ManSetRegNum( pNew, Gia_ManRegNum(p) );
     ABC_FREE( ppNodes );
     return pNew;
@@ -230,7 +238,7 @@ Aig_Man_t * Gia_ManCofactorAig( Aig_Man_t * p, int nFrames, int nCofFanLit )
     pGia = Gia_ManFromAig( p );
     pGia = Gia_ManUnrollAndCofactor( pTemp = pGia, nFrames, nCofFanLit, 1 );
     Gia_ManStop( pTemp );
-    pMan = Gia_ManToAig( pGia );
+    pMan = Gia_ManToAig( pGia, 0 );
     Gia_ManStop( pGia );
     return pMan;
 }
diff --git a/src/aig/gia/giaAig.h b/src/aig/gia/giaAig.h
index 07cf7bae..0c0ee598 100644
--- a/src/aig/gia/giaAig.h
+++ b/src/aig/gia/giaAig.h
@@ -48,7 +48,7 @@
 /*=== giaAig.c =============================================================*/
 extern Gia_Man_t *         Gia_ManFromAig( Aig_Man_t * p );
 extern Gia_Man_t *         Gia_ManFromAigSwitch( Aig_Man_t * p );
-extern Aig_Man_t *         Gia_ManToAig( Gia_Man_t * p );
+extern Aig_Man_t *         Gia_ManToAig( Gia_Man_t * p, int fChoices );
  
 #ifdef __cplusplus
 }
diff --git a/src/aig/gia/giaAiger.c b/src/aig/gia/giaAiger.c
index 8dbc0cab..afe9164f 100644
--- a/src/aig/gia/giaAiger.c
+++ b/src/aig/gia/giaAiger.c
@@ -413,7 +413,7 @@ Gia_Man_t * Gia_ReadAiger( char * pFileName, int fCheck )
     pNew = Gia_ManStart( nTotal + nLatches + nOutputs + 1 );
     pName = Gia_FileNameGeneric( pFileName );
     pNew->pName = Gia_UtilStrsav( pName );
-//    pNew->pSpec = Aig_UtilStrsav( pFileName );
+//    pNew->pSpec = Gia_UtilStrsav( pFileName );
     ABC_FREE( pName );
 
     // prepare the array of nodes
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index bd5297e4..63748403 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -387,6 +387,7 @@ Gia_Man_t * Gia_ManDupMarked( Gia_Man_t * p )
     {
         if ( pObj->fMark0 )
             continue;
+        pObj->fMark0 = 0;
         if ( Gia_ObjIsAnd(pObj) )
             pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
         else if ( Gia_ObjIsCi(pObj) )
@@ -396,14 +397,32 @@ Gia_Man_t * Gia_ManDupMarked( Gia_Man_t * p )
         }
         else if ( Gia_ObjIsCo(pObj) )
         {
-            Gia_Obj_t * pFanin = Gia_ObjFanin0(pObj);
-
+//            Gia_Obj_t * pFanin = Gia_ObjFanin0(pObj);
             pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
             nRis += Gia_ObjIsRi(p, pObj);
         }
     }
     assert( nRos == nRis );
     Gia_ManSetRegNum( pNew, nRos );
+    if ( p->pReprs && p->pNexts )
+    {
+        Gia_Obj_t * pRepr;
+        pNew->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) );
+        for ( i = 0; i < Gia_ManObjNum(p); i++ )
+            Gia_ObjSetRepr( pNew, i, GIA_VOID );
+        Gia_ManForEachObj1( p, pObj, i )
+        {
+            if ( !~pObj->Value )
+                continue;
+            pRepr = Gia_ObjReprObj( p, i );
+            if ( pRepr == NULL )
+                continue;
+            assert( ~pRepr->Value );
+            if ( Gia_Lit2Var(pObj->Value) != Gia_Lit2Var(pRepr->Value) )
+                Gia_ObjSetRepr( pNew, Gia_Lit2Var(pObj->Value), Gia_Lit2Var(pRepr->Value) ); 
+        }
+        pNew->pNexts = Gia_ManDeriveNexts( pNew );
+    }
     return pNew;
 }
 
diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c
index f802e15d..cdee73d0 100644
--- a/src/aig/gia/giaEquiv.c
+++ b/src/aig/gia/giaEquiv.c
@@ -94,7 +94,8 @@ int * Gia_ManDeriveNexts( Gia_Man_t * p )
 {
     unsigned * pNexts, * pTails;
     int i;
-    assert( p->pReprs );
+    assert( p->pReprs != NULL );
+    assert( p->pNexts == NULL );
     pNexts = ABC_CALLOC( unsigned, Gia_ManObjNum(p) );
     pTails = ABC_ALLOC( unsigned, Gia_ManObjNum(p) );
     for ( i = 0; i < Gia_ManObjNum(p); i++ )
@@ -112,6 +113,37 @@ int * Gia_ManDeriveNexts( Gia_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Given points to the next objects, derives representatives.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManDeriveReprs( Gia_Man_t * p )
+{
+    int i, iObj;
+    assert( p->pReprs == NULL );
+    assert( p->pNexts != NULL );
+    p->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) );
+    for ( i = 0; i < Gia_ManObjNum(p); i++ )
+        Gia_ObjSetRepr( p, i, GIA_VOID );
+    for ( i = 0; i < Gia_ManObjNum(p); i++ )
+    {
+        if ( p->pNexts[i] == 0 )
+            continue;
+        if ( p->pReprs[i].iRepr != GIA_VOID )
+            continue;
+        // next is set, repr is not set
+        for ( iObj = p->pNexts[i]; iObj; iObj = p->pNexts[iObj] )
+            p->pReprs[iObj].iRepr = i;
+    }
+}
+
+/**Function*************************************************************
+
   Synopsis    []
 
   Description []
@@ -186,6 +218,25 @@ int Gia_ManEquivCountLitsAll( Gia_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
+int Gia_ManEquivCountClasses( Gia_Man_t * p )
+{
+    int i, Counter = 0;
+    for ( i = 1; i < Gia_ManObjNum(p); i++ )
+        Counter += Gia_ObjIsHead(p, i);
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Gia_ManEquivCheckLits( Gia_Man_t * p, int nLits )
 {
     int nLitsReal = Gia_ManEquivCountLitsAll( p );
@@ -966,6 +1017,246 @@ void Gia_ManEquivImprove( Gia_Man_t * p )
 //    p->pNexts = Gia_ManDeriveNexts( p );
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if pOld is in the TFI of pNode.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ObjCheckTfi_rec( Gia_Man_t * p, Gia_Obj_t * pOld, Gia_Obj_t * pNode, Vec_Ptr_t * vVisited )
+{
+    // check the trivial cases
+    if ( pNode == NULL )
+        return 0;
+    if ( Gia_ObjIsCi(pNode) )
+        return 0;
+//    if ( pNode->Id < pOld->Id ) // cannot use because of choices of pNode
+//        return 0;
+    if ( pNode == pOld )
+        return 1;
+    // skip the visited node
+    if ( pNode->fMark0 )
+        return 0;
+    pNode->fMark0 = 1;
+    Vec_PtrPush( vVisited, pNode );
+    // check the children
+    if ( Gia_ObjCheckTfi_rec( p, pOld, Gia_ObjFanin0(pNode), vVisited ) )
+        return 1;
+    if ( Gia_ObjCheckTfi_rec( p, pOld, Gia_ObjFanin1(pNode), vVisited ) )
+        return 1;
+    // check equivalent nodes
+    return Gia_ObjCheckTfi_rec( p, pOld, Gia_ObjNextObj(p, Gia_ObjId(p, pNode)), vVisited );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if pOld is in the TFI of pNode.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ObjCheckTfi( Gia_Man_t * p, Gia_Obj_t * pOld, Gia_Obj_t * pNode )
+{
+    Vec_Ptr_t * vVisited;
+    Gia_Obj_t * pObj;
+    int RetValue, i;
+    assert( !Gia_IsComplement(pOld) );
+    assert( !Gia_IsComplement(pNode) );
+    vVisited = Vec_PtrAlloc( 100 );
+    RetValue = Gia_ObjCheckTfi_rec( p, pOld, pNode, vVisited );
+    Vec_PtrForEachEntry( vVisited, pObj, i )
+        pObj->fMark0 = 0;
+    Vec_PtrFree( vVisited );
+    return RetValue;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Adds the next entry while making choices.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManAddNextEntry_rec( Gia_Man_t * p, Gia_Obj_t * pOld, Gia_Obj_t * pNode )
+{
+    if ( Gia_ObjNext(p, Gia_ObjId(p, pOld)) == 0 )
+    {
+        Gia_ObjSetNext( p, Gia_ObjId(p, pOld), Gia_ObjId(p, pNode) );
+        return;
+    }
+    Gia_ManAddNextEntry_rec( p, Gia_ObjNextObj(p, Gia_ObjId(p, pOld)), pNode );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates the AIG in the DFS order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManEquivToChoices_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
+{
+    Gia_Obj_t * pRepr, * pReprNew, * pObjNew;
+    if ( ~pObj->Value )
+        return;
+    if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) )
+    {
+        if ( Gia_ObjIsConst0(pRepr) )
+        {
+            pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
+            return;
+        }
+        Gia_ManEquivToChoices_rec( pNew, p, pRepr );
+        assert( Gia_ObjIsAnd(pObj) );
+        Gia_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin0(pObj) );
+        Gia_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin1(pObj) );
+        pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+        if ( Gia_LitRegular(pObj->Value) == Gia_LitRegular(pRepr->Value) )
+        {
+            assert( (int)pObj->Value == Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) ) );
+            return;
+        }
+        assert( pRepr->Value < pObj->Value );
+        pReprNew = Gia_ManObj( pNew, Gia_Lit2Var(pRepr->Value) );
+        pObjNew  = Gia_ManObj( pNew, Gia_Lit2Var(pObj->Value) );
+        if ( Gia_ObjReprObj( pNew, Gia_ObjId(pNew, pObjNew) ) )
+        {
+            assert( Gia_ObjReprObj( pNew, Gia_ObjId(pNew, pObjNew) ) == pReprNew );
+            pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
+            return;
+        }
+        if ( !Gia_ObjCheckTfi( pNew, pReprNew, pObjNew ) )
+        {
+            assert( Gia_ObjNext(pNew, Gia_ObjId(pNew, pObjNew)) == 0 );
+            Gia_ObjSetRepr( pNew, Gia_ObjId(pNew, pObjNew), Gia_ObjId(pNew, pReprNew) );
+            Gia_ManAddNextEntry_rec( pNew, pReprNew, pObjNew ); 
+        }
+        pObj->Value = Gia_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
+        return;
+    }
+    assert( Gia_ObjIsAnd(pObj) );
+    Gia_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin0(pObj) );
+    Gia_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin1(pObj) );
+    pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Removes choices, which contain fanouts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManRemoveBadChoices( Gia_Man_t * p )
+{
+    Gia_Obj_t * pObj;
+    int i, iObj, iPrev, Counter = 0;
+    // mark nodes with fanout
+    Gia_ManForEachObj( p, pObj, i )
+    {
+        pObj->fMark0 = 0;
+        if ( Gia_ObjIsAnd(pObj) )
+        {
+            Gia_ObjFanin0(pObj)->fMark0 = 1;
+            Gia_ObjFanin1(pObj)->fMark0 = 1;
+        }
+        else if ( Gia_ObjIsCo(pObj) )
+            Gia_ObjFanin0(pObj)->fMark0 = 1;
+    }
+    // go through the classes and remove 
+    Gia_ManForEachClass( p, i )
+    {
+        for ( iPrev = i, iObj = Gia_ObjNext(p, i); iObj; iObj = Gia_ObjNext(p, iPrev) )
+        {
+            if ( !Gia_ManObj(p, iObj)->fMark0 )
+            {
+                iPrev = iObj; 
+                continue;
+            }
+            Gia_ObjSetRepr( p, iObj, GIA_VOID );
+            Gia_ObjSetNext( p, iPrev, Gia_ObjNext(p, iObj) );
+            Gia_ObjSetNext( p, iObj, 0 );
+            Counter++;
+        } 
+    }
+    // remove the marks
+    Gia_ManCleanMark0( p );
+//    printf( "Removed %d bad choices.\n", Counter );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reduces AIG using equivalence classes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManEquivToChoices( Gia_Man_t * p, int nSnapshots )
+{
+    Gia_Man_t * pNew, * pTemp;
+    Gia_Obj_t * pObj, * pRepr;
+    int i;
+    assert( (Gia_ManCoNum(p) % nSnapshots) == 0 );
+    Gia_ManSetPhase( p );
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Gia_UtilStrsav( p->pName );
+    pNew->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) );
+    pNew->pNexts = ABC_CALLOC( int, Gia_ManObjNum(p) );
+    for ( i = 0; i < Gia_ManObjNum(p); i++ )
+        Gia_ObjSetRepr( pNew, i, GIA_VOID );
+    Gia_ManFillValue( p );
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManForEachCi( p, pObj, i )
+        pObj->Value = Gia_ManAppendCi(pNew);
+    Gia_ManForEachRo( p, pObj, i )
+        if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) )
+        {
+            assert( Gia_ObjIsConst0(pRepr) || Gia_ObjIsRo(p, pRepr) );
+            pObj->Value = pRepr->Value;
+        }
+    Gia_ManHashAlloc( pNew );
+    Gia_ManForEachCo( p, pObj, i )
+        Gia_ManEquivToChoices_rec( pNew, p, Gia_ObjFanin0(pObj) );
+    Gia_ManForEachCo( p, pObj, i )
+        if ( i % nSnapshots == 0 )
+            Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    Gia_ManHashStop( pNew );
+    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+    Gia_ManRemoveBadChoices( pNew );
+//    Gia_ManEquivPrintClasses( pNew, 0, 0 );
+    pNew = Gia_ManCleanup( pTemp = pNew );
+    Gia_ManStop( pTemp );
+//    Gia_ManEquivPrintClasses( pNew, 0, 0 );
+    return pNew;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c
index f69ac266..7f4da081 100644
--- a/src/aig/gia/giaMan.c
+++ b/src/aig/gia/giaMan.c
@@ -158,7 +158,7 @@ void Gia_ManPrintPlacement( Gia_Man_t * p )
 void Gia_ManPrintStats( Gia_Man_t * p, int fSwitch )
 {
     if ( p->pName )
-        printf( "%8s : ", p->pName );
+        printf( "%-8s : ", p->pName );
     printf( "i/o =%7d/%7d", Gia_ManPiNum(p), Gia_ManPoNum(p) );
     if ( Gia_ManRegNum(p) )
         printf( "  ff =%7d", Gia_ManRegNum(p) );
@@ -166,6 +166,8 @@ void Gia_ManPrintStats( Gia_Man_t * p, int fSwitch )
     printf( "  lev =%5d", Gia_ManLevelNum(p) );
     printf( "  cut =%5d", Gia_ManCrossCut(p) );
     printf( "  mem =%5.2f Mb", 12.0*Gia_ManObjNum(p)/(1<<20) );
+    if ( Gia_ManHasDandling(p) )
+        printf( "  ch =%5d", Gia_ManEquivCountClasses(p) );
     if ( fSwitch )
     {
         if ( p->pSwitching )
diff --git a/src/aig/gia/giaScl.c b/src/aig/gia/giaScl.c
index cf72104f..5ac8e04a 100644
--- a/src/aig/gia/giaScl.c
+++ b/src/aig/gia/giaScl.c
@@ -41,12 +41,15 @@
 ***********************************************************************/
 int Gia_ManCombMarkUsed_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
 {
+    if ( pObj == NULL )
+        return 0;
     if ( !pObj->fMark0 )
         return 0;
     pObj->fMark0 = 0;
     assert( Gia_ObjIsAnd(pObj) );
     return 1 + Gia_ManCombMarkUsed_rec( p, Gia_ObjFanin0(pObj) )
-             + Gia_ManCombMarkUsed_rec( p, Gia_ObjFanin1(pObj) );
+             + Gia_ManCombMarkUsed_rec( p, Gia_ObjFanin1(pObj) )
+             + (p->pNexts ? Gia_ManCombMarkUsed_rec( p, Gia_ObjNextObj(p, Gia_ObjId(p, pObj)) ) : 0);
 }
 
 /**Function*************************************************************
@@ -88,6 +91,7 @@ Gia_Man_t * Gia_ManCleanup( Gia_Man_t * p )
     return Gia_ManDupMarked( p );
 }
 
+
 /**Function*************************************************************
 
   Synopsis    [Marks CIs/COs/ANDs unreachable from POs.]
diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c
index 5716c1a0..54bc98dd 100644
--- a/src/aig/gia/giaUtil.c
+++ b/src/aig/gia/giaUtil.c
@@ -858,6 +858,114 @@ int Gia_NodeMffcSize( Gia_Man_t * p, Gia_Obj_t * pNode )
     return ConeSize1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if AIG has choices.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManHasChoices( Gia_Man_t * p )
+{
+    Gia_Obj_t * pObj;
+    int i, Counter1 = 0, Counter2 = 0;
+    int nFailNoRepr = 0;
+    int nFailHaveRepr = 0;
+    int nChoiceNodes = 0;
+    int nChoices = 0;
+    if ( p->pReprs == NULL || p->pNexts == NULL )
+        return 0;
+    // check if there are any representatives
+    Gia_ManForEachObj( p, pObj, i )
+    {
+        if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) )
+            Counter1++;
+        if ( Gia_ObjNext( p, Gia_ObjId(p, pObj) ) )
+            Counter2++;
+    }
+    if ( Counter1 == 0 )
+    {
+        printf( "Warning: AIG has repr data-strucure but not reprs.\n" );
+        return 0;
+    }
+//    printf( "%d nodes have reprs.\n", Counter1 );
+//    printf( "%d nodes have nexts.\n", Counter2 );
+    // check if there are any internal nodes without fanout
+    // make sure all nodes without fanout have representatives
+    // make sure all nodes with fanout have no representatives
+    ABC_FREE( p->pRefs );
+    Gia_ManCreateRefs( p );
+    Gia_ManForEachAnd( p, pObj, i )
+    {
+        if ( Gia_ObjRefs(p, pObj) == 0 )
+        {
+            if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) == NULL )
+                nFailNoRepr++;
+            else
+                nChoices++;
+        }
+        else
+        {
+            if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) != NULL )
+                nFailHaveRepr++;
+            if ( Gia_ObjNextObj( p, Gia_ObjId(p, pObj) ) != NULL )
+                nChoiceNodes++;
+        }
+        if ( Gia_ObjReprObj( p, i ) )
+            assert( Gia_ObjRepr(p, i) < i );
+    }
+    if ( nChoices == 0 )
+        return 0;
+    if ( nFailNoRepr )
+    {
+        printf( "Gia_ManHasChoices(): Error: %d internal nodes have no fanout and no repr.\n", nFailNoRepr );
+//        return 0;
+    }
+    if ( nFailHaveRepr )
+    {
+        printf( "Gia_ManHasChoices(): Error: %d internal nodes have both fanout and repr.\n", nFailHaveRepr );
+//        return 0;
+    }
+//    printf( "Gia_ManHasChoices(): AIG has %d choice nodes with %d choices.\n", nChoiceNodes, nChoices );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if AIG has dangling nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManHasDandling( Gia_Man_t * p )
+{
+    Gia_Obj_t * pObj;
+    int i, Counter = 0;
+    Gia_ManForEachObj( p, pObj, i )
+    {
+        pObj->fMark0 = 0;
+        if ( Gia_ObjIsAnd(pObj) )
+        {
+            Gia_ObjFanin0(pObj)->fMark0 = 1;
+            Gia_ObjFanin1(pObj)->fMark0 = 1;
+        }
+        else if ( Gia_ObjIsCo(pObj) )
+            Gia_ObjFanin0(pObj)->fMark0 = 1;
+    }
+    Gia_ManForEachAnd( p, pObj, i )
+        Counter += !pObj->fMark0;
+    Gia_ManCleanMark0( p );
+    return Counter;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/ivy/ivyRwr.c b/src/aig/ivy/ivyRwr.c
index 8bfeb03c..af425079 100644
--- a/src/aig/ivy/ivyRwr.c
+++ b/src/aig/ivy/ivyRwr.c
@@ -96,9 +96,9 @@ int Ivy_ManRewritePre( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost, int fV
             }
             if ( nGain > 0 )
             { // print stats on the MFFC
-                extern void Ivy_NodeMffsConeSuppPrint( Ivy_Obj_t * pNode );
+                extern void Ivy_NodeMffcConeSuppPrint( Ivy_Obj_t * pNode );
                 printf( "Node %6d : Gain = %4d  ", pNode->Id, nGain );
-                Ivy_NodeMffsConeSuppPrint( pNode );
+                Ivy_NodeMffcConeSuppPrint( pNode );
             }
 */
             // complement the FF if needed
diff --git a/src/aig/ssw/sswClass.c b/src/aig/ssw/sswClass.c
index 8fce7904..ce6ebf85 100644
--- a/src/aig/ssw/sswClass.c
+++ b/src/aig/ssw/sswClass.c
@@ -392,7 +392,7 @@ void Ssw_ClassesPrintOne( Ssw_Cla_t * p, Aig_Obj_t * pRepr )
     printf( "{ " );
     Ssw_ClassForEachNode( p, pRepr, pObj, i )
         printf( "%d(%d,%d,%d) ", pObj->Id, pObj->Level, 
-        Aig_SupportSize(p->pAig,pObj), Aig_NodeMffsSupp(p->pAig,pObj,0,NULL) );
+        Aig_SupportSize(p->pAig,pObj), Aig_NodeMffcSupp(p->pAig,pObj,0,NULL) );
     printf( "}\n" );
 }
 
@@ -420,7 +420,7 @@ void Ssw_ClassesPrint( Ssw_Cla_t * p, int fVeryVerbose )
     Aig_ManForEachObj( p->pAig, pObj, i )
         if ( Ssw_ObjIsConst1Cand( p->pAig, pObj ) )
             printf( "%d(%d,%d,%d) ", pObj->Id, pObj->Level, 
-            Aig_SupportSize(p->pAig,pObj), Aig_NodeMffsSupp(p->pAig,pObj,0,NULL) );
+            Aig_SupportSize(p->pAig,pObj), Aig_NodeMffcSupp(p->pAig,pObj,0,NULL) );
     printf( "}\n" );
     Ssw_ManForEachClass( p, ppClass, i )
     {