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 ed4f81cb316e6f8f3e187ea14ed81a2a4243fcaf..0ddfb741de1d765cc652e9bb24a894bcd2d9a925 100644 (file)
--- 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 3ea588e01b3360416dd0f2a0ef6c1fcf3b3df2f4..eda397da0d18fd00db6a60de54cbff4b395e13d9 100644 (file)
--- 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 (file)
index 0000000..6760bdf
--- /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