4 files changed, 5 insertions, 3 deletions
diff --git a/src/opt/mfs/mfsCore.c b/src/opt/mfs/mfsCore.c
index 082b35d4..7e6cd454 100644
--- a/src/opt/mfs/mfsCore.c
+++ b/src/opt/mfs/mfsCore.c
@@ -56,6 +56,7 @@ p->timeWin += clock() - clk;
     // compute the divisors of the window
 clk = clock();
     p->vDivs  = Abc_MfsComputeDivisors( p, pNode, Abc_ObjRequiredLevel(pNode) - 1 );
+    p->nTotalDivs += Vec_PtrSize(p->vDivs);
 p->timeDiv += clock() - clk;
     // construct AIG for the window
 clk = clock();
diff --git a/src/opt/mfs/mfsDiv.c b/src/opt/mfs/mfsDiv.c
index 7b156b97..da6979d1 100644
--- a/src/opt/mfs/mfsDiv.c
+++ b/src/opt/mfs/mfsDiv.c
@@ -253,7 +253,7 @@ Vec_Ptr_t * Abc_MfsComputeDivisors( Mfs_Man_t * p, Abc_Obj_t * pNode, int nLevDi
             if ( !Abc_ObjIsNode(pFanout) ) 
                 continue;
             // skip nodes with large level
-            if ( (int)pFanout->Level >= nLevDivMax )
+            if ( (int)pFanout->Level > nLevDivMax )
                 continue;
             // skip nodes whose fanins are not divisors
             Abc_ObjForEachFanin( pFanout, pFanin, m )
diff --git a/src/opt/mfs/mfsInt.h b/src/opt/mfs/mfsInt.h
index e51e0bba..3c0349bb 100644
--- a/src/opt/mfs/mfsInt.h
+++ b/src/opt/mfs/mfsInt.h
@@ -83,6 +83,7 @@ struct Mfs_Man_t_
     int                 nMintsCare;
     int                 nMintsTotal;
     int                 nNodesBad;
+    int                 nTotalDivs;
     // node/edge stats
     int                 nTotalNodesBeg;
     int                 nTotalNodesEnd;
diff --git a/src/opt/mfs/mfsMan.c b/src/opt/mfs/mfsMan.c
index 768e5295..421f62af 100644
--- a/src/opt/mfs/mfsMan.c
+++ b/src/opt/mfs/mfsMan.c
@@ -115,8 +115,8 @@ void Mfs_ManPrint( Mfs_Man_t * p )
             p->nTotalEdgesBeg-p->nTotalEdgesEnd, 
             100.0*(p->nTotalEdgesBeg-p->nTotalEdgesEnd)/p->nTotalEdgesBeg );
         printf( "\n" );
-        printf( "Nodes = %d. Tried = %d. Resub = %d. Skipped = %d. SAT calls = %d.\n", 
-            Abc_NtkNodeNum(p->pNtk), p->nNodesTried, p->nNodesResub, p->nNodesBad, p->nSatCalls );
+        printf( "Nodes = %d. Tried = %d. Resub = %d. Divs = %d. SAT calls = %d.\n", 
+            Abc_NtkNodeNum(p->pNtk), p->nNodesTried, p->nNodesResub, p->nTotalDivs, p->nSatCalls );
         if ( p->pPars->fSwapEdge )
             printf( "Swappable edges = %d. Total edges = %d. Ratio = %5.2f.\n", 
                 p->nNodesResub, Abc_NtkGetTotalFanins(p->pNtk), 1.00 * p->nNodesResub / Abc_NtkGetTotalFanins(p->pNtk) );