1 files changed, 21 insertions, 0 deletions
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});
+}