diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2014-03-30 14:10:12 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2014-03-30 14:10:12 -0700 |
| commit | 37fd73cf9edb946e19b537ae94d8256f64db243e (patch) | |
| tree | 648de6040f6cc34c9a722c8e201431d679081836 /src/proof/pdr/pdrMan.c | |
| parent | 2f926f2fafba8dc2ec073c51b5ac9fdabd9ad201 (diff) | |
| download | abc-37fd73cf9edb946e19b537ae94d8256f64db243e.tar.gz abc-37fd73cf9edb946e19b537ae94d8256f64db243e.tar.bz2 abc-37fd73cf9edb946e19b537ae94d8256f64db243e.zip | |
Adding new code to verify invariant derived by 'pdr'.
Diffstat (limited to 'src/proof/pdr/pdrMan.c')
| -rw-r--r-- | src/proof/pdr/pdrMan.c | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/proof/pdr/pdrMan.c b/src/proof/pdr/pdrMan.c index ec20b8a9..9a73b697 100644 --- a/src/proof/pdr/pdrMan.c +++ b/src/proof/pdr/pdrMan.c @@ -54,7 +54,7 @@ Pdr_Man_t * Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrio p->pOrder = ABC_ALLOC( int, Aig_ManRegNum(pAig) ); p->vActVars = Vec_IntAlloc( 256 ); if ( !p->pPars->fMonoCnf ) - p->vVLits = Vec_WecStart( Abc_MaxInt(1, Aig_ManLevels(pAig)) ); + p->vVLits = Vec_WecStart( 1+Abc_MaxInt(1, Aig_ManLevels(pAig)) ); // internal use p->vPrio = vPrioInit ? vPrioInit : Vec_IntStart( Aig_ManRegNum(pAig) ); // priority flops p->vLits = Vec_IntAlloc( 100 ); // array of literals |