Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Aina Niemetz, Andrew Reynolds
       4                 :            :  *
       5                 :            :  * This file is part of the cvc5 project.
       6                 :            :  *
       7                 :            :  * Copyright (c) 2009-2025 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.
      11                 :            :  * ****************************************************************************
      12                 :            :  *
      13                 :            :  * Test for project issue #612
      14                 :            :  *
      15                 :            :  */
      16                 :            : #include <cvc5/cvc5.h>
      17                 :            : 
      18                 :            : using namespace cvc5;
      19                 :          1 : int main(void)
      20                 :            : {
      21                 :          1 :   TermManager tm;
      22                 :          1 :   Solver solver(tm);
      23                 :          1 :   solver.setOption("incremental", "false");
      24                 :          1 :   solver.setOption("produce-models", "true");
      25                 :          1 :   Sort s0 = tm.getRealSort();
      26                 :          1 :   Term t1 = tm.mkConst(s0, "_x0");
      27                 :          1 :   Term t2 = tm.mkReal(181067, 804);
      28                 :          1 :   Term t3 = tm.mkConst(s0, "_x1");
      29                 :          3 :   Term t4 = tm.mkTerm(Kind::SET_SINGLETON, {t1});
      30                 :          1 :   Sort s5 = t4.getSort();
      31                 :          3 :   Term t6 = tm.mkTerm(Kind::SET_COMPLEMENT, {t4});
      32                 :          1 :   Op o7 = tm.mkOp(Kind::REGEXP_ALLCHAR);
      33                 :          1 :   Term t8 = tm.mkTerm(o7, {});
      34                 :          1 :   Sort s9 = t8.getSort();
      35                 :          3 :   Term t10 = tm.mkTerm(Kind::SET_SINGLETON, {t1});
      36                 :          1 :   Term t11 = tm.mkVar(s0, "_f2_0");
      37                 :          1 :   Term t12 = tm.mkVar(s5, "_f2_1");
      38                 :          1 :   Term t13 = tm.mkVar(s0, "_f2_2");
      39                 :          1 :   Term t14 = tm.mkVar(s0, "_f2_3");
      40                 :          1 :   Op o15 = tm.mkOp(Kind::SET_CHOOSE);
      41                 :          3 :   Term t16 = tm.mkTerm(o15, {t12});
      42                 :          1 :   Term t17 = tm.mkPi();
      43                 :          1 :   Op o18 = tm.mkOp(Kind::ARCCOSECANT);
      44                 :          3 :   Term t19 = tm.mkTerm(o18, {t2});
      45                 :          1 :   Op o20 = tm.mkOp(Kind::SET_CHOOSE);
      46                 :          3 :   Term t21 = tm.mkTerm(o15, {t4});
      47                 :          1 :   Op o22 = tm.mkOp(Kind::DIVISION);
      48                 :          4 :   Term t23 = tm.mkTerm(o22, {t1, t11});
      49                 :          1 :   Op o24 = tm.mkOp(Kind::SUB);
      50                 :          4 :   Term t25 = tm.mkTerm(o24, {t14, t13});
      51                 :          1 :   Op o26 = tm.mkOp(Kind::NEG);
      52                 :          3 :   Term t27 = tm.mkTerm(o26, {t1});
      53                 :          1 :   Op o28 = tm.mkOp(Kind::ARCSECANT);
      54                 :          3 :   Term t29 = tm.mkTerm(o28, {t1});
      55                 :          1 :   Op o30 = tm.mkOp(Kind::SUB);
      56                 :          4 :   Term t31 = tm.mkTerm(o24, {t1, t1});
      57                 :          1 :   Op o32 = tm.mkOp(Kind::SUB);
      58                 :          4 :   Term t33 = tm.mkTerm(o24, {t1, t14});
      59                 :          1 :   Op o34 = tm.mkOp(Kind::DIVISION);
      60                 :          4 :   Term t35 = tm.mkTerm(o22, {t1, t1});
      61                 :          1 :   Op o36 = tm.mkOp(Kind::ARCSINE);
      62                 :          3 :   Term t37 = tm.mkTerm(o36, {t1});
      63                 :          1 :   Op o38 = tm.mkOp(Kind::NEG);
      64                 :          3 :   Term t39 = tm.mkTerm(o26, {t1});
      65                 :          1 :   Op o40 = tm.mkOp(Kind::DIVISION);
      66                 :          4 :   Term t41 = tm.mkTerm(o22, {t1, t1});
      67                 :          1 :   Op o42 = tm.mkOp(Kind::SET_CHOOSE);
      68                 :          3 :   Term t43 = tm.mkTerm(o15, {t4});
      69                 :          1 :   Op o44 = tm.mkOp(Kind::SUB);
      70                 :          4 :   Term t45 = tm.mkTerm(o24, {t11, t1});
      71                 :          1 :   Op o46 = tm.mkOp(Kind::SET_CHOOSE);
      72                 :          3 :   Term t47 = tm.mkTerm(o15, {t4});
      73                 :          1 :   Op o48 = tm.mkOp(Kind::SET_CHOOSE);
      74                 :          3 :   Term t49 = tm.mkTerm(o15, {t4});
      75                 :          1 :   Op o50 = tm.mkOp(Kind::ARCSINE);
      76                 :          3 :   Term t51 = tm.mkTerm(o36, {t1});
      77                 :          1 :   Op o52 = tm.mkOp(Kind::DIVISION);
      78                 :          4 :   Term t53 = tm.mkTerm(o22, {t1, t1});
      79                 :          1 :   Op o54 = tm.mkOp(Kind::ADD);
      80                 :          4 :   Term t55 = tm.mkTerm(o54, {t14, t1});
      81                 :          1 :   Op o56 = tm.mkOp(Kind::SET_CHOOSE);
      82                 :          3 :   Term t57 = tm.mkTerm(o15, {t4});
      83                 :          1 :   Op o58 = tm.mkOp(Kind::ARCCOTANGENT);
      84                 :          3 :   Term t59 = tm.mkTerm(o58, {t1});
      85                 :          1 :   Op o60 = tm.mkOp(Kind::SET_CHOOSE);
      86                 :          3 :   Term t61 = tm.mkTerm(o15, {t4});
      87                 :          1 :   Op o62 = tm.mkOp(Kind::LT);
      88                 :          5 :   Term t63 = tm.mkTerm(o62, {t1, t29, t29});
      89                 :          1 :   Sort s64 = t63.getSort();
      90                 :          1 :   Op o65 = tm.mkOp(Kind::NOT);
      91                 :          3 :   Term t66 = tm.mkTerm(o65, {t63});
      92                 :          4 :   Term t67 = tm.mkTerm(Kind::REGEXP_INTER, {t8, t8});
      93                 :          1 :   solver.assertFormula(t66);
      94                 :          1 :   solver.checkSat();
      95                 :          1 :   solver.blockModel(cvc5::modes::BlockModelsMode::LITERALS);
      96                 :            : 
      97                 :          1 :   return 0;
      98                 :          1 : }