summaryrefslogtreecommitdiffstats
path: root/src/sat/bsat/satProof.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/sat/bsat/satProof.c')
-rw-r--r--src/sat/bsat/satProof.c2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/sat/bsat/satProof.c b/src/sat/bsat/satProof.c
index 5616fdda..56de299e 100644
--- a/src/sat/bsat/satProof.c
+++ b/src/sat/bsat/satProof.c
@@ -412,6 +412,8 @@ int Sat_ProofReduce( Vec_Set_t * vProof, void * pRoots, int hProofPivot )
continue;
pNode->Id = Vec_SetAppendS( vProof, 2 + pNode->nEnts );
assert( pNode->Id > 1 );
+ assert( pNode->Id < (1<<vProof->nPageSize) );
+ assert( pNode->Id + nSize < (1<<vProof->nPageSize) );
Vec_PtrPush( vUsed, pNode );
// update fanins
Proof_NodeForeachFanin( vProof, pNode, pFanin, k )