Commit 40515727 by Alan Mishchenko

Debugging a proof error.

parent 0f82d82b
...@@ -440,7 +440,7 @@ int Sat_ProofReduce( Vec_Set_t * vProof, void * pRoots, int hProofPivot ) ...@@ -440,7 +440,7 @@ int Sat_ProofReduce( Vec_Set_t * vProof, void * pRoots, int hProofPivot )
// compact the nodes // compact the nodes
Vec_PtrForEachEntry( satset *, vUsed, pNode, i ) Vec_PtrForEachEntry( satset *, vUsed, pNode, i )
{ {
int X = sizeof(word)*Proof_NodeWordNum(pNode->nEnts); int X = Proof_NodeWordNum(pNode->nEnts);
hTemp = pNode->Id; pNode->Id = 0; hTemp = pNode->Id; pNode->Id = 0;
assert( hTemp > 1 ); assert( hTemp > 1 );
memmove( Vec_SetEntry(vProof, hTemp), pNode, sizeof(word)*Proof_NodeWordNum(pNode->nEnts) ); memmove( Vec_SetEntry(vProof, hTemp), pNode, sizeof(word)*Proof_NodeWordNum(pNode->nEnts) );
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment