From f14d0f0c65216514cde1f412255c88aee7e07643 Mon Sep 17 00:00:00 2001
From: Maarten Flippo <maartenflippo@outlook.com>
Date: Wed, 19 Nov 2025 14:43:27 +0100
Subject: [PATCH] fix(pumpkin-core): Don't use binary equality when logging
 proof

Previously we only disabled the binary equality propagator when logging
inferences. However, we cannot use the binary equality in the processor
either so we should not produce scaffolds using it.
---
 pumpkin-crates/core/src/api/solver.rs                         | 4 ++--
 pumpkin-crates/core/src/constraints/arithmetic/equality.rs    | 4 ++--
 .../core/src/engine/constraint_satisfaction_solver.rs         | 4 ++--
 pumpkin-crates/core/src/proof/mod.rs                          | 4 ++++
 4 files changed, 10 insertions(+), 6 deletions(-)

diff --git a/pumpkin-crates/core/src/api/solver.rs b/pumpkin-crates/core/src/api/solver.rs
index b9b4fe57b..95f01a5fe 100644
--- a/pumpkin-crates/core/src/api/solver.rs
+++ b/pumpkin-crates/core/src/api/solver.rs
@@ -143,8 +143,8 @@ impl Solver {
         self.satisfaction_solver.get_solution_reference()
     }
 
-    pub(crate) fn is_logging_full_proof(&self) -> bool {
-        self.satisfaction_solver.is_logging_full_proof()
+    pub(crate) fn is_logging_proof(&self) -> bool {
+        self.satisfaction_solver.is_logging_proof()
     }
 }
 
diff --git a/pumpkin-crates/core/src/constraints/arithmetic/equality.rs b/pumpkin-crates/core/src/constraints/arithmetic/equality.rs
index 9dbe430c1..8ffdddad1 100644
--- a/pumpkin-crates/core/src/constraints/arithmetic/equality.rs
+++ b/pumpkin-crates/core/src/constraints/arithmetic/equality.rs
@@ -85,7 +85,7 @@ where
     Var: IntegerVariable + Clone + 'static,
 {
     fn post(self, solver: &mut Solver) -> Result<(), ConstraintOperationError> {
-        if self.terms.len() == 2 && !solver.is_logging_full_proof() {
+        if self.terms.len() == 2 && !solver.is_logging_proof() {
             let _ = solver.add_propagator(BinaryEqualsPropagatorArgs {
                 a: self.terms[0].clone(),
                 b: self.terms[1].scaled(-1).offset(self.rhs),
@@ -110,7 +110,7 @@ where
         solver: &mut Solver,
         reification_literal: Literal,
     ) -> Result<(), ConstraintOperationError> {
-        if self.terms.len() == 2 {
+        if self.terms.len() == 2 && !solver.is_logging_proof() {
             let _ = solver.add_propagator(ReifiedPropagatorArgs {
                 propagator: BinaryEqualsPropagatorArgs {
                     a: self.terms[0].clone(),
diff --git a/pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs b/pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs
index 5f8c431c1..9d75a5b14 100644
--- a/pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs
+++ b/pumpkin-crates/core/src/engine/constraint_satisfaction_solver.rs
@@ -279,8 +279,8 @@ impl ConstraintSatisfactionSolver {
         finalize_proof(context);
     }
 
-    pub(crate) fn is_logging_full_proof(&self) -> bool {
-        self.internal_parameters.proof_log.is_logging_inferences()
+    pub(crate) fn is_logging_proof(&self) -> bool {
+        self.internal_parameters.proof_log.is_logging_proof()
     }
 }
 
diff --git a/pumpkin-crates/core/src/proof/mod.rs b/pumpkin-crates/core/src/proof/mod.rs
index 3d9ba7e6f..e0fd40af7 100644
--- a/pumpkin-crates/core/src/proof/mod.rs
+++ b/pumpkin-crates/core/src/proof/mod.rs
@@ -316,6 +316,10 @@ impl ProofLog {
             _ => ConstraintTag::create_from_index(0),
         }
     }
+
+    pub(crate) fn is_logging_proof(&self) -> bool {
+        self.internal_proof.is_some()
+    }
 }
 
 #[derive(Debug)]