Untest on unsat bugfix

wsc1 · wsc1 · commit 8ddfb9f91dd4 · 2018-11-24T22:36:10.000+01:00
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.
diff --git 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)

Original file line number	Diff line number	Diff line change
`@@ -649,7 +649,7 @@ func (s *S) cleanupSolve() {`
`649`	`649`	`if drvd.TargetLevel < s.endTestLevel {`
`650`	`650`	`trail.Back(s.endTestLevel)`
`651`	`651`	`s.x = CNull`
`652`		`- break`
	`652`	`+ //break`
`653`	`653`	`}`
`654`	`654`	`trail.Back(drvd.TargetLevel)`
`655`	`655`	`trail.Assign(drvd.Unit, drvd.P)`