Fix issues with double negation in circuit propagator (#6669)

This PR fixes a subtle issue with double negations when producing proofs in the circuit propagator.
Adds the test case as a new regression, as well as some similar instances.
Fixes cvc5/cvc5-projects#277.

1 files changed, 4 insertions, 4 deletions

diff --git a/src/theory/booleans/proof_circuit_propagator.cpp b/src/theory/booleans/proof_circuit_propagator.cpp
index 6c4e0f96b..ed4f81cb3 100644
--- a/src/theory/booleans/proof_circuit_propagator.cpp
+++ b/src/theory/booleans/proof_circuit_propagator.cpp
@@ -169,11 +169,11 @@ std::shared_ptr<ProofNode> ProofCircuitPropagator::neqXFromY(bool y,
   {
     return nullptr;
   }
-  return mkResolution(
+  return mkNot(mkResolution(
       mkProof(y ? PfRule::NOT_EQUIV_ELIM2 : PfRule::NOT_EQUIV_ELIM1,
               {assume(parent.notNode())}),
       parent[1],
-      !y);
+      !y));
 }
 
 std::shared_ptr<ProofNode> ProofCircuitPropagator::neqYFromX(bool x,
@@ -183,11 +183,11 @@ std::shared_ptr<ProofNode> ProofCircuitPropagator::neqYFromX(bool x,
   {
     return nullptr;
   }
-  return mkResolution(
+  return mkNot(mkResolution(
       mkProof(x ? PfRule::NOT_EQUIV_ELIM2 : PfRule::NOT_EQUIV_ELIM1,
               {assume(parent.notNode())}),
       parent[0],
-      !x);
+      !x));
 }
 
 std::shared_ptr<ProofNode> ProofCircuitPropagator::xorXFromY(bool negated,