diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-07-13 15:44:45 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-07-13 15:44:45 -0700 |
| commit | be95437d1a416deaab1bee7a63c526376243c431 (patch) | |
| tree | c9b8b54cc6c5fee4ec48c2574ad46ad62ddb01de /src/sat/bsat | |
| parent | f54bf25d70fd74ecc5b97c1b1b9291161d54f556 (diff) | |
| download | abc-be95437d1a416deaab1bee7a63c526376243c431.tar.gz abc-be95437d1a416deaab1bee7a63c526376243c431.tar.bz2 abc-be95437d1a416deaab1bee7a63c526376243c431.zip | |
Debugging a proof error.
Diffstat (limited to 'src/sat/bsat')
| -rw-r--r-- | src/sat/bsat/satProof.c | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/src/sat/bsat/satProof.c b/src/sat/bsat/satProof.c index 143e7907..22763e7b 100644 --- a/src/sat/bsat/satProof.c +++ b/src/sat/bsat/satProof.c @@ -396,13 +396,13 @@ 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 ); + assert( pNode->Id > 1 ); Vec_PtrPush( vUsed, pNode ); // update fanins Proof_NodeForeachFanin( vProof, pNode, pFanin, k ) if ( (pNode->pEnts[k] & 1) == 0 ) // proof node { - assert( pFanin->Id > 0 ); + assert( pFanin->Id > 1 ); pNode->pEnts[k] = (pFanin->Id << 2) | (pNode->pEnts[k] & 2); } // else // problem clause @@ -410,7 +410,10 @@ int Sat_ProofReduce( Vec_Set_t * vProof, void * pRoots, int hProofPivot ) } // update roots Proof_ForeachNodeVec1( vRoots, vProof, pNode, i ) + { + assert( pNode->Id > 1 ); Vec_IntWriteEntry( vRoots, i, pNode->Id ); + } // determine new pivot assert( hProofPivot >= 1 && hProofPivot <= Vec_SetHandCurrent(vProof) ); pPivot = Proof_NodeRead( vProof, hProofPivot ); @@ -420,6 +423,7 @@ int Sat_ProofReduce( Vec_Set_t * vProof, void * pRoots, int hProofPivot ) Vec_PtrForEachEntry( satset *, vUsed, pNode, i ) { hTemp = pNode->Id; pNode->Id = 0; + assert( hTemp > 1 ); memmove( Vec_SetEntry(vProof, hTemp), pNode, sizeof(word)*Proof_NodeWordNum(pNode->nEnts) ); if ( pPivot && pPivot <= pNode ) { |