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 6654157727326c41cf253b7d7ff18f1d4f3c86e9..f97c5bafb9f47ade31f14c81c16d7e157a14b23c 100644 (file)
--- 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 06750c7edbc2594af307fecac48257951abc0747..45a00a620b49efe350572f46ee6ac92866eceefc 100644 (file)
--- 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 4811cca1b80a82b1fb85198f78817d11e68e0a15..f6c1cf8dfbe86dfe2c24ec8a53c9123731dd5ac4 100644 (file)
--- 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 (file)
index 0000000..664536a
--- /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});
+}