From 0b65739ab1ee37a7ef8101874f687f5c6f4e8fd7 Mon Sep 17 00:00:00 2001
From: Steven de Oliveira <de.oliveira.steven@gmail.com>
Date: Mon, 11 Dec 2023 16:24:35 +0100
Subject: [PATCH] Not reinitializing to 0, but to last query start

---
 src/lib/reasoners/satml.ml | 14 ++++++++++----
 1 file changed, 10 insertions(+), 4 deletions(-)

diff --git a/src/lib/reasoners/satml.ml b/src/lib/reasoners/satml.ml
index a5cd9656ec..e0a5142037 100644
--- a/src/lib/reasoners/satml.ml
+++ b/src/lib/reasoners/satml.ml
@@ -239,6 +239,8 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
       mutable increm_guards : Atom.atom Vec.t;
 
       mutable next_dec_guard : int;
+
+      mutable decision_lvl_at_query_start : int;
     }
 
   exception Conflict of Atom.clause
@@ -347,6 +349,8 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
       increm_guards = Vec.make 1 ~dummy:Atom.dummy_atom;
 
       next_dec_guard = 0;
+
+      decision_lvl_at_query_start = 0;
     }
 
 
@@ -1462,10 +1466,11 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
       if Options.get_enable_restarts ()
       && n_of_conflicts >= 0 && !conflictC >= n_of_conflicts then begin
         env.progress_estimate <- progress_estimate env;
-        cancel_until env 0;
+        cancel_until env env.decision_lvl_at_query_start;
         raise Restart
       end;
-      if decision_level env = 0 then simplify env;
+      if decision_level env = env.decision_lvl_at_query_start then
+        simplify env;
 
       if n_of_learnts >= 0 &&
          Vec.size env.learnts - nb_assigns env >= n_of_learnts then
@@ -1513,6 +1518,7 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
 
   let solve env =
     if env.is_unsat then raise (Unsat env.unsat_core);
+    env.decision_lvl_at_query_start <- decision_level env;
     let n_of_conflicts = ref (Atom.to_float env.restart_first) in
     let n_of_learnts =
       ref ((Atom.to_float (nb_clauses env)) *. env.learntsize_factor) in
@@ -1616,11 +1622,11 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
         let lvl = a.var.level in
         assert (lvl <> 0);
         begin
-          if not (Options.get_minimal_bj ()) then cancel_until env 0
+          if not (Options.get_minimal_bj ()) then cancel_until env (env.decision_lvl_at_query_start)
           else if a.is_true || a.neg.is_true then cancel_until env (lvl - 1)
         end;
         a.var.vpremise <- init;
-        enqueue env a 0 None;
+        enqueue env a env.decision_lvl_at_query_start None;
         propagate_and_stabilize env propagate (ref 0) Auto
     (* TODO *)