summaryrefslogtreecommitdiffstats
path: root/src/proof/fra/fraIndVer.c
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2013-05-27 15:09:23 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2013-05-27 15:09:23 -0700
commit19c25fd6aab057b2373717f996fe538507c1b1e1 (patch)
tree7aa7cd7609a5de31d11b3455b6388fd9300c8d0f /src/proof/fra/fraIndVer.c
parent94356f0d1fa8e671303299717f631ecf0ca2f17e (diff)
downloadabc-19c25fd6aab057b2373717f996fe538507c1b1e1.tar.gz
abc-19c25fd6aab057b2373717f996fe538507c1b1e1.tar.bz2
abc-19c25fd6aab057b2373717f996fe538507c1b1e1.zip
Adding a wrapper around clock() for more accurate time counting in ABC.
Diffstat (limited to 'src/proof/fra/fraIndVer.c')
-rw-r--r--src/proof/fra/fraIndVer.c4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/proof/fra/fraIndVer.c b/src/proof/fra/fraIndVer.c
index 26b64647..a219ec52 100644
--- a/src/proof/fra/fraIndVer.c
+++ b/src/proof/fra/fraIndVer.c
@@ -50,7 +50,7 @@ int Fra_InvariantVerify( Aig_Man_t * pAig, int nFrames, Vec_Int_t * vClauses, Ve
int * pStart;
int RetValue, Beg, End, i, k;
int CounterBase = 0, CounterInd = 0;
- clock_t clk = clock();
+ abctime clk = Abc_Clock();
if ( nFrames != 1 )
{
@@ -153,7 +153,7 @@ int Fra_InvariantVerify( Aig_Man_t * pAig, int nFrames, Vec_Int_t * vClauses, Ve
if ( CounterBase || CounterInd )
return 0;
printf( "Invariant verification: %d clauses verified correctly. ", Vec_IntSize(vClauses) );
- ABC_PRT( "Time", clock() - clk );
+ ABC_PRT( "Time", Abc_Clock() - clk );
return 1;
}