diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-07-13 18:22:10 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-07-13 18:22:10 -0700 |
| commit | 4ebda996d7102a43fbd08cdf1c1ab0c1e36f302e (patch) | |
| tree | ade05ed6f73e0bca0641bbad02401b64739fd964 /src/misc/vec/vecSet.h | |
| parent | c50d108f984c2e421f1c8d9b545a19d31d10be3b (diff) | |
| download | abc-4ebda996d7102a43fbd08cdf1c1ab0c1e36f302e.tar.gz abc-4ebda996d7102a43fbd08cdf1c1ab0c1e36f302e.tar.bz2 abc-4ebda996d7102a43fbd08cdf1c1ab0c1e36f302e.zip | |
Debugging a proof error.
Diffstat (limited to 'src/misc/vec/vecSet.h')
| -rw-r--r-- | src/misc/vec/vecSet.h | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/misc/vec/vecSet.h b/src/misc/vec/vecSet.h index 153fb15f..0045e3df 100644 --- a/src/misc/vec/vecSet.h +++ b/src/misc/vec/vecSet.h @@ -233,11 +233,18 @@ static inline int Vec_SetAppend( Vec_Set_t * p, int * pArray, int nSize ) } static inline int Vec_SetAppendS( Vec_Set_t * p, int nSize ) { + int Before1, Before2, After; int nWords = Vec_SetWordNum( nSize ); assert( nWords < (1 << p->nPageSize) ); + Before1 = Vec_SetLimitS( p->pPages[p->iPageS] ); + if ( Vec_SetLimitS( p->pPages[p->iPageS] ) + nWords >= (1 << p->nPageSize) ) Vec_SetWriteLimitS( p->pPages[++p->iPageS], 2 ); + Before2 = Vec_SetLimitS( p->pPages[p->iPageS] ); + Vec_SetIncLimitS( p->pPages[p->iPageS], nWords ); + After = Vec_SetLimitS( p->pPages[p->iPageS] ); + assert( Vec_SetHandCurrentS(p) - nWords < (1 << p->nPageSize) ); return Vec_SetHandCurrentS(p) - nWords; } |