From 06e2d45f3d94976928b44a9c052214f89af6bccd Mon Sep 17 00:00:00 2001
From: Josh Deprez <josh.deprez@gmail.com>
Date: Sun, 7 Nov 2021 16:02:52 +1100
Subject: [PATCH] Fix cnfRec for more complex subclauses

When inserting a dummy variable d, -d must be added to each new
subclause, not merely the first one.
---
 bf/bf.go      |  4 +++-
 bf/bf_test.go | 41 +++++++++++++++++++++++++++++++++++++++++
 2 files changed, 44 insertions(+), 1 deletion(-)

diff --git a/bf/bf.go b/bf/bf.go
index 09d3a93..75157eb 100644
--- a/bf/bf.go
+++ b/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:
diff --git a/bf/bf_test.go b/bf/bf_test.go
index 92b8adf..d18bae1 100644
--- a/bf/bf_test.go
+++ b/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 {