summaryrefslogtreecommitdiffstats
path: root/src/aig/gia/giaAbsVta.c
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2012-07-07 17:46:54 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2012-07-07 17:46:54 -0700
commit3aab7245738a69f1dd4d898493d5dabf6596ea61 (patch)
tree16a23107ca27a250e82c492dcdd1a2bea640cff6 /src/aig/gia/giaAbsVta.c
parent16d96fcf533fb77ff4a45992991e38ac7ea74bb3 (diff)
downloadabc-3aab7245738a69f1dd4d898493d5dabf6596ea61.tar.gz
abc-3aab7245738a69f1dd4d898493d5dabf6596ea61.tar.bz2
abc-3aab7245738a69f1dd4d898493d5dabf6596ea61.zip
Fixing time primtouts throughout the code.
Diffstat (limited to 'src/aig/gia/giaAbsVta.c')
-rw-r--r--src/aig/gia/giaAbsVta.c6
1 files changed, 3 insertions, 3 deletions
diff --git a/src/aig/gia/giaAbsVta.c b/src/aig/gia/giaAbsVta.c
index 7b66b7dd..11c84853 100644
--- a/src/aig/gia/giaAbsVta.c
+++ b/src/aig/gia/giaAbsVta.c
@@ -1564,7 +1564,7 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
p = Vga_ManStart( pAig, pPars );
// set runtime limit
if ( p->pPars->nTimeOut )
- sat_solver2_set_runtime_limit( p->pSat, time(NULL) + p->pPars->nTimeOut - 1 );
+ sat_solver2_set_runtime_limit( p->pSat, p->pPars->nTimeOut * CLOCKS_PER_SEC + clock() );
// perform initial abstraction
if ( p->pPars->fVerbose )
{
@@ -1609,7 +1609,7 @@ int Gia_VtaPerformInt( Gia_Man_t * pAig, Gia_ParVta_t * pPars )
goto finish;
}
// check timeout
- if ( p->pSat->nRuntimeLimit && time(NULL) > p->pSat->nRuntimeLimit )
+ if ( p->pSat->nRuntimeLimit && clock() > p->pSat->nRuntimeLimit )
{
Vga_ManRollBack( p, nObjOld );
goto finish;
@@ -1716,7 +1716,7 @@ finish:
pAig->vObjClasses = Gia_VtaFramesToAbs( (Vec_Vec_t *)p->vCores );
if ( Status == -1 )
{
- if ( p->pPars->nTimeOut && time(NULL) >= p->pSat->nRuntimeLimit )
+ if ( p->pPars->nTimeOut && clock() >= p->pSat->nRuntimeLimit )
Abc_Print( 1, "SAT solver ran out of time at %d sec in frame %d. ", p->pPars->nTimeOut, f );
else if ( pPars->nConfLimit && sat_solver2_nconflicts(p->pSat) >= pPars->nConfLimit )
Abc_Print( 1, "SAT solver ran out of resources at %d conflicts in frame %d. ", pPars->nConfLimit, f );