+#####################
+## CMakeLists.txt
+## Top contributors (to current version):
+## Aina Niemetz, Mathias Preiner, Andrew Reynolds
+## This file is part of the CVC4 project.
+## Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
+## in the top-level source directory and their institutional affiliations.
+## All rights reserved. See the file COPYING in the top-level source
+## directory for licensing information.
+##
#-----------------------------------------------------------------------------#
# Regression level 0 tests
regress0/arith/issue3413.smt2
regress0/arith/issue3480.smt2
regress0/arith/issue3683.smt2
+ regress0/arith/issue4367.smt2
+ regress0/arith/issue4525.smt2
+ regress0/arith/issue5219-conflict-rewrite.smt2
regress0/arith/ite-lift.smt2
regress0/arith/leq.01.smtv1.smt2
regress0/arith/miplib.cvc
regress0/arrays/bug272.minimized.smtv1.smt2
regress0/arrays/bug272.smtv1.smt2
regress0/arrays/bug3020.smt2
+ regress0/arrays/bug4957.smt2
regress0/arrays/bug637.delta.smt2
regress0/arrays/constarr.cvc
regress0/arrays/constarr.smt2
regress0/bv/bv-abstr-bug2.smt2
regress0/bv/bv-int-collapse1.smt2
regress0/bv/bv-int-collapse2.smt2
- regress0/bv/bv-options1.smt2
- regress0/bv/bv-options2.smt2
- regress0/bv/bv-options3.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_int2.smt2
- regress0/bv/bv_to_int_bvmul1.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_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_elim_err.smt2
regress0/bv/bv_to_int_zext.smt2
- regress0/bv/bv_to_int_bitwise.smt2
- regress0/bv/bvuf_to_intuf.smt2
- regress0/bv/bvuf_to_intuf_smtlib.smt2
- regress0/bv/bvuf_to_intuf_sorts.smt2
regress0/bv/bv2nat-ground-c.smt2
regress0/bv/bv2nat-simp-range.smt2
regress0/bv/bvmul-pow2-only.smt2
regress0/bv/core/slice-18.smtv1.smt2
regress0/bv/core/slice-19.smtv1.smt2
regress0/bv/core/slice-20.smtv1.smt2
+ regress0/bv/div_mod.cvc
regress0/bv/divtest_2_5.smt2
regress0/bv/divtest_2_6.smt2
regress0/bv/eager-inc-cadical.smt2
regress0/bv/fuzz40.smtv1.smt2
regress0/bv/fuzz41.smtv1.smt2
regress0/bv/issue3621.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/mul-neg-unsat.smt2
regress0/bv/mul-negpow2.smt2
regress0/bv/mult-pow2-negative.smt2
+ regress0/bv/pr4993-bvugt-bvurem-a.smt2
+ regress0/bv/pr4993-bvugt-bvurem-b.smt2
regress0/bv/sizecheck.cvc
regress0/bv/smtcompbug.smtv1.smt2
regress0/bv/test-bv_intro_pow2.smt2
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/datatype3.cvc
regress0/datatypes/datatype4.cvc
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/issue1433.smt2
regress0/datatypes/issue2838.cvc
regress0/datatypes/jsat-2.6.smt2
+ regress0/datatypes/list-bool.smt2
regress0/datatypes/model-subterms-min.smt2
regress0/datatypes/mutually-recursive.cvc
regress0/datatypes/pair-bool-bool.cvc
regress0/datatypes/pair-real-bool.smt2
+ regress0/datatypes/parametric-alt-list.cvc
regress0/datatypes/rec1.cvc
regress0/datatypes/rec2.cvc
regress0/datatypes/rec4.cvc
regress0/distinct.smtv1.smt2
regress0/dump-unsat-core-full.smt2
regress0/simple-dump-model.smt2
+ regress0/eqrange1.smt2
+ regress0/eqrange2.smt2
+ regress0/eqrange3.smt2
regress0/expect/scrub.01.smtv1.smt2
regress0/expect/scrub.03.smt2
regress0/expect/scrub.06.cvc
regress0/fmf/fmf-strange-bounds-2.smt2
regress0/fmf/forall_unit_data2.smt2
regress0/fmf/issue3661-ccard-dec.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/quant_real_univ.cvc
regress0/fp/down-cast-RNA.smt2
regress0/fp/ext-rew-test.smt2
regress0/fp/issue3536.smt2
+ regress0/fp/issue3619.smt2
regress0/fp/issue4277-assign-func.smt2
regress0/fp/rti_3_5_bug.smt2
regress0/fp/rti_3_5_bug_report.smt2
regress0/ho/ho-matching-nested-app.smt2
regress0/ho/ho-std-fmf.smt2
regress0/ho/hoa0008.smt2
+ regress0/ho/issue4477.smt2
+ regress0/ho/issue4990-care-graph.smt2
+ regress0/ho/issue5233-part1-usort-owner.smt2
regress0/ho/ite-apply-eq.smt2
regress0/ho/lambda-equality-non-canon.smt2
regress0/ho/match-middle.smt2
regress0/issue1063-overloading-dt-sel.smt2
regress0/issue2832-qualId.smt2
regress0/issue4010-sort-inf-var.smt2
+ regress0/issue4469-unc-no-reuse-var.smt2
+ regress0/issue5144-resetAssertions.smt2
regress0/ite.cvc
regress0/ite2.smt2
regress0/ite3.smt2
regress0/nl/very-easy-sat.smt2
regress0/nl/very-simple-unsat.smt2
regress0/options/invalid_dump.smt2
- regress0/options/invalid_option_inc_proofs.smt2
regress0/opt-abd-no-use.smt2
regress0/parallel-let.smt2
regress0/parser/as.smt2
regress0/parser/bv_arity_smt2.6.smt2
regress0/parser/bv_nat.smt2
- regress0/parser/choice.cvc
- regress0/parser/choice.smt2
regress0/parser/constraint.smt2
regress0/parser/declarefun-emptyset-uf.smt2
regress0/parser/force_logic_set_logic.smt2
regress0/parser/force_logic_success.smt2
+ regress0/parser/issue5163.smt2
regress0/parser/shadow_fun_symbol_all.smt2
regress0/parser/shadow_fun_symbol_nirat.smt2
regress0/parser/strings20.smt2
regress0/preprocess/preprocess_13.cvc
regress0/preprocess/preprocess_14.cvc
regress0/preprocess/preprocess_15.cvc
+ regress0/print_define_fun_internal.smt2
regress0/print_lambda.cvc
regress0/print_model.cvc
regress0/printer/bv_consts_bin.smt2
regress0/printer/let_shadowing.smt2
regress0/printer/symbol_starting_w_digit.smt2
regress0/printer/tuples_and_records.cvc
- regress0/proof_no_support.smt2
regress0/push-pop/boolean/fuzz_12.smt2
regress0/push-pop/boolean/fuzz_13.smt2
regress0/push-pop/boolean/fuzz_14.smt2
regress0/quantifiers/issue2035.smt2
regress0/quantifiers/issue3655.smt2
regress0/quantifiers/issue4086-infs.smt2
+ regress0/quantifiers/issue4275-qcf-cegqi-rep.smt2
+ regress0/quantifiers/issue4437-unc-quant.smt2
+ regress0/quantifiers/issue4476-ext-rew.smt2
+ regress0/quantifiers/issue4576.smt2
regress0/quantifiers/lra-triv-gn.smt2
regress0/quantifiers/macros-int-real.smt2
regress0/quantifiers/macros-real-arg.smt2
regress0/quantifiers/qbv-test-invert-concat-1.smt2
regress0/quantifiers/qbv-test-invert-sign-extend.smt2
regress0/quantifiers/qcf-rel-dom-opt.smt2
+ regress0/quantifiers/quant-model-simplification.smt2
regress0/quantifiers/rew-to-scala.smt2
regress0/quantifiers/simp-len.smt2
regress0/quantifiers/simp-typ-test.smt2
+ regress0/quantifiers/sygus-inst-nia-psyco-060.smt2
+ regress0/quantifiers/sygus-inst-ufnia-sat-t3_rw1505.smt2
regress0/rec-fun-const-parse-bug.smt2
regress0/rels/addr_book_0.cvc
regress0/rels/atom_univ2.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_7.cvc
regress0/rels/rel_tc_8.cvc
regress0/rels/rel_tp_3_1.cvc
regress0/rels/rel_tp_join_0.cvc
regress0/sep/sep-01.smt2
regress0/sep/sep-plus1.smt2
regress0/sep/sep-simp-unsat-emp.smt2
+ regress0/sep/simple-080420-const-sets.smt2
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/seq-2var.smt2
+ regress0/seq/seq-ex1.smt2
+ regress0/seq/seq-ex2.smt2
+ regress0/seq/seq-ex3.smt2
+ regress0/seq/seq-ex4.smt2
+ regress0/seq/seq-ex5-dd.smt2
+ regress0/seq/seq-ex5.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-undef.smt2
+ regress0/seq/seq-rewrites.smt2
regress0/sets/abt-min.smt2
regress0/sets/abt-te-exh.smt2
regress0/sets/abt-te-exh2.smt2
regress0/simplification_bug2.smtv1.smt2
regress0/smallcnf.cvc
regress0/smt2output.smt2
+ regress0/smtlib/define-fun-rec-logic.smt2
regress0/smtlib/get-unsat-assumptions.smt2
regress0/smtlib/global-decls.smt2
regress0/smtlib/issue4028.smt2
regress0/smtlib/issue4077.smt2
regress0/smtlib/issue4151.smt2
+ regress0/smtlib/issue4552.smt2
+ regress0/smtlib/issue4866.smt2
regress0/smtlib/reason-unknown.smt2
regress0/smtlib/reset.smt2
regress0/smtlib/reset-assertions1.smt2
regress0/strings/issue3497.smt2
regress0/strings/issue3657-evalLeq.smt2
regress0/strings/issue4070.smt2
+ regress0/strings/issue4376.smt2
+ regress0/strings/issue4662-consume-nterm.smt2
+ regress0/strings/issue4674-recomp-nf.smt2
+ regress0/strings/issue4820.smt2
+ regress0/strings/issue4915.smt2
+ regress0/strings/issue5090.smt2
regress0/strings/itos-entail.smt2
regress0/strings/large-model.smt2
regress0/strings/leadingzero001.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-in-rewrite.smt2
regress0/strings/re-syntax.smt2
regress0/strings/re_diff.smt2
regress0/strings/regexp-native-simple.cvc
regress0/sygus/issue3356-syg-inf-usort.smt2
regress0/sygus/issue3624.sy
regress0/sygus/issue3645-grammar-sets.smt2
+ regress0/sygus/issue4383-cache-fv-id.sy
+ regress0/sygus/issue4790-dtd.sy
regress0/sygus/let-ringer.sy
regress0/sygus/let-simp.sy
regress0/sygus/no-logic.sy
regress0/sygus/parse-bv-let.sy
regress0/sygus/pbe-pred-contra.sy
regress0/sygus/pLTL-sygus-syntax-err.sy
+ regress0/sygus/print-debug.sy
regress0/sygus/print-define-fun.sy
regress0/sygus/real-si-all.sy
regress0/sygus/sygus-no-wf.sy
regress0/uf/euf_simp13.smtv1.smt2
regress0/uf/iso_brn001.smtv1.smt2
regress0/uf/issue2947.smt2
+ regress0/uf/issue4446.smt2
regress0/uf/pred.smtv1.smt2
regress0/uf/simple.01.cvc
regress0/uf/simple.02.cvc
regress0/uflra/simple.02.cvc
regress0/uflra/simple.03.cvc
regress0/uflra/simple.04.cvc
+ regress0/unconstrained/4481.smt2
regress0/unconstrained/arith.smt2
regress0/unconstrained/arith3.smt2
regress0/unconstrained/arith4.smt2
regress0/unconstrained/bvult5.smt2
regress0/unconstrained/geq.smt2
regress0/unconstrained/gt.smt2
+ regress0/unconstrained/issue4644.smt2
regress0/unconstrained/ite.smt2
regress0/unconstrained/leq.smt2
regress0/unconstrained/lt.smt2
# Regression level 1 tests
set(regress_1_tests
+ regress1/abduct-dt.smt2
regress1/arith/arith-int-004.cvc
regress1/arith/arith-int-011.cvc
regress1/arith/arith-int-012.cvc
regress1/arith/bug547.1.smt2
regress1/arith/bug716.0.smt2
regress1/arith/bug716.1.cvc
+ regress1/arith/bug716.2.cvc
regress1/arith/div.03.smt2
regress1/arith/div.06.smt2
regress1/arith/div.08.smt2
regress1/datatypes/issue3266-small.smt2
regress1/datatypes/issue-variant-dt-zero.smt2
regress1/datatypes/manos-model.smt2
+ regress1/datatypes/non-simple-rec.smt2
+ regress1/datatypes/non-simple-rec-mut-unsat.smt2
+ regress1/datatypes/non-simple-rec-param.smt2
regress1/decision/error3.smtv1.smt2
regress1/decision/quant-Arrays_Q1-noinfer.smt2
regress1/decision/quant-symmetric_unsat_7.smt2
regress1/fmf/issue3626.smt2
regress1/fmf/issue3689.smt2
regress1/fmf/issue4068-si-qf.smt2
+ regress1/fmf/issue4225-univ-fun.smt2
regress1/fmf/issue916-fmf-or.smt2
regress1/fmf/jasmin-cdt-crash.smt2
regress1/fmf/ko-bound-set.cvc
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
regress1/nl/exp1-lb.smt2
regress1/nl/exp_monotone.smt2
regress1/nl/factor_agg_s.smt2
+ regress1/nl/iand-native-1.smt2
+ regress1/nl/iand-native-2.smt2
regress1/nl/issue3300-approx-sqrt-witness.smt2
regress1/nl/issue3441.smt2
regress1/nl/issue3617.smt2
regress1/push-pop/fuzz_7.smt2
regress1/push-pop/fuzz_8.smt2
regress1/push-pop/fuzz_9.smt2
+ regress1/push-pop/model-unsound-ania.smt2
regress1/push-pop/quant-fun-proc-unmacro.smt2
regress1/push-pop/quant-fun-proc.smt2
regress1/quantifiers/006-cbqi-ite.smt2
regress1/quantifiers/anti-sk-simp.smt2
regress1/quantifiers/ari118-bv-2occ-x.smt2
regress1/quantifiers/arith-rec-fun.smt2
- regress1/quantifiers/arith-snorm.smt2
regress1/quantifiers/array-unsat-simp3.smt2
regress1/quantifiers/bi-artm-s.smt2
regress1/quantifiers/bignum_quant.smt2
regress1/quantifiers/dump-inst-i.smt2
regress1/quantifiers/dump-inst-proof.smt2
regress1/quantifiers/dump-inst.smt2
+ regress1/quantifiers/eqrange_ex_1.smt2
regress1/quantifiers/ext-ex-deq-trigger.smt2
regress1/quantifiers/extract-nproc.smt2
regress1/quantifiers/f993-loss-easy.smt2
regress1/quantifiers/issue4062-cegqi-aux.smt2
regress1/quantifiers/issue4243-prereg-inc.smt2
regress1/quantifiers/issue4290-cegqi-r.smt2
+ regress1/quantifiers/issue4620-erq-witness-unsound.smt2
+ regress1/quantifiers/issue4685-wrewrite.smt2
+ regress1/quantifiers/issue5019-cegqi-i.smt2
regress1/quantifiers/issue993.smt2
regress1/quantifiers/javafe.ast.StmtVec.009.smt2
regress1/quantifiers/lra-vts-inf.smt2
regress1/quantifiers/qcft-smtlib3dbc51.smt2
regress1/quantifiers/qe-partial.smt2
regress1/quantifiers/qe.smt2
+ regress1/quantifiers/qid.smt2
+ regress1/quantifiers/qid-debug-inst.smt2
regress1/quantifiers/quant-wf-int-ind.smt2
regress1/quantifiers/quaternion_ds1_symm_0428.fof.smt2
regress1/quantifiers/recfact.cvc
regress1/quantifiers/set-choice-koikonomou.cvc
regress1/quantifiers/set8.smt2
regress1/quantifiers/seu169+1.smt2
+ regress1/quantifiers/seq-solved-enum.smt2
+ regress1/quantifiers/seq-unsolved-ematch.smt2
regress1/quantifiers/small-pipeline-fixpoint-3.smt2
regress1/quantifiers/smtcomp-qbv-053118.smt2
regress1/quantifiers/smtlib384a03.smt2
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
regress1/sets/infinite-type/sets-card-int-1.smt2
regress1/sets/infinite-type/sets-card-int-2.smt2
regress1/sets/insert_invariant_37_2.smt2
+ regress1/sets/is_singleton1.smt2
regress1/sets/issue2568.smt2
regress1/sets/issue2904.smt2
+ regress1/sets/issue4391-card-lasso.smt2
regress1/sets/lemmabug-ListElts317minimized.smt2
regress1/sets/remove_check_free_31_6.smt2
regress1/sets/sets-disequal.smt2
regress1/strings/issue3272.smt2
regress1/strings/issue3357.smt2
regress1/strings/issue3657-unexpectedUnsatCVC4.smt2
+ regress1/strings/issue4379.smt2
+ regress1/strings/issue4608-re-derive.smt2
+ regress1/strings/issue4701_substr_splice.smt2
+ regress1/strings/issue4735.smt2
+ regress1/strings/issue4735_2.smt2
+ regress1/strings/issue4759-comp-delta.smt2
regress1/strings/kaluza-fl.smt2
regress1/strings/loop002.smt2
regress1/strings/loop003.smt2
regress1/strings/nterm-re-inter-sigma.smt2
regress1/strings/pierre150331.smt2
regress1/strings/policy_variable.smt2
+ regress1/strings/pre_ctn_no_skolem_share.smt2
regress1/strings/query4674.smt2
regress1/strings/query8485.smt2
regress1/strings/re-all-char-hard.smt2
regress1/strings/timeout-no-resp.smt2
regress1/strings/type002.smt2
regress1/strings/type003.smt2
+ regress1/strings/update-ex1.smt2
+ regress1/strings/update-ex2.smt2
regress1/strings/username_checker_min.smt2
regress1/sygus-abduct-ex1-grammar.smt2
regress1/sygus-abduct-test.smt2
regress1/sygus/dt-test-ns.sy
regress1/sygus/dup-op.sy
regress1/sygus/error1-dt.sy
+ regress1/sygus/eval-uc.sy
regress1/sygus/extract.sy
regress1/sygus/fast-enum-backtrack.sy
regress1/sygus/fg_polynomial3.sy
+ regress1/sygus/find_inv_eq_bvmul_4bit_withoutgrammar-v2.sy
regress1/sygus/find_sc_bvult_bvnot.sy
+ regress1/sygus/ground-ite-free-constant-si.sy
regress1/sygus/hd-01-d1-prog.sy
regress1/sygus/hd-19-d1-prog-dup-op.sy
regress1/sygus/hd-sdiv.sy
regress1/sygus/inv-example.sy
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
+ regress1/sygus/interpol_cosa_1.smt2
+ regress1/sygus/interpol_from_pono_1.smt2
+ regress1/sygus/interpol_from_pono_2.smt2
regress1/sygus/issue2914.sy
regress1/sygus/issue2935.sy
regress1/sygus/issue3199.smt2
regress1/sygus/rec-fun-while-infinite.sy
regress1/sygus/re-concat.sy
regress1/sygus/repair-const-rl.sy
+ regress1/sygus/replicate-mod.sy
+ regress1/sygus/rex-strings-alarm.sy
regress1/sygus/sets-pred-test.sy
regress1/sygus/simple-regexp.sy
regress1/sygus/stopwatch-bt.sy
regress2/GEO123+1.minimized.smt2
regress2/arith/abz5_1400.smtv1.smt2
regress2/arith/lpsat-goal-9.smt2
- regress2/arith/prp-13-24.smt2
regress2/arith/pursuit-safety-11.smtv1.smt2
regress2/arith/pursuit-safety-12.smtv1.smt2
regress2/arith/sc-7.base.cvc.smtv1.smt2
regress2/bug674.smt2
regress2/bug765.smt2
regress2/bug812.smt2
+ regress2/bv/opStructure_MBA_6.scrambled.min.smt2
+ regress2/bv_to_int2.smt2
+ regress2/bv_to_int_5095.smt2
+ regress2/bv_to_int_5095_2.smt2
regress2/bv_to_int_ashr.smt2
+ regress2/bv_to_int_bitwise.smt2
+ regress2/bv_to_int_bvmul1.smt2
+ regress2/bv_to_int_bvuf_to_intuf_smtlib.smt2
+ regress2/bv_to_int_inc1.smt2
regress2/bv_to_int_mask_array_1.smt2
regress2/bv_to_int_mask_array_2.smt2
+ regress2/bv_to_int_mask_array_3.smt2
regress2/bv_to_int_shifts.smt2
regress2/error0.smt2
regress2/error1.smtv1.smt2
- regress2/friedman_n4_i5.smtv1.smt2
regress2/fuzz_2.smtv1.smt2
regress2/hash_sat_06_19.smt2
regress2/hash_sat_07_17.smt2
regress2/quantifiers/specsharp-WindowsCard.15.RTE.Terminate_System.Int32.smt2
regress2/quantifiers/syn874-1.smt2
regress2/simplify.javafe.ast.ArrayInit.35_without_quantification2.smt2
+ regress2/strings/cmi-split-cm-fail.smt2
regress2/strings/cmu-dis-0707-3.smt2
regress2/strings/cmu-disagree-0707-dd.smt2
regress2/strings/cmu-prereg-fmf.smt2
regress2/strings/issue3203.smt2
regress2/strings/issue918.smt2
regress2/strings/non_termination_regular_expression6.smt2
- regress2/strings/norn-dis-0707-3.smt2
regress2/strings/range-perf.smt2
- regress2/strings/repl-repl.smt2
regress2/strings/repl-repl-i-no-push.smt2
+ regress2/strings/repl-repl.smt2
+ regress2/strings/replace_re.smt2
regress2/strings/replaceall-diffrange.smt2
regress2/strings/replaceall-len-c.smt2
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
# 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/bmc-ibm-1.smtv1.smt2
regress3/bmc-ibm-2.smtv1.smt2
regress3/bmc-ibm-5.smtv1.smt2
regress3/bmc-ibm-7.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_quant1.smt2
+ regress3/bv_to_int_quant2.smt2
+ regress3/bv_to_int_input_mouser_detect.c.smt2.minimized.smt2
regress3/eq_diamond14.smtv1.smt2
regress3/friedman_n6_i4.smtv1.smt2
regress3/hole9.cvc
regress3/incorrect1.smtv1.smt2
regress3/issue2429.smt2
regress3/issue4170.smt2
+ regress3/issue4714.smt2
regress3/pp-regfile.smtv1.smt2
regress3/qwh.35.405.shuffled-as.sat03-1651.smtv1.smt2
regress3/siegel-nl-bases.smt2
regress3/sixfuncs.sy
regress3/strings-any-term.sy
regress3/strings/extf_d_perf.smt2
+ regress3/strings/unsat-circ-reduce.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/mar2014/stacks0.hs.78.cvc4.smt2
regress0/sets/setel-eq.smt2
regress0/sets/sets-new.smt2
regress1/crash_burn_locusts.smt2
# regress1/ho/hoa0102.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
# issue1048-arrays-int-real.smt2 -- different errors on debug and production.
regress1/issue1048-arrays-int-real.smt2
# times out after update to tangent planes
regress1/nl/NAVIGATION2.smt2
# sat or unknown in different builds
regress1/nl/issue3307.smt2
+ # no longer support snorm option
+ regress1/quantifiers/arith-snorm.smt2
# ajreynol: different error messages on production and debug:
regress1/quantifiers/macro-subtype-param.smt2
# times out with competition build:
# 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
projects / cvc5.git / blobdiff