diff options
Diffstat (limited to 'test')
| -rw-r--r-- | test/api/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/api/issue5074.cpp | 30 |
2 files changed, 31 insertions, 0 deletions
diff --git a/test/api/CMakeLists.txt b/test/api/CMakeLists.txt index 8d9110e9f..9df87e9b5 100644 --- a/test/api/CMakeLists.txt +++ b/test/api/CMakeLists.txt @@ -34,6 +34,7 @@ cvc4_add_api_test(smt2_compliance) # TODO(cvc4-projects#209): Add methods for retrieving statistics to new API # cvc4_add_api_test(statistics) cvc4_add_api_test(two_solvers) +cvc4_add_api_test(issue5074) # if we've built using libedit, then we want the interactive shell tests if (USE_EDITLINE) diff --git a/test/api/issue5074.cpp b/test/api/issue5074.cpp new file mode 100644 index 000000000..b39701f6b --- /dev/null +++ b/test/api/issue5074.cpp @@ -0,0 +1,30 @@ +/********************* */ +/*! \file issue5074.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andres Noetzli + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 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.\endverbatim + ** + ** \brief Test for issue #5074 + **/ + +#include "api/cvc4cpp.h" + +using namespace CVC4::api; + +int main() +{ + Solver slv; + Term c1 = slv.mkConst(slv.getIntegerSort()); + Term t6 = slv.mkTerm(Kind::STRING_FROM_CODE, c1); + Term t12 = slv.mkTerm(Kind::STRING_TO_REGEXP, t6); + Term t14 = slv.mkTerm(Kind::STRING_REPLACE_RE, {t6, t12, t6}); + Term t16 = slv.mkTerm(Kind::STRING_CONTAINS, {t14, t14}); + slv.checkEntailed(t16); + + return 0; +} |