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 0ddfb741de1d765cc652e9bb24a894bcd2d9a925..3b1e40667684c90b250c88e1c3354cc8621e11c1 100644 (file)
--- 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 eda397da0d18fd00db6a60de54cbff4b395e13d9..8ef4ed362900d322d96c62279011c288578254f9 100644 (file)
--- 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 (file)
index 0000000..9e4bd28
--- /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)