summaryrefslogtreecommitdiffstats
path: root/src/sat/bsat
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2012-07-30 11:05:54 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2012-07-30 11:05:54 -0700
commitcd39fd6b0585659922908d172b0d058a5cb02dbb (patch)
tree47e0bce1b658026e15ba4f0d3373bb74b680c908 /src/sat/bsat
parent401aa6994a63ad60d51ac894dc5ef4141ca33f1a (diff)
downloadabc-cd39fd6b0585659922908d172b0d058a5cb02dbb.tar.gz
abc-cd39fd6b0585659922908d172b0d058a5cb02dbb.tar.bz2
abc-cd39fd6b0585659922908d172b0d058a5cb02dbb.zip
Fixing performance bug with old proof-logging (adding clauses multiple times).
Diffstat (limited to 'src/sat/bsat')
-rw-r--r--src/sat/bsat/satProof.c1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/sat/bsat/satProof.c b/src/sat/bsat/satProof.c
index 5e2ce067..e70a60ef 100644
--- a/src/sat/bsat/satProof.c
+++ b/src/sat/bsat/satProof.c
@@ -921,6 +921,7 @@ void * Proof_DeriveCore( Vec_Set_t * vProof, int hRoot )
// collect core clauses
vCore = Sat_ProofCollectCore( vProof, vUsed );
Vec_IntFree( vUsed );
+ Vec_IntSort( vCore, 1 );
return vCore;
}