diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-07-13 17:17:12 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-07-13 17:17:12 -0700 |
| commit | 47b5ad1dfbc62ad71baff258fe61a2b3e0c3e097 (patch) | |
| tree | 9a6c0cf94918992a38c9ead70599ad539c927824 | |
| parent | 7b367f5ecbd80c2fa04c8feaac632ac47c952729 (diff) | |
| download | abc-47b5ad1dfbc62ad71baff258fe61a2b3e0c3e097.tar.gz abc-47b5ad1dfbc62ad71baff258fe61a2b3e0c3e097.tar.bz2 abc-47b5ad1dfbc62ad71baff258fe61a2b3e0c3e097.zip | |
Debugging a proof error.
| -rw-r--r-- | src/sat/bsat/satProof.c | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/sat/bsat/satProof.c b/src/sat/bsat/satProof.c index 70527d1e..5dcd23a4 100644 --- a/src/sat/bsat/satProof.c +++ b/src/sat/bsat/satProof.c @@ -394,7 +394,7 @@ int Sat_ProofReduce( Vec_Set_t * vProof, void * pRoots, int hProofPivot ) clock_t clk = clock(); static clock_t TimeTotal = 0; int RetValue; - static Count = 0; + static int Count = 0; Count++; Sat_ProofCheck0( vProof ); @@ -448,6 +448,8 @@ 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 ); } Vec_SetWriteEntryNum( vProof, Vec_PtrSize(vUsed) ); Vec_PtrFree( vUsed ); |