Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * Test for project issue #575
11 : : *
12 : : */
13 : : #include <cvc5/cvc5.h>
14 : :
15 : : using namespace cvc5;
16 : 1 : int main(void)
17 : : {
18 : 1 : TermManager tm;
19 : 1 : Solver solver(tm);
20 : 1 : solver.setOption("incremental", "false");
21 : 1 : solver.setOption("preprocess-only", "true");
22 : 1 : solver.setOption("produce-models", "true");
23 : 1 : Sort s0 = tm.mkBitVectorSort(48);
24 : 1 : Sort s1 = tm.getIntegerSort();
25 : 1 : Sort s2 = tm.getRoundingModeSort();
26 : 2 : DatatypeDecl d3 = tm.mkDatatypeDecl("_dt0");
27 : 2 : DatatypeConstructorDecl dtcd4 = tm.mkDatatypeConstructorDecl("_cons5");
28 : 1 : dtcd4.addSelector("_sel1", s0);
29 : 1 : dtcd4.addSelector("_sel2", s1);
30 : 1 : dtcd4.addSelector("_sel3", s1);
31 : 1 : dtcd4.addSelector("_sel4", s1);
32 : 1 : d3.addConstructor(dtcd4);
33 : 2 : DatatypeConstructorDecl dtcd5 = tm.mkDatatypeConstructorDecl("_cons9");
34 : 1 : dtcd5.addSelector("_sel6", s2);
35 : 1 : dtcd5.addSelector("_sel7", s1);
36 : 1 : dtcd5.addSelector("_sel8", s2);
37 : 1 : d3.addConstructor(dtcd5);
38 : 2 : DatatypeConstructorDecl dtcd6 = tm.mkDatatypeConstructorDecl("_cons13");
39 : 1 : dtcd6.addSelector("_sel10", s2);
40 : 1 : dtcd6.addSelector("_sel11", s1);
41 : 1 : dtcd6.addSelector("_sel12", s1);
42 : 1 : d3.addConstructor(dtcd6);
43 : 5 : Sort s7 = solver.declareDatatype("_dt0", {dtcd4, dtcd5, dtcd6});
44 : 2 : DatatypeDecl d8 = tm.mkDatatypeDecl("_dt14");
45 : 2 : DatatypeConstructorDecl dtcd9 = tm.mkDatatypeConstructorDecl("_cons24");
46 : 1 : dtcd9.addSelector("_sel19", s0);
47 : 1 : dtcd9.addSelector("_sel20", s0);
48 : 1 : dtcd9.addSelector("_sel21", s7);
49 : 1 : dtcd9.addSelector("_sel22", s1);
50 : 1 : dtcd9.addSelector("_sel23", s7);
51 : 1 : d8.addConstructor(dtcd9);
52 : 1 : Sort s10 = tm.mkParamSort("_p16");
53 : 1 : Sort s11 = tm.mkParamSort("_p17");
54 : 4 : DatatypeDecl d12 = tm.mkDatatypeDecl("_dt15", {s10, s11});
55 : 2 : DatatypeConstructorDecl dtcd13 = tm.mkDatatypeConstructorDecl("_cons29");
56 : 1 : dtcd13.addSelector("_sel25", s11);
57 : 1 : dtcd13.addSelector("_sel26", s0);
58 : 1 : dtcd13.addSelector("_sel27", s10);
59 : 1 : dtcd13.addSelector("_sel28", s7);
60 : 1 : d12.addConstructor(dtcd13);
61 : 2 : DatatypeConstructorDecl dtcd14 = tm.mkDatatypeConstructorDecl("_cons31");
62 : 1 : dtcd14.addSelector("_sel30", s10);
63 : 1 : d12.addConstructor(dtcd14);
64 : 2 : DatatypeDecl d15 = tm.mkDatatypeDecl("_dt18");
65 : 2 : DatatypeConstructorDecl dtcd16 = tm.mkDatatypeConstructorDecl("_cons34");
66 : 1 : dtcd16.addSelector("_sel32", s0);
67 : 1 : dtcd16.addSelector("_sel33", s1);
68 : 1 : d15.addConstructor(dtcd16);
69 : 2 : DatatypeConstructorDecl dtcd17 = tm.mkDatatypeConstructorDecl("_cons36");
70 : 1 : dtcd17.addSelectorSelf("_sel35");
71 : 1 : d15.addConstructor(dtcd17);
72 : 2 : DatatypeConstructorDecl dtcd18 = tm.mkDatatypeConstructorDecl("_cons37");
73 : 1 : d15.addConstructor(dtcd18);
74 : 2 : DatatypeConstructorDecl dtcd19 = tm.mkDatatypeConstructorDecl("_cons41");
75 : 1 : dtcd19.addSelector("_sel38", s1);
76 : 1 : dtcd19.addSelectorSelf("_sel39");
77 : 1 : dtcd19.addSelector("_sel40", s2);
78 : 1 : d15.addConstructor(dtcd19);
79 : 5 : std::vector<Sort> v20 = tm.mkDatatypeSorts({d8, d12, d15});
80 : 1 : Sort s21 = v20[0];
81 : 1 : Sort s22 = v20[1];
82 : 1 : Sort s23 = v20[2];
83 : 1 : Sort s24 = tm.getRealSort();
84 : 1 : Sort s25 = tm.mkUninterpretedSort("_u42");
85 : 1 : Sort s26 = tm.mkUninterpretedSort("_u43");
86 : 1 : Sort s27 = tm.mkFloatingPointSort(5, 11);
87 : 1 : Sort s28 = tm.mkBitVectorSort(1);
88 : 1 : Sort s29 = tm.mkBitVectorSort(5);
89 : 1 : Sort s30 = tm.mkBitVectorSort(10);
90 : 1 : Sort s31 = tm.mkBitVectorSort(16);
91 : 2 : DatatypeDecl d32 = tm.mkDatatypeDecl("_dt44");
92 : 2 : DatatypeConstructorDecl dtcd33 = tm.mkDatatypeConstructorDecl("_cons45");
93 : 1 : d32.addConstructor(dtcd33);
94 : 2 : DatatypeConstructorDecl dtcd34 = tm.mkDatatypeConstructorDecl("_cons47");
95 : 1 : dtcd34.addSelector("_sel46", s7);
96 : 1 : d32.addConstructor(dtcd34);
97 : 4 : Sort s35 = solver.declareDatatype("_dt44", {dtcd33, dtcd34});
98 : 3 : Sort s36 = tm.mkFunctionSort({s27}, s31);
99 : 1 : Sort s37 = tm.getRoundingModeSort();
100 : 1 : Sort s38 = tm.mkUninterpretedSort("_u48");
101 : 1 : Sort s39 = tm.getRoundingModeSort();
102 : 1 : Term t40 = tm.mkConst(s36, "_x49");
103 : 1 : Term t41 = tm.mkConst(s23, "_x50");
104 : 1 : Term t42 = tm.mkConst(s21, "_x51");
105 : 1 : Term t43 = tm.mkConst(s27, "_x52");
106 : 1 : Term t44 = tm.mkConst(s25, "_x53");
107 : 1 : Term t45 = tm.mkVar(s31, "_x54");
108 : 1 : Term t46 = tm.mkVar(s25, "_x55");
109 : 1 : Term t47 = tm.mkConst(s1, "_x56");
110 : 1 : Term t48 = tm.mkConst(s27, "_x57");
111 : 1 : Term t49 = tm.mkConst(s23, "_x58");
112 : 1 : Term t50 = tm.mkConst(s2, "_x59");
113 : 1 : Term t51 = tm.mkFloatingPointPosZero(5, 11);
114 : 1 : Term t52 = tm.mkConst(s24, "_x61");
115 : 2 : Term t53 = tm.mkBitVector(16, "1011011010000101", 2);
116 : 1 : Term t54 = tm.mkFloatingPoint(5, 11, t53);
117 : 1 : Term t55 = tm.mkVar(s26, "_x62");
118 : 5 : Term t56 = tm.mkTerm(Kind::EQUAL, {t52, t52, t52});
119 : 1 : Sort s57 = t56.getSort();
120 : 1 : Op o58 = tm.mkOp(Kind::ADD);
121 : 4 : Term t59 = tm.mkTerm(o58, {t47, t47});
122 : 1 : Op o60 = tm.mkOp(Kind::NOT);
123 : 3 : Term t61 = tm.mkTerm(o60, {t56});
124 : 4 : Term t62 = tm.mkTerm(Kind::APPLY_UF, {t40, t51});
125 : 4 : Term t63 = tm.mkTerm(Kind::LT, {t47, t47});
126 : 1 : solver.assertFormula(t61);
127 : 1 : solver.checkSat();
128 : 1 : solver.blockModel(cvc5::modes::BlockModelsMode::LITERALS);
129 : :
130 : 1 : return 0;
131 : 1 : }
|
