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);
+                    }
                 }
             }
         }