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

Fixes cvc5/cvc5-projects#306.

2 files changed, 22 insertions, 0 deletions

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