diff --git a/src/internal/partial_solution.rs b/src/internal/partial_solution.rs index a0e59206..68d4b41e 100644 --- a/src/internal/partial_solution.rs +++ b/src/internal/partial_solution.rs @@ -208,8 +208,12 @@ impl PartialSolution>, ) { use indexmap::map::Entry; - let term = store[cause].get(&package).unwrap().negate(); - let global_index = self.next_global_index; + let mut dated_derivation = DatedDerivation { + global_index: self.next_global_index, + decision_level: self.current_decision_level, + cause, + accumulated_intersection: store[cause].get(&package).unwrap().negate(), + }; self.next_global_index += 1; let pa_last_index = self.package_assignments.len().saturating_sub(1); match self.package_assignments.entry(package) { @@ -217,15 +221,14 @@ impl PartialSolution { panic!("add_derivation should not be called after a decision") } AssignmentsIntersection::Derivations(t) => { - *t = t.intersection(&term); - accumulated_intersection = t.clone(); + *t = t.intersection(&dated_derivation.accumulated_intersection); + dated_derivation.accumulated_intersection = t.clone(); if t.is_positive() { // we can use `swap_indices` to make `changed_this_decision_level` only go down by 1 // but the copying is slower then the larger search @@ -234,14 +237,10 @@ impl PartialSolution { + let term = dated_derivation.accumulated_intersection.clone(); if term.is_positive() { self.changed_this_decision_level = std::cmp::min(self.changed_this_decision_level, pa_last_index); @@ -249,12 +248,7 @@ impl PartialSolution