summaryrefslogtreecommitdiffstats
path: root/src/proof/pdr
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof/pdr')
-rw-r--r--src/proof/pdr/pdrCore.c2
-rw-r--r--src/proof/pdr/pdrMan.c2
2 files changed, 2 insertions, 2 deletions
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c
index 43cc4527..afcb45b4 100644
--- a/src/proof/pdr/pdrCore.c
+++ b/src/proof/pdr/pdrCore.c
@@ -839,7 +839,7 @@ int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars )
int RetValue;
clock_t clk = clock();
if ( pPars->nTimeOutOne )
- pPars->nTimeOut = pPars->nTimeOutOne * Saig_ManPoNum(pAig);
+ pPars->nTimeOut = pPars->nTimeOutOne * Saig_ManPoNum(pAig) / 1000 + 1;
if ( pPars->nTimeOutOne && !pPars->fSolveAll )
pPars->nTimeOutOne = 0;
if ( pPars->fVerbose )
diff --git a/src/proof/pdr/pdrMan.c b/src/proof/pdr/pdrMan.c
index 51be5e17..ef930beb 100644
--- a/src/proof/pdr/pdrMan.c
+++ b/src/proof/pdr/pdrMan.c
@@ -79,7 +79,7 @@ Pdr_Man_t * Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrio
int i;
p->pTime4Outs = ABC_ALLOC( clock_t, Saig_ManPoNum(pAig) );
for ( i = 0; i < Saig_ManPoNum(pAig); i++ )
- p->pTime4Outs[i] = pPars->nTimeOutOne * CLOCKS_PER_SEC;
+ p->pTime4Outs[i] = pPars->nTimeOutOne * CLOCKS_PER_SEC / 1000 + 1;
}
if ( pPars->fSolveAll )
{