diff --git a/src/base/abci/abcOdc.c b/src/base/abci/abcOdc.c
index 23915b1e82..cb63b61a48 100644
--- a/src/base/abci/abcOdc.c
+++ b/src/base/abci/abcOdc.c
@@ -243,7 +243,9 @@ Odc_Man_t * Abc_NtkDontCareAlloc( int nVarsMax, int nLevels, int fVerbose, int f
 ***********************************************************************/
 void Abc_NtkDontCareClear( Odc_Man_t * p )
 {
-    abctime clk = Abc_Clock();
+    int fVerbose = p->fVerbose;
+    abctime clk;
+    ABC_TIME_START(fVerbose, clk);
     // clean the structural hashing table
     if ( Vec_IntSize(p->vUsedSpots) > p->nTableSize/3 ) // more than one third
         memset( p->pTable, 0, sizeof(Odc_Lit_t) * p->nTableSize );
@@ -259,7 +261,7 @@ void Abc_NtkDontCareClear( Odc_Man_t * p )
     // reset the root node
     p->iRoot = 0xffff;
 
-p->timeClean += Abc_Clock() - clk;
+    ABC_TIME_STOP(fVerbose, p->timeClean, clk);
 }
 
 /**Function*************************************************************
@@ -1041,8 +1043,10 @@ int Abc_NtkDontCareSimulateBefore( Odc_Man_t * p, unsigned * puTruth )
 ***********************************************************************/
 int Abc_NtkDontCareCompute( Odc_Man_t * p, Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves, unsigned * puTruth )
 {
+    int fVerbose = p->fVerbose;
     int nMints, RetValue;
-    abctime clk, clkTotal = Abc_Clock();
+    abctime clk, clkTotal;
+    ABC_TIME_START(fVerbose, clkTotal);
 
     p->nWins++;
     
@@ -1054,12 +1058,12 @@ int Abc_NtkDontCareCompute( Odc_Man_t * p, Abc_Obj_t * pNode, Vec_Ptr_t * vLeave
     p->pNode = pNode;
 
     // compute the window
-clk = Abc_Clock();
+    ABC_TIME_START(fVerbose, clk);
     RetValue = Abc_NtkDontCareWindow( p );
-p->timeWin += Abc_Clock() - clk;
+    ABC_TIME_STOP(fVerbose, p->timeWin, clk);
     if ( !RetValue )
     {
-p->timeAbort += Abc_Clock() - clkTotal;
+        ABC_TIME_STOP(fVerbose, p->timeAbort, clkTotal);
         Abc_InfoFill( puTruth, p->nWords );
         p->nWinsEmpty++;        
         return 0;
@@ -1075,14 +1079,14 @@ p->timeAbort += Abc_Clock() - clkTotal;
     }
 
     // transfer the window into the AIG package
-clk = Abc_Clock();
+    ABC_TIME_START(fVerbose, clk);
     Abc_NtkDontCareTransfer( p );
-p->timeMiter += Abc_Clock() - clk;
+    ABC_TIME_STOP(fVerbose, p->timeMiter, clk);
 
     // simulate to estimate the amount of don't-cares
-clk = Abc_Clock();
+    ABC_TIME_START(fVerbose, clk);
     nMints = Abc_NtkDontCareSimulateBefore( p, puTruth );
-p->timeSim += Abc_Clock() - clk;
+    ABC_TIME_STOP(fVerbose, p->timeSim, clk);
     if ( p->fVeryVerbose )
     {
         printf( "AIG = %5d ", Odc_NodeNum(p) );
@@ -1092,7 +1096,7 @@ p->timeSim += Abc_Clock() - clk;
     // if there is less then the given percentage of don't-cares, skip
     if ( 100.0 * (p->nBits - nMints) / p->nBits < 1.0 * p->nPercCutoff )
     {
-p->timeAbort += Abc_Clock() - clkTotal;
+        ABC_TIME_STOP(fVerbose, p->timeAbort, clkTotal);
         if ( p->fVeryVerbose )
             printf( "Simulation cutoff.\n" );
         Abc_InfoFill( puTruth, p->nWords );
@@ -1101,12 +1105,12 @@ p->timeAbort += Abc_Clock() - clkTotal;
     }
 
     // quantify external variables
-clk = Abc_Clock();
+    ABC_TIME_START(fVerbose, clk);
     RetValue = Abc_NtkDontCareQuantify( p );
-p->timeQuant += Abc_Clock() - clk;
+    ABC_TIME_STOP(fVerbose, p->timeQuant, clk);
     if ( !RetValue )
     {
-p->timeAbort += Abc_Clock() - clkTotal;
+        ABC_TIME_STOP(fVerbose, p->timeAbort, clkTotal);
         if ( p->fVeryVerbose )
             printf( "=== Overflow! ===\n" );
         Abc_InfoFill( puTruth, p->nWords );
@@ -1115,17 +1119,17 @@ p->timeAbort += Abc_Clock() - clkTotal;
     }
 
     // get the truth table
-clk = Abc_Clock();
+    ABC_TIME_START(fVerbose, clk);
     Abc_NtkDontCareSimulateSetElem( p );
     nMints = Abc_NtkDontCareSimulate( p, puTruth );
-p->timeTruth += Abc_Clock() - clk;
+    ABC_TIME_STOP(fVerbose, p->timeTruth, clk);
     if ( p->fVeryVerbose )
     {
         printf( "AIG = %5d ", Odc_NodeNum(p) );
         printf( "%6.2f %%  ", 100.0 * (p->nBits - nMints) / p->nBits );
         printf( "\n" );
     }
-p->timeTotal += Abc_Clock() - clkTotal;
+    ABC_TIME_STOP(fVerbose, p->timeTotal, clkTotal);
     p->nWinsFinish++;
     p->nTotalDcs += (int)(100.0 * (p->nBits - nMints) / p->nBits);
     return nMints;
diff --git a/src/base/abci/abcRefactor.c b/src/base/abci/abcRefactor.c
index ee034c951b..a5c877055e 100644
--- a/src/base/abci/abcRefactor.c
+++ b/src/base/abci/abcRefactor.c
@@ -168,9 +168,9 @@ Dec_Graph_t * Abc_NodeRefactor( Abc_ManRef_t * p, Abc_Obj_t * pNode, Vec_Ptr_t *
     Required = fUpdateLevel? Abc_ObjRequiredLevel(pNode) : ABC_INFINITY;
 
     // get the function of the cut
-clk = Abc_Clock();
+    ABC_TIME_START(fVerbose, clk);
     pTruth = Abc_NodeConeTruth( p->vVars, p->vFuncs, nWordsMax, pNode, vFanins, p->vVisited );
-p->timeTru += Abc_Clock() - clk;
+    ABC_TIME_STOP(fVerbose, p->timeTru, clk);
     if ( pTruth == NULL )
         return NULL;
 
@@ -184,9 +184,9 @@ p->timeTru += Abc_Clock() - clk;
     }
 
     // get the factored form
-clk = Abc_Clock();
+    ABC_TIME_START(fVerbose, clk);
     pFForm = (Dec_Graph_t *)Kit_TruthToGraph( (unsigned *)pTruth, nVars, p->vMemory );
-p->timeFact += Abc_Clock() - clk;
+    ABC_TIME_STOP(fVerbose, p->timeFact, clk);
 
     // mark the fanin boundary 
     // (can mark only essential fanins, belonging to bNodeFunc!)
@@ -203,9 +203,9 @@ p->timeFact += Abc_Clock() - clk;
     }
 
     // detect how many new nodes will be added (while taking into account reused nodes)
-clk = Abc_Clock();
+    ABC_TIME_START(fVerbose, clk);
     nNodesAdded = Dec_GraphToNetworkCount( pNode, pFForm, nNodesSaved, Required );
-p->timeEval += Abc_Clock() - clk;
+    ABC_TIME_STOP(fVerbose, p->timeEval, clk);
     // quit if there is no improvement
     //if ( nNodesAdded == -1 || (nNodesAdded == nNodesSaved && !fUseZeros) )
     if ( nNodesAdded == -1 || nNodesSaved - nNodesAdded < nMinSaved )
@@ -335,9 +335,10 @@ int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nMinSaved, int nCon
     Dec_Graph_t * pFForm;
     Vec_Ptr_t * vFanins;
     Abc_Obj_t * pNode;
-    abctime clk, clkStart = Abc_Clock();
+    abctime clk, clkStart;
     int i, nNodes, RetValue = 1;
 
+    ABC_TIME_START(fVerbose, clkStart);
     assert( Abc_NtkIsStrash(pNtk) );
     // cleanup the AIG
     Abc_AigCleanup((Abc_Aig_t *)pNtk->pManFunc);
@@ -369,28 +370,28 @@ int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nMinSaved, int nCon
         if ( i >= nNodes )
             break;
         // compute a reconvergence-driven cut
-clk = Abc_Clock();
+        ABC_TIME_START(fVerbose, clk);
         vFanins = Abc_NodeFindCut( pManCut, pNode, fUseDcs );
-pManRef->timeCut += Abc_Clock() - clk;
+        ABC_TIME_STOP(fVerbose, pManRef->timeCut, clk);
         // evaluate this cut
-clk = Abc_Clock();
+        ABC_TIME_START(fVerbose, clk);
         pFForm = Abc_NodeRefactor( pManRef, pNode, vFanins, nMinSaved, fUpdateLevel, fUseZeros, fUseDcs, fVerbose );
-pManRef->timeRes += Abc_Clock() - clk;
+        ABC_TIME_STOP(fVerbose, pManRef->timeRes, clk);
         if ( pFForm == NULL )
             continue;
         // acceptable replacement found, update the graph
-clk = Abc_Clock();
+        ABC_TIME_START(fVerbose, clk);
         if ( !Dec_GraphUpdateNetwork( pNode, pFForm, fUpdateLevel, pManRef->nLastGain ) )
         {
             Dec_GraphFree( pFForm );
             RetValue = -1;
             break;
         }
-pManRef->timeNtk += Abc_Clock() - clk;
+        ABC_TIME_STOP(fVerbose, pManRef->timeNtk, clk);
         Dec_GraphFree( pFForm );
     }
     Extra_ProgressBarStop( pProgress );
-pManRef->timeTotal = Abc_Clock() - clkStart;
+    ABC_TIME_STOP(fVerbose, pManRef->timeTotal, clkStart);
     pManRef->nNodesEnd = Abc_NtkNodeNum(pNtk);
 
     // print statistics of the manager
diff --git a/src/base/abci/abcResub.c b/src/base/abci/abcResub.c
index b7b8dbbd0a..eff0a5e455 100644
--- a/src/base/abci/abcResub.c
+++ b/src/base/abci/abcResub.c
@@ -211,10 +211,10 @@ int Abc_NtkResubstitute( Abc_Ntk_t * pNtk, int nCutMax, int nStepsMax, int nMinS
             break;
 
         // compute a reconvergence-driven cut
-clk = Abc_Clock();
+        ABC_TIME_START(fVerbose, clk);
         vLeaves = Abc_NodeFindCut( pManCut, pNode, 0 );
 //        vLeaves = Abc_CutFactorLarge( pNode, nCutMax );
-pManRes->timeCut += Abc_Clock() - clk;
+        ABC_TIME_STOP(fVerbose, pManRes->timeCut, clk);
 /*
         if ( fVerbose && vLeaves )
         printf( "Node %6d : Leaves = %3d. Volume = %3d.\n", pNode->Id, Vec_PtrSize(vLeaves), Abc_CutVolumeCheck(pNode, vLeaves) );
@@ -224,18 +224,18 @@ pManRes->timeCut += Abc_Clock() - clk;
         // get the don't-cares
         if ( pManOdc )
         {
-clk = Abc_Clock();
+            ABC_TIME_START(fVerbose, clk);
             Abc_NtkDontCareClear( pManOdc );
             Abc_NtkDontCareCompute( pManOdc, pNode, vLeaves, pManRes->pCareSet );
-pManRes->timeTruth += Abc_Clock() - clk;
+            ABC_TIME_STOP(fVerbose, pManRes->timeTruth, clk);
         }
 
         // evaluate this cut
-clk = Abc_Clock();
+        ABC_TIME_START(fVerbose, clk);
         pFForm = Abc_ManResubEval( pManRes, pNode, vLeaves, nStepsMax, fUpdateLevel, fVerbose );
 //        Vec_PtrFree( vLeaves );
 //        Abc_ManResubCleanup( pManRes );
-pManRes->timeRes += Abc_Clock() - clk;
+        ABC_TIME_STOP(fVerbose, pManRes->timeRes, clk);
         if ( pFForm == NULL )
             continue;
         if ( pManRes->nLastGain < nMinSaved )
@@ -254,9 +254,9 @@ pManRes->timeRes += Abc_Clock() - clk;
         }
 */
         // acceptable replacement found, update the graph
-clk = Abc_Clock();
+        ABC_TIME_START(fVerbose, clk);
         Dec_GraphUpdateNetwork( pNode, pFForm, fUpdateLevel, pManRes->nLastGain );
-pManRes->timeNtk += Abc_Clock() - clk;
+        ABC_TIME_STOP(fVerbose, pManRes->timeNtk, clk);
         Dec_GraphFree( pFForm );
     }
     Extra_ProgressBarStop( pProgress );
@@ -1958,24 +1958,24 @@ Dec_Graph_t * Abc_ManResubEval( Abc_ManRes_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t *
     p->nLastGain = -1;
 
     // collect the MFFC
-clk = Abc_Clock();
+    ABC_TIME_START(fVerbose, clk);
     p->nMffc = Abc_NodeMffcInside( pRoot, vLeaves, p->vTemp );
-p->timeMffc += Abc_Clock() - clk;
+    ABC_TIME_STOP(fVerbose, p->timeMffc, clk);
     assert( p->nMffc > 0 );
 
     // collect the divisor nodes
-clk = Abc_Clock();
+    ABC_TIME_START(fVerbose, clk);
     if ( !Abc_ManResubCollectDivs( p, pRoot, vLeaves, Required ) )
         return NULL;
-    p->timeDiv += Abc_Clock() - clk;
+    ABC_TIME_STOP(fVerbose, p->timeDiv, clk);
 
     p->nTotalDivs   += p->nDivs;
     p->nTotalLeaves += p->nLeaves;
 
     // simulate the nodes
-clk = Abc_Clock();
+    ABC_TIME_START(fVerbose, clk);
     Abc_ManResubSimulate( p->vDivs, p->nLeaves, p->vSims, p->nLeavesMax, p->nWords );
-p->timeSim += Abc_Clock() - clk;
+    ABC_TIME_STOP(fVerbose, p->timeSim, clk);
 
     if ( p->pFile && Vec_PtrSize(vLeaves) != p->nLeavesMax && p->nProbs < (1 << p->Log2Probs) ) 
     {
@@ -2003,7 +2003,7 @@ p->timeSim += Abc_Clock() - clk;
         return NULL;
     }
 
-clk = Abc_Clock();
+    ABC_TIME_START(fVerbose, clk);
     // consider constants
     if ( (pGraph = Abc_ManResubQuit( p )) )
     {
@@ -2015,14 +2015,14 @@ clk = Abc_Clock();
     // consider equal nodes
     if ( (pGraph = Abc_ManResubDivs0( p )) )
     {
-p->timeRes1 += Abc_Clock() - clk;
+        ABC_TIME_STOP(fVerbose, p->timeRes1, clk);
         p->nUsedNode0++;
         p->nLastGain = p->nMffc;
         return pGraph;
     }
     if ( nSteps == 0 || p->nMffc == 1 )
     {
-p->timeRes1 += Abc_Clock() - clk;
+        ABC_TIME_STOP(fVerbose, p->timeRes1, clk);
         return NULL;
     }
 
@@ -2035,50 +2035,50 @@ p->timeRes1 += Abc_Clock() - clk;
     // consider one node
     if ( (pGraph = Abc_ManResubDivs1( p, Required )) )
     {
-p->timeRes1 += Abc_Clock() - clk;
+        ABC_TIME_STOP(fVerbose, p->timeRes1, clk);
         p->nLastGain = p->nMffc - 1;
         return pGraph;
     }
-p->timeRes1 += Abc_Clock() - clk;
+    ABC_TIME_STOP(fVerbose, p->timeRes1, clk);
     if ( nSteps == 1 || p->nMffc == 2 )
         return NULL;
 
-clk = Abc_Clock();
+    ABC_TIME_START(fVerbose, clk);
     // consider triples
     if ( (pGraph = Abc_ManResubDivs12( p, Required )) )
     {
-p->timeRes2 += Abc_Clock() - clk;
+        ABC_TIME_STOP(fVerbose, p->timeRes2, clk);
         p->nLastGain = p->nMffc - 2;
         return pGraph;
     }
-p->timeRes2 += Abc_Clock() - clk;
+    ABC_TIME_STOP(fVerbose, p->timeRes2, clk);
 
     // get the two level divisors
-clk = Abc_Clock();
+    ABC_TIME_START(fVerbose, clk);
     Abc_ManResubDivsD( p, Required );
-p->timeResD += Abc_Clock() - clk;
+    ABC_TIME_STOP(fVerbose, p->timeResD, clk);
 
     // consider two nodes
-clk = Abc_Clock();
+    ABC_TIME_START(fVerbose, clk);
     if ( (pGraph = Abc_ManResubDivs2( p, Required )) )
     {
-p->timeRes2 += Abc_Clock() - clk;
+        ABC_TIME_STOP(fVerbose, p->timeRes2, clk);
         p->nLastGain = p->nMffc - 2;
         return pGraph;
     }
-p->timeRes2 += Abc_Clock() - clk;
+    ABC_TIME_STOP(fVerbose, p->timeRes2, clk);
     if ( nSteps == 2 || p->nMffc == 3 )
         return NULL;
 
     // consider two nodes
-clk = Abc_Clock();
+    ABC_TIME_START(fVerbose, clk);
     if ( (pGraph = Abc_ManResubDivs3( p, Required )) )
     {
-p->timeRes3 += Abc_Clock() - clk;
+        ABC_TIME_STOP(fVerbose, p->timeRes3, clk);
         p->nLastGain = p->nMffc - 3;
         return pGraph;
     }
-p->timeRes3 += Abc_Clock() - clk;
+    ABC_TIME_STOP(fVerbose, p->timeRes3, clk);
     if ( nSteps == 3 || p->nLeavesMax == 4 )
         return NULL;
     return NULL;
diff --git a/src/misc/util/abc_global.h b/src/misc/util/abc_global.h
index fbe299da62..81339a8ef5 100644
--- a/src/misc/util/abc_global.h
+++ b/src/misc/util/abc_global.h
@@ -421,6 +421,15 @@ static inline abctime Abc_ThreadClock()
 #endif
 }
 
+// stopwatch timing for verbose statistics
+#if defined(ABC_NO_TIMERS)
+    #define ABC_TIME_START(cond, clk)          do { (void)(clk); } while (0)
+    #define ABC_TIME_STOP(cond, acc, clk)      do { (void)(clk); } while (0)
+#else
+    #define ABC_TIME_START(cond, clk)          do { clk = (cond) ? Abc_Clock() : 0; } while (0)
+    #define ABC_TIME_STOP(cond, acc, clk)      do { if (cond) acc += Abc_Clock() - clk; } while (0)
+#endif
+
 // misc printing procedures
 enum Abc_VerbLevel
 {
diff --git a/src/opt/cut/cutNode.c b/src/opt/cut/cutNode.c
index 11810c3396..726fe65316 100644
--- a/src/opt/cut/cutNode.c
+++ b/src/opt/cut/cutNode.c
@@ -368,6 +368,7 @@ static inline int Cut_CutProcessTwo( Cut_Man_t * p, Cut_Cut_t * pCut0, Cut_Cut_t
 ***********************************************************************/
 Cut_Cut_t * Cut_NodeComputeCuts( Cut_Man_t * p, int Node, int Node0, int Node1, int fCompl0, int fCompl1, int fTriv, int TreeCode )
 {
+    int fVerbose = p->pParams->fVerbose;
     Cut_List_t Super, * pSuper = &Super;
     Cut_Cut_t * pList, * pCut;
     abctime clk;
@@ -381,11 +382,11 @@ Cut_Cut_t * Cut_NodeComputeCuts( Cut_Man_t * p, int Node, int Node0, int Node1,
         Cut_CutNumberList( Cut_NodeReadCutsNew(p, Node1) );
     }
     // compute the cuts
-clk = Abc_Clock();
+    ABC_TIME_START(fVerbose, clk);
     Cut_ListStart( pSuper );
     Cut_NodeDoComputeCuts( p, pSuper, Node, fCompl0, fCompl1, Cut_NodeReadCutsNew(p, Node0), Cut_NodeReadCutsNew(p, Node1), fTriv, TreeCode );
     pList = Cut_ListFinish( pSuper );
-p->timeMerge += Abc_Clock() - clk;
+    ABC_TIME_STOP(fVerbose, p->timeMerge, clk);
     // verify the result of cut computation
 //    Cut_CutListVerify( pList );
     // performing the recording
@@ -419,7 +420,7 @@ p->timeMerge += Abc_Clock() - clk;
 //        Cut_CutFilter( p, pList0 );
 //p->timeFilter += Abc_Clock() - clk;
     // perform mapping of this node with these cuts
-clk = Abc_Clock();
+    ABC_TIME_START(fVerbose, clk);
     if ( p->pParams->fMap && !p->pParams->fSeq )
     {
 //        int Delay1, Delay2;
@@ -428,7 +429,7 @@ clk = Abc_Clock();
 //        assert( Delay1 >= Delay2 );
         Cut_NodeMapping( p, pList, Node, Node0, Node1 );
     }
-p->timeMap += Abc_Clock() - clk;
+    ABC_TIME_STOP(fVerbose, p->timeMap, clk);
     return pList;
 }
 
@@ -677,11 +678,13 @@ void Cut_NodeDoComputeCuts( Cut_Man_t * p, Cut_List_t * pSuper, int Node, int fC
 ***********************************************************************/
 Cut_Cut_t * Cut_NodeUnionCuts( Cut_Man_t * p, Vec_Int_t * vNodes )
 {
+    int fVerbose = p->pParams->fVerbose;
     Cut_List_t Super, * pSuper = &Super;
     Cut_Cut_t * pList, * pListStart, * pCut, * pCut2;
     Cut_Cut_t * pTop = NULL; // Suppress "might be used uninitialized"
     int i, k, Node, Root, Limit = p->pParams->nVarsMax;
-    abctime clk = Abc_Clock();
+    abctime clk;
+    ABC_TIME_START(fVerbose, clk);
 
     // start the new list
     Cut_ListStart( pSuper );
@@ -771,7 +774,7 @@ finish :
     assert( Cut_NodeReadCutsNew(p, Root) == NULL );
     pList = Cut_ListFinish( pSuper );
     Cut_NodeWriteCutsNew( p, Root, pList );
-p->timeUnion += Abc_Clock() - clk;
+    ABC_TIME_STOP(fVerbose, p->timeUnion, clk);
     // filter the cuts
 //clk = Abc_Clock();
 //    if ( p->pParams->fFilter )
diff --git a/src/opt/dar/darCore.c b/src/opt/dar/darCore.c
index f050ced183..a9e4a0c732 100644
--- a/src/opt/dar/darCore.c
+++ b/src/opt/dar/darCore.c
@@ -79,6 +79,7 @@ void Dar_ManDefaultRwrParams( Dar_RwrPar_t * pPars )
 int Dar_ManRewrite( Aig_Man_t * pAig, Dar_RwrPar_t * pPars )
 {
     extern Vec_Int_t * Saig_ManComputeSwitchProbs( Aig_Man_t * p, int nFrames, int nPref, int fProbOne );
+    int fVerbose = pPars->fVerbose;
     Dar_Man_t * p;
 //    Bar_Progress_t * pProgress;
     Dar_Cut_t * pCut;
@@ -138,10 +139,10 @@ int Dar_ManRewrite( Aig_Man_t * pAig, Dar_RwrPar_t * pPars )
 
         // compute cuts for the node
         p->nNodesTried++;
-clk = Abc_Clock();
+        ABC_TIME_START(fVerbose, clk);
         Dar_ObjSetCuts( pObj, NULL );
         Dar_ObjComputeCuts_rec( p, pObj );
-p->timeCuts += Abc_Clock() - clk;
+        ABC_TIME_STOP(fVerbose, p->timeCuts, clk);
 
         // check if there is a trivial cut
         Dar_ObjForEachCut( pObj, pCut, k )
diff --git a/src/opt/dar/darLib.c b/src/opt/dar/darLib.c
index 51bf1d434a..429f4a5446 100644
--- a/src/opt/dar/darLib.c
+++ b/src/opt/dar/darLib.c
@@ -934,12 +934,14 @@ int Dar_LibEval_rec( Dar_Lib_t * pLib, Dar_LibObj_t * pObj, int Out, int nNodesS
 ***********************************************************************/
 void Dar_LibEval( Dar_Man_t * p, Aig_Obj_t * pRoot, Dar_Cut_t * pCut, int Required, int * pnMffcSize )
 {
+    int fVerbose = p->pPars->fVerbose;
     Dar_Lib_t * pLib = s_DarLib;
     int fTraining = 0;
     float PowerSaved, PowerAdded;
     Dar_LibObj_t * pObj;
     int Out, k, Class, nNodesSaved, nNodesAdded, nNodesGained;
-    abctime clk = Abc_Clock();
+    abctime clk;
+    ABC_TIME_START(fVerbose, clk);
     if ( pCut->nLeaves != 4 )
         return;
     // check if the cut exits and assigns leaves and their levels
@@ -981,9 +983,12 @@ void Dar_LibEval( Dar_Man_t * p, Aig_Obj_t * pRoot, Dar_Cut_t * pCut, int Requir
         assert( p->LevelBest <= Required );
         *pnMffcSize   = nNodesSaved;
     }
-clk = Abc_Clock() - clk;
-p->ClassTimes[Class] += clk;
-p->timeEval += clk;
+    if ( fVerbose )
+    {
+        clk = Abc_Clock() - clk;
+        p->timeEval += clk;
+        p->ClassTimes[Class] += clk;
+    }
 }
 
 /**Function*************************************************************
diff --git a/src/opt/dar/darRefact.c b/src/opt/dar/darRefact.c
index 8016568a14..d0d994fea6 100644
--- a/src/opt/dar/darRefact.c
+++ b/src/opt/dar/darRefact.c
@@ -496,6 +496,7 @@ int Dar_ObjCutLevelAchieved( Vec_Ptr_t * vCut, int nLevelMin )
 int Dar_ManRefactor( Aig_Man_t * pAig, Dar_RefPar_t * pPars )
 {
 //    Bar_Progress_t * pProgress;
+    int fVerbose = pPars->fVerbose;
     Ref_Man_t * p;
     Vec_Ptr_t * vCut, * vCut2;
     Aig_Obj_t * pObj, * pObjNew;
@@ -532,12 +533,12 @@ int Dar_ManRefactor( Aig_Man_t * pAig, Dar_RefPar_t * pPars )
 
 //printf( "\nConsidering node %d.\n", pObj->Id );
         // get the bounded MFFC size
-clk = Abc_Clock();
+        ABC_TIME_START(fVerbose, clk);
         nLevelMin = Abc_MaxInt( 0, Aig_ObjLevel(pObj) - 10 );
         nNodesSaved = Aig_NodeMffcSupp( pAig, pObj, nLevelMin, vCut );
         if ( nNodesSaved < p->pPars->nMffcMin ) // too small to consider
         {
-p->timeCuts += Abc_Clock() - clk;
+            ABC_TIME_STOP(fVerbose, p->timeCuts, clk);
             continue; 
         }
         p->nNodesTried++;
@@ -566,13 +567,13 @@ p->timeCuts += Abc_Clock() - clk;
             else
                 p->nNodesBelow++;
         }
-p->timeCuts += Abc_Clock() - clk;
+        ABC_TIME_STOP(fVerbose, p->timeCuts, clk);
 
         // try the cuts
-clk = Abc_Clock();
+        ABC_TIME_START(fVerbose, clk);
         Required = pAig->vLevelR? Aig_ObjRequiredLevel(pAig, pObj) : ABC_INFINITY;
         Dar_ManRefactorTryCuts( p, pObj, nNodesSaved, Required );
-p->timeEval += Abc_Clock() - clk;
+        ABC_TIME_STOP(fVerbose, p->timeEval, clk);
 
         // check the best gain
         if ( !(p->GainBest > 0 || (p->GainBest == 0 && p->pPars->fUseZeros)) )
diff --git a/src/opt/mfs/mfsCore.c b/src/opt/mfs/mfsCore.c
index 20ff1f1ad6..12b786d19a 100644
--- a/src/opt/mfs/mfsCore.c
+++ b/src/opt/mfs/mfsCore.c
@@ -235,36 +235,37 @@ void Abc_NtkMfsPowerResub( Mfs_Man_t * p, Mfs_Par_t * pPars)
 ***********************************************************************/
 int Abc_NtkMfsResub( Mfs_Man_t * p, Abc_Obj_t * pNode )
 {
+    int fVerbose = p->pPars->fVerbose;
     abctime clk;
     p->nNodesTried++;
     // prepare data structure for this node
     Mfs_ManClean( p );
     // compute window roots, window support, and window nodes
-clk = Abc_Clock();
+    ABC_TIME_START(fVerbose, clk);
     p->vRoots = Abc_MfsComputeRoots( pNode, p->pPars->nWinTfoLevs, p->pPars->nFanoutsMax );
     p->vSupp  = Abc_NtkNodeSupport( p->pNtk, (Abc_Obj_t **)Vec_PtrArray(p->vRoots), Vec_PtrSize(p->vRoots) );
     p->vNodes = Abc_NtkDfsNodes( p->pNtk, (Abc_Obj_t **)Vec_PtrArray(p->vRoots), Vec_PtrSize(p->vRoots) );
-p->timeWin += Abc_Clock() - clk;
+    ABC_TIME_STOP(fVerbose, p->timeWin, clk);
     if ( p->pPars->nWinMax && Vec_PtrSize(p->vNodes) > p->pPars->nWinMax )
     {
         p->nMaxDivs++;
         return 1;
     }
     // compute the divisors of the window
-clk = Abc_Clock();
+    ABC_TIME_START(fVerbose, clk);
     p->vDivs  = Abc_MfsComputeDivisors( p, pNode, Abc_ObjRequiredLevel(pNode) - 1 );
     p->nTotalDivs += Vec_PtrSize(p->vDivs) - Abc_ObjFaninNum(pNode);
-p->timeDiv += Abc_Clock() - clk;
+    ABC_TIME_STOP(fVerbose, p->timeDiv, clk);
     // construct AIG for the window
-clk = Abc_Clock();
+    ABC_TIME_START(fVerbose, clk);
     p->pAigWin = Abc_NtkConstructAig( p, pNode );
-p->timeAig += Abc_Clock() - clk;
+    ABC_TIME_STOP(fVerbose, p->timeAig, clk);
     // translate it into CNF
-clk = Abc_Clock();
+    ABC_TIME_START(fVerbose, clk);
     p->pCnf = Cnf_DeriveSimple( p->pAigWin, 1 + Vec_PtrSize(p->vDivs) );
-p->timeCnf += Abc_Clock() - clk;
+    ABC_TIME_STOP(fVerbose, p->timeCnf, clk);
     // create the SAT problem
-clk = Abc_Clock();
+    ABC_TIME_START(fVerbose, clk);
     p->pSat = Abc_MfsCreateSolverResub( p, NULL, 0, 0 );
     if ( p->pSat == NULL )
     {
@@ -286,7 +287,7 @@ clk = Abc_Clock();
         if ( p->pPars->fMoreEffort )
             Abc_NtkMfsResubNode2( p, pNode );
     }
-p->timeSat += Abc_Clock() - clk;
+    ABC_TIME_STOP(fVerbose, p->timeSat, clk);
 //    if ( p->pPars->fGiaSat )
 //        Abc_NtkMfsDeconstructGia( p );
     return 1;
diff --git a/src/opt/rwr/rwrEva.c b/src/opt/rwr/rwrEva.c
index 1856f7b74b..fffcf603d4 100644
--- a/src/opt/rwr/rwrEva.c
+++ b/src/opt/rwr/rwrEva.c
@@ -69,6 +69,7 @@ int Rwr_NodeRewrite( Rwr_Man_t * p, Cut_Man_t * pManCut, Abc_Obj_t * pNode, int
     int Required, nNodesSaved;
     int nNodesSaveCur = -1; // Suppress "might be used uninitialized"
     int i, GainCur = -1, GainBest = -1;
+    int fVerbose = Cut_ManReadParams(pManCut)->fVerbose;
     abctime clk, clk2;//, Counter;
 
     p->nNodesConsidered++;
@@ -76,10 +77,10 @@ int Rwr_NodeRewrite( Rwr_Man_t * p, Cut_Man_t * pManCut, Abc_Obj_t * pNode, int
     Required = fUpdateLevel? Abc_ObjRequiredLevel(pNode) : ABC_INFINITY;
 
     // get the node's cuts
-clk = Abc_Clock();
+    ABC_TIME_START(fVerbose, clk);
     pCut = (Cut_Cut_t *)Abc_NodeGetCutsRecursive( pManCut, pNode, 0, 0 );
     assert( pCut != NULL );
-p->timeCut += Abc_Clock() - clk;
+    ABC_TIME_STOP(fVerbose, p->timeCut, clk);
 
 //printf( " %d", Rwr_CutCountNumNodes(pNode, pCut) );
 /*
@@ -89,7 +90,7 @@ p->timeCut += Abc_Clock() - clk;
     printf( "%d ", Counter );
 */
     // go through the cuts
-clk = Abc_Clock();
+    ABC_TIME_START(fVerbose, clk);
     for ( pCut = pCut->pNext; pCut; pCut = pCut->pNext )
     {
         // consider only 4-input cuts
@@ -128,7 +129,7 @@ clk = Abc_Clock();
                 continue;
         }
 
-clk2 = Abc_Clock();
+        ABC_TIME_START(fVerbose, clk2);
 /*
         printf( "Considering: (" );
         Vec_PtrForEachEntry( Abc_Obj_t *, p->vFaninsCur, pFanin, i )
@@ -145,12 +146,12 @@ clk2 = Abc_Clock();
         // unmark the fanin boundary
         Vec_PtrForEachEntry( Abc_Obj_t *, p->vFaninsCur, pFanin, i )
             Abc_ObjRegular(pFanin)->vFanouts.nSize--;
-p->timeMffc += Abc_Clock() - clk2;
+        ABC_TIME_STOP(fVerbose, p->timeMffc, clk2);
 
         // evaluate the cut
-clk2 = Abc_Clock();
+        ABC_TIME_START(fVerbose, clk2);
         pGraph = Rwr_CutEvaluate( p, pNode, pCut, p->vFaninsCur, nNodesSaved, Required, &GainCur, fPlaceEnable );
-p->timeEval += Abc_Clock() - clk2;
+        ABC_TIME_STOP(fVerbose, p->timeEval, clk2);
 
         // check if the cut is better than the current best one
         if ( pGraph != NULL && GainBest < GainCur )
@@ -167,7 +168,7 @@ p->timeEval += Abc_Clock() - clk2;
                 Vec_PtrPush( p->vFanins, pFanin );
         }
     }
-p->timeRes += Abc_Clock() - clk;
+    ABC_TIME_STOP(fVerbose, p->timeRes, clk);
 
     if ( GainBest == -1 )
         return -1;
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index de3aa792f9..49e148607d 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -1522,13 +1522,15 @@ int sat_solver_simplify(sat_solver* s)
 
 void sat_solver_reducedb(sat_solver* s)
 {
-    abctime clk = Abc_Clock();
+    int fVerbose = s->fVerbose;
+    abctime clk;
     Sat_Mem_t * pMem = &s->Mem;
     int nLearnedOld = veci_size(&s->act_clas);
     int * act_clas = veci_begin(&s->act_clas);
     int * pPerm, * pArray, * pSortValues, nCutoffValue;
     int i, k, j, Id, Counter, CounterStart, nSelected;
     clause * c;
+    ABC_TIME_START(fVerbose, clk);
 
     assert( s->nLearntMax > 0 );
     assert( nLearnedOld == Sat_MemEntryNum(pMem, 1) );
@@ -1628,8 +1630,8 @@ void sat_solver_reducedb(sat_solver* s)
     assert( Counter == (int)s->stats.learnts );
 
     // report the results
-    s->timeReduceDb += Abc_Clock() - clk;
-    if ( s->fVerbose )
+    ABC_TIME_STOP(fVerbose, s->timeReduceDb, clk);
+    if ( fVerbose )
     {
     Abc_Print(1, "reduceDB: Keeping %7d out of %7d clauses (%5.2f %%)  ",
         s->stats.learnts, nLearnedOld, 100.0 * s->stats.learnts / nLearnedOld );