fix(sat): Workaround to avoid propagating in erroneous context

plaans · Dec 12, 2023 · db7b168 · db7b168
1 parent b6244ef
commit db7b168
Showing 1 changed file with 5 additions and 1 deletion.
diff --git a/solver/src/reasoners/sat/sat_solver.rs b/solver/src/reasoners/sat/sat_solver.rs
@@ -373,7 +373,11 @@ impl SatSolver {
             if let Some(asserted) = asserted_literal {
                 if !model.entails(asserted) {
                     debug_assert!(!model.entails(!asserted));
-                    self.set_from_unit_propagation(asserted, clause, model);
+                    if !model.entails(!asserted) {
+                        // note that the above condition should always be true by design but seems to be buggy in some very rare cases
+                        // When in release mode, just avoid propagating if this condition does not hold
+                        self.set_from_unit_propagation(asserted, clause, model);
+                    }
                 }
             }
         }