From: Andrew Reynolds Date: Mon, 25 Oct 2021 20:08:28 +0000 (-0500) Subject: Fix more missing uses of CDProof::isSame (#7491) X-Git-Tag: cvc5-1.0.0~982 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d7ac0a4acba9254b082effec1f7297033bd5c487;p=cvc5.git Fix more missing uses of CDProof::isSame (#7491) Fixes cvc5/cvc5-projects#306. --- diff --git a/src/preprocessing/assertion_pipeline.cpp b/src/preprocessing/assertion_pipeline.cpp index 665415772..f97c5bafb 100644 --- a/src/preprocessing/assertion_pipeline.cpp +++ b/src/preprocessing/assertion_pipeline.cpp @@ -186,7 +186,7 @@ void AssertionPipeline::conjoin(size_t i, Node n, ProofGenerator* pg) lcp->addLazyStep(d_nodes[i], d_pppg); lcp->addStep(newConj, PfRule::AND_INTRO, {d_nodes[i], n}, {}); } - if (newConjr != newConj) + if (!CDProof::isSame(newConjr, newConj)) { lcp->addStep( newConjr, PfRule::MACRO_SR_PRED_TRANSFORM, {newConj}, {newConjr}); diff --git a/src/theory/uf/eq_proof.cpp b/src/theory/uf/eq_proof.cpp index 06750c7ed..45a00a620 100644 --- a/src/theory/uf/eq_proof.cpp +++ b/src/theory/uf/eq_proof.cpp @@ -1432,7 +1432,7 @@ Node EqProof::addToProof(CDProof* p, // we obtained for example (= (f (f t1 t2 t3) t4) (f (f t5 t6) t7)), which is // flattened into the original conclusion (= (f t1 t2 t3 t4) (f t5 t6 t7)) via // rewriting - if (conclusion != d_node) + if (!CDProof::isSame(conclusion, d_node)) { Trace("eqproof-conv") << "EqProof::addToProof: add " << PfRule::MACRO_SR_PRED_TRANSFORM diff --git a/test/api/CMakeLists.txt b/test/api/CMakeLists.txt index 4811cca1b..f6c1cf8df 100644 --- a/test/api/CMakeLists.txt +++ b/test/api/CMakeLists.txt @@ -52,6 +52,7 @@ cvc5_add_api_test(two_solvers) cvc5_add_api_test(issue5074) cvc5_add_api_test(issue4889) cvc5_add_api_test(issue6111) +cvc5_add_api_test(proj-issue306) # if we've built using libedit, then we want the interactive shell tests if (USE_EDITLINE) diff --git a/test/api/proj-issue306.cpp b/test/api/proj-issue306.cpp new file mode 100644 index 000000000..664536a0b --- /dev/null +++ b/test/api/proj-issue306.cpp @@ -0,0 +1,21 @@ +#include "api/cpp/cvc5.h" + +using namespace cvc5::api; + +int main(void) +{ + Solver slv; + slv.setOption("check-proofs", "true"); + slv.setOption("proof-check", "eager"); + Sort s1 = slv.getBooleanSort(); + Sort s3 = slv.getStringSort(); + Term t1 = slv.mkConst(s3, "_x0"); + Term t3 = slv.mkConst(s1, "_x2"); + Term t11 = slv.mkString(""); + Term t14 = slv.mkConst(s3, "_x11"); + Term t42 = slv.mkTerm(Kind::ITE, t3, t14, t1); + Term t58 = slv.mkTerm(Kind::STRING_LEQ, t14, t11); + Term t95 = slv.mkTerm(Kind::EQUAL, t14, t42); + slv.assertFormula(t95); + slv.checkSatAssuming({t58}); +}