From f71d55abdbe6a51613a1ff33f24c708f66bf784e Mon Sep 17 00:00:00 2001
From: Gereon Kremer <nafur42@gmail.com>
Date: Thu, 21 Oct 2021 14:07:08 -0700
Subject: Also fix case of negated ite (#7454)

This PR follows #7452 and fixes the proofs generated for backward propagation of negated ite terms.
---
 src/theory/booleans/proof_circuit_propagator.cpp               |  3 ++-
 test/regress/CMakeLists.txt                                    |  2 ++
 .../regress0/preprocess/proj-issue305-circuit-prop-ite-c.smt2  | 10 ++++++++++
 .../regress0/preprocess/proj-issue305-circuit-prop-ite-d.smt2  | 10 ++++++++++
 4 files changed, 24 insertions(+), 1 deletion(-)
 create mode 100644 test/regress/regress0/preprocess/proj-issue305-circuit-prop-ite-c.smt2
 create mode 100644 test/regress/regress0/preprocess/proj-issue305-circuit-prop-ite-d.smt2

diff --git a/src/theory/booleans/proof_circuit_propagator.cpp b/src/theory/booleans/proof_circuit_propagator.cpp
index fa48f7638..71fb2a56f 100644
--- a/src/theory/booleans/proof_circuit_propagator.cpp
+++ b/src/theory/booleans/proof_circuit_propagator.cpp
@@ -402,7 +402,8 @@ std::shared_ptr<ProofNode> ProofCircuitPropagatorBackward::iteIsCase(unsigned c)
                         true);
   }
   return mkResolution(
-      mkProof(PfRule::NOT_ITE_ELIM2, {assume(d_parent.notNode())}),
+      mkProof(c == 0 ? PfRule::NOT_ITE_ELIM1 : PfRule::NOT_ITE_ELIM2,
+              {assume(d_parent.notNode())}),
       d_parent[c + 1],
       false);
 }
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 1ed42dd77..ca9ce349f 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -837,6 +837,8 @@ set(regress_0_tests
   regress0/preprocess/proj-issue304-circuit-prop-xor.smt2
   regress0/preprocess/proj-issue305-circuit-prop-ite-a.smt2
   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/print_define_fun_internal.smt2
   regress0/print_lambda.cvc.smt2
   regress0/print_model.cvc.smt2
diff --git a/test/regress/regress0/preprocess/proj-issue305-circuit-prop-ite-c.smt2 b/test/regress/regress0/preprocess/proj-issue305-circuit-prop-ite-c.smt2
new file mode 100644
index 000000000..1765c32f1
--- /dev/null
+++ b/test/regress/regress0/preprocess/proj-issue305-circuit-prop-ite-c.smt2
@@ -0,0 +1,10 @@
+; EXPECT: sat
+(set-logic ALL)
+(set-option :check-proofs true)
+(declare-fun a () Bool)
+(declare-fun b () Bool)
+(declare-fun c () Bool)
+(assert (not (ite a b c)))
+(assert b)
+(assert (not c))
+(check-sat)
\ No newline at end of file
diff --git a/test/regress/regress0/preprocess/proj-issue305-circuit-prop-ite-d.smt2 b/test/regress/regress0/preprocess/proj-issue305-circuit-prop-ite-d.smt2
new file mode 100644
index 000000000..b3b19f74b
--- /dev/null
+++ b/test/regress/regress0/preprocess/proj-issue305-circuit-prop-ite-d.smt2
@@ -0,0 +1,10 @@
+; EXPECT: sat
+(set-logic ALL)
+(set-option :check-proofs true)
+(declare-fun a () Bool)
+(declare-fun b () Bool)
+(declare-fun c () Bool)
+(assert (not (ite a b c)))
+(assert c)
+(assert (not b))
+(check-sat)
\ No newline at end of file
-- 
cgit v1.2.3