Fix cnfRec for more complex subclauses

bf/bf.go

@@ -463,7 +463,9 @@ func cnfRec(f Formula, vars *vars) [][]int {
 				lits = append(lits, d)
 				for _, sub2 := range sub {
 					cnf := cnfRec(sub2, vars)
-					cnf[0] = append(cnf[0], -d)
+					for i := range cnf {
+						cnf[i] = append(cnf[i], -d)
+					}
 					res = append(res, cnf...)
 				}
 			default:

bf/bf_test.go

@@ -304,6 +304,47 @@ func TestReproduceInvalidSolutionBug2(t *testing.T) {
 	}
 }
 
+func TestInvalidUnsatBug(t *testing.T) {
+	f := And(
+		Not(Var("a")),
+		Not(Or(
+			And(Var("a"), Not(Var("b"))),
+			And(Var("b"), Not(Var("a"))),
+		)),
+		Or(
+			And(And(Var("a"), Var("b")), Not(Not(Var("c")))),
+			And(Not(Var("c")), Not(And(Var("a"), Var("b")))),
+		),
+		Not(Or(
+			And(Or(And(And(Var("a"), Var("b")), Not(Var("c"))), Var("c")), Not(Var("d"))),
+			And(Var("d"), Not(Or(And(And(Var("a"), Var("b")), Not(Var("c"))), Var("c")))),
+		)),
+		Not(Or(
+			And(And(Or(And(And(Var("a"), Var("b")), Not(Var("c"))), Var("c")), Var("d")), Not(Var("e"))),
+			And(Var("e"), Not(And(Or(And(And(Var("a"), Var("b")), Not(Var("c"))), Var("c")), Var("d")))),
+		)),
+	)
+
+	model := map[string]bool{
+		"a": false,
+		"b": false,
+		"c": false,
+		"d": false,
+		"e": false,
+	}
+	if !f.Eval(model) {
+		t.Errorf("Model check with known solution failed")
+	}
+
+	model = Solve(f)
+	if model == nil {
+		t.Fatalf("Failed to solve; f:\n%s", f)
+	}
+	if !f.Eval(model) {
+		t.Errorf("Model check failed")
+	}
+}
+
 func TestPanic1(t *testing.T) {
 	ans := Solve(And(Var("x"), Var("x")))
 	if len(ans) != 1 {