From db7b168978b2485d619b98b015c8cef47eee8646 Mon Sep 17 00:00:00 2001 From: Arthur Bit-Monnot Date: Tue, 12 Dec 2023 14:29:36 +0100 Subject: [PATCH] fix(sat): Workaround to avoid propagating in erroneous context --- solver/src/reasoners/sat/sat_solver.rs | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/solver/src/reasoners/sat/sat_solver.rs b/solver/src/reasoners/sat/sat_solver.rs index b1936c1a..d00a5b7a 100644 --- 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); + } } } }