diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-03-02 23:10:18 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-03-02 23:10:18 +0000 |
commit | f4d77f6874d519c6e6dba9cd8dd2ac4124955c5b (patch) | |
tree | dd33bfed1452bf3f365335db3c74cb6cff531e86 /src/prop | |
parent | 320fc000e028c1a08b4453255fc80b0105b28bb3 (diff) |
fixing the big with lemma reallocation in minisat garbage collection
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/minisat/core/Solver.cc | 7 | ||||
-rw-r--r-- | src/prop/minisat/core/SolverTypes.h | 2 |
2 files changed, 9 insertions, 0 deletions
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<uint32_t> void reloc(CRef& cr, ClauseAllocator& to) { + if (cr == CRef_Lazy) return; + Clause& c = operator[](cr); if (c.reloced()) { cr = c.relocation(); return; } |