1 # escape the `=' in file names
5 regress0/arith/apply2const-test.smt2 \
6 regress0/arith/arith.01.cvc \
7 regress0/arith/arith.02.cvc \
8 regress0/arith/arith.03.cvc \
9 regress0/arith/bug443.delta01.smt \
10 regress0/arith/bug547.2.smt2 \
11 regress0/arith/bug569.smt2 \
12 regress0/arith/delta-minimized-row-vector-bug.smt \
13 regress0/arith/div.01.smt2 \
14 regress0/arith/div.02.smt2 \
15 regress0/arith/div.04.smt2 \
16 regress0/arith/div.05.smt2 \
17 regress0/arith/div.07.smt2 \
18 regress0/arith/div-chainable.smt2 \
19 regress0/arith/fuzz_3-eq.smt \
20 regress0/arith/integers/arith-int-042.cvc \
21 regress0/arith/integers/arith-int-042.min.cvc \
22 regress0/arith/leq.01.smt \
23 regress0/arith/miplib.cvc \
24 regress0/arith/miplib2.cvc \
25 regress0/arith/miplib4.cvc \
26 regress0/arith/miplibtrick.smt \
27 regress0/arith/mod-simp.smt2 \
28 regress0/arith/mod.01.smt2 \
29 regress0/arith/mult.01.smt2 \
30 regress0/arrayinuf_declare.smt2 \
31 regress0/arrays/arrays0.smt2 \
32 regress0/arrays/arrays1.smt2 \
33 regress0/arrays/arrays2.smt2 \
34 regress0/arrays/arrays3.smt2 \
35 regress0/arrays/arrays4.smt2 \
36 regress0/arrays/bool-array.smt2 \
37 regress0/arrays/bug272.minimized.smt \
38 regress0/arrays/bug272.smt \
39 regress0/arrays/bug637.delta.smt2 \
40 regress0/arrays/constarr.cvc \
41 regress0/arrays/constarr.smt2 \
42 regress0/arrays/constarr2.cvc \
43 regress0/arrays/constarr2.smt2 \
44 regress0/arrays/incorrect1.smt \
45 regress0/arrays/incorrect10.smt \
46 regress0/arrays/incorrect11.smt \
47 regress0/arrays/incorrect2.minimized.smt \
48 regress0/arrays/incorrect2.smt \
49 regress0/arrays/incorrect3.smt \
50 regress0/arrays/incorrect4.smt \
51 regress0/arrays/incorrect5.smt \
52 regress0/arrays/incorrect6.smt \
53 regress0/arrays/incorrect7.smt \
54 regress0/arrays/incorrect8.minimized.smt \
55 regress0/arrays/incorrect8.smt \
56 regress0/arrays/incorrect9.smt \
57 regress0/arrays/swap_t1_np_nf_ai_00005_007.cvc.smt \
58 regress0/arrays/x2.smt \
59 regress0/arrays/x3.smt \
60 regress0/aufbv/array_rewrite_bug.smt \
61 regress0/aufbv/bug00.smt \
62 regress0/aufbv/bug338.smt2 \
63 regress0/aufbv/bug347.smt \
64 regress0/aufbv/bug451.smt \
65 regress0/aufbv/bug509.smt \
66 regress0/aufbv/bug580.delta.smt2 \
67 regress0/aufbv/diseqprop.01.smt \
68 regress0/aufbv/dubreva005ue.delta01.smt \
69 regress0/aufbv/fifo32bc06k08.delta01.smt \
70 regress0/aufbv/fuzz00.smt \
71 regress0/aufbv/fuzz01.delta01.smt \
72 regress0/aufbv/fuzz01.smt \
73 regress0/aufbv/fuzz02.delta01.smt \
74 regress0/aufbv/fuzz02.smt \
75 regress0/aufbv/fuzz03.delta01.smt \
76 regress0/aufbv/fuzz03.smt \
77 regress0/aufbv/fuzz04.delta01.smt \
78 regress0/aufbv/fuzz04.smt \
79 regress0/aufbv/fuzz05.delta01.smt \
80 regress0/aufbv/fuzz05.smt \
81 regress0/aufbv/fuzz06.delta01.smt \
82 regress0/aufbv/fuzz06.smt \
83 regress0/aufbv/fuzz07.smt \
84 regress0/aufbv/fuzz08.smt \
85 regress0/aufbv/fuzz09.smt \
86 regress0/aufbv/fuzz11.smt \
87 regress0/aufbv/fuzz12.smt \
88 regress0/aufbv/fuzz13.smt \
89 regress0/aufbv/fuzz14.smt \
90 regress0/aufbv/fuzz15.smt \
91 regress0/aufbv/rewrite_bug.smt \
92 regress0/aufbv/try3_sameret_functions_fse-bfs_tac.calc_next.il.fse-bfs.delta01.smt \
93 regress0/aufbv/try5_small_difret_functions_wp_su.set_char_quoting.il.wp.delta01.smt \
94 regress0/aufbv/wchains010ue.delta01.smt \
95 regress0/aufbv/wchains010ue.delta02.smt \
96 regress0/auflia/a17.smt \
97 regress0/auflia/bug336.smt2 \
98 regress0/auflia/error72.delta2.smt \
99 regress0/auflia/fuzz-error1099.smt \
100 regress0/auflia/fuzz-error232.smt \
101 regress0/auflia/fuzz01.delta01.smt \
102 regress0/auflia/fuzz02.smt \
103 regress0/auflia/fuzz03.smt \
104 regress0/auflia/fuzz04.smt \
105 regress0/auflia/fuzz05.smt \
106 regress0/auflia/x2.smt \
107 regress0/boolean-prec.cvc \
108 regress0/boolean-terms-bug-array.smt2 \
109 regress0/boolean-terms-kernel1.smt2 \
110 regress0/boolean-terms.cvc \
111 regress0/bt-test-00.smt2 \
112 regress0/bt-test-01.smt2 \
113 regress0/bug1247.smt2 \
114 regress0/bug161.smt \
115 regress0/bug164.smt \
116 regress0/bug167.smt \
117 regress0/bug168.smt \
118 regress0/bug187.smt2 \
119 regress0/bug217.smt2 \
120 regress0/bug220.smt2 \
121 regress0/bug239.smt \
122 regress0/bug274.cvc \
123 regress0/bug288.smt \
124 regress0/bug288b.smt \
125 regress0/bug288c.smt \
126 regress0/bug303.smt2 \
127 regress0/bug310.cvc \
129 regress0/bug322.cvc \
130 regress0/bug322b.cvc \
131 regress0/bug339.smt2 \
132 regress0/bug365.smt2 \
133 regress0/bug382.smt2 \
134 regress0/bug383.smt2 \
135 regress0/bug398.smt2 \
136 regress0/bug421.smt2 \
137 regress0/bug421b.smt2 \
138 regress0/bug480.smt2 \
139 regress0/bug484.smt2 \
140 regress0/bug486.cvc \
142 regress0/bug512.minimized.smt2 \
143 regress0/bug521.minimized.smt2 \
144 regress0/bug522.smt2 \
145 regress0/bug528a.smt2 \
146 regress0/bug541.smt2 \
147 regress0/bug544.smt2 \
148 regress0/bug548a.smt2 \
149 regress0/bug576.smt2 \
150 regress0/bug576a.smt2 \
151 regress0/bug578.smt2 \
152 regress0/bug586.cvc \
153 regress0/bug595.cvc \
154 regress0/bug596.cvc \
155 regress0/bug596b.cvc \
156 regress0/bug605.cvc \
157 regress0/bug639.smt2 \
158 regress0/buggy-ite.smt2 \
159 regress0/bv/ackermann1.smt2 \
160 regress0/bv/ackermann2.smt2 \
161 regress0/bv/bool-to-bv.smt2 \
162 regress0/bv/bug260a.smt \
163 regress0/bv/bug260b.smt \
164 regress0/bv/bug440.smt \
165 regress0/bv/bug733.smt2 \
166 regress0/bv/bug734.smt2 \
167 regress0/bv/bv-abstr-bug.smt2 \
168 regress0/bv/bv-abstr-bug2.smt2 \
169 regress0/bv/bv-int-collapse1.smt2 \
170 regress0/bv/bv-int-collapse2.smt2 \
171 regress0/bv/bv-options1.smt2 \
172 regress0/bv/bv-options2.smt2 \
173 regress0/bv/bv-options3.smt2 \
174 regress0/bv/bv-options4.smt2 \
175 regress0/bv/bv-to-bool.smt \
176 regress0/bv/bv2nat-ground-c.smt2 \
177 regress0/bv/bv2nat-simp-range.smt2 \
178 regress0/bv/bvmul-pow2-only.smt2 \
179 regress0/bv/bvsimple.cvc \
180 regress0/bv/calc2_sec2_shifter_mult_bmc15.atlas.delta01.smt \
181 regress0/bv/core/a78test0002.smt \
182 regress0/bv/core/a95test0002.smt \
183 regress0/bv/core/bitvec0.smt \
184 regress0/bv/core/bitvec2.smt \
185 regress0/bv/core/bitvec5.smt \
186 regress0/bv/core/bitvec7.smt \
187 regress0/bv/core/bv_eq_diamond10.smt \
188 regress0/bv/core/concat-merge-0.smt \
189 regress0/bv/core/concat-merge-1.smt \
190 regress0/bv/core/concat-merge-2.smt \
191 regress0/bv/core/concat-merge-3.smt \
192 regress0/bv/core/equality-00.smt \
193 regress0/bv/core/equality-01.smt \
194 regress0/bv/core/equality-02.smt \
195 regress0/bv/core/equality-05.smt \
196 regress0/bv/core/extract-concat-0.smt \
197 regress0/bv/core/extract-concat-1.smt \
198 regress0/bv/core/extract-concat-10.smt \
199 regress0/bv/core/extract-concat-11.smt \
200 regress0/bv/core/extract-concat-2.smt \
201 regress0/bv/core/extract-concat-3.smt \
202 regress0/bv/core/extract-concat-4.smt \
203 regress0/bv/core/extract-concat-5.smt \
204 regress0/bv/core/extract-concat-6.smt \
205 regress0/bv/core/extract-concat-7.smt \
206 regress0/bv/core/extract-concat-8.smt \
207 regress0/bv/core/extract-concat-9.smt \
208 regress0/bv/core/extract-constant.smt \
209 regress0/bv/core/extract-extract-0.smt \
210 regress0/bv/core/extract-extract-1.smt \
211 regress0/bv/core/extract-extract-10.smt \
212 regress0/bv/core/extract-extract-11.smt \
213 regress0/bv/core/extract-extract-2.smt \
214 regress0/bv/core/extract-extract-3.smt \
215 regress0/bv/core/extract-extract-4.smt \
216 regress0/bv/core/extract-extract-5.smt \
217 regress0/bv/core/extract-extract-6.smt \
218 regress0/bv/core/extract-extract-7.smt \
219 regress0/bv/core/extract-extract-8.smt \
220 regress0/bv/core/extract-extract-9.smt \
221 regress0/bv/core/extract-whole-0.smt \
222 regress0/bv/core/extract-whole-1.smt \
223 regress0/bv/core/extract-whole-2.smt \
224 regress0/bv/core/extract-whole-3.smt \
225 regress0/bv/core/extract-whole-4.smt \
226 regress0/bv/core/slice-01.smt \
227 regress0/bv/core/slice-02.smt \
228 regress0/bv/core/slice-03.smt \
229 regress0/bv/core/slice-04.smt \
230 regress0/bv/core/slice-05.smt \
231 regress0/bv/core/slice-06.smt \
232 regress0/bv/core/slice-07.smt \
233 regress0/bv/core/slice-08.smt \
234 regress0/bv/core/slice-09.smt \
235 regress0/bv/core/slice-10.smt \
236 regress0/bv/core/slice-11.smt \
237 regress0/bv/core/slice-12.smt \
238 regress0/bv/core/slice-13.smt \
239 regress0/bv/core/slice-14.smt \
240 regress0/bv/core/slice-15.smt \
241 regress0/bv/core/slice-16.smt \
242 regress0/bv/core/slice-17.smt \
243 regress0/bv/core/slice-18.smt \
244 regress0/bv/core/slice-19.smt \
245 regress0/bv/core/slice-20.smt \
246 regress0/bv/divtest_2_5.smt2 \
247 regress0/bv/divtest_2_6.smt2 \
248 regress0/bv/eager-inc-cryptominisat.smt2 \
249 regress0/bv/fuzz01.smt \
250 regress0/bv/fuzz02.delta01.smt \
251 regress0/bv/fuzz02.smt \
252 regress0/bv/fuzz03.smt \
253 regress0/bv/fuzz04.smt \
254 regress0/bv/fuzz05.smt \
255 regress0/bv/fuzz06.smt \
256 regress0/bv/fuzz07.smt \
257 regress0/bv/fuzz08.smt \
258 regress0/bv/fuzz09.smt \
259 regress0/bv/fuzz10.smt \
260 regress0/bv/fuzz11.smt \
261 regress0/bv/fuzz12.smt \
262 regress0/bv/fuzz13.smt \
263 regress0/bv/fuzz14.smt \
264 regress0/bv/fuzz16.delta01.smt \
265 regress0/bv/fuzz17.delta01.smt \
266 regress0/bv/fuzz18.delta01.smt \
267 regress0/bv/fuzz18.delta02.smt \
268 regress0/bv/fuzz18.delta03.smt \
269 regress0/bv/fuzz18.smt \
270 regress0/bv/fuzz19.delta01.smt \
271 regress0/bv/fuzz19.smt \
272 regress0/bv/fuzz20.delta01.smt \
273 regress0/bv/fuzz20.smt \
274 regress0/bv/fuzz21.delta01.smt \
275 regress0/bv/fuzz21.smt \
276 regress0/bv/fuzz22.delta01.smt \
277 regress0/bv/fuzz22.smt \
278 regress0/bv/fuzz23.delta01.smt \
279 regress0/bv/fuzz23.smt \
280 regress0/bv/fuzz24.delta01.smt \
281 regress0/bv/fuzz24.smt \
282 regress0/bv/fuzz25.delta01.smt \
283 regress0/bv/fuzz25.smt \
284 regress0/bv/fuzz26.delta01.smt \
285 regress0/bv/fuzz26.smt \
286 regress0/bv/fuzz27.delta01.smt \
287 regress0/bv/fuzz27.smt \
288 regress0/bv/fuzz28.delta01.smt \
289 regress0/bv/fuzz28.smt \
290 regress0/bv/fuzz29.delta01.smt \
291 regress0/bv/fuzz29.smt \
292 regress0/bv/fuzz30.delta01.smt \
293 regress0/bv/fuzz30.smt \
294 regress0/bv/fuzz31.delta01.smt \
295 regress0/bv/fuzz31.smt \
296 regress0/bv/fuzz32.delta01.smt \
297 regress0/bv/fuzz32.smt \
298 regress0/bv/fuzz33.delta01.smt \
299 regress0/bv/fuzz33.smt \
300 regress0/bv/fuzz34.delta01.smt \
301 regress0/bv/fuzz35.delta01.smt \
302 regress0/bv/fuzz35.smt \
303 regress0/bv/fuzz36.delta01.smt \
304 regress0/bv/fuzz36.smt \
305 regress0/bv/fuzz37.delta01.smt \
306 regress0/bv/fuzz37.smt \
307 regress0/bv/fuzz38.delta01.smt \
308 regress0/bv/fuzz39.delta01.smt \
309 regress0/bv/fuzz39.smt \
310 regress0/bv/fuzz40.delta01.smt \
311 regress0/bv/fuzz40.smt \
312 regress0/bv/fuzz41.smt \
313 regress0/bv/mul-neg-unsat.smt2 \
314 regress0/bv/mul-negpow2.smt2 \
315 regress0/bv/mult-pow2-negative.smt2 \
316 regress0/bv/sizecheck.cvc \
317 regress0/bv/smtcompbug.smt \
318 regress0/bv/test-bv_intro_pow2.smt2 \
319 regress0/bv/unsound1-reduced.smt2 \
320 regress0/chained-equality.smt2 \
321 regress0/constant-rewrite.smt \
322 regress0/cvc3.userdoc.01.cvc \
323 regress0/cvc3.userdoc.02.cvc \
324 regress0/cvc3.userdoc.03.cvc \
325 regress0/cvc3.userdoc.04.cvc \
326 regress0/cvc3.userdoc.05.cvc \
327 regress0/cvc3.userdoc.06.cvc \
328 regress0/datatypes/Test1-tup-mp.cvc \
329 regress0/datatypes/boolean-equality.cvc \
330 regress0/datatypes/boolean-terms-datatype.cvc \
331 regress0/datatypes/boolean-terms-parametric-datatype-1.cvc \
332 regress0/datatypes/boolean-terms-parametric-datatype-2.cvc \
333 regress0/datatypes/boolean-terms-record.cvc \
334 regress0/datatypes/boolean-terms-rewrite.cvc \
335 regress0/datatypes/boolean-terms-tuple.cvc \
336 regress0/datatypes/bug286.cvc \
337 regress0/datatypes/bug438.cvc \
338 regress0/datatypes/bug438b.cvc \
339 regress0/datatypes/bug597-rbt.smt2 \
340 regress0/datatypes/bug604.smt2 \
341 regress0/datatypes/bug625.smt2 \
342 regress0/datatypes/cdt-model-cade15.smt2 \
343 regress0/datatypes/cdt-non-canon-stream.smt2 \
344 regress0/datatypes/coda_simp_model.smt2 \
345 regress0/datatypes/conqueue-dt-enum-iloop.smt2 \
346 regress0/datatypes/datatype.cvc \
347 regress0/datatypes/datatype0.cvc \
348 regress0/datatypes/datatype1.cvc \
349 regress0/datatypes/datatype13.cvc \
350 regress0/datatypes/datatype2.cvc \
351 regress0/datatypes/datatype3.cvc \
352 regress0/datatypes/datatype4.cvc \
353 regress0/datatypes/data-nested-codata.smt2 \
354 regress0/datatypes/dt-2.6.smt2 \
355 regress0/datatypes/dt-match-pat-param-2.6.smt2 \
356 regress0/datatypes/dt-param-2.6.smt2 \
357 regress0/datatypes/dt-param-card4-bool-sat.smt2 \
358 regress0/datatypes/dt-sel-2.6.smt2 \
359 regress0/datatypes/empty_tuprec.cvc \
360 regress0/datatypes/example-dailler-min.smt2 \
361 regress0/datatypes/is_test.smt2 \
362 regress0/datatypes/issue1433.smt2 \
363 regress0/datatypes/jsat-2.6.smt2 \
364 regress0/datatypes/model-subterms-min.smt2 \
365 regress0/datatypes/mutually-recursive.cvc \
366 regress0/datatypes/pair-bool-bool.cvc \
367 regress0/datatypes/pair-real-bool.smt2 \
368 regress0/datatypes/rec1.cvc \
369 regress0/datatypes/rec2.cvc \
370 regress0/datatypes/rec4.cvc \
371 regress0/datatypes/rewriter.cvc \
372 regress0/datatypes/sc-cdt1.smt2 \
373 regress0/datatypes/some-boolean-tests.cvc \
374 regress0/datatypes/stream-singleton.smt2 \
375 regress0/datatypes/tenum-bug.smt2 \
376 regress0/datatypes/tuple-model.cvc \
377 regress0/datatypes/tuple-no-clash.cvc \
378 regress0/datatypes/tuple-record-bug.cvc \
379 regress0/datatypes/tuple.cvc \
380 regress0/datatypes/tuples-empty.smt2 \
381 regress0/datatypes/tuples-multitype.smt2 \
382 regress0/datatypes/typed_v10l30054.cvc \
383 regress0/datatypes/typed_v1l80005.cvc \
384 regress0/datatypes/typed_v2l30079.cvc \
385 regress0/datatypes/typed_v3l20092.cvc \
386 regress0/datatypes/typed_v5l30069.cvc \
387 regress0/datatypes/v10l40099.cvc \
388 regress0/datatypes/v2l40025.cvc \
389 regress0/datatypes/v3l60006.cvc \
390 regress0/datatypes/v5l30058.cvc \
391 regress0/datatypes/wrong-sel-simp.cvc \
392 regress0/decision/aufbv-fuzz01.smt \
393 regress0/decision/bitvec0.delta01.smt \
394 regress0/decision/bitvec0.smt \
395 regress0/decision/bitvec5.smt \
396 regress0/decision/bug347.smt \
397 regress0/decision/bug374a.smt \
398 regress0/decision/bug374b.smt2 \
399 regress0/decision/error122.delta01.smt \
400 regress0/decision/error122.smt \
401 regress0/decision/error20.delta01.smt \
402 regress0/decision/error20.smt \
403 regress0/decision/error3.delta01.smt \
404 regress0/decision/pp-regfile.delta01.smt \
405 regress0/decision/pp-regfile.delta02.smt \
406 regress0/decision/quant-ex1.smt2 \
407 regress0/decision/uflia-xs-09-16-3-4-1-5.delta03.smt \
408 regress0/decision/wchains010ue.delta02.smt \
409 regress0/declare-fun-is-match.smt2 \
410 regress0/declare-funs.smt2 \
411 regress0/distinct.smt \
412 regress0/expect/scrub.01.smt \
413 regress0/expect/scrub.02.smt \
414 regress0/expect/scrub.03.smt2 \
415 regress0/expect/scrub.04.smt2 \
416 regress0/expect/scrub.06.cvc \
417 regress0/expect/scrub.08.sy \
418 regress0/expect/scrub.09.p \
421 regress0/fmf/Arrow_Order-smtlib.778341.smt \
422 regress0/fmf/QEpres-uf.855035.smt \
423 regress0/fmf/array_card.smt2 \
424 regress0/fmf/bounded_sets.smt2 \
425 regress0/fmf/bug-041417-set-options.cvc \
426 regress0/fmf/bug652.smt2 \
427 regress0/fmf/bug782.smt2 \
428 regress0/fmf/cruanes-no-minimal-unk.smt2 \
429 regress0/fmf/fc-simple.smt2 \
430 regress0/fmf/fc-unsat-pent.smt2 \
431 regress0/fmf/fc-unsat-tot-2.smt2 \
432 regress0/fmf/fd-false.smt2 \
433 regress0/fmf/fmc_unsound_model.smt2 \
434 regress0/fmf/fmf-strange-bounds-2.smt2 \
435 regress0/fmf/forall_unit_data2.smt2 \
436 regress0/fmf/krs-sat.smt2 \
437 regress0/fmf/no-minimal-sat.smt2 \
438 regress0/fmf/quant_real_univ.cvc \
439 regress0/fmf/sat-logic.smt2 \
440 regress0/fmf/sc_bad_model_1221.smt2 \
441 regress0/fmf/sort-infer-typed-082718.smt2 \
442 regress0/fmf/syn002-si-real-int.smt2 \
443 regress0/fmf/tail_rec.smt2 \
444 regress0/fp/simple.smt2 \
445 regress0/fp/ext-rew-test.smt2 \
446 regress0/fuzz_1.smt \
447 regress0/fuzz_3.smt \
448 regress0/get-value-incremental.smt2 \
449 regress0/get-value-ints.smt2 \
450 regress0/get-value-reals-ints.smt2 \
451 regress0/get-value-reals.smt2 \
452 regress0/ho/apply-collapse-sat.smt2 \
453 regress0/ho/apply-collapse-unsat.smt2 \
454 regress0/ho/cong-full-apply.smt2 \
455 regress0/ho/cong.smt2 \
456 regress0/ho/declare-fun-variants.smt2 \
457 regress0/ho/def-fun-flatten.smt2 \
458 regress0/ho/ext-finite-unsat.smt2 \
459 regress0/ho/ext-ho-nested-lambda-model.smt2 \
460 regress0/ho/ext-ho.smt2 \
461 regress0/ho/ext-sat-partial-eval.smt2 \
462 regress0/ho/ext-sat.smt2 \
463 regress0/ho/finite-fun-ext.smt2 \
464 regress0/ho/fta0144-alpha-eq.smt2 \
465 regress0/ho/ho-match-fun-suffix.smt2 \
466 regress0/ho/ho-matching-enum.smt2 \
467 regress0/ho/ho-matching-nested-app.smt2 \
468 regress0/ho/ite-apply-eq.smt2 \
469 regress0/ho/lambda-equality-non-canon.smt2 \
470 regress0/ho/modulo-func-equality.smt2 \
471 regress0/ho/simple-matching-partial.smt2 \
472 regress0/ho/simple-matching.smt2 \
473 regress0/ho/trans.smt2 \
474 regress0/hung10_itesdk_output1.smt2 \
475 regress0/hung10_itesdk_output2.smt2 \
476 regress0/hung13sdk_output1.smt2 \
477 regress0/hung13sdk_output2.smt2 \
478 regress0/ineq_basic.smt \
479 regress0/ineq_slack.smt \
480 regress0/issue1063-overloading-dt-cons.smt2 \
481 regress0/issue1063-overloading-dt-fun.smt2 \
482 regress0/issue1063-overloading-dt-sel.smt2 \
487 regress0/ite_real_int_type.smt \
488 regress0/ite_real_valid.smt \
489 regress0/lang_opts_2_5.smt2 \
490 regress0/lang_opts_2_6_1.smt2 \
491 regress0/lemmas/clocksynchro_5clocks.main_invar.base.model.smt \
492 regress0/lemmas/fs_not_sc_seen.induction.smt \
493 regress0/lemmas/mode_cntrl.induction.smt \
494 regress0/lemmas/sc_init_frame_gap.induction.smt \
498 regress0/logops.01.cvc \
499 regress0/logops.02.cvc \
500 regress0/logops.03.cvc \
501 regress0/logops.04.cvc \
502 regress0/logops.05.cvc \
503 regress0/model-core.smt2 \
504 regress0/nl/coeff-sat.smt2 \
505 regress0/nl/ext-rew-aggr-test.smt2 \
506 regress0/nl/magnitude-wrong-1020-m.smt2 \
507 regress0/nl/mult-po.smt2 \
508 regress0/nl/nia-wrong-tl.smt2 \
509 regress0/nl/nlExtPurify-test.smt2 \
510 regress0/nl/nta/cos-sig-value.smt2 \
511 regress0/nl/nta/exp-n0.5-lb.smt2 \
512 regress0/nl/nta/exp-n0.5-ub.smt2 \
513 regress0/nl/nta/exp1-ub.smt2 \
514 regress0/nl/nta/real-pi.smt2 \
515 regress0/nl/nta/sin-sym.smt2 \
516 regress0/nl/nta/sqrt-simple.smt2 \
517 regress0/nl/nta/tan-rewrite.smt2 \
518 regress0/nl/real-as-int.smt2 \
519 regress0/nl/real-div-ufnra.smt2 \
520 regress0/nl/subs0-unsat-confirm.smt2 \
521 regress0/nl/very-easy-sat.smt2 \
522 regress0/nl/very-simple-unsat.smt2 \
523 regress0/parallel-let.smt2 \
524 regress0/parser/as.smt2 \
525 regress0/parser/constraint.smt2 \
526 regress0/parser/declarefun-emptyset-uf.smt2 \
527 regress0/parser/shadow_fun_symbol_all.smt2 \
528 regress0/parser/shadow_fun_symbol_nirat.smt2 \
529 regress0/parser/strings20.smt2 \
530 regress0/parser/strings25.smt2 \
531 regress0/parser/to_fp.smt2 \
532 regress0/precedence/and-not.cvc \
533 regress0/precedence/and-xor.cvc \
534 regress0/precedence/bool-cmp.cvc \
535 regress0/precedence/cmp-plus.cvc \
536 regress0/precedence/eq-fun.cvc \
537 regress0/precedence/iff-assoc.cvc \
538 regress0/precedence/iff-implies.cvc \
539 regress0/precedence/implies-assoc.cvc \
540 regress0/precedence/implies-iff.cvc \
541 regress0/precedence/implies-or.cvc \
542 regress0/precedence/not-and.cvc \
543 regress0/precedence/not-eq.cvc \
544 regress0/precedence/or-implies.cvc \
545 regress0/precedence/or-xor.cvc \
546 regress0/precedence/plus-mult.cvc \
547 regress0/precedence/xor-and.cvc \
548 regress0/precedence/xor-assoc.cvc \
549 regress0/precedence/xor-or.cvc \
550 regress0/preprocess/preprocess_00.cvc \
551 regress0/preprocess/preprocess_01.cvc \
552 regress0/preprocess/preprocess_02.cvc \
553 regress0/preprocess/preprocess_03.cvc \
554 regress0/preprocess/preprocess_04.cvc \
555 regress0/preprocess/preprocess_05.cvc \
556 regress0/preprocess/preprocess_06.cvc \
557 regress0/preprocess/preprocess_07.cvc \
558 regress0/preprocess/preprocess_08.cvc \
559 regress0/preprocess/preprocess_09.cvc \
560 regress0/preprocess/preprocess_10.cvc \
561 regress0/preprocess/preprocess_11.cvc \
562 regress0/preprocess/preprocess_12.cvc \
563 regress0/preprocess/preprocess_13.cvc \
564 regress0/preprocess/preprocess_14.cvc \
565 regress0/preprocess/preprocess_15.cvc \
566 regress0/print_lambda.cvc \
567 regress0/push-pop/boolean/fuzz_12.smt2 \
568 regress0/push-pop/boolean/fuzz_13.smt2 \
569 regress0/push-pop/boolean/fuzz_14.smt2 \
570 regress0/push-pop/boolean/fuzz_18.smt2 \
571 regress0/push-pop/boolean/fuzz_2.smt2 \
572 regress0/push-pop/boolean/fuzz_21.smt2 \
573 regress0/push-pop/boolean/fuzz_22.smt2 \
574 regress0/push-pop/boolean/fuzz_27.smt2 \
575 regress0/push-pop/boolean/fuzz_3.smt2 \
576 regress0/push-pop/boolean/fuzz_31.smt2 \
577 regress0/push-pop/boolean/fuzz_33.smt2 \
578 regress0/push-pop/boolean/fuzz_36.smt2 \
579 regress0/push-pop/boolean/fuzz_38.smt2 \
580 regress0/push-pop/boolean/fuzz_46.smt2 \
581 regress0/push-pop/boolean/fuzz_47.smt2 \
582 regress0/push-pop/boolean/fuzz_48.smt2 \
583 regress0/push-pop/boolean/fuzz_49.smt2 \
584 regress0/push-pop/boolean/fuzz_50.smt2 \
585 regress0/push-pop/bug1990.smt2 \
586 regress0/push-pop/bug233.cvc \
587 regress0/push-pop/bug654-dd.smt2 \
588 regress0/push-pop/bug691.smt2 \
589 regress0/push-pop/bug821-check_sat_assuming.smt2 \
590 regress0/push-pop/bug821.smt2 \
591 regress0/push-pop/inc-define.smt2 \
592 regress0/push-pop/inc-double-u.smt2 \
593 regress0/push-pop/incremental-subst-bug.cvc \
594 regress0/push-pop/issue1986.smt2 \
595 regress0/push-pop/issue2137.min.smt2 \
596 regress0/push-pop/quant-fun-proc-unfd.smt2 \
597 regress0/push-pop/simple_unsat_cores.smt2 \
598 regress0/push-pop/test.00.cvc \
599 regress0/push-pop/test.01.cvc \
600 regress0/push-pop/tiny_bug.smt2 \
601 regress0/push-pop/units.cvc \
602 regress0/quantifiers/ARI176e1.smt2 \
603 regress0/quantifiers/agg-rew-test-cf.smt2 \
604 regress0/quantifiers/agg-rew-test.smt2 \
605 regress0/quantifiers/ari056.smt2 \
606 regress0/quantifiers/bug269.smt2 \
607 regress0/quantifiers/bug290.smt2 \
608 regress0/quantifiers/bug291.smt2 \
609 regress0/quantifiers/bug749-rounding.smt2 \
610 regress0/quantifiers/cbqi-lia-dt-simp.smt2 \
611 regress0/quantifiers/cegqi-nl-simp.cvc \
612 regress0/quantifiers/cegqi-nl-sq.smt2 \
613 regress0/quantifiers/clock-10.smt2 \
614 regress0/quantifiers/clock-3.smt2 \
615 regress0/quantifiers/cond-var-elim-binary.smt2 \
616 regress0/quantifiers/delta-simp.smt2 \
617 regress0/quantifiers/double-pattern.smt2 \
618 regress0/quantifiers/ex3.smt2 \
619 regress0/quantifiers/ex6.smt2 \
620 regress0/quantifiers/floor.smt2 \
621 regress0/quantifiers/horn-ground-pre-post.smt2 \
622 regress0/quantifiers/is-even-pred.smt2 \
623 regress0/quantifiers/is-int.smt2 \
624 regress0/quantifiers/issue1805.smt2 \
625 regress0/quantifiers/issue2031-bv-var-elim.smt2 \
626 regress0/quantifiers/issue2033-macro-arith.smt2 \
627 regress0/quantifiers/issue2035.smt2 \
628 regress0/quantifiers/lra-triv-gn.smt2 \
629 regress0/quantifiers/macros-int-real.smt2 \
630 regress0/quantifiers/macros-real-arg.smt2 \
631 regress0/quantifiers/matching-lia-1arg.smt2 \
632 regress0/quantifiers/mix-complete-strat.smt2 \
633 regress0/quantifiers/mix-match.smt2 \
634 regress0/quantifiers/mix-simp.smt2 \
635 regress0/quantifiers/nested-delta.smt2 \
636 regress0/quantifiers/nested-inf.smt2 \
637 regress0/quantifiers/partial-trigger.smt2 \
638 regress0/quantifiers/pure_dt_cbqi.smt2 \
639 regress0/quantifiers/qarray-sel-over-store.smt2 \
640 regress0/quantifiers/qbv-inequality2.smt2 \
641 regress0/quantifiers/qbv-simp.smt2 \
642 regress0/quantifiers/qbv-test-invert-bvadd-neq.smt2 \
643 regress0/quantifiers/qbv-test-invert-bvand-neq.smt2 \
644 regress0/quantifiers/qbv-test-invert-bvand.smt2 \
645 regress0/quantifiers/qbv-test-invert-bvashr-0-neq.smt2 \
646 regress0/quantifiers/qbv-test-invert-bvashr-1-neq.smt2 \
647 regress0/quantifiers/qbv-test-invert-bvlshr-0-neq.smt2 \
648 regress0/quantifiers/qbv-test-invert-bvlshr-0.smt2 \
649 regress0/quantifiers/qbv-test-invert-bvlshr-1-neq.smt2 \
650 regress0/quantifiers/qbv-test-invert-bvor-neq.smt2 \
651 regress0/quantifiers/qbv-test-invert-bvor.smt2 \
652 regress0/quantifiers/qbv-test-invert-bvshl-0.smt2 \
653 regress0/quantifiers/qbv-test-invert-bvult-1.smt2 \
654 regress0/quantifiers/qbv-test-invert-bvxor-neq.smt2 \
655 regress0/quantifiers/qbv-test-invert-bvxor.smt2 \
656 regress0/quantifiers/qbv-test-invert-concat-0.smt2 \
657 regress0/quantifiers/qbv-test-invert-concat-1.smt2 \
658 regress0/quantifiers/qbv-test-invert-sign-extend.smt2 \
659 regress0/quantifiers/qcf-rel-dom-opt.smt2 \
660 regress0/quantifiers/rew-to-scala.smt2 \
661 regress0/quantifiers/simp-len.smt2 \
662 regress0/quantifiers/simp-typ-test.smt2 \
663 regress0/queries0.cvc \
664 regress0/rec-fun-const-parse-bug.smt2 \
665 regress0/rels/addr_book_0.cvc \
666 regress0/rels/atom_univ2.cvc \
667 regress0/rels/card_transpose.cvc \
668 regress0/rels/iden_0.cvc \
669 regress0/rels/iden_1.cvc \
670 regress0/rels/join-eq-u-sat.cvc \
671 regress0/rels/join-eq-u.cvc \
672 regress0/rels/joinImg_0.cvc \
673 regress0/rels/oneLoc_no_quant-int_0_1.cvc \
674 regress0/rels/rel_1tup_0.cvc \
675 regress0/rels/rel_complex_0.cvc \
676 regress0/rels/rel_complex_1.cvc \
677 regress0/rels/rel_conflict_0.cvc \
678 regress0/rels/rel_join_0.cvc \
679 regress0/rels/rel_join_0_1.cvc \
680 regress0/rels/rel_join_1.cvc \
681 regress0/rels/rel_join_1_1.cvc \
682 regress0/rels/rel_join_2.cvc \
683 regress0/rels/rel_join_2_1.cvc \
684 regress0/rels/rel_join_3.cvc \
685 regress0/rels/rel_join_3_1.cvc \
686 regress0/rels/rel_join_4.cvc \
687 regress0/rels/rel_join_5.cvc \
688 regress0/rels/rel_join_6.cvc \
689 regress0/rels/rel_join_7.cvc \
690 regress0/rels/rel_product_0.cvc \
691 regress0/rels/rel_product_0_1.cvc \
692 regress0/rels/rel_product_1.cvc \
693 regress0/rels/rel_product_1_1.cvc \
694 regress0/rels/rel_symbolic_1.cvc \
695 regress0/rels/rel_symbolic_1_1.cvc \
696 regress0/rels/rel_symbolic_2_1.cvc \
697 regress0/rels/rel_symbolic_3_1.cvc \
698 regress0/rels/rel_tc_11.cvc \
699 regress0/rels/rel_tc_2_1.cvc \
700 regress0/rels/rel_tc_3.cvc \
701 regress0/rels/rel_tc_3_1.cvc \
702 regress0/rels/rel_tc_7.cvc \
703 regress0/rels/rel_tc_8.cvc \
704 regress0/rels/rel_tp_3_1.cvc \
705 regress0/rels/rel_tp_join_0.cvc \
706 regress0/rels/rel_tp_join_1.cvc \
707 regress0/rels/rel_tp_join_2.cvc \
708 regress0/rels/rel_tp_join_3.cvc \
709 regress0/rels/rel_tp_join_eq_0.cvc \
710 regress0/rels/rel_tp_join_int_0.cvc \
711 regress0/rels/rel_tp_join_pro_0.cvc \
712 regress0/rels/rel_tp_join_var_0.cvc \
713 regress0/rels/rel_transpose_0.cvc \
714 regress0/rels/rel_transpose_1.cvc \
715 regress0/rels/rel_transpose_1_1.cvc \
716 regress0/rels/rel_transpose_3.cvc \
717 regress0/rels/rel_transpose_4.cvc \
718 regress0/rels/rel_transpose_5.cvc \
719 regress0/rels/rel_transpose_6.cvc \
720 regress0/rels/rel_transpose_7.cvc \
721 regress0/rels/relations-ops.smt2 \
722 regress0/rels/rels-sharing-simp.cvc \
723 regress0/reset-assertions.smt2 \
724 regress0/rewriterules/datatypes.smt2 \
725 regress0/rewriterules/length_trick.smt2 \
726 regress0/rewriterules/native_arrays.smt2 \
727 regress0/rewriterules/relation.smt2 \
728 regress0/rewriterules/simulate_rewriting.smt2 \
729 regress0/sep/dispose-1.smt2 \
730 regress0/sep/dup-nemp.smt2 \
731 regress0/sep/nemp.smt2 \
732 regress0/sep/nil-no-elim.smt2 \
733 regress0/sep/nspatial-simp.smt2 \
734 regress0/sep/pto-01.smt2 \
735 regress0/sep/pto-02.smt2 \
736 regress0/sep/sep-01.smt2 \
737 regress0/sep/sep-plus1.smt2 \
738 regress0/sep/sep-simp-unsat-emp.smt2 \
739 regress0/sep/skolem_emp.smt2 \
740 regress0/sep/trees-1.smt2 \
741 regress0/sep/wand-crash.smt2 \
742 regress0/sets/abt-min.smt2 \
743 regress0/sets/abt-te-exh.smt2 \
744 regress0/sets/abt-te-exh2.smt2 \
745 regress0/sets/card-2.smt2 \
746 regress0/sets/card-3sets.cvc \
747 regress0/sets/card.smt2 \
748 regress0/sets/card3-ground.smt2 \
749 regress0/sets/complement.cvc \
750 regress0/sets/complement2.cvc \
751 regress0/sets/complement3.cvc \
752 regress0/sets/cvc-sample.cvc \
753 regress0/sets/dt-simp-mem.smt2 \
754 regress0/sets/emptyset.smt2 \
755 regress0/sets/eqtest.smt2 \
756 regress0/sets/error1.smt2 \
757 regress0/sets/error2.smt2 \
758 regress0/sets/insert.smt2 \
759 regress0/sets/int-real-univ-unsat.smt2 \
760 regress0/sets/int-real-univ.smt2 \
761 regress0/sets/jan24/deepmeas0.hs.fqout.cvc4.47.smt2 \
762 regress0/sets/jan24/deepmeas0.hs.fqout.small.smt2 \
763 regress0/sets/jan27/ListConcat.hs.fqout.177minimized.smt2 \
764 regress0/sets/jan27/ListConcat.hs.fqout.cvc4.177.smt2 \
765 regress0/sets/jan28/TalkingAboutSets.hs.fqout.3577minimized.smt2 \
766 regress0/sets/jan30/UniqueZipper.hs.fqout.minimized10.smt2 \
767 regress0/sets/jan30/UniqueZipper.hs.fqout.minimized1832.smt2 \
768 regress0/sets/mar2014/sharing-preregister.smt2 \
769 regress0/sets/mar2014/small.smt2 \
770 regress0/sets/mar2014/smaller.smt2 \
771 regress0/sets/nonvar-univ.smt2 \
772 regress0/sets/pre-proc-univ.smt2 \
773 regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2 \
774 regress0/sets/sets-equal.smt2 \
775 regress0/sets/sets-inter.smt2 \
776 regress0/sets/sets-of-sets-subtypes.smt2 \
777 regress0/sets/sets-poly-int-real.smt2 \
778 regress0/sets/sets-poly-nonint.smt2 \
779 regress0/sets/sets-sample.smt2 \
780 regress0/sets/sets-sharing.smt2 \
781 regress0/sets/sets-testlemma.smt2 \
782 regress0/sets/sets-union.smt2 \
783 regress0/sets/sharing-simp.smt2 \
784 regress0/sets/union-1a-flip.smt2 \
785 regress0/sets/union-1a.smt2 \
786 regress0/sets/union-1b-flip.smt2 \
787 regress0/sets/union-1b.smt2 \
788 regress0/sets/union-2.smt2 \
789 regress0/sets/univset-simp.smt2 \
790 regress0/simple-lra.smt \
791 regress0/simple-lra.smt2 \
792 regress0/simple-rdl.smt \
793 regress0/simple-rdl.smt2 \
794 regress0/simple-uf.smt \
795 regress0/simple-uf.smt2 \
796 regress0/simple.cvc \
797 regress0/simple.smt \
798 regress0/simple2.smt \
799 regress0/simplification_bug.smt \
800 regress0/simplification_bug2.smt \
801 regress0/smallcnf.cvc \
802 regress0/smt2output.smt2 \
803 regress0/smtlib/get-unsat-assumptions.smt2 \
804 regress0/strings/bug001.smt2 \
805 regress0/strings/bug002.smt2 \
806 regress0/strings/bug612.smt2 \
807 regress0/strings/bug613.smt2 \
808 regress0/strings/code-sat-neg-one.smt2 \
809 regress0/strings/escchar.smt2 \
810 regress0/strings/escchar_25.smt2 \
811 regress0/strings/hconst-092618.smt2 \
812 regress0/strings/idof-rewrites.smt2 \
813 regress0/strings/idof-sem.smt2 \
814 regress0/strings/ilc-like.smt2 \
815 regress0/strings/indexof-sym-simp.smt2 \
816 regress0/strings/issue1189.smt2 \
817 regress0/strings/leadingzero001.smt2 \
818 regress0/strings/loop001.smt2 \
819 regress0/strings/model001.smt2 \
820 regress0/strings/norn-31.smt2 \
821 regress0/strings/norn-simp-rew.smt2 \
822 regress0/strings/repl-rewrites2.smt2 \
823 regress0/strings/rewrites-re-concat.smt2 \
824 regress0/strings/rewrites-v2.smt2 \
825 regress0/strings/std2.6.1.smt2 \
826 regress0/strings/stoi-solve.smt2 \
827 regress0/strings/str003.smt2 \
828 regress0/strings/str004.smt2 \
829 regress0/strings/str005.smt2 \
830 regress0/strings/strings-charat.cvc \
831 regress0/strings/strings-native-simple.cvc \
832 regress0/strings/strip-endpoint-itos.smt2 \
833 regress0/strings/str_unsound_ext_rew_eq.smt2 \
834 regress0/strings/substr-rewrites.smt2 \
835 regress0/strings/type001.smt2 \
836 regress0/strings/unsound-0908.smt2 \
837 regress0/sygus/General_plus10.sy \
838 regress0/sygus/aig-si.sy \
839 regress0/sygus/c100.sy \
840 regress0/sygus/ccp16.lus.sy \
841 regress0/sygus/check-generic-red.sy \
842 regress0/sygus/const-var-test.sy \
843 regress0/sygus/dt-no-syntax.sy \
844 regress0/sygus/hd-05-d1-prog-nogrammar.sy \
845 regress0/sygus/inv-different-var-order.sy \
846 regress0/sygus/let-ringer.sy \
847 regress0/sygus/let-simp.sy \
848 regress0/sygus/no-syntax-test-bool.sy \
849 regress0/sygus/no-syntax-test.sy \
850 regress0/sygus/parity-AIG-d0.sy \
851 regress0/sygus/parse-bv-let.sy \
852 regress0/sygus/real-si-all.sy \
853 regress0/sygus/strings-unconstrained.sy \
854 regress0/sygus/uminus_one.sy \
855 regress0/test11.cvc \
857 regress0/tptp/ARI086$(equals)1.p \
858 regress0/tptp/DAT001$(equals)1.p \
859 regress0/tptp/KRS018+1.p \
860 regress0/tptp/KRS063+1.p \
861 regress0/tptp/MGT019+2.p \
862 regress0/tptp/MGT041-2.p \
863 regress0/tptp/PUZ131_1.p \
864 regress0/tptp/SYN000$(equals)2.p \
865 regress0/tptp/SYN000+1.p \
866 regress0/tptp/SYN000+2.p \
867 regress0/tptp/SYN000-1.p \
868 regress0/tptp/SYN000-2.p \
869 regress0/tptp/SYN000_1.p \
870 regress0/tptp/SYN000_2.p \
871 regress0/tptp/SYN075-1.p \
872 regress0/tptp/tff0-arith.p \
873 regress0/tptp/tff0.p \
874 regress0/tptp/tptp_parser.p \
875 regress0/tptp/tptp_parser10.p \
876 regress0/tptp/tptp_parser2.p \
877 regress0/tptp/tptp_parser3.p \
878 regress0/tptp/tptp_parser4.p \
879 regress0/tptp/tptp_parser5.p \
880 regress0/tptp/tptp_parser6.p \
881 regress0/tptp/tptp_parser7.p \
882 regress0/tptp/tptp_parser8.p \
883 regress0/tptp/tptp_parser9.p \
884 regress0/uf/NEQ016_size5_reduced2a.smt \
885 regress0/uf/NEQ016_size5_reduced2b.smt \
886 regress0/uf/bool-pred-nested.smt2 \
887 regress0/uf/ccredesign-fuzz.smt \
888 regress0/uf/cnf-and-neg.smt2 \
889 regress0/uf/cnf-iff-base.smt2 \
890 regress0/uf/cnf-iff.smt2 \
891 regress0/uf/cnf-ite.smt2 \
892 regress0/uf/cnf_abc.smt2 \
893 regress0/uf/dead_dnd002.smt \
894 regress0/uf/eq_diamond1.smt \
895 regress0/uf/eq_diamond14.reduced.smt \
896 regress0/uf/eq_diamond14.reduced2.smt \
897 regress0/uf/eq_diamond23.smt \
898 regress0/uf/euf_simp01.smt \
899 regress0/uf/euf_simp02.smt \
900 regress0/uf/euf_simp03.smt \
901 regress0/uf/euf_simp04.smt \
902 regress0/uf/euf_simp05.smt \
903 regress0/uf/euf_simp06.smt \
904 regress0/uf/euf_simp08.smt \
905 regress0/uf/euf_simp09.smt \
906 regress0/uf/euf_simp10.smt \
907 regress0/uf/euf_simp11.smt \
908 regress0/uf/euf_simp12.smt \
909 regress0/uf/euf_simp13.smt \
910 regress0/uf/iso_brn001.smt \
911 regress0/uf/pred.smt \
912 regress0/uf/simple.01.cvc \
913 regress0/uf/simple.02.cvc \
914 regress0/uf/simple.03.cvc \
915 regress0/uf/simple.04.cvc \
916 regress0/uf20-03.cvc \
917 regress0/uflia/check01.smt2 \
918 regress0/uflia/check02.smt2 \
919 regress0/uflia/check03.smt2 \
920 regress0/uflia/check04.smt2 \
921 regress0/uflia/error0.delta01.smt \
922 regress0/uflia/error1.smt \
923 regress0/uflia/error30.smt \
924 regress0/uflia/stalmark_e7_27_e7_31.ec.minimized.smt2 \
925 regress0/uflia/tiny.smt2 \
926 regress0/uflia/xs-09-16-3-4-1-5.delta01.smt \
927 regress0/uflia/xs-09-16-3-4-1-5.delta02.smt \
928 regress0/uflia/xs-09-16-3-4-1-5.delta03.smt \
929 regress0/uflia/xs-09-16-3-4-1-5.delta04.smt \
930 regress0/uflra/bug293.cvc \
931 regress0/uflra/bug449.smt \
932 regress0/uflra/constants0.smt \
933 regress0/uflra/fuzz01.smt \
934 regress0/uflra/incorrect1.delta01.smt \
935 regress0/uflra/incorrect1.delta02.smt \
936 regress0/uflra/neq-deltacomp.smt \
937 regress0/uflra/pb_real_10_0100_10_10.smt \
938 regress0/uflra/pb_real_10_0100_10_11.smt \
939 regress0/uflra/pb_real_10_0100_10_15.smt \
940 regress0/uflra/pb_real_10_0100_10_16.smt \
941 regress0/uflra/pb_real_10_0100_10_19.smt \
942 regress0/uflra/pb_real_10_0200_10_22.smt \
943 regress0/uflra/pb_real_10_0200_10_26.smt \
944 regress0/uflra/pb_real_10_0200_10_29.smt \
945 regress0/uflra/simple.01.cvc \
946 regress0/uflra/simple.02.cvc \
947 regress0/uflra/simple.03.cvc \
948 regress0/uflra/simple.04.cvc \
949 regress0/unconstrained/arith.smt2 \
950 regress0/unconstrained/arith3.smt2 \
951 regress0/unconstrained/arith4.smt2 \
952 regress0/unconstrained/arith5.smt2 \
953 regress0/unconstrained/arith6.smt2 \
954 regress0/unconstrained/array1.smt2 \
955 regress0/unconstrained/bvbool.smt2 \
956 regress0/unconstrained/bvbool2.smt2 \
957 regress0/unconstrained/bvbool3.smt2 \
958 regress0/unconstrained/bvcmp.smt2 \
959 regress0/unconstrained/bvconcat2.smt2 \
960 regress0/unconstrained/bvext.smt2 \
961 regress0/unconstrained/bvite.smt2 \
962 regress0/unconstrained/bvmul.smt2 \
963 regress0/unconstrained/bvmul2.smt2 \
964 regress0/unconstrained/bvmul3.smt2 \
965 regress0/unconstrained/bvnot.smt2 \
966 regress0/unconstrained/bvsle.smt2 \
967 regress0/unconstrained/bvsle2.smt2 \
968 regress0/unconstrained/bvsle3.smt2 \
969 regress0/unconstrained/bvsle4.smt2 \
970 regress0/unconstrained/bvsle5.smt2 \
971 regress0/unconstrained/bvslt.smt2 \
972 regress0/unconstrained/bvslt2.smt2 \
973 regress0/unconstrained/bvslt3.smt2 \
974 regress0/unconstrained/bvslt4.smt2 \
975 regress0/unconstrained/bvslt5.smt2 \
976 regress0/unconstrained/bvule.smt2 \
977 regress0/unconstrained/bvule2.smt2 \
978 regress0/unconstrained/bvule3.smt2 \
979 regress0/unconstrained/bvule4.smt2 \
980 regress0/unconstrained/bvule5.smt2 \
981 regress0/unconstrained/bvult.smt2 \
982 regress0/unconstrained/bvult2.smt2 \
983 regress0/unconstrained/bvult3.smt2 \
984 regress0/unconstrained/bvult4.smt2 \
985 regress0/unconstrained/bvult5.smt2 \
986 regress0/unconstrained/geq.smt2 \
987 regress0/unconstrained/gt.smt2 \
988 regress0/unconstrained/ite.smt2 \
989 regress0/unconstrained/leq.smt2 \
990 regress0/unconstrained/lt.smt2 \
991 regress0/unconstrained/mult1.smt2 \
992 regress0/unconstrained/uf1.smt2 \
993 regress0/unconstrained/xor.smt2 \
994 regress0/wiki.01.cvc \
995 regress0/wiki.02.cvc \
996 regress0/wiki.03.cvc \
997 regress0/wiki.04.cvc \
998 regress0/wiki.05.cvc \
999 regress0/wiki.06.cvc \
1000 regress0/wiki.07.cvc \
1001 regress0/wiki.08.cvc \
1002 regress0/wiki.09.cvc \
1003 regress0/wiki.10.cvc \
1004 regress0/wiki.11.cvc \
1005 regress0/wiki.12.cvc \
1006 regress0/wiki.13.cvc \
1007 regress0/wiki.14.cvc \
1008 regress0/wiki.15.cvc \
1009 regress0/wiki.16.cvc \
1010 regress0/wiki.17.cvc \
1011 regress0/wiki.18.cvc \
1012 regress0/wiki.19.cvc \
1013 regress0/wiki.20.cvc \
1014 regress0/wiki.21.cvc
1017 regress1/arith/arith-int-004.cvc \
1018 regress1/arith/arith-int-011.cvc \
1019 regress1/arith/arith-int-012.cvc \
1020 regress1/arith/arith-int-013.cvc \
1021 regress1/arith/arith-int-022.cvc \
1022 regress1/arith/arith-int-024.cvc \
1023 regress1/arith/arith-int-047.cvc \
1024 regress1/arith/arith-int-048.cvc \
1025 regress1/arith/arith-int-050.cvc \
1026 regress1/arith/arith-int-084.cvc \
1027 regress1/arith/arith-int-085.cvc \
1028 regress1/arith/arith-int-097.cvc \
1029 regress1/arith/bug547.1.smt2 \
1030 regress1/arith/bug716.0.smt2 \
1031 regress1/arith/bug716.1.cvc \
1032 regress1/arith/div.03.smt2 \
1033 regress1/arith/div.06.smt2 \
1034 regress1/arith/div.08.smt2 \
1035 regress1/arith/div.09.smt2 \
1036 regress1/arith/miplib3.cvc \
1037 regress1/arith/mod.02.smt2 \
1038 regress1/arith/mod.03.smt2 \
1039 regress1/arith/mult.02.smt2 \
1040 regress1/arith/pbrewrites-test.smt2 \
1041 regress1/arith/problem__003.smt2 \
1042 regress1/arith/real2int-test.smt2 \
1043 regress1/arrayinuf_error.smt2 \
1044 regress1/aufbv/bug580.smt2 \
1045 regress1/aufbv/fuzz10.smt \
1046 regress1/auflia/bug330.smt2 \
1047 regress1/boolean-terms-kernel2.smt2 \
1048 regress1/boolean.cvc \
1049 regress1/bug216.smt2 \
1050 regress1/bug296.smt2 \
1051 regress1/bug425.cvc \
1052 regress1/bug507.smt2 \
1053 regress1/bug512.smt2 \
1054 regress1/bug516.smt2 \
1055 regress1/bug519.smt2 \
1056 regress1/bug520.smt2 \
1057 regress1/bug521.smt2 \
1058 regress1/bug543.smt2 \
1059 regress1/bug567.smt2 \
1060 regress1/bug593.smt2 \
1061 regress1/bug681.smt2 \
1062 regress1/bug694-Unapply1.scala-0.smt2 \
1063 regress1/bug800.smt2 \
1064 regress1/bv/bug787.smt2 \
1065 regress1/bv/bug_extract_mult_leading_bit.smt2 \
1066 regress1/bv/bv-int-collapse2-sat.smt2 \
1067 regress1/bv/bv-proof00.smt \
1068 regress1/bv/bv2nat-ground.smt2 \
1069 regress1/bv/bv2nat-simp-range-sat.smt2 \
1070 regress1/bv/bv2nat-types.smt2 \
1071 regress1/bv/cmu-rdk-3.smt2 \
1072 regress1/bv/decision-weight00.smt2 \
1073 regress1/bv/divtest.smt2 \
1074 regress1/bv/fuzz34.smt \
1075 regress1/bv/fuzz38.smt \
1076 regress1/bv/test-bv-abstraction.smt2 \
1077 regress1/bv/unsound1.smt2 \
1078 regress1/bvdiv2.smt2 \
1079 regress1/constarr3.cvc \
1080 regress1/constarr3.smt2 \
1081 regress1/datatypes/acyclicity-sr-ground096.smt2 \
1082 regress1/datatypes/dt-color-2.6.smt2 \
1083 regress1/datatypes/dt-param-card4-unsat.smt2 \
1084 regress1/datatypes/error.cvc \
1085 regress1/datatypes/manos-model.smt2 \
1086 regress1/decision/error3.smt \
1087 regress1/decision/quant-Arrays_Q1-noinfer.smt2 \
1088 regress1/decision/quant-symmetric_unsat_7.smt2 \
1089 regress1/error.cvc \
1090 regress1/errorcrash.smt2 \
1091 regress1/fmf-fun-dbu.smt2 \
1092 regress1/fmf/ALG008-1.smt2 \
1093 regress1/fmf/Hoare-z3.931718.smt \
1094 regress1/fmf/LeftistHeap.scala-8-ncm.smt2 \
1095 regress1/fmf/PUZ001+1.smt2 \
1096 regress1/fmf/agree466.smt2 \
1097 regress1/fmf/agree467.smt2 \
1098 regress1/fmf/alg202+1.smt2 \
1099 regress1/fmf/am-bad-model.cvc \
1100 regress1/fmf/bound-int-alt.smt2 \
1101 regress1/fmf/bug0909.smt2 \
1102 regress1/fmf/bug651.smt2 \
1103 regress1/fmf/bug723-irrelevant-funs.smt2 \
1104 regress1/fmf/bug764.smt2 \
1105 regress1/fmf/cons-sets-bounds.smt2 \
1106 regress1/fmf/constr-ground-to.smt2 \
1107 regress1/fmf/datatypes-ufinite-nested.smt2 \
1108 regress1/fmf/datatypes-ufinite.smt2 \
1109 regress1/fmf/dt-proper-model.smt2 \
1110 regress1/fmf/fc-pigeonhole19.smt2 \
1111 regress1/fmf/fib-core.smt2 \
1112 regress1/fmf/fmf-bound-2dim.smt2 \
1113 regress1/fmf/fmf-bound-int.smt2 \
1114 regress1/fmf/fmf-fun-divisor-pp.smt2 \
1115 regress1/fmf/fmf-fun-no-elim-ext-arith.smt2 \
1116 regress1/fmf/fmf-fun-no-elim-ext-arith2.smt2 \
1117 regress1/fmf/fmf-strange-bounds.smt2 \
1118 regress1/fmf/forall_unit_data.smt2 \
1119 regress1/fmf/fore19-exp2-core.smt2 \
1120 regress1/fmf/german169.smt2 \
1121 regress1/fmf/german73.smt2 \
1122 regress1/fmf/issue2034-preinit.smt2 \
1123 regress1/fmf/issue916-fmf-or.smt2 \
1124 regress1/fmf/jasmin-cdt-crash.smt2 \
1125 regress1/fmf/ko-bound-set.cvc \
1126 regress1/fmf/loopy_coda.smt2 \
1127 regress1/fmf/lst-no-self-rev-exp.smt2 \
1128 regress1/fmf/memory_model-R_cpp-dd.cvc \
1129 regress1/fmf/nlp042+1.smt2 \
1130 regress1/fmf/nun-0208-to.smt2 \
1131 regress1/fmf/pow2-bool.smt2 \
1132 regress1/fmf/radu-quant-set.smt2 \
1133 regress1/fmf/refcount24.cvc.smt2 \
1134 regress1/fmf/sc-crash-052316.smt2 \
1135 regress1/fmf/sort-inf-int-real.smt2 \
1136 regress1/fmf/sort-inf-int.smt2 \
1137 regress1/fmf/with-ind-104-core.smt2 \
1138 regress1/gensys_brn001.smt2 \
1139 regress1/ho/auth0068.smt2 \
1140 regress1/ho/fta0210.smt2 \
1141 regress1/ho/fta0409.smt2 \
1142 regress1/ho/ho-exponential-model.smt2 \
1143 regress1/ho/ho-matching-enum-2.smt2 \
1144 regress1/ho/ho-std-fmf.smt2 \
1145 regress1/ho/hoa0008.smt2 \
1146 regress1/ho/match-middle.smt2 \
1147 regress1/hole6.cvc \
1148 regress1/ite5.smt2 \
1149 regress1/lemmas/clocksynchro_5clocks.main_invar.base.smt \
1150 regress1/lemmas/pursuit-safety-8.smt \
1151 regress1/lemmas/simple_startup_9nodes.abstract.base.smt \
1152 regress1/nl/NAVIGATION2.smt2 \
1153 regress1/nl/approx-sqrt-unsat.smt2 \
1154 regress1/nl/approx-sqrt.smt2 \
1155 regress1/nl/arctan2-expdef.smt2 \
1156 regress1/nl/arrowsmith-050317.smt2 \
1157 regress1/nl/bad-050217.smt2 \
1158 regress1/nl/bug698.smt2 \
1159 regress1/nl/coeff-unsat-base.smt2 \
1160 regress1/nl/coeff-unsat.smt2 \
1161 regress1/nl/combine.smt2 \
1162 regress1/nl/cos-bound.smt2 \
1163 regress1/nl/cos1-tc.smt2 \
1164 regress1/nl/disj-eval.smt2 \
1165 regress1/nl/dist-big.smt2 \
1166 regress1/nl/div-mod-partial.smt2 \
1167 regress1/nl/dumortier_llibre_artes_ex_5_13.transcendental.k2.smt2 \
1168 regress1/nl/exp-4.5-lt.smt2 \
1169 regress1/nl/exp-approx.smt2 \
1170 regress1/nl/exp1-lb.smt2 \
1171 regress1/nl/exp_monotone.smt2 \
1172 regress1/nl/factor_agg_s.smt2 \
1173 regress1/nl/metitarski-1025.smt2 \
1174 regress1/nl/metitarski-3-4.smt2 \
1175 regress1/nl/metitarski_3_4_2e.smt2 \
1176 regress1/nl/mirko-050417.smt2 \
1177 regress1/nl/nl-eq-infer.smt2 \
1178 regress1/nl/nl-help-unsat-quant.smt2 \
1179 regress1/nl/nl-unk-quant.smt2 \
1180 regress1/nl/nl_uf_lalt.smt2 \
1181 regress1/nl/ones.smt2 \
1182 regress1/nl/poly-1025.smt2 \
1183 regress1/nl/quant-nl.smt2 \
1184 regress1/nl/red-exp.smt2 \
1185 regress1/nl/rewriting-sums.smt2 \
1186 regress1/nl/shifting.smt2 \
1187 regress1/nl/shifting2.smt2 \
1188 regress1/nl/simple-mono-unsat.smt2 \
1189 regress1/nl/simple-mono.smt2 \
1190 regress1/nl/sin-compare-across-phase.smt2 \
1191 regress1/nl/sin-compare.smt2 \
1192 regress1/nl/sin-init-tangents.smt2 \
1193 regress1/nl/sin-sign.smt2 \
1194 regress1/nl/sin-sym2.smt2 \
1195 regress1/nl/sin1-deq-sat.smt2 \
1196 regress1/nl/sin1-lb.smt2 \
1197 regress1/nl/sin1-sat.smt2 \
1198 regress1/nl/sin1-ub.smt2 \
1199 regress1/nl/sin2-lb.smt2 \
1200 regress1/nl/sin2-ub.smt2 \
1201 regress1/nl/solve-eq-small-qf-nra.smt2 \
1202 regress1/nl/sqrt-problem-1.smt2 \
1203 regress1/nl/sugar-ident-2.smt2 \
1204 regress1/nl/sugar-ident-3.smt2 \
1205 regress1/nl/sugar-ident.smt2 \
1206 regress1/nl/tan-rewrite2.smt2 \
1207 regress1/nl/zero-subset.smt2 \
1208 regress1/non-fatal-errors.smt2 \
1209 regress1/parsing_ringer.cvc \
1210 regress1/proof00.smt2 \
1211 regress1/push-pop/arith_lra_01.smt2 \
1212 regress1/push-pop/arith_lra_02.smt2 \
1213 regress1/push-pop/bug-fmf-fun-skolem.smt2 \
1214 regress1/push-pop/bug216.smt2 \
1215 regress1/push-pop/bug326.smt2 \
1216 regress1/push-pop/fuzz_1.smt2 \
1217 regress1/push-pop/fuzz_10.smt2 \
1218 regress1/push-pop/fuzz_11.smt2 \
1219 regress1/push-pop/fuzz_15.smt2 \
1220 regress1/push-pop/fuzz_16.smt2 \
1221 regress1/push-pop/fuzz_19.smt2 \
1222 regress1/push-pop/fuzz_1_to_52_merged.smt2 \
1223 regress1/push-pop/fuzz_20.smt2 \
1224 regress1/push-pop/fuzz_23.smt2 \
1225 regress1/push-pop/fuzz_24.smt2 \
1226 regress1/push-pop/fuzz_25.smt2 \
1227 regress1/push-pop/fuzz_26.smt2 \
1228 regress1/push-pop/fuzz_28.smt2 \
1229 regress1/push-pop/fuzz_29.smt2 \
1230 regress1/push-pop/fuzz_30.smt2 \
1231 regress1/push-pop/fuzz_32.smt2 \
1232 regress1/push-pop/fuzz_34.smt2 \
1233 regress1/push-pop/fuzz_35.smt2 \
1234 regress1/push-pop/fuzz_37.smt2 \
1235 regress1/push-pop/fuzz_39.smt2 \
1236 regress1/push-pop/fuzz_3_1.smt2 \
1237 regress1/push-pop/fuzz_3_10.smt2 \
1238 regress1/push-pop/fuzz_3_11.smt2 \
1239 regress1/push-pop/fuzz_3_12.smt2 \
1240 regress1/push-pop/fuzz_3_13.smt2 \
1241 regress1/push-pop/fuzz_3_14.smt2 \
1242 regress1/push-pop/fuzz_3_15.smt2 \
1243 regress1/push-pop/fuzz_3_2.smt2 \
1244 regress1/push-pop/fuzz_3_3.smt2 \
1245 regress1/push-pop/fuzz_3_4.smt2 \
1246 regress1/push-pop/fuzz_3_5.smt2 \
1247 regress1/push-pop/fuzz_3_6.smt2 \
1248 regress1/push-pop/fuzz_3_7.smt2 \
1249 regress1/push-pop/fuzz_3_8.smt2 \
1250 regress1/push-pop/fuzz_3_9.smt2 \
1251 regress1/push-pop/fuzz_4.smt2 \
1252 regress1/push-pop/fuzz_40.smt2 \
1253 regress1/push-pop/fuzz_41.smt2 \
1254 regress1/push-pop/fuzz_42.smt2 \
1255 regress1/push-pop/fuzz_43.smt2 \
1256 regress1/push-pop/fuzz_44.smt2 \
1257 regress1/push-pop/fuzz_45.smt2 \
1258 regress1/push-pop/fuzz_5.smt2 \
1259 regress1/push-pop/fuzz_51.smt2 \
1260 regress1/push-pop/fuzz_52.smt2 \
1261 regress1/push-pop/fuzz_5_1.smt2 \
1262 regress1/push-pop/fuzz_5_2.smt2 \
1263 regress1/push-pop/fuzz_5_3.smt2 \
1264 regress1/push-pop/fuzz_5_4.smt2 \
1265 regress1/push-pop/fuzz_5_5.smt2 \
1266 regress1/push-pop/fuzz_5_6.smt2 \
1267 regress1/push-pop/fuzz_6.smt2 \
1268 regress1/push-pop/fuzz_7.smt2 \
1269 regress1/push-pop/fuzz_8.smt2 \
1270 regress1/push-pop/fuzz_9.smt2 \
1271 regress1/push-pop/quant-fun-proc-unmacro.smt2 \
1272 regress1/push-pop/quant-fun-proc.smt2 \
1273 regress1/quantifiers/006-cbqi-ite.smt2 \
1274 regress1/quantifiers/015-psyco-pp.smt2 \
1275 regress1/quantifiers/AdditiveMethods_OwnedResults.Mz.smt2 \
1276 regress1/quantifiers/Arrays_Q1-noinfer.smt2 \
1277 regress1/quantifiers/NUM878.smt2 \
1278 regress1/quantifiers/RND-small.smt2 \
1279 regress1/quantifiers/RNDPRE_4_1-dd-nqe.smt2 \
1280 regress1/quantifiers/RND_4_1-existing-inst.smt2 \
1281 regress1/quantifiers/RND_4_16.smt2 \
1282 regress1/quantifiers/anti-sk-simp.smt2 \
1283 regress1/quantifiers/ari118-bv-2occ-x.smt2 \
1284 regress1/quantifiers/arith-rec-fun.smt2 \
1285 regress1/quantifiers/arith-snorm.smt2 \
1286 regress1/quantifiers/array-unsat-simp3.smt2 \
1287 regress1/quantifiers/bi-artm-s.smt2 \
1288 regress1/quantifiers/bignum_quant.smt2 \
1289 regress1/quantifiers/bug802.smt2 \
1290 regress1/quantifiers/bug822.smt2 \
1291 regress1/quantifiers/bug_743.smt2 \
1292 regress1/quantifiers/burns13.smt2 \
1293 regress1/quantifiers/burns4.smt2 \
1294 regress1/quantifiers/cbqi-sdlx-fixpoint-3-dd.smt2 \
1295 regress1/quantifiers/cdt-0208-to.smt2 \
1296 regress1/quantifiers/const.cvc \
1297 regress1/quantifiers/constfunc.cvc \
1298 regress1/quantifiers/dump-inst.smt2 \
1299 regress1/quantifiers/dump-inst-i.smt2 \
1300 regress1/quantifiers/dump-inst-proof.smt2 \
1301 regress1/quantifiers/ext-ex-deq-trigger.smt2 \
1302 regress1/quantifiers/extract-nproc.smt2 \
1303 regress1/quantifiers/florian-case-ax.smt2 \
1304 regress1/quantifiers/fp-cegqi-unsat.smt2 \
1305 regress1/quantifiers/gauss_init_0030.fof.smt2 \
1306 regress1/quantifiers/horn-simple.smt2 \
1307 regress1/quantifiers/infer-arith-trigger-eq.smt2 \
1308 regress1/quantifiers/inst-max-level-segf.smt2 \
1309 regress1/quantifiers/inst-prop-simp.smt2 \
1310 regress1/quantifiers/intersection-example-onelane.proof-node22337.smt2 \
1311 regress1/quantifiers/is-even.smt2 \
1312 regress1/quantifiers/isaplanner-goal20.smt2 \
1313 regress1/quantifiers/javafe.ast.StmtVec.009.smt2 \
1314 regress1/quantifiers/lra-vts-inf.smt2 \
1315 regress1/quantifiers/mix-coeff.smt2 \
1316 regress1/quantifiers/model_6_1_bv.smt2 \
1317 regress1/quantifiers/mutualrec2.cvc \
1318 regress1/quantifiers/nested9_true-unreach-call.i_575.smt2 \
1319 regress1/quantifiers/nl-pow-trick.smt2 \
1320 regress1/quantifiers/nra-interleave-inst.smt2 \
1321 regress1/quantifiers/opisavailable-12.smt2 \
1322 regress1/quantifiers/parametric-lists.smt2 \
1323 regress1/quantifiers/psyco-001-bv.smt2 \
1324 regress1/quantifiers/psyco-107-bv.smt2 \
1325 regress1/quantifiers/psyco-196.smt2 \
1326 regress1/quantifiers/qbv-disequality3.smt2 \
1327 regress1/quantifiers/qbv-simple-2vars-vo.smt2 \
1328 regress1/quantifiers/qbv-subcall.smt2 \
1329 regress1/quantifiers/qbv-test-invert-bvashr-0.smt2 \
1330 regress1/quantifiers/qbv-test-invert-bvashr-1.smt2 \
1331 regress1/quantifiers/qbv-test-invert-bvcomp.smt2 \
1332 regress1/quantifiers/qbv-test-invert-bvlshr-1.smt2 \
1333 regress1/quantifiers/qbv-test-invert-bvmul-neq.smt2 \
1334 regress1/quantifiers/qbv-test-invert-bvmul.smt2 \
1335 regress1/quantifiers/qbv-test-invert-bvudiv-0-neq.smt2 \
1336 regress1/quantifiers/qbv-test-invert-bvudiv-0.smt2 \
1337 regress1/quantifiers/qbv-test-invert-bvudiv-1-neq.smt2 \
1338 regress1/quantifiers/qbv-test-invert-bvudiv-1.smt2 \
1339 regress1/quantifiers/qbv-test-invert-bvurem-1-neq.smt2 \
1340 regress1/quantifiers/qbv-test-invert-bvurem-1.smt2 \
1341 regress1/quantifiers/qbv-test-urem-rewrite.smt2 \
1342 regress1/quantifiers/qcft-javafe.filespace.TreeWalker.006.smt2 \
1343 regress1/quantifiers/qcft-smtlib3dbc51.smt2 \
1344 regress1/quantifiers/qe.smt2 \
1345 regress1/quantifiers/qe-partial.smt2 \
1346 regress1/quantifiers/quant-wf-int-ind.smt2 \
1347 regress1/quantifiers/quaternion_ds1_symm_0428.fof.smt2 \
1348 regress1/quantifiers/recfact.cvc \
1349 regress1/quantifiers/repair-const-nterm.smt2 \
1350 regress1/quantifiers/rew-to-0211-dd.smt2 \
1351 regress1/quantifiers/ricart-agrawala6.smt2 \
1352 regress1/quantifiers/set-choice-koikonomou.cvc \
1353 regress1/quantifiers/set8.smt2 \
1354 regress1/quantifiers/small-pipeline-fixpoint-3.smt2 \
1355 regress1/quantifiers/smtcomp-qbv-053118.smt2 \
1356 regress1/quantifiers/smtlib384a03.smt2 \
1357 regress1/quantifiers/smtlib46f14a.smt2 \
1358 regress1/quantifiers/smtlibe99bbe.smt2 \
1359 regress1/quantifiers/smtlibf957ea.smt2 \
1360 regress1/quantifiers/stream-x2014-09-18-unsat.smt2 \
1361 regress1/quantifiers/sygus-infer-nested.smt2 \
1362 regress1/quantifiers/symmetric_unsat_7.smt2 \
1363 regress1/quantifiers/z3.620661-no-fv-trigger.smt2 \
1364 regress1/rels/addr_book_1.cvc \
1365 regress1/rels/addr_book_1_1.cvc \
1366 regress1/rels/bv1-unit.cvc \
1367 regress1/rels/bv1-unitb.cvc \
1368 regress1/rels/bv1.cvc \
1369 regress1/rels/bv1p-sat.cvc \
1370 regress1/rels/bv1p.cvc \
1371 regress1/rels/bv2.cvc \
1372 regress1/rels/iden_1_1.cvc \
1373 regress1/rels/join-eq-structure-and.cvc \
1374 regress1/rels/join-eq-structure.cvc \
1375 regress1/rels/join-eq-structure_0_1.cvc \
1376 regress1/rels/joinImg_0_1.cvc \
1377 regress1/rels/joinImg_0_2.cvc \
1378 regress1/rels/joinImg_1.cvc \
1379 regress1/rels/joinImg_1_1.cvc \
1380 regress1/rels/joinImg_2.cvc \
1381 regress1/rels/joinImg_2_1.cvc \
1382 regress1/rels/prod-mod-eq.cvc \
1383 regress1/rels/prod-mod-eq2.cvc \
1384 regress1/rels/rel_complex_3.cvc \
1385 regress1/rels/rel_complex_4.cvc \
1386 regress1/rels/rel_complex_5.cvc \
1387 regress1/rels/rel_mix_0_1.cvc \
1388 regress1/rels/rel_pressure_0.cvc \
1389 regress1/rels/rel_tc_10_1.cvc \
1390 regress1/rels/rel_tc_4.cvc \
1391 regress1/rels/rel_tc_4_1.cvc \
1392 regress1/rels/rel_tc_5_1.cvc \
1393 regress1/rels/rel_tc_6.cvc \
1394 regress1/rels/rel_tc_9_1.cvc \
1395 regress1/rels/rel_tp_2.cvc \
1396 regress1/rels/rel_tp_join_2_1.cvc \
1397 regress1/rels/set-strat.cvc \
1398 regress1/rels/strat.cvc \
1399 regress1/rels/strat_0_1.cvc \
1400 regress1/rewriterules/datatypes_sat.smt2 \
1401 regress1/rewriterules/length_gen.smt2 \
1402 regress1/rewriterules/length_gen_020.smt2 \
1403 regress1/rewriterules/length_gen_020_sat.smt2 \
1404 regress1/rewriterules/length_gen_040.smt2 \
1405 regress1/rewriterules/length_gen_040_lemma.smt2 \
1406 regress1/rewriterules/length_gen_040_lemma_trigger.smt2 \
1407 regress1/rewriterules/reachability_back_to_the_future.smt2 \
1408 regress1/rewriterules/read5.smt2 \
1409 regress1/rr-verify/bool-crci.sy \
1410 regress1/rr-verify/bv-term-32.sy \
1411 regress1/rr-verify/bv-term.sy \
1412 regress1/rr-verify/regex.sy \
1413 regress1/rr-verify/string-term.sy \
1414 regress1/sep/chain-int.smt2 \
1415 regress1/sep/crash1220.smt2 \
1416 regress1/sep/dispose-list-4-init.smt2 \
1417 regress1/sep/emp2-quant-unsat.smt2 \
1418 regress1/sep/finite-witness-sat.smt2 \
1419 regress1/sep/fmf-nemp-2.smt2 \
1420 regress1/sep/loop-1220.smt2 \
1421 regress1/sep/pto-04.smt2 \
1422 regress1/sep/quant_wand.smt2 \
1423 regress1/sep/sep-02.smt2 \
1424 regress1/sep/sep-03.smt2 \
1425 regress1/sep/sep-find2.smt2 \
1426 regress1/sep/sep-fmf-priority.smt2 \
1427 regress1/sep/sep-neg-1refine.smt2 \
1428 regress1/sep/sep-neg-nstrict.smt2 \
1429 regress1/sep/sep-neg-nstrict2.smt2 \
1430 regress1/sep/sep-neg-simple.smt2 \
1431 regress1/sep/sep-neg-swap.smt2 \
1432 regress1/sep/sep-nterm-again.smt2 \
1433 regress1/sep/sep-nterm-val-model.smt2 \
1434 regress1/sep/sep-simp-unc.smt2 \
1435 regress1/sep/simple-neg-sat.smt2 \
1436 regress1/sep/sl-standard.smt2 \
1437 regress1/sep/split-find-unsat-w-emp.smt2 \
1438 regress1/sep/split-find-unsat.smt2 \
1439 regress1/sep/wand-0526-sat.smt2 \
1440 regress1/sep/wand-false.smt2 \
1441 regress1/sep/wand-nterm-simp.smt2 \
1442 regress1/sep/wand-nterm-simp2.smt2 \
1443 regress1/sep/wand-simp-sat.smt2 \
1444 regress1/sep/wand-simp-sat2.smt2 \
1445 regress1/sep/wand-simp-unsat.smt2 \
1446 regress1/sets/ListElem.hs.fqout.cvc4.38.smt2 \
1447 regress1/sets/ListElts.hs.fqout.cvc4.317.smt2 \
1448 regress1/sets/TalkingAboutSets.hs.fqout.cvc4.3577.smt2 \
1449 regress1/sets/UniqueZipper.hs.1030minimized.cvc4.smt2 \
1450 regress1/sets/UniqueZipper.hs.1030minimized2.cvc4.smt2 \
1451 regress1/sets/UniqueZipper.hs.fqout.cvc4.10.smt2 \
1452 regress1/sets/UniqueZipper.hs.fqout.cvc4.1832.smt2 \
1453 regress1/sets/arjun-set-univ.cvc \
1454 regress1/sets/card-3.smt2 \
1455 regress1/sets/card-4.smt2 \
1456 regress1/sets/card-5.smt2 \
1457 regress1/sets/card-6.smt2 \
1458 regress1/sets/card-7.smt2 \
1459 regress1/sets/card-vc6-minimized.smt2 \
1460 regress1/sets/copy_check_heap_access_33_4.smt2 \
1461 regress1/sets/deepmeas0.hs.fqout.cvc4.41.smt2 \
1462 regress1/sets/fuzz14418.smt2 \
1463 regress1/sets/fuzz15201.smt2 \
1464 regress1/sets/fuzz31811.smt2 \
1465 regress1/sets/insert_invariant_37_2.smt2 \
1466 regress1/sets/issue2568.smt2 \
1467 regress1/sets/lemmabug-ListElts317minimized.smt2 \
1468 regress1/sets/remove_check_free_31_6.smt2 \
1469 regress1/sets/sets-disequal.smt2 \
1470 regress1/sets/sets-tuple-poly.cvc \
1471 regress1/sets/sharingbug.smt2 \
1472 regress1/sets/univ-set-uf-elim.smt2 \
1473 regress1/simplification_bug4.smt2 \
1474 regress1/sqrt2-sort-inf-unk.smt2 \
1475 regress1/strings/artemis-0512-nonterm.smt2 \
1476 regress1/strings/at001.smt2 \
1477 regress1/strings/bug615.smt2 \
1478 regress1/strings/bug682.smt2 \
1479 regress1/strings/bug686dd.smt2 \
1480 regress1/strings/bug768.smt2 \
1481 regress1/strings/bug799-min.smt2 \
1482 regress1/strings/chapman150408.smt2 \
1483 regress1/strings/cmu-2db2-extf-reg.smt2 \
1484 regress1/strings/cmu-5042-0707-2.smt2 \
1485 regress1/strings/cmu-inc-nlpp-071516.smt2 \
1486 regress1/strings/cmu-substr-rw.smt2 \
1487 regress1/strings/code-sequence.smt2 \
1488 regress1/strings/crash-1019.smt2 \
1489 regress1/strings/csp-prefix-exp-bug.smt2 \
1490 regress1/strings/double-replace.smt2 \
1491 regress1/strings/fmf001.smt2 \
1492 regress1/strings/fmf002.smt2 \
1493 regress1/strings/gm-inc-071516-2.smt2 \
1494 regress1/strings/goodAI.smt2 \
1495 regress1/strings/idof-handg.smt2 \
1496 regress1/strings/idof-nconst-index.smt2 \
1497 regress1/strings/idof-neg-index.smt2 \
1498 regress1/strings/idof-triv.smt2 \
1499 regress1/strings/ilc-l-nt.smt2 \
1500 regress1/strings/issue1105.smt2 \
1501 regress1/strings/issue1684-regex.smt2 \
1502 regress1/strings/issue2060.smt2 \
1503 regress1/strings/issue2429-code.smt2 \
1504 regress1/strings/kaluza-fl.smt2 \
1505 regress1/strings/loop002.smt2 \
1506 regress1/strings/loop003.smt2 \
1507 regress1/strings/loop004.smt2 \
1508 regress1/strings/loop005.smt2 \
1509 regress1/strings/loop006.smt2 \
1510 regress1/strings/loop007.smt2 \
1511 regress1/strings/loop008.smt2 \
1512 regress1/strings/loop009.smt2 \
1513 regress1/strings/nf-ff-contains-abs.smt2 \
1514 regress1/strings/non_termination_regular_expression4.smt2 \
1515 regress1/strings/norn-13.smt2 \
1516 regress1/strings/norn-360.smt2 \
1517 regress1/strings/norn-ab.smt2 \
1518 regress1/strings/norn-nel-bug-052116.smt2 \
1519 regress1/strings/norn-simp-rew-sat.smt2 \
1520 regress1/strings/nt6-dd.smt2 \
1521 regress1/strings/nterm-re-inter-sigma.smt2 \
1522 regress1/strings/pierre150331.smt2 \
1523 regress1/strings/policy_variable.smt2 \
1524 regress1/strings/re-elim-exact.smt2 \
1525 regress1/strings/re-unsound-080718.smt2 \
1526 regress1/strings/regexp001.smt2 \
1527 regress1/strings/regexp002.smt2 \
1528 regress1/strings/regexp003.smt2 \
1529 regress1/strings/reloop.smt2 \
1530 regress1/strings/repl-empty-sem.smt2 \
1531 regress1/strings/repl-soundness-sem.smt2 \
1532 regress1/strings/rew-020618.smt2 \
1533 regress1/strings/str-code-sat.smt2 \
1534 regress1/strings/str-code-unsat-2.smt2 \
1535 regress1/strings/str-code-unsat-3.smt2 \
1536 regress1/strings/str-code-unsat.smt2 \
1537 regress1/strings/str001.smt2 \
1538 regress1/strings/str002.smt2 \
1539 regress1/strings/str006.smt2 \
1540 regress1/strings/str007.smt2 \
1541 regress1/strings/string-unsound-sem.smt2 \
1542 regress1/strings/strings-index-empty.smt2 \
1543 regress1/strings/strings-leq-trans-unsat.smt2 \
1544 regress1/strings/strings-lt-len5.smt2 \
1545 regress1/strings/strings-lt-simple.smt2 \
1546 regress1/strings/strip-endpt-sound.smt2 \
1547 regress1/strings/substr001.smt2 \
1548 regress1/strings/type002.smt2 \
1549 regress1/strings/type003.smt2 \
1550 regress1/strings/username_checker_min.smt2 \
1551 regress1/sygus/VC22_a.sy \
1552 regress1/sygus/abv.sy \
1553 regress1/sygus/array_search_2.sy \
1554 regress1/sygus/array_search_5-Q-easy.sy \
1555 regress1/sygus/array_sum_2_5.sy \
1556 regress1/sygus/bvudiv-by-2.sy \
1557 regress1/sygus/car_3.lus.sy \
1558 regress1/sygus/cegar1.sy \
1559 regress1/sygus/cegis-unif-inv-eq-fair.sy \
1560 regress1/sygus/cegisunif-depth1.sy \
1561 regress1/sygus/cggmp.sy \
1562 regress1/sygus/clock-inc-tuple.sy \
1563 regress1/sygus/commutative-stream.sy \
1564 regress1/sygus/commutative.sy \
1565 regress1/sygus/constant-bool-si-all.sy \
1566 regress1/sygus/constant-dec-tree-bug.sy \
1567 regress1/sygus/constant-ite-bv.sy \
1568 regress1/sygus/constant.sy \
1569 regress1/sygus/crci-ssb-unk.sy \
1570 regress1/sygus/crcy-si-rcons.sy \
1571 regress1/sygus/crcy-si.sy \
1572 regress1/sygus/dt-test-ns.sy \
1573 regress1/sygus/dup-op.sy \
1574 regress1/sygus/fg_polynomial3.sy \
1575 regress1/sygus/find_sc_bvult_bvnot.sy \
1576 regress1/sygus/hd-01-d1-prog.sy \
1577 regress1/sygus/hd-19-d1-prog-dup-op.sy \
1578 regress1/sygus/hd-sdiv.sy \
1579 regress1/sygus/icfp_14.12-flip-args.sy \
1580 regress1/sygus/icfp_14.12.sy \
1581 regress1/sygus/icfp_14_12_diff_types.sy \
1582 regress1/sygus/icfp_28_10.sy \
1583 regress1/sygus/icfp_easy-ite.sy \
1584 regress1/sygus/inv-example.sy \
1585 regress1/sygus/inv-missed-sol-true.sy \
1586 regress1/sygus/inv-unused.sy \
1587 regress1/sygus/large-const-simp.sy \
1588 regress1/sygus/let-bug-simp.sy \
1589 regress1/sygus/list-head-x.sy \
1590 regress1/sygus/logiccell_help.sy \
1591 regress1/sygus/max.sy \
1592 regress1/sygus/max2-bv.sy \
1593 regress1/sygus/multi-fun-polynomial2.sy \
1594 regress1/sygus/nflat-fwd-3.sy \
1595 regress1/sygus/nflat-fwd.sy \
1596 regress1/sygus/nia-max-square-ns.sy \
1597 regress1/sygus/no-flat-simp.sy \
1598 regress1/sygus/no-mention.sy \
1599 regress1/sygus/parity-si-rcons.sy \
1600 regress1/sygus/pbe_multi.sy \
1601 regress1/sygus/phone-1-long.sy \
1602 regress1/sygus/planning-unif.sy \
1603 regress1/sygus/process-10-vars.sy \
1604 regress1/sygus/qe.sy \
1605 regress1/sygus/real-grammar.sy \
1606 regress1/sygus/simple-regexp.sy \
1607 regress1/sygus/stopwatch-bt.sy \
1608 regress1/sygus/strings-concat-3-args.sy \
1609 regress1/sygus/strings-double-rec.sy \
1610 regress1/sygus/strings-small.sy \
1611 regress1/sygus/strings-template-infer-unused.sy \
1612 regress1/sygus/strings-template-infer.sy \
1613 regress1/sygus/strings-trivial-simp.sy \
1614 regress1/sygus/strings-trivial-two-type.sy \
1615 regress1/sygus/strings-trivial.sy \
1616 regress1/sygus/sygus-dt.sy \
1617 regress1/sygus/sygus-lambda-fv.sy \
1618 regress1/sygus/sygus-uf-ex.sy \
1619 regress1/sygus/t8.sy \
1620 regress1/sygus/tl-type-0.sy \
1621 regress1/sygus/tl-type-4x.sy \
1622 regress1/sygus/tl-type.sy \
1623 regress1/sygus/triv-type-mismatch-si.sy \
1624 regress1/sygus/trivial-stream.sy \
1625 regress1/sygus/twolets1.sy \
1626 regress1/sygus/twolets2-orig.sy \
1627 regress1/sygus/unbdd_inv_gen_ex7.sy \
1628 regress1/sygus/unbdd_inv_gen_winf1.sy \
1629 regress1/sygus/univ_2-long-repeat.sy \
1630 regress1/sym/qf-function.smt2 \
1631 regress1/sym/q-constant.smt2 \
1632 regress1/sym/q-function.smt2 \
1633 regress1/sym/sb-wrong.smt2 \
1634 regress1/sym/sym1.smt2 \
1635 regress1/sym/sym2.smt2 \
1636 regress1/sym/sym3.smt2 \
1637 regress1/sym/sym4.smt2 \
1638 regress1/sym/sym5.smt2 \
1639 regress1/sym/sym6.smt2 \
1640 regress1/sym/sym7-uf.smt2 \
1641 regress1/sym/sym-setAB.smt2 \
1642 regress1/test12.cvc \
1645 regress1/uflia/DRAGON_11_e1_2450.ec.minimized.smt2 \
1646 regress1/uflia/FIREFLY_3_e2_2236_e7_3681.ec.core.smt2 \
1647 regress1/uflia/FIREFLY_luke_1b_e2_3049_e7_1173.ec.minimized.smt2 \
1648 regress1/uflia/microwave21.ec.minimized.smt2 \
1649 regress1/uflia/simple_cyclic2.smt2 \
1650 regress1/uflia/speed2_e8_449_e8_517.ec.smt2 \
1651 regress1/uflia/stalmark_e7_27_e7_31.ec.smt2 \
1652 regress1/wrong-qfabvfp-smtcomp2018.smt2
1655 regress2/DTP_k2_n35_c175_s15.smt2 \
1656 regress2/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2 \
1657 regress2/GEO123+1.minimized.smt2 \
1658 regress2/arith/abz5_1400.smt \
1659 regress2/arith/lpsat-goal-9.smt2 \
1660 regress2/arith/prp-13-24.smt2 \
1661 regress2/arith/pursuit-safety-11.smt \
1662 regress2/arith/pursuit-safety-12.smt \
1663 regress2/arith/qlock-4-10-9.base.cvc.smt2 \
1664 regress2/arith/sc-7.base.cvc.smt \
1665 regress2/arith/uart-8.base.cvc.smt \
1666 regress2/auflia-fuzz06.smt \
1667 regress2/bug136.smt \
1668 regress2/bug148.smt \
1669 regress2/bug394.smt2 \
1670 regress2/bug674.smt2 \
1671 regress2/bug765.smt2 \
1672 regress2/bug812.smt2 \
1673 regress2/error0.smt2 \
1674 regress2/error1.smt \
1675 regress2/friedman_n4_i5.smt \
1676 regress2/fuzz_2.smt \
1677 regress2/hash_sat_06_19.smt2 \
1678 regress2/hash_sat_07_17.smt2 \
1679 regress2/hash_sat_09_09.smt2 \
1680 regress2/hash_sat_10_09.smt2 \
1681 regress2/hole7.cvc \
1682 regress2/hole8.cvc \
1683 regress2/instance_1444.smt \
1684 regress2/javafe.ast.StandardPrettyPrint.319_no_forall.smt2 \
1685 regress2/javafe.ast.WhileStmt.447_no_forall.smt2 \
1686 regress2/nl/siegel-nl-bases.smt2 \
1687 regress2/ooo.rf6.smt2 \
1688 regress2/ooo.tag10.smt2 \
1689 regress2/piVC_5581bd.smt2 \
1690 regress2/push-pop/DRAGON_4_e2_2799_e3_1915.lus.ic3.1.min.smt2 \
1691 regress2/quantifiers/AdditiveMethods_AdditiveMethods..ctor.smt2 \
1692 regress2/quantifiers/gn-wrong-091018.smt2 \
1693 regress2/quantifiers/javafe.ast.ArrayInit.35.smt2 \
1694 regress2/quantifiers/javafe.ast.StandardPrettyPrint.319.smt2 \
1695 regress2/quantifiers/javafe.ast.WhileStmt.447.smt2 \
1696 regress2/quantifiers/javafe.tc.CheckCompilationUnit.001.smt2 \
1697 regress2/quantifiers/javafe.tc.FlowInsensitiveChecks.682.smt2 \
1698 regress2/quantifiers/mutualrec2.cvc \
1699 regress2/quantifiers/net-policy-no-time.smt2 \
1700 regress2/quantifiers/nunchaku2309663.nun.min.smt2 \
1701 regress2/simplify.javafe.ast.ArrayInit.35_without_quantification2.smt2 \
1702 regress2/strings/cmu-dis-0707-3.smt2 \
1703 regress2/strings/cmu-disagree-0707-dd.smt2 \
1704 regress2/strings/cmu-prereg-fmf.smt2 \
1705 regress2/strings/cmu-repl-len-nterm.smt2 \
1706 regress2/strings/norn-dis-0707-3.smt2 \
1707 regress2/strings/repl-repl.smt2 \
1708 regress2/sygus/MPwL_d1s3.sy \
1709 regress2/sygus/array_sum_dd.sy \
1710 regress2/sygus/cegisunif-depth1-bv.sy \
1711 regress2/sygus/ex23.sy \
1712 regress2/sygus/icfp_easy_mt_ite.sy \
1713 regress2/sygus/inv_gen_n_c11.sy \
1714 regress2/sygus/lustre-real.sy \
1715 regress2/sygus/max2-univ.sy \
1716 regress2/sygus/mpg_guard1-dd.sy \
1717 regress2/sygus/multi-udiv.sy \
1718 regress2/sygus/nia-max-square.sy \
1719 regress2/sygus/no-syntax-test-no-si.sy \
1720 regress2/sygus/process-10-vars-2fun.sy \
1721 regress2/sygus/process-arg-invariance.sy \
1722 regress2/sygus/real-grammar-neg.sy \
1723 regress2/sygus/three.sy \
1724 regress2/sygus/vcb.sy \
1725 regress2/typed_v1l50016-simp.cvc \
1726 regress2/uflia-error0.smt2 \
1727 regress2/xs-09-16-3-4-1-5.decn.smt \
1728 regress2/xs-09-16-3-4-1-5.smt
1731 regress3/bmc-ibm-1.smt \
1732 regress3/bmc-ibm-2.smt \
1733 regress3/bmc-ibm-5.smt \
1734 regress3/bmc-ibm-7.smt \
1735 regress3/eq_diamond14.smt \
1736 regress3/friedman_n6_i4.smt \
1737 regress3/hole9.cvc \
1738 regress3/incorrect1.smt \
1739 regress3/incorrect2.smt \
1740 regress3/issue2429.smt2 \
1741 regress3/pp-regfile.smt \
1742 regress3/qwh.35.405.shuffled-as.sat03-1651.smt \
1743 regress3/sixfuncs.sy
1746 regress4/C880mul.miter.shuffled-as.sat03-348.smt \
1747 regress4/NEQ016_size5.smt \
1748 regress4/bug143.smt \
1749 regress4/comb2.shuffled-as.sat03-420.smt \
1750 regress4/hole10.cvc \
1751 regress4/instance_1151.smt
1753 # dejan: disabled these because it's mixed arithmetic and it doesn't go
1754 # well when changing theoryof:
1755 # - regress0/unconstrained/arith2.smt2
1756 # - regress0/unconstrained/arith7.smt2
1758 # lianah: disabled these as the unconstrained terms are no longer
1759 # recognized after implementing the divide-by-zero semantics for bv division:
1760 # - regress0/unconstrained/bvdiv.smt2,
1761 # - regress0/unconstrained/bvconcat.smt2
1763 # Proof checking takes too long. Add this back.
1764 # - regress0/bv/fuzz15.delta01.smt
1766 # regress1/ho/hoa0102.smt2 results in an assertion failure (see issue #1650).
1768 # ajreynol: disabled these since they give different error messages on
1769 # production and debug:
1770 # - regress1/quantifiers/macro-subtype-param.smt2
1771 # - regress1/quantifiers/subtype-param-unk.smt2
1772 # - regress1/quantifiers/subtype-param.smt2
1774 # issue1048-arrays-int-real.smt2 -- different errors on debug and production.
1776 # regress0/aufbv/bug348 does not seem to terminate with proofs
1777 # regress0/datatypes/datatype-dump.cvc (FIXME #1649)
1779 # regress1/quantifiers/set3.smt2 does not terminate/takes a long time when
1780 # doing a coverage build with LFSC.
1782 regress0/arith/bug549.cvc \
1783 regress0/arith/incorrect1.smt \
1784 regress0/arith/integers/arith-int-014.cvc \
1785 regress0/arith/integers/arith-int-015.cvc \
1786 regress0/arith/integers/arith-int-021.cvc \
1787 regress0/arith/integers/arith-int-023.cvc \
1788 regress0/arith/integers/arith-int-025.cvc \
1789 regress0/arith/integers/arith-int-079.cvc \
1790 regress0/arith/integers/arith-interval.cvc \
1791 regress0/arith/miplib-opt1217--27.smt \
1792 regress0/arith/miplib-pp08a-3000.smt \
1794 regress0/arr1.smt2 \
1796 regress0/aufbv/bug348.smt \
1797 regress0/aufbv/bug349.smt \
1798 regress0/aufbv/bug493.smt \
1799 regress0/aufbv/dubreva005ue.smt \
1800 regress0/aufbv/fifo32bc06k08.smt \
1801 regress0/aufbv/fifo32in06k08.delta01.smt \
1802 regress0/aufbv/fifo32in06k08.smt \
1803 regress0/aufbv/no_init_multi_delete14.smt \
1804 regress0/aufbv/try3_sameret_functions_fse-bfs_tac.calc_next.il.fse-bfs.smt \
1805 regress0/aufbv/wchains010ue.smt \
1806 regress0/auflia/fuzz01.smt \
1808 regress0/bug374.delta01.smt \
1809 regress0/bug374.smt \
1810 regress0/bv/bug345.smt \
1811 regress0/bv/bvcomp.cvc \
1812 regress0/bv/bvsmod.smt2 \
1813 regress0/bv/core/bitvec0.delta01.smt \
1814 regress0/bv/core/bitvec1.smt \
1815 regress0/bv/core/bitvec3.smt \
1816 regress0/bv/core/bv_eq_diamond11.smt \
1817 regress0/bv/core/bv_eq_diamond12.smt \
1818 regress0/bv/core/bv_eq_diamond13.smt \
1819 regress0/bv/core/bv_eq_diamond14.smt \
1820 regress0/bv/core/bv_eq_diamond15.smt \
1821 regress0/bv/core/bv_eq_diamond16.smt \
1822 regress0/bv/core/bv_eq_diamond17.smt \
1823 regress0/bv/core/concat-merge-0.cvc \
1824 regress0/bv/core/concat-merge-1.cvc \
1825 regress0/bv/core/concat-merge-2.cvc \
1826 regress0/bv/core/concat-merge-3.cvc \
1827 regress0/bv/core/constant_core.smt2 \
1828 regress0/bv/core/equality-00.cvc \
1829 regress0/bv/core/equality-01.cvc \
1830 regress0/bv/core/equality-02.cvc \
1831 regress0/bv/core/equality-03.cvc \
1832 regress0/bv/core/equality-03.smt \
1833 regress0/bv/core/equality-04.smt \
1834 regress0/bv/core/equality-05.smt \
1835 regress0/bv/core/ext_con_004_001_1024.smt \
1836 regress0/bv/core/extract-concat-0.cvc \
1837 regress0/bv/core/extract-concat-1.cvc \
1838 regress0/bv/core/extract-concat-10.cvc \
1839 regress0/bv/core/extract-concat-11.cvc \
1840 regress0/bv/core/extract-concat-2.cvc \
1841 regress0/bv/core/extract-concat-3.cvc \
1842 regress0/bv/core/extract-concat-4.cvc \
1843 regress0/bv/core/extract-concat-5.cvc \
1844 regress0/bv/core/extract-concat-6.cvc \
1845 regress0/bv/core/extract-concat-7.cvc \
1846 regress0/bv/core/extract-concat-8.cvc \
1847 regress0/bv/core/extract-concat-9.cvc \
1848 regress0/bv/core/extract-constant.cvc \
1849 regress0/bv/core/extract-extract-0.cvc \
1850 regress0/bv/core/extract-extract-1.cvc \
1851 regress0/bv/core/extract-extract-10.cvc \
1852 regress0/bv/core/extract-extract-11.cvc \
1853 regress0/bv/core/extract-extract-2.cvc \
1854 regress0/bv/core/extract-extract-3.cvc \
1855 regress0/bv/core/extract-extract-4.cvc \
1856 regress0/bv/core/extract-extract-5.cvc \
1857 regress0/bv/core/extract-extract-6.cvc \
1858 regress0/bv/core/extract-extract-7.cvc \
1859 regress0/bv/core/extract-extract-8.cvc \
1860 regress0/bv/core/extract-extract-9.cvc \
1861 regress0/bv/core/extract-whole-0.cvc \
1862 regress0/bv/core/extract-whole-1.cvc \
1863 regress0/bv/core/extract-whole-2.cvc \
1864 regress0/bv/core/extract-whole-3.cvc \
1865 regress0/bv/core/extract-whole-4.cvc \
1866 regress0/bv/core/incremental.smt \
1867 regress0/bv/core/slice-01.cvc \
1868 regress0/bv/core/slice-02.cvc \
1869 regress0/bv/core/slice-03.cvc \
1870 regress0/bv/core/slice-04.cvc \
1871 regress0/bv/core/slice-05.cvc \
1872 regress0/bv/core/slice-06.cvc \
1873 regress0/bv/core/slice-07.cvc \
1874 regress0/bv/core/slice-08.cvc \
1875 regress0/bv/core/slice-09.cvc \
1876 regress0/bv/core/slice-10.cvc \
1877 regress0/bv/core/slice-11.cvc \
1878 regress0/bv/core/slice-12.cvc \
1879 regress0/bv/core/slice-13.cvc \
1880 regress0/bv/core/slice-14.cvc \
1881 regress0/bv/core/slice-15.cvc \
1882 regress0/bv/core/slice-16.cvc \
1883 regress0/bv/core/slice-17.cvc \
1884 regress0/bv/core/slice-18.cvc \
1885 regress0/bv/core/slice-19.cvc \
1886 regress0/bv/core/slice-20.cvc \
1887 regress0/bv/fuzz07-delta.smt \
1888 regress0/bv/fuzz15.delta01.smt \
1889 regress0/bv/fuzz15.smt \
1890 regress0/bv/fuzz16.smt \
1891 regress0/bv/fuzz17.smt \
1892 regress0/bv/incorrect1.delta01.smt \
1893 regress0/bv/incorrect1.smt \
1894 regress0/bv/inequality00.smt2 \
1895 regress0/bv/inequality01.smt2 \
1896 regress0/bv/inequality02.smt2 \
1897 regress0/bv/inequality03.smt2 \
1898 regress0/bv/inequality04.smt2 \
1899 regress0/bv/inequality05.smt2 \
1900 regress0/bv/test00.smt \
1901 regress0/cvc3-bug15.cvc \
1902 regress0/decision/uflia-xs-09-16-3-4-1-5.smt \
1903 regress0/decision/wchains010ue.smt \
1904 regress0/incorrect1.smt \
1906 regress0/ite_arith.smt2 \
1907 regress0/lemmas/fischer3-mutex-16.smt \
1908 regress0/nl/all-logic.smt2 \
1909 regress0/quantifiers/qbv-multi-lit-uge.smt2 \
1910 regress0/quantifiers/qbv-test-invert-bvshl-0-neq.smt2 \
1911 regress0/quantifiers/qbv-test-invert-concat-0-neq.smt2 \
1912 regress0/quantifiers/qbv-test-invert-concat-1-neq.smt2 \
1913 regress0/rewriterules/datatypes_clark.smt2 \
1914 regress0/rewriterules/length.smt2 \
1915 regress0/rewriterules/length_gen_n.smt2 \
1916 regress0/rewriterules/length_gen_n_lemma.smt2 \
1917 regress0/rewriterules/length_trick2.smt2 \
1918 regress0/rewriterules/native_datatypes.smt2 \
1919 regress0/sets/mar2014/stacks0.hs.78.cvc4.smt2 \
1920 regress0/sets/setel-eq.smt2 \
1921 regress0/sets/sets-new.smt2 \
1922 regress0/sets/sets-testlemma-ints.smt2 \
1923 regress0/sets/sets-testlemma-reals.smt2 \
1924 regress0/sygus/sygus-uf.sy \
1925 regress0/symmetric.smt \
1926 regress0/tptp/BOO003-4.p \
1927 regress0/tptp/BOO027-1.p \
1928 regress0/tptp/MGT031-1.p \
1929 regress0/tptp/NLP114-1.p \
1930 regress0/tptp/SYN075+1.p \
1931 regress0/uf/PEQ018_size4.smt \
1932 regress0/uf/SEQ032_size2.smt \
1933 regress0/uf/iso_icl_repgen004.smt \
1934 regress0/uflia/diseqprop.01.smt \
1935 regress0/uflia/diseqprop.02.smt \
1936 regress0/uflia/diseqprop.03.smt \
1937 regress0/uflia/diseqprop.04.smt \
1938 regress0/uflia/diseqprop.05.smt \
1939 regress0/uflia/diseqprop.06.smt \
1940 regress0/uflia/xs-09-16-3-4-1-5.delta05.smt \
1941 regress0/uflra/pb_real_10_0200_10_25.smt \
1942 regress0/uflra/pb_real_10_0200_10_27.smt \
1943 regress0/unconstrained/arith2.smt2 \
1944 regress0/unconstrained/arith7.smt2 \
1945 regress0/unconstrained/bvconcat.smt2 \
1946 regress0/unconstrained/bvdiv.smt \
1947 regress1/arith/arith-int-001.cvc \
1948 regress1/arith/arith-int-002.cvc \
1949 regress1/arith/arith-int-003.cvc \
1950 regress1/arith/arith-int-005.cvc \
1951 regress1/arith/arith-int-006.cvc \
1952 regress1/arith/arith-int-007.cvc \
1953 regress1/arith/arith-int-008.cvc \
1954 regress1/arith/arith-int-009.cvc \
1955 regress1/arith/arith-int-010.cvc \
1956 regress1/arith/arith-int-016.cvc \
1957 regress1/arith/arith-int-017.cvc \
1958 regress1/arith/arith-int-018.cvc \
1959 regress1/arith/arith-int-019.cvc \
1960 regress1/arith/arith-int-020.cvc \
1961 regress1/arith/arith-int-026.cvc \
1962 regress1/arith/arith-int-027.cvc \
1963 regress1/arith/arith-int-028.cvc \
1964 regress1/arith/arith-int-029.cvc \
1965 regress1/arith/arith-int-030.cvc \
1966 regress1/arith/arith-int-031.cvc \
1967 regress1/arith/arith-int-032.cvc \
1968 regress1/arith/arith-int-033.cvc \
1969 regress1/arith/arith-int-034.cvc \
1970 regress1/arith/arith-int-035.cvc \
1971 regress1/arith/arith-int-036.cvc \
1972 regress1/arith/arith-int-037.cvc \
1973 regress1/arith/arith-int-038.cvc \
1974 regress1/arith/arith-int-039.cvc \
1975 regress1/arith/arith-int-040.cvc \
1976 regress1/arith/arith-int-041.cvc \
1977 regress1/arith/arith-int-043.cvc \
1978 regress1/arith/arith-int-044.cvc \
1979 regress1/arith/arith-int-045.cvc \
1980 regress1/arith/arith-int-046.cvc \
1981 regress1/arith/arith-int-049.cvc \
1982 regress1/arith/arith-int-051.cvc \
1983 regress1/arith/arith-int-052.cvc \
1984 regress1/arith/arith-int-053.cvc \
1985 regress1/arith/arith-int-054.cvc \
1986 regress1/arith/arith-int-055.cvc \
1987 regress1/arith/arith-int-056.cvc \
1988 regress1/arith/arith-int-057.cvc \
1989 regress1/arith/arith-int-058.cvc \
1990 regress1/arith/arith-int-059.cvc \
1991 regress1/arith/arith-int-060.cvc \
1992 regress1/arith/arith-int-061.cvc \
1993 regress1/arith/arith-int-062.cvc \
1994 regress1/arith/arith-int-063.cvc \
1995 regress1/arith/arith-int-064.cvc \
1996 regress1/arith/arith-int-065.cvc \
1997 regress1/arith/arith-int-066.cvc \
1998 regress1/arith/arith-int-067.cvc \
1999 regress1/arith/arith-int-068.cvc \
2000 regress1/arith/arith-int-069.cvc \
2001 regress1/arith/arith-int-070.cvc \
2002 regress1/arith/arith-int-071.cvc \
2003 regress1/arith/arith-int-072.cvc \
2004 regress1/arith/arith-int-073.cvc \
2005 regress1/arith/arith-int-074.cvc \
2006 regress1/arith/arith-int-075.cvc \
2007 regress1/arith/arith-int-076.cvc \
2008 regress1/arith/arith-int-077.cvc \
2009 regress1/arith/arith-int-078.cvc \
2010 regress1/arith/arith-int-080.cvc \
2011 regress1/arith/arith-int-081.cvc \
2012 regress1/arith/arith-int-082.cvc \
2013 regress1/arith/arith-int-083.cvc \
2014 regress1/arith/arith-int-086.cvc \
2015 regress1/arith/arith-int-087.cvc \
2016 regress1/arith/arith-int-088.cvc \
2017 regress1/arith/arith-int-089.cvc \
2018 regress1/arith/arith-int-090.cvc \
2019 regress1/arith/arith-int-091.cvc \
2020 regress1/arith/arith-int-092.cvc \
2021 regress1/arith/arith-int-093.cvc \
2022 regress1/arith/arith-int-094.cvc \
2023 regress1/arith/arith-int-095.cvc \
2024 regress1/arith/arith-int-096.cvc \
2025 regress1/arith/arith-int-099.cvc \
2026 regress1/arith/arith-int-100.cvc \
2027 regress1/auflia/bug337.smt2 \
2028 regress1/bug472.smt2 \
2029 regress1/bug585.cvc \
2030 regress1/bug590.smt2 \
2031 regress1/bv/bench_38.delta.smt2 \
2032 regress1/crash_burn_locusts.smt2 \
2033 regress1/ho/hoa0102.smt2 \
2034 regress1/issue1048-arrays-int-real.smt2 \
2035 regress1/quantifiers/macro-subtype-param.smt2 \
2036 regress1/quantifiers/set3.smt2 \
2037 regress1/quantifiers/subtype-param-unk.smt2 \
2038 regress1/quantifiers/subtype-param.smt2 \
2039 regress1/rels/garbage_collect.cvc \
2040 regress1/rewriterules/datatypes2.smt2 \
2041 regress1/rewriterules/datatypes3.smt2 \
2042 regress1/rewriterules/datatypes_clark_quantification.smt2 \
2043 regress1/rewriterules/length_gen_010.smt2 \
2044 regress1/rewriterules/length_gen_010_lemma.smt2 \
2045 regress1/rewriterules/length_gen_080.smt2 \
2046 regress1/rewriterules/length_gen_160_lemma.smt2 \
2047 regress1/rewriterules/length_gen_inv_160.smt2 \
2048 regress1/rewriterules/length_trick3.smt2 \
2049 regress1/rewriterules/length_trick3_int.smt2 \
2050 regress1/rewriterules/set_A_new_fast_tableau-base.smt2 \
2051 regress1/rewriterules/set_A_new_fast_tableau-base_sat.smt2 \
2052 regress1/rewriterules/test_guards.smt2 \
2053 regress1/rewriterules/why3_vstte10_max_sum_harness2.smt2 \
2054 regress1/sets/setofsets-disequal.smt2 \
2055 regress1/simple-rdl-definefun.smt2 \
2056 regress1/sygus/Base16_1.sy \
2057 regress1/sygus/enum-test.sy \
2058 regress1/sygus/inv_gen_fig8.sy \
2059 regress2/arith/arith-int-098.cvc \
2060 regress2/arith/miplib-opt1217--27.smt2 \
2061 regress2/arith/miplib-pp08a-3000.smt2 \
2062 regress2/bug396.smt2 \
2063 regress2/nl/dumortier-050317.smt2 \
2064 regress2/nl/nt-lemmas-bad.smt2 \
2065 regress2/quantifiers/ForElimination-scala-9.smt2 \
2066 regress2/quantifiers/small-bug1-fixpoint-3.smt2 \
2067 regress2/xs-11-20-5-2-5-3.smt \
2068 regress2/xs-11-20-5-2-5-3.smt2
projects / cvc5.git / blob