Debugging a proof error.

5ec4db2d · Alan Mishchenko · 7913c1d8 · 5ec4db2d
Commit 5ec4db2d authored Jul 13, 2012 by Alan Mishchenko
Hide whitespace changes
Inline Side-by-side

Showing with 2 additions and 0 deletions

src/sat/bsat/satProof.c
+2 -0

No files found.
--- 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 )