summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2012-07-13 18:51:24 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2012-07-13 18:51:24 -0700
commit08bb2e70b768efb7a5d7d8d1d1f6492cd13b23ca (patch)
tree574c285535c4c45557a6b1fb983d9c233a87fa8a /src
parentbbf4b9a58ddb8cada254e0a54ae96564e4e8c06c (diff)
downloadabc-08bb2e70b768efb7a5d7d8d1d1f6492cd13b23ca.tar.gz
abc-08bb2e70b768efb7a5d7d8d1d1f6492cd13b23ca.tar.bz2
abc-08bb2e70b768efb7a5d7d8d1d1f6492cd13b23ca.zip
Debugging a proof error.
Diffstat (limited to 'src')
-rw-r--r--src/sat/bsat/satProof.c2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/sat/bsat/satProof.c b/src/sat/bsat/satProof.c
index d54f94b4..7613e022 100644
--- a/src/sat/bsat/satProof.c
+++ b/src/sat/bsat/satProof.c
@@ -397,6 +397,8 @@ int Sat_ProofReduce( Vec_Set_t * vProof, void * pRoots, int hProofPivot )
static clock_t TimeTotal = 0;
int RetValue;
+Sat_ProofCheck0( vProof );
+
// collect visited nodes
nSize = Proof_MarkUsedRec( vProof, vRoots );
vUsed = Vec_PtrAlloc( nSize );