fix(sat): Properly handle tautologies in clause minimization.

plaans · Nov 4, 2024 · 9d7c161 · 9d7c161
1 parent 700aa64
commit 9d7c161
Showing 1 changed file with 5 additions and 2 deletions.
diff --git a/solver/src/core/state/domains.rs b/solver/src/core/state/domains.rs
@@ -545,8 +545,11 @@ impl Domains {
                     // not a decision, all antecedants that are not marked
                     for ante in antecedants {
                         if !marked.contains(ante) {
-                            let event = self.implying_event(ante).unwrap();
-                            self.queue.push(event, ante);
+                            if let Some(event) = self.implying_event(ante) {
+                                self.queue.push(event, ante);
+                            } else {
+                                // this is a tautology (entailed at ROOT), just ignore
+                            }
                         }
                     }
                 } else {