From 61b2694ac72d41aeff9c67e3631278e5a3bea5cb Mon Sep 17 00:00:00 2001
From: Gereon Kremer <nafur42@gmail.com>
Date: Wed, 2 Jun 2021 13:55:40 +0200
Subject: 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.
---
 src/theory/booleans/proof_circuit_propagator.cpp   |  8 ++--
 test/regress/CMakeLists.txt                        |  1 +
 .../proofs/issue277-circuit-propagator.smt2        | 47 ++++++++++++++++++++++
 3 files changed, 52 insertions(+), 4 deletions(-)
 create mode 100644 test/regress/regress0/proofs/issue277-circuit-propagator.smt2

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,
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 39f1985b0..3adb3ebbb 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -800,6 +800,7 @@ set(regress_0_tests
   regress0/printer/let_shadowing.smt2
   regress0/printer/symbol_starting_w_digit.smt2
   regress0/printer/tuples_and_records.cvc
+  regress0/proofs/issue277-circuit-propagator.smt2
   regress0/proofs/scope.smt2
   regress0/push-pop/boolean/fuzz_12.smt2
   regress0/push-pop/boolean/fuzz_13.smt2
diff --git a/test/regress/regress0/proofs/issue277-circuit-propagator.smt2 b/test/regress/regress0/proofs/issue277-circuit-propagator.smt2
new file mode 100644
index 000000000..f0815e8f2
--- /dev/null
+++ b/test/regress/regress0/proofs/issue277-circuit-propagator.smt2
@@ -0,0 +1,47 @@
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+; EXPECT: sat
+(set-logic QF_UF)
+(set-option :produce-proofs true)
+(set-option :incremental true)
+(declare-fun p () Bool)
+(declare-fun q () Bool)
+
+(push)
+(assert (not (= p (not q))))
+(assert p)
+(check-sat)
+(pop)
+
+(push)
+(assert (not (= (not q) p)))
+(assert p)
+(check-sat)
+(pop)
+
+(push)
+(assert (not (= (not p) (not (not q)))))
+(assert p)
+(check-sat)
+(pop)
+
+(push)
+(assert (not (= (not (not q)) (not p))))
+(assert p)
+(check-sat)
+(pop)
+
+(push)
+(assert (not (= (not (not p)) (not (not (not q))))))
+(assert p)
+(check-sat)
+(pop)
+
+(push)
+(assert (not (= (not (not (not q))) (not (not p)))))
+(assert p)
+(check-sat)
+(pop)
\ No newline at end of file
-- 
cgit v1.2.3