From f4d77f6874d519c6e6dba9cd8dd2ac4124955c5b Mon Sep 17 00:00:00 2001 From: =?utf8?q?Dejan=20Jovanovi=C4=87?= Date: Wed, 2 Mar 2011 23:10:18 +0000 Subject: [PATCH] fixing the big with lemma reallocation in minisat garbage collection --- src/prop/minisat/core/Solver.cc | 7 +++++++ src/prop/minisat/core/SolverTypes.h | 2 ++ 2 files changed, 9 insertions(+) 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; } -- 2.30.2