test/regress/cli/CMakeLists.txt

   1 ###############################################################################
   2 # Top contributors (to current version):
   3 #   Aina Niemetz, Andrew Reynolds, Mathias Preiner
   4 #
   5 # This file is part of the cvc5 project.
   6 #
   7 # Copyright (c) 2009-2022 by the authors listed in the file AUTHORS
   8 # in the top-level source directory and their institutional affiliations.
   9 # All rights reserved.  See the file COPYING in the top-level source
  10 # directory for licensing information.
  11 # #############################################################################
  12 #
  13 # The build system configuration.
  14 ##
  15
  16 # Regression level 0 tests
  17 set(regress_0_tests
  18   regress0/arith/ackermann.real.smt2
  19   regress0/arith/arith-eq.smt2
  20   regress0/arith/arith-mixed-types-no-tighten.smt2
  21   regress0/arith/arith-mixed-types-tighten.smt2
  22   regress0/arith/arith-strict-relaxed.smt2
  23   regress0/arith/arith-strict.smt2
  24   regress0/arith/arith-tighten-1.smt2
  25   regress0/arith/arith-tighten-2.smt2
  26   regress0/arith/arith.01.cvc.smt2
  27   regress0/arith/arith.02.cvc.smt2
  28   regress0/arith/arith.03.cvc.smt2
  29   regress0/arith/bug443.delta01.smtv1.smt2
  30   regress0/arith/bug547.2.smt2
  31   regress0/arith/bug549.cvc.smt2
  32   regress0/arith/bug569.smt2
  33   regress0/arith/delta-minimized-row-vector-bug.smtv1.smt2
  34   regress0/arith/div-chainable.smt2
  35   regress0/arith/div.01.smt2
  36   regress0/arith/div.02.smt2
  37   regress0/arith/div.04.smt2
  38   regress0/arith/div.05.smt2
  39   regress0/arith/div.07.smt2
  40   regress0/arith/exp-in-model.smt2
  41   regress0/arith/fuzz_3-eq.smtv1.smt2
  42   regress0/arith/incorrect1.smtv1.smt2
  43   regress0/arith/integers/ackermann1.smt2
  44   regress0/arith/integers/ackermann2.smt2
  45   regress0/arith/integers/ackermann3.smt2
  46   regress0/arith/integers/ackermann4.smt2
  47   regress0/arith/integers/ackermann5.smt2
  48   regress0/arith/integers/ackermann6.smt2
  49   regress0/arith/integers/arith-int-014.cvc.smt2
  50   regress0/arith/integers/arith-int-015.cvc.smt2
  51   regress0/arith/integers/arith-int-021.cvc.smt2
  52   regress0/arith/integers/arith-int-023.cvc.smt2
  53   regress0/arith/integers/arith-int-025.cvc.smt2
  54   regress0/arith/integers/arith-int-042.cvc.smt2
  55   regress0/arith/integers/arith-int-042.min.cvc.smt2
  56   regress0/arith/integers/arith-int-079.cvc.smt2
  57   regress0/arith/integers/arith-interval.cvc.smt2
  58   regress0/arith/integers/issue6146-stale-vars.smt2
  59   regress0/arith/issue1399.smt2
  60   regress0/arith/issue3412.smt2
  61   regress0/arith/issue3413.smt2
  62   regress0/arith/issue3683.smt2
  63   regress0/arith/issue4367.smt2
  64   regress0/arith/issue4525.smt2
  65   regress0/arith/issue5219-conflict-rewrite.smt2
  66   regress0/arith/issue5761-ppr.smt2
  67   regress0/arith/issue8097-iid.smt2
  68   regress0/arith/issue8159-rewrite-intreal.smt2
  69   regress0/arith/ite-lift.smt2
  70   regress0/arith/leq.01.smtv1.smt2
  71   regress0/arith/miplib.cvc.smt2
  72   regress0/arith/miplib2.cvc.smt2
  73   regress0/arith/miplib4.cvc.smt2
  74   regress0/arith/miplibtrick.smtv1.smt2
  75   regress0/arith/mod-simp.smt2
  76   regress0/arith/mod.01.smt2
  77   regress0/arith/mult.01.smt2
  78   regress0/arith/non-normal.smt2
  79   regress0/arith/projissue469-int-equality.smt2
  80   regress0/arr1.smt2
  81   regress0/arr1.smtv1.smt2
  82   regress0/arr2.smtv1.smt2
  83   regress0/array-const-real-parse.smt2
  84   regress0/arrayinuf_declare.smt2
  85   regress0/arrays/arrays0.smt2
  86   regress0/arrays/arrays1.smt2
  87   regress0/arrays/arrays2.smt2
  88   regress0/arrays/arrays3.smt2
  89   regress0/arrays/arrays4.smt2
  90   regress0/arrays/bool-array.smt2
  91   regress0/arrays/bug272.minimized.smtv1.smt2
  92   regress0/arrays/bug272.smtv1.smt2
  93   regress0/arrays/bug3020.smt2
  94   regress0/arrays/bug4957.smt2
  95   regress0/arrays/bug637.delta.smt2
  96   regress0/arrays/constarr.cvc.smt2
  97   regress0/arrays/constarr.smt2
  98   regress0/arrays/constarr2.cvc.smt2
  99   regress0/arrays/constarr2.smt2
 100   regress0/arrays/incorrect1.smtv1.smt2
 101   regress0/arrays/incorrect10.smtv1.smt2
 102   regress0/arrays/incorrect11.smtv1.smt2
 103   regress0/arrays/incorrect2.minimized.smtv1.smt2
 104   regress0/arrays/incorrect2.smtv1.smt2
 105   regress0/arrays/incorrect3.smtv1.smt2
 106   regress0/arrays/incorrect4.smtv1.smt2
 107   regress0/arrays/incorrect5.smtv1.smt2
 108   regress0/arrays/incorrect6.smtv1.smt2
 109   regress0/arrays/incorrect7.smtv1.smt2
 110   regress0/arrays/incorrect8.minimized.smtv1.smt2
 111   regress0/arrays/incorrect8.smtv1.smt2
 112   regress0/arrays/incorrect9.smtv1.smt2
 113   regress0/arrays/issue3813-massign-assert.smt2
 114   regress0/arrays/issue3814.smt2
 115   regress0/arrays/issue4240.smt2
 116   regress0/arrays/issue4414-2.smt2
 117   regress0/arrays/issue4414.smt2
 118   regress0/arrays/issue4546-2.smt2
 119   regress0/arrays/issue4546.smt2
 120   regress0/arrays/issue4780-3.smt2
 121   regress0/arrays/issue4780.smt2
 122   regress0/arrays/issue4927-unsat-cores.smt2
 123   regress0/arrays/issue5720.smt2
 124   regress0/arrays/issue5836-2.smt2
 125   regress0/arrays/issue5836.smt2
 126   regress0/arrays/issue5925.smt2
 127   regress0/arrays/issue5925-2.smt2
 128   regress0/arrays/issue6276-2.smt2
 129   regress0/arrays/issue6276.smt2
 130   regress0/arrays/issue6700-inc-check-model.smt2
 131   regress0/arrays/issue6807-idem-rew.smt2
 132   regress0/arrays/issue7596-define-array-uminus.smt2
 133   regress0/arrays/issue8103-1-weak-equiv-models.smt2
 134   regress0/arrays/issue8276-arith-getModelValue.smt2
 135   regress0/arrays/swap_t1_np_nf_ai_00005_007.cvc.smtv1.smt2
 136   regress0/arrays/x2.smtv1.smt2
 137   regress0/arrays/x3.smtv1.smt2
 138   regress0/aufbv/array_rewrite_bug.smtv1.smt2
 139   regress0/aufbv/bug00.smtv1.smt2
 140   regress0/aufbv/bug338.smt2
 141   regress0/aufbv/bug347.smtv1.smt2
 142   regress0/aufbv/bug451.smtv1.smt2
 143   regress0/aufbv/bug493.smtv1.smt2
 144   regress0/aufbv/bug509.smtv1.smt2
 145   regress0/aufbv/bug580.delta.smt2
 146   regress0/aufbv/cee-small-shared-eq.smt2
 147   regress0/aufbv/diseqprop.01.smtv1.smt2
 148   regress0/aufbv/dubreva005ue.delta01.smtv1.smt2
 149   regress0/aufbv/fifo32bc06k08.delta01.smtv1.smt2
 150   regress0/aufbv/fifo32in06k08.delta01.smtv1.smt2
 151   regress0/aufbv/fuzz00.smtv1.smt2
 152   regress0/aufbv/fuzz01.delta01.smtv1.smt2
 153   regress0/aufbv/fuzz01.smtv1.smt2
 154   regress0/aufbv/fuzz02.delta01.smtv1.smt2
 155   regress0/aufbv/fuzz02.smtv1.smt2
 156   regress0/aufbv/fuzz03.delta01.smtv1.smt2
 157   regress0/aufbv/fuzz04.delta01.smtv1.smt2
 158   regress0/aufbv/fuzz04.smtv1.smt2
 159   regress0/aufbv/fuzz05.delta01.smtv1.smt2
 160   regress0/aufbv/fuzz05.smtv1.smt2
 161   regress0/aufbv/fuzz06.delta01.smtv1.smt2
 162   regress0/aufbv/fuzz06.smtv1.smt2
 163   regress0/aufbv/fuzz07.smtv1.smt2
 164   regress0/aufbv/fuzz08.smtv1.smt2
 165   regress0/aufbv/fuzz09.smtv1.smt2
 166   regress0/aufbv/fuzz11.smtv1.smt2
 167   regress0/aufbv/fuzz12.smtv1.smt2
 168   regress0/aufbv/fuzz13.smtv1.smt2
 169   regress0/aufbv/fuzz14.smtv1.smt2
 170   regress0/aufbv/fuzz15.smtv1.smt2
 171   regress0/aufbv/issue3687-check-models-small.smt2
 172   regress0/aufbv/issue3737.smt2
 173   regress0/aufbv/rewrite_bug.smtv1.smt2
 174   regress0/aufbv/try3_sameret_functions_fse-bfs_tac.calc_next.il.fse-bfs.delta01.smtv1.smt2
 175   regress0/aufbv/try5_small_difret_functions_wp_su.set_char_quoting.il.wp.delta01.smtv1.smt2
 176   regress0/aufbv/wchains010ue.delta01.smtv1.smt2
 177   regress0/aufbv/wchains010ue.delta02.smtv1.smt2
 178   regress0/auflia/a17.smtv1.smt2
 179   regress0/auflia/bug336.smt2
 180   regress0/auflia/error72.delta2.smtv1.smt2
 181   regress0/auflia/fuzz-error1099.smtv1.smt2
 182   regress0/auflia/fuzz-error232.smtv1.smt2
 183   regress0/auflia/fuzz01.delta01.smtv1.smt2
 184   regress0/auflia/fuzz02.smtv1.smt2
 185   regress0/auflia/fuzz03.smtv1.smt2
 186   regress0/auflia/fuzz04.smtv1.smt2
 187   regress0/auflia/fuzz05.smtv1.smt2
 188   regress0/auflia/x2.smtv1.smt2
 189   regress0/bool/issue1978.smt2
 190   regress0/bool/issue6717-ite-rewrite.smt2
 191   regress0/boolean-prec.cvc.smt2
 192   regress0/boolean-terms-bug-array.smt2
 193   regress0/boolean-terms-kernel1.smt2
 194   regress0/boolean-terms.cvc.smt2
 195   regress0/bt-test-00.smt2
 196   regress0/bt-test-01.smt2
 197   regress0/bug1247.smt2
 198   regress0/bug161.smtv1.smt2
 199   regress0/bug164.smtv1.smt2
 200   regress0/bug167.smtv1.smt2
 201   regress0/bug168.smtv1.smt2
 202   regress0/bug187.smt2
 203   regress0/bug217.smt2
 204   regress0/bug220.smt2
 205   regress0/bug239.smtv1.smt2
 206   regress0/bug274.cvc.smt2
 207   regress0/bug288.smtv1.smt2
 208   regress0/bug288b.smtv1.smt2
 209   regress0/bug288c.smtv1.smt2
 210   regress0/bug303.smt2
 211   regress0/bug310.cvc.smt2
 212   regress0/bug32.cvc.smt2
 213   regress0/bug322.cvc.smt2
 214   regress0/bug322b.cvc.smt2
 215   regress0/bug339.smt2
 216   regress0/bug365.smt2
 217   regress0/bug382.smt2
 218   regress0/bug383.smt2
 219   regress0/bug398.smt2
 220   regress0/bug421.smt2
 221   regress0/bug480.smt2
 222   regress0/bug484.smt2
 223   regress0/bug486.cvc.smt2
 224   regress0/bug49.smtv1.smt2
 225   regress0/bug512.minimized.smt2
 226   regress0/bug521.minimized.smt2
 227   regress0/bug522.smt2
 228   regress0/bug528a.smt2
 229   regress0/bug541.smt2
 230   regress0/bug544.smt2
 231   regress0/bug548a.smt2
 232   regress0/bug576.smt2
 233   regress0/bug576a.smt2
 234   regress0/bug578.smt2
 235   regress0/bug586.cvc.smt2
 236   regress0/bug595.cvc.smt2
 237   regress0/bug596.cvc.smt2
 238   regress0/bug596b.cvc.smt2
 239   regress0/bug605.cvc.smt2
 240   regress0/bug639.smt2
 241   regress0/buggy-ite.smt2
 242   regress0/bv/ackermann1.smt2
 243   regress0/bv/ackermann2.smt2
 244   regress0/bv/ackermann3.smt2
 245   regress0/bv/ackermann4.smt2
 246   regress0/bv/ackermann5.smt2
 247   regress0/bv/ackermann6.smt2
 248   regress0/bv/ackermann7.smt2
 249   regress0/bv/ackermann8.smt2
 250   regress0/bv/bool-model.smt2
 251   regress0/bv/bool-to-bv-all-array-bool.smt2
 252   regress0/bv/bool-to-bv-all-test.smt2
 253   regress0/bv/bool-to-bv-all.smt2
 254   regress0/bv/bool-to-bv-ite-array-bool.smt2
 255   regress0/bv/bool-to-bv-ite.smt2
 256   regress0/bv/bug260a.smtv1.smt2
 257   regress0/bv/bug260b.smtv1.smt2
 258   regress0/bv/bug345.smtv1.smt2
 259   regress0/bv/bug440.smtv1.smt2
 260   regress0/bv/bug733.smt2
 261   regress0/bv/bug734.smt2
 262   regress0/bv/bv-abstr-bug2.smt2
 263   regress0/bv/bv-int-collapse1.smt2
 264   regress0/bv/bv-int-collapse2.smt2
 265   regress0/bv/bv-options4.smt2
 266   regress0/bv/bv-to-bool1.smtv1.smt2
 267   regress0/bv/bv-to-bool2.smt2
 268   regress0/bv/bv2nat-ground-c.smt2
 269   regress0/bv/bv2nat-simp-range.smt2
 270   regress0/bv/bv_to_int1.smt2
 271   regress0/bv/bv_to_int_5230_binary.smt2
 272   regress0/bv/bv_to_int_5230_missing_op.smt2
 273   regress0/bv/bv_to_int_5230_shift_const.smt2
 274   regress0/bv/bv_to_int_5281.smt2
 275   regress0/bv/bv_to_int_5293_1.smt2
 276   regress0/bv/bv_to_int_5293_2.smt2
 277   regress0/bv/bv_to_int_bvmul2.smt2
 278   regress0/bv/bv_to_int_bvuf_to_intuf.smt2
 279   regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2
 280   regress0/bv/bv_to_int_elim_err.smt2
 281   regress0/bv/bv_to_int_issue_8413_1.smt2
 282   regress0/bv/bv_to_int_issue_8413_2.smt2
 283   regress0/bv/bv_to_int_int1.smt2
 284   regress0/bv/bv_to_int_zext.smt2
 285   regress0/bv/bvcomp.cvc.smt2
 286   regress0/bv/bvmul-pow2-only.smt2
 287   regress0/bv/bvproof1.smt2
 288   regress0/bv/bvproof2.smt2
 289   regress0/bv/bvproof3.smt2
 290   regress0/bv/bvsimple.cvc.smt2
 291   regress0/bv/bvsmod.smt2
 292   regress0/bv/calc2_sec2_shifter_mult_bmc15.atlas.delta01.smtv1.smt2
 293   regress0/bv/core/a78test0002.smtv1.smt2
 294   regress0/bv/core/a95test0002.smtv1.smt2
 295   regress0/bv/core/bitvec0.delta01.smtv1.smt2
 296   regress0/bv/core/bitvec0.smtv1.smt2
 297   regress0/bv/core/bitvec1.smtv1.smt2
 298   regress0/bv/core/bitvec2.smtv1.smt2
 299   regress0/bv/core/bitvec3.smtv1.smt2
 300   regress0/bv/core/bitvec5.smtv1.smt2
 301   regress0/bv/core/bitvec7.smtv1.smt2
 302   regress0/bv/core/bv_eq_diamond10.smtv1.smt2
 303   regress0/bv/core/bv_eq_diamond11.smtv1.smt2
 304   regress0/bv/core/bv_eq_diamond12.smtv1.smt2
 305   regress0/bv/core/bv_eq_diamond13.smtv1.smt2
 306   regress0/bv/core/bv_eq_diamond14.smtv1.smt2
 307   regress0/bv/core/bv_eq_diamond15.smtv1.smt2
 308   regress0/bv/core/bv_eq_diamond16.smtv1.smt2
 309   regress0/bv/core/bv_eq_diamond17.smtv1.smt2
 310   regress0/bv/core/concat-merge-0.smtv1.smt2
 311   regress0/bv/core/concat-merge-1.smtv1.smt2
 312   regress0/bv/core/concat-merge-2.smtv1.smt2
 313   regress0/bv/core/concat-merge-3.smtv1.smt2
 314   regress0/bv/core/constant_core.smt2
 315   regress0/bv/core/equality-00.smtv1.smt2
 316   regress0/bv/core/equality-01.smtv1.smt2
 317   regress0/bv/core/equality-02.smtv1.smt2
 318   regress0/bv/core/equality-04.smtv1.smt2
 319   regress0/bv/core/equality-05.smtv1.smt2
 320   regress0/bv/core/extract-concat-0.smtv1.smt2
 321   regress0/bv/core/extract-concat-1.smtv1.smt2
 322   regress0/bv/core/extract-concat-10.smtv1.smt2
 323   regress0/bv/core/extract-concat-11.smtv1.smt2
 324   regress0/bv/core/extract-concat-2.smtv1.smt2
 325   regress0/bv/core/extract-concat-3.smtv1.smt2
 326   regress0/bv/core/extract-concat-4.smtv1.smt2
 327   regress0/bv/core/extract-concat-5.smtv1.smt2
 328   regress0/bv/core/extract-concat-6.smtv1.smt2
 329   regress0/bv/core/extract-concat-7.smtv1.smt2
 330   regress0/bv/core/extract-concat-8.smtv1.smt2
 331   regress0/bv/core/extract-concat-9.smtv1.smt2
 332   regress0/bv/core/extract-constant.smtv1.smt2
 333   regress0/bv/core/extract-extract-0.smtv1.smt2
 334   regress0/bv/core/extract-extract-1.smtv1.smt2
 335   regress0/bv/core/extract-extract-10.smtv1.smt2
 336   regress0/bv/core/extract-extract-11.smtv1.smt2
 337   regress0/bv/core/extract-extract-2.smtv1.smt2
 338   regress0/bv/core/extract-extract-3.smtv1.smt2
 339   regress0/bv/core/extract-extract-4.smtv1.smt2
 340   regress0/bv/core/extract-extract-5.smtv1.smt2
 341   regress0/bv/core/extract-extract-6.smtv1.smt2
 342   regress0/bv/core/extract-extract-7.smtv1.smt2
 343   regress0/bv/core/extract-extract-8.smtv1.smt2
 344   regress0/bv/core/extract-extract-9.smtv1.smt2
 345   regress0/bv/core/extract-whole-0.smtv1.smt2
 346   regress0/bv/core/extract-whole-1.smtv1.smt2
 347   regress0/bv/core/extract-whole-2.smtv1.smt2
 348   regress0/bv/core/extract-whole-3.smtv1.smt2
 349   regress0/bv/core/extract-whole-4.smtv1.smt2
 350   regress0/bv/core/incremental.smtv1.smt2
 351   regress0/bv/core/slice-01.smtv1.smt2
 352   regress0/bv/core/slice-02.smtv1.smt2
 353   regress0/bv/core/slice-03.smtv1.smt2
 354   regress0/bv/core/slice-04.smtv1.smt2
 355   regress0/bv/core/slice-05.smtv1.smt2
 356   regress0/bv/core/slice-06.smtv1.smt2
 357   regress0/bv/core/slice-07.smtv1.smt2
 358   regress0/bv/core/slice-08.smtv1.smt2
 359   regress0/bv/core/slice-09.smtv1.smt2
 360   regress0/bv/core/slice-10.smtv1.smt2
 361   regress0/bv/core/slice-11.smtv1.smt2
 362   regress0/bv/core/slice-12.smtv1.smt2
 363   regress0/bv/core/slice-13.smtv1.smt2
 364   regress0/bv/core/slice-14.smtv1.smt2
 365   regress0/bv/core/slice-15.smtv1.smt2
 366   regress0/bv/core/slice-16.smtv1.smt2
 367   regress0/bv/core/slice-17.smtv1.smt2
 368   regress0/bv/core/slice-18.smtv1.smt2
 369   regress0/bv/core/slice-19.smtv1.smt2
 370   regress0/bv/core/slice-20.smtv1.smt2
 371   regress0/bv/div_mod.cvc.smt2
 372   regress0/bv/divtest_2_5.smt2
 373   regress0/bv/divtest_2_6.smt2
 374   regress0/bv/eager-force-logic.smt2
 375   regress0/bv/eager-inc-cadical.smt2
 376   regress0/bv/eager-inc-cryptominisat.smt2
 377   regress0/bv/fuzz01.smtv1.smt2
 378   regress0/bv/fuzz02.delta01.smtv1.smt2
 379   regress0/bv/fuzz02.smtv1.smt2
 380   regress0/bv/fuzz03.smtv1.smt2
 381   regress0/bv/fuzz04.smtv1.smt2
 382   regress0/bv/fuzz05.smtv1.smt2
 383   regress0/bv/fuzz06.smtv1.smt2
 384   regress0/bv/fuzz07-delta.smtv1.smt2
 385   regress0/bv/fuzz07.smtv1.smt2
 386   regress0/bv/fuzz08.smtv1.smt2
 387   regress0/bv/fuzz09.smtv1.smt2
 388   regress0/bv/fuzz10.smtv1.smt2
 389   regress0/bv/fuzz11.smtv1.smt2
 390   regress0/bv/fuzz12.smtv1.smt2
 391   regress0/bv/fuzz13.smtv1.smt2
 392   regress0/bv/fuzz14.smtv1.smt2
 393   regress0/bv/fuzz15.delta01.smtv1.smt2
 394   regress0/bv/fuzz16.delta01.smtv1.smt2
 395   regress0/bv/fuzz17.delta01.smtv1.smt2
 396   regress0/bv/fuzz18.delta01.smtv1.smt2
 397   regress0/bv/fuzz18.delta02.smtv1.smt2
 398   regress0/bv/fuzz18.delta03.smtv1.smt2
 399   regress0/bv/fuzz19.delta01.smtv1.smt2
 400   regress0/bv/fuzz20.delta01.smtv1.smt2
 401   regress0/bv/fuzz20.smtv1.smt2
 402   regress0/bv/fuzz21.delta01.smtv1.smt2
 403   regress0/bv/fuzz21.smtv1.smt2
 404   regress0/bv/fuzz22.delta01.smtv1.smt2
 405   regress0/bv/fuzz22.smtv1.smt2
 406   regress0/bv/fuzz23.delta01.smtv1.smt2
 407   regress0/bv/fuzz23.smtv1.smt2
 408   regress0/bv/fuzz24.delta01.smtv1.smt2
 409   regress0/bv/fuzz24.smtv1.smt2
 410   regress0/bv/fuzz25.delta01.smtv1.smt2
 411   regress0/bv/fuzz25.smtv1.smt2
 412   regress0/bv/fuzz26.delta01.smtv1.smt2
 413   regress0/bv/fuzz26.smtv1.smt2
 414   regress0/bv/fuzz27.delta01.smtv1.smt2
 415   regress0/bv/fuzz27.smtv1.smt2
 416   regress0/bv/fuzz28.delta01.smtv1.smt2
 417   regress0/bv/fuzz28.smtv1.smt2
 418   regress0/bv/fuzz29.delta01.smtv1.smt2
 419   regress0/bv/fuzz29.smtv1.smt2
 420   regress0/bv/fuzz30.delta01.smtv1.smt2
 421   regress0/bv/fuzz30.smtv1.smt2
 422   regress0/bv/fuzz31.delta01.smtv1.smt2
 423   regress0/bv/fuzz31.smtv1.smt2
 424   regress0/bv/fuzz32.delta01.smtv1.smt2
 425   regress0/bv/fuzz32.smtv1.smt2
 426   regress0/bv/fuzz33.delta01.smtv1.smt2
 427   regress0/bv/fuzz33.smtv1.smt2
 428   regress0/bv/fuzz34.delta01.smtv1.smt2
 429   regress0/bv/fuzz35.delta01.smtv1.smt2
 430   regress0/bv/fuzz35.smtv1.smt2
 431   regress0/bv/fuzz36.delta01.smtv1.smt2
 432   regress0/bv/fuzz36.smtv1.smt2
 433   regress0/bv/fuzz37.delta01.smtv1.smt2
 434   regress0/bv/fuzz37.smtv1.smt2
 435   regress0/bv/fuzz38.delta01.smtv1.smt2
 436   regress0/bv/fuzz39.delta01.smtv1.smt2
 437   regress0/bv/fuzz39.smtv1.smt2
 438   regress0/bv/fuzz40.delta01.smtv1.smt2
 439   regress0/bv/fuzz40.smtv1.smt2
 440   regress0/bv/fuzz41.smtv1.smt2
 441   regress0/bv/incorrect1.delta01.smtv1.smt2
 442   regress0/bv/inequality00.smt2
 443   regress0/bv/inequality01.smt2
 444   regress0/bv/inequality02.smt2
 445   regress0/bv/inequality03.smt2
 446   regress0/bv/inequality04.smt2
 447   regress0/bv/inequality05.smt2
 448   regress0/bv/int_to_bv_err_on_demand_1.smt2
 449   regress0/bv/int_to_bv_model.smt2
 450   regress0/bv/int_to_bv_model2.smt2
 451   regress0/bv/issue-4075.smt2
 452   regress0/bv/issue-4076.smt2
 453   regress0/bv/issue-4130.smt2
 454   regress0/bv/issue3621.smt2
 455   regress0/bv/issue5396.smt2
 456   regress0/bv/issue8159-1-rewrite-bvneg.smt2
 457   regress0/bv/issue8240-rewrite-bvnot.smt2
 458   regress0/bv/mul-neg-unsat.smt2
 459   regress0/bv/mul-negpow2.smt2
 460   regress0/bv/mult-pow2-negative.smt2
 461   regress0/bv/pr4993-bvugt-bvurem-a.smt2
 462   regress0/bv/pr4993-bvugt-bvurem-b.smt2
 463   regress0/bv/proj-issue343.smt2
 464   regress0/bv/proj-issue438-prerewrite-fixed-point.smt2
 465   regress0/bv/reset-assertions-assert-input.smt2
 466   regress0/bv/sizecheck.cvc.smt2
 467   regress0/bv/smtcompbug.smtv1.smt2
 468   regress0/bv/test-bv_intro_pow2.smt2
 469   regress0/bv/unsound1-reduced.smt2
 470   regress0/chained-equality.smt2
 471   regress0/constant-rewrite.smtv1.smt2
 472   regress0/cores/issue3455.smt2
 473   regress0/cores/issue3651.smt2
 474   regress0/cores/issue4925.smt2
 475   regress0/cores/issue4971-0.smt2
 476   regress0/cores/issue4971-1.smt2
 477   regress0/cores/issue4971-2.smt2
 478   regress0/cores/issue4971-3.smt2
 479   regress0/cores/issue5079.smt2
 480   regress0/cores/issue5234-uc-ua.smt2
 481   regress0/cores/issue5238.smt2
 482   regress0/cores/issue5902.smt2
 483   regress0/cores/issue5908.smt2
 484   regress0/cvc-rerror-print.cvc.smt2
 485   regress0/cvc3-bug15.cvc.smt2
 486   regress0/cvc3.userdoc.01.cvc.smt2
 487   regress0/cvc3.userdoc.02.cvc.smt2
 488   regress0/cvc3.userdoc.03.cvc.smt2
 489   regress0/cvc3.userdoc.04.cvc.smt2
 490   regress0/cvc3.userdoc.05.cvc.smt2
 491   regress0/cvc3.userdoc.06.cvc.smt2
 492   regress0/datatypes/4482-unc-simp-one.smt2
 493   regress0/datatypes/boolean-equality.cvc.smt2
 494   regress0/datatypes/boolean-terms-datatype.cvc.smt2
 495   regress0/datatypes/boolean-terms-parametric-datatype-1.cvc.smt2
 496   regress0/datatypes/boolean-terms-record.cvc.smt2
 497   regress0/datatypes/boolean-terms-rewrite.cvc.smt2
 498   regress0/datatypes/boolean-terms-tuple.cvc.smt2
 499   regress0/datatypes/bug286.cvc.smt2
 500   regress0/datatypes/bug438.cvc.smt2
 501   regress0/datatypes/bug438b.cvc.smt2
 502   regress0/datatypes/bug597-rbt.smt2
 503   regress0/datatypes/bug604.smt2
 504   regress0/datatypes/bug625.smt2
 505   regress0/datatypes/canExp-dtPendingMerge.smt2
 506   regress0/datatypes/cdt-model-cade15.smt2
 507   regress0/datatypes/cdt-non-canon-stream.smt2
 508   regress0/datatypes/coda_simp_model.smt2
 509   regress0/datatypes/conqueue-dt-enum-iloop.smt2
 510   regress0/datatypes/data-nested-codata.smt2
 511   regress0/datatypes/datatype-dump.cvc.smt2
 512   regress0/datatypes/datatype.cvc.smt2
 513   regress0/datatypes/datatype0.cvc.smt2
 514   regress0/datatypes/datatype1.cvc.smt2
 515   regress0/datatypes/datatype13.cvc.smt2
 516   regress0/datatypes/datatype2.cvc.smt2
 517   regress0/datatypes/datatype3.cvc.smt2
 518   regress0/datatypes/datatype4.cvc.smt2
 519   regress0/datatypes/dt-2.6.smt2
 520   regress0/datatypes/dt-different-params.smt2
 521   regress0/datatypes/dt-match-pat-param-2.6.smt2
 522   regress0/datatypes/dt-param-2.6-print.smt2
 523   regress0/datatypes/dt-param-2.6.smt2
 524   regress0/datatypes/dt-param-card4-bool-sat.smt2
 525   regress0/datatypes/dt-sel-2.6.smt2
 526   regress0/datatypes/empty_tuprec.cvc.smt2
 527   regress0/datatypes/example-dailler-min.smt2
 528   regress0/datatypes/is_test.smt2
 529   regress0/datatypes/issue1433.smt2
 530   regress0/datatypes/issue2838.cvc.smt2
 531   regress0/datatypes/issue4393-cdt-model.smt2
 532   regress0/datatypes/issue5280-no-nrec.smt2
 533   regress0/datatypes/jsat-2.6.smt2
 534   regress0/datatypes/list-bool.smt2
 535   regress0/datatypes/list-update.smt2
 536   regress0/datatypes/list-update-sat.smt2
 537   regress0/datatypes/model-subterms-min.smt2
 538   regress0/datatypes/mutual-rec-param-dt.smt2
 539   regress0/datatypes/mutually-recursive.cvc.smt2
 540   regress0/datatypes/pair-bool-bool.cvc.smt2
 541   regress0/datatypes/pair-real-bool.smt2
 542   regress0/datatypes/par-updater-type-rule.smt2
 543   regress0/datatypes/parametric-alt-list.cvc.smt2
 544   regress0/datatypes/proj-issue172.smt2
 545   regress0/datatypes/proj-issue474-app-cons-value.smt2
 546   regress0/datatypes/rec1.cvc.smt2
 547   regress0/datatypes/rec2.cvc.smt2
 548   regress0/datatypes/rec4.cvc.smt2
 549   regress0/datatypes/rewriter.cvc.smt2
 550   regress0/datatypes/sc-cdt1.smt2
 551   regress0/datatypes/some-boolean-tests.cvc.smt2
 552   regress0/datatypes/stream-singleton.smt2
 553   regress0/datatypes/tenum-bug.smt2
 554   regress0/datatypes/Test1-tup-mp.cvc.smt2
 555   regress0/datatypes/tree-get-value.cvc.smt2
 556   regress0/datatypes/tuple-model.cvc.smt2
 557   regress0/datatypes/tuple-no-clash.cvc.smt2
 558   regress0/datatypes/tuple-record-bug.cvc.smt2
 559   regress0/datatypes/tuple.cvc.smt2
 560   regress0/datatypes/tuple_update.smt2
 561   regress0/datatypes/tuples-empty.smt2
 562   regress0/datatypes/tuples-multitype.smt2
 563   regress0/datatypes/typed_v10l30054.cvc.smt2
 564   regress0/datatypes/typed_v1l80005.cvc.smt2
 565   regress0/datatypes/typed_v2l30079.cvc.smt2
 566   regress0/datatypes/typed_v3l20092.cvc.smt2
 567   regress0/datatypes/typed_v5l30069.cvc.smt2
 568   regress0/datatypes/v10l40099.cvc.smt2
 569   regress0/datatypes/v2l40025.cvc.smt2
 570   regress0/datatypes/v3l60006.cvc.smt2
 571   regress0/datatypes/v5l30058.cvc.smt2
 572   regress0/datatypes/wrong-sel-simp.cvc.smt2
 573   regress0/decision/aufbv-fuzz01.smtv1.smt2
 574   regress0/decision/bitvec0.delta01.smtv1.smt2
 575   regress0/decision/bitvec0.smtv1.smt2
 576   regress0/decision/bitvec5.smtv1.smt2
 577   regress0/decision/bug347.smtv1.smt2
 578   regress0/decision/bug374b.smt2
 579   regress0/decision/error122.delta01.smtv1.smt2
 580   regress0/decision/error122.smtv1.smt2
 581   regress0/decision/error20.delta01.smtv1.smt2
 582   regress0/decision/error20.smtv1.smt2
 583   regress0/decision/error3.delta01.smtv1.smt2
 584   regress0/decision/issue8296-sk-def-before-assert.smt2
 585   regress0/decision/pp-regfile.delta01.smtv1.smt2
 586   regress0/decision/pp-regfile.delta02.smtv1.smt2
 587   regress0/decision/quant-ex1.smt2
 588   regress0/decision/uflia-xs-09-16-3-4-1-5.delta03.smtv1.smt2
 589   regress0/decision/wchains010ue.delta02.smtv1.smt2
 590   regress0/declare-fun-is-match.smt2
 591   regress0/declare-funs.smt2
 592   regress0/define-fun-model.smt2
 593   regress0/difficulty-simple.smt2
 594   regress0/difficulty-model-ex.smt2
 595   regress0/distinct.smtv1.smt2
 596   regress0/dump-unsat-core-full.smt2
 597   regress0/echo.smt2
 598   regress0/eqrange0.smt2
 599   regress0/eqrange1.smt2
 600   regress0/eqrange2.smt2
 601   regress0/eqrange3.smt2
 602   regress0/expect/scrub.01.smtv1.smt2
 603   regress0/expect/scrub.03.smt2
 604   regress0/expect/scrub.06.cvc.smt2
 605   regress0/expect/scrub.08.sy
 606   regress0/expect/scrub.09.p
 607   regress0/flet.smtv1.smt2
 608   regress0/flet2.smtv1.smt2
 609   regress0/fmf/array_card.smt2
 610   regress0/fmf/Arrow_Order-smtlib.778341.smtv1.smt2
 611   regress0/fmf/bounded_sets.smt2
 612   regress0/fmf/bug-041417-set-options.cvc.smt2
 613   regress0/fmf/bug782.smt2
 614   regress0/fmf/cruanes-no-minimal-unk.smt2
 615   regress0/fmf/fc-simple.smt2
 616   regress0/fmf/fc-unsat-pent.smt2
 617   regress0/fmf/fc-unsat-tot-2.smt2
 618   regress0/fmf/fd-false.smt2
 619   regress0/fmf/fmc_unsound_model.smt2
 620   regress0/fmf/fmf-strange-bounds-2.smt2
 621   regress0/fmf/forall_unit_data2.smt2
 622   regress0/fmf/issue3661-ccard-dec.smt2
 623   regress0/fmf/issue4850-force-card.smt2
 624   regress0/fmf/issue4872-qf_ufc.smt2
 625   regress0/fmf/issue5239-uf-ss-tot.smt2
 626   regress0/fmf/issue5922-fmf-not-x.smt2
 627   regress0/fmf/krs-sat.smt2
 628   regress0/fmf/no-minimal-sat.smt2
 629   regress0/fmf/QEpres-uf.855035.smtv1.smt2
 630   regress0/fmf/quant_real_univ.cvc.smt2
 631   regress0/fmf/sat-logic.smt2
 632   regress0/fmf/sc_bad_model_1221.smt2
 633   regress0/fmf/sort-infer-typed-082718.smt2
 634   regress0/fmf/syn002-si-real-int.smt2
 635   regress0/fmf/tail_rec.smt2
 636   regress0/fp/abs-unsound.smt2
 637   regress0/fp/abs-unsound2.smt2
 638   regress0/fp/bvcomp-rewrite.smt2
 639   regress0/fp/down-cast-RNA.smt2
 640   regress0/fp/ext-rew-test.smt2
 641   regress0/fp/from_ubv.smt2
 642   regress0/fp/from_sbv.smt2
 643   regress0/fp/issue-5524.smt2
 644   regress0/fp/issue3536.smt2
 645   regress0/fp/issue3582.smt2
 646   regress0/fp/issue3619.smt2
 647   regress0/fp/issue4277-assign-func.smt2
 648   regress0/fp/issue5511.smt2
 649   regress0/fp/issue5734.smt2
 650   regress0/fp/issue6164.smt2
 651   regress0/fp/issue7002.smt2
 652   regress0/fp/issue7569.smt2
 653   regress0/fp/proj-issue329-prereg-context.smt2
 654   regress0/fp/rti_3_5_bug.smt2
 655   regress0/fp/simple.smt2
 656   regress0/fp/word-blast.smt2
 657   regress0/fp/wrong-model.smt2
 658   regress0/fuzz_1.smtv1.smt2
 659   regress0/fuzz_3.smtv1.smt2
 660   regress0/get-value-incremental.smt2
 661   regress0/get-value-ints.smt2
 662   regress0/get-value-no-evaluate.smt2
 663   regress0/get-value-reals-ints.smt2
 664   regress0/get-value-reals.smt2
 665   regress0/ho/apply-collapse-sat.smt2
 666   regress0/ho/apply-collapse-unsat.smt2
 667   regress0/ho/bug_nodbuilding_interpreted_SYO042^1.p
 668   regress0/ho/cong-full-apply.smt2
 669   regress0/ho/cong.smt2
 670   regress0/ho/datatype-field-ho.smt2
 671   regress0/ho/declare-fun-variants.smt2
 672   regress0/ho/def-fun-flatten.smt2
 673   regress0/ho/ext-finite-unsat.smt2
 674   regress0/ho/ext-ho-nested-lambda-model.smt2
 675   regress0/ho/ext-ho.smt2
 676   regress0/ho/ext-sat-partial-eval.smt2
 677   regress0/ho/ext-sat.smt2
 678   regress0/ho/finite-fun-ext.smt2
 679   regress0/ho/fta0144-alpha-eq.smt2
 680   regress0/ho/fta0210.smt2
 681   regress0/ho/fun-subtyping.smt2
 682   regress0/ho/ho-exponential-model.smt2
 683   regress0/ho/ho-match-fun-suffix.smt2
 684   regress0/ho/ho-matching-enum-2.smt2
 685   regress0/ho/ho-matching-enum.smt2
 686   regress0/ho/ho-matching-nested-app.smt2
 687   regress0/ho/ho-std-fmf.smt2
 688   regress0/ho/hoa0008.smt2
 689   regress0/ho/issue4434-const-preserve.smt2
 690   regress0/ho/issue4477.smt2
 691   regress0/ho/issue4990-care-graph.smt2
 692   regress0/ho/issue5233-part1-usort-owner.smt2
 693   regress0/ho/issue5371.smt2
 694   regress0/ho/issue5741-1-cg-model.smt2
 695   regress0/ho/issue5741-3-cg-model.smt2
 696   regress0/ho/issue5744-cg-model.smt2
 697   regress0/ho/issue6526.smt2
 698   regress0/ho/issue6536.smt2
 699   regress0/ho/ite-apply-eq.smt2
 700   regress0/ho/lambda-equality-non-canon.smt2
 701   regress0/ho/lazy-lambda-model.smt2
 702   regress0/ho/match-middle.smt2
 703   regress0/ho/modulo-func-equality.smt2
 704   regress0/ho/qgu-fuzz-ho-1-dd.smt2
 705   regress0/ho/qgu-fuzz-ho-2-dd-no-ext.smt2
 706   regress0/ho/shadowing-defs.smt2
 707   regress0/ho/simple-conf-lazy-lambda-lift.smt2
 708   regress0/ho/simple-conf-lazy-lambda-lift-app.smt2
 709   regress0/ho/simple-matching-partial.smt2
 710   regress0/ho/simple-matching.smt2
 711   regress0/ho/trans.smt2
 712   regress0/hung10_itesdk_output1.smt2
 713   regress0/hung13sdk_output1.smt2
 714   regress0/incorrect1.smtv1.smt2
 715   regress0/ineq_basic.smtv1.smt2
 716   regress0/ineq_slack.smtv1.smt2
 717   regress0/int-to-bv/basic.smt2
 718   regress0/int-to-bv/neg-consts.smt2
 719   regress0/int-to-bv/not-enough-bits.smt2
 720   regress0/int-to-bv/overflow.smt2
 721   regress0/issue1063-overloading-dt-cons.smt2
 722   regress0/issue1063-overloading-dt-fun.smt2
 723   regress0/issue1063-overloading-dt-sel.smt2
 724   regress0/issue2832-qualId.smt2
 725   regress0/issue4010-sort-inf-var.smt2
 726   regress0/issue4469-unc-no-reuse-var.smt2
 727   regress0/issue4707-bv-to-bool-small.smt2
 728   regress0/issue5099-model-1.smt2
 729   regress0/issue5099-model-2.smt2
 730   regress0/issue5144-resetAssertions.smt2
 731   regress0/issue5187-div-justification.smt2
 732   regress0/issue5370.smt2
 733   regress0/issue5462.smt2
 734   regress0/issue5473.smt2
 735   regress0/issue5540-2-dump-model.smt2
 736   regress0/issue5540-model-decls.smt2
 737   regress0/issue5550-num-children.smt2
 738   regress0/issue5736.smt2
 739   regress0/issue5743.smt2
 740   regress0/issue5947.smt2
 741   regress0/issue6605-2-abd-triv.smt2
 742   regress0/issue6738.smt2
 743   regress0/issue6741.smt2
 744   regress0/ite_arith.smt2
 745   regress0/ite_real_int_type.smtv1.smt2
 746   regress0/ite_real_valid.smtv1.smt2
 747   regress0/ite.cvc.smt2
 748   regress0/ite.smt2
 749   regress0/ite2.smt2
 750   regress0/ite3.smt2
 751   regress0/ite4.smt2
 752   regress0/lang_opts_2_6_1.smt2
 753   regress0/lemmas/clocksynchro_5clocks.main_invar.base.model.smtv1.smt2
 754   regress0/lemmas/fs_not_sc_seen.induction.smtv1.smt2
 755   regress0/lemmas/mode_cntrl.induction.smtv1.smt2
 756   regress0/lemmas/sc_init_frame_gap.induction.smtv1.smt2
 757   regress0/let.cvc.smt2
 758   regress0/let.smtv1.smt2
 759   regress0/let2.smtv1.smt2
 760   regress0/logops.01.cvc.smt2
 761   regress0/logops.02.cvc.smt2
 762   regress0/logops.03.cvc.smt2
 763   regress0/logops.04.cvc.smt2
 764   regress0/logops.05.cvc.smt2
 765   regress0/model-core.smt2
 766   regress0/models-print-1.smt2
 767   regress0/models-print-2.smt2
 768   regress0/named-expr-use.smt2
 769   regress0/nl/all-logic.smt2
 770   regress0/nl/coeff-sat.smt2
 771   regress0/nl/combined-uf.smt2
 772   regress0/nl/iand-no-init.smt2
 773   regress0/nl/issue3003.smt2
 774   regress0/nl/issue3407.smt2
 775   regress0/nl/issue3411.smt2
 776   regress0/nl/issue3475.smt2
 777   regress0/nl/issue3652.smt2
 778   regress0/nl/issue3718.smt2
 779   regress0/nl/issue3719.smt2
 780   regress0/nl/issue3729-cm-solved-tf.smt2
 781   regress0/nl/issue3959.smt2
 782   regress0/nl/issue3971.smt2
 783   regress0/nl/issue3991.smt2
 784   regress0/nl/issue4007-rint-uf.smt2
 785   regress0/nl/issue4334-sat-proof-min.smt2
 786   regress0/nl/issue4463-ack-model.smt2
 787   regress0/nl/issue5534-no-assertions.smt2
 788   regress0/nl/issue5726-downpolys.smt2
 789   regress0/nl/issue5726-sqfactor.smt2
 790   regress0/nl/issue5737-div00.smt2
 791   regress0/nl/issue5740-mod00.smt2
 792   regress0/nl/issue5740-2-mod00.smt2
 793   regress0/nl/issue6547-ran-model.smt2
 794   regress0/nl/issue6619-ran-model.smt2
 795   regress0/nl/issue8135-icp-candidates.smt2
 796   regress0/nl/issue8161-var-elim.smt2
 797   regress0/nl/issue8226-ran-refinement.smt2
 798   regress0/nl/lazard-spurious-root.smt2
 799   regress0/nl/magnitude-wrong-1020-m.smt2
 800   regress0/nl/mult-po.smt2
 801   regress0/nl/nia-wrong-tl.smt2
 802   regress0/nl/nlExtPurify-test.smt2
 803   regress0/nl/nta/cos-sig-value.smt2
 804   regress0/nl/nta/exp-n0.5-lb.smt2
 805   regress0/nl/nta/exp-n0.5-ub.smt2
 806   regress0/nl/nta/exp-neg2-unsat-unsound.smt2
 807   regress0/nl/nta/exp1-ub.smt2
 808   regress0/nl/nta/issue4693-inc-purify.smt2
 809   regress0/nl/nta/issue4693-4-inc-purify-sat.smt2
 810   regress0/nl/nta/issue4693-5-inc-purify.smt2
 811   regress0/nl/nta/issue7938-tf-model.smt2
 812   regress0/nl/nta/issue8147-unc-model.smt2
 813   regress0/nl/nta/issue8160-model-purify.smt2
 814   regress0/nl/nta/issue8182-exact-mv-keep.smt2
 815   regress0/nl/nta/issue8182-2-exact-mv-keep.smt2
 816   regress0/nl/nta/issue8183-tc-pi.smt2
 817   regress0/nl/nta/issue8208-red-nred.smt2
 818   regress0/nl/nta/issue8294-2-double-solve.smt2
 819   regress0/nl/nta/proj-issue376.smt2
 820   regress0/nl/nta/proj-issue403.smt2
 821   regress0/nl/nta/proj-issue460-pi-value.smt2
 822   regress0/nl/nta/proj-issue483-arccos-oob.smt2
 823   regress0/nl/nta/real-pi.smt2
 824   regress0/nl/nta/sin-sym.smt2
 825   regress0/nl/nta/sin-sym-schema.smt2
 826   regress0/nl/nta/sqrt-simple.smt2
 827   regress0/nl/nta/tan-rewrite.smt2
 828   regress0/nl/pow2-native-0.smt2
 829   regress0/nl/pow2-native-1.smt2
 830   regress0/nl/pow2-native-2.smt2
 831   regress0/nl/pow2-native-3.smt2
 832   regress0/nl/pow2-pow.smt2
 833   regress0/nl/pow2-pow-isabelle.smt2
 834   regress0/nl/proj-issue-348.smt2
 835   regress0/nl/proj-issue-444-memout-eqelim.smt2
 836   regress0/nl/proj-issue-451-ran-combination-1.smt2
 837   regress0/nl/proj-issue-451-ran-combination-2.smt2
 838   regress0/nl/proj-issue-465-asan-proofs.smt2
 839   regress0/nl/real-as-int.smt2
 840   regress0/nl/real-div-ufnra.smt2
 841   regress0/nl/sin-cos-346-b-chunk-0169.smt2
 842   regress0/nl/sqrt.smt2
 843   regress0/nl/sqrt2-value.smt2
 844   regress0/nl/subs0-unsat-confirm.smt2
 845   regress0/nl/tpp-fail-pf-012921.smt2
 846   regress0/nl/very-easy-sat.smt2
 847   regress0/nl/very-simple-unsat.smt2
 848   regress0/opt-abd-no-use.smt2
 849   regress0/options/ast-and-sexpr.smt2
 850   regress0/options/didyoumean.smt2
 851   regress0/options/help.smt2
 852   regress0/options/interactive-mode.smt2
 853   regress0/options/named_muted.smt2
 854   regress0/options/set-after-init.smt2
 855   regress0/options/set-and-get-options.smt2
 856   regress0/options/statistics.smt2
 857   regress0/options/stream-printing.smt2
 858   regress0/options/version.smt2
 859   regress0/parallel-let.smt2
 860   regress0/parser/as.smt2
 861   regress0/parser/bv_arity_smt2.6.smt2
 862   regress0/parser/bv_nat.smt2
 863   regress0/parser/constraint.smt2
 864   regress0/parser/declarefun-emptyset-uf.smt2
 865   regress0/parser/define_sort.smt2
 866   regress0/parser/force_logic_set_logic.smt2
 867   regress0/parser/force_logic_success.smt2
 868   regress0/parser/get-model-sort-constructor.smt2
 869   regress0/parser/issue5163.smt2
 870   regress0/parser/issue6908-get-value-uc.smt2
 871   regress0/parser/issue7274.smt2
 872   regress0/parser/issue7860-parse-only-reset.smt2
 873   regress0/parser/issue7894-parse-error-assoc.smt2
 874   regress0/parser/issue8377-resolve-indexed.smt2
 875   regress0/parser/linear_arithmetic_err1.smt2
 876   regress0/parser/linear_arithmetic_err2.smt2
 877   regress0/parser/linear_arithmetic_err3.smt2
 878   regress0/parser/named-attr-error.smt2
 879   regress0/parser/named-attr.smt2
 880   regress0/parser/proj-issue370-push-pop-global.smt2
 881   regress0/parser/quoted-define-fun.smt2
 882   regress0/parser/shadow_fun_symbol_all.smt2
 883   regress0/parser/shadow_fun_symbol_nirat.smt2
 884   regress0/parser/strings20.smt2
 885   regress0/parser/strings25.smt2
 886   regress0/parser/to_fp.smt2
 887   regress0/precedence/and-not.cvc.smt2
 888   regress0/precedence/and-xor.cvc.smt2
 889   regress0/precedence/bool-cmp.cvc.smt2
 890   regress0/precedence/cmp-plus.cvc.smt2
 891   regress0/precedence/eq-fun.cvc.smt2
 892   regress0/precedence/iff-assoc.cvc.smt2
 893   regress0/precedence/iff-implies.cvc.smt2
 894   regress0/precedence/implies-assoc.cvc.smt2
 895   regress0/precedence/implies-iff.cvc.smt2
 896   regress0/precedence/implies-or.cvc.smt2
 897   regress0/precedence/not-and.cvc.smt2
 898   regress0/precedence/not-eq.cvc.smt2
 899   regress0/precedence/or-implies.cvc.smt2
 900   regress0/precedence/or-xor.cvc.smt2
 901   regress0/precedence/plus-mult.cvc.smt2
 902   regress0/precedence/xor-and.cvc.smt2
 903   regress0/precedence/xor-assoc.cvc.smt2
 904   regress0/precedence/xor-or.cvc.smt2
 905   regress0/preprocess/circuit-prop.smt2
 906   regress0/preprocess/issue5729-rewritten-assertions.smt2
 907   regress0/preprocess/issue5943-non-clausal-simp.smt2
 908   regress0/preprocess/issue6754-tpp.smt2
 909   regress0/preprocess/preprocess_00.cvc.smt2
 910   regress0/preprocess/preprocess_01.cvc.smt2
 911   regress0/preprocess/preprocess_02.cvc.smt2
 912   regress0/preprocess/preprocess_03.cvc.smt2
 913   regress0/preprocess/preprocess_04.cvc.smt2
 914   regress0/preprocess/preprocess_05.cvc.smt2
 915   regress0/preprocess/preprocess_06.cvc.smt2
 916   regress0/preprocess/preprocess_07.cvc.smt2
 917   regress0/preprocess/preprocess_08.cvc.smt2
 918   regress0/preprocess/preprocess_09.cvc.smt2
 919   regress0/preprocess/preprocess_10.cvc.smt2
 920   regress0/preprocess/preprocess_11.cvc.smt2
 921   regress0/preprocess/preprocess_12.cvc.smt2
 922   regress0/preprocess/preprocess_13.cvc.smt2
 923   regress0/preprocess/preprocess_14.cvc.smt2
 924   regress0/preprocess/preprocess_15.cvc.smt2
 925   regress0/preprocess/proj-issue304-circuit-prop-xor.smt2
 926   regress0/preprocess/proj-issue305-circuit-prop-ite-a.smt2
 927   regress0/preprocess/proj-issue305-circuit-prop-ite-b.smt2
 928   regress0/preprocess/proj-issue305-circuit-prop-ite-c.smt2
 929   regress0/preprocess/proj-issue305-circuit-prop-ite-d.smt2
 930   regress0/preprocess/proj-issue309-circuit-prop-ite.smt2
 931   regress0/preprocess/proj-issue332-circuit-prop-xor.smt2
 932   regress0/print_define_fun_internal.smt2
 933   regress0/print_lambda.cvc.smt2
 934   regress0/print_model.cvc.smt2
 935   regress0/printer/bv_consts_bin.smt2
 936   regress0/printer/bv_consts_dec.smt2
 937   regress0/printer/empty_sort.smt2
 938   regress0/printer/empty_symbol_name.smt2
 939   regress0/printer/learned-lit-output.smt2
 940   regress0/printer/let_shadowing.smt2
 941   regress0/printer/post-asserts-output.smt2
 942   regress0/printer/pre-asserts-output.smt2
 943   regress0/printer/print_subs.smt2
 944   regress0/printer/symbol_starting_w_digit.smt2
 945   regress0/printer/tuples_and_records.cvc.smt2
 946   regress0/proj-issue307-get-value-re.smt2
 947   regress0/proofs/cyclic-ucp.smt2
 948   regress0/proofs/issue277-circuit-propagator.smt2
 949   regress0/proofs/lfsc-test-1.smt2
 950   regress0/proofs/open-pf-datatypes.smt2
 951   regress0/proofs/open-pf-if-unordered-iff.smt2
 952   regress0/proofs/open-pf-rederivation.smt2
 953   regress0/proofs/project-issue317-inc-sat-conflictlit.smt2
 954   regress0/proofs/project-issue330-eqproof.smt2
 955   regress0/proofs/proj-issue326-nl-bounds-check.smt2
 956   regress0/proofs/proj-issue342-eager-checking-no-proof-checking.smt2
 957   regress0/proofs/proj-issue430-coverings-double-negation.smt2
 958   regress0/proofs/proj-issue462-sat-proof-option.smt2
 959   regress0/proofs/proj-issue468-mkScope.smt2
 960   regress0/proofs/proj-issue492-skolem-lemma-pf.smt2
 961   regress0/proofs/qgu-fuzz-1-bool-sat.smt2
 962   regress0/proofs/qgu-fuzz-2-bool-chainres-checking.smt2
 963   regress0/proofs/qgu-fuzz-3-chainres-checking.smt2
 964   regress0/proofs/qgu-fuzz-4-bool-chainres-postprocessing-singleton.smt2
 965   regress0/proofs/qgu-fuzz-5-bool-open-sat.smt2
 966   regress0/proofs/scope.smt2
 967   regress0/proofs/trust-subs-eq-open.smt2
 968   regress0/push-pop/boolean/fuzz_12.smt2
 969   regress0/push-pop/boolean/fuzz_13.smt2
 970   regress0/push-pop/boolean/fuzz_14.smt2
 971   regress0/push-pop/boolean/fuzz_18.smt2
 972   regress0/push-pop/boolean/fuzz_2.smt2
 973   regress0/push-pop/boolean/fuzz_21.smt2
 974   regress0/push-pop/boolean/fuzz_22.smt2
 975   regress0/push-pop/boolean/fuzz_27.smt2
 976   regress0/push-pop/boolean/fuzz_3.smt2
 977   regress0/push-pop/boolean/fuzz_31.smt2
 978   regress0/push-pop/boolean/fuzz_33.smt2
 979   regress0/push-pop/boolean/fuzz_36.smt2
 980   regress0/push-pop/boolean/fuzz_38.smt2
 981   regress0/push-pop/boolean/fuzz_46.smt2
 982   regress0/push-pop/boolean/fuzz_47.smt2
 983   regress0/push-pop/boolean/fuzz_48.smt2
 984   regress0/push-pop/boolean/fuzz_49.smt2
 985   regress0/push-pop/boolean/fuzz_50.smt2
 986   regress0/push-pop/bug1990.smt2
 987   regress0/push-pop/bug233.cvc.smt2
 988   regress0/push-pop/bug654-dd.smt2
 989   regress0/push-pop/bug691.smt2
 990   regress0/push-pop/bug821-check_sat_assuming.smt2
 991   regress0/push-pop/bug821.smt2
 992   regress0/push-pop/inc-define.smt2
 993   regress0/push-pop/inc-double-u.smt2
 994   regress0/push-pop/incremental-subst-bug.cvc.smt2
 995   regress0/push-pop/issue1986.smt2
 996   regress0/push-pop/issue2137.min.smt2
 997   regress0/push-pop/issue6535-inc-solve.smt2
 998   regress0/push-pop/issue7479-global-decls.smt2
 999   regress0/push-pop/quant-fun-proc-unfd.smt2
1000   regress0/push-pop/real-as-int-incremental.smt2
1001   regress0/push-pop/simple_unsat_cores.smt2
1002   regress0/push-pop/test.00.cvc.smt2
1003   regress0/push-pop/test.01.cvc.smt2
1004   regress0/push-pop/tiny_bug.smt2
1005   regress0/push-pop/units.cvc.smt2
1006   regress0/quantifiers/agg-rew-test-cf.smt2
1007   regress0/quantifiers/agg-rew-test.smt2
1008   regress0/quantifiers/ari056.smt2
1009   regress0/quantifiers/ARI176e1.smt2
1010   regress0/quantifiers/bug269.smt2
1011   regress0/quantifiers/bug290.smt2
1012   regress0/quantifiers/bug291.smt2
1013   regress0/quantifiers/bug749-rounding.smt2
1014   regress0/quantifiers/cbqi-lia-dt-simp.smt2
1015   regress0/quantifiers/cegqi-needs-justify.smt2
1016   regress0/quantifiers/cegqi-nl-simp.cvc.smt2
1017   regress0/quantifiers/cegqi-nl-sq.smt2
1018   regress0/quantifiers/cegqi-par-dt-simple.smt2
1019   regress0/quantifiers/clock-10.smt2
1020   regress0/quantifiers/clock-3.smt2
1021   regress0/quantifiers/cond-var-elim-binary.smt2
1022   regress0/quantifiers/delta-simp.smt2
1023   regress0/quantifiers/double-pattern.smt2
1024   regress0/quantifiers/ex3.smt2
1025   regress0/quantifiers/ex6.smt2
1026   regress0/quantifiers/floor.smt2
1027   regress0/quantifiers/horn-ground-pre-post.smt2
1028   regress0/quantifiers/is-even-pred.smt2
1029   regress0/quantifiers/is-int.smt2
1030   regress0/quantifiers/issue1805.smt2
1031   regress0/quantifiers/issue2031-bv-var-elim.smt2
1032   regress0/quantifiers/issue2033-macro-arith.smt2
1033   regress0/quantifiers/issue2035.smt2
1034   regress0/quantifiers/issue3655.smt2
1035   regress0/quantifiers/issue4086-infs.smt2
1036   regress0/quantifiers/issue4275-qcf-cegqi-rep.smt2
1037   regress0/quantifiers/issue4437-unc-quant.smt2
1038   regress0/quantifiers/issue4576.smt2
1039   regress0/quantifiers/issue5645-dt-cm-spurious.smt2
1040   regress0/quantifiers/issue5693-prenex.smt2
1041   regress0/quantifiers/issue6475-rr-const.smt2
1042   regress0/quantifiers/issue6603-dt-bool-cegqi.smt2
1043   regress0/quantifiers/issue6838-qpdt.smt2
1044   regress0/quantifiers/issue6996-trivial-elim.smt2
1045   regress0/quantifiers/issue6999-deq-elim.smt2
1046   regress0/quantifiers/issue7353-var-elim-par-dt.smt2
1047   regress0/quantifiers/issue8001-mem-leak.smt2
1048   regress0/quantifiers/issue8159-3-qext-nterm.smt2
1049   regress0/quantifiers/issue8227-subs-shadow.smt2
1050   regress0/quantifiers/lra-triv-gn.smt2
1051   regress0/quantifiers/macro-back-subs-sat.smt2
1052   regress0/quantifiers/macros-int-real.smt2
1053   regress0/quantifiers/macros-real-arg.smt2
1054   regress0/quantifiers/matching-lia-1arg.smt2
1055   regress0/quantifiers/mix-complete-strat.smt2
1056   regress0/quantifiers/mix-match.smt2
1057   regress0/quantifiers/mix-simp.smt2
1058   regress0/quantifiers/nested-delta.smt2
1059   regress0/quantifiers/nested-inf.smt2
1060   regress0/quantifiers/partial-trigger.smt2
1061   regress0/quantifiers/proj-issue152-2-non-std-nterm-ext-rew.smt2
1062   regress0/quantifiers/pure_dt_cbqi.smt2
1063   regress0/quantifiers/qarray-sel-over-store.smt2
1064   regress0/quantifiers/qbv-inequality2.smt2
1065   regress0/quantifiers/qbv-multi-lit-uge.smt2
1066   regress0/quantifiers/qbv-simp.smt2
1067   regress0/quantifiers/qbv-test-invert-bvadd-neq.smt2
1068   regress0/quantifiers/qbv-test-invert-bvand-neq.smt2
1069   regress0/quantifiers/qbv-test-invert-bvand.smt2
1070   regress0/quantifiers/qbv-test-invert-bvashr-0-neq.smt2
1071   regress0/quantifiers/qbv-test-invert-bvashr-1-neq.smt2
1072   regress0/quantifiers/qbv-test-invert-bvlshr-0-neq.smt2
1073   regress0/quantifiers/qbv-test-invert-bvlshr-0.smt2
1074   regress0/quantifiers/qbv-test-invert-bvlshr-1-neq.smt2
1075   regress0/quantifiers/qbv-test-invert-bvor-neq.smt2
1076   regress0/quantifiers/qbv-test-invert-bvor.smt2
1077   regress0/quantifiers/qbv-test-invert-bvshl-0-neq.smt2
1078   regress0/quantifiers/qbv-test-invert-bvshl-0.smt2
1079   regress0/quantifiers/qbv-test-invert-bvult-1.smt2
1080   regress0/quantifiers/qbv-test-invert-bvxor-neq.smt2
1081   regress0/quantifiers/qbv-test-invert-bvxor.smt2
1082   regress0/quantifiers/qbv-test-invert-concat-0-neq.smt2
1083   regress0/quantifiers/qbv-test-invert-concat-0.smt2
1084   regress0/quantifiers/qbv-test-invert-concat-1-neq.smt2
1085   regress0/quantifiers/qbv-test-invert-concat-1.smt2
1086   regress0/quantifiers/qbv-test-invert-sign-extend.smt2
1087   regress0/quantifiers/qcf-rel-dom-opt.smt2
1088   regress0/quantifiers/quant-model-simplification.smt2
1089   regress0/quantifiers/rew-to-scala.smt2
1090   regress0/quantifiers/selector-trigger.smt2
1091   regress0/quantifiers/simp-len.smt2
1092   regress0/quantifiers/simp-typ-test.smt2
1093   regress0/quantifiers/ufnia-fv-delta.smt2
1094   regress0/quantifiers/veqt-delta.smt2
1095   regress0/rec-fun-const-parse-bug.smt2
1096   regress0/rels/addr_book_0.cvc.smt2
1097   regress0/rels/atom_univ2.cvc.smt2
1098   regress0/rels/card_transpose.cvc.smt2
1099   regress0/rels/iden_0.cvc.smt2
1100   regress0/rels/iden_1.cvc.smt2
1101   regress0/rels/join-eq-u-sat.cvc.smt2
1102   regress0/rels/join-eq-u.cvc.smt2
1103   regress0/rels/joinImg_0.cvc.smt2
1104   regress0/rels/oneLoc_no_quant-int_0_1.cvc.smt2
1105   regress0/rels/qgu-fuzz-relations-1.smt2
1106   regress0/rels/qgu-fuzz-relations-1-dd.smt2
1107   regress0/rels/rel_1tup_0.cvc.smt2
1108   regress0/rels/rel_complex_0.cvc.smt2
1109   regress0/rels/rel_complex_1.cvc.smt2
1110   regress0/rels/rel_conflict_0.cvc.smt2
1111   regress0/rels/rel_join_0_1.cvc.smt2
1112   regress0/rels/rel_join_0.cvc.smt2
1113   regress0/rels/rel_join_1_1.cvc.smt2
1114   regress0/rels/rel_join_1.cvc.smt2
1115   regress0/rels/rel_join_2_1.cvc.smt2
1116   regress0/rels/rel_join_2.cvc.smt2
1117   regress0/rels/rel_join_3_1.cvc.smt2
1118   regress0/rels/rel_join_3.cvc.smt2
1119   regress0/rels/rel_join_4.cvc.smt2
1120   regress0/rels/rel_join_5.cvc.smt2
1121   regress0/rels/rel_join_6.cvc.smt2
1122   regress0/rels/rel_join_7.cvc.smt2
1123   regress0/rels/rel_product_0_1.cvc.smt2
1124   regress0/rels/rel_product_0.cvc.smt2
1125   regress0/rels/rel_product_1_1.cvc.smt2
1126   regress0/rels/rel_product_1.cvc.smt2
1127   regress0/rels/rel_symbolic_1_1.cvc.smt2
1128   regress0/rels/rel_symbolic_1.cvc.smt2
1129   regress0/rels/rel_symbolic_2_1.cvc.smt2
1130   regress0/rels/rel_symbolic_3_1.cvc.smt2
1131   regress0/rels/rel_tc_11.cvc.smt2
1132   regress0/rels/rel_tc_2_1.cvc.smt2
1133   regress0/rels/rel_tc_3_1.cvc.smt2
1134   regress0/rels/rel_tc_3.cvc.smt2
1135   regress0/rels/rel_tc_8.cvc.smt2
1136   regress0/rels/rel_tp_3_1.cvc.smt2
1137   regress0/rels/rel_tp_join_0.cvc.smt2
1138   regress0/rels/rel_tp_join_1.cvc.smt2
1139   regress0/rels/rel_tp_join_2.cvc.smt2
1140   regress0/rels/rel_tp_join_3.cvc.smt2
1141   regress0/rels/rel_tp_join_eq_0.cvc.smt2
1142   regress0/rels/rel_tp_join_int_0.cvc.smt2
1143   regress0/rels/rel_tp_join_pro_0.cvc.smt2
1144   regress0/rels/rel_tp_join_var_0.cvc.smt2
1145   regress0/rels/rel_transpose_0.cvc.smt2
1146   regress0/rels/rel_transpose_1_1.cvc.smt2
1147   regress0/rels/rel_transpose_1.cvc.smt2
1148   regress0/rels/rel_transpose_3.cvc.smt2
1149   regress0/rels/rel_transpose_4.cvc.smt2
1150   regress0/rels/rel_transpose_5.cvc.smt2
1151   regress0/rels/rel_transpose_6.cvc.smt2
1152   regress0/rels/rel_transpose_7.cvc.smt2
1153   regress0/rels/relations-ops.smt2
1154   regress0/rels/rels-sharing-simp.cvc.smt2
1155   regress0/sep/dispose-1.smt2
1156   regress0/sep/dup-nemp.smt2
1157   regress0/sep/issue3720-check-model.smt2
1158   regress0/sep/issue5343-err.smt2
1159   regress0/sep/nemp.smt2
1160   regress0/sep/nil-no-elim.smt2
1161   regress0/sep/nspatial-simp.smt2
1162   regress0/sep/pto-01.smt2
1163   regress0/sep/pto-02.smt2
1164   regress0/sep/sep-01.smt2
1165   regress0/sep/sep-plus1.smt2
1166   regress0/sep/sep-simp-unsat-emp.smt2
1167   regress0/sep/simple-080420-const-sets.smt2
1168   regress0/sep/skolem_emp.smt2
1169   regress0/sep/trees-1.smt2
1170   regress0/sep/wand-crash.smt2
1171   regress0/seq/err1.smt2
1172   regress0/seq/intseq.smt2
1173   regress0/seq/intseq_dt.smt2
1174   regress0/seq/issue4370-bool-terms.smt2
1175   regress0/seq/issue5543-unit-cmv.smt2
1176   regress0/seq/issue5547-seq-len-unit.smt2
1177   regress0/seq/issue5547-small-seq-len-unit.smt2
1178   regress0/seq/issue5665-invalid-model.smt2
1179   regress0/seq/issue6337-seq.smt2
1180   regress0/seq/issue8133-block-const-elems.smt2
1181   regress0/seq/len_simplify.smt2
1182   regress0/seq/mixed-types-seq-nth.smt2
1183   regress0/seq/nth-oob.smt2
1184   regress0/seq/nth-unit.smt2
1185   regress0/seq/nth-update.smt2
1186   regress0/seq/proj-issue340.smt2
1187   regress0/seq/proj-issue384-subtypes.smt2
1188   regress0/seq/proj-issue384-2-subtypes.smt2
1189   regress0/seq/proj-issue427-subtypes-value.smt2
1190   regress0/seq/quant_len_trigger.smt2
1191   regress0/seq/query0-subtype-skel.smt2
1192   regress0/seq/query1-subtype.smt2
1193   regress0/seq/query2-subtype.smt2
1194   regress0/seq/rev.smt2
1195   regress0/seq/seqa-model-unsound-dd.smt2
1196   regress0/seq/array/array1.smt2
1197   regress0/seq/array/array2.smt2
1198   regress0/seq/array/array3.smt2
1199   regress0/seq/array/array4.smt2
1200   regress0/seq/array/distinct-update.smt2
1201   regress0/seq/array/model-dd-1220.smt2
1202   regress0/seq/array/nth-concat.smt2
1203   regress0/seq/array/update-fallback.smt2
1204   regress0/seq/array/update-word-eq.smt2
1205   regress0/seq/issue6005-no-strings-exp.smt2
1206   regress0/seq/seq-2var.smt2
1207   regress0/seq/seq-ex1.smt2
1208   regress0/seq/seq-ex2.smt2
1209   regress0/seq/seq-ex3.smt2
1210   regress0/seq/seq-ex4.smt2
1211   regress0/seq/seq-ex5-dd.smt2
1212   regress0/seq/seq-ex5.smt2
1213   regress0/seq/seq-expand-defs.smt2
1214   regress0/seq/seq-nemp.smt2
1215   regress0/seq/seq-nth-type-check.smt2
1216   regress0/seq/seq-nth-uf-z.smt2
1217   regress0/seq/seq-nth-uf.smt2
1218   regress0/seq/seq-nth-undef-unsat.smt2
1219   regress0/seq/seq-nth.smt2
1220   regress0/seq/seq-rewrites.smt2
1221   regress0/seq/seq-types.smt2
1222   regress0/seq/shared-term-registration.smt2
1223   regress0/seq/update-concat-non-atomic.smt2
1224   regress0/seq/update-concat-non-atomic2.smt2
1225   regress0/seq/update-eq.smt2
1226   regress0/seq/update-eq-unsat.smt2
1227   regress0/seq/wrong-model-020322.smt2
1228   regress0/seq/wrong-sat-020322.smt2
1229   regress0/sets/abt-min.smt2
1230   regress0/sets/abt-te-exh.smt2
1231   regress0/sets/abt-te-exh2.smt2
1232   regress0/sets/card-2.smt2
1233   regress0/sets/card-3sets.cvc.smt2
1234   regress0/sets/card.smt2
1235   regress0/sets/card3-ground.smt2
1236   regress0/sets/comp-qf-error.smt2
1237   regress0/sets/complement.cvc.smt2
1238   regress0/sets/complement2.cvc.smt2
1239   regress0/sets/complement3.cvc.smt2
1240   regress0/sets/cvc-sample.cvc.smt2
1241   regress0/sets/dt-simp-mem.smt2
1242   regress0/sets/emptyset.smt2
1243   regress0/sets/eqtest.smt2
1244   regress0/sets/error1.smt2
1245   regress0/sets/error2.smt2
1246   regress0/sets/insert.smt2
1247   regress0/sets/int-real-univ-unsat.smt2
1248   regress0/sets/int-real-univ.smt2
1249   regress0/sets/issue5400-card-minus-univ.smt2
1250   regress0/sets/issue5400-2-card-minus-univ.smt2
1251   regress0/sets/issue5402-1-card.smt2
1252   regress0/sets/issue5402-2-card-finite.smt2
1253   regress0/sets/jan24/deepmeas0.hs.fqout.cvc4.47.smt2
1254   regress0/sets/jan24/deepmeas0.hs.fqout.small.smt2
1255   regress0/sets/jan27/ListConcat.hs.fqout.177minimized.smt2
1256   regress0/sets/jan27/ListConcat.hs.fqout.cvc4.177.smt2
1257   regress0/sets/jan28/TalkingAboutSets.hs.fqout.3577minimized.smt2
1258   regress0/sets/jan30/UniqueZipper.hs.fqout.minimized10.smt2
1259   regress0/sets/jan30/UniqueZipper.hs.fqout.minimized1832.smt2
1260   regress0/sets/mar2014/sharing-preregister.smt2
1261   regress0/sets/mar2014/small.smt2
1262   regress0/sets/mar2014/smaller.smt2
1263   regress0/sets/nonvar-univ.smt2
1264   regress0/sets/pre-proc-univ.smt2
1265   regress0/sets/proj-issue177.smt2
1266   regress0/sets/proj-issue486-sets-split-eq.smt2
1267   regress0/sets/proj-issue493-choose-det.smt2
1268   regress0/sets/proj-issue501-choose-bool-term-var.smt2
1269   regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2
1270   regress0/sets/setel-eq.smt2
1271   regress0/sets/sets-deq-dd.smt2
1272   regress0/sets/sets-equal.smt2
1273   regress0/sets/sets-extr.smt2
1274   regress0/sets/sets-inter.smt2
1275   regress0/sets/sets-new.smt2
1276   regress0/sets/sets-of-sets-subtypes.smt2
1277   regress0/sets/sets-poly-int-real.smt2
1278   regress0/sets/sets-poly-nonint.smt2
1279   regress0/sets/sets-sample.smt2
1280   regress0/sets/sets-sharing.smt2
1281   regress0/sets/sets-testlemma-ints.smt2
1282   regress0/sets/sets-testlemma-reals.smt2
1283   regress0/sets/sets-testlemma.smt2
1284   regress0/sets/sets-union.smt2
1285   regress0/sets/sharing-simp.smt2
1286   regress0/sets/union-1a-flip.smt2
1287   regress0/sets/union-1a.smt2
1288   regress0/sets/union-1b-flip.smt2
1289   regress0/sets/union-1b.smt2
1290   regress0/sets/union-2.smt2
1291   regress0/sets/univset-simp.smt2
1292   regress0/simple-dump-model.smt2
1293   regress0/simple-lra.smt2
1294   regress0/simple-lra.smtv1.smt2
1295   regress0/simple-rdl.smt2
1296   regress0/simple-rdl.smtv1.smt2
1297   regress0/simple-uf.smt2
1298   regress0/simple-uf.smtv1.smt2
1299   regress0/simple.cvc.smt2
1300   regress0/simple.smtv1.smt2
1301   regress0/simple2.smtv1.smt2
1302   regress0/simplification_bug.smtv1.smt2
1303   regress0/simplification_bug2.smtv1.smt2
1304   regress0/smallcnf.cvc.smt2
1305   regress0/smt2output.smt2
1306   regress0/smtlib/define-fun-rec-logic.smt2
1307   regress0/smtlib/get-unsat-assumptions.smt2
1308   regress0/smtlib/global-decls.smt2
1309   regress0/smtlib/issue4028.smt2
1310   regress0/smtlib/issue4077.smt2
1311   regress0/smtlib/issue4151.smt2
1312   regress0/smtlib/issue4552.smt2
1313   regress0/smtlib/issue4866.smt2
1314   regress0/smtlib/reason-unknown.smt2
1315   regress0/smtlib/reset-assertions-global.smt2
1316   regress0/smtlib/reset-assertions1.smt2
1317   regress0/smtlib/reset-assertions2.smt2
1318   regress0/smtlib/reset-force-logic.smt2
1319   regress0/smtlib/reset-set-logic.smt2
1320   regress0/smtlib/reset.smt2
1321   regress0/smtlib/set-info-status.smt2
1322   regress0/strings/bug001.smt2
1323   regress0/strings/bug002.smt2
1324   regress0/strings/bug612.smt2
1325   regress0/strings/bug613.smt2
1326   regress0/strings/char-representations.smt2
1327   regress0/strings/code-eval.smt2
1328   regress0/strings/code-perf.smt2
1329   regress0/strings/code-sat-neg-one.smt2
1330   regress0/strings/complement-simple.smt2
1331   regress0/strings/delta-trust-subs.smt2
1332   regress0/strings/distinct-witness-id.smt2
1333   regress0/strings/escchar_25.smt2
1334   regress0/strings/escchar.smt2
1335   regress0/strings/from_code.smt2
1336   regress0/strings/gen-esc-seq.smt2
1337   regress0/strings/hconst-092618.smt2
1338   regress0/strings/idof-rewrites.smt2
1339   regress0/strings/idof-sem.smt2
1340   regress0/strings/ilc-like.smt2
1341   regress0/strings/indexof-sym-simp.smt2
1342   regress0/strings/indexof_re.smt2
1343   regress0/strings/indexof_re-start-index.smt2
1344   regress0/strings/is_digit_simple.smt2
1345   regress0/strings/issue1189.smt2
1346   regress0/strings/issue2958.smt2
1347   regress0/strings/issue3440.smt2
1348   regress0/strings/issue3497.smt2
1349   regress0/strings/issue3657-evalLeq.smt2
1350   regress0/strings/issue4070.smt2
1351   regress0/strings/issue4376.smt2
1352   regress0/strings/issue4662-consume-nterm.smt2
1353   regress0/strings/issue4674-recomp-nf.smt2
1354   regress0/strings/issue4820.smt2
1355   regress0/strings/issue4915.smt2
1356   regress0/strings/issue5090.smt2
1357   regress0/strings/issue5384-double-conflict.smt2
1358   regress0/strings/issue5428-re-diff-assoc.smt2
1359   regress0/strings/issue5508-multiple-conflicts.smt2
1360   regress0/strings/issue5542-strings-seq-mix.smt2
1361   regress0/strings/issue5608-eager-pp.smt2
1362   regress0/strings/issue5666-orig-unit-deq.smt2
1363   regress0/strings/issue5666-unit-deq.smt2
1364   regress0/strings/issue5745-eager-pp.smt2
1365   regress0/strings/issue5767-eager-pp.smt2
1366   regress0/strings/issue5771-eager-pp.smt2
1367   regress0/strings/issue5815-ndet-string-ent.smt2
1368   regress0/strings/issue5816-re-kind.smt2
1369   regress0/strings/issue5915-repl-ctn-rewrite.smt2
1370   regress0/strings/issue6203-3-unfold-trivial-true.smt2
1371   regress0/strings/issue6510-seq-bool.smt2
1372   regress0/strings/issue6520.smt2
1373   regress0/strings/issue6560-indexof-reduction.smt2
1374   regress0/strings/issue6604-re-elim.smt2
1375   regress0/strings/issue6643-ctn-decompose-conflict.smt2
1376   regress0/strings/issue6681-split-eq-strip-l.smt2
1377   regress0/strings/issue6834-str-eq-const-nhomog.smt2
1378   regress0/strings/issue7974-incomplete-neg-member.smt2
1379   regress0/strings/issue8295-star-union-char.smt2
1380   regress0/strings/issue8346-idof-max.smt2
1381   regress0/strings/itos-entail.smt2
1382   regress0/strings/large-model.smt2
1383   regress0/strings/leadingzero001.smt2
1384   regress0/strings/leq.smt2
1385   regress0/strings/loop-wrong-sem.smt2
1386   regress0/strings/loop001.smt2
1387   regress0/strings/model-code-point.smt2
1388   regress0/strings/model-friendly.smt2
1389   regress0/strings/model001.smt2
1390   regress0/strings/ncontrib-rewrites.smt2
1391   regress0/strings/norn-31.smt2
1392   regress0/strings/norn-simp-rew.smt2
1393   regress0/strings/parser-syms.cvc.smt2
1394   regress0/strings/proj-issue316-regexp-ite.smt2
1395   regress0/strings/proj-issue390-update-rev-rewrite.smt2
1396   regress0/strings/proj-issue409-re-loop-none.smt2
1397   regress0/strings/quad-028-2-2-unsat.smt2
1398   regress0/strings/quad-138-4-2-unsat.smt2
1399   regress0/strings/re_diff.smt2
1400   regress0/strings/re-in-rewrite.smt2
1401   regress0/strings/re-syntax.smt2
1402   regress0/strings/re.all.smt2
1403   regress0/strings/regexp_inclusion_reduction.smt2
1404   regress0/strings/regexp_inclusion.smt2
1405   regress0/strings/regexp-native-simple.cvc.smt2
1406   regress0/strings/repl-rewrites2.smt2
1407   regress0/strings/replace-const.smt2
1408   regress0/strings/replaceall-eval.smt2
1409   regress0/strings/rewrites-re-concat.smt2
1410   regress0/strings/rewrites-v2.smt2
1411   regress0/strings/std2.6.1.smt2
1412   regress0/strings/str_unsound_ext_rew_eq.smt2
1413   regress0/strings/str-rev-simple.smt2
1414   regress0/strings/str003.smt2
1415   regress0/strings/str004.smt2
1416   regress0/strings/str005.smt2
1417   regress0/strings/strings-charat.cvc.smt2
1418   regress0/strings/strings-native-simple.cvc.smt2
1419   regress0/strings/strip-endpoint-itos.smt2
1420   regress0/strings/substr-rewrites.smt2
1421   regress0/strings/tolower-rrs.smt2
1422   regress0/strings/tolower-simple.smt2
1423   regress0/strings/type001.smt2
1424   regress0/strings/unicode-esc.smt2
1425   regress0/strings/unsound-0908.smt2
1426   regress0/strings/unsound-repl-rewrite.smt2
1427   regress0/sygus/assume-simple.sy
1428   regress0/sygus/array-grammar-select.sy
1429   regress0/sygus/ccp16.lus.sy
1430   regress0/sygus/cegqi-si-string-triv-2fun.sy
1431   regress0/sygus/cegqi-si-string-triv.sy
1432   regress0/sygus/check-generic-red.sy
1433   regress0/sygus/const-var-test.sy
1434   regress0/sygus/dt-no-syntax.sy
1435   regress0/sygus/dt-sel-parse1.sy
1436   regress0/sygus/General_plus10.sy
1437   regress0/sygus/hd-05-d1-prog-nogrammar.sy
1438   regress0/sygus/ho-occ-synth-fun.sy
1439   regress0/sygus/incremental-modify-ex.sy
1440   regress0/sygus/inv-different-var-order.sy
1441   regress0/sygus/issue3356-syg-inf-usort.smt2
1442   regress0/sygus/issue3624.sy
1443   regress0/sygus/issue3645-grammar-sets.smt2
1444   regress0/sygus/issue4383-cache-fv-id.sy
1445   regress0/sygus/issue4790-dtd.sy
1446   regress0/sygus/issue5512-vvv.sy
1447   regress0/sygus/issue6298-par.sy
1448   regress0/sygus/let-ringer.sy
1449   regress0/sygus/let-simp.sy
1450   regress0/sygus/no-logic.sy
1451   regress0/sygus/no-syntax-test-bool.sy
1452   regress0/sygus/no-syntax-test.sy
1453   regress0/sygus/parse-bv-let.sy
1454   regress0/sygus/pbe-pred-contra.sy
1455   regress0/sygus/pLTL-sygus-syntax-err.sy
1456   regress0/sygus/print-debug.sy
1457   regress0/sygus/print-define-fun.sy
1458   regress0/sygus/print-grammar.sy
1459   regress0/sygus/proj-issue464-rr-option.smt2
1460   regress0/sygus/real-si-all.sy
1461   regress0/sygus/setFeature.sy
1462   regress0/sygus/strings-unconstrained.sy
1463   regress0/sygus/sygus-no-wf.sy
1464   regress0/sygus/sygus-uf.sy
1465   regress0/sygus/uminus_one.sy
1466   regress0/sygus/univ_3-long-repeat-conflict.sy
1467   regress0/symmetric.smtv1.smt2
1468   regress0/test11.cvc.smt2
1469   regress0/test9.cvc.smt2
1470   regress0/tptp/ARI086=1.p
1471   regress0/tptp/DAT001=1.p
1472   regress0/tptp/is_rat_simple.p
1473   regress0/tptp/KRS018+1.p
1474   regress0/tptp/KRS063+1.p
1475   regress0/tptp/MGT019+2.p
1476   regress0/tptp/MGT041-2.p
1477   regress0/tptp/PUZ131_1.p
1478   regress0/tptp/parse-neg-rational.p
1479   regress0/tptp/SYN000_1.p
1480   regress0/tptp/SYN000_2.p
1481   regress0/tptp/SYN000-1.p
1482   regress0/tptp/SYN000-2.p
1483   regress0/tptp/SYN000+1.p
1484   regress0/tptp/SYN000+2.p
1485   regress0/tptp/SYN000=2.p
1486   regress0/tptp/SYN075-1.p
1487   regress0/tptp/tff0-arith.p
1488   regress0/tptp/tff0.p
1489   regress0/tptp/tptp_parser.p
1490   regress0/tptp/tptp_parser10.p
1491   regress0/tptp/tptp_parser2.p
1492   regress0/tptp/tptp_parser3.p
1493   regress0/tptp/tptp_parser4.p
1494   regress0/tptp/tptp_parser5.p
1495   regress0/tptp/tptp_parser6.p
1496   regress0/tptp/tptp_parser7.p
1497   regress0/tptp/tptp_parser8.p
1498   regress0/tptp/tptp_parser9.p
1499   regress0/uf/bool-pred-nested.smt2
1500   regress0/uf/ccredesign-fuzz.smtv1.smt2
1501   regress0/uf/cnf_abc.smt2
1502   regress0/uf/cnf-and-neg.smt2
1503   regress0/uf/cnf-iff-base.smt2
1504   regress0/uf/cnf-iff.smt2
1505   regress0/uf/cnf-ite.smt2
1506   regress0/uf/dead_dnd002.smtv1.smt2
1507   regress0/uf/eq_diamond1.smtv1.smt2
1508   regress0/uf/eq_diamond14.reduced.smtv1.smt2
1509   regress0/uf/eq_diamond14.reduced2.smtv1.smt2
1510   regress0/uf/eq_diamond23.smtv1.smt2
1511   regress0/uf/euf_simp01.smtv1.smt2
1512   regress0/uf/euf_simp02.smtv1.smt2
1513   regress0/uf/euf_simp03.smtv1.smt2
1514   regress0/uf/euf_simp04.smtv1.smt2
1515   regress0/uf/euf_simp05.smtv1.smt2
1516   regress0/uf/euf_simp06.smtv1.smt2
1517   regress0/uf/euf_simp08.smtv1.smt2
1518   regress0/uf/euf_simp09.smtv1.smt2
1519   regress0/uf/euf_simp10.smtv1.smt2
1520   regress0/uf/euf_simp11.smtv1.smt2
1521   regress0/uf/euf_simp12.smtv1.smt2
1522   regress0/uf/euf_simp13.smtv1.smt2
1523   regress0/uf/iso_brn001.smtv1.smt2
1524   regress0/uf/issue2947.smt2
1525   regress0/uf/issue4446.smt2
1526   regress0/uf/NEQ016_size5_reduced2a.smtv1.smt2
1527   regress0/uf/NEQ016_size5_reduced2b.smtv1.smt2
1528   regress0/uf/pred.smtv1.smt2
1529   regress0/uf/SEQ032_size2.smtv1.smt2
1530   regress0/uf/simple.01.cvc.smt2
1531   regress0/uf/simple.02.cvc.smt2
1532   regress0/uf/simple.03.cvc.smt2
1533   regress0/uf/simple.04.cvc.smt2
1534   regress0/uf20-03.cvc.smt2
1535   regress0/uflia/check01.smt2
1536   regress0/uflia/check02.smt2
1537   regress0/uflia/check03.smt2
1538   regress0/uflia/check04.smt2
1539   regress0/uflia/diseqprop.01.smtv1.smt2
1540   regress0/uflia/diseqprop.02.smtv1.smt2
1541   regress0/uflia/diseqprop.03.smtv1.smt2
1542   regress0/uflia/diseqprop.04.smtv1.smt2
1543   regress0/uflia/diseqprop.05.smtv1.smt2
1544   regress0/uflia/diseqprop.06.smtv1.smt2
1545   regress0/uflia/error0.delta01.smtv1.smt2
1546   regress0/uflia/error30.smtv1.smt2
1547   regress0/uflia/stalmark_e7_27_e7_31.ec.minimized.smt2
1548   regress0/uflia/tiny.smt2
1549   regress0/uflia/xs-09-16-3-4-1-5.delta01.smtv1.smt2
1550   regress0/uflia/xs-09-16-3-4-1-5.delta02.smtv1.smt2
1551   regress0/uflia/xs-09-16-3-4-1-5.delta03.smtv1.smt2
1552   regress0/uflia/xs-09-16-3-4-1-5.delta04.smtv1.smt2
1553   regress0/uflia/xs-09-16-3-4-1-5.delta05.smtv1.smt2
1554   regress0/uflra/bug293.cvc.smt2
1555   regress0/uflra/bug449.smtv1.smt2
1556   regress0/uflra/constants0.smtv1.smt2
1557   regress0/uflra/fuzz01.smtv1.smt2
1558   regress0/uflra/incorrect1.delta01.smtv1.smt2
1559   regress0/uflra/incorrect1.delta02.smtv1.smt2
1560   regress0/uflra/neq-deltacomp.smtv1.smt2
1561   regress0/uflra/pb_real_10_0100_10_10.smtv1.smt2
1562   regress0/uflra/pb_real_10_0100_10_11.smtv1.smt2
1563   regress0/uflra/pb_real_10_0100_10_15.smtv1.smt2
1564   regress0/uflra/pb_real_10_0100_10_16.smtv1.smt2
1565   regress0/uflra/pb_real_10_0100_10_19.smtv1.smt2
1566   regress0/uflra/pb_real_10_0200_10_22.smtv1.smt2
1567   regress0/uflra/pb_real_10_0200_10_25.smtv1.smt2
1568   regress0/uflra/pb_real_10_0200_10_26.smtv1.smt2
1569   regress0/uflra/pb_real_10_0200_10_27.smtv1.smt2
1570   regress0/uflra/pb_real_10_0200_10_29.smtv1.smt2
1571   regress0/uflra/simple.01.cvc.smt2
1572   regress0/uflra/simple.02.cvc.smt2
1573   regress0/uflra/simple.03.cvc.smt2
1574   regress0/uflra/simple.04.cvc.smt2
1575   regress0/unconstrained/4481.smt2
1576   regress0/unconstrained/arith.smt2
1577   regress0/unconstrained/arith2.smt2
1578   regress0/unconstrained/arith3.smt2
1579   regress0/unconstrained/arith4.smt2
1580   regress0/unconstrained/arith5.smt2
1581   regress0/unconstrained/arith6.smt2
1582   regress0/unconstrained/arith7.smt2
1583   regress0/unconstrained/array1.smt2
1584   regress0/unconstrained/bvbool.smt2
1585   regress0/unconstrained/bvbool2.smt2
1586   regress0/unconstrained/bvbool3.smt2
1587   regress0/unconstrained/bvcmp.smt2
1588   regress0/unconstrained/bvconcat.smt2
1589   regress0/unconstrained/bvconcat2.smt2
1590   regress0/unconstrained/bvext.smt2
1591   regress0/unconstrained/bvite.smt2
1592   regress0/unconstrained/bvmul.smt2
1593   regress0/unconstrained/bvmul2.smt2
1594   regress0/unconstrained/bvmul3.smt2
1595   regress0/unconstrained/bvnot.smt2
1596   regress0/unconstrained/bvsle.smt2
1597   regress0/unconstrained/bvsle2.smt2
1598   regress0/unconstrained/bvsle3.smt2
1599   regress0/unconstrained/bvsle4.smt2
1600   regress0/unconstrained/bvsle5.smt2
1601   regress0/unconstrained/bvslt.smt2
1602   regress0/unconstrained/bvslt2.smt2
1603   regress0/unconstrained/bvslt3.smt2
1604   regress0/unconstrained/bvslt4.smt2
1605   regress0/unconstrained/bvslt5.smt2
1606   regress0/unconstrained/bvdiv.smt2
1607   regress0/unconstrained/bvule.smt2
1608   regress0/unconstrained/bvule2.smt2
1609   regress0/unconstrained/bvule3.smt2
1610   regress0/unconstrained/bvule4.smt2
1611   regress0/unconstrained/bvule5.smt2
1612   regress0/unconstrained/bvult.smt2
1613   regress0/unconstrained/bvult2.smt2
1614   regress0/unconstrained/bvult3.smt2
1615   regress0/unconstrained/bvult4.smt2
1616   regress0/unconstrained/bvult5.smt2
1617   regress0/unconstrained/geq.smt2
1618   regress0/unconstrained/gt.smt2
1619   regress0/unconstrained/issue4644.smt2
1620   regress0/unconstrained/issue4656-bool-term-vars.smt2
1621   regress0/unconstrained/ite.smt2
1622   regress0/unconstrained/leq.smt2
1623   regress0/unconstrained/lt.smt2
1624   regress0/unconstrained/mult1.smt2
1625   regress0/unconstrained/uf1.smt2
1626   regress0/unconstrained/xor.smt2
1627   regress0/use_approx/bug812_approx.smt2
1628   regress0/use_approx/error0_approx.smt2
1629   regress0/use_approx/issue2429_approx.smt2
1630   regress0/use_approx/issue4714_approx.smt2
1631   regress0/use_approx/siegel-nl-bases_approx.smt2
1632   regress0/use_approx/specsharp-WindowsCard.15.RTE.Terminate_System.Int32_approx.smt2
1633   regress0/wiki.01.cvc.smt2
1634   regress0/wiki.02.cvc.smt2
1635   regress0/wiki.03.cvc.smt2
1636   regress0/wiki.04.cvc.smt2
1637   regress0/wiki.05.cvc.smt2
1638   regress0/wiki.06.cvc.smt2
1639   regress0/wiki.07.cvc.smt2
1640   regress0/wiki.08.cvc.smt2
1641   regress0/wiki.09.cvc.smt2
1642   regress0/wiki.10.cvc.smt2
1643   regress0/wiki.11.cvc.smt2
1644   regress0/wiki.12.cvc.smt2
1645   regress0/wiki.13.cvc.smt2
1646   regress0/wiki.14.cvc.smt2
1647   regress0/wiki.15.cvc.smt2
1648   regress0/wiki.16.cvc.smt2
1649   regress0/wiki.17.cvc.smt2
1650   regress0/wiki.18.cvc.smt2
1651   regress0/wiki.19.cvc.smt2
1652   regress0/wiki.20.cvc.smt2
1653   regress0/wiki.21.cvc.smt2
1654 )
1655
1656 #-----------------------------------------------------------------------------#
1657 # Regression level 1 tests
1658
1659 set(regress_1_tests
1660   regress1/abduction/abduction_1255.corecstrs.readable.smt2
1661   regress1/abduction/abduction_streq.readable.smt2
1662   regress1/abduction/abduction-no-pbe-sym-break.smt2
1663   regress1/abduction/abduct-dt.smt2
1664   regress1/abduction/abd-real-const.smt2
1665   regress1/abduction/abd-simple-conj-4.smt2
1666   regress1/abduction/issue5848-2.smt2
1667   regress1/abduction/issue5848-3-trivial-no-abduct.smt2
1668   regress1/abduction/issue5848-4.smt2
1669   regress1/abduction/issue5848.smt2
1670   regress1/abduction/issue6605-1.smt2
1671   regress1/abduction/simple-incremental.smt2
1672   regress1/abduction/simple-incremental-push-pop.smt2
1673   regress1/abduction/sygus-abduct-ex1-grammar.smt2
1674   regress1/abduction/sygus-abduct-test.smt2
1675   regress1/abduction/sygus-abduct-test-ccore.smt2
1676   regress1/abduction/sygus-abduct-test-user.smt2
1677   regress1/abduction/uf-abduct.smt2
1678   regress1/abduction/yoni-true-sol.smt2
1679   regress1/arith/arith-brab-test.smt2
1680   regress1/arith/arith-int-004.cvc.smt2
1681   regress1/arith/arith-int-011.cvc.smt2
1682   regress1/arith/arith-int-012.cvc.smt2
1683   regress1/arith/arith-int-013.cvc.smt2
1684   regress1/arith/arith-int-022.cvc.smt2
1685   regress1/arith/arith-int-024.cvc.smt2
1686   regress1/arith/arith-int-047.cvc.smt2
1687   regress1/arith/arith-int-048.cvc.smt2
1688   regress1/arith/arith-int-050.cvc.smt2
1689   regress1/arith/arith-int-084.cvc.smt2
1690   regress1/arith/arith-int-085.cvc.smt2
1691   regress1/arith/arith-int-097.cvc.smt2
1692   regress1/arith/bug547.1.smt2
1693   regress1/arith/bug716.0.smt2
1694   regress1/arith/bug716.1.cvc.smt2
1695   regress1/arith/bug716.2.cvc.smt2
1696   regress1/arith/div.03.smt2
1697   regress1/arith/div.06.smt2
1698   regress1/arith/div.08.smt2
1699   regress1/arith/div.09.smt2
1700   regress1/arith/issue3480.smt2
1701   regress1/arith/issue3952-rew-eq.smt2
1702   regress1/arith/issue4985-model-success.smt2
1703   regress1/arith/issue4985b-model-success.smt2
1704   regress1/arith/issue6774-sanity-int-model.smt2
1705   regress1/arith/issue7252-arith-sanity.smt2
1706   regress1/arith/issue789.smt2
1707   regress1/arith/miplib3.cvc.smt2
1708   regress1/arith/mod.02.smt2
1709   regress1/arith/mod.03.smt2
1710   regress1/arith/mult.02.smt2
1711   regress1/arith/pbrewrites-test.smt2
1712   regress1/arith/problem__003.smt2
1713   regress1/arith/proj-issue158.smt2
1714   regress1/arrayinuf_error.smt2
1715   regress1/aufbv/bug348.smtv1.smt2
1716   regress1/aufbv/bug580.smt2
1717   regress1/aufbv/fuzz03.smtv1.smt2
1718   regress1/aufbv/fuzz10.smtv1.smt2
1719   regress1/auflia/bug330.smt2
1720   regress1/boolean-terms-kernel2.smt2
1721   regress1/boolean.cvc.smt2
1722   regress1/bug296.smt2
1723   regress1/bug425.cvc.smt2
1724   regress1/bug507.smt2
1725   regress1/bug512.smt2
1726   regress1/bug516.smt2
1727   regress1/bug519.smt2
1728   regress1/bug520.smt2
1729   regress1/bug521.smt2
1730   regress1/bug543.smt2
1731   regress1/bug567.smt2
1732   regress1/bug590.smt2
1733   regress1/bug593.smt2
1734   regress1/bug681.smt2
1735   regress1/bug694-Unapply1.scala-0.smt2
1736   regress1/bug800.smt2
1737   regress1/bags/bag_member.smt2
1738   regress1/bags/bags-of-bags-subtypes.smt2
1739   regress1/bags/card1.smt2
1740   regress1/bags/card2.smt2
1741   regress1/bags/card3.smt2
1742   regress1/bags/choose1.smt2
1743   regress1/bags/choose2.smt2
1744   regress1/bags/choose3.smt2
1745   regress1/bags/choose4.smt2
1746   regress1/bags/difference_remove1.smt2
1747   regress1/bags/disequality.smt2
1748   regress1/bags/duplicate_removal1.smt2
1749   regress1/bags/duplicate_removal2.smt2
1750   regress1/bags/emptybag1.smt2
1751   regress1/bags/filter1.smt2
1752   regress1/bags/filter2.smt2
1753   regress1/bags/filter3.smt2
1754   regress1/bags/filter4.smt2
1755   regress1/bags/filter5.smt2
1756   regress1/bags/fol_0000119.smt2
1757   regress1/bags/fold1.smt2
1758   regress1/bags/fuzzy1.smt2
1759   regress1/bags/fuzzy2.smt2
1760   regress1/bags/fuzzy3.smt2
1761   regress1/bags/fuzzy3b.smt2
1762   regress1/bags/fuzzy4.smt2
1763   regress1/bags/fuzzy5.smt2
1764   regress1/bags/fuzzy6.smt2
1765   regress1/bags/intersection_min1.smt2
1766   regress1/bags/intersection_min2.smt2
1767   regress1/bags/issue5759.smt2
1768   regress1/bags/map1.smt2
1769   regress1/bags/map2.smt2
1770   regress1/bags/map3.smt2
1771   regress1/bags/map-lazy-lam.smt2
1772   regress1/bags/murxla1.smt2
1773   regress1/bags/murxla2.smt2
1774   regress1/bags/murxla3.smt2
1775   regress1/bags/murxla4.smt2
1776   regress1/bags/murxla5.smt2
1777   regress1/bags/murxla6.smt2
1778   regress1/bags/product1.smt2
1779   regress1/bags/product2.smt2
1780   regress1/bags/product3.smt2
1781   regress1/bags/proj-issue497.smt2
1782   regress1/bags/subbag1.smt2
1783   regress1/bags/subbag2.smt2
1784   regress1/bags/union_disjoint.smt2
1785   regress1/bags/union_max1.smt2
1786   regress1/bags/union_max2.smt2
1787   regress1/bv2int-isabelle.smt2
1788   regress1/bv2int-make-binary.smt2
1789   regress1/bv/bench_38.delta.smt2
1790   regress1/bv/bug787.smt2
1791   regress1/bv/bug_extract_mult_leading_bit.smt2
1792   regress1/bv/bv-int-collapse2-sat.smt2
1793   regress1/bv/bv-proof00.smtv1.smt2
1794   regress1/bv/bv2nat-ground.smt2
1795   regress1/bv/bv2nat-simp-range-sat.smt2
1796   regress1/bv/bv2nat-types.smt2
1797   regress1/bv/cmu-rdk-3.smt2
1798   regress1/bv/decision-weight00.smt2
1799   regress1/bv/divtest.smt2
1800   regress1/bv/fuzz18.smtv1.smt2
1801   regress1/bv/fuzz19.smtv1.smt2
1802   regress1/bv/fuzz34.smtv1.smt2
1803   regress1/bv/fuzz38.smtv1.smt2
1804   regress1/bv/incorrect1.smtv1.smt2
1805   regress1/bv/issue3654.smt2
1806   regress1/bv/issue3776.smt2
1807   regress1/bv/issue3958.smt2
1808   regress1/bv/min-pp-rewrite-error.smt2
1809   regress1/bv/proj-issue438-prerewrite-fixed-point-original.smt2
1810   regress1/bv/unsound1.smt2
1811   regress1/bvdiv2.smt2
1812   regress1/cee-bug0909-dd-scope.smt2
1813   regress1/constarr3.cvc.smt2
1814   regress1/constarr3.smt2
1815   regress1/cores/issue5604.smt2
1816   regress1/cores/issue6988-arith-sanity.smt2
1817   regress1/datatypes/acyclicity-sr-ground096.smt2
1818   regress1/datatypes/cee-prs-small-dd2.smt2
1819   regress1/datatypes/dt-color-2.6.smt2
1820   regress1/datatypes/dt-param-card4-unsat.smt2
1821   regress1/datatypes/issue3266-small.smt2
1822   regress1/datatypes/issue4851-cdt-model.smt2
1823   regress1/datatypes/issue8124-real-int-cg.smt2
1824   regress1/datatypes/issue-variant-dt-zero.smt2
1825   regress1/datatypes/manos-model.smt2
1826   regress1/datatypes/non-simple-rec.smt2
1827   regress1/datatypes/non-simple-rec-mut-unsat.smt2
1828   regress1/datatypes/non-simple-rec-param.smt2
1829   regress1/datatypes/proj-issue433-tester-merge-pf.smt2
1830   regress1/datatypes/tuple_projection.smt2
1831   regress1/decision/bug374a.smtv1.smt2
1832   regress1/decision/error3.smtv1.smt2
1833   regress1/decision/issue5454-2.smt2
1834   regress1/decision/issue5454-3.smt2
1835   regress1/decision/issue5454.smt2
1836   regress1/decision/issue5785.smt2
1837   regress1/decision/jh-test1.smt2
1838   regress1/decision/quant-Arrays_Q1-noinfer.smt2
1839   regress1/decision/wishue114.smt2
1840   regress1/decision/wishue115.smt2
1841   regress1/decision/wishue116.smt2
1842   regress1/decision/wishue149-2.smt2
1843   regress1/decision/wishue149-3.smt2
1844   regress1/decision/wishue160.smt2
1845   regress1/difficulty-polarity.smt2
1846   regress1/errorcrash.smt2
1847   regress1/fp/fp_to_real.smt2
1848   regress1/fp/rti_3_5_bug_report.smt2
1849   regress1/fmf-fun-dbu.smt2
1850   regress1/fmf/ALG008-1.smt2
1851   regress1/fmf/Hoare-z3.931718.smtv1.smt2
1852   regress1/fmf/LeftistHeap.scala-8-ncm.smt2
1853   regress1/fmf/PUZ001+1.smt2
1854   regress1/fmf/agree466.smt2
1855   regress1/fmf/agree467.smt2
1856   regress1/fmf/alg202+1.smt2
1857   regress1/fmf/am-bad-model.cvc.smt2
1858   regress1/fmf/bound-int-alt.smt2
1859   regress1/fmf/bug0909.smt2
1860   regress1/fmf/bug651.smt2
1861   regress1/fmf/bug723-irrelevant-funs.smt2
1862   regress1/fmf/bug764.smt2
1863   regress1/fmf/cons-sets-bounds.smt2
1864   regress1/fmf/constr-ground-to.smt2
1865   regress1/fmf/datatypes-ufinite-nested.smt2
1866   regress1/fmf/datatypes-ufinite.smt2
1867   regress1/fmf/dt-proper-model.smt2
1868   regress1/fmf/fc-pigeonhole19.smt2
1869   regress1/fmf/fib-core.smt2
1870   regress1/fmf/fmf-bound-2dim.smt2
1871   regress1/fmf/fmf-bound-int.smt2
1872   regress1/fmf/fmf-fun-divisor-pp.smt2
1873   regress1/fmf/fmf-fun-no-elim-ext-arith.smt2
1874   regress1/fmf/fmf-fun-no-elim-ext-arith2.smt2
1875   regress1/fmf/fmf-strange-bounds.smt2
1876   regress1/fmf/forall_unit_data.smt2
1877   regress1/fmf/fore19-exp2-core.smt2
1878   regress1/fmf/german169.smt2
1879   regress1/fmf/german73.smt2
1880   regress1/fmf/issue2034-preinit.smt2
1881   regress1/fmf/issue3587.smt2
1882   regress1/fmf/issue3615.smt2
1883   regress1/fmf/issue3626.smt2
1884   regress1/fmf/issue3689.smt2
1885   regress1/fmf/issue4068-si-qf.smt2
1886   regress1/fmf/issue4225-univ-fun.smt2
1887   regress1/fmf/issue5738-dt-interp-finite.smt2
1888   regress1/fmf/issue6690-re-enum.smt2
1889   regress1/fmf/issue6744-2-unc-bool-var.smt2
1890   regress1/fmf/issue6744-3-unc-bool-var.smt2
1891   regress1/fmf/issue8096-non-const-rep.smt2
1892   regress1/fmf/issue8163-nconst-arg.smt2
1893   regress1/fmf/issue916-fmf-or.smt2
1894   regress1/fmf/jasmin-cdt-crash.smt2
1895   regress1/fmf/ko-bound-set.cvc.smt2
1896   regress1/fmf/loopy_coda.smt2
1897   regress1/fmf/lst-no-self-rev-exp.smt2
1898   regress1/fmf/memory_model-R_cpp-dd.cvc.smt2
1899   regress1/fmf/nlp042+1.smt2
1900   regress1/fmf/nun-0208-to.smt2
1901   regress1/fmf/pow2-bool.smt2
1902   regress1/fmf/radu-quant-set.smt2
1903   regress1/fmf/refcount24.cvc.smt2
1904   regress1/fmf/sc-crash-052316.smt2
1905   regress1/fmf/sort-inf-int-real.smt2
1906   regress1/fmf/sort-inf-int.smt2
1907   regress1/fmf/with-ind-104-core.smt2
1908   regress1/gensys_brn001.smt2
1909   regress1/get-learned-literals.smt2
1910   regress1/ho/bug_freeVar_BDD_General_data_270.p
1911   regress1/ho/bug_freevar_PHI004^4-delta.smt2
1912   regress1/ho/bound_var_bug.p
1913   regress1/ho/fta0328.lfho.p
1914   regress1/ho/ho-fun-sharing-dd.smt2
1915   regress1/ho/issue3136-fconst-bool-bool.smt2
1916   regress1/ho/issue4065-no-rep.smt2
1917   regress1/ho/issue4092-sinf.smt2
1918   regress1/ho/issue4134-sinf.smt2
1919   regress1/ho/issue4758.smt2
1920   regress1/ho/issue5078-small.smt2
1921   regress1/ho/issue5201-1.smt2
1922   regress1/ho/issue5741-3.smt2
1923   regress1/ho/NUM638^1.smt2
1924   regress1/ho/NUM925^1.p
1925   regress1/ho/proj-issue139-2.smt2
1926   regress1/ho/soundness_fmf_SYO362^5-delta.p
1927   regress1/ho/store-ax-min.p
1928   regress1/hole6.cvc.smt2
1929   regress1/ite5.smt2
1930   regress1/issue3970-nl-ext-purify.smt2
1931   regress1/issue3990-sort-inference.smt2
1932   regress1/issue4273-ext-rew-cache.smt2
1933   regress1/issue4335-unsat-core.smt2
1934   regress1/issue5101-alira-subtypes.smt2
1935   regress1/issue5739-rtf-processed.smt2
1936   regress1/issue7902-abd-subsolver-uc.smt2
1937   regress1/issue7937-difficulty-irr.smt2
1938   regress1/lemmas/clocksynchro_5clocks.main_invar.base.smtv1.smt2
1939   regress1/lemmas/pursuit-safety-8.smtv1.smt2
1940   regress1/minimal_unsat_core.smt2
1941   regress1/model-blocker-simple.smt2
1942   regress1/model-blocker-values.smt2
1943   regress1/nl/approx-sqrt.smt2
1944   regress1/nl/approx-sqrt-unsat.smt2
1945   regress1/nl/arctan2-expdef.smt2
1946   regress1/nl/arrowsmith-050317.smt2
1947   regress1/nl/bad-050217.smt2
1948   regress1/nl/bug698.smt2
1949   regress1/nl/coeff-unsat-base.smt2
1950   regress1/nl/coeff-unsat.smt2
1951   regress1/nl/combine.smt2
1952   regress1/nl/cos-bound.smt2
1953   regress1/nl/cos1-tc.smt2
1954   regress1/nl/disj-eval.smt2
1955   regress1/nl/dist-big.smt2
1956   regress1/nl/div-mod-partial.smt2
1957   regress1/nl/exp-4.5-lt.smt2
1958   regress1/nl/exp-approx.smt2
1959   regress1/nl/exp-soundness-bound.smt2
1960   regress1/nl/exp1-lb.smt2
1961   regress1/nl/exp_monotone.smt2
1962   regress1/nl/ext-rew-aggr-test.smt2
1963   regress1/nl/factor_agg_s.smt2
1964   regress1/nl/iand-native-2.smt2
1965   regress1/nl/iand-native-granularities.smt2
1966   regress1/nl/issue3300-approx-sqrt-witness.smt2
1967   regress1/nl/issue3441.smt2
1968   regress1/nl/issue3617.smt2
1969   regress1/nl/issue3647.smt2
1970   regress1/nl/issue3656.smt2
1971   regress1/nl/issue3803-nl-check-model.smt2
1972   regress1/nl/issue3955-ee-double-notify.smt2
1973   regress1/nl/issue3966-conf-coeff.smt2
1974   regress1/nl/issue4334-sat-proof.smt2
1975   regress1/nl/issue4791-llr.smt2
1976   regress1/nl/issue5372-2-no-m-presolve.smt2
1977   regress1/nl/issue5461-iand-init-refine.smt2
1978   regress1/nl/issue5660-mb-success.smt2
1979   regress1/nl/issue5662-nl-tc.smt2
1980   regress1/nl/issue5662-nl-tc-min.smt2
1981   regress1/nl/issue7924-sqrt-partial.smt2
1982   regress1/nl/issue7948-3-unsound-sin-region.smt2
1983   regress1/nl/issue8016-iand-rewrite.smt2
1984   regress1/nl/issue8052-iand-rewrite.smt2
1985   regress1/nl/issue8118-elim-sin.smt2
1986   regress1/nl/issue8162-drop-pi-bound.smt2
1987   regress1/nl/metitarski-1025.smt2
1988   regress1/nl/metitarski-3-4.smt2
1989   regress1/nl/metitarski_3_4_2e.smt2
1990   regress1/nl/mirko-050417.smt2
1991   regress1/nl/nl-eq-infer.smt2
1992   regress1/nl/nl-help-unsat-quant.smt2
1993   regress1/nl/nl-unk-quant.smt2
1994   regress1/nl/nl_uf_lalt.smt2
1995   regress1/nl/nra-cad-performance.smt2
1996   regress1/nl/ones.smt2
1997   regress1/nl/pinto-model-core-ni.smt2
1998   regress1/nl/poly-1025.smt2
1999   regress1/nl/proj-365-is-int-pi.smt2
2000   regress1/nl/proj-issue215.smt2
2001   regress1/nl/proj-issue232.smt2
2002   regress1/nl/proj-issue253.smt2
2003   regress1/nl/proj-issue279.smt2
2004   regress1/nl/proj-issue280.smt2
2005   regress1/nl/proj-issue282.smt2
2006   regress1/nl/proj-issue286.smt2
2007   regress1/nl/proj-issue290.smt2
2008   regress1/nl/proj-issue291.smt2
2009   regress1/nl/proj-issue292.smt2
2010   regress1/nl/proj-issue294.smt2
2011   regress1/nl/proj-issue297.smt2
2012   regress1/nl/proj-issue302.smt2
2013   regress1/nl/quant-nl.smt2
2014   regress1/nl/red-exp.smt2
2015   regress1/nl/rewriting-sums.smt2
2016   regress1/nl/shifting.smt2
2017   regress1/nl/shifting2.smt2
2018   regress1/nl/simple-mono-unsat.smt2
2019   regress1/nl/simple-mono.smt2
2020   regress1/nl/sin-compare-across-phase.smt2
2021   regress1/nl/sin-compare.smt2
2022   regress1/nl/sin-init-tangents.smt2
2023   regress1/nl/sin-sign.smt2
2024   regress1/nl/sin-sym2.smt2
2025   regress1/nl/sin1-deq-sat.smt2
2026   regress1/nl/sin1-lb.smt2
2027   regress1/nl/sin1-sat.smt2
2028   regress1/nl/sin1-ub.smt2
2029   regress1/nl/sin2-lb.smt2
2030   regress1/nl/sin2-ub.smt2
2031   regress1/nl/solve-eq-small-qf-nra.smt2
2032   regress1/nl/sqrt-problem-1.smt2
2033   regress1/nl/sugar-ident-2.smt2
2034   regress1/nl/sugar-ident-3.smt2
2035   regress1/nl/sugar-ident.smt2
2036   regress1/nl/tan-rewrite2.smt2
2037   regress1/nl/transcedental_model_simple.smt2
2038   regress1/nl/zero-subset.smt2
2039   regress1/non-fatal-errors.smt2
2040   regress1/proj-issue175.smt2
2041   regress1/proj-issue406-diff-unsat-core.smt2
2042   regress1/proj-issue476-theoryOf-no-uf.smt2
2043   regress1/proof00.smt2
2044   regress1/proofs/issue6625-unsat-core-proofs.smt2
2045   regress1/proofs/macro-res-exp-crowding-lit-inside-unit.smt2
2046   regress1/proofs/macro-res-exp-singleton-after-elimCrowd.smt2
2047   regress1/proofs/qgu-fuzz-1-strings-pp.smt2
2048   regress1/proofs/qgu-fuzz-arrays-1-dd-te-auto.smt2
2049   regress1/proofs/quant-alpha-eq.smt2
2050   regress1/proofs/sat-trivial-cycle.smt2
2051   regress1/proofs/str-ovf-dd.smt2
2052   regress1/proofs/unsat-cores-proofs.smt2
2053   regress1/push-pop/arith_lra_01.smt2
2054   regress1/push-pop/arith_lra_02.smt2
2055   regress1/push-pop/bug-fmf-fun-skolem.smt2
2056   regress1/push-pop/bug216.smt2
2057   regress1/push-pop/cee-prs-small.smt2
2058   regress1/push-pop/fuzz_1.smt2
2059   regress1/push-pop/fuzz_10.smt2
2060   regress1/push-pop/fuzz_11.smt2
2061   regress1/push-pop/fuzz_15.smt2
2062   regress1/push-pop/fuzz_16.smt2
2063   regress1/push-pop/fuzz_19.smt2
2064   regress1/push-pop/fuzz_1_to_52_merged.smt2
2065   regress1/push-pop/fuzz_20.smt2
2066   regress1/push-pop/fuzz_23.smt2
2067   regress1/push-pop/fuzz_24.smt2
2068   regress1/push-pop/fuzz_25.smt2
2069   regress1/push-pop/fuzz_26.smt2
2070   regress1/push-pop/fuzz_28.smt2
2071   regress1/push-pop/fuzz_29.smt2
2072   regress1/push-pop/fuzz_30.smt2
2073   regress1/push-pop/fuzz_32.smt2
2074   regress1/push-pop/fuzz_34.smt2
2075   regress1/push-pop/fuzz_35.smt2
2076   regress1/push-pop/fuzz_37.smt2
2077   regress1/push-pop/fuzz_39.smt2
2078   regress1/push-pop/fuzz_3_1.smt2
2079   regress1/push-pop/fuzz_3_10.smt2
2080   regress1/push-pop/fuzz_3_11.smt2
2081   regress1/push-pop/fuzz_3_12.smt2
2082   regress1/push-pop/fuzz_3_13.smt2
2083   regress1/push-pop/fuzz_3_14.smt2
2084   regress1/push-pop/fuzz_3_15.smt2
2085   regress1/push-pop/fuzz_3_2.smt2
2086   regress1/push-pop/fuzz_3_3.smt2
2087   regress1/push-pop/fuzz_3_4.smt2
2088   regress1/push-pop/fuzz_3_5.smt2
2089   regress1/push-pop/fuzz_3_6.smt2
2090   regress1/push-pop/fuzz_3_7.smt2
2091   regress1/push-pop/fuzz_3_8.smt2
2092   regress1/push-pop/fuzz_3_9.smt2
2093   regress1/push-pop/fuzz_4.smt2
2094   regress1/push-pop/fuzz_40.smt2
2095   regress1/push-pop/fuzz_41.smt2
2096   regress1/push-pop/fuzz_42.smt2
2097   regress1/push-pop/fuzz_43.smt2
2098   regress1/push-pop/fuzz_44.smt2
2099   regress1/push-pop/fuzz_45.smt2
2100   regress1/push-pop/fuzz_5.smt2
2101   regress1/push-pop/fuzz_51.smt2
2102   regress1/push-pop/fuzz_52.smt2
2103   regress1/push-pop/fuzz_5_1.smt2
2104   regress1/push-pop/fuzz_5_2.smt2
2105   regress1/push-pop/fuzz_5_3.smt2
2106   regress1/push-pop/fuzz_5_4.smt2
2107   regress1/push-pop/fuzz_5_5.smt2
2108   regress1/push-pop/fuzz_5_6.smt2
2109   regress1/push-pop/fuzz_6.smt2
2110   regress1/push-pop/fuzz_7.smt2
2111   regress1/push-pop/fuzz_8.smt2
2112   regress1/push-pop/fuzz_9.smt2
2113   regress1/push-pop/issue6773-arith-no-check.smt2
2114   regress1/push-pop/model-unsound-ania.smt2
2115   regress1/push-pop/proj-issue161.smt2
2116   regress1/push-pop/quant-fun-proc-unmacro.smt2
2117   regress1/push-pop/quant-fun-proc.smt2
2118   regress1/quantifiers/006-cbqi-ite.smt2
2119   regress1/quantifiers/015-psyco-pp.smt2
2120   regress1/quantifiers/AdditiveMethods_OwnedResults.Mz.smt2
2121   regress1/quantifiers/Arrays_Q1-noinfer.smt2
2122   regress1/quantifiers/NUM878.smt2
2123   regress1/quantifiers/RND-small.smt2
2124   regress1/quantifiers/RNDPRE_4_1-dd-nqe.smt2
2125   regress1/quantifiers/RND_4_1-existing-inst.smt2
2126   regress1/quantifiers/RND_4_16.smt2
2127   regress1/quantifiers/ari118-bv-2occ-x.smt2
2128   regress1/quantifiers/arith-rec-fun.smt2
2129   regress1/quantifiers/array-unsat-simp3.smt2
2130   regress1/quantifiers/bi-artm-s.smt2
2131   regress1/quantifiers/bignum_quant.smt2
2132   regress1/quantifiers/bug802.smt2
2133   regress1/quantifiers/bug822.smt2
2134   regress1/quantifiers/bug_743.smt2
2135   regress1/quantifiers/burns13.smt2
2136   regress1/quantifiers/burns4.smt2
2137   regress1/quantifiers/cbqi-sdlx-fixpoint-3-dd.smt2
2138   regress1/quantifiers/cee-npnt-dd.smt2
2139   regress1/quantifiers/cee-os-delta.smt2
2140   regress1/quantifiers/cdt-0208-to.smt2
2141   regress1/quantifiers/choice-move-delta-relt.smt2
2142   regress1/quantifiers/const.cvc.smt2
2143   regress1/quantifiers/constfunc.cvc.smt2
2144   regress1/quantifiers/ddatv-delta2.smt2
2145   regress1/quantifiers/dt-tc-opt-small.smt2
2146   regress1/quantifiers/dump-inst-i.smt2
2147   regress1/quantifiers/dump-inst-proof.smt2
2148   regress1/quantifiers/dump-inst.smt2
2149   regress1/quantifiers/eqrange_ex_1.smt2
2150   regress1/quantifiers/ext-ex-deq-trigger.smt2
2151   regress1/quantifiers/extract-nproc.smt2
2152   regress1/quantifiers/f993-loss-easy.smt2
2153   regress1/quantifiers/florian-case-ax.smt2
2154   regress1/quantifiers/fp-cegqi-unsat.smt2
2155   regress1/quantifiers/gauss_init_0030.fof.smt2
2156   regress1/quantifiers/horn-simple.smt2
2157   regress1/quantifiers/inst-max-level-segf.smt2
2158   regress1/quantifiers/inst-prop-simp.smt2
2159   regress1/quantifiers/intersection-example-onelane.proof-node22337.smt2
2160   regress1/quantifiers/is-even.smt2
2161   regress1/quantifiers/isaplanner-goal20.smt2
2162   regress1/quantifiers/issue2970-string-var-elim.smt2
2163   regress1/quantifiers/issue3250-syg-inf-q.smt2
2164   regress1/quantifiers/issue3316.smt2
2165   regress1/quantifiers/issue3317.smt2
2166   regress1/quantifiers/issue3481.smt2
2167   regress1/quantifiers/issue3537.smt2
2168   regress1/quantifiers/issue3628.smt2
2169   regress1/quantifiers/issue3664.smt2
2170   regress1/quantifiers/issue3724-quant.smt2
2171   regress1/quantifiers/issue3765.smt2
2172   regress1/quantifiers/issue3765-quant-dd.smt2
2173   regress1/quantifiers/issue4021-ind-opts.smt2
2174   regress1/quantifiers/issue4243-prereg-inc.smt2
2175   regress1/quantifiers/issue4290-cegqi-r.smt2
2176   regress1/quantifiers/issue4328-nqe.smt2
2177   regress1/quantifiers/issue4400-2-already-conf.smt2
2178   regress1/quantifiers/issue4412-cegqi-type.smt2
2179   regress1/quantifiers/issue4420-order-sensitive.smt2
2180   regress1/quantifiers/issue4433-nqe.smt2
2181   regress1/quantifiers/issue4620-erq-witness-unsound.smt2
2182   regress1/quantifiers/issue4685-wrewrite.smt2
2183   regress1/quantifiers/issue4813-qe-quant.smt2
2184   regress1/quantifiers/issue4849-nqe.smt2
2185   regress1/quantifiers/issue5019-cegqi-i.smt2
2186   regress1/quantifiers/issue5278-ext-rewrite-rec.smt2
2187   regress1/quantifiers/issue5279-nqe.smt2
2188   regress1/quantifiers/issue5288-vts-real-int.smt2
2189   regress1/quantifiers/issue5365-nqe.smt2
2190   regress1/quantifiers/issue5373-1-qe-inc.smt2
2191   regress1/quantifiers/issue5373-2.smt2
2192   regress1/quantifiers/issue5378-witness.smt2
2193   regress1/quantifiers/issue5469-aext.smt2
2194   regress1/quantifiers/issue5470-aext.smt2
2195   regress1/quantifiers/issue5471-aext.smt2
2196   regress1/quantifiers/issue5482-rtf-no-fv.smt2
2197   regress1/quantifiers/issue5484-qe.smt2
2198   regress1/quantifiers/issue5484b-qe.smt2
2199   regress1/quantifiers/issue5506-qe.smt2
2200   regress1/quantifiers/issue5507-qe.smt2
2201   regress1/quantifiers/issue5658-qe.smt2
2202   regress1/quantifiers/issue5735-subtypes.smt2
2203   regress1/quantifiers/issue5735-2-subtypes.smt2
2204   regress1/quantifiers/issue5766-wrong-sel-trigger.smt2
2205   regress1/quantifiers/issue5899-qe.smt2
2206   regress1/quantifiers/issue6607-witness-te.smt2
2207   regress1/quantifiers/issue6638-sygus-inst.smt2
2208   regress1/quantifiers/issue6642-em-types.smt2
2209   regress1/quantifiers/issue6699-nc-shadow.smt2
2210   regress1/quantifiers/issue6775-vts-int.smt2
2211   regress1/quantifiers/issue6845-nl-lemma-tc.smt2
2212   regress1/quantifiers/issue7385-sygus-inst-i.smt2
2213   regress1/quantifiers/issue7537-cegqi-comp-types.smt2
2214   regress1/quantifiers/issue8157-duplicate-conflicts.smt2
2215   regress1/quantifiers/issue8344-cegqi-string-witness.smt2
2216   regress1/quantifiers/issue8410-vts-subtypes.smt2
2217   regress1/quantifiers/issue8456-2-syqi-ic.smt2
2218   regress1/quantifiers/issue8456-syqi-ic.smt2
2219   regress1/quantifiers/issue993.smt2
2220   regress1/quantifiers/javafe.ast.StmtVec.009.smt2
2221   regress1/quantifiers/lia-witness-div-pp.smt2
2222   regress1/quantifiers/lra-vts-inf.smt2
2223   regress1/quantifiers/macro-geo-small-3.smt2
2224   regress1/quantifiers/min-ppgt-em-incomplete.smt2
2225   regress1/quantifiers/min-ppgt-em-incomplete2.smt2
2226   regress1/quantifiers/mix-coeff.smt2
2227   regress1/quantifiers/mutualrec2.cvc.smt2
2228   regress1/quantifiers/nested9_true-unreach-call.i_575.smt2
2229   regress1/quantifiers/nl-pow-trick.smt2
2230   regress1/quantifiers/nra-interleave-inst.smt2
2231   regress1/quantifiers/opisavailable-12.smt2
2232   regress1/quantifiers/parametric-lists.smt2
2233   regress1/quantifiers/pool-example.smt2
2234   regress1/quantifiers/prenex-scholl-smt08_RNDPRE_RNDPRE_4_6.smt2
2235   regress1/quantifiers/proj-issue151-2.smt2
2236   regress1/quantifiers/proj-issue155.smt2
2237   regress1/quantifiers/proj-issue295.smt2
2238   regress1/quantifiers/psyco-001-bv.smt2
2239   regress1/quantifiers/psyco-107-bv.smt2
2240   regress1/quantifiers/psyco-196.smt2
2241   regress1/quantifiers/qbv-disequality3.smt2
2242   regress1/quantifiers/qbv-simple-2vars-vo.smt2
2243   regress1/quantifiers/qbv-subcall.smt2
2244   regress1/quantifiers/qbv-test-invert-bvashr-0.smt2
2245   regress1/quantifiers/qbv-test-invert-bvashr-1.smt2
2246   regress1/quantifiers/qbv-test-invert-bvcomp.smt2
2247   regress1/quantifiers/qbv-test-invert-bvlshr-1.smt2
2248   regress1/quantifiers/qbv-test-invert-bvmul-neq.smt2
2249   regress1/quantifiers/qbv-test-invert-bvmul.smt2
2250   regress1/quantifiers/qbv-test-invert-bvudiv-0-neq.smt2
2251   regress1/quantifiers/qbv-test-invert-bvudiv-0.smt2
2252   regress1/quantifiers/qbv-test-invert-bvudiv-1-neq.smt2
2253   regress1/quantifiers/qbv-test-invert-bvudiv-1.smt2
2254   regress1/quantifiers/qbv-test-invert-bvurem-1-neq.smt2
2255   regress1/quantifiers/qbv-test-invert-bvurem-1.smt2
2256   regress1/quantifiers/qbv-test-urem-rewrite.smt2
2257   regress1/quantifiers/qcft-javafe.filespace.TreeWalker.006.smt2
2258   regress1/quantifiers/qcft-smtlib3dbc51.smt2
2259   regress1/quantifiers/qe.smt2
2260   regress1/quantifiers/qe-partial.smt2
2261   regress1/quantifiers/qe-subtypes.smt2
2262   regress1/quantifiers/qid.smt2
2263   regress1/quantifiers/qid-debug-inst.smt2
2264   regress1/quantifiers/quant-wf-int-ind.smt2
2265   regress1/quantifiers/quaternion_ds1_symm_0428.fof.smt2
2266   regress1/quantifiers/qs-has-term.smt2
2267   regress1/quantifiers/recfact.cvc.smt2
2268   regress1/quantifiers/rel-trigger-unusable.smt2
2269   regress1/quantifiers/repair-const-nterm.smt2
2270   regress1/quantifiers/rew-to-0211-dd.smt2
2271   regress1/quantifiers/ricart-agrawala6.smt2
2272   regress1/quantifiers/set-choice-koikonomou.cvc.smt2
2273   regress1/quantifiers/set3.smt2
2274   regress1/quantifiers/set8.smt2
2275   regress1/quantifiers/seu169+1.smt2
2276   regress1/quantifiers/seq-solved-enum.smt2
2277   regress1/quantifiers/seq-unsolved-ematch.smt2
2278   regress1/quantifiers/seqa-unsat-unknown-110921.smt2
2279   regress1/quantifiers/small-pipeline-fixpoint-3.smt2
2280   regress1/quantifiers/smtcomp-qbv-053118.smt2
2281   regress1/quantifiers/smtlib384a03.smt2
2282   regress1/quantifiers/smtlib46f14a.smt2
2283   regress1/quantifiers/smtlibe99bbe.smt2
2284   regress1/quantifiers/smtlibf957ea.smt2
2285   regress1/quantifiers/stream-x2014-09-18-unsat.smt2
2286   regress1/quantifiers/sygus-infer-nested.smt2
2287   regress1/quantifiers/sygus-inst-nia-psyco-060.smt2
2288   regress1/quantifiers/symmetric_unsat_7.smt2
2289   regress1/quantifiers/tpp-unit-fail-qbv.smt2
2290   regress1/quantifiers/var-eq-trigger.smt2
2291   regress1/quantifiers/var-eq-trigger-simple.smt2
2292   regress1/quantifiers/z3.620661-no-fv-trigger.smt2
2293   regress1/rels/addr_book_1.cvc.smt2
2294   regress1/rels/addr_book_1_1.cvc.smt2
2295   regress1/rels/bv1-unit.cvc.smt2
2296   regress1/rels/bv1-unitb.cvc.smt2
2297   regress1/rels/bv1.cvc.smt2
2298   regress1/rels/bv1p-sat.cvc.smt2
2299   regress1/rels/bv1p.cvc.smt2
2300   regress1/rels/bv2.cvc.smt2
2301   regress1/rels/iden_1_1.cvc.smt2
2302   regress1/rels/join-eq-structure-and.cvc.smt2
2303   regress1/rels/join-eq-structure.cvc.smt2
2304   regress1/rels/joinImg_0_1.cvc.smt2
2305   regress1/rels/joinImg_0_2.cvc.smt2
2306   regress1/rels/joinImg_1.cvc.smt2
2307   regress1/rels/joinImg_1_1.cvc.smt2
2308   regress1/rels/joinImg_2.cvc.smt2
2309   regress1/rels/joinImg_2_1.cvc.smt2
2310   regress1/rels/prod-mod-eq.cvc.smt2
2311   regress1/rels/prod-mod-eq2.cvc.smt2
2312   regress1/rels/qgu-fuzz-relations-2.smt2
2313   regress1/rels/qgu-fuzz-relations-3-upwards.smt2
2314   regress1/rels/rel_complex_3.cvc.smt2
2315   regress1/rels/rel_complex_4.cvc.smt2
2316   regress1/rels/rel_complex_5.cvc.smt2
2317   regress1/rels/rel_mix_0_1.cvc.smt2
2318   regress1/rels/rel_pressure_0.cvc.smt2
2319   regress1/rels/rel_tc_10_1.cvc.smt2
2320   regress1/rels/rel_tc_4.cvc.smt2
2321   regress1/rels/rel_tc_4_1.cvc.smt2
2322   regress1/rels/rel_tc_5_1.cvc.smt2
2323   regress1/rels/rel_tc_6.cvc.smt2
2324   regress1/rels/rel_tc_9_1.cvc.smt2
2325   regress1/rels/rel_tp_2.cvc.smt2
2326   regress1/rels/rel_tp_join_2_1.cvc.smt2
2327   regress1/rels/set-strat.cvc.smt2
2328   regress1/rels/strat.cvc.smt2
2329   regress1/rr-verify/bool-crci.sy
2330   regress1/rr-verify/bv-term-32.sy
2331   regress1/rr-verify/bv-term.sy
2332   regress1/rr-verify/fp-arith.sy
2333   regress1/rr-verify/fp-bool.sy
2334   regress1/rr-verify/string-term.sy
2335   regress1/sep/chain-int.smt2
2336   regress1/sep/crash1220.smt2
2337   regress1/sep/dispose-list-4-init.smt2
2338   regress1/sep/fmf-nemp-2.smt2
2339   regress1/sep/loop-1220.smt2
2340   regress1/sep/pto-04.smt2
2341   regress1/sep/quant_wand.smt2
2342   regress1/sep/sep-02.smt2
2343   regress1/sep/sep-03.smt2
2344   regress1/sep/sep-find2.smt2
2345   regress1/sep/sep-neg-1refine.smt2
2346   regress1/sep/sep-neg-nstrict.smt2
2347   regress1/sep/sep-neg-nstrict2.smt2
2348   regress1/sep/sep-neg-simple.smt2
2349   regress1/sep/sep-neg-swap.smt2
2350   regress1/sep/sep-nterm-again.smt2
2351   regress1/sep/sep-nterm-val-model.smt2
2352   regress1/sep/sep-simp-unc.smt2
2353   regress1/sep/simple-neg-sat.smt2
2354   regress1/sep/sl-standard.smt2
2355   regress1/sep/split-find-unsat-w-emp.smt2
2356   regress1/sep/split-find-unsat.smt2
2357   regress1/sep/wand-0526-sat.smt2
2358   regress1/sep/wand-false.smt2
2359   regress1/sep/wand-nterm-simp.smt2
2360   regress1/sep/wand-nterm-simp2.smt2
2361   regress1/sep/wand-simp-sat.smt2
2362   regress1/sep/wand-simp-sat2.smt2
2363   regress1/sep/wand-simp-unsat.smt2
2364   regress1/seq/issue8148-2-const-mv.smt2
2365   regress1/seq/issue8148-const-mv.smt2
2366   regress1/sets/choose.cvc.smt2
2367   regress1/sets/choose1.smt2
2368   regress1/sets/choose2.smt2
2369   regress1/sets/choose3.smt2
2370   regress1/sets/choose4.smt2
2371   regress1/sets/issue5705-cg-subtyping.smt2
2372   regress1/sets/ListElem.hs.fqout.cvc4.38.smt2
2373   regress1/sets/ListElts.hs.fqout.cvc4.317.smt2
2374   regress1/sets/TalkingAboutSets.hs.fqout.cvc4.3577.smt2
2375   regress1/sets/UniqueZipper.hs.1030minimized.cvc4.smt2
2376   regress1/sets/UniqueZipper.hs.1030minimized2.cvc4.smt2
2377   regress1/sets/UniqueZipper.hs.fqout.cvc4.10.smt2
2378   regress1/sets/UniqueZipper.hs.fqout.cvc4.1832.smt2
2379   regress1/sets/arjun-set-univ.cvc.smt2
2380   regress1/sets/card-3.smt2
2381   regress1/sets/card-4.smt2
2382   regress1/sets/card-5.smt2
2383   regress1/sets/card-6.smt2
2384   regress1/sets/card-7.smt2
2385   regress1/sets/card-vc6-minimized.smt2
2386   regress1/sets/comp-intersect.smt2
2387   regress1/sets/comp-odd.smt2
2388   regress1/sets/comp-positive.smt2
2389   regress1/sets/comp-pos-member.smt2
2390   regress1/sets/copy_check_heap_access_33_4.smt2
2391   regress1/sets/deepmeas0.hs.fqout.cvc4.41.smt2
2392   regress1/sets/finite-type/bug3663.smt2
2393   regress1/sets/finite-type/sets-card-arrcolor.smt2
2394   regress1/sets/finite-type/sets-card-arrunit.smt2
2395   regress1/sets/finite-type/sets-card-bool-1.smt2
2396   regress1/sets/finite-type/sets-card-bool-2.smt2
2397   regress1/sets/finite-type/sets-card-bool-3.smt2
2398   regress1/sets/finite-type/sets-card-bool-4.smt2
2399   regress1/sets/finite-type/sets-card-bool-rec.smt2
2400   regress1/sets/finite-type/sets-card-bv-1.smt2
2401   regress1/sets/finite-type/sets-card-bv-2.smt2
2402   regress1/sets/finite-type/sets-card-bv-3.smt2
2403   regress1/sets/finite-type/sets-card-bv-4.smt2
2404   regress1/sets/finite-type/sets-card-color.smt2
2405   regress1/sets/finite-type/sets-card-color-sat.smt2
2406   regress1/sets/finite-type/sets-card-datatype-1.smt2
2407   regress1/sets/finite-type/sets-card-datatype-2.smt2
2408   regress1/sets/finite-type/sets-card-neg-mem-union-1.smt2
2409   regress1/sets/fuzz14418.smt2
2410   regress1/sets/fuzz15201.smt2
2411   regress1/sets/fuzz31811.smt2
2412   regress1/sets/infinite-type/sets-card-array-int-1.smt2
2413   regress1/sets/infinite-type/sets-card-array-int-2.smt2
2414   regress1/sets/infinite-type/sets-card-int-1.smt2
2415   regress1/sets/infinite-type/sets-card-int-2.smt2
2416   regress1/sets/insert_invariant_37_2.smt2
2417   regress1/sets/is_singleton1.smt2
2418   regress1/sets/issue2568.smt2
2419   regress1/sets/issue2904.smt2
2420   regress1/sets/issue4124-need-check.smt2
2421   regress1/sets/issue4370-2-lemma-ee-iter.smt2
2422   regress1/sets/issue4370-4-lemma-ee-iter.smt2
2423   regress1/sets/issue4391-card-lasso.smt2
2424   regress1/sets/issue5271.smt2
2425   regress1/sets/issue5309.smt2
2426   regress1/sets/issue5342.smt2
2427   regress1/sets/issue5342_difference_version.smt2
2428   regress1/sets/issue5942-witness.smt2
2429   regress1/sets/lemmabug-ListElts317minimized.smt2
2430   regress1/sets/proj-issue164.smt2
2431   regress1/sets/proj-issue178.smt2
2432   regress1/sets/proj-issue494-finite-leafof.smt2
2433   regress1/sets/remove_check_free_31_6.smt2
2434   regress1/sets/sets-disequal.smt2
2435   regress1/sets/sets-tuple-poly.cvc.smt2
2436   regress1/sets/sets-uc-wrong.smt2
2437   regress1/sets/set-comp-sat.smt2
2438   regress1/sets/sharingbug.smt2
2439   regress1/sets/univ-set-uf-elim.smt2
2440   regress1/simplification_bug4.smt2
2441   regress1/sqrt2-sort-inf-unk.smt2
2442   regress1/strings/artemis-0512-nonterm.smt2
2443   regress1/strings/at001.smt2
2444   regress1/strings/bug615.smt2
2445   regress1/strings/bug682.smt2
2446   regress1/strings/bug686dd.smt2
2447   regress1/strings/bug768.smt2
2448   regress1/strings/bug799-min.smt2
2449   regress1/strings/cee-norn-aes-trivially.smt2
2450   regress1/strings/chapman150408.smt2
2451   regress1/strings/cmu-2db2-extf-reg.smt2
2452   regress1/strings/cmu-5042-0707-2.smt2
2453   regress1/strings/cmu-inc-nlpp-071516.smt2
2454   regress1/strings/cmu-substr-rw.smt2
2455   regress1/strings/code-sequence.smt2
2456   regress1/strings/complement-test.smt2
2457   regress1/strings/indexof_re_red.smt2
2458   regress1/strings/crash-1019.smt2
2459   regress1/strings/csp-prefix-exp-bug.smt2
2460   regress1/strings/double-replace.smt2
2461   regress1/strings/fmf001.smt2
2462   regress1/strings/fmf002.smt2
2463   regress1/strings/gm-inc-071516-2.smt2
2464   regress1/strings/goodAI.smt2
2465   regress1/strings/idof-handg.smt2
2466   regress1/strings/idof-nconst-index.smt2
2467   regress1/strings/idof-neg-index.smt2
2468   regress1/strings/idof-triv.smt2
2469   regress1/strings/ilc-l-nt.smt2
2470   regress1/strings/instance1079-re-loop-cong.smt2
2471   regress1/strings/instance2984-null-term.smt2
2472   regress1/strings/instance3303-delta.smt2
2473   regress1/strings/instance6561-dd-concat-unify-char.smt2
2474   regress1/strings/instance7075-delta.smt2
2475   regress1/strings/issue1105.smt2
2476   regress1/strings/issue1684-regex.smt2
2477   regress1/strings/issue2060.smt2
2478   regress1/strings/issue2429-code.smt2
2479   regress1/strings/issue2981.smt2
2480   regress1/strings/issue2982.smt2
2481   regress1/strings/issue3090.smt2
2482   regress1/strings/issue3217.smt2
2483   regress1/strings/issue3272.smt2
2484   regress1/strings/issue3357.smt2
2485   regress1/strings/issue3657-unexpectedUnsatCVC4.smt2
2486   regress1/strings/issue4379.smt2
2487   regress1/strings/issue4608-re-derive.smt2
2488   regress1/strings/issue4701_substr_splice.smt2
2489   regress1/strings/issue4735.smt2
2490   regress1/strings/issue4735_2.smt2
2491   regress1/strings/issue4759-comp-delta.smt2
2492   regress1/strings/issue5330.smt2
2493   regress1/strings/issue5330_2.smt2
2494   regress1/strings/issue5374-proxy-i.smt2
2495   regress1/strings/issue5406-eager-pp.smt2
2496   regress1/strings/issue5483-pp-leq.smt2
2497   regress1/strings/issue5510-re-consume.smt2
2498   regress1/strings/issue5520-re-consume.smt2
2499   regress1/strings/issue5610-infer-proxy.smt2
2500   regress1/strings/issue5610-2-infer-proxy.smt2
2501   regress1/strings/issue5611-deq-norm-emp.smt2
2502   regress1/strings/issue5692-infer-proxy.smt2
2503   regress1/strings/issue5780-repeat-skolem.smt2
2504   regress1/strings/issue5940-skc-len-conc.smt2
2505   regress1/strings/issue5940-2-skc-len-conc.smt2
2506   regress1/strings/issue6057-replace-re.smt2
2507   regress1/strings/issue6057-replace-re-all-jiwonparc.smt2
2508   regress1/strings/issue6072-inc-no-const-reg.smt2
2509   regress1/strings/issue6075-repl-len-one-rr.smt2
2510   regress1/strings/issue6101.smt2
2511   regress1/strings/issue6101-2.smt2
2512   regress1/strings/issue6132-non-unique-skolem.smt2
2513   regress1/strings/issue6142-repl-inv-rew.smt2
2514   regress1/strings/issue6180-proxy-vars.smt2
2515   regress1/strings/issue6180-2-proxy-vars.smt2
2516   regress1/strings/issue6184-unsat-core.smt2
2517   regress1/strings/issue6191-replace-all.smt2
2518   regress1/strings/issue6203-1-substr-ctn-strip.smt2
2519   regress1/strings/issue6203-2-re-ccache.smt2
2520   regress1/strings/issue6203-6-replace-re.smt2
2521   regress1/strings/issue6214-2-sym-re-inc.smt2
2522   regress1/strings/issue6214-3-sym-re-inc.smt2
2523   regress1/strings/issue6214-4-sym-re-inc.smt2
2524   regress1/strings/issue6270.smt2
2525   regress1/strings/issue6271-rnf.smt2
2526   regress1/strings/issue6271-2-rnf.smt2
2527   regress1/strings/issue6337-replace-re-all.smt2
2528   regress1/strings/issue6337-replace-re.smt2
2529   regress1/strings/issue6567-empty-re-range.smt2
2530   regress1/strings/issue6604-2.smt2
2531   regress1/strings/issue6635-rre.smt2
2532   regress1/strings/issue6653-2-update-c-len.smt2
2533   regress1/strings/issue6653-3-seq.smt2
2534   regress1/strings/issue6653-4-rre.smt2
2535   regress1/strings/issue6653-rre.smt2
2536   regress1/strings/issue6653-rre-small.smt2
2537   regress1/strings/issue6654-indexof_re_red.smt2
2538   regress1/strings/issue6766-re-elim-bv.smt2
2539   regress1/strings/issue6777-seq-nth-eval-cm.smt2
2540   regress1/strings/issue6913.smt2
2541   regress1/strings/issue6973-dup-lemma-conc.smt2
2542   regress1/strings/issue7677-test-const-rv.smt2
2543   regress1/strings/issue7918-learned-rewrite.smt2
2544   regress1/strings/issue8094-witness-model.smt2
2545   regress1/strings/kaluza-fl.smt2
2546   regress1/strings/loop002.smt2
2547   regress1/strings/loop003.smt2
2548   regress1/strings/loop004.smt2
2549   regress1/strings/loop005.smt2
2550   regress1/strings/loop006.smt2
2551   regress1/strings/loop007.smt2
2552   regress1/strings/loop008.smt2
2553   regress1/strings/loop009.smt2
2554   regress1/strings/nf-ff-contains-abs.smt2
2555   regress1/strings/no-lazy-pp-quant.smt2
2556   regress1/strings/non_termination_regular_expression4.smt2
2557   regress1/strings/non-terminating-rewrite-aent.smt2
2558   regress1/strings/norn-13.smt2
2559   regress1/strings/norn-360.smt2
2560   regress1/strings/norn-ab.smt2
2561   regress1/strings/norn-nel-bug-052116.smt2
2562   regress1/strings/norn-simp-rew-sat.smt2
2563   regress1/strings/nt6-dd.smt2
2564   regress1/strings/nterm-re-inter-sigma.smt2
2565   regress1/strings/open-pf-merge.smt2
2566   regress1/strings/pattern1.smt2
2567   regress1/strings/pierre150331.smt2
2568   regress1/strings/policy_variable.smt2
2569   regress1/strings/pre_ctn_no_skolem_share.smt2
2570   regress1/strings/proj254-re-elim-agg.smt2
2571   regress1/strings/proj-issue281.smt2
2572   regress1/strings/proj-issue331.smt2
2573   regress1/strings/proj-issue502-merge-type.smt2
2574   regress1/strings/query4674.smt2
2575   regress1/strings/query8485.smt2
2576   regress1/strings/re-all-char-hard.smt2
2577   regress1/strings/re-agg-total1.smt2
2578   regress1/strings/re-agg-total2.smt2
2579   regress1/strings/re-elim-exact.smt2
2580   regress1/strings/re-mod-eq.smt2
2581   regress1/strings/re-neg-concat-reduct.smt2
2582   regress1/strings/re-neg-unfold-rev-a.smt2
2583   regress1/strings/re-unsound-080718.smt2
2584   regress1/strings/regexp001.smt2
2585   regress1/strings/regexp002.smt2
2586   regress1/strings/regexp003.smt2
2587   regress1/strings/regexp-050-multiply-graft-fuzz-dd.smt2
2588   regress1/strings/regexp-strat-fix.smt2
2589   regress1/strings/reloop.smt2
2590   regress1/strings/repl-empty-sem.smt2
2591   regress1/strings/repl-soundness-sem.smt2
2592   regress1/strings/replaceall-len.smt2
2593   regress1/strings/replaceall-replace.smt2
2594   regress1/strings/rev-conv1.smt2
2595   regress1/strings/rev-ex1.smt2
2596   regress1/strings/rev-ex2.smt2
2597   regress1/strings/rev-ex3.smt2
2598   regress1/strings/rev-ex4.smt2
2599   regress1/strings/rev-ex5.smt2
2600   regress1/strings/rew-020618.smt2
2601   regress1/strings/rew-check1.smt2
2602   regress1/strings/seq-cardinality.smt2
2603   regress1/strings/seq-quant-infinite-branch.smt2
2604   regress1/strings/seq-skeleton-gap.smt2
2605   regress1/strings/simple-re-consume.smt2
2606   regress1/strings/stoi-400million.smt2
2607   regress1/strings/stoi-solve.smt2
2608   regress1/strings/str-code-sat.smt2
2609   regress1/strings/str-code-unsat-2.smt2
2610   regress1/strings/str-code-unsat-3.smt2
2611   regress1/strings/str-code-unsat.smt2
2612   regress1/strings/str-rev-simple-s.smt2
2613   regress1/strings/str001.smt2
2614   regress1/strings/str002.smt2
2615   regress1/strings/str006.smt2
2616   regress1/strings/str007.smt2
2617   regress1/strings/string-unsound-sem.smt2
2618   regress1/strings/strings-index-empty.smt2
2619   regress1/strings/strings-leq-trans-unsat.smt2
2620   regress1/strings/strings-lt-len5.smt2
2621   regress1/strings/strings-lt-simple.smt2
2622   regress1/strings/strip-endpt-sound.smt2
2623   regress1/strings/substr001.smt2
2624   regress1/strings/tolower-find.smt2
2625   regress1/strings/timeout-no-resp.smt2
2626   regress1/strings/type002.smt2
2627   regress1/strings/type003.smt2
2628   regress1/strings/update-ex1.smt2
2629   regress1/strings/update-ex2.smt2
2630   regress1/strings/username_checker_min.smt2
2631   regress1/strings/witness-model.smt2
2632   regress1/sygus/VC22_a.sy
2633   regress1/sygus/abv.sy
2634   regress1/sygus/array-grammar-store.sy
2635   regress1/sygus/array_search_5-Q-easy.sy
2636   regress1/sygus/array-uc.sy
2637   regress1/sygus/bvudiv-by-2.sy
2638   regress1/sygus/cegar1.sy
2639   regress1/sygus/cegis-unif-inv-eq-fair.sy
2640   regress1/sygus/cggmp.sy
2641   regress1/sygus/clock-inc-tuple.sy
2642   regress1/sygus/coeff-solve-inv.sy
2643   regress1/sygus/commutative-stream.sy
2644   regress1/sygus/commutative.sy
2645   regress1/sygus/concat_extract_example.sy
2646   regress1/sygus/constant-bool-si-all.sy
2647   regress1/sygus/constant-dec-tree-bug.sy
2648   regress1/sygus/constant-ite-bv.sy
2649   regress1/sygus/constant.sy
2650   regress1/sygus/crci-ssb-unk.sy
2651   regress1/sygus/crcy-si.sy
2652   regress1/sygus/cube-nia.sy
2653   regress1/sygus/discPresent.sy
2654   regress1/sygus/double.sy
2655   regress1/sygus/dt-test-ns.sy
2656   regress1/sygus/dup-op.sy
2657   regress1/sygus/eq-sub-obs.sy
2658   regress1/sygus/error1-dt.sy
2659   regress1/sygus/eval-uc.sy
2660   regress1/sygus/extract.sy
2661   regress1/sygus/fast-enum-backtrack.sy
2662   regress1/sygus/fg_polynomial3.sy
2663   regress1/sygus/find_inv_eq_bvmul_4bit_withoutgrammar-v2.sy
2664   regress1/sygus/find_sc_bvult_bvnot.sy
2665   regress1/sygus/ground-ite-free-constant-si.sy
2666   regress1/sygus/hd-01-d1-prog.sy
2667   regress1/sygus/hd-19-d1-prog-dup-op.sy
2668   regress1/sygus/hd-sdiv.sy
2669   regress1/sygus/ho-sygus.sy
2670   regress1/sygus/icfp_14.12-flip-args.sy
2671   regress1/sygus/icfp_14.12.sy
2672   regress1/sygus/icfp_14_12_diff_types.sy
2673   regress1/sygus/icfp_28_10.sy
2674   regress1/sygus/icfp_easy-ite.sy
2675   regress1/sygus/incremental-stream-ex.sy
2676   regress1/sygus/incremental-stream-ex2.sy
2677   regress1/sygus/int-any-const.sy
2678   regress1/sygus/inv-example.sy
2679   regress1/sygus/inv-missed-sol-true.sy
2680   regress1/sygus/inv-unused.sy
2681   regress1/sygus/interpol1.smt2
2682   regress1/sygus/interpol1-push-pop.smt2
2683   regress1/sygus/interpol3.smt2
2684   regress1/sygus/interpol3-next.smt2
2685   regress1/sygus/interpol_arr1.smt2
2686   regress1/sygus/interpol_arr2.smt2
2687   regress1/sygus/interpol_cosa_1.smt2
2688   regress1/sygus/interpol_from_pono_1.smt2
2689   regress1/sygus/interpol_from_pono_2.smt2
2690   regress1/sygus/issue2914.sy
2691   regress1/sygus/issue2935.sy
2692   regress1/sygus/issue3109-share-sel.sy
2693   regress1/sygus/issue3199.smt2
2694   regress1/sygus/issue3200.smt2
2695   regress1/sygus/issue3201.smt2
2696   regress1/sygus/issue3205.smt2
2697   regress1/sygus/issue3247.smt2
2698   regress1/sygus/issue3320-quant.sy
2699   regress1/sygus/issue3461.sy
2700   regress1/sygus/issue3514.smt2
2701   regress1/sygus/issue3507.smt2
2702   regress1/sygus/issue3580.sy
2703   regress1/sygus/issue3633.smt2
2704   regress1/sygus/issue3634.smt2
2705   regress1/sygus/issue3635.smt2
2706   regress1/sygus/issue3644.smt2
2707   regress1/sygus/issue3649.sy
2708   regress1/sygus/issue3802-default-consts.sy
2709   regress1/sygus/issue3839-cond-rewrite.smt2
2710   regress1/sygus/issue3944-div-rewrite.smt2
2711   regress1/sygus/issue3947-agg-miniscope.smt2
2712   regress1/sygus/issue3995-fmf-var-op.smt2
2713   regress1/sygus/issue4009-qep.smt2
2714   regress1/sygus/issue4025-no-rlv-cond.smt2
2715   regress1/sygus/issue4083-var-shadow.smt2
2716   regress1/sygus/issue4425-sets-sygus-infer.smt2
2717   regress1/sygus/issue7925-dt-share-config.sy
2718   regress1/sygus/issue8216-rr-input-re.smt2
2719   regress1/sygus/large-const-simp.sy
2720   regress1/sygus/let-bug-simp.sy
2721   regress1/sygus/list-head-x.sy
2722   regress1/sygus/list_recursor.sy
2723   regress1/sygus/logiccell_help.sy
2724   regress1/sygus/max-all.sy
2725   regress1/sygus/max-limit.sy
2726   regress1/sygus/max-try1.sy
2727   regress1/sygus/max-try2.sy
2728   regress1/sygus/max.sy
2729   regress1/sygus/max2-bv.sy
2730   regress1/sygus/multi-fun-polynomial2.sy
2731   regress1/sygus/complex-no-rewrite.sy
2732   regress1/sygus/complex-rewrite-in-db.sy
2733   regress1/sygus/no-var-in-sol.sy
2734   regress1/sygus/simple-no-rewrite.sy
2735   regress1/sygus/simple-rewrite-in-db.sy
2736   regress1/sygus/simple-rewrite-not-in-db.sy
2737   regress1/sygus/nflat-fwd-3.sy
2738   regress1/sygus/nflat-fwd.sy
2739   regress1/sygus/nia-max-square-ns.sy
2740   regress1/sygus/node-discrete.sy
2741   regress1/sygus/no-flat-simp.sy
2742   regress1/sygus/no-mention.sy
2743   regress1/sygus/once_2.sy
2744   regress1/sygus/only-const-grammar.sy
2745   regress1/sygus/pbe_multi.sy
2746   regress1/sygus/phone-1-long.sy
2747   regress1/sygus/planning-unif.sy
2748   regress1/sygus/process-10-vars.sy
2749   regress1/sygus/proj-issue135.smt2
2750   regress1/sygus/proj-issue165.smt2
2751   regress1/sygus/proj-issue181.smt2
2752   regress1/sygus/proj-issue183.smt2
2753   regress1/sygus/proj-issue185.smt2
2754   regress1/sygus/proj-issue264.smt2
2755   regress1/sygus/pLTL_5_trace.sy
2756   regress1/sygus/qe.sy
2757   regress1/sygus/qf_abv.smt2
2758   regress1/sygus/rand_const.sy
2759   regress1/sygus/rand_p_0.sy
2760   regress1/sygus/rand_p_1.sy
2761   regress1/sygus/real-any-const.sy
2762   regress1/sygus/real-grammar.sy
2763   regress1/sygus/rec-fun-swap.sy
2764   regress1/sygus/rec-fun-sygus.sy
2765   regress1/sygus/rec-fun-while-1.sy
2766   regress1/sygus/rec-fun-while-2.sy
2767   regress1/sygus/rec-fun-while-infinite.sy
2768   regress1/sygus/re-concat.sy
2769   regress1/sygus/repair-const-rl.sy
2770   regress1/sygus/replicate-mod.sy
2771   regress1/sygus/replicate-mod-assume.sy
2772   regress1/sygus/rex-strings-alarm.sy
2773   regress1/sygus/sets-pred-test.sy
2774   regress1/sygus/simple-regexp.sy
2775   regress1/sygus/stopwatch-bt.sy
2776   regress1/sygus/strings-any-term1.sy
2777   regress1/sygus/strings-no-syntax.sy
2778   regress1/sygus/strings-concat-3-args.sy
2779   regress1/sygus/strings-double-rec.sy
2780   regress1/sygus/strings-small.sy
2781   regress1/sygus/strings-template-infer-unused.sy
2782   regress1/sygus/strings-template-infer.sy
2783   regress1/sygus/strings-trivial-simp.sy
2784   regress1/sygus/strings-trivial-two-type.sy
2785   regress1/sygus/strings-trivial.sy
2786   regress1/sygus/sygus-dt.sy
2787   regress1/sygus/sygus-lambda-fv.sy
2788   regress1/sygus/sygus-uf-ex.sy
2789   regress1/sygus/t8.sy
2790   regress1/sygus/temp_input_to_synth_ic-error-121418.sy
2791   regress1/sygus/tester.sy
2792   regress1/sygus/tl-type-0.sy
2793   regress1/sygus/tl-type-4x.sy
2794   regress1/sygus/tl-type.sy
2795   regress1/sygus/triv-type-mismatch-si.sy
2796   regress1/sygus/trivial-stream.sy
2797   regress1/sygus/twolets1.sy
2798   regress1/sygus/twolets2-orig.sy
2799   regress1/sygus/unbdd_inv_gen_winf1.sy
2800   regress1/sygus/univ_2-long-repeat.sy
2801   regress1/sym/q-constant.smt2
2802   regress1/sym/q-function.smt2
2803   regress1/sym/qf-function.smt2
2804   regress1/sym/sb-wrong.smt2
2805   regress1/sym/sym-setAB.smt2
2806   regress1/sym/sym1.smt2
2807   regress1/sym/sym2.smt2
2808   regress1/sym/sym3.smt2
2809   regress1/sym/sym4.smt2
2810   regress1/sym/sym5.smt2
2811   regress1/sym/sym6.smt2
2812   regress1/sym/sym7-uf.smt2
2813   regress1/test12.cvc.smt2
2814   regress1/trim.cvc.smt2
2815   regress1/uf2.smt2
2816   regress1/uflia/DRAGON_11_e1_2450.ec.minimized.smt2
2817   regress1/uflia/FIREFLY_3_e2_2236_e7_3681.ec.core.smt2
2818   regress1/uflia/FIREFLY_luke_1b_e2_3049_e7_1173.ec.minimized.smt2
2819   regress1/uflia/error1.smtv1.smt2
2820   regress1/uflia/microwave21.ec.minimized.smt2
2821   regress1/uflia/simple_cyclic2.smt2
2822   regress1/uflia/speed2_e8_449_e8_517.ec.smt2
2823   regress1/uflia/stalmark_e7_27_e7_31.ec.smt2
2824   regress1/wrong-qfabvfp-smtcomp2018.smt2
2825 )
2826
2827 #-----------------------------------------------------------------------------#
2828 # Regression level 2 tests
2829
2830 set(regress_2_tests
2831   regress2/DTP_k2_n35_c175_s15.smt2
2832   regress2/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2
2833   regress2/GEO123+1.minimized.smt2
2834   regress2/arith/arith-int-098.cvc.smt2
2835   regress2/arith/pursuit-safety-11.smtv1.smt2
2836   regress2/arith/pursuit-safety-12.smtv1.smt2
2837   regress2/arith/real2int-test.smt2
2838   regress2/arith/sc-7.base.cvc.smtv1.smt2
2839   regress2/arith/uart-8.base.cvc.smtv1.smt2
2840   regress2/bug136.smtv1.smt2
2841   regress2/bug148.smtv1.smt2
2842   regress2/bug349.smtv1.smt2
2843   regress2/bug374.smtv1.smt2
2844   regress2/bug394.smt2
2845   regress2/bug674.smt2
2846   regress2/bug765.smt2
2847   regress2/bug812.smt2
2848   regress2/bv/opStructure_MBA_6.scrambled.min.smt2
2849   regress2/bv_to_int2.smt2
2850   regress2/bv_to_int_5095.smt2
2851   regress2/bv_to_int_5095_2.smt2
2852   regress2/bv_to_int_ashr.smt2
2853   regress2/bv_to_int_bitwise.smt2
2854   regress2/bv_to_int_bvuf_to_intuf_smtlib.smt2
2855   regress2/bv_to_int_bvmul1.smt2
2856   regress2/bv_to_int_inc1.smt2
2857   regress2/bv_to_int_mask_array_2.smt2
2858   regress2/bv_to_int_mask_array_3.smt2
2859   regress2/bv_to_int_shifts.smt2
2860   regress2/bv_to_int_quantifiers_bvand.smt2
2861   regress2/error1.smtv1.smt2
2862   regress2/fp/issue7056.smt2
2863   regress2/fuzz_2.smtv1.smt2
2864   regress2/hash_sat_06_19.smt2
2865   regress2/hash_sat_07_17.smt2
2866   regress2/hash_sat_09_09.smt2
2867   regress2/hash_sat_10_09.smt2
2868   regress2/ho/auth0068.smt2
2869   regress2/ho/bug_instfalse_SEU882^5.p
2870   regress2/ho/fta0409.smt2
2871   regress2/ho/involved_parsing_ALG248^3.p
2872   regress2/ho/partial_app_interpreted_SWW474^2.p
2873   regress2/hole7.cvc.smt2
2874   regress2/hole8.cvc.smt2
2875   regress2/instance_1444.smtv1.smt2
2876   regress2/issue3687-check-models.smt2
2877   regress2/issue4707-bv-to-bool-large.smt2
2878   regress2/issue6495-dup-pat-term.smt2
2879   regress2/lemmas/simple_startup_9nodes.abstract.base.smtv1.smt2
2880   regress2/javafe.ast.StandardPrettyPrint.319_no_forall.smt2
2881   regress2/javafe.ast.WhileStmt.447_no_forall.smt2
2882   regress2/nl/ufnia-factor-open-proof.smt2
2883   regress2/ooo.rf6.smt2
2884   regress2/ooo.tag10.smt2
2885   regress2/piVC_5581bd.smt2
2886   regress2/proofs/sat-proof-reloaded-reason.smt2
2887   regress2/push-pop/DRAGON_4_e2_2799_e3_1915.lus.ic3.1.min.smt2
2888   regress2/quantifiers/AdditiveMethods_AdditiveMethods..ctor.smt2
2889   regress2/quantifiers/cee-event-wrong-sat.smt2
2890   regress2/quantifiers/gn-wrong-091018.smt2
2891   regress2/quantifiers/issue3481-unsat1.smt2
2892   regress2/quantifiers/javafe.ast.StandardPrettyPrint.319.smt2
2893   regress2/quantifiers/javafe.ast.WhileStmt.447.smt2
2894   regress2/quantifiers/javafe.tc.CheckCompilationUnit.001.smt2
2895   regress2/quantifiers/javafe.tc.FlowInsensitiveChecks.682.smt2
2896   regress2/quantifiers/net-policy-no-time.smt2
2897   regress2/quantifiers/nunchaku2309663.nun.min.smt2
2898   regress2/quantifiers/small-bug1-fixpoint-3.smt2
2899   regress2/quantifiers/syn874-1.smt2
2900   regress2/seq/err-model-soundness.smt2
2901   regress2/simplify.javafe.ast.ArrayInit.35_without_quantification2.smt2
2902   regress2/strings/bidir_star.smt2
2903   regress2/strings/cmi-split-cm-fail.smt2
2904   regress2/strings/cmu-dis-0707-3.smt2
2905   regress2/strings/cmu-disagree-0707-dd.smt2
2906   regress2/strings/cmu-prereg-fmf.smt2
2907   regress2/strings/cmu-repl-len-nterm.smt2
2908   regress2/strings/issue3203.smt2
2909   regress2/strings/issue5381.smt2
2910   regress2/strings/issue6483.smt2
2911   regress2/strings/issue6057-replace-re-all.smt2
2912   regress2/strings/issue6057-replace-re-all-simplified.smt2
2913   regress2/strings/issue6636-replace-re-all.smt2
2914   regress2/strings/issue6637-replace-re-all.smt2
2915   regress2/strings/issue6639-replace-re-all.smt2
2916   regress2/strings/issue918.smt2
2917   regress2/strings/non_termination_regular_expression6.smt2
2918   regress2/strings/proj-439-cyclic-str-ipc.smt2
2919   regress2/strings/proof-fail-083021-delta.smt2
2920   regress2/strings/range-perf.smt2
2921   regress2/strings/repl-repl-i-no-push.smt2
2922   regress2/strings/repl-repl.smt2
2923   regress2/strings/replace_re.smt2
2924   regress2/strings/replaceall-diffrange.smt2
2925   regress2/strings/replaceall-len-c.smt2
2926   regress2/strings/small-1.smt2
2927   regress2/strings/strings-alpha-card-65.smt2
2928   regress2/strings/update-ex3.smt2
2929   regress2/strings/update-ex4-seq.smt2
2930   regress2/sygus/MPwL_d1s3.sy
2931   regress2/sygus/array_sum_dd.sy
2932   regress2/sygus/cegisunif-depth1-bv.sy
2933   regress2/sygus/ex23.sy
2934   regress2/sygus/examples-deq.sy
2935   regress2/sygus/icfp_easy_mt_ite.sy
2936   regress2/sygus/issue4022-conjecture-gen.smt2
2937   regress2/sygus/lustre-real.sy
2938   regress2/sygus/max2-univ.sy
2939   regress2/sygus/min_IC_1.sy
2940   regress2/sygus/mpg_guard1-dd.sy
2941   regress2/sygus/multi-udiv.sy
2942   regress2/sygus/no-bad-filter.sy
2943   regress2/sygus/no-syntax-test-no-si.sy
2944   regress2/sygus/pbe_bvurem.sy
2945   regress2/sygus/process-10-vars-2fun.sy
2946   regress2/sygus/process-arg-invariance.sy
2947   regress2/sygus/proj-issue119.sy
2948   regress2/sygus/qgu-bools.sy
2949   regress2/sygus/real-grammar-neg.sy
2950   regress2/sygus/sets-fun-test.sy
2951   regress2/sygus/sumn_recur_synth.sy
2952   regress2/sygus/strings-no-syntax-len.sy
2953   regress2/sygus/three.sy
2954   regress2/typed_v1l50016-simp.cvc.smt2
2955   regress2/uflia-error0.smt2
2956   regress2/xs-09-16-3-4-1-5.smtv1.smt2
2957 )
2958
2959 #-----------------------------------------------------------------------------#
2960 # Regression level 3 tests
2961
2962 set(regress_3_tests
2963   regress3/arith/abz5_1400.smtv1.smt2
2964   regress3/arith_prp-13-24.smt2
2965   regress3/aufbv-wchains010ue.smtv1.smt2
2966   regress3/auflia-fuzz06.smtv1.smt2
2967   regress3/bmc-ibm-1.smtv1.smt2
2968   regress3/bmc-ibm-2.smtv1.smt2
2969   regress3/bmc-ibm-5.smtv1.smt2
2970   regress3/bmc-ibm-7.smtv1.smt2
2971   regress3/bug2.smtv1.smt2
2972   regress3/bv_to_int_and_or.smt2
2973   regress3/bv_to_int_bench_9839.smt2.minimized.smt2
2974   regress3/bv_to_int_check_bvsge_bvashr0_4bit.smt2.minimized.smt2
2975   regress3/bv_to_int_check_bvsgt_bvlshr0_4bit.smt2.minimized.smt2
2976   regress3/bv_to_int_check_ne_bvlshr0_4bit.smt2.minimized.smt2
2977   regress3/bv_to_int_input_mouser_detect.c.smt2.minimized.smt2
2978   regress3/bv_to_int_quant1.smt2
2979   regress3/bv_to_int_quant2.smt2
2980   regress3/bv-core-ext_con_004_001_1024.smtv1.smt2
2981   regress3/bv-fuzz15.smtv1.smt2
2982   regress3/bv-fuzz16.smtv1.smt2
2983   regress3/bv-fuzz17.smtv1.smt2
2984   regress3/cegisunif-depth1.sy
2985   regress3/decision-uflia-xs-09-16-3-4-1-5.smtv1.smt2
2986   regress3/decision-wchains010ue.smtv1.smt2
2987   regress3/DRAGON_1.lus.sy
2988   regress3/eq_diamond14.smtv1.smt2
2989   regress3/error0.smt2
2990   regress3/friedman_n4_i5.smtv1.smt2
2991   regress3/friedman_n6_i4.smtv1.smt2
2992   regress3/ho/SYO362^5.p
2993   regress3/hole9.cvc.smt2
2994   regress3/hole10.cvc.smt2
2995   regress3/incorrect1.smtv1.smt2
2996   regress3/interpol2.smt2
2997   regress3/inv_gen_n_c11.sy
2998   regress3/issue4170.smt2
2999   regress3/issue4714.smt2
3000   regress3/lpsat-goal-9.smt2
3001   regress3/nia-max-square.sy
3002   regress3/nl/iand-native-1.smt2
3003   regress3/PEQ018_size4.smtv1.smt2
3004   regress3/policyM.sy
3005   regress3/quantifiers/ForElimination-scala-9.smt2
3006   regress3/quantifiers/javafe.ast.ArrayInit.35.smt2
3007   regress3/quantifiers/sygus-inst-ufbv-sdlx-fixpoint-5.smt2
3008   regress3/qwh.35.405.shuffled-as.sat03-1651.smtv1.smt2
3009   regress3/regex-rrv.sy
3010   regress3/sixfuncs.sy
3011   regress3/specsharp-WindowsCard.15.RTE.Terminate_System.Int32.smt2
3012   regress3/strings-any-term.sy
3013   regress3/strings/extf_d_perf.smt2
3014   regress3/strings/indexof_re_red.smt2
3015   regress3/strings/norn-dis-0707-3.smt2
3016   regress3/strings/replace_re_all.smt2
3017   regress3/unbdd_inv_gen_ex7.sy
3018   regress3/vcb.sy
3019 )
3020
3021 #-----------------------------------------------------------------------------#
3022 # Regression level 4 tests
3023
3024 set(regress_4_tests
3025   regress4/bug143.smtv1.smt2
3026   regress4/bug337.smt2
3027   regress4/bug396.smt2
3028   regress4/C880mul.miter.shuffled-as.sat03-348.smtv1.smt2
3029   regress4/comb2.shuffled-as.sat03-420.smtv1.smt2
3030   regress4/fischer3-mutex-16.smtv1.smt2
3031   regress4/instance_1151.smtv1.smt2
3032   regress4/issue2429.smt2
3033   regress4/miplib-pp08a-3000.smt2
3034   regress4/miplib-pp08a-3000.smtv1.smt2
3035   regress4/NEQ016_size5.smtv1.smt2
3036   regress4/pp-regfile.smtv1.smt2
3037   regress4/sets-card-neg-mem-union-2.smt2
3038   regress4/siegel-nl-bases.smt2
3039   regress4/unsat-circ-reduce.smt2
3040   regress4/xs-11-20-5-2-5-3.smt2
3041   regress4/xs-11-20-5-2-5-3.smtv1.smt2
3042 )
3043
3044 #-----------------------------------------------------------------------------#
3045 # Disabled tests, will not be run.
3046
3047 set(regression_disabled_tests
3048   regress0/arith/miplib-opt1217--27.smtv1.smt2
3049   # unknown on some builds
3050   regress0/arith/issue7984-quant-trans.smt2
3051   regress0/aufbv/dubreva005ue.smtv1.smt2
3052   regress0/aufbv/fifo32bc06k08.smtv1.smt2
3053   regress0/aufbv/fifo32in06k08.smtv1.smt2
3054   regress0/aufbv/no_init_multi_delete14.smtv1.smt2
3055   regress0/aufbv/try3_sameret_functions_fse-bfs_tac.calc_next.il.fse-bfs.smtv1.smt2
3056   regress0/auflia/fuzz01.smtv1.smt2
3057   ###
3058   regress0/bv/test00.smtv1.smt2
3059   # timeout after fixing upwards closure for relations
3060   regress0/rels/rel_tc_7.cvc.smt2
3061   # FIXME #1649
3062   regress0/datatypes/datatype-dump.cvc.smt2
3063   # no longer support overloaded symbols across multiple parametric datatypes
3064   regress0/datatypes/repeated-selectors-2769.smt2
3065   # need finite model finding command line in tptp regression
3066   regress0/tptp/BOO003-4.p
3067   regress0/tptp/BOO027-1.p
3068   regress0/tptp/MGT031-1.p
3069   regress0/tptp/NLP114-1.p
3070   regress0/tptp/SYN075+1.p
3071   regress0/uf/iso_icl_repgen004.smtv1.smt2
3072   ###
3073   # takes around 30 sec
3074   regress1/bags/fold2.smt2
3075   regress1/bug472.smt2
3076   regress1/datatypes/non-simple-rec-set.smt2
3077   # results in an assertion failure (see issue #1650).
3078   regress1/ho/hoa0102.smt2
3079   # after disallowing solving for terms with quantifiers
3080   regress1/ho/nested_lambdas-AGT034^2.smt2
3081   regress1/ho/nested_lambdas-sat-SYO056^1-delta.smt2
3082   regress1/ho/SYO056^1.p
3083   # times out after update to circuit propagator
3084   regress1/nl/dumortier_llibre_artes_ex_5_13.transcendental.k2.smt2
3085   # times out after update to tangent planes
3086   regress1/nl/NAVIGATION2.smt2
3087   # sat or unknown in different builds
3088   regress1/nl/issue3307.smt2
3089   # times out on various builds
3090   regress1/nl/proj-issue231.smt2
3091   # times out after changes to nl-ext in #8236
3092   regress1/nl/proj-issue251.smt2
3093   # slow with sygus-inference after removing anti-skolemization
3094   regress1/quantifiers/anti-sk-simp.smt2
3095   # no longer support snorm option
3096   regress1/quantifiers/arith-snorm.smt2
3097   # timeout on some builds after changes to justification heuristic
3098   regress1/quantifiers/infer-arith-trigger-eq.smt2
3099   # ajreynol: different error messages on production and debug:
3100   regress1/quantifiers/macro-subtype-param.smt2
3101   # times out with competition build, ok with other builds:
3102   regress1/quantifiers/model_6_1_bv.smt2
3103   # time out on some regressions
3104   regress1/quantifiers/proj-issue285.smt2
3105   # ajreynol: different error messages on production and debug:
3106   regress1/quantifiers/subtype-param-unk.smt2
3107   regress1/quantifiers/subtype-param.smt2
3108   # timeout after changes to theory preprocessing, note is non-linear and does not involve sygus-inst
3109   regress1/quantifiers/sygus-inst-ufnia-sat-t3_rw1505.smt2
3110   # timeout on some builds after not applying default sygus options when using sygus-inst
3111   regress1/quantifiers/issue4062-cegqi-aux.smt2
3112   ###
3113   regress1/rels/garbage_collect.cvc.smt2
3114   regress1/sets/setofsets-disequal.smt2
3115   regress1/sets/finite-type/sets-card-neg-mem-union-2.smt2
3116   # no longer support quant-epr + sep
3117   regress1/sep/emp2-quant-unsat.smt2
3118   regress1/sep/finite-witness-sat.smt2
3119   regress1/sep/sep-fmf-priority.smt2
3120   regress1/simple-rdl-definefun.smt2
3121   # does not solve after minor modification to search
3122   regress1/sygus/car_3.lus.sy
3123   regress1/sygus/Base16_1.sy
3124   regress1/sygus/interpol_from_pono_3.smt2
3125   regress1/sygus/interpol_dt.smt2
3126   regress1/sygus/inv_gen_fig8.sy
3127   # timeout since nl-rlv is required; however it cannot be used with quantifiers
3128   regress1/sygus/issue3648.smt2
3129   # new reconstruct algorithm is slow at reconstructing random constants (see wishue #82)
3130   regress0/sygus/c100.sy
3131   # For the six regressions below, solution terms require rewrites not in
3132   # database and are too big to enumerate
3133   regress0/sygus/aig-si.sy
3134   regress0/sygus/parity-AIG-d0.sy
3135   regress1/sygus/array_search_2.sy
3136   regress1/sygus/array_sum_2_5.sy
3137   regress1/sygus/crcy-si-rcons.sy
3138   regress1/sygus/parity-si-rcons.sy
3139   # should print a better error message to indicate that a term is not in the
3140   # provided grammar
3141   regress1/sygus/simple-not-in-grammar.sy
3142   # previously sygus inference did not apply, now (correctly) times out
3143   regress1/sygus/issue3498.smt2
3144   regress2/arith/miplib-opt1217--27.smt2
3145   # times out after #7345
3146   regress2/bv_to_int_mask_array_1.smt2
3147   regress2/nl/dumortier-050317.smt2
3148   # timeout on some builds after changes to justification heuristic
3149   regress2/nl/nt-lemmas-bad.smt2
3150   # timeout after refactoring justification heuristic
3151   regress2/ho/SYO362^5.p
3152   # timeout after refactoring selectors
3153   regress2/quantifiers/exp-trivially-dd3.smt2
3154   # time out
3155   regress3/unifpi-solve-car_1.lus.sy
3156   # unknown (is sat)
3157   regress3/issue4476-ext-rew.smt2
3158 )
3159
3160 #-----------------------------------------------------------------------------#
3161 # Add target 'regress', builds and runs
3162 # > regression tests of levels 0 and 1
3163
3164 get_target_property(path_to_cvc5 cvc5-bin RUNTIME_OUTPUT_DIRECTORY)
3165 set(run_regress_script ${CMAKE_CURRENT_LIST_DIR}/run_regression.py)
3166
3167 add_custom_target(build-regress DEPENDS cvc5-bin)
3168 add_dependencies(build-tests build-regress)
3169
3170 add_custom_target(regress
3171   COMMAND
3172     ctest --output-on-failure -L "regress[0-2]" -j${CTEST_NTHREADS} $$ARGS
3173   DEPENDS build-regress)
3174
3175 macro(cvc5_add_regression_test level file)
3176   add_test(${file}
3177     ${run_regress_script}
3178     ${RUN_REGRESSION_ARGS}
3179     ${path_to_cvc5}/cvc5 ${CMAKE_CURRENT_LIST_DIR}/${file})
3180   set_tests_properties(${file} PROPERTIES LABELS "regress${level}")
3181
3182   # For CMake 3.9.0 and newer, skipped tests do not count as a failure anymore:
3183   # https://cmake.org/cmake/help/latest/release/3.9.html#other-changes
3184   # This means that for newer versions, we can use the SKIP_RETURN_CODE to mark
3185   # skipped tests as such.
3186   if(NOT ${CMAKE_VERSION} VERSION_LESS "3.9.0")
3187     set_tests_properties(${file} PROPERTIES SKIP_RETURN_CODE 77)
3188   endif()
3189 endmacro()
3190
3191 if(NOT ${CMAKE_VERSION} VERSION_LESS "3.9.0")
3192   # For CMake 3.9.0 and newer, we want the regression script to return 77 for
3193   # skipped tests, such that we can mark them as skipped. See the
3194   # `cvc5_add_regression_test` macro for more details.
3195   set(RUN_REGRESSION_ARGS ${RUN_REGRESSION_ARGS} --use-skip-return-code)
3196 endif()
3197
3198 foreach(file ${regress_0_tests})
3199   cvc5_add_regression_test(0 ${file})
3200 endforeach()
3201
3202 foreach(file ${regress_1_tests})
3203   cvc5_add_regression_test(1 ${file})
3204 endforeach()
3205
3206 foreach(file ${regress_2_tests})
3207   cvc5_add_regression_test(2 ${file})
3208 endforeach()
3209
3210 foreach(file ${regress_3_tests})
3211   cvc5_add_regression_test(3 ${file})
3212 endforeach()
3213
3214 foreach(file ${regress_4_tests})
3215   cvc5_add_regression_test(4 ${file})
3216 endforeach()