From f23822a765843d1e37ba5d9a21c75d026b2a1be4 Mon Sep 17 00:00:00 2001
From: Johann Rosain <johann.rosain@ens-lyon.org>
Date: Wed, 8 Oct 2025 21:16:29 +0200
Subject: [PATCH 1/2] Fix: interpret negated conjecture when transforming
 statement list

---
 src/main.go | 23 +++++++++++++++++------
 1 file changed, 17 insertions(+), 6 deletions(-)

diff --git a/src/main.go b/src/main.go
index 07107474..18fc6e8e 100644
--- a/src/main.go
+++ b/src/main.go
@@ -207,7 +207,7 @@ func initDebuggers() {
 
 func StatementListToFormula(statements []Core.Statement, old_bound int, problemDir string) (form AST.Form, bound int, containsEquality bool) {
 	and_list := AST.NewFormList()
-	var not_form AST.Form
+	var negated_conjecture AST.Form
 	bound = old_bound
 
 	for _, statement := range statements {
@@ -249,11 +249,19 @@ func StatementListToFormula(statements []Core.Statement, old_bound int, problemD
 		case Core.Conjecture:
 			switch f := statement.GetForm().(type) {
 			case Lib.Some[AST.Form]:
-				not_form = doConjectureStatement(f.Val)
+				negated_conjecture = AST.MakerNot(doConjectureStatement(f.Val))
 			case Lib.None[AST.Form]:
 				Glob.Anomaly("main", "Conjecture statement "+statement.ToString()+" has no formula")
 			}
 
+		case Core.NegatedConjecture:
+			switch f := statement.GetForm().(type) {
+			case Lib.Some[AST.Form]:
+				negated_conjecture = doConjectureStatement(f.Val)
+			case Lib.None[AST.Form]:
+				Glob.Anomaly("main", "Negated conjecture statement "+statement.ToString()+" has no formula")
+			}
+
 		case Core.Type:
 			switch ty := statement.GetAtomTyping().(type) {
 			case Lib.Some[Core.TFFAtomTyping]:
@@ -261,19 +269,22 @@ func StatementListToFormula(statements []Core.Statement, old_bound int, problemD
 			case Lib.None[Core.TFFAtomTyping]:
 				Glob.Anomaly("main", "Type statement "+statement.ToString()+" has no formula")
 			}
+
+		default:
+			Glob.Fatal("main", fmt.Sprintf("Unmanaged statement role: %s", statement.GetRole().ToString()))
 		}
 	}
 
 	switch {
-	case and_list.IsEmpty() && not_form == nil:
+	case and_list.IsEmpty() && negated_conjecture == nil:
 		return nil, bound, containsEquality
 	case and_list.IsEmpty():
-		return AST.MakerNot(not_form), bound, containsEquality
-	case not_form == nil:
+		return negated_conjecture, bound, containsEquality
+	case negated_conjecture == nil:
 		return AST.MakerAnd(and_list), bound, containsEquality
 	default:
 		flattened := and_list.Flatten()
-		flattened.Append(AST.MakerNot(not_form))
+		flattened.Append(negated_conjecture)
 		return AST.MakerAnd(flattened), bound, containsEquality
 	}
 }

From 317d1325d6a21067bccd7dc8aee46bdc95632ed3 Mon Sep 17 00:00:00 2001
From: Johann Rosain <johann.rosain@ens-lyon.org>
Date: Wed, 8 Oct 2025 21:20:51 +0200
Subject: [PATCH 2/2] Add: bug files in the test suite

---
 devtools/test-suite/bugs/bug_66-1.p | 4 ++++
 devtools/test-suite/bugs/bug_66-2.p | 4 ++++
 2 files changed, 8 insertions(+)
 create mode 100644 devtools/test-suite/bugs/bug_66-1.p
 create mode 100644 devtools/test-suite/bugs/bug_66-2.p

diff --git a/devtools/test-suite/bugs/bug_66-1.p b/devtools/test-suite/bugs/bug_66-1.p
new file mode 100644
index 00000000..8c200560
--- /dev/null
+++ b/devtools/test-suite/bugs/bug_66-1.p
@@ -0,0 +1,4 @@
+% result: VALID
+
+fof(h, hypothesis, p ).
+fof(nc, negated_conjecture, ~p ).
diff --git a/devtools/test-suite/bugs/bug_66-2.p b/devtools/test-suite/bugs/bug_66-2.p
new file mode 100644
index 00000000..299fbaac
--- /dev/null
+++ b/devtools/test-suite/bugs/bug_66-2.p
@@ -0,0 +1,4 @@
+% result: NOT VALID
+
+fof(h, hypothesis, p ).
+fof(nc, negated_conjecture, p ).