1 #-----------------------------------------------------------------------------#
2 # Regression level 0 tests
5 regress0/arith/ackermann.real.smt2
6 regress0/arith/arith-eq.smt2
7 regress0/arith/arith-mixed-types-no-tighten.smt2
8 regress0/arith/arith-mixed-types-tighten.smt2
9 regress0/arith/arith-strict-relaxed.smt2
10 regress0/arith/arith-strict.smt2
11 regress0/arith/arith-tighten-1.smt2
12 regress0/arith/arith-tighten-2.smt2
13 regress0/arith/arith.01.cvc
14 regress0/arith/arith.02.cvc
15 regress0/arith/arith.03.cvc
16 regress0/arith/bug443.delta01.smtv1.smt2
17 regress0/arith/bug547.2.smt2
18 regress0/arith/bug569.smt2
19 regress0/arith/delta-minimized-row-vector-bug.smtv1.smt2
20 regress0/arith/div-chainable.smt2
21 regress0/arith/div.01.smt2
22 regress0/arith/div.02.smt2
23 regress0/arith/div.04.smt2
24 regress0/arith/div.05.smt2
25 regress0/arith/div.07.smt2
26 regress0/arith/fuzz_3-eq.smtv1.smt2
27 regress0/arith/integers/ackermann1.smt2
28 regress0/arith/integers/ackermann2.smt2
29 regress0/arith/integers/ackermann3.smt2
30 regress0/arith/integers/ackermann4.smt2
31 regress0/arith/integers/ackermann5.smt2
32 regress0/arith/integers/ackermann6.smt2
33 regress0/arith/integers/arith-int-042.cvc
34 regress0/arith/integers/arith-int-042.min.cvc
35 regress0/arith/issue1399.smt2
36 regress0/arith/issue3412.smt2
37 regress0/arith/issue3413.smt2
38 regress0/arith/issue3480.smt2
39 regress0/arith/issue3683.smt2
40 regress0/arith/ite-lift.smt2
41 regress0/arith/leq.01.smtv1.smt2
42 regress0/arith/miplib.cvc
43 regress0/arith/miplib2.cvc
44 regress0/arith/miplib4.cvc
45 regress0/arith/miplibtrick.smtv1.smt2
46 regress0/arith/mod-simp.smt2
47 regress0/arith/mod.01.smt2
48 regress0/arith/mult.01.smt2
49 regress0/array-const-real-parse.smt2
50 regress0/arrayinuf_declare.smt2
51 regress0/arrays/arrays0.smt2
52 regress0/arrays/arrays1.smt2
53 regress0/arrays/arrays2.smt2
54 regress0/arrays/arrays3.smt2
55 regress0/arrays/arrays4.smt2
56 regress0/arrays/bool-array.smt2
57 regress0/arrays/bug272.minimized.smtv1.smt2
58 regress0/arrays/bug272.smtv1.smt2
59 regress0/arrays/bug3020.smt2
60 regress0/arrays/bug637.delta.smt2
61 regress0/arrays/constarr.cvc
62 regress0/arrays/constarr.smt2
63 regress0/arrays/constarr2.cvc
64 regress0/arrays/constarr2.smt2
65 regress0/arrays/incorrect1.smtv1.smt2
66 regress0/arrays/incorrect10.smtv1.smt2
67 regress0/arrays/incorrect11.smtv1.smt2
68 regress0/arrays/incorrect2.minimized.smtv1.smt2
69 regress0/arrays/incorrect2.smtv1.smt2
70 regress0/arrays/incorrect3.smtv1.smt2
71 regress0/arrays/incorrect4.smtv1.smt2
72 regress0/arrays/incorrect5.smtv1.smt2
73 regress0/arrays/incorrect6.smtv1.smt2
74 regress0/arrays/incorrect7.smtv1.smt2
75 regress0/arrays/incorrect8.minimized.smtv1.smt2
76 regress0/arrays/incorrect8.smtv1.smt2
77 regress0/arrays/incorrect9.smtv1.smt2
78 regress0/arrays/issue3813-massign-assert.smt2
79 regress0/arrays/issue3814.smt2
80 regress0/arrays/swap_t1_np_nf_ai_00005_007.cvc.smtv1.smt2
81 regress0/arrays/x2.smtv1.smt2
82 regress0/arrays/x3.smtv1.smt2
83 regress0/aufbv/array_rewrite_bug.smtv1.smt2
84 regress0/aufbv/bug00.smtv1.smt2
85 regress0/aufbv/bug338.smt2
86 regress0/aufbv/bug347.smtv1.smt2
87 regress0/aufbv/bug451.smtv1.smt2
88 regress0/aufbv/bug509.smtv1.smt2
89 regress0/aufbv/bug580.delta.smt2
90 regress0/aufbv/diseqprop.01.smtv1.smt2
91 regress0/aufbv/dubreva005ue.delta01.smtv1.smt2
92 regress0/aufbv/fifo32bc06k08.delta01.smtv1.smt2
93 regress0/aufbv/fuzz00.smtv1.smt2
94 regress0/aufbv/fuzz01.delta01.smtv1.smt2
95 regress0/aufbv/fuzz01.smtv1.smt2
96 regress0/aufbv/fuzz02.delta01.smtv1.smt2
97 regress0/aufbv/fuzz02.smtv1.smt2
98 regress0/aufbv/fuzz03.delta01.smtv1.smt2
99 regress0/aufbv/fuzz03.smtv1.smt2
100 regress0/aufbv/fuzz04.delta01.smtv1.smt2
101 regress0/aufbv/fuzz04.smtv1.smt2
102 regress0/aufbv/fuzz05.delta01.smtv1.smt2
103 regress0/aufbv/fuzz05.smtv1.smt2
104 regress0/aufbv/fuzz06.delta01.smtv1.smt2
105 regress0/aufbv/fuzz06.smtv1.smt2
106 regress0/aufbv/fuzz07.smtv1.smt2
107 regress0/aufbv/fuzz08.smtv1.smt2
108 regress0/aufbv/fuzz09.smtv1.smt2
109 regress0/aufbv/fuzz11.smtv1.smt2
110 regress0/aufbv/fuzz12.smtv1.smt2
111 regress0/aufbv/fuzz13.smtv1.smt2
112 regress0/aufbv/fuzz14.smtv1.smt2
113 regress0/aufbv/fuzz15.smtv1.smt2
114 regress0/aufbv/issue3737.smt2
115 regress0/aufbv/rewrite_bug.smtv1.smt2
116 regress0/aufbv/try3_sameret_functions_fse-bfs_tac.calc_next.il.fse-bfs.delta01.smtv1.smt2
117 regress0/aufbv/try5_small_difret_functions_wp_su.set_char_quoting.il.wp.delta01.smtv1.smt2
118 regress0/aufbv/wchains010ue.delta01.smtv1.smt2
119 regress0/aufbv/wchains010ue.delta02.smtv1.smt2
120 regress0/auflia/a17.smtv1.smt2
121 regress0/auflia/bug336.smt2
122 regress0/auflia/error72.delta2.smtv1.smt2
123 regress0/auflia/fuzz-error1099.smtv1.smt2
124 regress0/auflia/fuzz-error232.smtv1.smt2
125 regress0/auflia/fuzz01.delta01.smtv1.smt2
126 regress0/auflia/fuzz02.smtv1.smt2
127 regress0/auflia/fuzz03.smtv1.smt2
128 regress0/auflia/fuzz04.smtv1.smt2
129 regress0/auflia/fuzz05.smtv1.smt2
130 regress0/auflia/x2.smtv1.smt2
131 regress0/boolean-prec.cvc
132 regress0/boolean-terms-bug-array.smt2
133 regress0/boolean-terms-kernel1.smt2
134 regress0/boolean-terms.cvc
135 regress0/bt-test-00.smt2
136 regress0/bt-test-01.smt2
137 regress0/bug1247.smt2
138 regress0/bug161.smtv1.smt2
139 regress0/bug164.smtv1.smt2
140 regress0/bug167.smtv1.smt2
141 regress0/bug168.smtv1.smt2
145 regress0/bug239.smtv1.smt2
147 regress0/bug288.smtv1.smt2
148 regress0/bug288b.smtv1.smt2
149 regress0/bug288c.smtv1.smt2
161 regress0/bug421b.smt2
165 regress0/bug49.smtv1.smt2
166 regress0/bug512.minimized.smt2
167 regress0/bug521.minimized.smt2
169 regress0/bug528a.smt2
172 regress0/bug548a.smt2
174 regress0/bug576a.smt2
182 regress0/buggy-ite.smt2
183 regress0/bv/ackermann1.smt2
184 regress0/bv/ackermann2.smt2
185 regress0/bv/ackermann3.smt2
186 regress0/bv/ackermann4.smt2
187 regress0/bv/ackermann5.smt2
188 regress0/bv/ackermann6.smt2
189 regress0/bv/ackermann7.smt2
190 regress0/bv/ackermann8.smt2
191 regress0/bv/bool-model.smt2
192 regress0/bv/bool-to-bv-all.smt2
193 regress0/bv/bool-to-bv-all-array-bool.smt2
194 regress0/bv/bool-to-bv-ite-array-bool.smt2
195 regress0/bv/bool-to-bv-all-test.smt2
196 regress0/bv/bool-to-bv-ite.smt2
197 regress0/bv/bug260a.smtv1.smt2
198 regress0/bv/bug260b.smtv1.smt2
199 regress0/bv/bug440.smtv1.smt2
200 regress0/bv/bug733.smt2
201 regress0/bv/bug734.smt2
202 regress0/bv/bv-abstr-bug.smt2
203 regress0/bv/bv-abstr-bug2.smt2
204 regress0/bv/bv-int-collapse1.smt2
205 regress0/bv/bv-int-collapse2.smt2
206 regress0/bv/bv-options1.smt2
207 regress0/bv/bv-options2.smt2
208 regress0/bv/bv-options3.smt2
209 regress0/bv/bv-options4.smt2
210 regress0/bv/bv-to-bool1.smtv1.smt2
211 regress0/bv/bv-to-bool2.smt2
212 regress0/bv/bv_to_int1.smt2
213 regress0/bv/bv_to_int2.smt2
214 regress0/bv/bv_to_int_bvmul1.smt2
215 regress0/bv/bv_to_int_bvmul2.smt2
216 regress0/bv/bv_to_int_zext.smt2
217 regress0/bv/bv_to_int_bitwise.smt2
218 regress0/bv/bvuf_to_intuf.smt2
219 regress0/bv/bvuf_to_intuf_smtlib.smt2
220 regress0/bv/bvuf_to_intuf_sorts.smt2
221 regress0/bv/bv2nat-ground-c.smt2
222 regress0/bv/bv2nat-simp-range.smt2
223 regress0/bv/bvmul-pow2-only.smt2
224 regress0/bv/bvsimple.cvc
225 regress0/bv/calc2_sec2_shifter_mult_bmc15.atlas.delta01.smtv1.smt2
226 regress0/bv/core/a78test0002.smtv1.smt2
227 regress0/bv/core/a95test0002.smtv1.smt2
228 regress0/bv/core/bitvec0.smtv1.smt2
229 regress0/bv/core/bitvec2.smtv1.smt2
230 regress0/bv/core/bitvec5.smtv1.smt2
231 regress0/bv/core/bitvec7.smtv1.smt2
232 regress0/bv/core/bv_eq_diamond10.smtv1.smt2
233 regress0/bv/core/concat-merge-0.smtv1.smt2
234 regress0/bv/core/concat-merge-1.smtv1.smt2
235 regress0/bv/core/concat-merge-2.smtv1.smt2
236 regress0/bv/core/concat-merge-3.smtv1.smt2
237 regress0/bv/core/equality-00.smtv1.smt2
238 regress0/bv/core/equality-01.smtv1.smt2
239 regress0/bv/core/equality-02.smtv1.smt2
240 regress0/bv/core/equality-05.smtv1.smt2
241 regress0/bv/core/extract-concat-0.smtv1.smt2
242 regress0/bv/core/extract-concat-1.smtv1.smt2
243 regress0/bv/core/extract-concat-10.smtv1.smt2
244 regress0/bv/core/extract-concat-11.smtv1.smt2
245 regress0/bv/core/extract-concat-2.smtv1.smt2
246 regress0/bv/core/extract-concat-3.smtv1.smt2
247 regress0/bv/core/extract-concat-4.smtv1.smt2
248 regress0/bv/core/extract-concat-5.smtv1.smt2
249 regress0/bv/core/extract-concat-6.smtv1.smt2
250 regress0/bv/core/extract-concat-7.smtv1.smt2
251 regress0/bv/core/extract-concat-8.smtv1.smt2
252 regress0/bv/core/extract-concat-9.smtv1.smt2
253 regress0/bv/core/extract-constant.smtv1.smt2
254 regress0/bv/core/extract-extract-0.smtv1.smt2
255 regress0/bv/core/extract-extract-1.smtv1.smt2
256 regress0/bv/core/extract-extract-10.smtv1.smt2
257 regress0/bv/core/extract-extract-11.smtv1.smt2
258 regress0/bv/core/extract-extract-2.smtv1.smt2
259 regress0/bv/core/extract-extract-3.smtv1.smt2
260 regress0/bv/core/extract-extract-4.smtv1.smt2
261 regress0/bv/core/extract-extract-5.smtv1.smt2
262 regress0/bv/core/extract-extract-6.smtv1.smt2
263 regress0/bv/core/extract-extract-7.smtv1.smt2
264 regress0/bv/core/extract-extract-8.smtv1.smt2
265 regress0/bv/core/extract-extract-9.smtv1.smt2
266 regress0/bv/core/extract-whole-0.smtv1.smt2
267 regress0/bv/core/extract-whole-1.smtv1.smt2
268 regress0/bv/core/extract-whole-2.smtv1.smt2
269 regress0/bv/core/extract-whole-3.smtv1.smt2
270 regress0/bv/core/extract-whole-4.smtv1.smt2
271 regress0/bv/core/slice-01.smtv1.smt2
272 regress0/bv/core/slice-02.smtv1.smt2
273 regress0/bv/core/slice-03.smtv1.smt2
274 regress0/bv/core/slice-04.smtv1.smt2
275 regress0/bv/core/slice-05.smtv1.smt2
276 regress0/bv/core/slice-06.smtv1.smt2
277 regress0/bv/core/slice-07.smtv1.smt2
278 regress0/bv/core/slice-08.smtv1.smt2
279 regress0/bv/core/slice-09.smtv1.smt2
280 regress0/bv/core/slice-10.smtv1.smt2
281 regress0/bv/core/slice-11.smtv1.smt2
282 regress0/bv/core/slice-12.smtv1.smt2
283 regress0/bv/core/slice-13.smtv1.smt2
284 regress0/bv/core/slice-14.smtv1.smt2
285 regress0/bv/core/slice-15.smtv1.smt2
286 regress0/bv/core/slice-16.smtv1.smt2
287 regress0/bv/core/slice-17.smtv1.smt2
288 regress0/bv/core/slice-18.smtv1.smt2
289 regress0/bv/core/slice-19.smtv1.smt2
290 regress0/bv/core/slice-20.smtv1.smt2
291 regress0/bv/divtest_2_5.smt2
292 regress0/bv/divtest_2_6.smt2
293 regress0/bv/eager-inc-cadical.smt2
294 regress0/bv/eager-inc-cryptominisat.smt2
295 regress0/bv/eager-force-logic.smt2
296 regress0/bv/fuzz01.smtv1.smt2
297 regress0/bv/fuzz02.delta01.smtv1.smt2
298 regress0/bv/fuzz02.smtv1.smt2
299 regress0/bv/fuzz03.smtv1.smt2
300 regress0/bv/fuzz04.smtv1.smt2
301 regress0/bv/fuzz05.smtv1.smt2
302 regress0/bv/fuzz06.smtv1.smt2
303 regress0/bv/fuzz07.smtv1.smt2
304 regress0/bv/fuzz08.smtv1.smt2
305 regress0/bv/fuzz09.smtv1.smt2
306 regress0/bv/fuzz10.smtv1.smt2
307 regress0/bv/fuzz11.smtv1.smt2
308 regress0/bv/fuzz12.smtv1.smt2
309 regress0/bv/fuzz13.smtv1.smt2
310 regress0/bv/fuzz14.smtv1.smt2
311 regress0/bv/fuzz16.delta01.smtv1.smt2
312 regress0/bv/fuzz17.delta01.smtv1.smt2
313 regress0/bv/fuzz18.delta01.smtv1.smt2
314 regress0/bv/fuzz18.delta02.smtv1.smt2
315 regress0/bv/fuzz18.delta03.smtv1.smt2
316 regress0/bv/fuzz18.smtv1.smt2
317 regress0/bv/fuzz19.delta01.smtv1.smt2
318 regress0/bv/fuzz19.smtv1.smt2
319 regress0/bv/fuzz20.delta01.smtv1.smt2
320 regress0/bv/fuzz20.smtv1.smt2
321 regress0/bv/fuzz21.delta01.smtv1.smt2
322 regress0/bv/fuzz21.smtv1.smt2
323 regress0/bv/fuzz22.delta01.smtv1.smt2
324 regress0/bv/fuzz22.smtv1.smt2
325 regress0/bv/fuzz23.delta01.smtv1.smt2
326 regress0/bv/fuzz23.smtv1.smt2
327 regress0/bv/fuzz24.delta01.smtv1.smt2
328 regress0/bv/fuzz24.smtv1.smt2
329 regress0/bv/fuzz25.delta01.smtv1.smt2
330 regress0/bv/fuzz25.smtv1.smt2
331 regress0/bv/fuzz26.delta01.smtv1.smt2
332 regress0/bv/fuzz26.smtv1.smt2
333 regress0/bv/fuzz27.delta01.smtv1.smt2
334 regress0/bv/fuzz27.smtv1.smt2
335 regress0/bv/fuzz28.delta01.smtv1.smt2
336 regress0/bv/fuzz28.smtv1.smt2
337 regress0/bv/fuzz29.delta01.smtv1.smt2
338 regress0/bv/fuzz29.smtv1.smt2
339 regress0/bv/fuzz30.delta01.smtv1.smt2
340 regress0/bv/fuzz30.smtv1.smt2
341 regress0/bv/fuzz31.delta01.smtv1.smt2
342 regress0/bv/fuzz31.smtv1.smt2
343 regress0/bv/fuzz32.delta01.smtv1.smt2
344 regress0/bv/fuzz32.smtv1.smt2
345 regress0/bv/fuzz33.delta01.smtv1.smt2
346 regress0/bv/fuzz33.smtv1.smt2
347 regress0/bv/fuzz34.delta01.smtv1.smt2
348 regress0/bv/fuzz35.delta01.smtv1.smt2
349 regress0/bv/fuzz35.smtv1.smt2
350 regress0/bv/fuzz36.delta01.smtv1.smt2
351 regress0/bv/fuzz36.smtv1.smt2
352 regress0/bv/fuzz37.delta01.smtv1.smt2
353 regress0/bv/fuzz37.smtv1.smt2
354 regress0/bv/fuzz38.delta01.smtv1.smt2
355 regress0/bv/fuzz39.delta01.smtv1.smt2
356 regress0/bv/fuzz39.smtv1.smt2
357 regress0/bv/fuzz40.delta01.smtv1.smt2
358 regress0/bv/fuzz40.smtv1.smt2
359 regress0/bv/fuzz41.smtv1.smt2
360 regress0/bv/issue3621.smt2
361 regress0/bv/int_to_bv_err_on_demand_1.smt2
362 regress0/bv/mul-neg-unsat.smt2
363 regress0/bv/mul-negpow2.smt2
364 regress0/bv/mult-pow2-negative.smt2
365 regress0/bv/sizecheck.cvc
366 regress0/bv/smtcompbug.smtv1.smt2
367 regress0/bv/test-bv_intro_pow2.smt2
368 regress0/bv/unsound1-reduced.smt2
369 regress0/chained-equality.smt2
370 regress0/constant-rewrite.smtv1.smt2
371 regress0/cvc3.userdoc.01.cvc
372 regress0/cvc3.userdoc.02.cvc
373 regress0/cvc3.userdoc.03.cvc
374 regress0/cvc3.userdoc.04.cvc
375 regress0/cvc3.userdoc.05.cvc
376 regress0/cvc3.userdoc.06.cvc
377 regress0/cvc-rerror-print.cvc
378 regress0/datatypes/4482-unc-simp-one.smt2
379 regress0/datatypes/Test1-tup-mp.cvc
380 regress0/datatypes/boolean-equality.cvc
381 regress0/datatypes/boolean-terms-datatype.cvc
382 regress0/datatypes/boolean-terms-parametric-datatype-1.cvc
383 regress0/datatypes/boolean-terms-record.cvc
384 regress0/datatypes/boolean-terms-rewrite.cvc
385 regress0/datatypes/boolean-terms-tuple.cvc
386 regress0/datatypes/bug286.cvc
387 regress0/datatypes/bug438.cvc
388 regress0/datatypes/bug438b.cvc
389 regress0/datatypes/bug597-rbt.smt2
390 regress0/datatypes/bug604.smt2
391 regress0/datatypes/bug625.smt2
392 regress0/datatypes/cdt-model-cade15.smt2
393 regress0/datatypes/cdt-non-canon-stream.smt2
394 regress0/datatypes/coda_simp_model.smt2
395 regress0/datatypes/conqueue-dt-enum-iloop.smt2
396 regress0/datatypes/data-nested-codata.smt2
397 regress0/datatypes/datatype.cvc
398 regress0/datatypes/datatype0.cvc
399 regress0/datatypes/datatype1.cvc
400 regress0/datatypes/datatype13.cvc
401 regress0/datatypes/datatype2.cvc
402 regress0/datatypes/datatype3.cvc
403 regress0/datatypes/datatype4.cvc
404 regress0/datatypes/dt-2.6.smt2
405 regress0/datatypes/dt-match-pat-param-2.6.smt2
406 regress0/datatypes/dt-param-2.6.smt2
407 regress0/datatypes/dt-param-2.6-print.smt2
408 regress0/datatypes/dt-param-card4-bool-sat.smt2
409 regress0/datatypes/dt-sel-2.6.smt2
410 regress0/datatypes/empty_tuprec.cvc
411 regress0/datatypes/example-dailler-min.smt2
412 regress0/datatypes/is_test.smt2
413 regress0/datatypes/issue1433.smt2
414 regress0/datatypes/issue2838.cvc
415 regress0/datatypes/jsat-2.6.smt2
416 regress0/datatypes/model-subterms-min.smt2
417 regress0/datatypes/mutually-recursive.cvc
418 regress0/datatypes/pair-bool-bool.cvc
419 regress0/datatypes/pair-real-bool.smt2
420 regress0/datatypes/parametric-alt-list.cvc
421 regress0/datatypes/rec1.cvc
422 regress0/datatypes/rec2.cvc
423 regress0/datatypes/rec4.cvc
424 regress0/datatypes/repeated-selectors-2769.smt2
425 regress0/datatypes/rewriter.cvc
426 regress0/datatypes/sc-cdt1.smt2
427 regress0/datatypes/some-boolean-tests.cvc
428 regress0/datatypes/stream-singleton.smt2
429 regress0/datatypes/tenum-bug.smt2
430 regress0/datatypes/tree-get-value.cvc
431 regress0/datatypes/tuple-model.cvc
432 regress0/datatypes/tuple-no-clash.cvc
433 regress0/datatypes/tuple-record-bug.cvc
434 regress0/datatypes/tuple.cvc
435 regress0/datatypes/tuples-empty.smt2
436 regress0/datatypes/tuples-multitype.smt2
437 regress0/datatypes/typed_v10l30054.cvc
438 regress0/datatypes/typed_v1l80005.cvc
439 regress0/datatypes/typed_v2l30079.cvc
440 regress0/datatypes/typed_v3l20092.cvc
441 regress0/datatypes/typed_v5l30069.cvc
442 regress0/datatypes/v10l40099.cvc
443 regress0/datatypes/v2l40025.cvc
444 regress0/datatypes/v3l60006.cvc
445 regress0/datatypes/v5l30058.cvc
446 regress0/datatypes/wrong-sel-simp.cvc
447 regress0/decision/aufbv-fuzz01.smtv1.smt2
448 regress0/decision/bitvec0.delta01.smtv1.smt2
449 regress0/decision/bitvec0.smtv1.smt2
450 regress0/decision/bitvec5.smtv1.smt2
451 regress0/decision/bug347.smtv1.smt2
452 regress0/decision/bug374a.smtv1.smt2
453 regress0/decision/bug374b.smt2
454 regress0/decision/error122.delta01.smtv1.smt2
455 regress0/decision/error122.smtv1.smt2
456 regress0/decision/error20.delta01.smtv1.smt2
457 regress0/decision/error20.smtv1.smt2
458 regress0/decision/error3.delta01.smtv1.smt2
459 regress0/decision/pp-regfile.delta01.smtv1.smt2
460 regress0/decision/pp-regfile.delta02.smtv1.smt2
461 regress0/decision/quant-ex1.smt2
462 regress0/decision/uflia-xs-09-16-3-4-1-5.delta03.smtv1.smt2
463 regress0/decision/wchains010ue.delta02.smtv1.smt2
464 regress0/declare-fun-is-match.smt2
465 regress0/declare-funs.smt2
466 regress0/define-fun-model.smt2
467 regress0/distinct.smtv1.smt2
468 regress0/dump-unsat-core-full.smt2
469 regress0/simple-dump-model.smt2
470 regress0/expect/scrub.01.smtv1.smt2
471 regress0/expect/scrub.03.smt2
472 regress0/expect/scrub.06.cvc
473 regress0/expect/scrub.08.sy
474 regress0/expect/scrub.09.p
475 regress0/flet.smtv1.smt2
476 regress0/flet2.smtv1.smt2
477 regress0/fmf/Arrow_Order-smtlib.778341.smtv1.smt2
478 regress0/fmf/QEpres-uf.855035.smtv1.smt2
479 regress0/fmf/array_card.smt2
480 regress0/fmf/bounded_sets.smt2
481 regress0/fmf/bug-041417-set-options.cvc
482 regress0/fmf/bug652.smt2
483 regress0/fmf/bug782.smt2
484 regress0/fmf/cruanes-no-minimal-unk.smt2
485 regress0/fmf/fc-simple.smt2
486 regress0/fmf/fc-unsat-pent.smt2
487 regress0/fmf/fc-unsat-tot-2.smt2
488 regress0/fmf/fd-false.smt2
489 regress0/fmf/fmc_unsound_model.smt2
490 regress0/fmf/fmf-strange-bounds-2.smt2
491 regress0/fmf/forall_unit_data2.smt2
492 regress0/fmf/issue3661-ccard-dec.smt2
493 regress0/fmf/krs-sat.smt2
494 regress0/fmf/no-minimal-sat.smt2
495 regress0/fmf/quant_real_univ.cvc
496 regress0/fmf/sat-logic.smt2
497 regress0/fmf/sc_bad_model_1221.smt2
498 regress0/fmf/sort-infer-typed-082718.smt2
499 regress0/fmf/syn002-si-real-int.smt2
500 regress0/fmf/tail_rec.smt2
501 regress0/fp/abs-unsound.smt2
502 regress0/fp/abs-unsound2.smt2
503 regress0/fp/down-cast-RNA.smt2
504 regress0/fp/ext-rew-test.smt2
505 regress0/fp/issue3536.smt2
506 regress0/fp/issue3619.smt2
507 regress0/fp/issue4277-assign-func.smt2
508 regress0/fp/rti_3_5_bug.smt2
509 regress0/fp/rti_3_5_bug_report.smt2
510 regress0/fp/simple.smt2
511 regress0/fp/wrong-model.smt2
512 regress0/fuzz_1.smtv1.smt2
513 regress0/fuzz_3.smtv1.smt2
514 regress0/get-value-incremental.smt2
515 regress0/get-value-ints.smt2
516 regress0/get-value-reals-ints.smt2
517 regress0/get-value-reals.smt2
518 regress0/ho/apply-collapse-sat.smt2
519 regress0/ho/apply-collapse-unsat.smt2
520 regress0/ho/bug_nodbuilding_interpreted_SYO042^1.p
521 regress0/ho/cong-full-apply.smt2
522 regress0/ho/cong.smt2
523 regress0/ho/declare-fun-variants.smt2
524 regress0/ho/def-fun-flatten.smt2
525 regress0/ho/ext-finite-unsat.smt2
526 regress0/ho/ext-ho-nested-lambda-model.smt2
527 regress0/ho/ext-ho.smt2
528 regress0/ho/ext-sat-partial-eval.smt2
529 regress0/ho/ext-sat.smt2
530 regress0/ho/finite-fun-ext.smt2
531 regress0/ho/fta0144-alpha-eq.smt2
532 regress0/ho/fta0210.smt2
533 regress0/ho/fun-subtyping.smt2
534 regress0/ho/ho-exponential-model.smt2
535 regress0/ho/ho-match-fun-suffix.smt2
536 regress0/ho/ho-matching-enum.smt2
537 regress0/ho/ho-matching-enum-2.smt2
538 regress0/ho/ho-matching-nested-app.smt2
539 regress0/ho/ho-std-fmf.smt2
540 regress0/ho/hoa0008.smt2
541 regress0/ho/ite-apply-eq.smt2
542 regress0/ho/lambda-equality-non-canon.smt2
543 regress0/ho/match-middle.smt2
544 regress0/ho/modulo-func-equality.smt2
545 regress0/ho/shadowing-defs.smt2
546 regress0/ho/simple-matching-partial.smt2
547 regress0/ho/simple-matching.smt2
548 regress0/ho/trans.smt2
549 regress0/hung10_itesdk_output1.smt2
550 regress0/hung13sdk_output1.smt2
551 regress0/ineq_basic.smtv1.smt2
552 regress0/ineq_slack.smtv1.smt2
553 regress0/issue1063-overloading-dt-cons.smt2
554 regress0/issue1063-overloading-dt-fun.smt2
555 regress0/issue1063-overloading-dt-sel.smt2
556 regress0/issue2832-qualId.smt2
557 regress0/issue4010-sort-inf-var.smt2
558 regress0/issue4469-unc-no-reuse-var.smt2
563 regress0/ite_real_int_type.smtv1.smt2
564 regress0/ite_real_valid.smtv1.smt2
565 regress0/lang_opts_2_5.smt2
566 regress0/lang_opts_2_6_1.smt2
567 regress0/lemmas/clocksynchro_5clocks.main_invar.base.model.smtv1.smt2
568 regress0/lemmas/fs_not_sc_seen.induction.smtv1.smt2
569 regress0/lemmas/mode_cntrl.induction.smtv1.smt2
570 regress0/lemmas/sc_init_frame_gap.induction.smtv1.smt2
572 regress0/let.smtv1.smt2
573 regress0/let2.smtv1.smt2
574 regress0/logops.01.cvc
575 regress0/logops.02.cvc
576 regress0/logops.03.cvc
577 regress0/logops.04.cvc
578 regress0/logops.05.cvc
579 regress0/model-core.smt2
580 regress0/nl/coeff-sat.smt2
581 regress0/nl/ext-rew-aggr-test.smt2
582 regress0/nl/issue3003.smt2
583 regress0/nl/issue3407.smt2
584 regress0/nl/issue3411.smt2
585 regress0/nl/issue3475.smt2
586 regress0/nl/issue3652.smt2
587 regress0/nl/issue3718.smt2
588 regress0/nl/issue3719.smt2
589 regress0/nl/issue3729-cm-solved-tf.smt2
590 regress0/nl/issue3959.smt2
591 regress0/nl/issue3971.smt2
592 regress0/nl/issue3991.smt2
593 regress0/nl/issue4007-rint-uf.smt2
594 regress0/nl/magnitude-wrong-1020-m.smt2
595 regress0/nl/mult-po.smt2
596 regress0/nl/nia-wrong-tl.smt2
597 regress0/nl/nlExtPurify-test.smt2
598 regress0/nl/nta/cos-sig-value.smt2
599 regress0/nl/nta/exp-n0.5-lb.smt2
600 regress0/nl/nta/exp-n0.5-ub.smt2
601 regress0/nl/nta/exp-neg2-unsat-unsound.smt2
602 regress0/nl/nta/exp1-ub.smt2
603 regress0/nl/nta/real-pi.smt2
604 regress0/nl/nta/sin-sym.smt2
605 regress0/nl/nta/sqrt-simple.smt2
606 regress0/nl/nta/tan-rewrite.smt2
607 regress0/nl/real-as-int.smt2
608 regress0/nl/real-div-ufnra.smt2
609 regress0/nl/sin-cos-346-b-chunk-0169.smt2
610 regress0/nl/sqrt.smt2
611 regress0/nl/sqrt2-value.smt2
612 regress0/nl/subs0-unsat-confirm.smt2
613 regress0/nl/very-easy-sat.smt2
614 regress0/nl/very-simple-unsat.smt2
615 regress0/options/invalid_dump.smt2
616 regress0/options/invalid_option_inc_proofs.smt2
617 regress0/opt-abd-no-use.smt2
618 regress0/parallel-let.smt2
619 regress0/parser/as.smt2
620 regress0/parser/bv_arity_smt2.6.smt2
621 regress0/parser/bv_nat.smt2
622 regress0/parser/constraint.smt2
623 regress0/parser/declarefun-emptyset-uf.smt2
624 regress0/parser/force_logic_set_logic.smt2
625 regress0/parser/force_logic_success.smt2
626 regress0/parser/shadow_fun_symbol_all.smt2
627 regress0/parser/shadow_fun_symbol_nirat.smt2
628 regress0/parser/strings20.smt2
629 regress0/parser/strings25.smt2
630 regress0/parser/to_fp.smt2
631 regress0/precedence/and-not.cvc
632 regress0/precedence/and-xor.cvc
633 regress0/precedence/bool-cmp.cvc
634 regress0/precedence/cmp-plus.cvc
635 regress0/precedence/eq-fun.cvc
636 regress0/precedence/iff-assoc.cvc
637 regress0/precedence/iff-implies.cvc
638 regress0/precedence/implies-assoc.cvc
639 regress0/precedence/implies-iff.cvc
640 regress0/precedence/implies-or.cvc
641 regress0/precedence/not-and.cvc
642 regress0/precedence/not-eq.cvc
643 regress0/precedence/or-implies.cvc
644 regress0/precedence/or-xor.cvc
645 regress0/precedence/plus-mult.cvc
646 regress0/precedence/xor-and.cvc
647 regress0/precedence/xor-assoc.cvc
648 regress0/precedence/xor-or.cvc
649 regress0/preprocess/preprocess_00.cvc
650 regress0/preprocess/preprocess_01.cvc
651 regress0/preprocess/preprocess_02.cvc
652 regress0/preprocess/preprocess_03.cvc
653 regress0/preprocess/preprocess_04.cvc
654 regress0/preprocess/preprocess_05.cvc
655 regress0/preprocess/preprocess_06.cvc
656 regress0/preprocess/preprocess_07.cvc
657 regress0/preprocess/preprocess_08.cvc
658 regress0/preprocess/preprocess_09.cvc
659 regress0/preprocess/preprocess_10.cvc
660 regress0/preprocess/preprocess_11.cvc
661 regress0/preprocess/preprocess_12.cvc
662 regress0/preprocess/preprocess_13.cvc
663 regress0/preprocess/preprocess_14.cvc
664 regress0/preprocess/preprocess_15.cvc
665 regress0/print_lambda.cvc
666 regress0/print_model.cvc
667 regress0/printer/bv_consts_bin.smt2
668 regress0/printer/bv_consts_dec.smt2
669 regress0/printer/empty_sort.smt2
670 regress0/printer/empty_symbol_name.smt2
671 regress0/printer/let_shadowing.smt2
672 regress0/printer/symbol_starting_w_digit.smt2
673 regress0/printer/tuples_and_records.cvc
674 regress0/proof_no_support.smt2
675 regress0/push-pop/boolean/fuzz_12.smt2
676 regress0/push-pop/boolean/fuzz_13.smt2
677 regress0/push-pop/boolean/fuzz_14.smt2
678 regress0/push-pop/boolean/fuzz_18.smt2
679 regress0/push-pop/boolean/fuzz_2.smt2
680 regress0/push-pop/boolean/fuzz_21.smt2
681 regress0/push-pop/boolean/fuzz_22.smt2
682 regress0/push-pop/boolean/fuzz_27.smt2
683 regress0/push-pop/boolean/fuzz_3.smt2
684 regress0/push-pop/boolean/fuzz_31.smt2
685 regress0/push-pop/boolean/fuzz_33.smt2
686 regress0/push-pop/boolean/fuzz_36.smt2
687 regress0/push-pop/boolean/fuzz_38.smt2
688 regress0/push-pop/boolean/fuzz_46.smt2
689 regress0/push-pop/boolean/fuzz_47.smt2
690 regress0/push-pop/boolean/fuzz_48.smt2
691 regress0/push-pop/boolean/fuzz_49.smt2
692 regress0/push-pop/boolean/fuzz_50.smt2
693 regress0/push-pop/bug1990.smt2
694 regress0/push-pop/bug233.cvc
695 regress0/push-pop/bug654-dd.smt2
696 regress0/push-pop/bug691.smt2
697 regress0/push-pop/bug821-check_sat_assuming.smt2
698 regress0/push-pop/bug821.smt2
699 regress0/push-pop/inc-define.smt2
700 regress0/push-pop/inc-double-u.smt2
701 regress0/push-pop/incremental-subst-bug.cvc
702 regress0/push-pop/issue1986.smt2
703 regress0/push-pop/issue2137.min.smt2
704 regress0/push-pop/quant-fun-proc-unfd.smt2
705 regress0/push-pop/real-as-int-incremental.smt2
706 regress0/push-pop/simple_unsat_cores.smt2
707 regress0/push-pop/test.00.cvc
708 regress0/push-pop/test.01.cvc
709 regress0/push-pop/tiny_bug.smt2
710 regress0/push-pop/units.cvc
711 regress0/quantifiers/ARI176e1.smt2
712 regress0/quantifiers/agg-rew-test-cf.smt2
713 regress0/quantifiers/agg-rew-test.smt2
714 regress0/quantifiers/ari056.smt2
715 regress0/quantifiers/bug269.smt2
716 regress0/quantifiers/bug290.smt2
717 regress0/quantifiers/bug291.smt2
718 regress0/quantifiers/bug749-rounding.smt2
719 regress0/quantifiers/cbqi-lia-dt-simp.smt2
720 regress0/quantifiers/cegqi-nl-simp.cvc
721 regress0/quantifiers/cegqi-nl-sq.smt2
722 regress0/quantifiers/clock-10.smt2
723 regress0/quantifiers/clock-3.smt2
724 regress0/quantifiers/cond-var-elim-binary.smt2
725 regress0/quantifiers/delta-simp.smt2
726 regress0/quantifiers/double-pattern.smt2
727 regress0/quantifiers/ex3.smt2
728 regress0/quantifiers/ex6.smt2
729 regress0/quantifiers/floor.smt2
730 regress0/quantifiers/horn-ground-pre-post.smt2
731 regress0/quantifiers/is-even-pred.smt2
732 regress0/quantifiers/is-int.smt2
733 regress0/quantifiers/issue1805.smt2
734 regress0/quantifiers/issue2031-bv-var-elim.smt2
735 regress0/quantifiers/issue2033-macro-arith.smt2
736 regress0/quantifiers/issue2035.smt2
737 regress0/quantifiers/issue3655.smt2
738 regress0/quantifiers/issue4086-infs.smt2
739 regress0/quantifiers/issue4275-qcf-cegqi-rep.smt2
740 regress0/quantifiers/lra-triv-gn.smt2
741 regress0/quantifiers/macros-int-real.smt2
742 regress0/quantifiers/macros-real-arg.smt2
743 regress0/quantifiers/matching-lia-1arg.smt2
744 regress0/quantifiers/mix-complete-strat.smt2
745 regress0/quantifiers/mix-match.smt2
746 regress0/quantifiers/mix-simp.smt2
747 regress0/quantifiers/nested-delta.smt2
748 regress0/quantifiers/nested-inf.smt2
749 regress0/quantifiers/partial-trigger.smt2
750 regress0/quantifiers/pure_dt_cbqi.smt2
751 regress0/quantifiers/qarray-sel-over-store.smt2
752 regress0/quantifiers/qbv-inequality2.smt2
753 regress0/quantifiers/qbv-simp.smt2
754 regress0/quantifiers/qbv-test-invert-bvadd-neq.smt2
755 regress0/quantifiers/qbv-test-invert-bvand-neq.smt2
756 regress0/quantifiers/qbv-test-invert-bvand.smt2
757 regress0/quantifiers/qbv-test-invert-bvashr-0-neq.smt2
758 regress0/quantifiers/qbv-test-invert-bvashr-1-neq.smt2
759 regress0/quantifiers/qbv-test-invert-bvlshr-0-neq.smt2
760 regress0/quantifiers/qbv-test-invert-bvlshr-0.smt2
761 regress0/quantifiers/qbv-test-invert-bvlshr-1-neq.smt2
762 regress0/quantifiers/qbv-test-invert-bvor-neq.smt2
763 regress0/quantifiers/qbv-test-invert-bvor.smt2
764 regress0/quantifiers/qbv-test-invert-bvshl-0.smt2
765 regress0/quantifiers/qbv-test-invert-bvult-1.smt2
766 regress0/quantifiers/qbv-test-invert-bvxor-neq.smt2
767 regress0/quantifiers/qbv-test-invert-bvxor.smt2
768 regress0/quantifiers/qbv-test-invert-concat-0.smt2
769 regress0/quantifiers/qbv-test-invert-concat-1.smt2
770 regress0/quantifiers/qbv-test-invert-sign-extend.smt2
771 regress0/quantifiers/qcf-rel-dom-opt.smt2
772 regress0/quantifiers/quant-model-simplification.smt2
773 regress0/quantifiers/rew-to-scala.smt2
774 regress0/quantifiers/simp-len.smt2
775 regress0/quantifiers/simp-typ-test.smt2
776 regress0/quantifiers/sygus-inst-nia-psyco-060.smt2
777 regress0/quantifiers/sygus-inst-ufnia-sat-t3_rw1505.smt2
778 regress0/rec-fun-const-parse-bug.smt2
779 regress0/rels/addr_book_0.cvc
780 regress0/rels/atom_univ2.cvc
781 regress0/rels/card_transpose.cvc
782 regress0/rels/iden_0.cvc
783 regress0/rels/iden_1.cvc
784 regress0/rels/join-eq-u-sat.cvc
785 regress0/rels/join-eq-u.cvc
786 regress0/rels/joinImg_0.cvc
787 regress0/rels/oneLoc_no_quant-int_0_1.cvc
788 regress0/rels/rel_1tup_0.cvc
789 regress0/rels/rel_complex_0.cvc
790 regress0/rels/rel_complex_1.cvc
791 regress0/rels/rel_conflict_0.cvc
792 regress0/rels/rel_join_0.cvc
793 regress0/rels/rel_join_0_1.cvc
794 regress0/rels/rel_join_1.cvc
795 regress0/rels/rel_join_1_1.cvc
796 regress0/rels/rel_join_2.cvc
797 regress0/rels/rel_join_2_1.cvc
798 regress0/rels/rel_join_3.cvc
799 regress0/rels/rel_join_3_1.cvc
800 regress0/rels/rel_join_4.cvc
801 regress0/rels/rel_join_5.cvc
802 regress0/rels/rel_join_6.cvc
803 regress0/rels/rel_join_7.cvc
804 regress0/rels/rel_product_0.cvc
805 regress0/rels/rel_product_0_1.cvc
806 regress0/rels/rel_product_1.cvc
807 regress0/rels/rel_product_1_1.cvc
808 regress0/rels/rel_symbolic_1.cvc
809 regress0/rels/rel_symbolic_1_1.cvc
810 regress0/rels/rel_symbolic_2_1.cvc
811 regress0/rels/rel_symbolic_3_1.cvc
812 regress0/rels/rel_tc_11.cvc
813 regress0/rels/rel_tc_2_1.cvc
814 regress0/rels/rel_tc_3.cvc
815 regress0/rels/rel_tc_3_1.cvc
816 regress0/rels/rel_tc_7.cvc
817 regress0/rels/rel_tc_8.cvc
818 regress0/rels/rel_tp_3_1.cvc
819 regress0/rels/rel_tp_join_0.cvc
820 regress0/rels/rel_tp_join_1.cvc
821 regress0/rels/rel_tp_join_2.cvc
822 regress0/rels/rel_tp_join_3.cvc
823 regress0/rels/rel_tp_join_eq_0.cvc
824 regress0/rels/rel_tp_join_int_0.cvc
825 regress0/rels/rel_tp_join_pro_0.cvc
826 regress0/rels/rel_tp_join_var_0.cvc
827 regress0/rels/rel_transpose_0.cvc
828 regress0/rels/rel_transpose_1.cvc
829 regress0/rels/rel_transpose_1_1.cvc
830 regress0/rels/rel_transpose_3.cvc
831 regress0/rels/rel_transpose_4.cvc
832 regress0/rels/rel_transpose_5.cvc
833 regress0/rels/rel_transpose_6.cvc
834 regress0/rels/rel_transpose_7.cvc
835 regress0/rels/relations-ops.smt2
836 regress0/rels/rels-sharing-simp.cvc
837 regress0/sep/dispose-1.smt2
838 regress0/sep/dup-nemp.smt2
839 regress0/sep/issue3720-check-model.smt2
840 regress0/sep/nemp.smt2
841 regress0/sep/nil-no-elim.smt2
842 regress0/sep/nspatial-simp.smt2
843 regress0/sep/pto-01.smt2
844 regress0/sep/pto-02.smt2
845 regress0/sep/sep-01.smt2
846 regress0/sep/sep-plus1.smt2
847 regress0/sep/sep-simp-unsat-emp.smt2
848 regress0/sep/skolem_emp.smt2
849 regress0/sep/trees-1.smt2
850 regress0/sep/wand-crash.smt2
851 regress0/sets/abt-min.smt2
852 regress0/sets/abt-te-exh.smt2
853 regress0/sets/abt-te-exh2.smt2
854 regress0/sets/card-2.smt2
855 regress0/sets/card-3sets.cvc
856 regress0/sets/card.smt2
857 regress0/sets/card3-ground.smt2
858 regress0/sets/complement.cvc
859 regress0/sets/complement2.cvc
860 regress0/sets/complement3.cvc
861 regress0/sets/comp-qf-error.smt2
862 regress0/sets/cvc-sample.cvc
863 regress0/sets/dt-simp-mem.smt2
864 regress0/sets/emptyset.smt2
865 regress0/sets/eqtest.smt2
866 regress0/sets/error1.smt2
867 regress0/sets/error2.smt2
868 regress0/sets/insert.smt2
869 regress0/sets/int-real-univ-unsat.smt2
870 regress0/sets/int-real-univ.smt2
871 regress0/sets/jan24/deepmeas0.hs.fqout.cvc4.47.smt2
872 regress0/sets/jan24/deepmeas0.hs.fqout.small.smt2
873 regress0/sets/jan27/ListConcat.hs.fqout.177minimized.smt2
874 regress0/sets/jan27/ListConcat.hs.fqout.cvc4.177.smt2
875 regress0/sets/jan28/TalkingAboutSets.hs.fqout.3577minimized.smt2
876 regress0/sets/jan30/UniqueZipper.hs.fqout.minimized10.smt2
877 regress0/sets/jan30/UniqueZipper.hs.fqout.minimized1832.smt2
878 regress0/sets/mar2014/sharing-preregister.smt2
879 regress0/sets/mar2014/small.smt2
880 regress0/sets/mar2014/smaller.smt2
881 regress0/sets/nonvar-univ.smt2
882 regress0/sets/pre-proc-univ.smt2
883 regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2
884 regress0/sets/sets-equal.smt2
885 regress0/sets/sets-extr.smt2
886 regress0/sets/sets-inter.smt2
887 regress0/sets/sets-of-sets-subtypes.smt2
888 regress0/sets/sets-poly-int-real.smt2
889 regress0/sets/sets-poly-nonint.smt2
890 regress0/sets/sets-sample.smt2
891 regress0/sets/sets-sharing.smt2
892 regress0/sets/sets-testlemma.smt2
893 regress0/sets/sets-union.smt2
894 regress0/sets/sharing-simp.smt2
895 regress0/sets/union-1a-flip.smt2
896 regress0/sets/union-1a.smt2
897 regress0/sets/union-1b-flip.smt2
898 regress0/sets/union-1b.smt2
899 regress0/sets/union-2.smt2
900 regress0/sets/univset-simp.smt2
901 regress0/simple-lra.smtv1.smt2
902 regress0/simple-lra.smt2
903 regress0/simple-rdl.smtv1.smt2
904 regress0/simple-rdl.smt2
905 regress0/simple-uf.smtv1.smt2
906 regress0/simple-uf.smt2
908 regress0/simple.smtv1.smt2
909 regress0/simple2.smtv1.smt2
910 regress0/simplification_bug.smtv1.smt2
911 regress0/simplification_bug2.smtv1.smt2
912 regress0/smallcnf.cvc
913 regress0/smt2output.smt2
914 regress0/smtlib/get-unsat-assumptions.smt2
915 regress0/smtlib/global-decls.smt2
916 regress0/smtlib/issue4028.smt2
917 regress0/smtlib/issue4077.smt2
918 regress0/smtlib/issue4151.smt2
919 regress0/smtlib/reason-unknown.smt2
920 regress0/smtlib/reset.smt2
921 regress0/smtlib/reset-assertions1.smt2
922 regress0/smtlib/reset-assertions2.smt2
923 regress0/smtlib/reset-assertions-global.smt2
924 regress0/smtlib/reset-force-logic.smt2
925 regress0/smtlib/reset-set-logic.smt2
926 regress0/smtlib/set-info-status.smt2
927 regress0/strings/bidir_star.smt2
928 regress0/strings/bug001.smt2
929 regress0/strings/bug002.smt2
930 regress0/strings/bug612.smt2
931 regress0/strings/bug613.smt2
932 regress0/strings/char-representations.smt2
933 regress0/strings/code-eval.smt2
934 regress0/strings/code-perf.smt2
935 regress0/strings/code-sat-neg-one.smt2
936 regress0/strings/complement-simple.smt2
937 regress0/strings/escchar.smt2
938 regress0/strings/escchar_25.smt2
939 regress0/strings/from_code.smt2
940 regress0/strings/gen-esc-seq.smt2
941 regress0/strings/hconst-092618.smt2
942 regress0/strings/idof-rewrites.smt2
943 regress0/strings/idof-sem.smt2
944 regress0/strings/ilc-like.smt2
945 regress0/strings/indexof-sym-simp.smt2
946 regress0/strings/is_digit_simple.smt2
947 regress0/strings/issue1189.smt2
948 regress0/strings/issue2958.smt2
949 regress0/strings/issue3440.smt2
950 regress0/strings/issue3497.smt2
951 regress0/strings/issue3657-evalLeq.smt2
952 regress0/strings/issue4070.smt2
953 regress0/strings/issue4376.smt2
954 regress0/strings/itos-entail.smt2
955 regress0/strings/large-model.smt2
956 regress0/strings/leadingzero001.smt2
957 regress0/strings/loop001.smt2
958 regress0/strings/loop-wrong-sem.smt2
959 regress0/strings/model001.smt2
960 regress0/strings/model-code-point.smt2
961 regress0/strings/model-friendly.smt2
962 regress0/strings/ncontrib-rewrites.smt2
963 regress0/strings/norn-31.smt2
964 regress0/strings/norn-simp-rew.smt2
965 regress0/strings/parser-syms.cvc
966 regress0/strings/quad-028-2-2-unsat.smt2
967 regress0/strings/re.all.smt2
968 regress0/strings/re-in-rewrite.smt2
969 regress0/strings/re-syntax.smt2
970 regress0/strings/re_diff.smt2
971 regress0/strings/regexp-native-simple.cvc
972 regress0/strings/regexp_inclusion.smt2
973 regress0/strings/regexp_inclusion_reduction.smt2
974 regress0/strings/repl-rewrites2.smt2
975 regress0/strings/replace-const.smt2
976 regress0/strings/replaceall-eval.smt2
977 regress0/strings/rewrites-re-concat.smt2
978 regress0/strings/rewrites-v2.smt2
979 regress0/strings/std2.6.1.smt2
980 regress0/strings/str003.smt2
981 regress0/strings/str004.smt2
982 regress0/strings/str005.smt2
983 regress0/strings/str_unsound_ext_rew_eq.smt2
984 regress0/strings/str-rev-simple.smt2
985 regress0/strings/strings-charat.cvc
986 regress0/strings/strings-native-simple.cvc
987 regress0/strings/strip-endpoint-itos.smt2
988 regress0/strings/substr-rewrites.smt2
989 regress0/strings/tolower-rrs.smt2
990 regress0/strings/tolower-simple.smt2
991 regress0/strings/type001.smt2
992 regress0/strings/unicode-esc.smt2
993 regress0/strings/unsound-0908.smt2
994 regress0/strings/unsound-repl-rewrite.smt2
995 regress0/sygus/General_plus10.sy
996 regress0/sygus/aig-si.sy
997 regress0/sygus/array-grammar-select.sy
998 regress0/sygus/array-grammar-store.sy
999 regress0/sygus/c100.sy
1000 regress0/sygus/ccp16.lus.sy
1001 regress0/sygus/cegqi-si-string-triv.sy
1002 regress0/sygus/cegqi-si-string-triv-2fun.sy
1003 regress0/sygus/check-generic-red.sy
1004 regress0/sygus/const-var-test.sy
1005 regress0/sygus/dt-no-syntax.sy
1006 regress0/sygus/dt-sel-parse1.sy
1007 regress0/sygus/hd-05-d1-prog-nogrammar.sy
1008 regress0/sygus/inv-different-var-order.sy
1009 regress0/sygus/issue3356-syg-inf-usort.smt2
1010 regress0/sygus/issue3624.sy
1011 regress0/sygus/issue3645-grammar-sets.smt2
1012 regress0/sygus/issue4383-cache-fv-id.sy
1013 regress0/sygus/let-ringer.sy
1014 regress0/sygus/let-simp.sy
1015 regress0/sygus/no-logic.sy
1016 regress0/sygus/no-syntax-test-bool.sy
1017 regress0/sygus/no-syntax-test.sy
1018 regress0/sygus/parity-AIG-d0.sy
1019 regress0/sygus/parse-bv-let.sy
1020 regress0/sygus/pbe-pred-contra.sy
1021 regress0/sygus/pLTL-sygus-syntax-err.sy
1022 regress0/sygus/print-define-fun.sy
1023 regress0/sygus/real-si-all.sy
1024 regress0/sygus/sygus-no-wf.sy
1025 regress0/sygus/sygus-uf.sy
1026 regress0/sygus/strings-unconstrained.sy
1027 regress0/sygus/uminus_one.sy
1028 regress0/sygus/univ_3-long-repeat-conflict.sy
1031 regress0/tptp/ARI086=1.p
1032 regress0/tptp/DAT001=1.p
1033 regress0/tptp/KRS018+1.p
1034 regress0/tptp/KRS063+1.p
1035 regress0/tptp/MGT019+2.p
1036 regress0/tptp/MGT041-2.p
1037 regress0/tptp/PUZ131_1.p
1038 regress0/tptp/SYN000+1.p
1039 regress0/tptp/SYN000+2.p
1040 regress0/tptp/SYN000-1.p
1041 regress0/tptp/SYN000-2.p
1042 regress0/tptp/SYN000=2.p
1043 regress0/tptp/SYN000_1.p
1044 regress0/tptp/SYN000_2.p
1045 regress0/tptp/SYN075-1.p
1046 regress0/tptp/is_rat_simple.p
1047 regress0/tptp/tff0-arith.p
1048 regress0/tptp/tff0.p
1049 regress0/tptp/tptp_parser.p
1050 regress0/tptp/tptp_parser10.p
1051 regress0/tptp/tptp_parser2.p
1052 regress0/tptp/tptp_parser3.p
1053 regress0/tptp/tptp_parser4.p
1054 regress0/tptp/tptp_parser5.p
1055 regress0/tptp/tptp_parser6.p
1056 regress0/tptp/tptp_parser7.p
1057 regress0/tptp/tptp_parser8.p
1058 regress0/tptp/tptp_parser9.p
1059 regress0/uf/NEQ016_size5_reduced2a.smtv1.smt2
1060 regress0/uf/NEQ016_size5_reduced2b.smtv1.smt2
1061 regress0/uf/bool-pred-nested.smt2
1062 regress0/uf/ccredesign-fuzz.smtv1.smt2
1063 regress0/uf/cnf-and-neg.smt2
1064 regress0/uf/cnf-iff-base.smt2
1065 regress0/uf/cnf-iff.smt2
1066 regress0/uf/cnf-ite.smt2
1067 regress0/uf/cnf_abc.smt2
1068 regress0/uf/dead_dnd002.smtv1.smt2
1069 regress0/uf/eq_diamond1.smtv1.smt2
1070 regress0/uf/eq_diamond14.reduced.smtv1.smt2
1071 regress0/uf/eq_diamond14.reduced2.smtv1.smt2
1072 regress0/uf/eq_diamond23.smtv1.smt2
1073 regress0/uf/euf_simp01.smtv1.smt2
1074 regress0/uf/euf_simp02.smtv1.smt2
1075 regress0/uf/euf_simp03.smtv1.smt2
1076 regress0/uf/euf_simp04.smtv1.smt2
1077 regress0/uf/euf_simp05.smtv1.smt2
1078 regress0/uf/euf_simp06.smtv1.smt2
1079 regress0/uf/euf_simp08.smtv1.smt2
1080 regress0/uf/euf_simp09.smtv1.smt2
1081 regress0/uf/euf_simp10.smtv1.smt2
1082 regress0/uf/euf_simp11.smtv1.smt2
1083 regress0/uf/euf_simp12.smtv1.smt2
1084 regress0/uf/euf_simp13.smtv1.smt2
1085 regress0/uf/iso_brn001.smtv1.smt2
1086 regress0/uf/issue2947.smt2
1087 regress0/uf/pred.smtv1.smt2
1088 regress0/uf/simple.01.cvc
1089 regress0/uf/simple.02.cvc
1090 regress0/uf/simple.03.cvc
1091 regress0/uf/simple.04.cvc
1092 regress0/uf20-03.cvc
1093 regress0/uflia/check01.smt2
1094 regress0/uflia/check02.smt2
1095 regress0/uflia/check03.smt2
1096 regress0/uflia/check04.smt2
1097 regress0/uflia/error0.delta01.smtv1.smt2
1098 regress0/uflia/error1.smtv1.smt2
1099 regress0/uflia/error30.smtv1.smt2
1100 regress0/uflia/stalmark_e7_27_e7_31.ec.minimized.smt2
1101 regress0/uflia/tiny.smt2
1102 regress0/uflia/xs-09-16-3-4-1-5.delta01.smtv1.smt2
1103 regress0/uflia/xs-09-16-3-4-1-5.delta02.smtv1.smt2
1104 regress0/uflia/xs-09-16-3-4-1-5.delta03.smtv1.smt2
1105 regress0/uflia/xs-09-16-3-4-1-5.delta04.smtv1.smt2
1106 regress0/uflra/bug293.cvc
1107 regress0/uflra/bug449.smtv1.smt2
1108 regress0/uflra/constants0.smtv1.smt2
1109 regress0/uflra/fuzz01.smtv1.smt2
1110 regress0/uflra/incorrect1.delta01.smtv1.smt2
1111 regress0/uflra/incorrect1.delta02.smtv1.smt2
1112 regress0/uflra/neq-deltacomp.smtv1.smt2
1113 regress0/uflra/pb_real_10_0100_10_10.smtv1.smt2
1114 regress0/uflra/pb_real_10_0100_10_11.smtv1.smt2
1115 regress0/uflra/pb_real_10_0100_10_15.smtv1.smt2
1116 regress0/uflra/pb_real_10_0100_10_16.smtv1.smt2
1117 regress0/uflra/pb_real_10_0100_10_19.smtv1.smt2
1118 regress0/uflra/pb_real_10_0200_10_22.smtv1.smt2
1119 regress0/uflra/pb_real_10_0200_10_26.smtv1.smt2
1120 regress0/uflra/pb_real_10_0200_10_29.smtv1.smt2
1121 regress0/uflra/simple.01.cvc
1122 regress0/uflra/simple.02.cvc
1123 regress0/uflra/simple.03.cvc
1124 regress0/uflra/simple.04.cvc
1125 regress0/unconstrained/4481.smt2
1126 regress0/unconstrained/4484.smt2
1127 regress0/unconstrained/4486.smt2
1128 regress0/unconstrained/arith.smt2
1129 regress0/unconstrained/arith3.smt2
1130 regress0/unconstrained/arith4.smt2
1131 regress0/unconstrained/arith5.smt2
1132 regress0/unconstrained/arith6.smt2
1133 regress0/unconstrained/array1.smt2
1134 regress0/unconstrained/bvbool.smt2
1135 regress0/unconstrained/bvbool2.smt2
1136 regress0/unconstrained/bvbool3.smt2
1137 regress0/unconstrained/bvcmp.smt2
1138 regress0/unconstrained/bvconcat2.smt2
1139 regress0/unconstrained/bvext.smt2
1140 regress0/unconstrained/bvite.smt2
1141 regress0/unconstrained/bvmul.smt2
1142 regress0/unconstrained/bvmul2.smt2
1143 regress0/unconstrained/bvmul3.smt2
1144 regress0/unconstrained/bvnot.smt2
1145 regress0/unconstrained/bvsle.smt2
1146 regress0/unconstrained/bvsle2.smt2
1147 regress0/unconstrained/bvsle3.smt2
1148 regress0/unconstrained/bvsle4.smt2
1149 regress0/unconstrained/bvsle5.smt2
1150 regress0/unconstrained/bvslt.smt2
1151 regress0/unconstrained/bvslt2.smt2
1152 regress0/unconstrained/bvslt3.smt2
1153 regress0/unconstrained/bvslt4.smt2
1154 regress0/unconstrained/bvslt5.smt2
1155 regress0/unconstrained/bvule.smt2
1156 regress0/unconstrained/bvule2.smt2
1157 regress0/unconstrained/bvule3.smt2
1158 regress0/unconstrained/bvule4.smt2
1159 regress0/unconstrained/bvule5.smt2
1160 regress0/unconstrained/bvult.smt2
1161 regress0/unconstrained/bvult2.smt2
1162 regress0/unconstrained/bvult3.smt2
1163 regress0/unconstrained/bvult4.smt2
1164 regress0/unconstrained/bvult5.smt2
1165 regress0/unconstrained/geq.smt2
1166 regress0/unconstrained/gt.smt2
1167 regress0/unconstrained/ite.smt2
1168 regress0/unconstrained/leq.smt2
1169 regress0/unconstrained/lt.smt2
1170 regress0/unconstrained/mult1.smt2
1171 regress0/unconstrained/uf1.smt2
1172 regress0/unconstrained/xor.smt2
1173 regress0/wiki.01.cvc
1174 regress0/wiki.02.cvc
1175 regress0/wiki.03.cvc
1176 regress0/wiki.04.cvc
1177 regress0/wiki.05.cvc
1178 regress0/wiki.06.cvc
1179 regress0/wiki.07.cvc
1180 regress0/wiki.08.cvc
1181 regress0/wiki.09.cvc
1182 regress0/wiki.10.cvc
1183 regress0/wiki.11.cvc
1184 regress0/wiki.12.cvc
1185 regress0/wiki.13.cvc
1186 regress0/wiki.14.cvc
1187 regress0/wiki.15.cvc
1188 regress0/wiki.16.cvc
1189 regress0/wiki.17.cvc
1190 regress0/wiki.18.cvc
1191 regress0/wiki.19.cvc
1192 regress0/wiki.20.cvc
1193 regress0/wiki.21.cvc
1196 #-----------------------------------------------------------------------------#
1197 # Regression level 1 tests
1200 regress1/arith/arith-int-004.cvc
1201 regress1/arith/arith-int-011.cvc
1202 regress1/arith/arith-int-012.cvc
1203 regress1/arith/arith-int-013.cvc
1204 regress1/arith/arith-int-022.cvc
1205 regress1/arith/arith-int-024.cvc
1206 regress1/arith/arith-int-047.cvc
1207 regress1/arith/arith-int-048.cvc
1208 regress1/arith/arith-int-050.cvc
1209 regress1/arith/arith-int-084.cvc
1210 regress1/arith/arith-int-085.cvc
1211 regress1/arith/arith-int-097.cvc
1212 regress1/arith/bug547.1.smt2
1213 regress1/arith/bug716.0.smt2
1214 regress1/arith/bug716.1.cvc
1215 regress1/arith/div.03.smt2
1216 regress1/arith/div.06.smt2
1217 regress1/arith/div.08.smt2
1218 regress1/arith/div.09.smt2
1219 regress1/arith/issue3952-rew-eq.smt2
1220 regress1/arith/issue789.smt2
1221 regress1/arith/miplib3.cvc
1222 regress1/arith/mod.02.smt2
1223 regress1/arith/mod.03.smt2
1224 regress1/arith/mult.02.smt2
1225 regress1/arith/pbrewrites-test.smt2
1226 regress1/arith/problem__003.smt2
1227 regress1/arrayinuf_error.smt2
1228 regress1/aufbv/bug580.smt2
1229 regress1/aufbv/fuzz10.smtv1.smt2
1230 regress1/auflia/bug330.smt2
1231 regress1/boolean-terms-kernel2.smt2
1232 regress1/boolean.cvc
1233 regress1/bug296.smt2
1235 regress1/bug507.smt2
1236 regress1/bug512.smt2
1237 regress1/bug516.smt2
1238 regress1/bug519.smt2
1239 regress1/bug520.smt2
1240 regress1/bug521.smt2
1241 regress1/bug543.smt2
1242 regress1/bug567.smt2
1243 regress1/bug593.smt2
1244 regress1/bug681.smt2
1245 regress1/bug694-Unapply1.scala-0.smt2
1246 regress1/bug800.smt2
1247 regress1/bv/bug787.smt2
1248 regress1/bv/bug_extract_mult_leading_bit.smt2
1249 regress1/bv/bv-int-collapse2-sat.smt2
1250 regress1/bv/bv-proof00.smtv1.smt2
1251 regress1/bv/bv2nat-ground.smt2
1252 regress1/bv/bv2nat-simp-range-sat.smt2
1253 regress1/bv/bv2nat-types.smt2
1254 regress1/bv/cmu-rdk-3.smt2
1255 regress1/bv/decision-weight00.smt2
1256 regress1/bv/divtest.smt2
1257 regress1/bv/fuzz34.smtv1.smt2
1258 regress1/bv/fuzz38.smtv1.smt2
1259 regress1/bv/issue3654.smt2
1260 regress1/bv/issue3776.smt2
1261 regress1/bv/test-bv-abstraction.smt2
1262 regress1/bv/unsound1.smt2
1263 regress1/bvdiv2.smt2
1264 regress1/constarr3.cvc
1265 regress1/constarr3.smt2
1266 regress1/datatypes/acyclicity-sr-ground096.smt2
1267 regress1/datatypes/dt-color-2.6.smt2
1268 regress1/datatypes/dt-param-card4-unsat.smt2
1269 regress1/datatypes/error.cvc
1270 regress1/datatypes/issue3266-small.smt2
1271 regress1/datatypes/issue-variant-dt-zero.smt2
1272 regress1/datatypes/manos-model.smt2
1273 regress1/decision/error3.smtv1.smt2
1274 regress1/decision/quant-Arrays_Q1-noinfer.smt2
1275 regress1/decision/quant-symmetric_unsat_7.smt2
1277 regress1/errorcrash.smt2
1278 regress1/fmf-fun-dbu.smt2
1279 regress1/fmf/ALG008-1.smt2
1280 regress1/fmf/Hoare-z3.931718.smtv1.smt2
1281 regress1/fmf/LeftistHeap.scala-8-ncm.smt2
1282 regress1/fmf/PUZ001+1.smt2
1283 regress1/fmf/agree466.smt2
1284 regress1/fmf/agree467.smt2
1285 regress1/fmf/alg202+1.smt2
1286 regress1/fmf/am-bad-model.cvc
1287 regress1/fmf/bound-int-alt.smt2
1288 regress1/fmf/bug0909.smt2
1289 regress1/fmf/bug651.smt2
1290 regress1/fmf/bug723-irrelevant-funs.smt2
1291 regress1/fmf/bug764.smt2
1292 regress1/fmf/cons-sets-bounds.smt2
1293 regress1/fmf/constr-ground-to.smt2
1294 regress1/fmf/datatypes-ufinite-nested.smt2
1295 regress1/fmf/datatypes-ufinite.smt2
1296 regress1/fmf/dt-proper-model.smt2
1297 regress1/fmf/fc-pigeonhole19.smt2
1298 regress1/fmf/fib-core.smt2
1299 regress1/fmf/fmf-bound-2dim.smt2
1300 regress1/fmf/fmf-bound-int.smt2
1301 regress1/fmf/fmf-fun-divisor-pp.smt2
1302 regress1/fmf/fmf-fun-no-elim-ext-arith.smt2
1303 regress1/fmf/fmf-fun-no-elim-ext-arith2.smt2
1304 regress1/fmf/fmf-strange-bounds.smt2
1305 regress1/fmf/forall_unit_data.smt2
1306 regress1/fmf/fore19-exp2-core.smt2
1307 regress1/fmf/german169.smt2
1308 regress1/fmf/german73.smt2
1309 regress1/fmf/issue2034-preinit.smt2
1310 regress1/fmf/issue3587.smt2
1311 regress1/fmf/issue3615.smt2
1312 regress1/fmf/issue3626.smt2
1313 regress1/fmf/issue3689.smt2
1314 regress1/fmf/issue4068-si-qf.smt2
1315 regress1/fmf/issue916-fmf-or.smt2
1316 regress1/fmf/jasmin-cdt-crash.smt2
1317 regress1/fmf/ko-bound-set.cvc
1318 regress1/fmf/loopy_coda.smt2
1319 regress1/fmf/lst-no-self-rev-exp.smt2
1320 regress1/fmf/memory_model-R_cpp-dd.cvc
1321 regress1/fmf/nlp042+1.smt2
1322 regress1/fmf/nun-0208-to.smt2
1323 regress1/fmf/pow2-bool.smt2
1324 regress1/fmf/radu-quant-set.smt2
1325 regress1/fmf/refcount24.cvc.smt2
1326 regress1/fmf/sc-crash-052316.smt2
1327 regress1/fmf/sort-inf-int-real.smt2
1328 regress1/fmf/sort-inf-int.smt2
1329 regress1/fmf/with-ind-104-core.smt2
1330 regress1/gensys_brn001.smt2
1331 regress1/ho/fta0328.lfho.p
1332 regress1/ho/issue3136-fconst-bool-bool.smt2
1333 regress1/ho/issue4065-no-rep.smt2
1334 regress1/ho/issue4092-sinf.smt2
1335 regress1/ho/issue4134-sinf.smt2
1336 regress1/ho/nested_lambdas-AGT034^2.smt2
1337 regress1/ho/nested_lambdas-sat-SYO056^1-delta.smt2
1338 regress1/ho/NUM638^1.smt2
1339 regress1/ho/NUM925^1.p
1340 regress1/ho/soundness_fmf_SYO362^5-delta.p
1341 regress1/ho/store-ax-min.p
1342 regress1/ho/SYO056^1.p
1345 regress1/issue3970-nl-ext-purify.smt2
1346 regress1/issue3990-sort-inference.smt2
1347 regress1/issue4273-ext-rew-cache.smt2
1348 regress1/lemmas/clocksynchro_5clocks.main_invar.base.smtv1.smt2
1349 regress1/lemmas/pursuit-safety-8.smtv1.smt2
1350 regress1/lemmas/simple_startup_9nodes.abstract.base.smtv1.smt2
1351 regress1/model-blocker-simple.smt2
1352 regress1/model-blocker-values.smt2
1353 regress1/nl/approx-sqrt-unsat.smt2
1354 regress1/nl/approx-sqrt.smt2
1355 regress1/nl/arctan2-expdef.smt2
1356 regress1/nl/arrowsmith-050317.smt2
1357 regress1/nl/bad-050217.smt2
1358 regress1/nl/bug698.smt2
1359 regress1/nl/coeff-unsat-base.smt2
1360 regress1/nl/coeff-unsat.smt2
1361 regress1/nl/combine.smt2
1362 regress1/nl/cos-bound.smt2
1363 regress1/nl/cos1-tc.smt2
1364 regress1/nl/disj-eval.smt2
1365 regress1/nl/dist-big.smt2
1366 regress1/nl/div-mod-partial.smt2
1367 regress1/nl/dumortier_llibre_artes_ex_5_13.transcendental.k2.smt2
1368 regress1/nl/exp-4.5-lt.smt2
1369 regress1/nl/exp-approx.smt2
1370 regress1/nl/exp-soundness-bound.smt2
1371 regress1/nl/exp1-lb.smt2
1372 regress1/nl/exp_monotone.smt2
1373 regress1/nl/factor_agg_s.smt2
1374 regress1/nl/issue3300-approx-sqrt-witness.smt2
1375 regress1/nl/issue3441.smt2
1376 regress1/nl/issue3617.smt2
1377 regress1/nl/issue3647.smt2
1378 regress1/nl/issue3656.smt2
1379 regress1/nl/issue3803-nl-check-model.smt2
1380 regress1/nl/issue3955-ee-double-notify.smt2
1381 regress1/nl/metitarski-1025.smt2
1382 regress1/nl/metitarski-3-4.smt2
1383 regress1/nl/metitarski_3_4_2e.smt2
1384 regress1/nl/mirko-050417.smt2
1385 regress1/nl/nl-eq-infer.smt2
1386 regress1/nl/nl-help-unsat-quant.smt2
1387 regress1/nl/nl-unk-quant.smt2
1388 regress1/nl/nl_uf_lalt.smt2
1389 regress1/nl/ones.smt2
1390 regress1/nl/pinto-model-core-ni.smt2
1391 regress1/nl/poly-1025.smt2
1392 regress1/nl/quant-nl.smt2
1393 regress1/nl/red-exp.smt2
1394 regress1/nl/rewriting-sums.smt2
1395 regress1/nl/shifting.smt2
1396 regress1/nl/shifting2.smt2
1397 regress1/nl/simple-mono-unsat.smt2
1398 regress1/nl/simple-mono.smt2
1399 regress1/nl/sin-compare-across-phase.smt2
1400 regress1/nl/sin-compare.smt2
1401 regress1/nl/sin-init-tangents.smt2
1402 regress1/nl/sin-sign.smt2
1403 regress1/nl/sin-sym2.smt2
1404 regress1/nl/sin1-deq-sat.smt2
1405 regress1/nl/sin1-lb.smt2
1406 regress1/nl/sin1-sat.smt2
1407 regress1/nl/sin1-ub.smt2
1408 regress1/nl/sin2-lb.smt2
1409 regress1/nl/sin2-ub.smt2
1410 regress1/nl/solve-eq-small-qf-nra.smt2
1411 regress1/nl/sqrt-problem-1.smt2
1412 regress1/nl/sugar-ident-2.smt2
1413 regress1/nl/sugar-ident-3.smt2
1414 regress1/nl/sugar-ident.smt2
1415 regress1/nl/tan-rewrite2.smt2
1416 regress1/nl/zero-subset.smt2
1417 regress1/non-fatal-errors.smt2
1418 regress1/parsing_ringer.cvc
1419 regress1/proof00.smt2
1420 regress1/push-pop/arith_lra_01.smt2
1421 regress1/push-pop/arith_lra_02.smt2
1422 regress1/push-pop/bug-fmf-fun-skolem.smt2
1423 regress1/push-pop/bug216.smt2
1424 regress1/push-pop/fuzz_1.smt2
1425 regress1/push-pop/fuzz_10.smt2
1426 regress1/push-pop/fuzz_11.smt2
1427 regress1/push-pop/fuzz_15.smt2
1428 regress1/push-pop/fuzz_16.smt2
1429 regress1/push-pop/fuzz_19.smt2
1430 regress1/push-pop/fuzz_1_to_52_merged.smt2
1431 regress1/push-pop/fuzz_20.smt2
1432 regress1/push-pop/fuzz_23.smt2
1433 regress1/push-pop/fuzz_24.smt2
1434 regress1/push-pop/fuzz_25.smt2
1435 regress1/push-pop/fuzz_26.smt2
1436 regress1/push-pop/fuzz_28.smt2
1437 regress1/push-pop/fuzz_29.smt2
1438 regress1/push-pop/fuzz_30.smt2
1439 regress1/push-pop/fuzz_32.smt2
1440 regress1/push-pop/fuzz_34.smt2
1441 regress1/push-pop/fuzz_35.smt2
1442 regress1/push-pop/fuzz_37.smt2
1443 regress1/push-pop/fuzz_39.smt2
1444 regress1/push-pop/fuzz_3_1.smt2
1445 regress1/push-pop/fuzz_3_10.smt2
1446 regress1/push-pop/fuzz_3_11.smt2
1447 regress1/push-pop/fuzz_3_12.smt2
1448 regress1/push-pop/fuzz_3_13.smt2
1449 regress1/push-pop/fuzz_3_14.smt2
1450 regress1/push-pop/fuzz_3_15.smt2
1451 regress1/push-pop/fuzz_3_2.smt2
1452 regress1/push-pop/fuzz_3_3.smt2
1453 regress1/push-pop/fuzz_3_4.smt2
1454 regress1/push-pop/fuzz_3_5.smt2
1455 regress1/push-pop/fuzz_3_6.smt2
1456 regress1/push-pop/fuzz_3_7.smt2
1457 regress1/push-pop/fuzz_3_8.smt2
1458 regress1/push-pop/fuzz_3_9.smt2
1459 regress1/push-pop/fuzz_4.smt2
1460 regress1/push-pop/fuzz_40.smt2
1461 regress1/push-pop/fuzz_41.smt2
1462 regress1/push-pop/fuzz_42.smt2
1463 regress1/push-pop/fuzz_43.smt2
1464 regress1/push-pop/fuzz_44.smt2
1465 regress1/push-pop/fuzz_45.smt2
1466 regress1/push-pop/fuzz_5.smt2
1467 regress1/push-pop/fuzz_51.smt2
1468 regress1/push-pop/fuzz_52.smt2
1469 regress1/push-pop/fuzz_5_1.smt2
1470 regress1/push-pop/fuzz_5_2.smt2
1471 regress1/push-pop/fuzz_5_3.smt2
1472 regress1/push-pop/fuzz_5_4.smt2
1473 regress1/push-pop/fuzz_5_5.smt2
1474 regress1/push-pop/fuzz_5_6.smt2
1475 regress1/push-pop/fuzz_6.smt2
1476 regress1/push-pop/fuzz_7.smt2
1477 regress1/push-pop/fuzz_8.smt2
1478 regress1/push-pop/fuzz_9.smt2
1479 regress1/push-pop/model-unsound-ania.smt2
1480 regress1/push-pop/quant-fun-proc-unmacro.smt2
1481 regress1/push-pop/quant-fun-proc.smt2
1482 regress1/quantifiers/006-cbqi-ite.smt2
1483 regress1/quantifiers/015-psyco-pp.smt2
1484 regress1/quantifiers/AdditiveMethods_OwnedResults.Mz.smt2
1485 regress1/quantifiers/Arrays_Q1-noinfer.smt2
1486 regress1/quantifiers/NUM878.smt2
1487 regress1/quantifiers/RND-small.smt2
1488 regress1/quantifiers/RNDPRE_4_1-dd-nqe.smt2
1489 regress1/quantifiers/RND_4_1-existing-inst.smt2
1490 regress1/quantifiers/RND_4_16.smt2
1491 regress1/quantifiers/anti-sk-simp.smt2
1492 regress1/quantifiers/ari118-bv-2occ-x.smt2
1493 regress1/quantifiers/arith-rec-fun.smt2
1494 regress1/quantifiers/arith-snorm.smt2
1495 regress1/quantifiers/array-unsat-simp3.smt2
1496 regress1/quantifiers/bi-artm-s.smt2
1497 regress1/quantifiers/bignum_quant.smt2
1498 regress1/quantifiers/bug802.smt2
1499 regress1/quantifiers/bug822.smt2
1500 regress1/quantifiers/bug_743.smt2
1501 regress1/quantifiers/burns13.smt2
1502 regress1/quantifiers/burns4.smt2
1503 regress1/quantifiers/cbqi-sdlx-fixpoint-3-dd.smt2
1504 regress1/quantifiers/cdt-0208-to.smt2
1505 regress1/quantifiers/const.cvc
1506 regress1/quantifiers/constfunc.cvc
1507 regress1/quantifiers/dump-inst-i.smt2
1508 regress1/quantifiers/dump-inst-proof.smt2
1509 regress1/quantifiers/dump-inst.smt2
1510 regress1/quantifiers/ext-ex-deq-trigger.smt2
1511 regress1/quantifiers/extract-nproc.smt2
1512 regress1/quantifiers/f993-loss-easy.smt2
1513 regress1/quantifiers/florian-case-ax.smt2
1514 regress1/quantifiers/fp-cegqi-unsat.smt2
1515 regress1/quantifiers/gauss_init_0030.fof.smt2
1516 regress1/quantifiers/horn-simple.smt2
1517 regress1/quantifiers/infer-arith-trigger-eq.smt2
1518 regress1/quantifiers/inst-max-level-segf.smt2
1519 regress1/quantifiers/inst-prop-simp.smt2
1520 regress1/quantifiers/intersection-example-onelane.proof-node22337.smt2
1521 regress1/quantifiers/is-even.smt2
1522 regress1/quantifiers/isaplanner-goal20.smt2
1523 regress1/quantifiers/issue2970-string-var-elim.smt2
1524 regress1/quantifiers/issue3250-syg-inf-q.smt2
1525 regress1/quantifiers/issue3316.smt2
1526 regress1/quantifiers/issue3317.smt2
1527 regress1/quantifiers/issue3481.smt2
1528 regress1/quantifiers/issue3481-unsat1.smt2
1529 regress1/quantifiers/issue3537.smt2
1530 regress1/quantifiers/issue3628.smt2
1531 regress1/quantifiers/issue3664.smt2
1532 regress1/quantifiers/issue3724-quant.smt2
1533 regress1/quantifiers/issue3765.smt2
1534 regress1/quantifiers/issue3765-quant-dd.smt2
1535 regress1/quantifiers/issue4021-ind-opts.smt2
1536 regress1/quantifiers/issue4062-cegqi-aux.smt2
1537 regress1/quantifiers/issue4243-prereg-inc.smt2
1538 regress1/quantifiers/issue4290-cegqi-r.smt2
1539 regress1/quantifiers/issue993.smt2
1540 regress1/quantifiers/javafe.ast.StmtVec.009.smt2
1541 regress1/quantifiers/lra-vts-inf.smt2
1542 regress1/quantifiers/mix-coeff.smt2
1543 regress1/quantifiers/mutualrec2.cvc
1544 regress1/quantifiers/nested9_true-unreach-call.i_575.smt2
1545 regress1/quantifiers/nl-pow-trick.smt2
1546 regress1/quantifiers/nra-interleave-inst.smt2
1547 regress1/quantifiers/opisavailable-12.smt2
1548 regress1/quantifiers/parametric-lists.smt2
1549 regress1/quantifiers/psyco-001-bv.smt2
1550 regress1/quantifiers/psyco-107-bv.smt2
1551 regress1/quantifiers/psyco-196.smt2
1552 regress1/quantifiers/qbv-disequality3.smt2
1553 regress1/quantifiers/qbv-simple-2vars-vo.smt2
1554 regress1/quantifiers/qbv-subcall.smt2
1555 regress1/quantifiers/qbv-test-invert-bvashr-0.smt2
1556 regress1/quantifiers/qbv-test-invert-bvashr-1.smt2
1557 regress1/quantifiers/qbv-test-invert-bvcomp.smt2
1558 regress1/quantifiers/qbv-test-invert-bvlshr-1.smt2
1559 regress1/quantifiers/qbv-test-invert-bvmul-neq.smt2
1560 regress1/quantifiers/qbv-test-invert-bvmul.smt2
1561 regress1/quantifiers/qbv-test-invert-bvudiv-0-neq.smt2
1562 regress1/quantifiers/qbv-test-invert-bvudiv-0.smt2
1563 regress1/quantifiers/qbv-test-invert-bvudiv-1-neq.smt2
1564 regress1/quantifiers/qbv-test-invert-bvudiv-1.smt2
1565 regress1/quantifiers/qbv-test-invert-bvurem-1-neq.smt2
1566 regress1/quantifiers/qbv-test-invert-bvurem-1.smt2
1567 regress1/quantifiers/qbv-test-urem-rewrite.smt2
1568 regress1/quantifiers/qcft-javafe.filespace.TreeWalker.006.smt2
1569 regress1/quantifiers/qcft-smtlib3dbc51.smt2
1570 regress1/quantifiers/qe-partial.smt2
1571 regress1/quantifiers/qe.smt2
1572 regress1/quantifiers/quant-wf-int-ind.smt2
1573 regress1/quantifiers/quaternion_ds1_symm_0428.fof.smt2
1574 regress1/quantifiers/recfact.cvc
1575 regress1/quantifiers/rel-trigger-unusable.smt2
1576 regress1/quantifiers/repair-const-nterm.smt2
1577 regress1/quantifiers/rew-to-0211-dd.smt2
1578 regress1/quantifiers/ricart-agrawala6.smt2
1579 regress1/quantifiers/set-choice-koikonomou.cvc
1580 regress1/quantifiers/set8.smt2
1581 regress1/quantifiers/seu169+1.smt2
1582 regress1/quantifiers/small-pipeline-fixpoint-3.smt2
1583 regress1/quantifiers/smtcomp-qbv-053118.smt2
1584 regress1/quantifiers/smtlib384a03.smt2
1585 regress1/quantifiers/smtlib46f14a.smt2
1586 regress1/quantifiers/smtlibe99bbe.smt2
1587 regress1/quantifiers/smtlibf957ea.smt2
1588 regress1/quantifiers/stream-x2014-09-18-unsat.smt2
1589 regress1/quantifiers/sygus-infer-nested.smt2
1590 regress1/quantifiers/symmetric_unsat_7.smt2
1591 regress1/quantifiers/var-eq-trigger.smt2
1592 regress1/quantifiers/var-eq-trigger-simple.smt2
1593 regress1/quantifiers/z3.620661-no-fv-trigger.smt2
1594 regress1/rels/addr_book_1.cvc
1595 regress1/rels/addr_book_1_1.cvc
1596 regress1/rels/bv1-unit.cvc
1597 regress1/rels/bv1-unitb.cvc
1598 regress1/rels/bv1.cvc
1599 regress1/rels/bv1p-sat.cvc
1600 regress1/rels/bv1p.cvc
1601 regress1/rels/bv2.cvc
1602 regress1/rels/iden_1_1.cvc
1603 regress1/rels/join-eq-structure-and.cvc
1604 regress1/rels/join-eq-structure.cvc
1605 regress1/rels/joinImg_0_1.cvc
1606 regress1/rels/joinImg_0_2.cvc
1607 regress1/rels/joinImg_1.cvc
1608 regress1/rels/joinImg_1_1.cvc
1609 regress1/rels/joinImg_2.cvc
1610 regress1/rels/joinImg_2_1.cvc
1611 regress1/rels/prod-mod-eq.cvc
1612 regress1/rels/prod-mod-eq2.cvc
1613 regress1/rels/rel_complex_3.cvc
1614 regress1/rels/rel_complex_4.cvc
1615 regress1/rels/rel_complex_5.cvc
1616 regress1/rels/rel_mix_0_1.cvc
1617 regress1/rels/rel_pressure_0.cvc
1618 regress1/rels/rel_tc_10_1.cvc
1619 regress1/rels/rel_tc_4.cvc
1620 regress1/rels/rel_tc_4_1.cvc
1621 regress1/rels/rel_tc_5_1.cvc
1622 regress1/rels/rel_tc_6.cvc
1623 regress1/rels/rel_tc_9_1.cvc
1624 regress1/rels/rel_tp_2.cvc
1625 regress1/rels/rel_tp_join_2_1.cvc
1626 regress1/rels/set-strat.cvc
1627 regress1/rels/strat.cvc
1628 regress1/rr-verify/bool-crci.sy
1629 regress1/rr-verify/bv-term-32.sy
1630 regress1/rr-verify/bv-term.sy
1631 regress1/rr-verify/fp-arith.sy
1632 regress1/rr-verify/fp-bool.sy
1633 regress1/rr-verify/regex.sy
1634 regress1/rr-verify/string-term.sy
1635 regress1/sep/chain-int.smt2
1636 regress1/sep/crash1220.smt2
1637 regress1/sep/dispose-list-4-init.smt2
1638 regress1/sep/emp2-quant-unsat.smt2
1639 regress1/sep/finite-witness-sat.smt2
1640 regress1/sep/fmf-nemp-2.smt2
1641 regress1/sep/loop-1220.smt2
1642 regress1/sep/pto-04.smt2
1643 regress1/sep/quant_wand.smt2
1644 regress1/sep/sep-02.smt2
1645 regress1/sep/sep-03.smt2
1646 regress1/sep/sep-find2.smt2
1647 regress1/sep/sep-fmf-priority.smt2
1648 regress1/sep/sep-neg-1refine.smt2
1649 regress1/sep/sep-neg-nstrict.smt2
1650 regress1/sep/sep-neg-nstrict2.smt2
1651 regress1/sep/sep-neg-simple.smt2
1652 regress1/sep/sep-neg-swap.smt2
1653 regress1/sep/sep-nterm-again.smt2
1654 regress1/sep/sep-nterm-val-model.smt2
1655 regress1/sep/sep-simp-unc.smt2
1656 regress1/sep/simple-neg-sat.smt2
1657 regress1/sep/sl-standard.smt2
1658 regress1/sep/split-find-unsat-w-emp.smt2
1659 regress1/sep/split-find-unsat.smt2
1660 regress1/sep/wand-0526-sat.smt2
1661 regress1/sep/wand-false.smt2
1662 regress1/sep/wand-nterm-simp.smt2
1663 regress1/sep/wand-nterm-simp2.smt2
1664 regress1/sep/wand-simp-sat.smt2
1665 regress1/sep/wand-simp-sat2.smt2
1666 regress1/sep/wand-simp-unsat.smt2
1667 regress1/sets/choose.cvc
1668 regress1/sets/choose1.smt2
1669 regress1/sets/choose2.smt2
1670 regress1/sets/choose3.smt2
1671 regress1/sets/choose4.smt2
1672 regress1/sets/ListElem.hs.fqout.cvc4.38.smt2
1673 regress1/sets/ListElts.hs.fqout.cvc4.317.smt2
1674 regress1/sets/TalkingAboutSets.hs.fqout.cvc4.3577.smt2
1675 regress1/sets/UniqueZipper.hs.1030minimized.cvc4.smt2
1676 regress1/sets/UniqueZipper.hs.1030minimized2.cvc4.smt2
1677 regress1/sets/UniqueZipper.hs.fqout.cvc4.10.smt2
1678 regress1/sets/UniqueZipper.hs.fqout.cvc4.1832.smt2
1679 regress1/sets/arjun-set-univ.cvc
1680 regress1/sets/card-3.smt2
1681 regress1/sets/card-4.smt2
1682 regress1/sets/card-5.smt2
1683 regress1/sets/card-6.smt2
1684 regress1/sets/card-7.smt2
1685 regress1/sets/card-vc6-minimized.smt2
1686 regress1/sets/comp-intersect.smt2
1687 regress1/sets/comp-odd.smt2
1688 regress1/sets/comp-positive.smt2
1689 regress1/sets/comp-pos-member.smt2
1690 regress1/sets/copy_check_heap_access_33_4.smt2
1691 regress1/sets/deepmeas0.hs.fqout.cvc4.41.smt2
1692 regress1/sets/finite-type/bug3663.smt2
1693 regress1/sets/finite-type/sets-card-arrcolor.smt2
1694 regress1/sets/finite-type/sets-card-arrunit.smt2
1695 regress1/sets/finite-type/sets-card-bool-1.smt2
1696 regress1/sets/finite-type/sets-card-bool-2.smt2
1697 regress1/sets/finite-type/sets-card-bool-3.smt2
1698 regress1/sets/finite-type/sets-card-bool-4.smt2
1699 regress1/sets/finite-type/sets-card-bool-rec.smt2
1700 regress1/sets/finite-type/sets-card-bv-1.smt2
1701 regress1/sets/finite-type/sets-card-bv-2.smt2
1702 regress1/sets/finite-type/sets-card-bv-3.smt2
1703 regress1/sets/finite-type/sets-card-bv-4.smt2
1704 regress1/sets/finite-type/sets-card-color.smt2
1705 regress1/sets/finite-type/sets-card-color-sat.smt2
1706 regress1/sets/finite-type/sets-card-datatype-1.smt2
1707 regress1/sets/finite-type/sets-card-datatype-2.smt2
1708 regress1/sets/finite-type/sets-card-neg-mem-union-1.smt2
1709 regress1/sets/fuzz14418.smt2
1710 regress1/sets/fuzz15201.smt2
1711 regress1/sets/fuzz31811.smt2
1712 regress1/sets/infinite-type/sets-card-array-int-1.smt2
1713 regress1/sets/infinite-type/sets-card-array-int-2.smt2
1714 regress1/sets/infinite-type/sets-card-int-1.smt2
1715 regress1/sets/infinite-type/sets-card-int-2.smt2
1716 regress1/sets/insert_invariant_37_2.smt2
1717 regress1/sets/issue2568.smt2
1718 regress1/sets/issue2904.smt2
1719 regress1/sets/issue4391-card-lasso.smt2
1720 regress1/sets/lemmabug-ListElts317minimized.smt2
1721 regress1/sets/remove_check_free_31_6.smt2
1722 regress1/sets/sets-disequal.smt2
1723 regress1/sets/sets-tuple-poly.cvc
1724 regress1/sets/set-comp-sat.smt2
1725 regress1/sets/sharingbug.smt2
1726 regress1/sets/univ-set-uf-elim.smt2
1727 regress1/simplification_bug4.smt2
1728 regress1/sqrt2-sort-inf-unk.smt2
1729 regress1/strings/artemis-0512-nonterm.smt2
1730 regress1/strings/at001.smt2
1731 regress1/strings/bug615.smt2
1732 regress1/strings/bug682.smt2
1733 regress1/strings/bug686dd.smt2
1734 regress1/strings/bug768.smt2
1735 regress1/strings/bug799-min.smt2
1736 regress1/strings/chapman150408.smt2
1737 regress1/strings/cmu-2db2-extf-reg.smt2
1738 regress1/strings/cmu-5042-0707-2.smt2
1739 regress1/strings/cmu-inc-nlpp-071516.smt2
1740 regress1/strings/cmu-substr-rw.smt2
1741 regress1/strings/code-sequence.smt2
1742 regress1/strings/complement-test.smt2
1743 regress1/strings/crash-1019.smt2
1744 regress1/strings/csp-prefix-exp-bug.smt2
1745 regress1/strings/double-replace.smt2
1746 regress1/strings/fmf001.smt2
1747 regress1/strings/fmf002.smt2
1748 regress1/strings/gm-inc-071516-2.smt2
1749 regress1/strings/goodAI.smt2
1750 regress1/strings/idof-handg.smt2
1751 regress1/strings/idof-nconst-index.smt2
1752 regress1/strings/idof-neg-index.smt2
1753 regress1/strings/idof-triv.smt2
1754 regress1/strings/ilc-l-nt.smt2
1755 regress1/strings/issue1105.smt2
1756 regress1/strings/issue1684-regex.smt2
1757 regress1/strings/issue2060.smt2
1758 regress1/strings/issue2429-code.smt2
1759 regress1/strings/issue2981.smt2
1760 regress1/strings/issue2982.smt2
1761 regress1/strings/issue3090.smt2
1762 regress1/strings/issue3217.smt2
1763 regress1/strings/issue3272.smt2
1764 regress1/strings/issue3357.smt2
1765 regress1/strings/issue3657-unexpectedUnsatCVC4.smt2
1766 regress1/strings/issue4379.smt2
1767 regress1/strings/kaluza-fl.smt2
1768 regress1/strings/loop002.smt2
1769 regress1/strings/loop003.smt2
1770 regress1/strings/loop004.smt2
1771 regress1/strings/loop005.smt2
1772 regress1/strings/loop006.smt2
1773 regress1/strings/loop007.smt2
1774 regress1/strings/loop008.smt2
1775 regress1/strings/loop009.smt2
1776 regress1/strings/nf-ff-contains-abs.smt2
1777 regress1/strings/no-lazy-pp-quant.smt2
1778 regress1/strings/non_termination_regular_expression4.smt2
1779 regress1/strings/norn-13.smt2
1780 regress1/strings/norn-360.smt2
1781 regress1/strings/norn-ab.smt2
1782 regress1/strings/norn-nel-bug-052116.smt2
1783 regress1/strings/norn-simp-rew-sat.smt2
1784 regress1/strings/nt6-dd.smt2
1785 regress1/strings/nterm-re-inter-sigma.smt2
1786 regress1/strings/pierre150331.smt2
1787 regress1/strings/policy_variable.smt2
1788 regress1/strings/pre_ctn_no_skolem_share.smt2
1789 regress1/strings/query4674.smt2
1790 regress1/strings/query8485.smt2
1791 regress1/strings/re-all-char-hard.smt2
1792 regress1/strings/re-agg-total1.smt2
1793 regress1/strings/re-agg-total2.smt2
1794 regress1/strings/re-elim-exact.smt2
1795 regress1/strings/re-mod-eq.smt2
1796 regress1/strings/re-neg-concat-reduct.smt2
1797 regress1/strings/re-neg-unfold-rev-a.smt2
1798 regress1/strings/re-unsound-080718.smt2
1799 regress1/strings/regexp001.smt2
1800 regress1/strings/regexp002.smt2
1801 regress1/strings/regexp003.smt2
1802 regress1/strings/regexp-strat-fix.smt2
1803 regress1/strings/reloop.smt2
1804 regress1/strings/repl-empty-sem.smt2
1805 regress1/strings/repl-soundness-sem.smt2
1806 regress1/strings/replaceall-len.smt2
1807 regress1/strings/replaceall-replace.smt2
1808 regress1/strings/rev-conv1.smt2
1809 regress1/strings/rev-ex1.smt2
1810 regress1/strings/rev-ex2.smt2
1811 regress1/strings/rev-ex3.smt2
1812 regress1/strings/rev-ex4.smt2
1813 regress1/strings/rev-ex5.smt2
1814 regress1/strings/rew-020618.smt2
1815 regress1/strings/rew-check1.smt2
1816 regress1/strings/simple-re-consume.smt2
1817 regress1/strings/stoi-400million.smt2
1818 regress1/strings/stoi-solve.smt2
1819 regress1/strings/str-code-sat.smt2
1820 regress1/strings/str-code-unsat-2.smt2
1821 regress1/strings/str-code-unsat-3.smt2
1822 regress1/strings/str-code-unsat.smt2
1823 regress1/strings/str-rev-simple-s.smt2
1824 regress1/strings/str001.smt2
1825 regress1/strings/str002.smt2
1826 regress1/strings/str006.smt2
1827 regress1/strings/str007.smt2
1828 regress1/strings/string-unsound-sem.smt2
1829 regress1/strings/strings-index-empty.smt2
1830 regress1/strings/strings-leq-trans-unsat.smt2
1831 regress1/strings/strings-lt-len5.smt2
1832 regress1/strings/strings-lt-simple.smt2
1833 regress1/strings/strip-endpt-sound.smt2
1834 regress1/strings/substr001.smt2
1835 regress1/strings/tolower-find.smt2
1836 regress1/strings/timeout-no-resp.smt2
1837 regress1/strings/type002.smt2
1838 regress1/strings/type003.smt2
1839 regress1/strings/username_checker_min.smt2
1840 regress1/sygus-abduct-ex1-grammar.smt2
1841 regress1/sygus-abduct-test.smt2
1842 regress1/sygus-abduct-test-ccore.smt2
1843 regress1/sygus-abduct-test-user.smt2
1844 regress1/sygus/VC22_a.sy
1845 regress1/sygus/abd-simple-conj-4.smt2
1846 regress1/sygus/abduction_1255.corecstrs.readable.smt2
1847 regress1/sygus/abduction_streq.readable.smt2
1848 regress1/sygus/abv.sy
1849 regress1/sygus/array_search_5-Q-easy.sy
1850 regress1/sygus/bvudiv-by-2.sy
1851 regress1/sygus/cegar1.sy
1852 regress1/sygus/cegis-unif-inv-eq-fair.sy
1853 regress1/sygus/cegisunif-depth1.sy
1854 regress1/sygus/cggmp.sy
1855 regress1/sygus/clock-inc-tuple.sy
1856 regress1/sygus/coeff-solve-inv.sy
1857 regress1/sygus/commutative-stream.sy
1858 regress1/sygus/commutative.sy
1859 regress1/sygus/concat_extract_example.sy
1860 regress1/sygus/constant-bool-si-all.sy
1861 regress1/sygus/constant-dec-tree-bug.sy
1862 regress1/sygus/constant-ite-bv.sy
1863 regress1/sygus/constant.sy
1864 regress1/sygus/crci-ssb-unk.sy
1865 regress1/sygus/crcy-si.sy
1866 regress1/sygus/cube-nia.sy
1867 regress1/sygus/double.sy
1868 regress1/sygus/dt-test-ns.sy
1869 regress1/sygus/dup-op.sy
1870 regress1/sygus/error1-dt.sy
1871 regress1/sygus/extract.sy
1872 regress1/sygus/fast-enum-backtrack.sy
1873 regress1/sygus/fg_polynomial3.sy
1874 regress1/sygus/find_sc_bvult_bvnot.sy
1875 regress1/sygus/hd-01-d1-prog.sy
1876 regress1/sygus/hd-19-d1-prog-dup-op.sy
1877 regress1/sygus/hd-sdiv.sy
1878 regress1/sygus/ho-sygus.sy
1879 regress1/sygus/icfp_14.12-flip-args.sy
1880 regress1/sygus/icfp_14.12.sy
1881 regress1/sygus/icfp_14_12_diff_types.sy
1882 regress1/sygus/icfp_28_10.sy
1883 regress1/sygus/icfp_easy-ite.sy
1884 regress1/sygus/int-any-const.sy
1885 regress1/sygus/inv-example.sy
1886 regress1/sygus/inv-missed-sol-true.sy
1887 regress1/sygus/inv-unused.sy
1888 regress1/sygus/issue2914.sy
1889 regress1/sygus/issue2935.sy
1890 regress1/sygus/issue3199.smt2
1891 regress1/sygus/issue3200.smt2
1892 regress1/sygus/issue3201.smt2
1893 regress1/sygus/issue3205.smt2
1894 regress1/sygus/issue3247.smt2
1895 regress1/sygus/issue3320-quant.sy
1896 regress1/sygus/issue3461.sy
1897 regress1/sygus/issue3498.smt2
1898 regress1/sygus/issue3514.smt2
1899 regress1/sygus/issue3507.smt2
1900 regress1/sygus/issue3633.smt2
1901 regress1/sygus/issue3634.smt2
1902 regress1/sygus/issue3635.smt2
1903 regress1/sygus/issue3644.smt2
1904 regress1/sygus/issue3648.smt2
1905 regress1/sygus/issue3649.sy
1906 regress1/sygus/issue3802-default-consts.sy
1907 regress1/sygus/issue3839-cond-rewrite.smt2
1908 regress1/sygus/issue3944-div-rewrite.smt2
1909 regress1/sygus/issue3947-agg-miniscope.smt2
1910 regress1/sygus/issue3995-fmf-var-op.smt2
1911 regress1/sygus/issue4009-qep.smt2
1912 regress1/sygus/issue4025-no-rlv-cond.smt2
1913 regress1/sygus/issue4083-var-shadow.smt2
1914 regress1/sygus/large-const-simp.sy
1915 regress1/sygus/let-bug-simp.sy
1916 regress1/sygus/list-head-x.sy
1917 regress1/sygus/list_recursor.sy
1918 regress1/sygus/logiccell_help.sy
1919 regress1/sygus/max.sy
1920 regress1/sygus/max2-bv.sy
1921 regress1/sygus/multi-fun-polynomial2.sy
1922 regress1/sygus/nflat-fwd-3.sy
1923 regress1/sygus/nflat-fwd.sy
1924 regress1/sygus/nia-max-square-ns.sy
1925 regress1/sygus/node-discrete.sy
1926 regress1/sygus/no-flat-simp.sy
1927 regress1/sygus/no-mention.sy
1928 regress1/sygus/once_2.sy
1929 regress1/sygus/only-const-grammar.sy
1930 regress1/sygus/parity-si-rcons.sy
1931 regress1/sygus/pbe_multi.sy
1932 regress1/sygus/phone-1-long.sy
1933 regress1/sygus/planning-unif.sy
1934 regress1/sygus/process-10-vars.sy
1935 regress1/sygus/pLTL_5_trace.sy
1936 regress1/sygus/qe.sy
1937 regress1/sygus/qf_abv.smt2
1938 regress1/sygus/real-any-const.sy
1939 regress1/sygus/real-grammar.sy
1940 regress1/sygus/rec-fun-swap.sy
1941 regress1/sygus/rec-fun-sygus.sy
1942 regress1/sygus/rec-fun-while-1.sy
1943 regress1/sygus/rec-fun-while-2.sy
1944 regress1/sygus/rec-fun-while-infinite.sy
1945 regress1/sygus/re-concat.sy
1946 regress1/sygus/repair-const-rl.sy
1947 regress1/sygus/sets-pred-test.sy
1948 regress1/sygus/simple-regexp.sy
1949 regress1/sygus/stopwatch-bt.sy
1950 regress1/sygus/strings-any-term1.sy
1951 regress1/sygus/strings-no-syntax.sy
1952 regress1/sygus/strings-concat-3-args.sy
1953 regress1/sygus/strings-double-rec.sy
1954 regress1/sygus/strings-small.sy
1955 regress1/sygus/strings-template-infer-unused.sy
1956 regress1/sygus/strings-template-infer.sy
1957 regress1/sygus/strings-trivial-simp.sy
1958 regress1/sygus/strings-trivial-two-type.sy
1959 regress1/sygus/strings-trivial.sy
1960 regress1/sygus/sygus-dt.sy
1961 regress1/sygus/sygus-lambda-fv.sy
1962 regress1/sygus/sygus-uf-ex.sy
1963 regress1/sygus/t8.sy
1964 regress1/sygus/temp_input_to_synth_ic-error-121418.sy
1965 regress1/sygus/tester.sy
1966 regress1/sygus/tl-type-0.sy
1967 regress1/sygus/tl-type-4x.sy
1968 regress1/sygus/tl-type.sy
1969 regress1/sygus/triv-type-mismatch-si.sy
1970 regress1/sygus/trivial-stream.sy
1971 regress1/sygus/twolets1.sy
1972 regress1/sygus/twolets2-orig.sy
1973 regress1/sygus/uf-abduct.smt2
1974 regress1/sygus/unbdd_inv_gen_ex7.sy
1975 regress1/sygus/unbdd_inv_gen_winf1.sy
1976 regress1/sygus/univ_2-long-repeat.sy
1977 regress1/sygus/yoni-true-sol.smt2
1978 regress1/sym/q-constant.smt2
1979 regress1/sym/q-function.smt2
1980 regress1/sym/qf-function.smt2
1981 regress1/sym/sb-wrong.smt2
1982 regress1/sym/sym-setAB.smt2
1983 regress1/sym/sym1.smt2
1984 regress1/sym/sym2.smt2
1985 regress1/sym/sym3.smt2
1986 regress1/sym/sym4.smt2
1987 regress1/sym/sym5.smt2
1988 regress1/sym/sym6.smt2
1989 regress1/sym/sym7-uf.smt2
1993 regress1/uflia/DRAGON_11_e1_2450.ec.minimized.smt2
1994 regress1/uflia/FIREFLY_3_e2_2236_e7_3681.ec.core.smt2
1995 regress1/uflia/FIREFLY_luke_1b_e2_3049_e7_1173.ec.minimized.smt2
1996 regress1/uflia/microwave21.ec.minimized.smt2
1997 regress1/uflia/simple_cyclic2.smt2
1998 regress1/uflia/speed2_e8_449_e8_517.ec.smt2
1999 regress1/uflia/stalmark_e7_27_e7_31.ec.smt2
2000 regress1/wrong-qfabvfp-smtcomp2018.smt2
2003 #-----------------------------------------------------------------------------#
2004 # Regression level 2 tests
2007 regress2/DTP_k2_n35_c175_s15.smt2
2008 regress2/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2
2009 regress2/GEO123+1.minimized.smt2
2010 regress2/arith/abz5_1400.smtv1.smt2
2011 regress2/arith/lpsat-goal-9.smt2
2012 regress2/arith/pursuit-safety-11.smtv1.smt2
2013 regress2/arith/pursuit-safety-12.smtv1.smt2
2014 regress2/arith/sc-7.base.cvc.smtv1.smt2
2015 regress2/arith/uart-8.base.cvc.smtv1.smt2
2016 regress2/auflia-fuzz06.smtv1.smt2
2017 regress2/bug136.smtv1.smt2
2018 regress2/bug148.smtv1.smt2
2019 regress2/bug394.smt2
2020 regress2/bug674.smt2
2021 regress2/bug765.smt2
2022 regress2/bug812.smt2
2023 regress2/bv/opStructure_MBA_6.scrambled.min.smt2
2024 regress2/bv_to_int_ashr.smt2
2025 regress2/bv_to_int_mask_array_1.smt2
2026 regress2/bv_to_int_mask_array_2.smt2
2027 regress2/bv_to_int_shifts.smt2
2028 regress2/error0.smt2
2029 regress2/error1.smtv1.smt2
2030 regress2/friedman_n4_i5.smtv1.smt2
2031 regress2/fuzz_2.smtv1.smt2
2032 regress2/hash_sat_06_19.smt2
2033 regress2/hash_sat_07_17.smt2
2034 regress2/hash_sat_09_09.smt2
2035 regress2/hash_sat_10_09.smt2
2036 regress2/ho/auth0068.smt2
2037 regress2/ho/bug_instfalse_SEU882^5.p
2038 regress2/ho/fta0409.smt2
2039 regress2/ho/involved_parsing_ALG248^3.p
2040 regress2/ho/partial_app_interpreted_SWW474^2.p
2041 regress2/ho/SYO362^5.p
2044 regress2/instance_1444.smtv1.smt2
2045 regress2/javafe.ast.StandardPrettyPrint.319_no_forall.smt2
2046 regress2/javafe.ast.WhileStmt.447_no_forall.smt2
2047 regress2/ooo.rf6.smt2
2048 regress2/ooo.tag10.smt2
2049 regress2/piVC_5581bd.smt2
2050 regress2/push-pop/DRAGON_4_e2_2799_e3_1915.lus.ic3.1.min.smt2
2051 regress2/quantifiers/AdditiveMethods_AdditiveMethods..ctor.smt2
2052 regress2/quantifiers/gn-wrong-091018.smt2
2053 regress2/quantifiers/javafe.ast.ArrayInit.35.smt2
2054 regress2/quantifiers/javafe.ast.StandardPrettyPrint.319.smt2
2055 regress2/quantifiers/javafe.ast.WhileStmt.447.smt2
2056 regress2/quantifiers/javafe.tc.CheckCompilationUnit.001.smt2
2057 regress2/quantifiers/javafe.tc.FlowInsensitiveChecks.682.smt2
2058 regress2/quantifiers/net-policy-no-time.smt2
2059 regress2/quantifiers/nunchaku2309663.nun.min.smt2
2060 regress2/quantifiers/specsharp-WindowsCard.15.RTE.Terminate_System.Int32.smt2
2061 regress2/quantifiers/sygus-inst-ufbv-sdlx-fixpoint-5.smt2
2062 regress2/quantifiers/syn874-1.smt2
2063 regress2/simplify.javafe.ast.ArrayInit.35_without_quantification2.smt2
2064 regress2/strings/cmi-split-cm-fail.smt2
2065 regress2/strings/cmu-dis-0707-3.smt2
2066 regress2/strings/cmu-disagree-0707-dd.smt2
2067 regress2/strings/cmu-prereg-fmf.smt2
2068 regress2/strings/cmu-repl-len-nterm.smt2
2069 regress2/strings/issue3203.smt2
2070 regress2/strings/issue918.smt2
2071 regress2/strings/non_termination_regular_expression6.smt2
2072 regress2/strings/norn-dis-0707-3.smt2
2073 regress2/strings/range-perf.smt2
2074 regress2/strings/repl-repl.smt2
2075 regress2/strings/repl-repl-i-no-push.smt2
2076 regress2/strings/replaceall-diffrange.smt2
2077 regress2/strings/replaceall-len-c.smt2
2078 regress2/strings/small-1.smt2
2079 regress2/sygus/DRAGON_1.lus.sy
2080 regress2/sygus/MPwL_d1s3.sy
2081 regress2/sygus/array_sum_dd.sy
2082 regress2/sygus/cegisunif-depth1-bv.sy
2083 regress2/sygus/ex23.sy
2084 regress2/sygus/examples-deq.sy
2085 regress2/sygus/icfp_easy_mt_ite.sy
2086 regress2/sygus/issue4022-conjecture-gen.smt2
2087 regress2/sygus/lustre-real.sy
2088 regress2/sygus/max2-univ.sy
2089 regress2/sygus/min_IC_1.sy
2090 regress2/sygus/mpg_guard1-dd.sy
2091 regress2/sygus/multi-udiv.sy
2092 regress2/sygus/nia-max-square.sy
2093 regress2/sygus/no-syntax-test-no-si.sy
2094 regress2/sygus/pbe_bvurem.sy
2095 regress2/sygus/process-10-vars-2fun.sy
2096 regress2/sygus/process-arg-invariance.sy
2097 regress2/sygus/real-grammar-neg.sy
2098 regress2/sygus/sets-fun-test.sy
2099 regress2/sygus/strings-no-syntax-len.sy
2100 regress2/sygus/three.sy
2101 regress2/sygus/vcb.sy
2102 regress2/typed_v1l50016-simp.cvc
2103 regress2/uflia-error0.smt2
2104 regress2/xs-09-16-3-4-1-5.smtv1.smt2
2107 #-----------------------------------------------------------------------------#
2108 # Regression level 3 tests
2111 regress3/arith_prp-13-24.smt2
2112 regress3/bmc-ibm-1.smtv1.smt2
2113 regress3/bmc-ibm-2.smtv1.smt2
2114 regress3/bmc-ibm-5.smtv1.smt2
2115 regress3/bmc-ibm-7.smtv1.smt2
2116 regress3/bv_to_int_and_or.smt2
2117 regress3/eq_diamond14.smtv1.smt2
2118 regress3/friedman_n6_i4.smtv1.smt2
2120 regress3/incorrect1.smtv1.smt2
2121 regress3/issue2429.smt2
2122 regress3/issue4170.smt2
2123 regress3/pp-regfile.smtv1.smt2
2124 regress3/qwh.35.405.shuffled-as.sat03-1651.smtv1.smt2
2125 regress3/siegel-nl-bases.smt2
2126 regress3/sixfuncs.sy
2127 regress3/strings-any-term.sy
2128 regress3/strings/extf_d_perf.smt2
2129 regress3/strings/unsat-circ-reduce.smt2
2132 #-----------------------------------------------------------------------------#
2133 # Regression level 4 tests
2136 regress4/C880mul.miter.shuffled-as.sat03-348.smtv1.smt2
2137 regress4/NEQ016_size5.smtv1.smt2
2138 regress4/bug143.smtv1.smt2
2139 regress4/comb2.shuffled-as.sat03-420.smtv1.smt2
2141 regress4/instance_1151.smtv1.smt2
2144 #-----------------------------------------------------------------------------#
2145 # Disabled tests, will not be run.
2147 set(regression_disabled_tests
2148 regress0/arith/bug549.cvc
2149 regress0/arith/incorrect1.smtv1.smt2
2150 regress0/arith/integers/arith-int-014.cvc
2151 regress0/arith/integers/arith-int-015.cvc
2152 regress0/arith/integers/arith-int-021.cvc
2153 regress0/arith/integers/arith-int-023.cvc
2154 regress0/arith/integers/arith-int-025.cvc
2155 regress0/arith/integers/arith-int-079.cvc
2156 regress0/arith/integers/arith-interval.cvc
2157 regress0/arith/miplib-opt1217--27.smtv1.smt2
2158 regress0/arith/miplib-pp08a-3000.smtv1.smt2
2159 regress0/arr1.smtv1.smt2
2161 regress0/arr2.smtv1.smt2
2162 # regress0/aufbv/bug348 does not seem to terminate with proofs
2163 regress0/aufbv/bug348.smtv1.smt2
2164 regress0/aufbv/bug349.smtv1.smt2
2165 regress0/aufbv/bug493.smtv1.smt2
2166 regress0/aufbv/dubreva005ue.smtv1.smt2
2167 regress0/aufbv/fifo32bc06k08.smtv1.smt2
2168 regress0/aufbv/fifo32in06k08.delta01.smtv1.smt2
2169 regress0/aufbv/fifo32in06k08.smtv1.smt2
2170 regress0/aufbv/no_init_multi_delete14.smtv1.smt2
2171 regress0/aufbv/try3_sameret_functions_fse-bfs_tac.calc_next.il.fse-bfs.smtv1.smt2
2172 regress0/aufbv/wchains010ue.smtv1.smt2
2173 regress0/auflia/fuzz01.smtv1.smt2
2174 regress0/bug2.smtv1.smt2
2175 regress0/bug374.smtv1.smt2
2176 regress0/bv/bug345.smtv1.smt2
2177 regress0/bv/bvcomp.cvc
2178 regress0/bv/bvsmod.smt2
2179 regress0/bv/core/bitvec0.delta01.smtv1.smt2
2180 regress0/bv/core/bitvec1.smtv1.smt2
2181 regress0/bv/core/bitvec3.smtv1.smt2
2182 regress0/bv/core/bv_eq_diamond11.smtv1.smt2
2183 regress0/bv/core/bv_eq_diamond12.smtv1.smt2
2184 regress0/bv/core/bv_eq_diamond13.smtv1.smt2
2185 regress0/bv/core/bv_eq_diamond14.smtv1.smt2
2186 regress0/bv/core/bv_eq_diamond15.smtv1.smt2
2187 regress0/bv/core/bv_eq_diamond16.smtv1.smt2
2188 regress0/bv/core/bv_eq_diamond17.smtv1.smt2
2189 regress0/bv/core/concat-merge-0.cvc
2190 regress0/bv/core/concat-merge-1.cvc
2191 regress0/bv/core/concat-merge-2.cvc
2192 regress0/bv/core/concat-merge-3.cvc
2193 regress0/bv/core/constant_core.smt2
2194 regress0/bv/core/equality-00.cvc
2195 regress0/bv/core/equality-01.cvc
2196 regress0/bv/core/equality-02.cvc
2197 regress0/bv/core/equality-03.cvc
2198 regress0/bv/core/equality-03.smtv1.smt2
2199 regress0/bv/core/equality-04.smtv1.smt2
2200 regress0/bv/core/equality-05.smtv1.smt2
2201 regress0/bv/core/ext_con_004_001_1024.smtv1.smt2
2202 regress0/bv/core/extract-concat-0.cvc
2203 regress0/bv/core/extract-concat-1.cvc
2204 regress0/bv/core/extract-concat-10.cvc
2205 regress0/bv/core/extract-concat-11.cvc
2206 regress0/bv/core/extract-concat-2.cvc
2207 regress0/bv/core/extract-concat-3.cvc
2208 regress0/bv/core/extract-concat-4.cvc
2209 regress0/bv/core/extract-concat-5.cvc
2210 regress0/bv/core/extract-concat-6.cvc
2211 regress0/bv/core/extract-concat-7.cvc
2212 regress0/bv/core/extract-concat-8.cvc
2213 regress0/bv/core/extract-concat-9.cvc
2214 regress0/bv/core/extract-constant.cvc
2215 regress0/bv/core/extract-extract-0.cvc
2216 regress0/bv/core/extract-extract-1.cvc
2217 regress0/bv/core/extract-extract-10.cvc
2218 regress0/bv/core/extract-extract-11.cvc
2219 regress0/bv/core/extract-extract-2.cvc
2220 regress0/bv/core/extract-extract-3.cvc
2221 regress0/bv/core/extract-extract-4.cvc
2222 regress0/bv/core/extract-extract-5.cvc
2223 regress0/bv/core/extract-extract-6.cvc
2224 regress0/bv/core/extract-extract-7.cvc
2225 regress0/bv/core/extract-extract-8.cvc
2226 regress0/bv/core/extract-extract-9.cvc
2227 regress0/bv/core/extract-whole-0.cvc
2228 regress0/bv/core/extract-whole-1.cvc
2229 regress0/bv/core/extract-whole-2.cvc
2230 regress0/bv/core/extract-whole-3.cvc
2231 regress0/bv/core/extract-whole-4.cvc
2232 regress0/bv/core/incremental.smtv1.smt2
2233 regress0/bv/core/slice-01.cvc
2234 regress0/bv/core/slice-02.cvc
2235 regress0/bv/core/slice-03.cvc
2236 regress0/bv/core/slice-04.cvc
2237 regress0/bv/core/slice-05.cvc
2238 regress0/bv/core/slice-06.cvc
2239 regress0/bv/core/slice-07.cvc
2240 regress0/bv/core/slice-08.cvc
2241 regress0/bv/core/slice-09.cvc
2242 regress0/bv/core/slice-10.cvc
2243 regress0/bv/core/slice-11.cvc
2244 regress0/bv/core/slice-12.cvc
2245 regress0/bv/core/slice-13.cvc
2246 regress0/bv/core/slice-14.cvc
2247 regress0/bv/core/slice-15.cvc
2248 regress0/bv/core/slice-16.cvc
2249 regress0/bv/core/slice-17.cvc
2250 regress0/bv/core/slice-18.cvc
2251 regress0/bv/core/slice-19.cvc
2252 regress0/bv/core/slice-20.cvc
2253 regress0/bv/fuzz07-delta.smtv1.smt2
2254 # Proof checking takes too long. Add this back. FIXME
2255 regress0/bv/fuzz15.delta01.smtv1.smt2
2257 regress0/bv/fuzz15.smtv1.smt2
2258 regress0/bv/fuzz16.smtv1.smt2
2259 regress0/bv/fuzz17.smtv1.smt2
2260 regress0/bv/incorrect1.delta01.smtv1.smt2
2261 regress0/bv/incorrect1.smtv1.smt2
2262 regress0/bv/inequality00.smt2
2263 regress0/bv/inequality01.smt2
2264 regress0/bv/inequality02.smt2
2265 regress0/bv/inequality03.smt2
2266 regress0/bv/inequality04.smt2
2267 regress0/bv/inequality05.smt2
2268 regress0/bv/test00.smtv1.smt2
2269 regress0/cvc3-bug15.cvc
2270 # regress0/datatypes/datatype-dump.cvc (FIXME #1649)
2271 regress0/datatypes/datatype-dump.cvc
2272 regress0/decision/uflia-xs-09-16-3-4-1-5.smtv1.smt2
2273 regress0/decision/wchains010ue.smtv1.smt2
2274 regress0/incorrect1.smtv1.smt2
2276 regress0/ite_arith.smt2
2277 regress0/lemmas/fischer3-mutex-16.smtv1.smt2
2278 regress0/nl/all-logic.smt2
2279 regress0/quantifiers/qbv-multi-lit-uge.smt2
2280 regress0/quantifiers/qbv-test-invert-bvshl-0-neq.smt2
2281 regress0/quantifiers/qbv-test-invert-concat-0-neq.smt2
2282 regress0/quantifiers/qbv-test-invert-concat-1-neq.smt2
2283 regress0/sets/mar2014/stacks0.hs.78.cvc4.smt2
2284 regress0/sets/setel-eq.smt2
2285 regress0/sets/sets-new.smt2
2286 regress0/sets/sets-testlemma-ints.smt2
2287 regress0/sets/sets-testlemma-reals.smt2
2288 regress0/symmetric.smtv1.smt2
2289 regress0/tptp/BOO003-4.p
2290 regress0/tptp/BOO027-1.p
2291 regress0/tptp/MGT031-1.p
2292 regress0/tptp/NLP114-1.p
2293 regress0/tptp/SYN075+1.p
2294 regress0/uf/PEQ018_size4.smtv1.smt2
2295 regress0/uf/SEQ032_size2.smtv1.smt2
2296 regress0/uf/iso_icl_repgen004.smtv1.smt2
2297 regress0/uflia/diseqprop.01.smtv1.smt2
2298 regress0/uflia/diseqprop.02.smtv1.smt2
2299 regress0/uflia/diseqprop.03.smtv1.smt2
2300 regress0/uflia/diseqprop.04.smtv1.smt2
2301 regress0/uflia/diseqprop.05.smtv1.smt2
2302 regress0/uflia/diseqprop.06.smtv1.smt2
2303 regress0/uflia/xs-09-16-3-4-1-5.delta05.smtv1.smt2
2304 regress0/uflra/pb_real_10_0200_10_25.smtv1.smt2
2305 regress0/uflra/pb_real_10_0200_10_27.smtv1.smt2
2306 # dejan: disabled these because it's mixed arithmetic and it doesn't go
2307 # well when changing theoryof:
2308 regress0/unconstrained/arith2.smt2
2309 regress0/unconstrained/arith7.smt2
2311 # lianah: disabled these as the unconstrained terms are no longer
2312 # recognized after implementing the divide-by-zero semantics for bv division:
2313 regress0/unconstrained/bvconcat.smt2
2314 regress0/unconstrained/bvdiv.smtv1.smt2
2316 regress1/arith/arith-int-001.cvc
2317 regress1/arith/arith-int-002.cvc
2318 regress1/arith/arith-int-003.cvc
2319 regress1/arith/arith-int-005.cvc
2320 regress1/arith/arith-int-006.cvc
2321 regress1/arith/arith-int-007.cvc
2322 regress1/arith/arith-int-008.cvc
2323 regress1/arith/arith-int-009.cvc
2324 regress1/arith/arith-int-010.cvc
2325 regress1/arith/arith-int-016.cvc
2326 regress1/arith/arith-int-017.cvc
2327 regress1/arith/arith-int-018.cvc
2328 regress1/arith/arith-int-019.cvc
2329 regress1/arith/arith-int-020.cvc
2330 regress1/arith/arith-int-026.cvc
2331 regress1/arith/arith-int-027.cvc
2332 regress1/arith/arith-int-028.cvc
2333 regress1/arith/arith-int-029.cvc
2334 regress1/arith/arith-int-030.cvc
2335 regress1/arith/arith-int-031.cvc
2336 regress1/arith/arith-int-032.cvc
2337 regress1/arith/arith-int-033.cvc
2338 regress1/arith/arith-int-034.cvc
2339 regress1/arith/arith-int-035.cvc
2340 regress1/arith/arith-int-036.cvc
2341 regress1/arith/arith-int-037.cvc
2342 regress1/arith/arith-int-038.cvc
2343 regress1/arith/arith-int-039.cvc
2344 regress1/arith/arith-int-040.cvc
2345 regress1/arith/arith-int-041.cvc
2346 regress1/arith/arith-int-043.cvc
2347 regress1/arith/arith-int-044.cvc
2348 regress1/arith/arith-int-045.cvc
2349 regress1/arith/arith-int-046.cvc
2350 regress1/arith/arith-int-049.cvc
2351 regress1/arith/arith-int-051.cvc
2352 regress1/arith/arith-int-052.cvc
2353 regress1/arith/arith-int-053.cvc
2354 regress1/arith/arith-int-054.cvc
2355 regress1/arith/arith-int-055.cvc
2356 regress1/arith/arith-int-056.cvc
2357 regress1/arith/arith-int-057.cvc
2358 regress1/arith/arith-int-058.cvc
2359 regress1/arith/arith-int-059.cvc
2360 regress1/arith/arith-int-060.cvc
2361 regress1/arith/arith-int-061.cvc
2362 regress1/arith/arith-int-062.cvc
2363 regress1/arith/arith-int-063.cvc
2364 regress1/arith/arith-int-064.cvc
2365 regress1/arith/arith-int-065.cvc
2366 regress1/arith/arith-int-066.cvc
2367 regress1/arith/arith-int-067.cvc
2368 regress1/arith/arith-int-068.cvc
2369 regress1/arith/arith-int-069.cvc
2370 regress1/arith/arith-int-070.cvc
2371 regress1/arith/arith-int-071.cvc
2372 regress1/arith/arith-int-072.cvc
2373 regress1/arith/arith-int-073.cvc
2374 regress1/arith/arith-int-074.cvc
2375 regress1/arith/arith-int-075.cvc
2376 regress1/arith/arith-int-076.cvc
2377 regress1/arith/arith-int-077.cvc
2378 regress1/arith/arith-int-078.cvc
2379 regress1/arith/arith-int-080.cvc
2380 regress1/arith/arith-int-081.cvc
2381 regress1/arith/arith-int-082.cvc
2382 regress1/arith/arith-int-083.cvc
2383 regress1/arith/arith-int-086.cvc
2384 regress1/arith/arith-int-087.cvc
2385 regress1/arith/arith-int-088.cvc
2386 regress1/arith/arith-int-089.cvc
2387 regress1/arith/arith-int-090.cvc
2388 regress1/arith/arith-int-091.cvc
2389 regress1/arith/arith-int-092.cvc
2390 regress1/arith/arith-int-093.cvc
2391 regress1/arith/arith-int-094.cvc
2392 regress1/arith/arith-int-095.cvc
2393 regress1/arith/arith-int-096.cvc
2394 regress1/arith/arith-int-099.cvc
2395 regress1/arith/arith-int-100.cvc
2396 regress1/auflia/bug337.smt2
2397 regress1/bug472.smt2
2399 regress1/bug590.smt2
2400 regress1/bv/bench_38.delta.smt2
2401 regress1/crash_burn_locusts.smt2
2402 # regress1/ho/hoa0102.smt2 results in an assertion failure (see issue #1650).
2403 regress1/ho/hoa0102.smt2
2404 # issue1048-arrays-int-real.smt2 -- different errors on debug and production.
2405 regress1/issue1048-arrays-int-real.smt2
2406 # times out after update to tangent planes
2407 regress1/nl/NAVIGATION2.smt2
2408 # sat or unknown in different builds
2409 regress1/nl/issue3307.smt2
2410 # ajreynol: different error messages on production and debug:
2411 regress1/quantifiers/macro-subtype-param.smt2
2412 # times out with competition build:
2413 regress1/quantifiers/model_6_1_bv.smt2
2414 # ajreynol: different error messages on production and debug:
2415 regress1/quantifiers/subtype-param-unk.smt2
2416 regress1/quantifiers/subtype-param.smt2
2418 # regress1/quantifiers/set3.smt2 does not terminate/takes a long time when
2419 # doing a coverage build with LFSC.
2420 regress1/quantifiers/set3.smt2
2421 regress1/rels/garbage_collect.cvc
2422 regress1/sets/setofsets-disequal.smt2
2423 regress1/sets/finite-type/sets-card-neg-mem-union-2.smt2
2424 regress1/simple-rdl-definefun.smt2
2425 # does not solve after minor modification to search
2426 regress1/sygus/car_3.lus.sy
2427 regress1/sygus/Base16_1.sy
2428 regress1/sygus/enum-test.sy
2429 regress1/sygus/inv_gen_fig8.sy
2430 # slow (179 seconds) in debug at 45e489e2
2431 regress1/sygus/unifpi-solve-car_1.lus.sy
2432 # rely on heuristic solution reconstruction TODO #3146 revisit
2433 regress1/sygus/array_search_2.sy
2434 regress1/sygus/array_sum_2_5.sy
2435 regress1/sygus/crcy-si-rcons.sy
2436 # currently slow at c9fd28a
2437 regress1/sygus/issue3580.sy
2438 regress2/arith/arith-int-098.cvc
2439 regress2/arith/miplib-opt1217--27.smt2
2440 regress2/arith/miplib-pp08a-3000.smt2
2442 regress2/arith/real2int-test.smt2
2443 regress2/bug396.smt2
2444 regress2/nl/dumortier-050317.smt2
2445 regress2/nl/nt-lemmas-bad.smt2
2446 regress2/quantifiers/ForElimination-scala-9.smt2
2447 regress2/quantifiers/small-bug1-fixpoint-3.smt2
2448 # currently slow at 24357fea
2449 regress2/sygus/inv_gen_n_c11.sy
2450 regress2/xs-11-20-5-2-5-3.smtv1.smt2
2451 regress2/xs-11-20-5-2-5-3.smt2
2454 #-----------------------------------------------------------------------------#
2455 # Add target 'regress', builds and runs
2456 # > regression tests of levels 0 and 1
2458 get_target_property(path_to_cvc4 cvc4-bin RUNTIME_OUTPUT_DIRECTORY)
2459 set(run_regress_script ${CMAKE_CURRENT_LIST_DIR}/run_regression.py)
2461 add_custom_target(build-regress DEPENDS cvc4-bin)
2462 add_dependencies(build-tests build-regress)
2464 add_custom_target(regress
2466 ctest --output-on-failure -L "regress[0-2]" -j${CTEST_NTHREADS} $$ARGS
2467 DEPENDS build-regress)
2469 macro(cvc4_add_regression_test level file)
2471 ${run_regress_script}
2472 ${RUN_REGRESSION_ARGS}
2473 ${path_to_cvc4}/cvc4 ${CMAKE_CURRENT_LIST_DIR}/${file})
2474 set_tests_properties(${file} PROPERTIES LABELS "regress${level}")
2476 # For CMake 3.9.0 and newer, skipped tests do not count as a failure anymore:
2477 # https://cmake.org/cmake/help/latest/release/3.9.html#other-changes
2478 # This means that for newer versions, we can use the SKIP_RETURN_CODE to mark
2479 # skipped tests as such.
2480 if(NOT ${CMAKE_VERSION} VERSION_LESS "3.9.0")
2481 set_tests_properties(${file} PROPERTIES SKIP_RETURN_CODE 77)
2485 if(NOT ${CMAKE_VERSION} VERSION_LESS "3.9.0")
2486 # For CMake 3.9.0 and newer, we want the regression script to return 77 for
2487 # skipped tests, such that we can mark them as skipped. See the
2488 # `cvc4_add_regression_test` macro for more details.
2489 set(RUN_REGRESSION_ARGS ${RUN_REGRESSION_ARGS} --use-skip-return-code)
2492 foreach(file ${regress_0_tests})
2493 cvc4_add_regression_test(0 ${file})
2496 foreach(file ${regress_1_tests})
2497 cvc4_add_regression_test(1 ${file})
2500 foreach(file ${regress_2_tests})
2501 cvc4_add_regression_test(2 ${file})
2504 foreach(file ${regress_3_tests})
2505 cvc4_add_regression_test(3 ${file})
2508 foreach(file ${regress_4_tests})
2509 cvc4_add_regression_test(4 ${file})
projects / cvc5.git / blob