Commit c25f488a by Alan Mishchenko

Debugging a proof error.

parent 6578d9cd
...@@ -213,7 +213,7 @@ static inline int Vec_SetAppend( Vec_Set_t * p, int * pArray, int nSize ) ...@@ -213,7 +213,7 @@ static inline int Vec_SetAppend( Vec_Set_t * p, int * pArray, int nSize )
int nWords = Vec_SetWordNum( nSize ); int nWords = Vec_SetWordNum( nSize );
assert( nWords < (1 << p->nPageSize) ); assert( nWords < (1 << p->nPageSize) );
p->nEntries++; p->nEntries++;
if ( Vec_SetLimit( p->pPages[p->iPage] ) + nWords > (1 << p->nPageSize) ) if ( Vec_SetLimit( p->pPages[p->iPage] ) + nWords >= (1 << p->nPageSize) )
{ {
if ( ++p->iPage == p->nPagesAlloc ) if ( ++p->iPage == p->nPagesAlloc )
{ {
...@@ -235,7 +235,7 @@ static inline int Vec_SetAppendS( Vec_Set_t * p, int nSize ) ...@@ -235,7 +235,7 @@ static inline int Vec_SetAppendS( Vec_Set_t * p, int nSize )
{ {
int nWords = Vec_SetWordNum( nSize ); int nWords = Vec_SetWordNum( nSize );
assert( nWords < (1 << p->nPageSize) ); assert( nWords < (1 << p->nPageSize) );
if ( Vec_SetLimitS( p->pPages[p->iPageS] ) + nWords > (1 << p->nPageSize) ) if ( Vec_SetLimitS( p->pPages[p->iPageS] ) + nWords >= (1 << p->nPageSize) )
Vec_SetWriteLimitS( p->pPages[++p->iPageS], 2 ); Vec_SetWriteLimitS( p->pPages[++p->iPageS], 2 );
Vec_SetIncLimitS( p->pPages[p->iPageS], nWords ); Vec_SetIncLimitS( p->pPages[p->iPageS], nWords );
return Vec_SetHandCurrentS(p) - nWords; return Vec_SetHandCurrentS(p) - nWords;
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment