From 37f51226cc8a96fc699648068f8c72a2f0832f51 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 10 Dec 2020 09:09:05 -0600 Subject: [PATCH] Refactor regressions (#5639) This adds a net +82 regressions to regress[0-2] and adds several additional disabled regressions to regress3 and regress4. This involved fixing the status on several regressions, and ensuring CMakeLists.txt includes all files (exactly once) in the test/regress/ subdirectory. It also moves several regressions to the proper regression levels (those that take >30 seconds in debug are moved to regress3+). --- test/regress/CMakeLists.txt | 423 +++++++++--------- test/regress/regress0/aufbv/bug493.smtv1.smt2 | 4 +- .../aufbv/fifo32in06k08.delta01.smtv1.smt2 | 2 +- test/regress/regress0/bv/bug345.smtv1.smt2 | 2 +- .../bv/core/bitvec0.delta01.smtv1.smt2 | 2 +- test/regress/regress0/bv/core/equality-05.cvc | 6 - .../regress0/bv/core/incremental.smtv1.smt2 | 2 +- .../regress0/bv/fuzz07-delta.smtv1.smt2 | 2 +- test/regress/regress0/incorrect1.smtv1.smt2 | 2 +- .../quantifiers/qbv-multi-lit-uge.smt2 | 2 +- .../regress0/uflia/diseqprop.01.smtv1.smt2 | 1 + .../regress0/uflia/diseqprop.02.smtv1.smt2 | 1 + .../regress0/uflia/diseqprop.03.smtv1.smt2 | 1 + .../regress0/uflia/diseqprop.04.smtv1.smt2 | 1 + .../regress0/uflia/diseqprop.05.smtv1.smt2 | 1 + .../regress0/uflia/diseqprop.06.smtv1.smt2 | 1 + .../uflia/xs-09-16-3-4-1-5.delta05.smtv1.smt2 | 2 +- .../aufbv/bug348.smtv1.smt2 | 0 test/regress/regress1/bug590.smt2 | 2 +- .../bv/incorrect1.smtv1.smt2 | 0 .../regress1/nl/issue3803-nl-check-model.smt2 | 2 +- .../regress1/quantifiers/arith-snorm.smt2 | 2 - .../quantifiers/issue4476-ext-rew.smt2 | 0 .../aufbv => regress2}/bug349.smtv1.smt2 | 0 .../{regress0 => regress2}/bug374.smtv1.smt2 | 2 +- .../regress/{regress4 => regress2}/hole10.cvc | 0 .../regress/regress2/nl/dumortier-050317.smt2 | 2 +- .../strings/bidir_star.smt2 | 0 .../sygus => regress3}/DRAGON_1.lus.sy | 0 .../uf => regress3}/PEQ018_size4.smtv1.smt2 | 0 .../aufbv-wchains010ue.smtv1.smt2} | 0 .../auflia-fuzz06.smtv1.smt2 | 0 .../{regress0 => regress3}/bug2.smtv1.smt2 | 0 .../bv-core-ext_con_004_001_1024.smtv1.smt2} | 0 .../bv-fuzz15.smtv1.smt2} | 0 .../bv-fuzz16.smtv1.smt2} | 0 .../bv-fuzz17.smtv1.smt2} | 0 .../sygus => regress3}/cegisunif-depth1.sy | 0 ...ecision-uflia-xs-09-16-3-4-1-5.smtv1.smt2} | 0 .../decision-wchains010ue.smtv1.smt2} | 0 .../sygus => regress3}/interpol2.smt2 | 0 .../sygus => regress3}/inv_gen_n_c11.sy | 0 .../arith => regress3}/lpsat-goal-9.smt2 | 0 .../sygus => regress3}/nia-max-square.sy | 0 .../{regress2/sygus => regress3}/policyM.sy | 0 .../regex.sy => regress3/regex-rrv.sy} | 0 ...owsCard.15.RTE.Terminate_System.Int32.smt2 | 0 .../sygus => regress3}/unbdd_inv_gen_ex7.sy | 0 .../unifpi-solve-car_1.lus.sy | 0 .../{regress2/sygus => regress3}/vcb.sy | 0 .../{regress1/auflia => regress4}/bug337.smt2 | 0 .../{regress2 => regress4}/bug396.smt2 | 0 .../fischer3-mutex-16.smtv1.smt2 | 0 .../{regress3 => regress4}/issue2429.smt2 | 0 .../arith => regress4}/miplib-pp08a-3000.smt2 | 0 .../miplib-pp08a-3000.smtv1.smt2 | 0 .../pp-regfile.smtv1.smt2 | 0 .../sets-card-neg-mem-union-2.smt2 | 0 .../unsat-circ-reduce.smt2 | 0 .../xs-11-20-5-2-5-3.smt2 | 0 .../xs-11-20-5-2-5-3.smtv1.smt2 | 0 61 files changed, 227 insertions(+), 238 deletions(-) delete mode 100644 test/regress/regress0/bv/core/equality-05.cvc rename test/regress/{regress0 => regress1}/aufbv/bug348.smtv1.smt2 (100%) rename test/regress/{regress0 => regress1}/bv/incorrect1.smtv1.smt2 (100%) rename test/regress/{regress0 => regress1}/quantifiers/issue4476-ext-rew.smt2 (100%) rename test/regress/{regress0/aufbv => regress2}/bug349.smtv1.smt2 (100%) rename test/regress/{regress0 => regress2}/bug374.smtv1.smt2 (99%) rename test/regress/{regress4 => regress2}/hole10.cvc (100%) rename test/regress/{regress0 => regress2}/strings/bidir_star.smt2 (100%) rename test/regress/{regress2/sygus => regress3}/DRAGON_1.lus.sy (100%) rename test/regress/{regress0/uf => regress3}/PEQ018_size4.smtv1.smt2 (100%) rename test/regress/{regress0/aufbv/wchains010ue.smtv1.smt2 => regress3/aufbv-wchains010ue.smtv1.smt2} (100%) rename test/regress/{regress2 => regress3}/auflia-fuzz06.smtv1.smt2 (100%) rename test/regress/{regress0 => regress3}/bug2.smtv1.smt2 (100%) rename test/regress/{regress0/bv/core/ext_con_004_001_1024.smtv1.smt2 => regress3/bv-core-ext_con_004_001_1024.smtv1.smt2} (100%) rename test/regress/{regress0/bv/fuzz15.smtv1.smt2 => regress3/bv-fuzz15.smtv1.smt2} (100%) rename test/regress/{regress0/bv/fuzz16.smtv1.smt2 => regress3/bv-fuzz16.smtv1.smt2} (100%) rename test/regress/{regress0/bv/fuzz17.smtv1.smt2 => regress3/bv-fuzz17.smtv1.smt2} (100%) rename test/regress/{regress1/sygus => regress3}/cegisunif-depth1.sy (100%) rename test/regress/{regress0/decision/uflia-xs-09-16-3-4-1-5.smtv1.smt2 => regress3/decision-uflia-xs-09-16-3-4-1-5.smtv1.smt2} (100%) rename test/regress/{regress0/decision/wchains010ue.smtv1.smt2 => regress3/decision-wchains010ue.smtv1.smt2} (100%) rename test/regress/{regress1/sygus => regress3}/interpol2.smt2 (100%) rename test/regress/{regress2/sygus => regress3}/inv_gen_n_c11.sy (100%) rename test/regress/{regress2/arith => regress3}/lpsat-goal-9.smt2 (100%) rename test/regress/{regress2/sygus => regress3}/nia-max-square.sy (100%) rename test/regress/{regress2/sygus => regress3}/policyM.sy (100%) rename test/regress/{regress1/rr-verify/regex.sy => regress3/regex-rrv.sy} (100%) rename test/regress/{regress2/quantifiers => regress3}/specsharp-WindowsCard.15.RTE.Terminate_System.Int32.smt2 (100%) rename test/regress/{regress1/sygus => regress3}/unbdd_inv_gen_ex7.sy (100%) rename test/regress/{regress1/sygus => regress3}/unifpi-solve-car_1.lus.sy (100%) rename test/regress/{regress2/sygus => regress3}/vcb.sy (100%) rename test/regress/{regress1/auflia => regress4}/bug337.smt2 (100%) rename test/regress/{regress2 => regress4}/bug396.smt2 (100%) rename test/regress/{regress0/lemmas => regress4}/fischer3-mutex-16.smtv1.smt2 (100%) rename test/regress/{regress3 => regress4}/issue2429.smt2 (100%) rename test/regress/{regress2/arith => regress4}/miplib-pp08a-3000.smt2 (100%) rename test/regress/{regress0/arith => regress4}/miplib-pp08a-3000.smtv1.smt2 (100%) rename test/regress/{regress3 => regress4}/pp-regfile.smtv1.smt2 (100%) rename test/regress/{regress1/sets/infinite-type => regress4}/sets-card-neg-mem-union-2.smt2 (100%) rename test/regress/{regress3/strings => regress4}/unsat-circ-reduce.smt2 (100%) rename test/regress/{regress2 => regress4}/xs-11-20-5-2-5-3.smt2 (100%) rename test/regress/{regress2 => regress4}/xs-11-20-5-2-5-3.smtv1.smt2 (100%) 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 similarity index 100% rename from test/regress/regress0/aufbv/bug348.smtv1.smt2 rename to 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 similarity index 100% rename from test/regress/regress0/bv/incorrect1.smtv1.smt2 rename to 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 similarity index 100% rename from test/regress/regress0/quantifiers/issue4476-ext-rew.smt2 rename to 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 similarity index 100% rename from test/regress/regress0/aufbv/bug349.smtv1.smt2 rename to test/regress/regress2/bug349.smtv1.smt2 diff --git a/test/regress/regress0/bug374.smtv1.smt2 b/test/regress/regress2/bug374.smtv1.smt2 similarity index 99% rename from test/regress/regress0/bug374.smtv1.smt2 rename to 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 similarity index 100% rename from test/regress/regress4/hole10.cvc rename to 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 similarity index 100% rename from test/regress/regress0/strings/bidir_star.smt2 rename to 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 similarity index 100% rename from test/regress/regress2/sygus/DRAGON_1.lus.sy rename to 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 similarity index 100% rename from test/regress/regress0/uf/PEQ018_size4.smtv1.smt2 rename to 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 similarity index 100% rename from test/regress/regress0/aufbv/wchains010ue.smtv1.smt2 rename to 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 similarity index 100% rename from test/regress/regress2/auflia-fuzz06.smtv1.smt2 rename to test/regress/regress3/auflia-fuzz06.smtv1.smt2 diff --git a/test/regress/regress0/bug2.smtv1.smt2 b/test/regress/regress3/bug2.smtv1.smt2 similarity index 100% rename from test/regress/regress0/bug2.smtv1.smt2 rename to 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 similarity index 100% rename from test/regress/regress0/bv/core/ext_con_004_001_1024.smtv1.smt2 rename to 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 similarity index 100% rename from test/regress/regress0/bv/fuzz15.smtv1.smt2 rename to 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 similarity index 100% rename from test/regress/regress0/bv/fuzz16.smtv1.smt2 rename to 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 similarity index 100% rename from test/regress/regress0/bv/fuzz17.smtv1.smt2 rename to test/regress/regress3/bv-fuzz17.smtv1.smt2 diff --git a/test/regress/regress1/sygus/cegisunif-depth1.sy b/test/regress/regress3/cegisunif-depth1.sy similarity index 100% rename from test/regress/regress1/sygus/cegisunif-depth1.sy rename to 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 similarity index 100% rename from test/regress/regress0/decision/uflia-xs-09-16-3-4-1-5.smtv1.smt2 rename to 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 similarity index 100% rename from test/regress/regress0/decision/wchains010ue.smtv1.smt2 rename to test/regress/regress3/decision-wchains010ue.smtv1.smt2 diff --git a/test/regress/regress1/sygus/interpol2.smt2 b/test/regress/regress3/interpol2.smt2 similarity index 100% rename from test/regress/regress1/sygus/interpol2.smt2 rename to 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 similarity index 100% rename from test/regress/regress2/sygus/inv_gen_n_c11.sy rename to 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 similarity index 100% rename from test/regress/regress2/arith/lpsat-goal-9.smt2 rename to 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 similarity index 100% rename from test/regress/regress2/sygus/nia-max-square.sy rename to test/regress/regress3/nia-max-square.sy diff --git a/test/regress/regress2/sygus/policyM.sy b/test/regress/regress3/policyM.sy similarity index 100% rename from test/regress/regress2/sygus/policyM.sy rename to test/regress/regress3/policyM.sy diff --git a/test/regress/regress1/rr-verify/regex.sy b/test/regress/regress3/regex-rrv.sy similarity index 100% rename from test/regress/regress1/rr-verify/regex.sy rename to 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 similarity index 100% rename from test/regress/regress2/quantifiers/specsharp-WindowsCard.15.RTE.Terminate_System.Int32.smt2 rename to 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 similarity index 100% rename from test/regress/regress1/sygus/unbdd_inv_gen_ex7.sy rename to 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 similarity index 100% rename from test/regress/regress1/sygus/unifpi-solve-car_1.lus.sy rename to test/regress/regress3/unifpi-solve-car_1.lus.sy diff --git a/test/regress/regress2/sygus/vcb.sy b/test/regress/regress3/vcb.sy similarity index 100% rename from test/regress/regress2/sygus/vcb.sy rename to test/regress/regress3/vcb.sy diff --git a/test/regress/regress1/auflia/bug337.smt2 b/test/regress/regress4/bug337.smt2 similarity index 100% rename from test/regress/regress1/auflia/bug337.smt2 rename to test/regress/regress4/bug337.smt2 diff --git a/test/regress/regress2/bug396.smt2 b/test/regress/regress4/bug396.smt2 similarity index 100% rename from test/regress/regress2/bug396.smt2 rename to 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 similarity index 100% rename from test/regress/regress0/lemmas/fischer3-mutex-16.smtv1.smt2 rename to test/regress/regress4/fischer3-mutex-16.smtv1.smt2 diff --git a/test/regress/regress3/issue2429.smt2 b/test/regress/regress4/issue2429.smt2 similarity index 100% rename from test/regress/regress3/issue2429.smt2 rename to test/regress/regress4/issue2429.smt2 diff --git a/test/regress/regress2/arith/miplib-pp08a-3000.smt2 b/test/regress/regress4/miplib-pp08a-3000.smt2 similarity index 100% rename from test/regress/regress2/arith/miplib-pp08a-3000.smt2 rename to 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 similarity index 100% rename from test/regress/regress0/arith/miplib-pp08a-3000.smtv1.smt2 rename to 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 similarity index 100% rename from test/regress/regress3/pp-regfile.smtv1.smt2 rename to 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 similarity index 100% rename from test/regress/regress1/sets/infinite-type/sets-card-neg-mem-union-2.smt2 rename to 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 similarity index 100% rename from test/regress/regress3/strings/unsat-circ-reduce.smt2 rename to 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 similarity index 100% rename from test/regress/regress2/xs-11-20-5-2-5-3.smt2 rename to 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 similarity index 100% rename from test/regress/regress2/xs-11-20-5-2-5-3.smtv1.smt2 rename to test/regress/regress4/xs-11-20-5-2-5-3.smtv1.smt2 -- 2.30.2