From: Gereon Kremer <nafur42@gmail.com>
Date: Thu, 21 Oct 2021 16:48:47 +0000 (-0700)
Subject: Add regression (#7447)
X-Git-Tag: cvc5-1.0.0~1017
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=109f17375661cc29f8125d289c4a776514c23e33;p=cvc5.git

Add regression (#7447)

This PR fixes a proof for an xor term that failed to eliminate a double negation.

Fixes cvc5/cvc5-projects#304
---

diff --git a/src/theory/booleans/proof_circuit_propagator.cpp b/src/theory/booleans/proof_circuit_propagator.cpp
index 0ddfb741d..3b1e40667 100644
--- a/src/theory/booleans/proof_circuit_propagator.cpp
+++ b/src/theory/booleans/proof_circuit_propagator.cpp
@@ -223,11 +223,11 @@ std::shared_ptr<ProofNode> ProofCircuitPropagator::xorYFromX(bool negated,
   }
   if (x)
   {
-    return mkResolution(
+    return mkNot(mkResolution(
         mkProof(negated ? PfRule::NOT_XOR_ELIM2 : PfRule::XOR_ELIM2,
                 {assume(negated ? parent.notNode() : Node(parent))}),
         parent[0],
-        false);
+        false));
   }
   return mkNot(
       mkResolution(mkProof(negated ? PfRule::NOT_XOR_ELIM1 : PfRule::XOR_ELIM1,
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index eda397da0..8ef4ed362 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -834,6 +834,7 @@ set(regress_0_tests
   regress0/preprocess/preprocess_13.cvc.smt2
   regress0/preprocess/preprocess_14.cvc.smt2
   regress0/preprocess/preprocess_15.cvc.smt2
+  regress0/preprocess/proj-issue304-circuit-prop-xor.smt2
   regress0/preprocess/proj-issue305-circuit-prop-ite.smt2
   regress0/print_define_fun_internal.smt2
   regress0/print_lambda.cvc.smt2
diff --git a/test/regress/regress0/preprocess/proj-issue304-circuit-prop-xor.smt2 b/test/regress/regress0/preprocess/proj-issue304-circuit-prop-xor.smt2
new file mode 100644
index 000000000..9e4bd285c
--- /dev/null
+++ b/test/regress/regress0/preprocess/proj-issue304-circuit-prop-xor.smt2
@@ -0,0 +1,8 @@
+; EXPECT: sat
+(set-logic ALL)
+(set-option :check-proofs true)
+(declare-const a Bool)
+(declare-const b Bool)
+(assert b)
+(assert (xor b (not a)))
+(check-sat)