From 5ec4db2d44348ad668a10c9e5a81011fa949b403 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Fri, 13 Jul 2012 18:11:02 -0700
Subject: Debugging a proof error.

---
 src/sat/bsat/satProof.c | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'src/sat/bsat')

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 )
-- 
cgit v1.2.3