From: Dejan Jovanović Date: Wed, 2 Mar 2011 23:10:18 +0000 (+0000) Subject: fixing the big with lemma reallocation in minisat garbage collection X-Git-Tag: cvc5-1.0.0~8677 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f4d77f6874d519c6e6dba9cd8dd2ac4124955c5b;p=cvc5.git fixing the big with lemma reallocation in minisat garbage collection --- diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 28a90d741..5143f0974 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -1250,6 +1250,13 @@ void Solver::relocAll(ClauseAllocator& to) // for (int i = 0; i < clauses.size(); i++) ca.reloc(clauses[i], to); + + // All lemmas + // + for (int i = 0; i < lemma_propagated_reasons.size(); i ++) + ca.reloc(lemma_propagated_reasons[i], to); + for (int i = 0; i < propagating_lemmas.size(); i ++) + ca.reloc(lemma_propagated_reasons[i], to); } diff --git a/src/prop/minisat/core/SolverTypes.h b/src/prop/minisat/core/SolverTypes.h index 41e9be744..5fdabb2f1 100644 --- a/src/prop/minisat/core/SolverTypes.h +++ b/src/prop/minisat/core/SolverTypes.h @@ -238,6 +238,8 @@ class ClauseAllocator : public RegionAllocator void reloc(CRef& cr, ClauseAllocator& to) { + if (cr == CRef_Lazy) return; + Clause& c = operator[](cr); if (c.reloced()) { cr = c.relocation(); return; }