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 28a90d741d8fe1b50d6d266a979f92933da742e3..5143f0974a6552a37221b27477d9d03f9554adeb 100644 (file)
--- 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 41e9be744daa2841370dff28aabc056d17dcf1d9..5fdabb2f19db988c655d91f0f901b0afa9c8ac9e 100644 (file)
--- 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; }