Fix more missing uses of CDProof::isSame (#7491)

Fixes cvc5/cvc5-projects#306.

4 files changed, 24 insertions, 2 deletions

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});
+}