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/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/issue4990-care-graph.smt2
regress0/ho/issue5233-part1-usort-owner.smt2
regress0/ho/issue5371.smt2
+ regress0/ho/issue5741-1-cg-model.smt2
+ regress0/ho/issue5741-3-cg-model.smt2
+ regress0/ho/issue5744-cg-model.smt2
regress0/ho/issue6526.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/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/set-after-init.smt2
regress0/options/set-and-get-options.smt2
regress0/options/statistics.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/preprocess/proj-issue305-circuit-prop-ite-c.smt2
regress0/preprocess/proj-issue305-circuit-prop-ite-d.smt2
regress0/preprocess/proj-issue309-circuit-prop-ite.smt2
+ regress0/preprocess/proj-issue332-circuit-prop-xor.smt2
regress0/print_define_fun_internal.smt2
regress0/print_lambda.cvc.smt2
regress0/print_model.cvc.smt2
regress0/printer/let_shadowing.smt2
regress0/printer/symbol_starting_w_digit.smt2
regress0/printer/tuples_and_records.cvc.smt2
+ regress0/proj-issue307-get-value-re.smt2
regress0/proofs/cyclic-ucp.smt2
regress0/proofs/issue277-circuit-propagator.smt2
regress0/proofs/lfsc-test-1.smt2
regress0/proofs/open-pf-if-unordered-iff.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/join-eq-u.cvc.smt2
regress0/rels/joinImg_0.cvc.smt2
regress0/rels/oneLoc_no_quant-int_0_1.cvc.smt2
+ regress0/rels/qgu-fuzz-relations-1.smt2
+ regress0/rels/qgu-fuzz-relations-1-dd.smt2
regress0/rels/rel_1tup_0.cvc.smt2
regress0/rels/rel_complex_0.cvc.smt2
regress0/rels/rel_complex_1.cvc.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-31.smt2
regress0/strings/norn-simp-rew.smt2
regress0/strings/parser-syms.cvc.smt2
+ regress0/strings/proj-issue316-regexp-ite.smt2
regress0/strings/re_diff.smt2
regress0/strings/re-in-rewrite.smt2
regress0/strings/re-syntax.smt2
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/abd-real-const.smt2
regress1/abduction/sygus-abduct-test-user.smt2
regress1/abduction/issue5848-4.smt2
regress1/abduction/issue5848-2.smt2
regress1/bug681.smt2
regress1/bug694-Unapply1.scala-0.smt2
regress1/bug800.smt2
+ regress1/bags/card1.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/map-lazy-lam.smt2
regress1/bags/map1.smt2
regress1/bags/map2.smt2
regress1/bags/map3.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/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/ho/issue4134-sinf.smt2
+ regress1/ho/issue4758.smt2
+ regress1/ho/issue5078-small.smt2
+ regress1/ho/issue5201-1.smt2
regress1/ho/issue5741-3.smt2
regress1/ho/NUM638^1.smt2
regress1/ho/NUM925^1.p
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/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/strings/issue6653-4-rre.smt2
regress1/strings/issue6653-rre.smt2
regress1/strings/issue6653-rre-small.smt2
+ regress1/strings/issue6766-re-elim-bv.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/nf-ff-contains-abs.smt2
regress1/strings/no-lazy-pp-quant.smt2
regress1/strings/non_termination_regular_expression4.smt2
+ regress1/strings/non-terminating-rewrite-aent.smt2
regress1/strings/norn-13.smt2
regress1/strings/norn-360.smt2
regress1/strings/norn-ab.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
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
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