From 8f4eacebff0ea1d9ed7a3d00e3cee03c1877a016 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Thu, 21 Oct 2021 09:33:23 -0700 Subject: [PATCH] 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. --- src/theory/booleans/proof_circuit_propagator.cpp | 2 +- test/regress/CMakeLists.txt | 1 + .../preprocess/proj-issue305-circuit-prop-ite.smt2 | 10 ++++++++++ 3 files changed, 12 insertions(+), 1 deletion(-) create mode 100644 test/regress/regress0/preprocess/proj-issue305-circuit-prop-ite.smt2 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 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 -- 2.30.2