diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-05-03 19:58:25 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-05-03 19:58:25 -0700 |
| commit | 50095be5ac2c1b9830a74c87fd0d8e2edc8b8438 (patch) | |
| tree | 06e61100033466fac89fadda0eeb22dff338c8bf /src/proof/pdr/pdrInt.h | |
| parent | a59968ce8c55618ca7c84972faacba31c591a39f (diff) | |
| download | abc-50095be5ac2c1b9830a74c87fd0d8e2edc8b8438.tar.gz abc-50095be5ac2c1b9830a74c87fd0d8e2edc8b8438.tar.bz2 abc-50095be5ac2c1b9830a74c87fd0d8e2edc8b8438.zip | |
Adding runtime limit per output to multi-output DPR (pdr -H <num_sec>).
Diffstat (limited to 'src/proof/pdr/pdrInt.h')
| -rw-r--r-- | src/proof/pdr/pdrInt.h | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/proof/pdr/pdrInt.h b/src/proof/pdr/pdrInt.h index f6d3d170..03d522d3 100644 --- a/src/proof/pdr/pdrInt.h +++ b/src/proof/pdr/pdrInt.h @@ -97,6 +97,7 @@ struct Pdr_Man_t_ Vec_Int_t * vRes; // final result Vec_Int_t * vSuppLits; // support literals Pdr_Set_t * pCubeJust; // justification + clock_t * pTime4Outs;// timeout per output // statistics int nBlocks; // the number of times blockState was called int nObligs; // the number of proof obligations derived @@ -115,6 +116,7 @@ struct Pdr_Man_t_ int nQueLim; // runtime time_t timeToStop; + time_t timeToStopOne; // time stats clock_t tSat; clock_t tSatSat; |