diff options
Diffstat (limited to 'src/sat/bsat')
| -rw-r--r-- | src/sat/bsat/satProof.c | 2 | ||||
| -rw-r--r-- | src/sat/bsat/satSolver2.c | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/src/sat/bsat/satProof.c b/src/sat/bsat/satProof.c index 223c830b..d61dea4f 100644 --- a/src/sat/bsat/satProof.c +++ b/src/sat/bsat/satProof.c @@ -155,7 +155,7 @@ Vec_Int_t * Proof_CollectUsedIter( Vec_Set_t * vProof, Vec_Int_t * vRoots, int f Vec_IntFree( vStack ); // Abc_PrintTime( 1, "Iterative clause collection time", clock() - clk ); clk = clock(); - Abc_Sort( Vec_IntArray(vUsed), Vec_IntSize(vUsed) ); + Abc_MergeSort( Vec_IntArray(vUsed), Vec_IntSize(vUsed) ); // Abc_PrintTime( 1, "Postprocessing with sorting time", clock() - clk ); // verify topological order if ( fVerify ) diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c index a17c4762..484c5f8f 100644 --- a/src/sat/bsat/satSolver2.c +++ b/src/sat/bsat/satSolver2.c @@ -1416,7 +1416,7 @@ void sat_solver2_reducedb(sat_solver2* s) // preserve 1/10 of most active clauses pClaAct = veci_begin(&s->claActs) + 1; nClaAct = veci_size(&s->claActs) - 1; - pPerm = Abc_SortCost( pClaAct, nClaAct ); + pPerm = Abc_MergeSortCost( pClaAct, nClaAct ); assert( pClaAct[pPerm[0]] <= pClaAct[pPerm[nClaAct-1]] ); ActCutOff = pClaAct[pPerm[nClaAct*9/10]]; ABC_FREE( pPerm ); |