From c9235d3a95807083581e5f35bb5e7dc490325803 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Wed, 23 Jun 2010 14:46:24 +0000 Subject: [PATCH] Bugfix. Simplifying minisat wasn't using the separate malloc/free routines. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@870 e59a4935-1847-0410-ae03-e826735625c1 --- src/sat/simp/SimpSolver.C | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/sat/simp/SimpSolver.C b/src/sat/simp/SimpSolver.C index 4a3cf10..80cab67 100644 --- a/src/sat/simp/SimpSolver.C +++ b/src/sat/simp/SimpSolver.C @@ -46,12 +46,12 @@ SimpSolver::SimpSolver() : SimpSolver::~SimpSolver() { - free(bwdsub_tmpunit); + tlfree(bwdsub_tmpunit); // NOTE: elimtable.size() might be lower than nVars() at the moment for (int i = 0; i < elimtable.size(); i++) for (int j = 0; j < elimtable[i].eliminated.size(); j++) - free(elimtable[i].eliminated[j]); + tlfree(elimtable[i].eliminated[j]); } @@ -529,7 +529,7 @@ void SimpSolver::remember(Var v) remembered_clauses++; check(addClause(clause)); - free(&c); + tlfree(&c); } elimtable[v].eliminated.clear(); @@ -662,7 +662,7 @@ void SimpSolver::cleanUpClauses() for (i = j = 0; i < clauses.size(); i++) if (clauses[i]->mark() == 1) - free(clauses[i]); + tlfree(clauses[i]); else clauses[j++] = clauses[i]; clauses.shrink(i - j); -- 2.47.3