diff options
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; } |