From: Gereon Kremer <nafur42@gmail.com>
Date: Thu, 21 Oct 2021 16:33:23 +0000 (-0700)
Subject: Fix incorrect proof from ITE in circuit propagator (#7446)
X-Git-Tag: cvc5-1.0.0~1018
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8f4eacebff0ea1d9ed7a3d00e3cee03c1877a016;p=cvc5.git

Fix incorrect proof from ITE in circuit propagator (#7446)

This PR fixes an incorrect proof in the circuit propagator related to back-propagation of an ite term.
Fixes cvc5/cvc5-projects#305.
---

diff --git a/src/theory/booleans/proof_circuit_propagator.cpp b/src/theory/booleans/proof_circuit_propagator.cpp
index ed4f81cb3..0ddfb741d 100644
--- a/src/theory/booleans/proof_circuit_propagator.cpp
+++ b/src/theory/booleans/proof_circuit_propagator.cpp
@@ -397,7 +397,7 @@ std::shared_ptr<ProofNode> ProofCircuitPropagatorBackward::iteIsCase(unsigned c)
   if (d_parentAssignment)
   {
     return mkResolution(
-        mkProof(PfRule::ITE_ELIM2, {assume(d_parent)}), d_parent[c + 1], false);
+        mkProof(PfRule::ITE_ELIM2, {assume(d_parent)}), d_parent[c + 1], true);
   }
   return mkResolution(
       mkProof(PfRule::NOT_ITE_ELIM2, {assume(d_parent.notNode())}),
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 3ea588e01..eda397da0 100644
--- 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-issue305-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-issue305-circuit-prop-ite.smt2 b/test/regress/regress0/preprocess/proj-issue305-circuit-prop-ite.smt2
new file mode 100644
index 000000000..6760bdf4d
--- /dev/null
+++ b/test/regress/regress0/preprocess/proj-issue305-circuit-prop-ite.smt2
@@ -0,0 +1,10 @@
+; EXPECT: sat
+(set-logic ALL)
+(set-option :check-proofs true)
+(declare-const x Bool)
+(declare-const y Bool)
+(declare-const z Bool)
+(assert y)
+(assert (not z))
+(assert (ite x y z))
+(check-sat)
\ No newline at end of file