From: Gereon Kremer <nafur42@gmail.com>
Date: Fri, 22 Oct 2021 21:37:54 +0000 (-0700)
Subject: Fix another double negation proof issue (#7468)
X-Git-Tag: cvc5-1.0.0~998
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f1db161860d0283cb5537ad8847e0b52d1485e28;p=cvc5.git

Fix another double negation proof issue (#7468)

This PR fixes another subtle proof issue in the circuit propagator concerning negated ites.
Fixes cvc5/cvc5-projects#309.
---

diff --git a/src/theory/booleans/proof_circuit_propagator.cpp b/src/theory/booleans/proof_circuit_propagator.cpp
index 71fb2a56f..e462414d1 100644
--- a/src/theory/booleans/proof_circuit_propagator.cpp
+++ b/src/theory/booleans/proof_circuit_propagator.cpp
@@ -382,10 +382,11 @@ std::shared_ptr<ProofNode> ProofCircuitPropagatorBackward::iteC(bool c)
         d_parent[0],
         !c);
   }
-  return mkResolution(mkProof(c ? PfRule::NOT_ITE_ELIM1 : PfRule::NOT_ITE_ELIM2,
-                              {assume(d_parent.notNode())}),
-                      d_parent[0],
-                      !c);
+  return mkNot(
+      mkResolution(mkProof(c ? PfRule::NOT_ITE_ELIM1 : PfRule::NOT_ITE_ELIM2,
+                           {assume(d_parent.notNode())}),
+                   d_parent[0],
+                   !c));
 }
 
 std::shared_ptr<ProofNode> ProofCircuitPropagatorBackward::iteIsCase(unsigned c)
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 1c81316c3..ab449dc13 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -839,6 +839,7 @@ set(regress_0_tests
   regress0/preprocess/proj-issue305-circuit-prop-ite-b.smt2
   regress0/preprocess/proj-issue305-circuit-prop-ite-c.smt2
   regress0/preprocess/proj-issue305-circuit-prop-ite-d.smt2
+  regress0/preprocess/proj-issue309-circuit-prop-ite.smt2
   regress0/print_define_fun_internal.smt2
   regress0/print_lambda.cvc.smt2
   regress0/print_model.cvc.smt2
diff --git a/test/regress/regress0/preprocess/proj-issue309-circuit-prop-ite.smt2 b/test/regress/regress0/preprocess/proj-issue309-circuit-prop-ite.smt2
new file mode 100644
index 000000000..09626896d
--- /dev/null
+++ b/test/regress/regress0/preprocess/proj-issue309-circuit-prop-ite.smt2
@@ -0,0 +1,9 @@
+; EXPECT: sat
+(set-logic ALL)
+(set-option :check-proofs true)
+(declare-fun a () Bool)
+(declare-fun c () Bool)
+(declare-fun d () Bool)
+(assert (not a))
+(assert (not (ite a d (not c))))
+(check-sat)