diff options
Diffstat (limited to 'test/api/cpp/proj-issue344.cpp')
-rw-r--r-- | test/api/cpp/proj-issue344.cpp | 33 |
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}); +} |