From c25f488a83b361535ad8cb04bb67cf1abbbc9e60 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 13 Jul 2012 17:53:08 -0700 Subject: Debugging a proof error. --- src/misc/vec/vecSet.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/misc/vec/vecSet.h b/src/misc/vec/vecSet.h index 7e5c6c62..b47e05ad 100644 --- a/src/misc/vec/vecSet.h +++ b/src/misc/vec/vecSet.h @@ -213,7 +213,7 @@ static inline int Vec_SetAppend( Vec_Set_t * p, int * pArray, int nSize ) int nWords = Vec_SetWordNum( nSize ); assert( nWords < (1 << p->nPageSize) ); 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 ) { @@ -235,7 +235,7 @@ static inline int Vec_SetAppendS( Vec_Set_t * p, int nSize ) { int nWords = Vec_SetWordNum( nSize ); 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_SetIncLimitS( p->pPages[p->iPageS], nWords ); return Vec_SetHandCurrentS(p) - nWords; -- cgit v1.2.3