Debugging a proof error.

This commit is contained in:
Alan Mishchenko 2012-07-13 18:22:10 -07:00
parent c50d108f98
commit 4ebda996d7
1 changed files with 7 additions and 0 deletions

View File

@ -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;
}