regress0/arrays/issue3813-massign-assert.smt2
regress0/arrays/issue3814.smt2
regress0/arrays/issue4927-unsat-cores.smt2
+ regress0/arrays/issue7596-define-array-uminus.smt2
regress0/arrays/swap_t1_np_nf_ai_00005_007.cvc.smtv1.smt2
regress0/arrays/x2.smtv1.smt2
regress0/arrays/x3.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_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_int1.smt2
regress0/bv/bv_to_int_zext.smt2
regress0/bv/bvcomp.cvc.smt2
regress0/bv/bvmul-pow2-only.smt2
regress0/bv/mult-pow2-negative.smt2
regress0/bv/pr4993-bvugt-bvurem-a.smt2
regress0/bv/pr4993-bvugt-bvurem-b.smt2
+ regress0/bv/proj-issue343.smt2
regress0/bv/reset-assertions-assert-input.smt2
regress0/bv/sizecheck.cvc.smt2
regress0/bv/smtcompbug.smtv1.smt2
regress0/datatypes/list-update.smt2
regress0/datatypes/list-update-sat.smt2
regress0/datatypes/model-subterms-min.smt2
+ regress0/datatypes/mutual-rec-param-dt.smt2
regress0/datatypes/mutually-recursive.cvc.smt2
regress0/datatypes/pair-bool-bool.cvc.smt2
regress0/datatypes/pair-real-bool.smt2
+ regress0/datatypes/par-updater-type-rule.smt2
regress0/datatypes/parametric-alt-list.cvc.smt2
+ regress0/datatypes/proj-issue172.smt2
regress0/datatypes/rec1.cvc.smt2
regress0/datatypes/rec2.cvc.smt2
regress0/datatypes/rec4.cvc.smt2
regress0/declare-fun-is-match.smt2
regress0/declare-funs.smt2
regress0/define-fun-model.smt2
+ regress0/difficulty-simple.smt2
+ regress0/difficulty-model-ex.smt2
regress0/distinct.smtv1.smt2
regress0/dump-unsat-core-full.smt2
regress0/echo.smt2
regress0/fp/issue5734.smt2
regress0/fp/issue6164.smt2
regress0/fp/issue7002.smt2
+ regress0/fp/issue7569.smt2
+ regress0/fp/proj-issue329-prereg-context.smt2
regress0/fp/rti_3_5_bug.smt2
regress0/fp/simple.smt2
regress0/fp/word-blast.smt2
regress0/ho/bug_nodbuilding_interpreted_SYO042^1.p
regress0/ho/cong-full-apply.smt2
regress0/ho/cong.smt2
+ regress0/ho/datatype-field-ho.smt2
regress0/ho/declare-fun-variants.smt2
regress0/ho/def-fun-flatten.smt2
regress0/ho/ext-finite-unsat.smt2
regress0/ho/issue6536.smt2
regress0/ho/ite-apply-eq.smt2
regress0/ho/lambda-equality-non-canon.smt2
+ regress0/ho/lazy-lambda-model.smt2
regress0/ho/match-middle.smt2
regress0/ho/modulo-func-equality.smt2
regress0/ho/qgu-fuzz-ho-1-dd.smt2
+ regress0/ho/qgu-fuzz-ho-2-dd-no-ext.smt2
regress0/ho/shadowing-defs.smt2
+ regress0/ho/simple-conf-lazy-lambda-lift.smt2
+ regress0/ho/simple-conf-lazy-lambda-lift-app.smt2
regress0/ho/simple-matching-partial.smt2
regress0/ho/simple-matching.smt2
regress0/ho/trans.smt2
regress0/nl/pow2-native-3.smt2
regress0/nl/pow2-pow.smt2
regress0/nl/pow2-pow-isabelle.smt2
+ regress0/nl/proj-issue-348.smt2
regress0/nl/real-as-int.smt2
regress0/nl/real-div-ufnra.smt2
regress0/nl/sin-cos-346-b-chunk-0169.smt2
regress0/nl/very-simple-unsat.smt2
regress0/opt-abd-no-use.smt2
regress0/options/ast-and-sexpr.smt2
+ regress0/options/didyoumean.smt2
+ regress0/options/help.smt2
regress0/options/interactive-mode.smt2
- regress0/options/invalid_dump.smt2
+ regress0/options/named_muted.smt2
regress0/options/set-after-init.smt2
regress0/options/set-and-get-options.smt2
regress0/options/statistics.smt2
regress0/parser/define_sort.smt2
regress0/parser/force_logic_set_logic.smt2
regress0/parser/force_logic_success.smt2
+ regress0/parser/get-model-sort-constructor.smt2
regress0/parser/issue5163.smt2
regress0/parser/issue6908-get-value-uc.smt2
regress0/parser/issue7274.smt2
regress0/parser/linear_arithmetic_err3.smt2
regress0/parser/named-attr-error.smt2
regress0/parser/named-attr.smt2
+ regress0/parser/proj-issue370-push-pop-global.smt2
+ regress0/parser/quoted-define-fun.smt2
regress0/parser/shadow_fun_symbol_all.smt2
regress0/parser/shadow_fun_symbol_nirat.smt2
regress0/parser/strings20.smt2
regress0/proofs/open-pf-rederivation.smt2
regress0/proofs/project-issue317-inc-sat-conflictlit.smt2
regress0/proofs/project-issue330-eqproof.smt2
+ regress0/proofs/proj-issue326-nl-bounds-check.smt2
+ regress0/proofs/proj-issue342-eager-checking-no-proof-checking.smt2
regress0/proofs/qgu-fuzz-1-bool-sat.smt2
regress0/proofs/qgu-fuzz-2-bool-chainres-checking.smt2
regress0/proofs/qgu-fuzz-3-chainres-checking.smt2
regress0/proofs/qgu-fuzz-4-bool-chainres-postprocessing-singleton.smt2
+ regress0/proofs/qgu-fuzz-5-bool-open-sat.smt2
regress0/proofs/scope.smt2
regress0/proofs/trust-subs-eq-open.smt2
regress0/push-pop/boolean/fuzz_12.smt2
regress0/rels/rel_tc_2_1.cvc.smt2
regress0/rels/rel_tc_3_1.cvc.smt2
regress0/rels/rel_tc_3.cvc.smt2
- regress0/rels/rel_tc_7.cvc.smt2
regress0/rels/rel_tc_8.cvc.smt2
regress0/rels/rel_tp_3_1.cvc.smt2
regress0/rels/rel_tp_join_0.cvc.smt2
regress0/seq/issue5665-invalid-model.smt2
regress0/seq/issue6337-seq.smt2
regress0/seq/len_simplify.smt2
+ regress0/seq/proj-issue340.smt2
regress0/seq/seq-2var.smt2
regress0/seq/seq-ex1.smt2
regress0/seq/seq-ex2.smt2
regress0/strings/norn-simp-rew.smt2
regress0/strings/parser-syms.cvc.smt2
regress0/strings/proj-issue316-regexp-ite.smt2
+ regress0/strings/proj-issue390-update-rev-rewrite.smt2
regress0/strings/re_diff.smt2
regress0/strings/re-in-rewrite.smt2
regress0/strings/re-syntax.smt2
regress0/sygus/General_plus10.sy
regress0/sygus/hd-05-d1-prog-nogrammar.sy
regress0/sygus/ho-occ-synth-fun.sy
+ regress0/sygus/incremental-modify-ex.sy
regress0/sygus/inv-different-var-order.sy
regress0/sygus/issue3356-syg-inf-usort.smt2
regress0/sygus/issue3624.sy
regress0/sygus/pLTL-sygus-syntax-err.sy
regress0/sygus/print-debug.sy
regress0/sygus/print-define-fun.sy
+ regress0/sygus/print-grammar.sy
regress0/sygus/real-si-all.sy
regress0/sygus/setFeature.sy
regress0/sygus/strings-unconstrained.sy
# Regression level 1 tests
set(regress_1_tests
- regress1/abduction/sygus-abduct-test-user.smt2
- regress1/abduction/issue5848-4.smt2
+ regress1/abduction/abduction_1255.corecstrs.readable.smt2
+ regress1/abduction/abduction_streq.readable.smt2
+ regress1/abduction/abduction-no-pbe-sym-break.smt2
+ regress1/abduction/abduct-dt.smt2
+ regress1/abduction/abd-real-const.smt2
+ regress1/abduction/abd-simple-conj-4.smt2
regress1/abduction/issue5848-2.smt2
+ regress1/abduction/issue5848-3-trivial-no-abduct.smt2
+ regress1/abduction/issue5848-4.smt2
regress1/abduction/issue5848.smt2
regress1/abduction/issue6605-1.smt2
- regress1/abduction/abduct-dt.smt2
- regress1/abduction/sygus-abduct-test-ccore.smt2
+ regress1/abduction/simple-incremental.smt2
+ regress1/abduction/simple-incremental-push-pop.smt2
+ regress1/abduction/sygus-abduct-ex1-grammar.smt2
regress1/abduction/sygus-abduct-test.smt2
- regress1/abduction/abd-simple-conj-4.smt2
- regress1/abduction/abduction_streq.readable.smt2
- regress1/abduction/yoni-true-sol.smt2
+ regress1/abduction/sygus-abduct-test-ccore.smt2
+ regress1/abduction/sygus-abduct-test-user.smt2
regress1/abduction/uf-abduct.smt2
- regress1/abduction/abduction_1255.corecstrs.readable.smt2
- regress1/abduction/abduction-no-pbe-sym-break.smt2
- regress1/abduction/issue5848-3-trivial-no-abduct.smt2
- regress1/abduction/sygus-abduct-ex1-grammar.smt2
+ regress1/abduction/yoni-true-sol.smt2
regress1/arith/arith-brab-test.smt2
regress1/arith/arith-int-004.cvc.smt2
regress1/arith/arith-int-011.cvc.smt2
regress1/bug681.smt2
regress1/bug694-Unapply1.scala-0.smt2
regress1/bug800.smt2
+ regress1/bags/bags-of-bags-subtypes.smt2
+ regress1/bags/card1.smt2
+ regress1/bags/card2.smt2
+ regress1/bags/choose1.smt2
+ regress1/bags/choose2.smt2
+ regress1/bags/choose3.smt2
+ regress1/bags/choose4.smt2
regress1/bags/difference_remove1.smt2
regress1/bags/disequality.smt2
regress1/bags/duplicate_removal1.smt2
regress1/bags/duplicate_removal2.smt2
regress1/bags/emptybag1.smt2
+ regress1/bags/fold1.smt2
regress1/bags/fuzzy1.smt2
regress1/bags/fuzzy2.smt2
+ regress1/bags/fuzzy3.smt2
+ regress1/bags/fuzzy4.smt2
+ regress1/bags/fuzzy5.smt2
+ regress1/bags/fuzzy6.smt2
regress1/bags/intersection_min1.smt2
regress1/bags/intersection_min2.smt2
regress1/bags/issue5759.smt2
regress1/bags/map1.smt2
regress1/bags/map2.smt2
regress1/bags/map3.smt2
+ regress1/bags/map-lazy-lam.smt2
+ regress1/bags/murxla1.smt2
+ regress1/bags/murxla2.smt2
+ regress1/bags/murxla3.smt2
regress1/bags/subbag1.smt2
regress1/bags/subbag2.smt2
regress1/bags/union_disjoint.smt2
regress1/bv/issue3776.smt2
regress1/bv/issue3958.smt2
regress1/bv/min-pp-rewrite-error.smt2
- regress1/bv/test-bv-abstraction.smt2
regress1/bv/unsound1.smt2
regress1/bvdiv2.smt2
regress1/cee-bug0909-dd-scope.smt2
regress1/datatypes/dt-color-2.6.smt2
regress1/datatypes/dt-param-card4-unsat.smt2
regress1/datatypes/issue3266-small.smt2
+ regress1/datatypes/issue4851-cdt-model.smt2
regress1/datatypes/issue-variant-dt-zero.smt2
regress1/datatypes/manos-model.smt2
regress1/datatypes/non-simple-rec.smt2
regress1/decision/wishue149-2.smt2
regress1/decision/wishue149-3.smt2
regress1/decision/wishue160.smt2
+ regress1/difficulty-polarity.smt2
regress1/errorcrash.smt2
regress1/fp/fp_to_real.smt2
regress1/fp/rti_3_5_bug_report.smt2
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/bug_freevar_PHI004^4-delta.smt2
regress1/ho/bound_var_bug.p
regress1/ho/fta0328.lfho.p
+ regress1/ho/ho-fun-sharing-dd.smt2
regress1/ho/issue3136-fconst-bool-bool.smt2
regress1/ho/issue4065-no-rep.smt2
regress1/ho/issue4092-sinf.smt2
regress1/nl/nl-help-unsat-quant.smt2
regress1/nl/nl-unk-quant.smt2
regress1/nl/nl_uf_lalt.smt2
+ regress1/nl/nra-cad-performance.smt2
regress1/nl/ones.smt2
regress1/nl/pinto-model-core-ni.smt2
regress1/nl/poly-1025.smt2
+ regress1/nl/proj-365-is-int-pi.smt2
regress1/nl/quant-nl.smt2
regress1/nl/red-exp.smt2
regress1/nl/rewriting-sums.smt2
regress1/nl/tan-rewrite2.smt2
regress1/nl/zero-subset.smt2
regress1/non-fatal-errors.smt2
+ regress1/proj-issue175.smt2
regress1/proof00.smt2
regress1/proofs/issue6625-unsat-core-proofs.smt2
regress1/proofs/macro-res-exp-crowding-lit-inside-unit.smt2
regress1/proofs/qgu-fuzz-arrays-1-dd-te-auto.smt2
regress1/proofs/quant-alpha-eq.smt2
regress1/proofs/sat-trivial-cycle.smt2
+ regress1/proofs/str-ovf-dd.smt2
regress1/proofs/unsat-cores-proofs.smt2
regress1/push-pop/arith_lra_01.smt2
regress1/push-pop/arith_lra_02.smt2
regress1/quantifiers/issue4433-nqe.smt2
regress1/quantifiers/issue4620-erq-witness-unsound.smt2
regress1/quantifiers/issue4685-wrewrite.smt2
+ regress1/quantifiers/issue4813-qe-quant.smt2
regress1/quantifiers/issue4849-nqe.smt2
regress1/quantifiers/issue5019-cegqi-i.smt2
+ regress1/quantifiers/issue5278-ext-rewrite-rec.smt2
regress1/quantifiers/issue5279-nqe.smt2
regress1/quantifiers/issue5288-vts-real-int.smt2
regress1/quantifiers/issue5365-nqe.smt2
regress1/quantifiers/issue6775-vts-int.smt2
regress1/quantifiers/issue6845-nl-lemma-tc.smt2
regress1/quantifiers/issue7385-sygus-inst-i.smt2
+ regress1/quantifiers/issue7537-cegqi-comp-types.smt2
regress1/quantifiers/issue993.smt2
regress1/quantifiers/javafe.ast.StmtVec.009.smt2
regress1/quantifiers/lia-witness-div-pp.smt2
regress1/quantifiers/stream-x2014-09-18-unsat.smt2
regress1/quantifiers/sygus-infer-nested.smt2
regress1/quantifiers/sygus-inst-nia-psyco-060.smt2
- regress1/quantifiers/sygus-inst-ufnia-sat-t3_rw1505.smt2
regress1/quantifiers/symmetric_unsat_7.smt2
regress1/quantifiers/tpp-unit-fail-qbv.smt2
regress1/quantifiers/var-eq-trigger.smt2
regress1/rels/joinImg_2_1.cvc.smt2
regress1/rels/prod-mod-eq.cvc.smt2
regress1/rels/prod-mod-eq2.cvc.smt2
+ regress1/rels/qgu-fuzz-relations-2.smt2
+ regress1/rels/qgu-fuzz-relations-3-upwards.smt2
regress1/rels/rel_complex_3.cvc.smt2
regress1/rels/rel_complex_4.cvc.smt2
regress1/rels/rel_complex_5.cvc.smt2
regress1/sets/issue5342_difference_version.smt2
regress1/sets/issue5942-witness.smt2
regress1/sets/lemmabug-ListElts317minimized.smt2
+ regress1/sets/proj-issue164.smt2
+ regress1/sets/proj-issue178.smt2
regress1/sets/remove_check_free_31_6.smt2
regress1/sets/sets-disequal.smt2
regress1/sets/sets-tuple-poly.cvc.smt2
regress1/strings/issue6777-seq-nth-eval-cm.smt2
regress1/strings/issue6913.smt2
regress1/strings/issue6973-dup-lemma-conc.smt2
+ regress1/strings/issue7677-test-const-rv.smt2
regress1/strings/kaluza-fl.smt2
regress1/strings/loop002.smt2
regress1/strings/loop003.smt2
regress1/strings/policy_variable.smt2
regress1/strings/pre_ctn_no_skolem_share.smt2
regress1/strings/proj254-re-elim-agg.smt2
+ regress1/strings/proj-issue331.smt2
regress1/strings/query4674.smt2
regress1/strings/query8485.smt2
regress1/strings/re-all-char-hard.smt2
regress1/sygus/icfp_14_12_diff_types.sy
regress1/sygus/icfp_28_10.sy
regress1/sygus/icfp_easy-ite.sy
+ regress1/sygus/incremental-stream-ex.sy
regress1/sygus/int-any-const.sy
regress1/sygus/inv-example.sy
regress1/sygus/inv-missed-sol-true.sy
regress1/sygus/phone-1-long.sy
regress1/sygus/planning-unif.sy
regress1/sygus/process-10-vars.sy
+ regress1/sygus/proj-issue181.smt2
+ regress1/sygus/proj-issue183.smt2
+ regress1/sygus/proj-issue185.smt2
regress1/sygus/pLTL_5_trace.sy
regress1/sygus/qe.sy
regress1/sygus/qf_abv.smt2
+ regress1/sygus/rand_const.sy
+ regress1/sygus/rand_p_0.sy
+ regress1/sygus/rand_p_1.sy
regress1/sygus/real-any-const.sy
regress1/sygus/real-grammar.sy
regress1/sygus/rec-fun-swap.sy
regress2/bv_to_int_bvuf_to_intuf_smtlib.smt2
regress2/bv_to_int_bvmul1.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/bv_to_int_quantifiers_bvand.smt2
regress2/error1.smtv1.smt2
regress2/fp/issue7056.smt2
regress2/fuzz_2.smtv1.smt2
regress2/strings/replaceall-diffrange.smt2
regress2/strings/replaceall-len-c.smt2
regress2/strings/small-1.smt2
- regress2/strings/strings-alpha-card-129.smt2
+ regress2/strings/strings-alpha-card-65.smt2
regress2/strings/update-ex3.smt2
regress2/strings/update-ex4-seq.smt2
regress2/sygus/MPwL_d1s3.sy
regress0/auflia/fuzz01.smtv1.smt2
###
regress0/bv/test00.smtv1.smt2
+ # timeout after fixing upwards closure for relations
+ regress0/rels/rel_tc_7.cvc.smt2
# timeout after changes to equality rewriting policy in strings
regress0/strings/quad-028-2-2-unsat.smt2
# FIXME #1649
regress0/tptp/SYN075+1.p
regress0/uf/iso_icl_repgen004.smtv1.smt2
###
+ # takes around 30 sec
+ regress1/bags/fold2.smt2
regress1/bug472.smt2
regress1/datatypes/non-simple-rec-set.smt2
# results in an assertion failure (see issue #1650).
# ajreynol: different error messages on production and debug:
regress1/quantifiers/subtype-param-unk.smt2
regress1/quantifiers/subtype-param.smt2
+ # timeout after changes to theory preprocessing, note is non-linear and does not involve sygus-inst
+ regress1/quantifiers/sygus-inst-ufnia-sat-t3_rw1505.smt2
###
regress1/rels/garbage_collect.cvc.smt2
regress1/sets/setofsets-disequal.smt2
# previously sygus inference did not apply, now (correctly) times out
regress1/sygus/issue3498.smt2
regress2/arith/miplib-opt1217--27.smt2
+ # times out after #7345
+ regress2/bv_to_int_mask_array_1.smt2
regress2/nl/dumortier-050317.smt2
# timeout on some builds after changes to justification heuristic
regress2/nl/nt-lemmas-bad.smt2
projects / cvc5.git / blobdiff