From d1aa15b0c84a8092aaf61e659fdf0dc48d896172 Mon Sep 17 00:00:00 2001
From: Jannis Harder <me@jix.one>
Date: Mon, 19 Aug 2024 14:08:11 +0200
Subject: [PATCH] glucose2: Create initial extra jlevel entries

My understanding is that jlevel needs to have this extra space as there
is existing code that assumes it is safe to index into it at index
decisionLevel()+1.
---
 src/sat/glucose2/Glucose2.cpp | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/src/sat/glucose2/Glucose2.cpp b/src/sat/glucose2/Glucose2.cpp
index f2ff3bcb5..ce553a6cb 100644
--- a/src/sat/glucose2/Glucose2.cpp
+++ b/src/sat/glucose2/Glucose2.cpp
@@ -187,6 +187,9 @@ Solver::Solver() :
   travId = 0;
   travId_prev = 0;
 
+  jlevel.push(-1);
+  jlevel.push(-1);
+
   // allocate space for clause interpretation 
   vec<Lit> tmp; tmp.growTo(3); 
   itpc = ca.alloc(tmp);
@@ -1911,6 +1914,9 @@ void Solver::reset()
     jlevel       .shrink_(jlevel.size());
     jnext        .shrink_(jnext.size());
 
+    jlevel.push(-1);
+    jlevel.push(-1);
+
     //var2FaninLits.shrink_(var2FaninLits.size());
     var2NodeData .shrink_(var2NodeData .size());
     var2Fanout0  .shrink_(var2Fanout0  .size());