1 files changed, 13 insertions, 13 deletions

diff --git a/src/proof/ssc/sscSat.c b/src/proof/ssc/sscSat.c
index 1de99c2e..9992f18e 100644
--- a/src/proof/ssc/sscSat.c
+++ b/src/proof/ssc/sscSat.c
@@ -209,12 +209,12 @@ static void Ssc_ManCnfNodeAddToSolver( Ssc_Man_t * p, int NodeId )
 {
     Gia_Obj_t * pNode;
     int i, k, Id, Lit;
-    clock_t clk;
+    abctime clk;
     assert( NodeId > 0 );
     // quit if CNF is ready
     if ( Ssc_ObjSatVar(p, NodeId) )
         return;
-clk = clock();
+clk = Abc_Clock();
     // start the frontier
     Vec_IntClear( p->vFront );
     Ssc_ManCnfAddToFrontier( p, NodeId, p->vFront );
@@ -243,7 +243,7 @@ clk = clock();
         }
         assert( Vec_IntSize(p->vFanins) > 1 );
     }
-p->timeCnfGen += clock() - clk;
+p->timeCnfGen += Abc_Clock() - clk;
 }
 
 
@@ -346,10 +346,10 @@ Vec_Int_t * Ssc_ManFindPivotSat( Ssc_Man_t * p )
 int Ssc_ManCheckEquivalence( Ssc_Man_t * p, int iRepr, int iNode, int fCompl )
 {
     int pLitsSat[2], RetValue;
-    clock_t clk;
+    abctime clk;
     assert( iRepr < iNode );
 //    if ( p->nTimeOut )
-//        sat_solver_set_runtime_limit( p->pSat, p->nTimeOut * CLOCKS_PER_SEC + clock() );
+//        sat_solver_set_runtime_limit( p->pSat, p->nTimeOut * CLOCKS_PER_SEC + Abc_Clock() );
 
     // create CNF
     if ( iRepr )
@@ -363,7 +363,7 @@ int Ssc_ManCheckEquivalence( Ssc_Man_t * p, int iRepr, int iNode, int fCompl )
 
     // solve under assumptions
     // A = 1; B = 0
-    clk = clock();
+    clk = Abc_Clock();
     RetValue = sat_solver_solve( p->pSat, pLitsSat, pLitsSat + 2, (ABC_INT64_T)p->pPars->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
     if ( RetValue == l_False )
     {
@@ -371,17 +371,17 @@ int Ssc_ManCheckEquivalence( Ssc_Man_t * p, int iRepr, int iNode, int fCompl )
         pLitsSat[1] = Abc_LitNot( pLitsSat[1] ); // compl
         RetValue = sat_solver_addclause( p->pSat, pLitsSat, pLitsSat + 2 );
         assert( RetValue );
-        p->timeSatUnsat += clock() - clk;
+        p->timeSatUnsat += Abc_Clock() - clk;
     }
     else if ( RetValue == l_True )
     {
         Ssc_ManCollectSatPattern( p, p->vPattern );
-        p->timeSatSat += clock() - clk;
+        p->timeSatSat += Abc_Clock() - clk;
         return l_True;
     }
     else // if ( RetValue1 == l_Undef )
     {
-        p->timeSatUndec += clock() - clk;
+        p->timeSatUndec += Abc_Clock() - clk;
         return l_Undef;
     }
 
@@ -391,7 +391,7 @@ int Ssc_ManCheckEquivalence( Ssc_Man_t * p, int iRepr, int iNode, int fCompl )
 
     // solve under assumptions
     // A = 0; B = 1
-    clk = clock();
+    clk = Abc_Clock();
     RetValue = sat_solver_solve( p->pSat, pLitsSat, pLitsSat + 2, (ABC_INT64_T)p->pPars->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
     if ( RetValue == l_False )
     {
@@ -399,17 +399,17 @@ int Ssc_ManCheckEquivalence( Ssc_Man_t * p, int iRepr, int iNode, int fCompl )
         pLitsSat[1] = Abc_LitNot( pLitsSat[1] );
         RetValue = sat_solver_addclause( p->pSat, pLitsSat, pLitsSat + 2 );
         assert( RetValue );
-        p->timeSatUnsat += clock() - clk;
+        p->timeSatUnsat += Abc_Clock() - clk;
     }
     else if ( RetValue == l_True )
     {
         Ssc_ManCollectSatPattern( p, p->vPattern );
-        p->timeSatSat += clock() - clk;
+        p->timeSatSat += Abc_Clock() - clk;
         return l_True;
     }
     else // if ( RetValue1 == l_Undef )
     {
-        p->timeSatUndec += clock() - clk;
+        p->timeSatUndec += Abc_Clock() - clk;
         return l_Undef;
     }
     return l_False;