Merge branch 'master' into cav22-stringscav22-strings

1 files changed, 33 insertions, 0 deletions

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