1 files changed, 15 insertions, 3 deletions
diff --git a/src/sat/glucose2/SolverTypes.h b/src/sat/glucose2/SolverTypes.h
index b15c887f..ea0f76d0 100644
--- a/src/sat/glucose2/SolverTypes.h
+++ b/src/sat/glucose2/SolverTypes.h
@@ -38,6 +38,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "sat/glucose2/Map.h"
 #include "sat/glucose2/Alloc.h"
 
+#include "sat/glucose2/CGlucose.h"
+
 ABC_NAMESPACE_CXX_HEADER_START
 
 namespace Gluco2 {
@@ -145,6 +147,10 @@ class Clause {
 
     friend class ClauseAllocator;
 
+    #ifdef CGLUCOSE_EXP
+    friend class Solver;
+    #endif
+
     // NOTE: This constructor cannot be used directly (doesn't allocate enough memory).
     template<class V>
     Clause(const V& ps, bool use_extra, bool learnt) {
@@ -306,9 +312,15 @@ class OccLists
     }
 
     void  clear(bool free = true){
-        occs   .clear(free);
-        dirty  .clear(free);
-        dirties.clear(free);
+        if(free){
+            occs   .clear(free);
+            dirty  .clear(free);
+            dirties.clear(free);
+        } else {
+            occs   .shrink_(occs   .size());
+            dirty  .shrink_(dirty  .size());
+            dirties.shrink_(dirties.size());
+        }
     }
 };