test/api/issue5074.cpp

   1 /*********************                                                        */
   2 /*! \file issue5074.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andres Noetzli
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief Test for issue #5074
  13  **/
  14
  15 #include "api/cvc4cpp.h"
  16
  17 using namespace CVC4::api;
  18
  19 int main()
  20 {
  21   Solver slv;
  22   Term c1 = slv.mkConst(slv.getIntegerSort());
  23   Term t6 = slv.mkTerm(Kind::STRING_FROM_CODE, c1);
  24   Term t12 = slv.mkTerm(Kind::STRING_TO_REGEXP, t6);
  25   Term t14 = slv.mkTerm(Kind::STRING_REPLACE_RE, {t6, t12, t6});
  26   Term t16 = slv.mkTerm(Kind::STRING_CONTAINS, {t14, t14});
  27   slv.checkEntailed(t16);
  28
  29   return 0;
  30 }