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 71fb2a56fa0316b04ff8c75e9c1ba6d1eb26f7e7..e462414d1aa7d1d1153c9c264c309a0e3469f727 100644 (file)
--- 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 1c81316c3bff82911ab145eb774df3cd1b6e0bd6..ab449dc1357a5a5907a4c5c1a355e3434d98c6d8 100644 (file)
--- 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 (file)
index 0000000..0962689
--- /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)