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 : : * Black box testing of grammar-related functions of the C API.
11 : : */
12 : :
13 : : extern "C" {
14 : : #include <cvc5/c/cvc5.h>
15 : : }
16 : :
17 : : #include "base/output.h"
18 : : #include "gtest/gtest.h"
19 : : #include "test_capi.h"
20 : :
21 : : namespace cvc5::internal::test {
22 : :
23 : : class TestCApiBlackGrammar : public ::testing::Test
24 : : {
25 : : protected:
26 : 8 : void SetUp() override
27 : : {
28 : 8 : d_tm = cvc5_term_manager_new();
29 : 8 : d_solver = cvc5_new(d_tm);
30 : 8 : d_bool = cvc5_get_boolean_sort(d_tm);
31 : 8 : d_int = cvc5_get_integer_sort(d_tm);
32 : 8 : d_real = cvc5_get_real_sort(d_tm);
33 : 8 : d_str = cvc5_get_string_sort(d_tm);
34 : 8 : d_uninterpreted = cvc5_mk_uninterpreted_sort(d_tm, "u");
35 : 8 : }
36 : 8 : void TearDown() override
37 : : {
38 : 8 : cvc5_delete(d_solver);
39 : 8 : cvc5_term_manager_release(d_tm);
40 : 8 : cvc5_term_manager_delete(d_tm);
41 : 8 : }
42 : :
43 : : Cvc5TermManager* d_tm;
44 : : Cvc5* d_solver;
45 : : Cvc5Sort d_bool;
46 : : Cvc5Sort d_int;
47 : : Cvc5Sort d_real;
48 : : Cvc5Sort d_str;
49 : : Cvc5Sort d_uninterpreted;
50 : : };
51 : :
52 : 4 : TEST_F(TestCApiBlackGrammar, to_string)
53 : : {
54 : 1 : cvc5_set_option(d_solver, "sygus", "true");
55 : 1 : Cvc5Term start = cvc5_mk_var(d_tm, d_bool, "start");
56 : 1 : std::vector<Cvc5Term> bvars;
57 : 1 : std::vector<Cvc5Term> symbols = {start};
58 : 2 : Cvc5Grammar g = cvc5_mk_grammar(
59 : 2 : d_solver, bvars.size(), bvars.data(), symbols.size(), symbols.data());
60 [ - + ][ + - ]: 1 : ASSERT_EQ(cvc5_grammar_to_string(g), std::string(""));
61 : 1 : cvc5_grammar_add_rule(g, start, cvc5_mk_false(d_tm));
62 [ - + ][ + - ]: 5 : ASSERT_CVC5_ERROR(cvc5_grammar_to_string(nullptr), "invalid grammar");
[ - + ][ + - ]
[ + - ][ + - ]
63 [ - + ][ + - ]: 1 : ASSERT_NE(cvc5_grammar_to_string(g), std::string(""));
64 [ + - ][ + - ]: 1 : }
65 : :
66 : 4 : TEST_F(TestCApiBlackGrammar, add_rule)
67 : : {
68 : 1 : cvc5_set_option(d_solver, "sygus", "true");
69 : 1 : Cvc5Term start = cvc5_mk_var(d_tm, d_bool, "start");
70 : 1 : Cvc5Term nts = cvc5_mk_var(d_tm, d_bool, "nts");
71 : :
72 : 1 : std::vector<Cvc5Term> bvars;
73 : 1 : std::vector<Cvc5Term> symbols = {start};
74 : 2 : Cvc5Grammar g = cvc5_mk_grammar(
75 : 2 : d_solver, bvars.size(), bvars.data(), symbols.size(), symbols.data());
76 : :
77 : 1 : cvc5_grammar_add_rule(g, start, cvc5_mk_false(d_tm));
78 : :
79 [ - + ][ + - ]: 5 : ASSERT_CVC5_ERROR(cvc5_grammar_add_rule(nullptr, start, cvc5_mk_false(d_tm)),
[ - + ][ + - ]
[ + - ][ + - ]
80 : : "invalid grammar");
81 [ - + ][ + - ]: 5 : ASSERT_CVC5_ERROR(cvc5_grammar_add_rule(g, nullptr, cvc5_mk_false(d_tm)),
[ - + ][ + - ]
[ + - ][ + - ]
82 : : "invalid term");
83 [ - + ][ + - ]: 5 : ASSERT_CVC5_ERROR(cvc5_grammar_add_rule(g, start, nullptr), "invalid term");
[ - + ][ + - ]
[ + - ][ + - ]
84 : :
85 [ - + ][ + - ]: 5 : ASSERT_CVC5_ERROR(cvc5_grammar_add_rule(g, nts, cvc5_mk_false(d_tm)),
[ - + ][ + - ]
[ + - ][ + - ]
86 : : "invalid argument");
87 [ - + ][ + - ]: 5 : ASSERT_CVC5_ERROR(
[ - + ][ + - ]
[ + - ][ + - ]
88 : : cvc5_grammar_add_rule(g, start, cvc5_mk_integer_int64(d_tm, 0)),
89 : : "same sort");
90 : :
91 : 1 : (void)cvc5_synth_fun_with_grammar(d_solver, "f", 0, nullptr, d_bool, g);
92 [ - + ][ + - ]: 5 : ASSERT_CVC5_ERROR(cvc5_grammar_add_rule(g, start, cvc5_mk_false(d_tm)),
[ - + ][ + - ]
[ + - ][ + - ]
93 : : "cannot be modified");
94 [ + - ][ + - ]: 1 : }
95 : :
96 : 4 : TEST_F(TestCApiBlackGrammar, add_rules)
97 : : {
98 : 1 : cvc5_set_option(d_solver, "sygus", "true");
99 : 1 : Cvc5Term start = cvc5_mk_var(d_tm, d_bool, "start");
100 : 1 : Cvc5Term nts = cvc5_mk_var(d_tm, d_bool, "nts");
101 : :
102 : 1 : std::vector<Cvc5Term> bvars;
103 : 1 : std::vector<Cvc5Term> symbols = {start};
104 : 2 : Cvc5Grammar g = cvc5_mk_grammar(
105 : 2 : d_solver, bvars.size(), bvars.data(), symbols.size(), symbols.data());
106 : :
107 : 1 : std::vector<Cvc5Term> rules = {cvc5_mk_false(d_tm)};
108 : 1 : cvc5_grammar_add_rules(g, start, rules.size(), rules.data());
109 : :
110 [ - + ][ + - ]: 5 : ASSERT_CVC5_ERROR(
[ - + ][ + - ]
[ + - ][ + - ]
111 : : cvc5_grammar_add_rules(nullptr, start, rules.size(), rules.data()),
112 : : "invalid grammar");
113 [ - + ][ + - ]: 5 : ASSERT_CVC5_ERROR(
[ - + ][ + - ]
[ + - ][ + - ]
114 : : cvc5_grammar_add_rules(g, nullptr, rules.size(), rules.data()),
115 : : "invalid term");
116 [ - + ][ + - ]: 5 : ASSERT_CVC5_ERROR(cvc5_grammar_add_rules(g, start, 0, nullptr),
[ - + ][ + - ]
[ + - ][ + - ]
117 : : "unexpected NULL argument");
118 : :
119 [ - + ][ + - ]: 5 : ASSERT_CVC5_ERROR(cvc5_grammar_add_rules(g, nts, rules.size(), rules.data()),
[ - + ][ + - ]
[ + - ][ + - ]
120 : : "invalid argument");
121 : 1 : rules.push_back(nullptr);
122 [ - + ][ + - ]: 5 : ASSERT_CVC5_ERROR(
[ - + ][ + - ]
[ + - ][ + - ]
123 : : cvc5_grammar_add_rules(g, start, rules.size(), rules.data()),
124 : : "invalid term at index 1");
125 : 1 : rules = {cvc5_mk_false(d_tm)};
126 [ - + ][ + - ]: 5 : ASSERT_CVC5_ERROR(cvc5_grammar_add_rules(g, nts, rules.size(), rules.data()),
[ - + ][ + - ]
[ + - ][ + - ]
127 : : "invalid argument");
128 : 1 : rules = {cvc5_mk_integer_int64(d_tm, 0)};
129 [ - + ][ + - ]: 5 : ASSERT_CVC5_ERROR(
[ - + ][ + - ]
[ + - ][ + - ]
130 : : cvc5_grammar_add_rules(g, start, rules.size(), rules.data()),
131 : : "Expected term with sort Bool");
132 : :
133 : 1 : (void)cvc5_synth_fun_with_grammar(d_solver, "f", 0, nullptr, d_bool, g);
134 : :
135 : 1 : rules = {cvc5_mk_false(d_tm)};
136 [ - + ][ + - ]: 5 : ASSERT_CVC5_ERROR(
[ - + ][ + - ]
[ + - ][ + - ]
137 : : cvc5_grammar_add_rules(g, start, rules.size(), rules.data()),
138 : : "cannot be modified");
139 [ + - ][ + - ]: 1 : }
[ + - ]
140 : :
141 : 4 : TEST_F(TestCApiBlackGrammar, add_any_constant)
142 : : {
143 : 1 : cvc5_set_option(d_solver, "sygus", "true");
144 : :
145 : 1 : Cvc5Term start = cvc5_mk_var(d_tm, d_bool, "start");
146 : 1 : Cvc5Term nts = cvc5_mk_var(d_tm, d_bool, "nts");
147 : :
148 : 1 : std::vector<Cvc5Term> bvars;
149 : 1 : std::vector<Cvc5Term> symbols = {start};
150 : 2 : Cvc5Grammar g = cvc5_mk_grammar(
151 : 2 : d_solver, bvars.size(), bvars.data(), symbols.size(), symbols.data());
152 : :
153 : 1 : cvc5_grammar_add_any_constant(g, start);
154 : 1 : cvc5_grammar_add_any_constant(g, start);
155 : :
156 [ - + ][ + - ]: 5 : ASSERT_CVC5_ERROR(cvc5_grammar_add_any_constant(nullptr, start),
[ - + ][ + - ]
[ + - ][ + - ]
157 : : "invalid grammar");
158 [ - + ][ + - ]: 5 : ASSERT_CVC5_ERROR(cvc5_grammar_add_any_constant(g, nullptr), "invalid term");
[ - + ][ + - ]
[ + - ][ + - ]
159 [ - + ][ + - ]: 5 : ASSERT_CVC5_ERROR(cvc5_grammar_add_any_constant(g, nts),
[ - + ][ + - ]
[ + - ][ + - ]
160 : : "expected ntSymbol to be one of the non-terminal symbols");
161 : :
162 : 1 : (void)cvc5_synth_fun_with_grammar(d_solver, "f", 0, nullptr, d_bool, g);
163 : :
164 [ - + ][ + - ]: 5 : ASSERT_CVC5_ERROR(cvc5_grammar_add_any_constant(g, start),
[ - + ][ + - ]
[ + - ][ + - ]
165 : : "cannot be modified");
166 [ + - ][ + - ]: 1 : }
167 : :
168 : 4 : TEST_F(TestCApiBlackGrammar, add_any_variable)
169 : : {
170 : 1 : cvc5_set_option(d_solver, "sygus", "true");
171 : :
172 : 1 : Cvc5Term start = cvc5_mk_var(d_tm, d_bool, "start");
173 : 1 : Cvc5Term nts = cvc5_mk_var(d_tm, d_bool, "nts");
174 : :
175 : 1 : Cvc5Term x = cvc5_mk_var(d_tm, d_bool, "x");
176 : 1 : std::vector<Cvc5Term> bvars = {x};
177 : 1 : std::vector<Cvc5Term> symbols = {start};
178 : 2 : Cvc5Grammar g1 = cvc5_mk_grammar(
179 : 2 : d_solver, bvars.size(), bvars.data(), symbols.size(), symbols.data());
180 : : Cvc5Grammar g2 =
181 : 1 : cvc5_mk_grammar(d_solver, 0, nullptr, symbols.size(), symbols.data());
182 : :
183 : 1 : cvc5_grammar_add_any_variable(g1, start);
184 : 1 : cvc5_grammar_add_any_variable(g1, start);
185 : 1 : cvc5_grammar_add_any_variable(g2, start);
186 : :
187 [ - + ][ + - ]: 5 : ASSERT_CVC5_ERROR(cvc5_grammar_add_any_variable(nullptr, start),
[ - + ][ + - ]
[ + - ][ + - ]
188 : : "invalid grammar");
189 [ - + ][ + - ]: 5 : ASSERT_CVC5_ERROR(cvc5_grammar_add_any_variable(g1, nullptr), "invalid term");
[ - + ][ + - ]
[ + - ][ + - ]
190 [ - + ][ + - ]: 5 : ASSERT_CVC5_ERROR(cvc5_grammar_add_any_variable(g1, nts),
[ - + ][ + - ]
[ + - ][ + - ]
191 : : "expected ntSymbol to be one of the non-terminal symbols");
192 : :
193 : 1 : (void)cvc5_synth_fun_with_grammar(d_solver, "f", 0, nullptr, d_bool, g1);
194 : :
195 [ - + ][ + - ]: 5 : ASSERT_CVC5_ERROR(cvc5_grammar_add_any_variable(g1, start),
[ - + ][ + - ]
[ + - ][ + - ]
196 : : "cannot be modified");
197 [ + - ][ + - ]: 1 : }
198 : :
199 : 4 : TEST_F(TestCApiBlackGrammar, equal_hash)
200 : : {
201 : 1 : cvc5_set_option(d_solver, "sygus", "true");
202 : :
203 : 1 : Cvc5Term x = cvc5_mk_var(d_tm, d_bool, "x");
204 : 1 : Cvc5Term start1 = cvc5_mk_var(d_tm, d_bool, "start");
205 : 1 : Cvc5Term start2 = cvc5_mk_var(d_tm, d_bool, "start");
206 : 1 : std::vector<Cvc5Term> bvars, symbols;
207 : : Cvc5Grammar g1, g2;
208 : :
209 : : {
210 : 1 : symbols = {start1};
211 : 1 : bvars = {};
212 : 2 : g1 = cvc5_mk_grammar(
213 : 2 : d_solver, bvars.size(), bvars.data(), symbols.size(), symbols.data());
214 : 2 : g2 = cvc5_mk_grammar(
215 : 2 : d_solver, bvars.size(), bvars.data(), symbols.size(), symbols.data());
216 [ - + ][ + - ]: 1 : ASSERT_EQ(cvc5_grammar_hash(g1), cvc5_grammar_hash(g1));
217 [ - + ][ + - ]: 1 : ASSERT_EQ(cvc5_grammar_hash(g1), cvc5_grammar_hash(g2));
218 [ - + ][ + - ]: 1 : ASSERT_TRUE(cvc5_grammar_is_equal(g1, g1));
219 [ - + ][ + - ]: 1 : ASSERT_FALSE(cvc5_grammar_is_equal(g1, g2));
220 [ - + ][ + - ]: 1 : ASSERT_TRUE(cvc5_grammar_is_disequal(g1, g2));
221 : : }
222 : :
223 : : {
224 : 1 : symbols = {start1};
225 : 1 : bvars = {};
226 : 2 : g1 = cvc5_mk_grammar(
227 : 2 : d_solver, bvars.size(), bvars.data(), symbols.size(), symbols.data());
228 : 1 : bvars = {x};
229 : 2 : g2 = cvc5_mk_grammar(
230 : 2 : d_solver, bvars.size(), bvars.data(), symbols.size(), symbols.data());
231 [ - + ][ + - ]: 1 : ASSERT_NE(cvc5_grammar_hash(g1), cvc5_grammar_hash(g2));
232 [ - + ][ + - ]: 1 : ASSERT_TRUE(cvc5_grammar_is_equal(g1, g1));
233 [ - + ][ + - ]: 1 : ASSERT_FALSE(cvc5_grammar_is_equal(g1, g2));
234 [ - + ][ + - ]: 1 : ASSERT_TRUE(cvc5_grammar_is_disequal(g1, g2));
235 : : }
236 : :
237 : : {
238 : 1 : bvars = {x};
239 : 1 : symbols = {start1};
240 : 2 : g1 = cvc5_mk_grammar(
241 : 2 : d_solver, bvars.size(), bvars.data(), symbols.size(), symbols.data());
242 : 1 : symbols = {start2};
243 : 2 : g2 = cvc5_mk_grammar(
244 : 2 : d_solver, bvars.size(), bvars.data(), symbols.size(), symbols.data());
245 [ - + ][ + - ]: 1 : ASSERT_NE(cvc5_grammar_hash(g1), cvc5_grammar_hash(g2));
246 [ - + ][ + - ]: 1 : ASSERT_TRUE(cvc5_grammar_is_equal(g1, g1));
247 [ - + ][ + - ]: 1 : ASSERT_FALSE(cvc5_grammar_is_equal(g1, g2));
248 [ - + ][ + - ]: 1 : ASSERT_TRUE(cvc5_grammar_is_disequal(g1, g2));
249 : : }
250 : :
251 : : {
252 : 1 : bvars = {x};
253 : 1 : symbols = {start1};
254 : 2 : g1 = cvc5_mk_grammar(
255 : 2 : d_solver, bvars.size(), bvars.data(), symbols.size(), symbols.data());
256 : 2 : g2 = cvc5_mk_grammar(
257 : 2 : d_solver, bvars.size(), bvars.data(), symbols.size(), symbols.data());
258 : 1 : cvc5_grammar_add_any_variable(g2, start1);
259 [ - + ][ + - ]: 1 : ASSERT_NE(cvc5_grammar_hash(g1), cvc5_grammar_hash(g2));
260 [ - + ][ + - ]: 1 : ASSERT_TRUE(cvc5_grammar_is_equal(g1, g1));
261 [ - + ][ + - ]: 1 : ASSERT_FALSE(cvc5_grammar_is_equal(g1, g2));
262 [ - + ][ + - ]: 1 : ASSERT_TRUE(cvc5_grammar_is_disequal(g1, g2));
263 : : }
264 : :
265 : : {
266 : 1 : bvars = {x};
267 : 1 : symbols = {start1};
268 : 2 : g1 = cvc5_mk_grammar(
269 : 2 : d_solver, bvars.size(), bvars.data(), symbols.size(), symbols.data());
270 : 2 : g2 = cvc5_mk_grammar(
271 : 2 : d_solver, bvars.size(), bvars.data(), symbols.size(), symbols.data());
272 : 1 : std::vector<Cvc5Term> rules = {cvc5_mk_false(d_tm)};
273 : 1 : cvc5_grammar_add_rules(g1, start1, rules.size(), rules.data());
274 : 1 : cvc5_grammar_add_rules(g2, start1, rules.size(), rules.data());
275 [ - + ][ + - ]: 1 : ASSERT_EQ(cvc5_grammar_hash(g1), cvc5_grammar_hash(g2));
276 [ - + ][ + - ]: 1 : ASSERT_TRUE(cvc5_grammar_is_equal(g1, g1));
277 [ - + ][ + - ]: 1 : ASSERT_FALSE(cvc5_grammar_is_equal(g1, g2));
278 [ - + ][ + - ]: 1 : ASSERT_TRUE(cvc5_grammar_is_disequal(g1, g2));
279 [ + - ]: 1 : }
280 : :
281 : : {
282 : 1 : bvars = {x};
283 : 1 : symbols = {start1};
284 : 2 : g1 = cvc5_mk_grammar(
285 : 2 : d_solver, bvars.size(), bvars.data(), symbols.size(), symbols.data());
286 : 2 : g2 = cvc5_mk_grammar(
287 : 2 : d_solver, bvars.size(), bvars.data(), symbols.size(), symbols.data());
288 : 1 : std::vector<Cvc5Term> rules2 = {cvc5_mk_false(d_tm)};
289 : 1 : cvc5_grammar_add_rules(g2, start1, rules2.size(), rules2.data());
290 [ - + ][ + - ]: 1 : ASSERT_NE(cvc5_grammar_hash(g1), cvc5_grammar_hash(g2));
291 [ - + ][ + - ]: 1 : ASSERT_TRUE(cvc5_grammar_is_equal(g1, g1));
292 [ - + ][ + - ]: 1 : ASSERT_FALSE(cvc5_grammar_is_equal(g1, g2));
293 [ - + ][ + - ]: 1 : ASSERT_TRUE(cvc5_grammar_is_disequal(g1, g2));
294 [ + - ]: 1 : }
295 : :
296 : : {
297 : 1 : bvars = {x};
298 : 1 : symbols = {start1};
299 : 2 : g1 = cvc5_mk_grammar(
300 : 2 : d_solver, bvars.size(), bvars.data(), symbols.size(), symbols.data());
301 : 2 : g2 = cvc5_mk_grammar(
302 : 2 : d_solver, bvars.size(), bvars.data(), symbols.size(), symbols.data());
303 : 1 : std::vector<Cvc5Term> rules1 = {cvc5_mk_true(d_tm)};
304 : 1 : std::vector<Cvc5Term> rules2 = {cvc5_mk_false(d_tm)};
305 : 1 : cvc5_grammar_add_rules(g1, start1, rules1.size(), rules1.data());
306 : 1 : cvc5_grammar_add_rules(g2, start1, rules2.size(), rules2.data());
307 [ - + ][ + - ]: 1 : ASSERT_NE(cvc5_grammar_hash(g1), cvc5_grammar_hash(g2));
308 [ - + ][ + - ]: 1 : ASSERT_TRUE(cvc5_grammar_is_equal(g1, g1));
309 [ - + ][ + - ]: 1 : ASSERT_FALSE(cvc5_grammar_is_equal(g1, g2));
310 [ - + ][ + - ]: 1 : ASSERT_TRUE(cvc5_grammar_is_disequal(g1, g2));
311 [ + - ][ + - ]: 1 : }
312 [ - + ][ + - ]: 5 : ASSERT_CVC5_ERROR(cvc5_grammar_hash(nullptr), "invalid grammar");
[ - + ][ + - ]
[ + - ][ + - ]
313 [ + - ][ + - ]: 1 : }
314 : :
315 : 4 : TEST_F(TestCApiBlackGrammar, copy_release)
316 : : {
317 [ - + ][ + - ]: 5 : ASSERT_CVC5_ERROR(cvc5_grammar_copy(nullptr), "invalid grammar");
[ - + ][ + - ]
[ + - ][ + - ]
318 [ - + ][ + - ]: 5 : ASSERT_CVC5_ERROR(cvc5_grammar_release(nullptr), "invalid grammar");
[ - + ][ + - ]
[ + - ][ + - ]
319 : 1 : cvc5_set_option(d_solver, "sygus", "true");
320 : 1 : Cvc5Term start = cvc5_mk_var(d_tm, d_bool, "start");
321 : 1 : Cvc5Term x = cvc5_mk_var(d_tm, d_bool, "x");
322 : 1 : std::vector<Cvc5Term> bvars = {x};
323 : 1 : std::vector<Cvc5Term> symbols = {start};
324 : 2 : Cvc5Grammar g1 = cvc5_mk_grammar(
325 : 2 : d_solver, bvars.size(), bvars.data(), symbols.size(), symbols.data());
326 : 1 : Cvc5Grammar g2 = cvc5_grammar_copy(g1);
327 [ - + ][ + - ]: 1 : ASSERT_EQ(cvc5_grammar_hash(g1), cvc5_grammar_hash(g2));
328 : 1 : cvc5_grammar_release(g1);
329 [ - + ][ + - ]: 1 : ASSERT_EQ(cvc5_grammar_hash(g1), cvc5_grammar_hash(g2));
330 : 1 : cvc5_grammar_release(g1);
331 : : // we cannot reliably check that querying on the (now freed) grammar fails
332 : : // unless ASAN is enabled
333 : : }
334 : 4 : TEST_F(TestCApiBlackGrammar, release_after_add_rule)
335 : : {
336 : : // Grammars are mutable, releasing a grammar after it was modified must
337 : : // still find (and free) it.
338 : 1 : cvc5_set_option(d_solver, "sygus", "true");
339 : 1 : Cvc5Term start = cvc5_mk_var(d_tm, d_bool, "start");
340 : 1 : std::vector<Cvc5Term> bvars;
341 : 1 : std::vector<Cvc5Term> symbols = {start};
342 : 2 : Cvc5Grammar g = cvc5_mk_grammar(
343 : 2 : d_solver, bvars.size(), bvars.data(), symbols.size(), symbols.data());
344 : 1 : cvc5_grammar_add_rule(g, start, cvc5_mk_false(d_tm));
345 : 1 : cvc5_grammar_add_any_constant(g, start);
346 : 1 : cvc5_grammar_release(g);
347 [ - + ][ + - ]: 1 : ASSERT_FALSE(cvc5_has_error());
348 [ + - ][ + - ]: 1 : }
349 : :
350 : : } // namespace cvc5::internal::test
|
