Debugging a proof error.

This commit is contained in:
Alan Mishchenko 2012-07-13 16:31:12 -07:00
parent da525b2a23
commit 3fb103dadc
1 changed files with 19 additions and 0 deletions

View File

@ -154,6 +154,25 @@ static inline void Vec_SetRestart( Vec_Set_t * p )
Vec_SetWriteLimit( p->pPages[0], 2 );
}
/**Function*************************************************************
Synopsis [Returns memory in bytes occupied by the vector.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline double Vec_ReportMemory( Vec_Set_t * p )
{
double Mem = sizeof(Vec_Set_t);
Mem += p->nPagesAlloc * sizeof(void *);
Mem += sizeof(word) * (1 << p->nPageSize) * (1 + p->iPage);
return Mem;
}
/**Function*************************************************************
Synopsis [Freeing vector.]