fix(pumpkin-core): Don't use binary equality when logging proof

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()
     }
 }
 

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(),

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()
     }
 }
 

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)]