From: Dejan Jovanović <dejan.jovanovic@gmail.com>
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<uint32_t>
 
     void reloc(CRef& cr, ClauseAllocator& to)
     {
+        if (cr == CRef_Lazy) return;
+
         Clause& c = operator[](cr);
         
         if (c.reloced()) { cr = c.relocation(); return; }