Also fix case of negated ite (#7454)

This PR follows #7452 and fixes the proofs generated for backward propagation of negated ite terms.

diff --git a/src/theory/booleans/proof_circuit_propagator.cpp b/src/theory/booleans/proof_circuit_propagator.cpp
index fa48f7638e7020221579da5bbc3a77d6cf4a86fc..71fb2a56fa0316b04ff8c75e9c1ba6d1eb26f7e7 100644 (file)
--- 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 1ed42dd77c52078e0d52a8dc41d628dc3425fd74..ca9ce349f0c4c99e99e2ab0955c4fd73be7ff3b5 100644 (file)
--- 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 (file)
index 0000000..1765c32
--- /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 (file)
index 0000000..b3b19f7
--- /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