1 files changed, 5 insertions, 12 deletions

diff --git a/src/aig/saig/saigGlaPba.c b/src/aig/saig/saigGlaPba.c
index 5834db76..cdbc05c7 100644
--- a/src/aig/saig/saigGlaPba.c
+++ b/src/aig/saig/saigGlaPba.c
@@ -432,11 +432,10 @@ Vec_Int_t * Saig_AbsSolverUnsatCore( sat_solver * pSat, int nConfMax, int fVerbo
     Vec_Int_t * vCore;
     void * pSatCnf; 
     Intp_Man_t * pManProof;
-    int RetValue;
+    int RetValue, clk = clock();
     if ( piRetValue )
         *piRetValue = -1;
     // solve the problem
-    Abc_Clock(2,1);
     RetValue = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfMax, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
     if ( RetValue == l_Undef )
     {
@@ -453,19 +452,19 @@ Vec_Int_t * Saig_AbsSolverUnsatCore( sat_solver * pSat, int nConfMax, int fVerbo
     if ( fVerbose )
     {
         printf( "SAT solver returned UNSAT after %7d conflicts.      ", pSat->stats.conflicts );
-        ABC_PRT( "Time", (Abc_Clock(2,0)/ABC_CPS)*CLOCKS_PER_SEC );
+        Abc_PrintTime( 1, "Time", clock() - clk );
     }
     assert( RetValue == l_False );
     pSatCnf = sat_solver_store_release( pSat ); 
     // derive the UNSAT core
-    Abc_Clock(2,1);
+    clk = clock();
     pManProof = Intp_ManAlloc();
     vCore = (Vec_Int_t *)Intp_ManUnsatCore( pManProof, (Sto_Man_t *)pSatCnf, 0 );
     Intp_ManFree( pManProof );
     if ( fVerbose )
     {
-        printf( "SAT core contains %8d clauses (out of %8d).   ", Vec_IntSize(vCore), ((Sto_Man_t *)pSatCnf)->nRoots );
-        ABC_PRT( "Time", (Abc_Clock(2,0)/ABC_CPS)*CLOCKS_PER_SEC );
+        printf( "SAT core contains %8d clauses (out of %8d).   ", Vec_IntSize(vCore), sat_solver_nclauses(pSat) );
+        Abc_PrintTime( 1, "Time", clock() - clk );
     }
     Sto_ManFree( (Sto_Man_t *)pSatCnf );
     return vCore;
@@ -561,7 +560,6 @@ Vec_Int_t * Aig_Gla2ManPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, in
     int clk, clk2 = clock();
     assert( Saig_ManPoNum(pAig) == 1 );
 
-    Abc_Clock(0,1); 
     if ( fVerbose )
     {
         if ( TimeLimit )
@@ -572,7 +570,6 @@ Vec_Int_t * Aig_Gla2ManPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, in
 
     // start the solver
     clk = clock();
-    Abc_Clock(1,1); 
     p = Aig_Gla2ManStart( pAig, nStart, nFramesMax, fVerbose );
     if ( !Aig_Gla2CreateSatSolver( p ) )
     {
@@ -581,7 +578,6 @@ Vec_Int_t * Aig_Gla2ManPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, in
         return NULL;
     }
     sat_solver_set_random( p->pSat, fSkipRand );
-//    p->timePre += (Abc_Clock(1,0)/ABC_CPS)*CLOCKS_PER_SEC;
     p->timePre += clock() - clk;
 
     // set runtime limit
@@ -590,15 +586,12 @@ Vec_Int_t * Aig_Gla2ManPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, in
 
     // compute UNSAT core
     clk = clock();
-    Abc_Clock(1,1); 
     vCore = Saig_AbsSolverUnsatCore( p->pSat, nConfLimit, fVerbose, NULL );
     if ( vCore == NULL )
     {
         Aig_Gla2ManStop( p );
         return NULL;
     }
-//    p->timeSat += (Abc_Clock(1,0)/ABC_CPS)*CLOCKS_PER_SEC;
-//    p->timeTotal = (Abc_Clock(0,0)/ABC_CPS)*CLOCKS_PER_SEC;
     p->timeSat += clock() - clk;
     p->timeTotal += clock() - clk2;