3 files changed, 69 insertions, 0 deletions
diff --git a/test/api/cpp/CMakeLists.txt b/test/api/cpp/CMakeLists.txt
index eae57f3b9..929c5bef2 100644
--- a/test/api/cpp/CMakeLists.txt
+++ b/test/api/cpp/CMakeLists.txt
@@ -54,3 +54,5 @@ cvc5_add_api_test(issue4889)
 cvc5_add_api_test(issue6111)
 cvc5_add_api_test(proj-issue306)
 cvc5_add_api_test(proj-issue334)
+cvc5_add_api_test(proj-issue344)
+cvc5_add_api_test(proj-issue345)
diff --git a/test/api/cpp/proj-issue344.cpp b/test/api/cpp/proj-issue344.cpp
new file mode 100644
index 000000000..5f486706c
--- /dev/null
+++ b/test/api/cpp/proj-issue344.cpp
@@ -0,0 +1,33 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Yoni Zohar
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Test for project issue #345
+ *
+ */
+
+
+#include "api/cpp/cvc5.h"
+#include <cassert>
+
+using namespace cvc5::api;
+
+int main(void)
+{
+  Solver slv;
+  slv.setOption("solve-bv-as-int", "iand");
+  Sort s12 = slv.getIntegerSort();
+  Term t13 = slv.mkConst(s12, "_x11");
+  Term t25 = slv.mkTerm(slv.mkOp(Kind::INT_TO_BITVECTOR, 4124876294), {t13});
+  Term t66 = slv.mkTerm(Kind::BITVECTOR_ULTBV, {t25, t25});
+  Term t154 = slv.mkTerm(Kind::BITVECTOR_SGT, {t66, t66});
+  slv.checkEntailed({t154, t154, t154, t154});
+}
diff --git a/test/api/cpp/proj-issue345.cpp b/test/api/cpp/proj-issue345.cpp
new file mode 100644
index 000000000..c33e9e5b8
--- /dev/null
+++ b/test/api/cpp/proj-issue345.cpp
@@ -0,0 +1,34 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Yoni Zohar
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Test for project issue #345
+ *
+ */
+
+
+#include "api/cpp/cvc5.h"
+#include <cassert>
+
+using namespace cvc5::api;
+
+int main(void)
+{
+  Solver slv;
+  slv.setOption("solve-bv-as-int", "iand");
+  Sort s12 = slv.getIntegerSort();
+  Term t13 = slv.mkConst(s12, "_x11");
+  Term t25 = slv.mkTerm(slv.mkOp(Kind::INT_TO_BITVECTOR, 4124876294), {t13});
+  Term t66 = slv.mkTerm(Kind::BITVECTOR_SLTBV, {t25, t25});
+  Term t154 = slv.mkTerm(Kind::BITVECTOR_SGT, {t66, t66});
+  slv.checkEntailed({t154, t154, t154, t154});
+}
+