fix(linear propagator): overflowed sum lower bound

plaans · Nov 13, 2023 · 066c448 · 066c448
1 parent cef0cf7
commit 066c448
Showing 1 changed file with 6 additions and 3 deletions.
diff --git a/solver/src/reasoners/cp/mod.rs b/solver/src/reasoners/cp/mod.rs
@@ -154,13 +154,16 @@ impl Propagator for LinearSumLeq {
     fn propagate(&self, domains: &mut Domains, cause: Cause) -> Result<(), Contradiction> {
         if domains.entails(self.active) {
             // constraint is active, propagate
-            let sum_lb: IntCst = self
+            let sum_elems = self
                 .elements
                 .iter()
                 .copied()
                 .filter(|e| !domains.entails(!e.lit))
-                .map(|e| self.get_lower_bound(e, domains))
-                .sum();
+                .map(|e| self.get_lower_bound(e, domains));
+            let mut sum_lb: IntCst = 0;
+            for e in sum_elems {
+                sum_lb.saturating_add(e).clamp(INT_CST_MIN, INT_CST_MAX);
+            }
             let f = self.ub - sum_lb;
             // println!("Propagation : {} <= {}", sum_lb, self.ub);
             // self.print(domains);