From 8ddfb9f91dd4bb8a39dd1ac66531a77be7e906c1 Mon Sep 17 00:00:00 2001 From: Scott Date: Sat, 24 Nov 2018 22:36:10 +0100 Subject: [PATCH] Untest on unsat bugfix This commit fixes a bug in Untest when the last sat call was Unsat. The conflict on untest results in more derivations during backtracking. This fix ensures that all unit clauses are propagated. Previously, the unit clause from derivations during untest backtracking were not propagated. --- internal/xo/s.go | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/internal/xo/s.go b/internal/xo/s.go index 51f1ab7..e40ccf9 100644 --- a/internal/xo/s.go +++ b/internal/xo/s.go @@ -649,7 +649,7 @@ func (s *S) cleanupSolve() { if drvd.TargetLevel < s.endTestLevel { trail.Back(s.endTestLevel) s.x = CNull - break + //break } trail.Back(drvd.TargetLevel) trail.Assign(drvd.Unit, drvd.P)