diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-07-13 15:02:46 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-07-13 15:02:46 -0700 |
| commit | d3ad7fbaf33540075d02255741b4d35b90779cff (patch) | |
| tree | 4ba53c2756de06fb24cfbd51be5642607872a46e /src/sat/bsat/satProof.c | |
| parent | 86a0ae0bca9c604c95e90d802785ff73338efba1 (diff) | |
| download | abc-d3ad7fbaf33540075d02255741b4d35b90779cff.tar.gz abc-d3ad7fbaf33540075d02255741b4d35b90779cff.tar.bz2 abc-d3ad7fbaf33540075d02255741b4d35b90779cff.zip | |
Several small changes and fixes.
Diffstat (limited to 'src/sat/bsat/satProof.c')
| -rw-r--r-- | src/sat/bsat/satProof.c | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/sat/bsat/satProof.c b/src/sat/bsat/satProof.c index 680b1996..eeadf09e 100644 --- a/src/sat/bsat/satProof.c +++ b/src/sat/bsat/satProof.c @@ -396,11 +396,15 @@ int Sat_ProofReduce( Vec_Set_t * vProof, void * pRoots, int hProofPivot ) if ( pNode->Id == 0 ) continue; pNode->Id = Vec_SetAppendS( vProof, 2 + pNode->nEnts ); + assert( pNode->Id > 0 ); Vec_PtrPush( vUsed, pNode ); // update fanins Proof_NodeForeachFanin( vProof, pNode, pFanin, k ) if ( (pNode->pEnts[k] & 1) == 0 ) // proof node + { + assert( pFanin->Id > 0 ); pNode->pEnts[k] = (pFanin->Id << 2) | (pNode->pEnts[k] & 2); + } // else // problem clause // assert( (int*)pFanin >= Vec_IntArray(vClauses) && (int*)pFanin < Vec_IntArray(vClauses)+Vec_IntSize(vClauses) ); } @@ -420,7 +424,6 @@ int Sat_ProofReduce( Vec_Set_t * vProof, void * pRoots, int hProofPivot ) if ( pPivot && pPivot <= pNode ) { RetValue = hTemp; -// s->iProofPivot = i; pPivot = NULL; } } |