61 files changed, 227 insertions, 238 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index efe7dee36..063c4b6e2 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -25,6 +25,7 @@ set(regress_0_tests
   regress0/arith/arith.03.cvc
   regress0/arith/bug443.delta01.smtv1.smt2
   regress0/arith/bug547.2.smt2
+  regress0/arith/bug549.cvc
   regress0/arith/bug569.smt2
   regress0/arith/delta-minimized-row-vector-bug.smtv1.smt2
   regress0/arith/div-chainable.smt2
@@ -34,14 +35,22 @@ set(regress_0_tests
   regress0/arith/div.05.smt2
   regress0/arith/div.07.smt2
   regress0/arith/fuzz_3-eq.smtv1.smt2
+  regress0/arith/incorrect1.smtv1.smt2
   regress0/arith/integers/ackermann1.smt2
   regress0/arith/integers/ackermann2.smt2
   regress0/arith/integers/ackermann3.smt2
   regress0/arith/integers/ackermann4.smt2
   regress0/arith/integers/ackermann5.smt2
   regress0/arith/integers/ackermann6.smt2
+  regress0/arith/integers/arith-int-014.cvc
+  regress0/arith/integers/arith-int-015.cvc
+  regress0/arith/integers/arith-int-021.cvc
+  regress0/arith/integers/arith-int-023.cvc
+  regress0/arith/integers/arith-int-025.cvc
   regress0/arith/integers/arith-int-042.cvc
   regress0/arith/integers/arith-int-042.min.cvc
+  regress0/arith/integers/arith-int-079.cvc
+  regress0/arith/integers/arith-interval.cvc
   regress0/arith/issue1399.smt2
   regress0/arith/issue3412.smt2
   regress0/arith/issue3413.smt2
@@ -59,6 +68,9 @@ set(regress_0_tests
   regress0/arith/mod-simp.smt2
   regress0/arith/mod.01.smt2
   regress0/arith/mult.01.smt2
+  regress0/arr1.smt2
+  regress0/arr1.smtv1.smt2
+  regress0/arr2.smtv1.smt2
   regress0/array-const-real-parse.smt2
   regress0/arrayinuf_declare.smt2
   regress0/arrays/arrays0.smt2
@@ -100,11 +112,13 @@ set(regress_0_tests
   regress0/aufbv/bug338.smt2
   regress0/aufbv/bug347.smtv1.smt2
   regress0/aufbv/bug451.smtv1.smt2
+  regress0/aufbv/bug493.smtv1.smt2
   regress0/aufbv/bug509.smtv1.smt2
   regress0/aufbv/bug580.delta.smt2
   regress0/aufbv/diseqprop.01.smtv1.smt2
   regress0/aufbv/dubreva005ue.delta01.smtv1.smt2
   regress0/aufbv/fifo32bc06k08.delta01.smtv1.smt2
+  regress0/aufbv/fifo32in06k08.delta01.smtv1.smt2
   regress0/aufbv/fuzz00.smtv1.smt2
   regress0/aufbv/fuzz01.delta01.smtv1.smt2
   regress0/aufbv/fuzz01.smtv1.smt2
@@ -126,8 +140,8 @@ set(regress_0_tests
   regress0/aufbv/fuzz13.smtv1.smt2
   regress0/aufbv/fuzz14.smtv1.smt2
   regress0/aufbv/fuzz15.smtv1.smt2
-  regress0/aufbv/issue3737.smt2
   regress0/aufbv/issue3687-check-models-small.smt2
+  regress0/aufbv/issue3737.smt2
   regress0/aufbv/rewrite_bug.smtv1.smt2
   regress0/aufbv/try3_sameret_functions_fse-bfs_tac.calc_next.il.fse-bfs.delta01.smtv1.smt2
   regress0/aufbv/try5_small_difret_functions_wp_su.set_char_quoting.il.wp.delta01.smtv1.smt2
@@ -206,52 +220,67 @@ set(regress_0_tests
   regress0/bv/ackermann7.smt2
   regress0/bv/ackermann8.smt2
   regress0/bv/bool-model.smt2
-  regress0/bv/bool-to-bv-all.smt2
   regress0/bv/bool-to-bv-all-array-bool.smt2
-  regress0/bv/bool-to-bv-ite-array-bool.smt2
   regress0/bv/bool-to-bv-all-test.smt2
+  regress0/bv/bool-to-bv-all.smt2
+  regress0/bv/bool-to-bv-ite-array-bool.smt2
   regress0/bv/bool-to-bv-ite.smt2
   regress0/bv/bug260a.smtv1.smt2
   regress0/bv/bug260b.smtv1.smt2
+  regress0/bv/bug345.smtv1.smt2
   regress0/bv/bug440.smtv1.smt2
   regress0/bv/bug733.smt2
   regress0/bv/bug734.smt2
-  regress0/bv/bv-abstr-bug.smt2
-  regress0/bv/bv-abstr-bug2.smt2
-  regress0/bv/bv-int-collapse1.smt2
-  regress0/bv/bv-int-collapse2.smt2
-  regress0/bv/bv-options4.smt2
-  regress0/bv/bv-to-bool1.smtv1.smt2
-  regress0/bv/bv-to-bool2.smt2
-  regress0/bv/bv_to_int1.smt2
-  regress0/bv/bv_to_int_5230_shift_const.smt2
   regress0/bv/bv_to_int_5230_binary.smt2
   regress0/bv/bv_to_int_5230_missing_op.smt2
+  regress0/bv/bv_to_int_5230_shift_const.smt2
   regress0/bv/bv_to_int_5281.smt2
   regress0/bv/bv_to_int_bvmul2.smt2
-  regress0/bv/bv_to_int_bvuf_to_intuf.smt2
   regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2
+  regress0/bv/bv_to_int_bvuf_to_intuf.smt2
   regress0/bv/bv_to_int_elim_err.smt2
   regress0/bv/bv_to_int_zext.smt2
+  regress0/bv/bv_to_int1.smt2
+  regress0/bv/bv-abstr-bug.smt2
+  regress0/bv/bv-abstr-bug2.smt2
+  regress0/bv/bv-int-collapse1.smt2
+  regress0/bv/bv-int-collapse2.smt2
+  regress0/bv/bv-options4.smt2
+  regress0/bv/bv-to-bool1.smtv1.smt2
+  regress0/bv/bv-to-bool2.smt2
   regress0/bv/bv2nat-ground-c.smt2
   regress0/bv/bv2nat-simp-range.smt2
+  regress0/bv/bvcomp.cvc
   regress0/bv/bvmul-pow2-only.smt2
   regress0/bv/bvsimple.cvc
+  regress0/bv/bvsmod.smt2
   regress0/bv/calc2_sec2_shifter_mult_bmc15.atlas.delta01.smtv1.smt2
   regress0/bv/core/a78test0002.smtv1.smt2
   regress0/bv/core/a95test0002.smtv1.smt2
+  regress0/bv/core/bitvec0.delta01.smtv1.smt2
   regress0/bv/core/bitvec0.smtv1.smt2
+  regress0/bv/core/bitvec1.smtv1.smt2
   regress0/bv/core/bitvec2.smtv1.smt2
+  regress0/bv/core/bitvec3.smtv1.smt2
   regress0/bv/core/bitvec5.smtv1.smt2
   regress0/bv/core/bitvec7.smtv1.smt2
   regress0/bv/core/bv_eq_diamond10.smtv1.smt2
+  regress0/bv/core/bv_eq_diamond11.smtv1.smt2
+  regress0/bv/core/bv_eq_diamond12.smtv1.smt2
+  regress0/bv/core/bv_eq_diamond13.smtv1.smt2
+  regress0/bv/core/bv_eq_diamond14.smtv1.smt2
+  regress0/bv/core/bv_eq_diamond15.smtv1.smt2
+  regress0/bv/core/bv_eq_diamond16.smtv1.smt2
+  regress0/bv/core/bv_eq_diamond17.smtv1.smt2
   regress0/bv/core/concat-merge-0.smtv1.smt2
   regress0/bv/core/concat-merge-1.smtv1.smt2
   regress0/bv/core/concat-merge-2.smtv1.smt2
   regress0/bv/core/concat-merge-3.smtv1.smt2
+  regress0/bv/core/constant_core.smt2
   regress0/bv/core/equality-00.smtv1.smt2
   regress0/bv/core/equality-01.smtv1.smt2
   regress0/bv/core/equality-02.smtv1.smt2
+  regress0/bv/core/equality-04.smtv1.smt2
   regress0/bv/core/equality-05.smtv1.smt2
   regress0/bv/core/extract-concat-0.smtv1.smt2
   regress0/bv/core/extract-concat-1.smtv1.smt2
@@ -283,6 +312,7 @@ set(regress_0_tests
   regress0/bv/core/extract-whole-2.smtv1.smt2
   regress0/bv/core/extract-whole-3.smtv1.smt2
   regress0/bv/core/extract-whole-4.smtv1.smt2
+  regress0/bv/core/incremental.smtv1.smt2
   regress0/bv/core/slice-01.smtv1.smt2
   regress0/bv/core/slice-02.smtv1.smt2
   regress0/bv/core/slice-03.smtv1.smt2
@@ -306,9 +336,9 @@ set(regress_0_tests
   regress0/bv/div_mod.cvc
   regress0/bv/divtest_2_5.smt2
   regress0/bv/divtest_2_6.smt2
+  regress0/bv/eager-force-logic.smt2
   regress0/bv/eager-inc-cadical.smt2
   regress0/bv/eager-inc-cryptominisat.smt2
-  regress0/bv/eager-force-logic.smt2
   regress0/bv/fuzz01.smtv1.smt2
   regress0/bv/fuzz02.delta01.smtv1.smt2
   regress0/bv/fuzz02.smtv1.smt2
@@ -316,6 +346,7 @@ set(regress_0_tests
   regress0/bv/fuzz04.smtv1.smt2
   regress0/bv/fuzz05.smtv1.smt2
   regress0/bv/fuzz06.smtv1.smt2
+  regress0/bv/fuzz07-delta.smtv1.smt2
   regress0/bv/fuzz07.smtv1.smt2
   regress0/bv/fuzz08.smtv1.smt2
   regress0/bv/fuzz09.smtv1.smt2
@@ -324,6 +355,7 @@ set(regress_0_tests
   regress0/bv/fuzz12.smtv1.smt2
   regress0/bv/fuzz13.smtv1.smt2
   regress0/bv/fuzz14.smtv1.smt2
+  regress0/bv/fuzz15.delta01.smtv1.smt2
   regress0/bv/fuzz16.delta01.smtv1.smt2
   regress0/bv/fuzz17.delta01.smtv1.smt2
   regress0/bv/fuzz18.delta01.smtv1.smt2
@@ -373,11 +405,18 @@ set(regress_0_tests
   regress0/bv/fuzz40.delta01.smtv1.smt2
   regress0/bv/fuzz40.smtv1.smt2
   regress0/bv/fuzz41.smtv1.smt2
-  regress0/bv/issue3621.smt2
+  regress0/bv/incorrect1.delta01.smtv1.smt2
+  regress0/bv/inequality00.smt2
+  regress0/bv/inequality01.smt2
+  regress0/bv/inequality02.smt2
+  regress0/bv/inequality03.smt2
+  regress0/bv/inequality04.smt2
+  regress0/bv/inequality05.smt2
+  regress0/bv/int_to_bv_err_on_demand_1.smt2
   regress0/bv/issue-4075.smt2
   regress0/bv/issue-4076.smt2
   regress0/bv/issue-4130.smt2
-  regress0/bv/int_to_bv_err_on_demand_1.smt2
+  regress0/bv/issue3621.smt2
   regress0/bv/mul-neg-unsat.smt2
   regress0/bv/mul-negpow2.smt2
   regress0/bv/mult-pow2-negative.smt2
@@ -389,15 +428,15 @@ set(regress_0_tests
   regress0/bv/unsound1-reduced.smt2
   regress0/chained-equality.smt2
   regress0/constant-rewrite.smtv1.smt2
+  regress0/cvc-rerror-print.cvc
+  regress0/cvc3-bug15.cvc
   regress0/cvc3.userdoc.01.cvc
   regress0/cvc3.userdoc.02.cvc
   regress0/cvc3.userdoc.03.cvc
   regress0/cvc3.userdoc.04.cvc
   regress0/cvc3.userdoc.05.cvc
   regress0/cvc3.userdoc.06.cvc
-  regress0/cvc-rerror-print.cvc
   regress0/datatypes/4482-unc-simp-one.smt2
-  regress0/datatypes/Test1-tup-mp.cvc
   regress0/datatypes/boolean-equality.cvc
   regress0/datatypes/boolean-terms-datatype.cvc
   regress0/datatypes/boolean-terms-parametric-datatype-1.cvc
@@ -425,8 +464,8 @@ set(regress_0_tests
   regress0/datatypes/dt-2.6.smt2
   regress0/datatypes/dt-different-params.smt2
   regress0/datatypes/dt-match-pat-param-2.6.smt2
-  regress0/datatypes/dt-param-2.6.smt2
   regress0/datatypes/dt-param-2.6-print.smt2
+  regress0/datatypes/dt-param-2.6.smt2
   regress0/datatypes/dt-param-card4-bool-sat.smt2
   regress0/datatypes/dt-sel-2.6.smt2
   regress0/datatypes/empty_tuprec.cvc
@@ -450,6 +489,7 @@ set(regress_0_tests
   regress0/datatypes/some-boolean-tests.cvc
   regress0/datatypes/stream-singleton.smt2
   regress0/datatypes/tenum-bug.smt2
+  regress0/datatypes/Test1-tup-mp.cvc
   regress0/datatypes/tree-get-value.cvc
   regress0/datatypes/tuple-model.cvc
   regress0/datatypes/tuple-no-clash.cvc
@@ -489,7 +529,6 @@ set(regress_0_tests
   regress0/define-fun-model.smt2
   regress0/distinct.smtv1.smt2
   regress0/dump-unsat-core-full.smt2
-  regress0/simple-dump-model.smt2
   regress0/eqrange1.smt2
   regress0/eqrange2.smt2
   regress0/eqrange3.smt2
@@ -500,9 +539,8 @@ set(regress_0_tests
   regress0/expect/scrub.09.p
   regress0/flet.smtv1.smt2
   regress0/flet2.smtv1.smt2
-  regress0/fmf/Arrow_Order-smtlib.778341.smtv1.smt2
-  regress0/fmf/QEpres-uf.855035.smtv1.smt2
   regress0/fmf/array_card.smt2
+  regress0/fmf/Arrow_Order-smtlib.778341.smtv1.smt2
   regress0/fmf/bounded_sets.smt2
   regress0/fmf/bug-041417-set-options.cvc
   regress0/fmf/bug652.smt2
@@ -516,10 +554,12 @@ set(regress_0_tests
   regress0/fmf/fmf-strange-bounds-2.smt2
   regress0/fmf/forall_unit_data2.smt2
   regress0/fmf/issue3661-ccard-dec.smt2
+  regress0/fmf/issue4850-force-card.smt2
   regress0/fmf/issue4872-qf_ufc.smt2
   regress0/fmf/issue5239-uf-ss-tot.smt2
   regress0/fmf/krs-sat.smt2
   regress0/fmf/no-minimal-sat.smt2
+  regress0/fmf/QEpres-uf.855035.smtv1.smt2
   regress0/fmf/quant_real_univ.cvc
   regress0/fmf/sat-logic.smt2
   regress0/fmf/sc_bad_model_1221.smt2
@@ -530,12 +570,12 @@ set(regress_0_tests
   regress0/fp/abs-unsound2.smt2
   regress0/fp/down-cast-RNA.smt2
   regress0/fp/ext-rew-test.smt2
+  regress0/fp/issue-5524.smt2
   regress0/fp/issue3536.smt2
   regress0/fp/issue3619.smt2
   regress0/fp/issue4277-assign-func.smt2
-  regress0/fp/issue-5524.smt2
-  regress0/fp/rti_3_5_bug.smt2
   regress0/fp/rti_3_5_bug_report.smt2
+  regress0/fp/rti_3_5_bug.smt2
   regress0/fp/simple.smt2
   regress0/fp/wrong-model.smt2
   regress0/fuzz_1.smtv1.smt2
@@ -562,8 +602,8 @@ set(regress_0_tests
   regress0/ho/fun-subtyping.smt2
   regress0/ho/ho-exponential-model.smt2
   regress0/ho/ho-match-fun-suffix.smt2
-  regress0/ho/ho-matching-enum.smt2
   regress0/ho/ho-matching-enum-2.smt2
+  regress0/ho/ho-matching-enum.smt2
   regress0/ho/ho-matching-nested-app.smt2
   regress0/ho/ho-std-fmf.smt2
   regress0/ho/hoa0008.smt2
@@ -580,6 +620,7 @@ set(regress_0_tests
   regress0/ho/trans.smt2
   regress0/hung10_itesdk_output1.smt2
   regress0/hung13sdk_output1.smt2
+  regress0/incorrect1.smtv1.smt2
   regress0/ineq_basic.smtv1.smt2
   regress0/ineq_slack.smtv1.smt2
   regress0/issue1063-overloading-dt-cons.smt2
@@ -597,12 +638,14 @@ set(regress_0_tests
   regress0/issue5540-2-dump-model.smt2
   regress0/issue5540-model-decls.smt2
   regress0/issue5550-num-children.smt2
+  regress0/ite_arith.smt2
+  regress0/ite_real_int_type.smtv1.smt2
+  regress0/ite_real_valid.smtv1.smt2
   regress0/ite.cvc
+  regress0/ite.smt2
   regress0/ite2.smt2
   regress0/ite3.smt2
   regress0/ite4.smt2
-  regress0/ite_real_int_type.smtv1.smt2
-  regress0/ite_real_valid.smtv1.smt2
   regress0/lang_opts_2_5.smt2
   regress0/lang_opts_2_6_1.smt2
   regress0/lemmas/clocksynchro_5clocks.main_invar.base.model.smtv1.smt2
@@ -621,6 +664,7 @@ set(regress_0_tests
   regress0/models-print-1.smt2
   regress0/models-print-2.smt2
   regress0/named-expr-use.smt2
+  regress0/nl/all-logic.smt2
   regress0/nl/coeff-sat.smt2
   regress0/nl/ext-rew-aggr-test.smt2
   regress0/nl/iand-no-init.smt2
@@ -658,8 +702,8 @@ set(regress_0_tests
   regress0/nl/subs0-unsat-confirm.smt2
   regress0/nl/very-easy-sat.smt2
   regress0/nl/very-simple-unsat.smt2
-  regress0/options/invalid_dump.smt2
   regress0/opt-abd-no-use.smt2
+  regress0/options/invalid_dump.smt2
   regress0/parallel-let.smt2
   regress0/parser/as.smt2
   regress0/parser/bv_arity_smt2.6.smt2
@@ -754,10 +798,10 @@ set(regress_0_tests
   regress0/push-pop/test.01.cvc
   regress0/push-pop/tiny_bug.smt2
   regress0/push-pop/units.cvc
-  regress0/quantifiers/ARI176e1.smt2
   regress0/quantifiers/agg-rew-test-cf.smt2
   regress0/quantifiers/agg-rew-test.smt2
   regress0/quantifiers/ari056.smt2
+  regress0/quantifiers/ARI176e1.smt2
   regress0/quantifiers/bug269.smt2
   regress0/quantifiers/bug290.smt2
   regress0/quantifiers/bug291.smt2
@@ -799,6 +843,7 @@ set(regress_0_tests
   regress0/quantifiers/pure_dt_cbqi.smt2
   regress0/quantifiers/qarray-sel-over-store.smt2
   regress0/quantifiers/qbv-inequality2.smt2
+  regress0/quantifiers/qbv-multi-lit-uge.smt2
   regress0/quantifiers/qbv-simp.smt2
   regress0/quantifiers/qbv-test-invert-bvadd-neq.smt2
   regress0/quantifiers/qbv-test-invert-bvand-neq.smt2
@@ -810,11 +855,14 @@ set(regress_0_tests
   regress0/quantifiers/qbv-test-invert-bvlshr-1-neq.smt2
   regress0/quantifiers/qbv-test-invert-bvor-neq.smt2
   regress0/quantifiers/qbv-test-invert-bvor.smt2
+  regress0/quantifiers/qbv-test-invert-bvshl-0-neq.smt2
   regress0/quantifiers/qbv-test-invert-bvshl-0.smt2
   regress0/quantifiers/qbv-test-invert-bvult-1.smt2
   regress0/quantifiers/qbv-test-invert-bvxor-neq.smt2
   regress0/quantifiers/qbv-test-invert-bvxor.smt2
+  regress0/quantifiers/qbv-test-invert-concat-0-neq.smt2
   regress0/quantifiers/qbv-test-invert-concat-0.smt2
+  regress0/quantifiers/qbv-test-invert-concat-1-neq.smt2
   regress0/quantifiers/qbv-test-invert-concat-1.smt2
   regress0/quantifiers/qbv-test-invert-sign-extend.smt2
   regress0/quantifiers/qcf-rel-dom-opt.smt2
@@ -839,30 +887,31 @@ set(regress_0_tests
   regress0/rels/rel_complex_0.cvc
   regress0/rels/rel_complex_1.cvc
   regress0/rels/rel_conflict_0.cvc
-  regress0/rels/rel_join_0.cvc
   regress0/rels/rel_join_0_1.cvc
-  regress0/rels/rel_join_1.cvc
+  regress0/rels/rel_join_0.cvc
   regress0/rels/rel_join_1_1.cvc
-  regress0/rels/rel_join_2.cvc
+  regress0/rels/rel_join_1.cvc
   regress0/rels/rel_join_2_1.cvc
-  regress0/rels/rel_join_3.cvc
+  regress0/rels/rel_join_2.cvc
   regress0/rels/rel_join_3_1.cvc
+  regress0/rels/rel_join_3.cvc
   regress0/rels/rel_join_4.cvc
   regress0/rels/rel_join_5.cvc
   regress0/rels/rel_join_6.cvc
   regress0/rels/rel_join_7.cvc
-  regress0/rels/rel_product_0.cvc
   regress0/rels/rel_product_0_1.cvc
-  regress0/rels/rel_product_1.cvc
+  regress0/rels/rel_product_0.cvc
   regress0/rels/rel_product_1_1.cvc
-  regress0/rels/rel_symbolic_1.cvc
+  regress0/rels/rel_product_1.cvc
   regress0/rels/rel_symbolic_1_1.cvc
+  regress0/rels/rel_symbolic_1.cvc
   regress0/rels/rel_symbolic_2_1.cvc
   regress0/rels/rel_symbolic_3_1.cvc
   regress0/rels/rel_tc_11.cvc
   regress0/rels/rel_tc_2_1.cvc
-  regress0/rels/rel_tc_3.cvc
   regress0/rels/rel_tc_3_1.cvc
+  regress0/rels/rel_tc_3.cvc
+  regress0/rels/rel_tc_7.cvc
   regress0/rels/rel_tc_8.cvc
   regress0/rels/rel_tp_3_1.cvc
   regress0/rels/rel_tp_join_0.cvc
@@ -874,8 +923,8 @@ set(regress_0_tests
   regress0/rels/rel_tp_join_pro_0.cvc
   regress0/rels/rel_tp_join_var_0.cvc
   regress0/rels/rel_transpose_0.cvc
-  regress0/rels/rel_transpose_1.cvc
   regress0/rels/rel_transpose_1_1.cvc
+  regress0/rels/rel_transpose_1.cvc
   regress0/rels/rel_transpose_3.cvc
   regress0/rels/rel_transpose_4.cvc
   regress0/rels/rel_transpose_5.cvc
@@ -899,8 +948,8 @@ set(regress_0_tests
   regress0/sep/skolem_emp.smt2
   regress0/sep/trees-1.smt2
   regress0/sep/wand-crash.smt2
-  regress0/seq/intseq.smt2
   regress0/seq/intseq_dt.smt2
+  regress0/seq/intseq.smt2
   regress0/seq/issue4370-bool-terms.smt2
   regress0/seq/issue5543-unit-cmv.smt2
   regress0/seq/seq-2var.smt2
@@ -912,10 +961,10 @@ set(regress_0_tests
   regress0/seq/seq-ex5.smt2
   regress0/seq/seq-expand-defs.smt2
   regress0/seq/seq-nemp.smt2
-  regress0/seq/seq-nth.smt2
-  regress0/seq/seq-nth-uf.smt2
   regress0/seq/seq-nth-uf-z.smt2
+  regress0/seq/seq-nth-uf.smt2
   regress0/seq/seq-nth-undef-unsat.smt2
+  regress0/seq/seq-nth.smt2
   regress0/seq/seq-rewrites.smt2
   regress0/seq/seq-types.smt2
   regress0/sets/abt-min.smt2
@@ -925,10 +974,10 @@ set(regress_0_tests
   regress0/sets/card-3sets.cvc
   regress0/sets/card.smt2
   regress0/sets/card3-ground.smt2
+  regress0/sets/comp-qf-error.smt2
   regress0/sets/complement.cvc
   regress0/sets/complement2.cvc
   regress0/sets/complement3.cvc
-  regress0/sets/comp-qf-error.smt2
   regress0/sets/cvc-sample.cvc
   regress0/sets/dt-simp-mem.smt2
   regress0/sets/emptyset.smt2
@@ -951,14 +1000,18 @@ set(regress_0_tests
   regress0/sets/nonvar-univ.smt2
   regress0/sets/pre-proc-univ.smt2
   regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2
+  regress0/sets/setel-eq.smt2
   regress0/sets/sets-equal.smt2
   regress0/sets/sets-extr.smt2
   regress0/sets/sets-inter.smt2
+  regress0/sets/sets-new.smt2
   regress0/sets/sets-of-sets-subtypes.smt2
   regress0/sets/sets-poly-int-real.smt2
   regress0/sets/sets-poly-nonint.smt2
   regress0/sets/sets-sample.smt2
   regress0/sets/sets-sharing.smt2
+  regress0/sets/sets-testlemma-ints.smt2
+  regress0/sets/sets-testlemma-reals.smt2
   regress0/sets/sets-testlemma.smt2
   regress0/sets/sets-union.smt2
   regress0/sets/sharing-simp.smt2
@@ -968,12 +1021,13 @@ set(regress_0_tests
   regress0/sets/union-1b.smt2
   regress0/sets/union-2.smt2
   regress0/sets/univset-simp.smt2
-  regress0/simple-lra.smtv1.smt2
+  regress0/simple-dump-model.smt2
   regress0/simple-lra.smt2
-  regress0/simple-rdl.smtv1.smt2
+  regress0/simple-lra.smtv1.smt2
   regress0/simple-rdl.smt2
-  regress0/simple-uf.smtv1.smt2
+  regress0/simple-rdl.smtv1.smt2
   regress0/simple-uf.smt2
+  regress0/simple-uf.smtv1.smt2
   regress0/simple.cvc
   regress0/simple.smtv1.smt2
   regress0/simple2.smtv1.smt2
@@ -990,14 +1044,13 @@ set(regress_0_tests
   regress0/smtlib/issue4552.smt2
   regress0/smtlib/issue4866.smt2
   regress0/smtlib/reason-unknown.smt2
-  regress0/smtlib/reset.smt2
+  regress0/smtlib/reset-assertions-global.smt2
   regress0/smtlib/reset-assertions1.smt2
   regress0/smtlib/reset-assertions2.smt2
-  regress0/smtlib/reset-assertions-global.smt2
   regress0/smtlib/reset-force-logic.smt2
   regress0/smtlib/reset-set-logic.smt2
+  regress0/smtlib/reset.smt2
   regress0/smtlib/set-info-status.smt2
-  regress0/strings/bidir_star.smt2
   regress0/strings/bug001.smt2
   regress0/strings/bug002.smt2
   regress0/strings/bug612.smt2
@@ -1007,8 +1060,8 @@ set(regress_0_tests
   regress0/strings/code-perf.smt2
   regress0/strings/code-sat-neg-one.smt2
   regress0/strings/complement-simple.smt2
-  regress0/strings/escchar.smt2
   regress0/strings/escchar_25.smt2
+  regress0/strings/escchar.smt2
   regress0/strings/from_code.smt2
   regress0/strings/gen-esc-seq.smt2
   regress0/strings/hconst-092618.smt2
@@ -1036,34 +1089,34 @@ set(regress_0_tests
   regress0/strings/large-model.smt2
   regress0/strings/leadingzero001.smt2
   regress0/strings/leq.smt2
-  regress0/strings/loop001.smt2
   regress0/strings/loop-wrong-sem.smt2
-  regress0/strings/model001.smt2
+  regress0/strings/loop001.smt2
   regress0/strings/model-code-point.smt2
   regress0/strings/model-friendly.smt2
+  regress0/strings/model001.smt2
   regress0/strings/ncontrib-rewrites.smt2
   regress0/strings/norn-31.smt2
   regress0/strings/norn-simp-rew.smt2
   regress0/strings/parser-syms.cvc
   regress0/strings/quad-028-2-2-unsat.smt2
-  regress0/strings/re.all.smt2
+  regress0/strings/re_diff.smt2
   regress0/strings/re-in-rewrite.smt2
   regress0/strings/re-syntax.smt2
-  regress0/strings/re_diff.smt2
-  regress0/strings/regexp-native-simple.cvc
-  regress0/strings/regexp_inclusion.smt2
+  regress0/strings/re.all.smt2
   regress0/strings/regexp_inclusion_reduction.smt2
+  regress0/strings/regexp_inclusion.smt2
+  regress0/strings/regexp-native-simple.cvc
   regress0/strings/repl-rewrites2.smt2
   regress0/strings/replace-const.smt2
   regress0/strings/replaceall-eval.smt2
   regress0/strings/rewrites-re-concat.smt2
   regress0/strings/rewrites-v2.smt2
   regress0/strings/std2.6.1.smt2
+  regress0/strings/str_unsound_ext_rew_eq.smt2
+  regress0/strings/str-rev-simple.smt2
   regress0/strings/str003.smt2
   regress0/strings/str004.smt2
   regress0/strings/str005.smt2
-  regress0/strings/str_unsound_ext_rew_eq.smt2
-  regress0/strings/str-rev-simple.smt2
   regress0/strings/strings-charat.cvc
   regress0/strings/strings-native-simple.cvc
   regress0/strings/strip-endpoint-itos.smt2
@@ -1074,18 +1127,18 @@ set(regress_0_tests
   regress0/strings/unicode-esc.smt2
   regress0/strings/unsound-0908.smt2
   regress0/strings/unsound-repl-rewrite.smt2
-  regress0/sygus/General_plus10.sy
   regress0/sygus/aig-si.sy
   regress0/sygus/array-grammar-select.sy
   regress0/sygus/array-grammar-store.sy
   regress0/sygus/c100.sy
   regress0/sygus/ccp16.lus.sy
-  regress0/sygus/cegqi-si-string-triv.sy
   regress0/sygus/cegqi-si-string-triv-2fun.sy
+  regress0/sygus/cegqi-si-string-triv.sy
   regress0/sygus/check-generic-red.sy
   regress0/sygus/const-var-test.sy
   regress0/sygus/dt-no-syntax.sy
   regress0/sygus/dt-sel-parse1.sy
+  regress0/sygus/General_plus10.sy
   regress0/sygus/hd-05-d1-prog-nogrammar.sy
   regress0/sygus/inv-different-var-order.sy
   regress0/sygus/issue3356-syg-inf-usort.smt2
@@ -1106,29 +1159,30 @@ set(regress_0_tests
   regress0/sygus/print-debug.sy
   regress0/sygus/print-define-fun.sy
   regress0/sygus/real-si-all.sy
+  regress0/sygus/strings-unconstrained.sy
   regress0/sygus/sygus-no-wf.sy
   regress0/sygus/sygus-uf.sy
-  regress0/sygus/strings-unconstrained.sy
   regress0/sygus/uminus_one.sy
   regress0/sygus/univ_3-long-repeat-conflict.sy
+  regress0/symmetric.smtv1.smt2
   regress0/test11.cvc
   regress0/test9.cvc
   regress0/tptp/ARI086=1.p
   regress0/tptp/DAT001=1.p
+  regress0/tptp/is_rat_simple.p
   regress0/tptp/KRS018+1.p
   regress0/tptp/KRS063+1.p
   regress0/tptp/MGT019+2.p
   regress0/tptp/MGT041-2.p
   regress0/tptp/PUZ131_1.p
-  regress0/tptp/SYN000+1.p
-  regress0/tptp/SYN000+2.p
+  regress0/tptp/SYN000_1.p
+  regress0/tptp/SYN000_2.p
   regress0/tptp/SYN000-1.p
   regress0/tptp/SYN000-2.p
+  regress0/tptp/SYN000+1.p
+  regress0/tptp/SYN000+2.p
   regress0/tptp/SYN000=2.p
-  regress0/tptp/SYN000_1.p
-  regress0/tptp/SYN000_2.p
   regress0/tptp/SYN075-1.p
-  regress0/tptp/is_rat_simple.p
   regress0/tptp/tff0-arith.p
   regress0/tptp/tff0.p
   regress0/tptp/tptp_parser.p
@@ -1141,15 +1195,13 @@ set(regress_0_tests
   regress0/tptp/tptp_parser7.p
   regress0/tptp/tptp_parser8.p
   regress0/tptp/tptp_parser9.p
-  regress0/uf/NEQ016_size5_reduced2a.smtv1.smt2
-  regress0/uf/NEQ016_size5_reduced2b.smtv1.smt2
   regress0/uf/bool-pred-nested.smt2
   regress0/uf/ccredesign-fuzz.smtv1.smt2
+  regress0/uf/cnf_abc.smt2
   regress0/uf/cnf-and-neg.smt2
   regress0/uf/cnf-iff-base.smt2
   regress0/uf/cnf-iff.smt2
   regress0/uf/cnf-ite.smt2
-  regress0/uf/cnf_abc.smt2
   regress0/uf/dead_dnd002.smtv1.smt2
   regress0/uf/eq_diamond1.smtv1.smt2
   regress0/uf/eq_diamond14.reduced.smtv1.smt2
@@ -1170,7 +1222,10 @@ set(regress_0_tests
   regress0/uf/iso_brn001.smtv1.smt2
   regress0/uf/issue2947.smt2
   regress0/uf/issue4446.smt2
+  regress0/uf/NEQ016_size5_reduced2a.smtv1.smt2
+  regress0/uf/NEQ016_size5_reduced2b.smtv1.smt2
   regress0/uf/pred.smtv1.smt2
+  regress0/uf/SEQ032_size2.smtv1.smt2
   regress0/uf/simple.01.cvc
   regress0/uf/simple.02.cvc
   regress0/uf/simple.03.cvc
@@ -1180,6 +1235,12 @@ set(regress_0_tests
   regress0/uflia/check02.smt2
   regress0/uflia/check03.smt2
   regress0/uflia/check04.smt2
+  regress0/uflia/diseqprop.01.smtv1.smt2
+  regress0/uflia/diseqprop.02.smtv1.smt2
+  regress0/uflia/diseqprop.03.smtv1.smt2
+  regress0/uflia/diseqprop.04.smtv1.smt2
+  regress0/uflia/diseqprop.05.smtv1.smt2
+  regress0/uflia/diseqprop.06.smtv1.smt2
   regress0/uflia/error0.delta01.smtv1.smt2
   regress0/uflia/error1.smtv1.smt2
   regress0/uflia/error30.smtv1.smt2
@@ -1189,6 +1250,7 @@ set(regress_0_tests
   regress0/uflia/xs-09-16-3-4-1-5.delta02.smtv1.smt2
   regress0/uflia/xs-09-16-3-4-1-5.delta03.smtv1.smt2
   regress0/uflia/xs-09-16-3-4-1-5.delta04.smtv1.smt2
+  regress0/uflia/xs-09-16-3-4-1-5.delta05.smtv1.smt2
   regress0/uflra/bug293.cvc
   regress0/uflra/bug449.smtv1.smt2
   regress0/uflra/constants0.smtv1.smt2
@@ -1202,7 +1264,9 @@ set(regress_0_tests
   regress0/uflra/pb_real_10_0100_10_16.smtv1.smt2
   regress0/uflra/pb_real_10_0100_10_19.smtv1.smt2
   regress0/uflra/pb_real_10_0200_10_22.smtv1.smt2
+  regress0/uflra/pb_real_10_0200_10_25.smtv1.smt2
   regress0/uflra/pb_real_10_0200_10_26.smtv1.smt2
+  regress0/uflra/pb_real_10_0200_10_27.smtv1.smt2
   regress0/uflra/pb_real_10_0200_10_29.smtv1.smt2
   regress0/uflra/simple.01.cvc
   regress0/uflra/simple.02.cvc
@@ -1210,15 +1274,18 @@ set(regress_0_tests
   regress0/uflra/simple.04.cvc
   regress0/unconstrained/4481.smt2
   regress0/unconstrained/arith.smt2
+  regress0/unconstrained/arith2.smt2
   regress0/unconstrained/arith3.smt2
   regress0/unconstrained/arith4.smt2
   regress0/unconstrained/arith5.smt2
   regress0/unconstrained/arith6.smt2
+  regress0/unconstrained/arith7.smt2
   regress0/unconstrained/array1.smt2
   regress0/unconstrained/bvbool.smt2
   regress0/unconstrained/bvbool2.smt2
   regress0/unconstrained/bvbool3.smt2
   regress0/unconstrained/bvcmp.smt2
+  regress0/unconstrained/bvconcat.smt2
   regress0/unconstrained/bvconcat2.smt2
   regress0/unconstrained/bvext.smt2
   regress0/unconstrained/bvite.smt2
@@ -1236,6 +1303,7 @@ set(regress_0_tests
   regress0/unconstrained/bvslt3.smt2
   regress0/unconstrained/bvslt4.smt2
   regress0/unconstrained/bvslt5.smt2
+  regress0/unconstrained/bvdiv.smt2
   regress0/unconstrained/bvule.smt2
   regress0/unconstrained/bvule2.smt2
   regress0/unconstrained/bvule3.smt2
@@ -1283,6 +1351,7 @@ set(regress_0_tests
 
 set(regress_1_tests
   regress1/abduct-dt.smt2
+  regress1/arith/arith-brab-test.smt2
   regress1/arith/arith-int-004.cvc
   regress1/arith/arith-int-011.cvc
   regress1/arith/arith-int-012.cvc
@@ -1314,6 +1383,7 @@ set(regress_1_tests
   regress1/arith/pbrewrites-test.smt2
   regress1/arith/problem__003.smt2
   regress1/arrayinuf_error.smt2
+  regress1/aufbv/bug348.smtv1.smt2
   regress1/aufbv/bug580.smt2
   regress1/aufbv/fuzz10.smtv1.smt2
   regress1/auflia/bug330.smt2
@@ -1329,10 +1399,12 @@ set(regress_1_tests
   regress1/bug521.smt2
   regress1/bug543.smt2
   regress1/bug567.smt2
+  regress1/bug590.smt2
   regress1/bug593.smt2
   regress1/bug681.smt2
   regress1/bug694-Unapply1.scala-0.smt2
   regress1/bug800.smt2
+  regress1/bv/bench_38.delta.smt2
   regress1/bv/bug787.smt2
   regress1/bv/bug_extract_mult_leading_bit.smt2
   regress1/bv/bv-int-collapse2-sat.smt2
@@ -1345,6 +1417,7 @@ set(regress_1_tests
   regress1/bv/divtest.smt2
   regress1/bv/fuzz34.smtv1.smt2
   regress1/bv/fuzz38.smtv1.smt2
+  regress1/bv/incorrect1.smtv1.smt2
   regress1/bv/issue3654.smt2
   regress1/bv/issue3776.smt2
   regress1/bv/test-bv-abstraction.smt2
@@ -1421,12 +1494,16 @@ set(regress_1_tests
   regress1/fmf/sort-inf-int.smt2
   regress1/fmf/with-ind-104-core.smt2
   regress1/gensys_brn001.smt2
+  regress1/ho/bug_freevar_PHI004^4-delta.smt2
+  regress1/ho/bug_freeVar_BDD_General_data_270.p
+  regress1/ho/bound_var_bug.p
   regress1/ho/fta0328.lfho.p
   regress1/ho/issue3136-fconst-bool-bool.smt2
   regress1/ho/issue4065-no-rep.smt2
   regress1/ho/issue4092-sinf.smt2
   regress1/ho/issue4134-sinf.smt2
   regress1/ho/nested_lambdas-AGT034^2.smt2
+  regress1/ho/nested_lambdas-sat-SYO056^1-delta.smt2
   regress1/ho/NUM638^1.smt2
   regress1/ho/NUM925^1.p
   regress1/ho/soundness_fmf_SYO362^5-delta.p
@@ -1465,11 +1542,13 @@ set(regress_1_tests
   regress1/nl/factor_agg_s.smt2
   regress1/nl/iand-native-1.smt2
   regress1/nl/iand-native-2.smt2
+  regress1/nl/iand-native-granularities.smt2
   regress1/nl/issue3300-approx-sqrt-witness.smt2
   regress1/nl/issue3441.smt2
   regress1/nl/issue3617.smt2
   regress1/nl/issue3647.smt2
   regress1/nl/issue3656.smt2
+  regress1/nl/issue3803-nl-check-model.smt2
   regress1/nl/issue3955-ee-double-notify.smt2
   regress1/nl/issue5372-2-no-m-presolve.smt2
   regress1/nl/metitarski-1025.smt2
@@ -1632,6 +1711,7 @@ set(regress_1_tests
   regress1/quantifiers/issue4243-prereg-inc.smt2
   regress1/quantifiers/issue4290-cegqi-r.smt2
   regress1/quantifiers/issue4433-nqe.smt2
+  regress1/quantifiers/issue4476-ext-rew.smt2
   regress1/quantifiers/issue4620-erq-witness-unsound.smt2
   regress1/quantifiers/issue4685-wrewrite.smt2
   regress1/quantifiers/issue4849-nqe.smt2
@@ -1654,6 +1734,7 @@ set(regress_1_tests
   regress1/quantifiers/mix-coeff.smt2
   regress1/quantifiers/mutualrec2.cvc
   regress1/quantifiers/nested9_true-unreach-call.i_575.smt2
+  regress1/quantifiers/nl-pow-trick.smt2
   regress1/quantifiers/nra-interleave-inst.smt2
   regress1/quantifiers/opisavailable-12.smt2
   regress1/quantifiers/parametric-lists.smt2
@@ -1730,6 +1811,7 @@ set(regress_1_tests
   regress1/rels/rel_pressure_0.cvc
   regress1/rels/rel_tc_10_1.cvc
   regress1/rels/rel_tc_4.cvc
+  regress1/rels/rel_tc_4_1.cvc
   regress1/rels/rel_tc_5_1.cvc
   regress1/rels/rel_tc_6.cvc
   regress1/rels/rel_tc_9_1.cvc
@@ -1742,7 +1824,6 @@ set(regress_1_tests
   regress1/rr-verify/bv-term.sy
   regress1/rr-verify/fp-arith.sy
   regress1/rr-verify/fp-bool.sy
-  regress1/rr-verify/regex.sy
   regress1/rr-verify/string-term.sy
   regress1/sep/chain-int.smt2
   regress1/sep/crash1220.smt2
@@ -1980,7 +2061,6 @@ set(regress_1_tests
   regress1/sygus/bvudiv-by-2.sy
   regress1/sygus/cegar1.sy
   regress1/sygus/cegis-unif-inv-eq-fair.sy
-  regress1/sygus/cegisunif-depth1.sy
   regress1/sygus/cggmp.sy
   regress1/sygus/clock-inc-tuple.sy
   regress1/sygus/coeff-solve-inv.sy
@@ -2019,7 +2099,6 @@ set(regress_1_tests
   regress1/sygus/inv-missed-sol-true.sy
   regress1/sygus/inv-unused.sy
   regress1/sygus/interpol1.smt2
-  regress1/sygus/interpol2.smt2
   regress1/sygus/interpol3.smt2
   regress1/sygus/interpol_arr1.smt2
   regress1/sygus/interpol_arr2.smt2
@@ -2037,6 +2116,7 @@ set(regress_1_tests
   regress1/sygus/issue3461.sy
   regress1/sygus/issue3514.smt2
   regress1/sygus/issue3507.smt2
+  regress1/sygus/issue3580.sy
   regress1/sygus/issue3633.smt2
   regress1/sygus/issue3634.smt2
   regress1/sygus/issue3635.smt2
@@ -2113,7 +2193,6 @@ set(regress_1_tests
   regress1/sygus/twolets1.sy
   regress1/sygus/twolets2-orig.sy
   regress1/sygus/uf-abduct.smt2
-  regress1/sygus/unbdd_inv_gen_ex7.sy
   regress1/sygus/unbdd_inv_gen_winf1.sy
   regress1/sygus/univ_2-long-repeat.sy
   regress1/sygus/yoni-true-sol.smt2
@@ -2150,14 +2229,16 @@ set(regress_2_tests
   regress2/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2
   regress2/GEO123+1.minimized.smt2
   regress2/arith/abz5_1400.smtv1.smt2
-  regress2/arith/lpsat-goal-9.smt2
+  regress2/arith/arith-int-098.cvc
   regress2/arith/pursuit-safety-11.smtv1.smt2
   regress2/arith/pursuit-safety-12.smtv1.smt2
+  regress2/arith/real2int-test.smt2
   regress2/arith/sc-7.base.cvc.smtv1.smt2
   regress2/arith/uart-8.base.cvc.smtv1.smt2
-  regress2/auflia-fuzz06.smtv1.smt2
   regress2/bug136.smtv1.smt2
   regress2/bug148.smtv1.smt2
+  regress2/bug349.smtv1.smt2
+  regress2/bug374.smtv1.smt2
   regress2/bug394.smt2
   regress2/bug674.smt2
   regress2/bug765.smt2
@@ -2190,16 +2271,19 @@ set(regress_2_tests
   regress2/ho/SYO362^5.p
   regress2/hole7.cvc
   regress2/hole8.cvc
+  regress2/hole10.cvc
   regress2/instance_1444.smtv1.smt2
   regress2/issue3687-check-models.smt2
   regress2/issue4707-bv-to-bool-large.smt2
   regress2/javafe.ast.StandardPrettyPrint.319_no_forall.smt2
   regress2/javafe.ast.WhileStmt.447_no_forall.smt2
+  regress2/nl/nt-lemmas-bad.smt2
   regress2/ooo.rf6.smt2
   regress2/ooo.tag10.smt2
   regress2/piVC_5581bd.smt2
   regress2/push-pop/DRAGON_4_e2_2799_e3_1915.lus.ic3.1.min.smt2
   regress2/quantifiers/AdditiveMethods_AdditiveMethods..ctor.smt2
+  regress2/quantifiers/ForElimination-scala-9.smt2
   regress2/quantifiers/gn-wrong-091018.smt2
   regress2/quantifiers/javafe.ast.ArrayInit.35.smt2
   regress2/quantifiers/javafe.ast.StandardPrettyPrint.319.smt2
@@ -2208,9 +2292,10 @@ set(regress_2_tests
   regress2/quantifiers/javafe.tc.FlowInsensitiveChecks.682.smt2
   regress2/quantifiers/net-policy-no-time.smt2
   regress2/quantifiers/nunchaku2309663.nun.min.smt2
-  regress2/quantifiers/specsharp-WindowsCard.15.RTE.Terminate_System.Int32.smt2
+  regress2/quantifiers/small-bug1-fixpoint-3.smt2
   regress2/quantifiers/syn874-1.smt2
   regress2/simplify.javafe.ast.ArrayInit.35_without_quantification2.smt2
+  regress2/strings/bidir_star.smt2
   regress2/strings/cmi-split-cm-fail.smt2
   regress2/strings/cmu-dis-0707-3.smt2
   regress2/strings/cmu-disagree-0707-dd.smt2
@@ -2229,7 +2314,6 @@ set(regress_2_tests
   regress2/strings/small-1.smt2
   regress2/strings/update-ex3.smt2
   regress2/strings/update-ex4-seq.smt2
-  regress2/sygus/DRAGON_1.lus.sy
   regress2/sygus/MPwL_d1s3.sy
   regress2/sygus/array_sum_dd.sy
   regress2/sygus/cegisunif-depth1-bv.sy
@@ -2242,17 +2326,14 @@ set(regress_2_tests
   regress2/sygus/min_IC_1.sy
   regress2/sygus/mpg_guard1-dd.sy
   regress2/sygus/multi-udiv.sy
-  regress2/sygus/nia-max-square.sy
   regress2/sygus/no-syntax-test-no-si.sy
   regress2/sygus/pbe_bvurem.sy
-  regress2/sygus/policyM.sy
   regress2/sygus/process-10-vars-2fun.sy
   regress2/sygus/process-arg-invariance.sy
   regress2/sygus/real-grammar-neg.sy
   regress2/sygus/sets-fun-test.sy
   regress2/sygus/strings-no-syntax-len.sy
   regress2/sygus/three.sy
-  regress2/sygus/vcb.sy
   regress2/typed_v1l50016-simp.cvc
   regress2/uflia-error0.smt2
   regress2/xs-09-16-3-4-1-5.smtv1.smt2
@@ -2262,179 +2343,111 @@ set(regress_2_tests
 # Regression level 3 tests
 
 set(regress_3_tests
-  regress3/strings/norn-dis-0707-3.smt2
-  regress3/strings/replace_re_all.smt2
-  regress3/quantifiers/sygus-inst-ufbv-sdlx-fixpoint-5.smt2
-  regress3/friedman_n4_i5.smtv1.smt2
   regress3/arith_prp-13-24.smt2
+  regress3/aufbv-wchains010ue.smtv1.smt2
+  regress3/auflia-fuzz06.smtv1.smt2
   regress3/bmc-ibm-1.smtv1.smt2
   regress3/bmc-ibm-2.smtv1.smt2
   regress3/bmc-ibm-5.smtv1.smt2
   regress3/bmc-ibm-7.smtv1.smt2
+  regress3/bug2.smtv1.smt2
   regress3/bv_to_int_and_or.smt2
   regress3/bv_to_int_bench_9839.smt2.minimized.smt2
   regress3/bv_to_int_check_bvsge_bvashr0_4bit.smt2.minimized.smt2
   regress3/bv_to_int_check_bvsgt_bvlshr0_4bit.smt2.minimized.smt2
   regress3/bv_to_int_check_ne_bvlshr0_4bit.smt2.minimized.smt2
+  regress3/bv_to_int_input_mouser_detect.c.smt2.minimized.smt2
   regress3/bv_to_int_quant1.smt2
   regress3/bv_to_int_quant2.smt2
-  regress3/bv_to_int_input_mouser_detect.c.smt2.minimized.smt2
+  regress3/bv-core-ext_con_004_001_1024.smtv1.smt2
+  regress3/bv-fuzz15.smtv1.smt2
+  regress3/bv-fuzz16.smtv1.smt2
+  regress3/bv-fuzz17.smtv1.smt2
+  regress3/cegisunif-depth1.sy
+  regress3/decision-uflia-xs-09-16-3-4-1-5.smtv1.smt2
+  regress3/decision-wchains010ue.smtv1.smt2
+  regress3/DRAGON_1.lus.sy
   regress3/eq_diamond14.smtv1.smt2
+  regress3/friedman_n4_i5.smtv1.smt2
   regress3/friedman_n6_i4.smtv1.smt2
   regress3/hole9.cvc
   regress3/incorrect1.smtv1.smt2
-  regress3/issue2429.smt2
+  regress3/interpol2.smt2
+  regress3/inv_gen_n_c11.sy
   regress3/issue4170.smt2
   regress3/issue4714.smt2
-  regress3/pp-regfile.smtv1.smt2
+  regress3/lpsat-goal-9.smt2
+  regress3/nia-max-square.sy
+  regress3/PEQ018_size4.smtv1.smt2
+  regress3/policyM.sy
+  regress3/quantifiers/sygus-inst-ufbv-sdlx-fixpoint-5.smt2
   regress3/qwh.35.405.shuffled-as.sat03-1651.smtv1.smt2
+  regress3/regex-rrv.sy
   regress3/siegel-nl-bases.smt2
   regress3/sixfuncs.sy
+  regress3/specsharp-WindowsCard.15.RTE.Terminate_System.Int32.smt2
   regress3/strings-any-term.sy
   regress3/strings/extf_d_perf.smt2
-  regress3/strings/unsat-circ-reduce.smt2
+  regress3/strings/norn-dis-0707-3.smt2
+  regress3/strings/replace_re_all.smt2
+  regress3/unbdd_inv_gen_ex7.sy
+  regress3/unifpi-solve-car_1.lus.sy
+  regress3/vcb.sy
 )
 
 #-----------------------------------------------------------------------------#
 # Regression level 4 tests
 
 set(regress_4_tests
-  regress4/C880mul.miter.shuffled-as.sat03-348.smtv1.smt2
-  regress4/NEQ016_size5.smtv1.smt2
   regress4/bug143.smtv1.smt2
+  regress4/bug337.smt2
+  regress4/bug396.smt2
+  regress4/C880mul.miter.shuffled-as.sat03-348.smtv1.smt2
   regress4/comb2.shuffled-as.sat03-420.smtv1.smt2
-  regress4/hole10.cvc
+  regress4/fischer3-mutex-16.smtv1.smt2
   regress4/instance_1151.smtv1.smt2
+  regress4/issue2429.smt2
+  regress4/miplib-pp08a-3000.smt2
+  regress4/miplib-pp08a-3000.smtv1.smt2
+  regress4/NEQ016_size5.smtv1.smt2
+  regress4/pp-regfile.smtv1.smt2
+  regress4/sets-card-neg-mem-union-2.smt2
+  regress4/unsat-circ-reduce.smt2
+  regress4/xs-11-20-5-2-5-3.smt2
+  regress4/xs-11-20-5-2-5-3.smtv1.smt2
 )
 
 #-----------------------------------------------------------------------------#
 # Disabled tests, will not be run.
 
 set(regression_disabled_tests
-  regress0/arith/bug549.cvc
-  regress0/arith/incorrect1.smtv1.smt2
-  regress0/arith/integers/arith-int-014.cvc
-  regress0/arith/integers/arith-int-015.cvc
-  regress0/arith/integers/arith-int-021.cvc
-  regress0/arith/integers/arith-int-023.cvc
-  regress0/arith/integers/arith-int-025.cvc
-  regress0/arith/integers/arith-int-079.cvc
-  regress0/arith/integers/arith-interval.cvc
   regress0/arith/miplib-opt1217--27.smtv1.smt2
-  regress0/arith/miplib-pp08a-3000.smtv1.smt2
-  regress0/arr1.smtv1.smt2
-  regress0/arr1.smt2
-  regress0/arr2.smtv1.smt2
-  # regress0/aufbv/bug348 does not seem to terminate with proofs
-  regress0/aufbv/bug348.smtv1.smt2
-  regress0/aufbv/bug349.smtv1.smt2
-  regress0/aufbv/bug493.smtv1.smt2
   regress0/aufbv/dubreva005ue.smtv1.smt2
   regress0/aufbv/fifo32bc06k08.smtv1.smt2
-  regress0/aufbv/fifo32in06k08.delta01.smtv1.smt2
   regress0/aufbv/fifo32in06k08.smtv1.smt2
   regress0/aufbv/no_init_multi_delete14.smtv1.smt2
   regress0/aufbv/try3_sameret_functions_fse-bfs_tac.calc_next.il.fse-bfs.smtv1.smt2
-  regress0/aufbv/wchains010ue.smtv1.smt2
   regress0/auflia/fuzz01.smtv1.smt2
-  regress0/bug2.smtv1.smt2
-  regress0/bug374.smtv1.smt2
-  regress0/bv/bug345.smtv1.smt2
-  regress0/bv/bvcomp.cvc
-  regress0/bv/bvsmod.smt2
-  regress0/bv/core/bitvec0.delta01.smtv1.smt2
-  regress0/bv/core/bitvec1.smtv1.smt2
-  regress0/bv/core/bitvec3.smtv1.smt2
-  regress0/bv/core/bv_eq_diamond11.smtv1.smt2
-  regress0/bv/core/bv_eq_diamond12.smtv1.smt2
-  regress0/bv/core/bv_eq_diamond13.smtv1.smt2
-  regress0/bv/core/bv_eq_diamond14.smtv1.smt2
-  regress0/bv/core/bv_eq_diamond15.smtv1.smt2
-  regress0/bv/core/bv_eq_diamond16.smtv1.smt2
-  regress0/bv/core/bv_eq_diamond17.smtv1.smt2
-  regress0/bv/core/constant_core.smt2
-  regress0/bv/core/equality-04.smtv1.smt2
-  regress0/bv/core/equality-05.smtv1.smt2
-  regress0/bv/core/ext_con_004_001_1024.smtv1.smt2
-  regress0/bv/core/incremental.smtv1.smt2
-  regress0/bv/fuzz07-delta.smtv1.smt2
-  # Proof checking takes too long. Add this back. FIXME
-  regress0/bv/fuzz15.delta01.smtv1.smt2
   ###
-  regress0/bv/fuzz15.smtv1.smt2
-  regress0/bv/fuzz16.smtv1.smt2
-  regress0/bv/fuzz17.smtv1.smt2
-  regress0/bv/incorrect1.delta01.smtv1.smt2
-  regress0/bv/incorrect1.smtv1.smt2
-  regress0/bv/inequality00.smt2
-  regress0/bv/inequality01.smt2
-  regress0/bv/inequality02.smt2
-  regress0/bv/inequality03.smt2
-  regress0/bv/inequality04.smt2
-  regress0/bv/inequality05.smt2
   regress0/bv/test00.smtv1.smt2
-  regress0/cvc3-bug15.cvc
-  # regress0/datatypes/datatype-dump.cvc (FIXME #1649)
+  # FIXME #1649
   regress0/datatypes/datatype-dump.cvc
   # no longer support overloaded symbols across multiple parametric datatypes
   regress0/datatypes/repeated-selectors-2769.smt2
-  regress0/decision/uflia-xs-09-16-3-4-1-5.smtv1.smt2
-  regress0/decision/wchains010ue.smtv1.smt2
-  regress0/incorrect1.smtv1.smt2
-  regress0/ite.smt2
-  regress0/ite_arith.smt2
-  regress0/lemmas/fischer3-mutex-16.smtv1.smt2
-  regress0/nl/all-logic.smt2
-  # timeout after change to datatypes, impacting sygus-inst
-  regress0/quantifiers/issue4476-ext-rew.smt2
-  regress0/quantifiers/qbv-multi-lit-uge.smt2
-  regress0/quantifiers/qbv-test-invert-bvshl-0-neq.smt2
-  regress0/quantifiers/qbv-test-invert-concat-0-neq.smt2
-  regress0/quantifiers/qbv-test-invert-concat-1-neq.smt2
-  # times out on some CI configs after dt fact vs lemma update #5115
-  regress0/rels/rel_tc_7.cvc
-  regress0/sets/setel-eq.smt2
-  regress0/sets/sets-new.smt2
-  regress0/sets/sets-testlemma-ints.smt2
-  regress0/sets/sets-testlemma-reals.smt2
-  regress0/symmetric.smtv1.smt2
+  # need finite model finding command line in tptp regression
   regress0/tptp/BOO003-4.p
   regress0/tptp/BOO027-1.p
   regress0/tptp/MGT031-1.p
   regress0/tptp/NLP114-1.p
   regress0/tptp/SYN075+1.p
-  regress0/uf/PEQ018_size4.smtv1.smt2
-  regress0/uf/SEQ032_size2.smtv1.smt2
   regress0/uf/iso_icl_repgen004.smtv1.smt2
-  regress0/uflia/diseqprop.01.smtv1.smt2
-  regress0/uflia/diseqprop.02.smtv1.smt2
-  regress0/uflia/diseqprop.03.smtv1.smt2
-  regress0/uflia/diseqprop.04.smtv1.smt2
-  regress0/uflia/diseqprop.05.smtv1.smt2
-  regress0/uflia/diseqprop.06.smtv1.smt2
-  regress0/uflia/xs-09-16-3-4-1-5.delta05.smtv1.smt2
-  regress0/uflra/pb_real_10_0200_10_25.smtv1.smt2
-  regress0/uflra/pb_real_10_0200_10_27.smtv1.smt2
-  # dejan: disabled these because it's mixed arithmetic and it doesn't go
-  # well when changing theoryof:
-  regress0/unconstrained/arith2.smt2
-  regress0/unconstrained/arith7.smt2
   ###
-  # lianah: disabled these as the unconstrained terms are no longer
-  # recognized after implementing the divide-by-zero semantics for bv division:
-  regress0/unconstrained/bvconcat.smt2
-  regress1/auflia/bug337.smt2
   regress1/bug472.smt2
-  regress1/bug590.smt2
-  regress1/bv/bench_38.delta.smt2
+  regress1/datatypes/non-simple-rec-set.smt2
   # results in an assertion failure (see issue #1650).
   regress1/ho/hoa0102.smt2
-  # unknown after update to commands
-  regress1/ho/nested_lambdas-sat-SYO056^1-delta.smt2
   # slow on some builds after changes to tangent planes
   regress1/nl/approx-sqrt-unsat.smt2
-  # times out after no expand definitions for arithmetic
-  regress1/nl/issue3803-nl-check-model.smt2
   # times out after update to tangent planes
   regress1/nl/NAVIGATION2.smt2
   # sat or unknown in different builds
@@ -2443,56 +2456,36 @@ set(regression_disabled_tests
   regress1/quantifiers/arith-snorm.smt2
   # ajreynol: different error messages on production and debug:
   regress1/quantifiers/macro-subtype-param.smt2
-  # times out with competition build:
+  # times out with competition build, ok with other builds:
   regress1/quantifiers/model_6_1_bv.smt2
-  # times out after change to arithmetic expand definitions
-  regress1/quantifiers/nl-pow-trick.smt2
   # timeout after changes to nonlinear on PR #5351
   regress1/quantifiers/rel-trigger-unusable.smt2
+  # does not terminate/takes a long time when doing a coverage build with LFSC.
+  regress1/quantifiers/set3.smt2
   # changes to expand definitions, related to trigger selection for selectors
   regress1/quantifiers/stream-x2014-09-18-unsat.smt2
   # ajreynol: different error messages on production and debug:
   regress1/quantifiers/subtype-param-unk.smt2
   regress1/quantifiers/subtype-param.smt2
   ###
-  # regress1/quantifiers/set3.smt2 does not terminate/takes a long time when
-  # doing a coverage build with LFSC.
-  regress1/quantifiers/set3.smt2
   regress1/rels/garbage_collect.cvc
-  # times out after dt fact update due to overly eager splitting for tclosure
-  regress1/rels/rel_tc_4_1.cvc
   regress1/sets/setofsets-disequal.smt2
   regress1/sets/finite-type/sets-card-neg-mem-union-2.smt2
   regress1/simple-rdl-definefun.smt2
   # does not solve after minor modification to search
   regress1/sygus/car_3.lus.sy
   regress1/sygus/Base16_1.sy
+  regress1/sygus/interpol_from_pono_3.smt2
+  regress1/sygus/interpol_dt.smt2
   regress1/sygus/inv_gen_fig8.sy
-  # slow (179 seconds) in debug at 45e489e2
-  regress1/sygus/unifpi-solve-car_1.lus.sy
   # rely on heuristic solution reconstruction TODO #3146 revisit
   regress1/sygus/array_search_2.sy
   regress1/sygus/array_sum_2_5.sy
   regress1/sygus/crcy-si-rcons.sy
   # previously sygus inference did not apply, now (correctly) times out
   regress1/sygus/issue3498.smt2
-  # currently slow at c9fd28a
-  regress1/sygus/issue3580.sy
-  regress2/arith/arith-int-098.cvc
   regress2/arith/miplib-opt1217--27.smt2
-  regress2/arith/miplib-pp08a-3000.smt2
-  # timeout on debug
-  regress2/arith/real2int-test.smt2
-  regress2/bug396.smt2
-  # due to bv2int not handling unsigned/signed division
   regress2/nl/dumortier-050317.smt2
-  regress2/nl/nt-lemmas-bad.smt2
-  regress2/quantifiers/ForElimination-scala-9.smt2
-  regress2/quantifiers/small-bug1-fixpoint-3.smt2
-  # currently slow at 24357fea
-  regress2/sygus/inv_gen_n_c11.sy
-  regress2/xs-11-20-5-2-5-3.smtv1.smt2
-  regress2/xs-11-20-5-2-5-3.smt2
 )
 
 #-----------------------------------------------------------------------------#
diff --git a/test/regress/regress0/aufbv/bug493.smtv1.smt2 b/test/regress/regress0/aufbv/bug493.smtv1.smt2
index e702d8c7c..43ec2b2ca 100644
--- a/test/regress/regress0/aufbv/bug493.smtv1.smt2
+++ b/test/regress/regress0/aufbv/bug493.smtv1.smt2
@@ -1,7 +1,5 @@
 (set-option :incremental false)
-(set-info :source "Source unknown")
-(set-info :status unknown)
-(set-info :category "unknown")
+(set-info :status unsat)
 (set-logic QF_AUFBV)
 (declare-fun m () (Array (_ BitVec 8) (_ BitVec 8)))
 (declare-fun regionSize () (Array (_ BitVec 8) (_ BitVec 8)))
diff --git a/test/regress/regress0/aufbv/fifo32in06k08.delta01.smtv1.smt2 b/test/regress/regress0/aufbv/fifo32in06k08.delta01.smtv1.smt2
index 9f5c85f15..5b4853ff6 100644
--- a/test/regress/regress0/aufbv/fifo32in06k08.delta01.smtv1.smt2
+++ b/test/regress/regress0/aufbv/fifo32in06k08.delta01.smtv1.smt2
@@ -1,5 +1,5 @@
 (set-option :incremental false)
-(set-info :status unknown)
+(set-info :status sat)
 (set-logic QF_AUFBV)
 (declare-fun full_fq_2 () (_ BitVec 1))
 (declare-fun full_fs_2 () (_ BitVec 1))
diff --git a/test/regress/regress0/bv/bug345.smtv1.smt2 b/test/regress/regress0/bv/bug345.smtv1.smt2
index bdf646178..d35330d95 100644
--- a/test/regress/regress0/bv/bug345.smtv1.smt2
+++ b/test/regress/regress0/bv/bug345.smtv1.smt2
@@ -1,5 +1,5 @@
 (set-option :incremental false)
-(set-info :status unknown)
+(set-info :status sat)
 (set-logic QF_AUFBV)
 (declare-fun mem_35_197 () (Array (_ BitVec 32) (_ BitVec 8)))
 (check-sat-assuming ( (let ((_let_0 (concat (_ bv0 24) (select mem_35_197 (_ bv0 32))))) (let ((_let_1 ((_ extract 7 0) (concat (_ bv0 24) (select mem_35_197 (_ bv1 32)))))) (= (_ bv1 1) (bvor ((_ extract 0 0) (concat (_ bv0 31) (ite (= (_ bv0 32) _let_0) (_ bv1 1) (_ bv0 1)))) (ite (= (_ bv0 32) (concat (_ bv0 24) (select (store (store mem_35_197 (_ bv0 32) ((_ extract 7 0) (ite (= (_ bv0 8) _let_1) (_ bv1 32) (ite (= _let_1 (_ bv1 8)) (_ bv0 32) (ite (= _let_1 (_ bv3 8)) (_ bv1 32) (_ bv0 32)))))) (bvadd _let_0 (concat (_ bv0 24) ((_ extract 7 0) (concat (_ bv0 24) ((_ extract 7 0) (concat (_ bv0 24) _let_1)))))) (_ bv0 8)) (_ bv0 32)))) (_ bv1 1) (_ bv0 1)))))) ))
diff --git a/test/regress/regress0/bv/core/bitvec0.delta01.smtv1.smt2 b/test/regress/regress0/bv/core/bitvec0.delta01.smtv1.smt2
index 136b59825..59b7e0e91 100644
--- a/test/regress/regress0/bv/core/bitvec0.delta01.smtv1.smt2
+++ b/test/regress/regress0/bv/core/bitvec0.delta01.smtv1.smt2
@@ -1,5 +1,5 @@
 (set-option :incremental false)
-(set-info :status unknown)
+(set-info :status unsat)
 (set-logic QF_BV)
 (declare-fun t () (_ BitVec 32))
 (check-sat-assuming ( (not (ite (= ((_ extract 4 0) t) ((_ extract 6 2) t)) (and (= ((_ extract 6 6) t) ((_ extract 0 0) t)) (= ((_ extract 1 1) t) ((_ extract 5 5) t))) true)) ))
diff --git a/test/regress/regress0/bv/core/equality-05.cvc b/test/regress/regress0/bv/core/equality-05.cvc
deleted file mode 100644
index 93bef502d..000000000
--- a/test/regress/regress0/bv/core/equality-05.cvc
+++ /dev/null
@@ -1,6 +0,0 @@
-x,y:BITVECTOR(1);
-ASSERT(x = 0bin0);
-ASSERT(y = 0bin1);
-ASSERT(x = y);
-CHECKSAT;
-
diff --git a/test/regress/regress0/bv/core/incremental.smtv1.smt2 b/test/regress/regress0/bv/core/incremental.smtv1.smt2
index a3f340543..3abe543af 100644
--- a/test/regress/regress0/bv/core/incremental.smtv1.smt2
+++ b/test/regress/regress0/bv/core/incremental.smtv1.smt2
@@ -1,5 +1,5 @@
 (set-option :incremental false)
-(set-info :status unknown)
+(set-info :status unsat)
 (set-logic QF_BV)
 (declare-fun v4 () (_ BitVec 16))
 (declare-fun dummy4 () (_ BitVec 1))
diff --git a/test/regress/regress0/bv/fuzz07-delta.smtv1.smt2 b/test/regress/regress0/bv/fuzz07-delta.smtv1.smt2
index 20ddbe219..1d010a606 100644
--- a/test/regress/regress0/bv/fuzz07-delta.smtv1.smt2
+++ b/test/regress/regress0/bv/fuzz07-delta.smtv1.smt2
@@ -1,5 +1,5 @@
 (set-option :incremental false)
-(set-info :status unknown)
+(set-info :status sat)
 (set-logic QF_BV)
 (declare-fun v1 () (_ BitVec 2))
 (check-sat-assuming ( (let ((_let_0 ((_ sign_extend 1) (ite (bvugt (bvcomp v1 (_ bv1 2)) (_ bv0 1)) (_ bv1 1) (_ bv0 1))))) (ite (= (_ bv0 8) (concat (_ bv0 2) (concat (ite (= (_ bv0 5) ((_ sign_extend 3) v1)) (_ bv1 1) (_ bv0 1)) (_ bv0 5)))) false (ite (= (_ bv0 4) ((_ sign_extend 2) _let_0)) true (= (_ bv0 16) ((_ zero_extend 15) (ite (distinct (_ bv0 3) ((_ zero_extend 2) (ite (bvsle (_ bv0 2) _let_0) (_ bv1 1) (_ bv0 1)))) (_ bv1 1) (_ bv0 1))))))) ))
diff --git a/test/regress/regress0/incorrect1.smtv1.smt2 b/test/regress/regress0/incorrect1.smtv1.smt2
index 1d24f09ac..498a842fb 100644
--- a/test/regress/regress0/incorrect1.smtv1.smt2
+++ b/test/regress/regress0/incorrect1.smtv1.smt2
@@ -1,5 +1,5 @@
 (set-option :incremental false)
-(set-info :status unknown)
+(set-info :status sat)
 (set-logic QF_BV)
 (declare-fun v0 () (_ BitVec 10))
 (check-sat-assuming ( (let ((_let_0 (ite (bvule (_ bv30369 16) (_ bv30369 16)) (_ bv1 1) (_ bv0 1)))) (let ((_let_1 (bvcomp ((_ zero_extend 1) _let_0) (_ bv3 2)))) (let ((_let_2 ((_ sign_extend 15) _let_1))) (let ((_let_3 (bvsmod (_ bv30369 16) (_ bv30369 16)))) (let ((_let_4 ((_ sign_extend 15) _let_0))) (let ((_let_5 (or (xor (bvsgt _let_4 _let_3) (bvuge (_ bv30369 16) ((_ sign_extend 15) (ite (bvsgt _let_2 (_ bv30369 16)) (_ bv1 1) (_ bv0 1))))) (bvslt ((_ sign_extend 14) (_ bv3 2)) _let_3)))) (let ((_let_6 (not (xor (bvsge (bvsdiv v0 v0) ((_ zero_extend 9) _let_0)) (bvsge (bvsdiv v0 v0) ((_ zero_extend 9) _let_0)))))) (and (and (and (and (= (or (or (bvsgt v0 ((_ sign_extend 9) _let_0)) (bvsgt (_ bv3 2) ((_ sign_extend 1) _let_0))) (=> (bvslt ((_ zero_extend 9) _let_0) (bvsdiv v0 v0)) (bvult (_ bv3 2) (_ bv3 2)))) (= (and _let_6 _let_6) (= (= (xor (and _let_5 _let_5) (xor (bvslt _let_3 ((_ zero_extend 15) _let_1)) (bvugt _let_2 _let_3))) (not (distinct ((_ zero_extend 9) _let_1) v0))) (xor (= (not (and (bvsle (_ bv30369 16) ((_ zero_extend 14) (_ bv3 2))) (bvslt _let_0 _let_1))) (= ((_ zero_extend 8) (_ bv3 2)) v0)) (and (not (bvsgt _let_1 _let_1)) (= _let_3 _let_4)))))) (not (= v0 (_ bv0 10)))) (not (= v0 (bvnot (_ bv0 10))))) (not (= (_ bv30369 16) (_ bv0 16)))) (not (= (_ bv30369 16) (bvnot (_ bv0 16)))))))))))) ))
diff --git a/test/regress/regress0/quantifiers/qbv-multi-lit-uge.smt2 b/test/regress/regress0/quantifiers/qbv-multi-lit-uge.smt2
index b6095fcab..b7f245c7d 100644
--- a/test/regress/regress0/quantifiers/qbv-multi-lit-uge.smt2
+++ b/test/regress/regress0/quantifiers/qbv-multi-lit-uge.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cegqi-bv --no-cegqi-full
+; COMMAND-LINE: --cegqi-bv
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
diff --git a/test/regress/regress0/uflia/diseqprop.01.smtv1.smt2 b/test/regress/regress0/uflia/diseqprop.01.smtv1.smt2
index 5432077c0..093842012 100644
--- a/test/regress/regress0/uflia/diseqprop.01.smtv1.smt2
+++ b/test/regress/regress0/uflia/diseqprop.01.smtv1.smt2
@@ -1,4 +1,5 @@
 (set-option :incremental false)
+(set-info :status sat)
 (set-logic QF_UFLIA)
 (declare-fun f (Int) Int)
 (declare-fun x1 () Int)
diff --git a/test/regress/regress0/uflia/diseqprop.02.smtv1.smt2 b/test/regress/regress0/uflia/diseqprop.02.smtv1.smt2
index e146bd7fd..3d7123757 100644
--- a/test/regress/regress0/uflia/diseqprop.02.smtv1.smt2
+++ b/test/regress/regress0/uflia/diseqprop.02.smtv1.smt2
@@ -1,4 +1,5 @@
 (set-option :incremental false)
+(set-info :status sat)
 (set-logic QF_UFLIA)
 (declare-fun f (Int) Int)
 (declare-fun x1 () Int)
diff --git a/test/regress/regress0/uflia/diseqprop.03.smtv1.smt2 b/test/regress/regress0/uflia/diseqprop.03.smtv1.smt2
index 3acee371b..c8f2f889c 100644
--- a/test/regress/regress0/uflia/diseqprop.03.smtv1.smt2
+++ b/test/regress/regress0/uflia/diseqprop.03.smtv1.smt2
@@ -1,4 +1,5 @@
 (set-option :incremental false)
+(set-info :status sat)
 (set-logic QF_UFLIA)
 (declare-fun f (Int) Int)
 (declare-fun x1 () Int)
diff --git a/test/regress/regress0/uflia/diseqprop.04.smtv1.smt2 b/test/regress/regress0/uflia/diseqprop.04.smtv1.smt2
index a1fec8795..b9d10fdc6 100644
--- a/test/regress/regress0/uflia/diseqprop.04.smtv1.smt2
+++ b/test/regress/regress0/uflia/diseqprop.04.smtv1.smt2
@@ -1,4 +1,5 @@
 (set-option :incremental false)
+(set-info :status sat)
 (set-logic QF_UFLIA)
 (declare-fun f (Int) Int)
 (declare-fun x1 () Int)
diff --git a/test/regress/regress0/uflia/diseqprop.05.smtv1.smt2 b/test/regress/regress0/uflia/diseqprop.05.smtv1.smt2
index dc18a4560..c53d44bc8 100644
--- a/test/regress/regress0/uflia/diseqprop.05.smtv1.smt2
+++ b/test/regress/regress0/uflia/diseqprop.05.smtv1.smt2
@@ -1,4 +1,5 @@
 (set-option :incremental false)
+(set-info :status sat)
 (set-logic QF_UFLIA)
 (declare-fun f (Int) Int)
 (declare-fun x1 () Int)
diff --git a/test/regress/regress0/uflia/diseqprop.06.smtv1.smt2 b/test/regress/regress0/uflia/diseqprop.06.smtv1.smt2
index 0e411d752..1449607e5 100644
--- a/test/regress/regress0/uflia/diseqprop.06.smtv1.smt2
+++ b/test/regress/regress0/uflia/diseqprop.06.smtv1.smt2
@@ -1,4 +1,5 @@
 (set-option :incremental false)
+(set-info :status sat)
 (set-logic QF_UFLIA)
 (declare-fun f (Int) Int)
 (declare-fun x1 () Int)
diff --git a/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta05.smtv1.smt2 b/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta05.smtv1.smt2
index e8386d2ab..852328903 100644
--- a/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta05.smtv1.smt2
+++ b/test/regress/regress0/uflia/xs-09-16-3-4-1-5.delta05.smtv1.smt2
@@ -1,5 +1,5 @@
 (set-option :incremental false)
-(set-info :status unknown)
+(set-info :status sat)
 (set-logic QF_UFLIA)
 (declare-fun select_format (Int) Int)
 (declare-fun adr_lo () Int)
diff --git a/test/regress/regress0/aufbv/bug348.smtv1.smt2 b/test/regress/regress1/aufbv/bug348.smtv1.smt2
index 207da82c5..207da82c5 100644
--- a/test/regress/regress0/aufbv/bug348.smtv1.smt2
+++ b/test/regress/regress1/aufbv/bug348.smtv1.smt2
diff --git a/test/regress/regress1/bug590.smt2 b/test/regress/regress1/bug590.smt2
index 448c65f99..d50024268 100644
--- a/test/regress/regress1/bug590.smt2
+++ b/test/regress/regress1/bug590.smt2
@@ -1,7 +1,7 @@
 ; EXPECT: unknown
 ; EXPECT: ((charlst2 ((as const (Array Int String)) "")))
 
-(set-logic QF_ALL_SUPPORTED)
+(set-logic ALL)
 (set-option :strings-exp true)
 (set-option :produce-models true)
 (set-info :smt-lib-version 2.0)
diff --git a/test/regress/regress0/bv/incorrect1.smtv1.smt2 b/test/regress/regress1/bv/incorrect1.smtv1.smt2
index 8d79f91e2..8d79f91e2 100644
--- a/test/regress/regress0/bv/incorrect1.smtv1.smt2
+++ b/test/regress/regress1/bv/incorrect1.smtv1.smt2
diff --git a/test/regress/regress1/nl/issue3803-nl-check-model.smt2 b/test/regress/regress1/nl/issue3803-nl-check-model.smt2
index 7dfda36ea..99d945ce2 100644
--- a/test/regress/regress1/nl/issue3803-nl-check-model.smt2
+++ b/test/regress/regress1/nl/issue3803-nl-check-model.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --ext-rew-prep
+; COMMAND-LINE: --ext-rew-prep -q
 ; EXPECT: sat
 (set-logic ALL)
 (set-info :status sat)
diff --git a/test/regress/regress1/quantifiers/arith-snorm.smt2 b/test/regress/regress1/quantifiers/arith-snorm.smt2
index c7968f8ee..8076f5660 100644
--- a/test/regress/regress1/quantifiers/arith-snorm.smt2
+++ b/test/regress/regress1/quantifiers/arith-snorm.smt2
@@ -1,5 +1,3 @@
-; COMMAND-LINE: --snorm-infer-eq
-; EXPECT: unsat
 (set-info :smt-lib-version 2.6)
 (set-logic UFLIA)
 (set-info :source | Simplify Theorem Prover Benchmark Suite |)
diff --git a/test/regress/regress0/quantifiers/issue4476-ext-rew.smt2 b/test/regress/regress1/quantifiers/issue4476-ext-rew.smt2
index 8f1d8285d..8f1d8285d 100644
--- a/test/regress/regress0/quantifiers/issue4476-ext-rew.smt2
+++ b/test/regress/regress1/quantifiers/issue4476-ext-rew.smt2
diff --git a/test/regress/regress0/aufbv/bug349.smtv1.smt2 b/test/regress/regress2/bug349.smtv1.smt2
index f1807fd8f..f1807fd8f 100644
--- a/test/regress/regress0/aufbv/bug349.smtv1.smt2
+++ b/test/regress/regress2/bug349.smtv1.smt2
diff --git a/test/regress/regress0/bug374.smtv1.smt2 b/test/regress/regress2/bug374.smtv1.smt2
index b5054cd7c..37b6fea4f 100644
--- a/test/regress/regress0/bug374.smtv1.smt2
+++ b/test/regress/regress2/bug374.smtv1.smt2
@@ -1,5 +1,5 @@
 (set-option :incremental false)
-(set-info :status unknown)
+(set-info :status unsat)
 (set-logic AUFLIA)
 (declare-fun f0 (Int Int) Int)
 (declare-fun f1 ((Array Int Int) (Array Int Int) (Array Int Int)) (Array Int Int))
diff --git a/test/regress/regress4/hole10.cvc b/test/regress/regress2/hole10.cvc
index fb4c41b35..fb4c41b35 100644
--- a/test/regress/regress4/hole10.cvc
+++ b/test/regress/regress2/hole10.cvc
diff --git a/test/regress/regress2/nl/dumortier-050317.smt2 b/test/regress/regress2/nl/dumortier-050317.smt2
index 04c498ca0..0c815bf2a 100644
--- a/test/regress/regress2/nl/dumortier-050317.smt2
+++ b/test/regress/regress2/nl/dumortier-050317.smt2
@@ -1,4 +1,4 @@
-(set-logic QF_NRA)
+(set-logic QF_NRAT)
 (declare-fun time__AT0@0 () Real)
 (declare-fun instance.y__AT0@0 () Real)
 (declare-fun instance.x__AT0@0 () Real)
diff --git a/test/regress/regress0/strings/bidir_star.smt2 b/test/regress/regress2/strings/bidir_star.smt2
index 8a13ed085..8a13ed085 100644
--- a/test/regress/regress0/strings/bidir_star.smt2
+++ b/test/regress/regress2/strings/bidir_star.smt2
diff --git a/test/regress/regress2/sygus/DRAGON_1.lus.sy b/test/regress/regress3/DRAGON_1.lus.sy
index 4d9510ade..4d9510ade 100644
--- a/test/regress/regress2/sygus/DRAGON_1.lus.sy
+++ b/test/regress/regress3/DRAGON_1.lus.sy
diff --git a/test/regress/regress0/uf/PEQ018_size4.smtv1.smt2 b/test/regress/regress3/PEQ018_size4.smtv1.smt2
index 5481ddddd..5481ddddd 100644
--- a/test/regress/regress0/uf/PEQ018_size4.smtv1.smt2
+++ b/test/regress/regress3/PEQ018_size4.smtv1.smt2
diff --git a/test/regress/regress0/aufbv/wchains010ue.smtv1.smt2 b/test/regress/regress3/aufbv-wchains010ue.smtv1.smt2
index f1792136b..f1792136b 100644
--- a/test/regress/regress0/aufbv/wchains010ue.smtv1.smt2
+++ b/test/regress/regress3/aufbv-wchains010ue.smtv1.smt2
diff --git a/test/regress/regress2/auflia-fuzz06.smtv1.smt2 b/test/regress/regress3/auflia-fuzz06.smtv1.smt2
index b0163912f..b0163912f 100644
--- a/test/regress/regress2/auflia-fuzz06.smtv1.smt2
+++ b/test/regress/regress3/auflia-fuzz06.smtv1.smt2
diff --git a/test/regress/regress0/bug2.smtv1.smt2 b/test/regress/regress3/bug2.smtv1.smt2
index 720c0410d..720c0410d 100644
--- a/test/regress/regress0/bug2.smtv1.smt2
+++ b/test/regress/regress3/bug2.smtv1.smt2
diff --git a/test/regress/regress0/bv/core/ext_con_004_001_1024.smtv1.smt2 b/test/regress/regress3/bv-core-ext_con_004_001_1024.smtv1.smt2
index b2884e132..b2884e132 100644
--- a/test/regress/regress0/bv/core/ext_con_004_001_1024.smtv1.smt2
+++ b/test/regress/regress3/bv-core-ext_con_004_001_1024.smtv1.smt2
diff --git a/test/regress/regress0/bv/fuzz15.smtv1.smt2 b/test/regress/regress3/bv-fuzz15.smtv1.smt2
index d621b3356..d621b3356 100644
--- a/test/regress/regress0/bv/fuzz15.smtv1.smt2
+++ b/test/regress/regress3/bv-fuzz15.smtv1.smt2
diff --git a/test/regress/regress0/bv/fuzz16.smtv1.smt2 b/test/regress/regress3/bv-fuzz16.smtv1.smt2
index 51d748749..51d748749 100644
--- a/test/regress/regress0/bv/fuzz16.smtv1.smt2
+++ b/test/regress/regress3/bv-fuzz16.smtv1.smt2
diff --git a/test/regress/regress0/bv/fuzz17.smtv1.smt2 b/test/regress/regress3/bv-fuzz17.smtv1.smt2
index 989b860c1..989b860c1 100644
--- a/test/regress/regress0/bv/fuzz17.smtv1.smt2
+++ b/test/regress/regress3/bv-fuzz17.smtv1.smt2
diff --git a/test/regress/regress1/sygus/cegisunif-depth1.sy b/test/regress/regress3/cegisunif-depth1.sy
index 06c4d3a78..06c4d3a78 100644
--- a/test/regress/regress1/sygus/cegisunif-depth1.sy
+++ b/test/regress/regress3/cegisunif-depth1.sy
diff --git a/test/regress/regress0/decision/uflia-xs-09-16-3-4-1-5.smtv1.smt2 b/test/regress/regress3/decision-uflia-xs-09-16-3-4-1-5.smtv1.smt2
index 2f46fd382..2f46fd382 100644
--- a/test/regress/regress0/decision/uflia-xs-09-16-3-4-1-5.smtv1.smt2
+++ b/test/regress/regress3/decision-uflia-xs-09-16-3-4-1-5.smtv1.smt2
diff --git a/test/regress/regress0/decision/wchains010ue.smtv1.smt2 b/test/regress/regress3/decision-wchains010ue.smtv1.smt2
index 3d25b142d..3d25b142d 100644
--- a/test/regress/regress0/decision/wchains010ue.smtv1.smt2
+++ b/test/regress/regress3/decision-wchains010ue.smtv1.smt2
diff --git a/test/regress/regress1/sygus/interpol2.smt2 b/test/regress/regress3/interpol2.smt2
index c6876ee15..c6876ee15 100644
--- a/test/regress/regress1/sygus/interpol2.smt2
+++ b/test/regress/regress3/interpol2.smt2
diff --git a/test/regress/regress2/sygus/inv_gen_n_c11.sy b/test/regress/regress3/inv_gen_n_c11.sy
index aebc03dea..aebc03dea 100644
--- a/test/regress/regress2/sygus/inv_gen_n_c11.sy
+++ b/test/regress/regress3/inv_gen_n_c11.sy
diff --git a/test/regress/regress2/arith/lpsat-goal-9.smt2 b/test/regress/regress3/lpsat-goal-9.smt2
index d71fc1340..d71fc1340 100644
--- a/test/regress/regress2/arith/lpsat-goal-9.smt2
+++ b/test/regress/regress3/lpsat-goal-9.smt2
diff --git a/test/regress/regress2/sygus/nia-max-square.sy b/test/regress/regress3/nia-max-square.sy
index 0657494b1..0657494b1 100644
--- a/test/regress/regress2/sygus/nia-max-square.sy
+++ b/test/regress/regress3/nia-max-square.sy
diff --git a/test/regress/regress2/sygus/policyM.sy b/test/regress/regress3/policyM.sy
index 0e9b33148..0e9b33148 100644
--- a/test/regress/regress2/sygus/policyM.sy
+++ b/test/regress/regress3/policyM.sy
diff --git a/test/regress/regress1/rr-verify/regex.sy b/test/regress/regress3/regex-rrv.sy
index 2d911e56a..2d911e56a 100644
--- a/test/regress/regress1/rr-verify/regex.sy
+++ b/test/regress/regress3/regex-rrv.sy
diff --git a/test/regress/regress2/quantifiers/specsharp-WindowsCard.15.RTE.Terminate_System.Int32.smt2 b/test/regress/regress3/specsharp-WindowsCard.15.RTE.Terminate_System.Int32.smt2
index 7be432dbf..7be432dbf 100644
--- a/test/regress/regress2/quantifiers/specsharp-WindowsCard.15.RTE.Terminate_System.Int32.smt2
+++ b/test/regress/regress3/specsharp-WindowsCard.15.RTE.Terminate_System.Int32.smt2
diff --git a/test/regress/regress1/sygus/unbdd_inv_gen_ex7.sy b/test/regress/regress3/unbdd_inv_gen_ex7.sy
index 34abb6de8..34abb6de8 100644
--- a/test/regress/regress1/sygus/unbdd_inv_gen_ex7.sy
+++ b/test/regress/regress3/unbdd_inv_gen_ex7.sy
diff --git a/test/regress/regress1/sygus/unifpi-solve-car_1.lus.sy b/test/regress/regress3/unifpi-solve-car_1.lus.sy
index c1d196f60..c1d196f60 100644
--- a/test/regress/regress1/sygus/unifpi-solve-car_1.lus.sy
+++ b/test/regress/regress3/unifpi-solve-car_1.lus.sy
diff --git a/test/regress/regress2/sygus/vcb.sy b/test/regress/regress3/vcb.sy
index a0122193d..a0122193d 100644
--- a/test/regress/regress2/sygus/vcb.sy
+++ b/test/regress/regress3/vcb.sy
diff --git a/test/regress/regress1/auflia/bug337.smt2 b/test/regress/regress4/bug337.smt2
index b7a564a60..b7a564a60 100644
--- a/test/regress/regress1/auflia/bug337.smt2
+++ b/test/regress/regress4/bug337.smt2
diff --git a/test/regress/regress2/bug396.smt2 b/test/regress/regress4/bug396.smt2
index 8e93cf447..8e93cf447 100644
--- a/test/regress/regress2/bug396.smt2
+++ b/test/regress/regress4/bug396.smt2
diff --git a/test/regress/regress0/lemmas/fischer3-mutex-16.smtv1.smt2 b/test/regress/regress4/fischer3-mutex-16.smtv1.smt2
index e475252ec..e475252ec 100644
--- a/test/regress/regress0/lemmas/fischer3-mutex-16.smtv1.smt2
+++ b/test/regress/regress4/fischer3-mutex-16.smtv1.smt2
diff --git a/test/regress/regress3/issue2429.smt2 b/test/regress/regress4/issue2429.smt2
index 9fe07b6f4..9fe07b6f4 100644
--- a/test/regress/regress3/issue2429.smt2
+++ b/test/regress/regress4/issue2429.smt2
diff --git a/test/regress/regress2/arith/miplib-pp08a-3000.smt2 b/test/regress/regress4/miplib-pp08a-3000.smt2
index edd77a9d1..edd77a9d1 100644
--- a/test/regress/regress2/arith/miplib-pp08a-3000.smt2
+++ b/test/regress/regress4/miplib-pp08a-3000.smt2
diff --git a/test/regress/regress0/arith/miplib-pp08a-3000.smtv1.smt2 b/test/regress/regress4/miplib-pp08a-3000.smtv1.smt2
index 90902366b..90902366b 100644
--- a/test/regress/regress0/arith/miplib-pp08a-3000.smtv1.smt2
+++ b/test/regress/regress4/miplib-pp08a-3000.smtv1.smt2
diff --git a/test/regress/regress3/pp-regfile.smtv1.smt2 b/test/regress/regress4/pp-regfile.smtv1.smt2
index b279cf209..b279cf209 100644
--- a/test/regress/regress3/pp-regfile.smtv1.smt2
+++ b/test/regress/regress4/pp-regfile.smtv1.smt2
diff --git a/test/regress/regress1/sets/infinite-type/sets-card-neg-mem-union-2.smt2 b/test/regress/regress4/sets-card-neg-mem-union-2.smt2
index baeb1387a..baeb1387a 100644
--- a/test/regress/regress1/sets/infinite-type/sets-card-neg-mem-union-2.smt2
+++ b/test/regress/regress4/sets-card-neg-mem-union-2.smt2
diff --git a/test/regress/regress3/strings/unsat-circ-reduce.smt2 b/test/regress/regress4/unsat-circ-reduce.smt2
index b584c0fb1..b584c0fb1 100644
--- a/test/regress/regress3/strings/unsat-circ-reduce.smt2
+++ b/test/regress/regress4/unsat-circ-reduce.smt2
diff --git a/test/regress/regress2/xs-11-20-5-2-5-3.smt2 b/test/regress/regress4/xs-11-20-5-2-5-3.smt2
index bdf0d25ab..bdf0d25ab 100644
--- a/test/regress/regress2/xs-11-20-5-2-5-3.smt2
+++ b/test/regress/regress4/xs-11-20-5-2-5-3.smt2
diff --git a/test/regress/regress2/xs-11-20-5-2-5-3.smtv1.smt2 b/test/regress/regress4/xs-11-20-5-2-5-3.smtv1.smt2
index a239ee21e..a239ee21e 100644
--- a/test/regress/regress2/xs-11-20-5-2-5-3.smtv1.smt2
+++ b/test/regress/regress4/xs-11-20-5-2-5-3.smtv1.smt2