diff --git a/src/aig/gia/giaNf.c b/src/aig/gia/giaNf.c
index b38093f23..7d044c0f7 100644
--- a/src/aig/gia/giaNf.c
+++ b/src/aig/gia/giaNf.c
@@ -2245,6 +2245,171 @@ void Nf_ManDumpMatches( Nf_Man_t * p )
     fclose( pFile );
 }
 
+
+
+static int IsLeafInCut(int iNode, int *pLeaves, int nLeaves)
+{
+    int i;
+    for (i = 0; i < nLeaves; i++)
+        if (pLeaves[i] == iNode)
+            return 1;
+    return 0;
+}
+void Gia_MarkCutNodes_rec(Gia_Man_t *pGia, int iNode, int *pLeaves, int nLeaves)
+{
+    Gia_Obj_t *pObj = Gia_ManObj(pGia, iNode);
+    if (pObj->fMark0)
+        return; 
+    pObj->fMark0 = 1;
+
+    if (IsLeafInCut(iNode, pLeaves, nLeaves))
+        return;
+    if (Gia_ObjIsAnd(pObj)) {
+        Gia_MarkCutNodes_rec(pGia, Gia_ObjFaninId0(pObj, iNode), pLeaves, nLeaves);
+        Gia_MarkCutNodes_rec(pGia, Gia_ObjFaninId1(pObj, iNode), pLeaves, nLeaves);
+    }
+}
+
+void Gia_ClearAllMark0(Gia_Man_t *pGia)
+{
+    int i;
+    Gia_Obj_t *pObj;
+    Gia_ManForEachObj(pGia, pObj, i)
+        pObj->fMark0 = 0;
+}
+void Gia_ClearAllMark1(Gia_Man_t *pGia)
+{
+    int i;
+    Gia_Obj_t *pObj;
+    Gia_ManForEachObj(pGia, pObj, i)
+        pObj->fMark1 = 0;
+}
+void Gia_ConeMark0_rec(Gia_Man_t *pGia, int iObj)
+{
+    Gia_Obj_t *pObj = Gia_ManObj(pGia, iObj);
+    if (pObj->fMark0) return; 
+    pObj->fMark0 = 1;
+    if (!Gia_ObjIsAnd(pObj) && !Gia_ObjIsCi(pObj))
+        return; 
+    if (Gia_ObjIsAnd(pObj)) {
+        Gia_ConeMark0_rec(pGia, Gia_ObjFaninId0(pObj, iObj));
+        Gia_ConeMark0_rec(pGia, Gia_ObjFaninId1(pObj, iObj));
+    }
+}
+
+void Gia_ConeMark1_rec(Gia_Man_t *pGia, int iObj)
+{
+    Gia_Obj_t *pObj = Gia_ManObj(pGia, iObj);
+    if (pObj->fMark1) return; 
+    pObj->fMark1 = 1;
+    if (!Gia_ObjIsAnd(pObj) && !Gia_ObjIsCi(pObj))
+        return;
+    if (Gia_ObjIsAnd(pObj)) {
+        Gia_ConeMark1_rec(pGia, Gia_ObjFaninId0(pObj, iObj));
+        Gia_ConeMark1_rec(pGia, Gia_ObjFaninId1(pObj, iObj));
+    }
+}
+
+
+
+void Nf_PrintChoiceSelection(Nf_Man_t *p)
+{
+    Nf_Mat_t * pM;
+    int i, c, id, * pCut;
+    int mappedCount=0, mark0Count=0, mark1Count=0;
+    if (Gia_ManHasChoices(p->pGia) != 1) {
+        return;
+    }
+    Gia_ClearAllMark0( p->pGia );
+    Gia_ManForEachAndId( p->pGia, i )
+    {
+        Gia_Obj_t * pObj = Gia_ManObj(p->pGia, i);
+        if ( Gia_ObjIsBuf(pObj) )
+        {
+            continue;
+        }
+        for ( c = 0; c < 2; c++ )
+        if ( Nf_ObjMapRefNum(p, i, c) )
+        {
+            pM = Nf_ObjMatchBest( p, i, c );
+            pCut = Nf_CutFromHandle( Nf_ObjCutSet(p, i), pM->CutH );
+            int *pLeaves = Nf_CutLeaves(pCut);
+            int nLeaves = Nf_CutSize(pCut);
+            Gia_MarkCutNodes_rec(p->pGia, i, pLeaves, nLeaves);
+        }
+    }
+    // collect mapping nodes
+    Vec_Int_t *vMappedNodes = Vec_IntAlloc(Gia_ManAndNum(p->pGia));
+    Gia_Obj_t *pObj;
+    Gia_ManForEachObj(p->pGia, pObj, i) {
+        if (pObj->fMark0)
+            Vec_IntPush(vMappedNodes, i);
+    }
+    // clear marks
+    Gia_ClearAllMark0(p->pGia);
+    Gia_ClearAllMark1(p->pGia);
+
+    // collect vRepr and vChoice nodes
+    Vec_Int_t *vRepr = Vec_IntAlloc(Gia_ManChoiceNum(p->pGia));
+    Vec_Int_t *vChoice = Vec_IntAlloc(Gia_ManChoiceNum(p->pGia));
+    Gia_ManForEachObj(p->pGia, pObj, i) {
+        if (Gia_ObjIsHead(p->pGia, i))
+            Vec_IntPush(vRepr, i);
+    }
+    int iHead;
+    Vec_IntForEachEntry(vRepr, iHead, i) {
+        int iNext = Gia_ObjNext(p->pGia, iHead);
+        while (iNext > 0) {
+            Vec_IntPush(vChoice, iNext);
+            iNext = Gia_ObjNext(p->pGia, iNext);
+        }
+    }
+
+    Vec_IntForEachEntry(vRepr, id, i)
+        Gia_ConeMark0_rec(p->pGia, id);
+    Vec_IntForEachEntry(vChoice, id, i)
+        Gia_ConeMark1_rec(p->pGia, id);
+   
+    Vec_IntForEachEntry(vMappedNodes, id, i) {
+        mappedCount++;
+    }
+    Gia_ManForEachObj(p->pGia, pObj, i) {
+        if (pObj->fMark0) 
+            mark0Count++;
+    }
+    Gia_ManForEachObj(p->pGia, pObj, i) {
+        if (pObj->fMark1 && !pObj->fMark0) 
+            mark1Count++;
+    }
+    int reprInMap = 0,choiceInMap = 0;
+    int mark0InMapped = 0, mark1InMapped = 0;
+    Gia_ManForEachObj(p->pGia, pObj, i) {
+        if (pObj->fMark0 && !pObj->fMark1 && Vec_IntFind(vMappedNodes, i) >= 0) {
+            reprInMap++;
+        }
+        if (pObj->fMark1 && !pObj->fMark0 && Vec_IntFind(vMappedNodes, i) >= 0) {
+            choiceInMap++;
+        }
+    }
+    Vec_IntForEachEntry(vMappedNodes, id, i) {
+        Gia_Obj_t* pObj = Gia_ManObj(p->pGia, id);
+        if (pObj->fMark0 && !pObj->fMark1)
+            mark0InMapped++;
+        if (pObj->fMark1 && !pObj->fMark0)
+            mark1InMapped++;
+    }
+    int allMarkedInMapped = mark0InMapped + mark1InMapped;
+    
+    float reprSupportRatio   = (allMarkedInMapped > 0) ? (float)reprInMap   / allMarkedInMapped * 100.0f : 0.0f;
+    float choiceSupportRatio = (allMarkedInMapped > 0) ? (float)choiceInMap / allMarkedInMapped * 100.0f : 0.0f;
+    
+    printf("vRepr unique support: %d/%d (%.2f%%), vChoice unique support: %d/%d (%.2f%%)\n", reprInMap, allMarkedInMapped, reprSupportRatio, choiceInMap, allMarkedInMapped, choiceSupportRatio);
+    Gia_ClearAllMark0(p->pGia);
+    Gia_ClearAllMark1(p->pGia);
+    Vec_IntFree(vRepr);
+    Vec_IntFree(vChoice);
+    Vec_IntFree(vMappedNodes);
+}
 /**Function*************************************************************
 
   Synopsis    [Deriving mapping.]
@@ -2300,6 +2465,9 @@ Gia_Man_t * Nf_ManDeriveMapping( Nf_Man_t * p )
     }
 //    assert( Vec_IntCap(vMapping) == 16 || Vec_IntSize(vMapping) == Vec_IntCap(vMapping) );
     p->pGia->vCellMapping = vMapping;
+
+    if(p->pPars->fVerbose)
+        Nf_PrintChoiceSelection(p);
     if ( p->pPars->ZFile )
         Nf_ManDumpMatches( p );
     return p->pGia;