diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-07-13 17:23:30 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-07-13 17:23:30 -0700 |
| commit | f37d0544ded12a1a1a7388cd71a3dc1b1959a331 (patch) | |
| tree | 730dd2bf093e8593ddf531beb4783ec766cfb73a /src/sat/bsat | |
| parent | 47b5ad1dfbc62ad71baff258fe61a2b3e0c3e097 (diff) | |
| download | abc-f37d0544ded12a1a1a7388cd71a3dc1b1959a331.tar.gz abc-f37d0544ded12a1a1a7388cd71a3dc1b1959a331.tar.bz2 abc-f37d0544ded12a1a1a7388cd71a3dc1b1959a331.zip | |
Debugging a proof error.
Diffstat (limited to 'src/sat/bsat')
| -rw-r--r-- | src/sat/bsat/satProof.c | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/src/sat/bsat/satProof.c b/src/sat/bsat/satProof.c index 5dcd23a4..864d87fe 100644 --- a/src/sat/bsat/satProof.c +++ b/src/sat/bsat/satProof.c @@ -448,8 +448,11 @@ int Sat_ProofReduce( Vec_Set_t * vProof, void * pRoots, int hProofPivot ) RetValue = hTemp; pPivot = NULL; } - pNode = (satset *)Vec_SetEntry(vProof, hTemp); - assert( pNode->partA == 0 ); + { + satset * pTemp = (satset *)Vec_SetEntry(vProof, hTemp); + assert( pTemp->partA == 0 ); + assert( Proof_NodeWordNum(pNode->nEnts) == Vec_SetWordNum( 2 + pTemp->nEnts ) ); + } } Vec_SetWriteEntryNum( vProof, Vec_PtrSize(vUsed) ); Vec_PtrFree( vUsed ); |