Improved order Vars are added to the heap when canceling

c-cube · Mar 19, 2024 · f888533 · f888533
1 parent 288548b
commit f888533
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/batsat/src/core.rs b/src/batsat/src/core.rs
@@ -1916,7 +1916,7 @@ impl SolverV {
         debug_assert!(self.decision_level() > level);
         let trail_lim_last = *self.vars.trail_lim.last().expect("trail_lim is empty") as usize;
         let trail_lim_level = self.vars.trail_lim[level as usize] as usize;
-        for c in (trail_lim_level..self.vars.trail.len()).rev() {
+        for c in trail_lim_level..self.vars.trail.len() {
             let x = self.vars.trail[c].var();
             self.vars.ass[x] = lbool::UNDEF;
             if self.opts.phase_saving > 1 || (self.opts.phase_saving == 1 && c > trail_lim_last) {