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/cores/issue4971-2.smt2
regress0/cores/issue4971-3.smt2
regress0/cores/issue5079.smt2
+ regress0/cores/issue5234-uc-ua.smt2
regress0/cores/issue5238.smt2
regress0/cores/issue5902.smt2
regress0/cores/issue5908.smt2
regress0/datatypes/coda_simp_model.smt2
regress0/datatypes/conqueue-dt-enum-iloop.smt2
regress0/datatypes/data-nested-codata.smt2
+ regress0/datatypes/datatype-dump.cvc.smt2
regress0/datatypes/datatype.cvc.smt2
regress0/datatypes/datatype0.cvc.smt2
regress0/datatypes/datatype1.cvc.smt2
regress0/distinct.smtv1.smt2
regress0/dump-unsat-core-full.smt2
regress0/echo.smt2
+ regress0/eqrange0.smt2
regress0/eqrange1.smt2
regress0/eqrange2.smt2
regress0/eqrange3.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/invalid_dump.smt2
+ regress0/options/didyoumean.smt2
+ regress0/options/help.smt2
+ regress0/options/interactive-mode.smt2
regress0/options/set-after-init.smt2
regress0/options/set-and-get-options.smt2
regress0/options/statistics.smt2
regress0/options/stream-printing.smt2
+ regress0/options/version.smt2
regress0/parallel-let.smt2
regress0/parser/as.smt2
regress0/parser/bv_arity_smt2.6.smt2
regress0/parser/force_logic_set_logic.smt2
regress0/parser/force_logic_success.smt2
regress0/parser/issue5163.smt2
+ regress0/parser/issue6908-get-value-uc.smt2
regress0/parser/issue7274.smt2
regress0/parser/linear_arithmetic_err1.smt2
regress0/parser/linear_arithmetic_err2.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/preprocess_13.cvc.smt2
regress0/preprocess/preprocess_14.cvc.smt2
regress0/preprocess/preprocess_15.cvc.smt2
+ regress0/preprocess/proj-issue304-circuit-prop-xor.smt2
+ regress0/preprocess/proj-issue305-circuit-prop-ite-a.smt2
+ regress0/preprocess/proj-issue305-circuit-prop-ite-b.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-datatypes.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/push-pop/incremental-subst-bug.cvc.smt2
regress0/push-pop/issue1986.smt2
regress0/push-pop/issue2137.min.smt2
+ regress0/push-pop/issue6535-inc-solve.smt2
+ regress0/push-pop/issue7479-global-decls.smt2
regress0/push-pop/quant-fun-proc-unfd.smt2
regress0/push-pop/real-as-int-incremental.smt2
regress0/push-pop/simple_unsat_cores.smt2
regress0/quantifiers/issue4576.smt2
regress0/quantifiers/issue5645-dt-cm-spurious.smt2
regress0/quantifiers/issue5693-prenex.smt2
+ regress0/quantifiers/issue6475-rr-const.smt2
regress0/quantifiers/issue6603-dt-bool-cegqi.smt2
regress0/quantifiers/issue6838-qpdt.smt2
regress0/quantifiers/issue6996-trivial-elim.smt2
regress0/quantifiers/simp-len.smt2
regress0/quantifiers/simp-typ-test.smt2
regress0/quantifiers/ufnia-fv-delta.smt2
+ regress0/quantifiers/veqt-delta.smt2
regress0/rec-fun-const-parse-bug.smt2
regress0/rels/addr_book_0.cvc.smt2
regress0/rels/atom_univ2.cvc.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
regress0/unconstrained/geq.smt2
regress0/unconstrained/gt.smt2
regress0/unconstrained/issue4644.smt2
+ regress0/unconstrained/issue4656-bool-term-vars.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/abduction/abd-real-const.smt2
+ regress1/abduction/sygus-abduct-test-user.smt2
+ regress1/abduction/issue5848-4.smt2
+ regress1/abduction/issue5848-2.smt2
+ regress1/abduction/issue5848.smt2
+ regress1/abduction/issue6605-1.smt2
+ regress1/abduction/abduct-dt.smt2
+ regress1/abduction/sygus-abduct-test-ccore.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/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/arith/arith-brab-test.smt2
regress1/arith/arith-int-004.cvc.smt2
regress1/arith/arith-int-011.cvc.smt2
regress1/arith/issue3952-rew-eq.smt2
regress1/arith/issue4985-model-success.smt2
regress1/arith/issue4985b-model-success.smt2
+ regress1/arith/issue6774-sanity-int-model.smt2
+ regress1/arith/issue7252-arith-sanity.smt2
regress1/arith/issue789.smt2
regress1/arith/miplib3.cvc.smt2
regress1/arith/mod.02.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/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/constarr3.cvc.smt2
regress1/constarr3.smt2
regress1/cores/issue5604.smt2
+ regress1/cores/issue6988-arith-sanity.smt2
regress1/datatypes/acyclicity-sr-ground096.smt2
regress1/datatypes/cee-prs-small-dd2.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/issue4225-univ-fun.smt2
regress1/fmf/issue5738-dt-interp-finite.smt2
regress1/fmf/issue6690-re-enum.smt2
+ regress1/fmf/issue6744-2-unc-bool-var.smt2
+ regress1/fmf/issue6744-3-unc-bool-var.smt2
regress1/fmf/issue916-fmf-or.smt2
regress1/fmf/jasmin-cdt-crash.smt2
+ regress1/fmf/ko-bound-set.cvc.smt2
regress1/fmf/loopy_coda.smt2
regress1/fmf/lst-no-self-rev-exp.smt2
regress1/fmf/memory_model-R_cpp-dd.cvc.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/ho/soundness_fmf_SYO362^5-delta.p
regress1/model-blocker-simple.smt2
regress1/model-blocker-values.smt2
regress1/nl/approx-sqrt.smt2
+ regress1/nl/approx-sqrt-unsat.smt2
regress1/nl/arctan2-expdef.smt2
regress1/nl/arrowsmith-050317.smt2
regress1/nl/bad-050217.smt2
regress1/nl/issue3656.smt2
regress1/nl/issue3803-nl-check-model.smt2
regress1/nl/issue3955-ee-double-notify.smt2
- regress1/nl/issue3966-conf-coeff.smt2
+ regress1/nl/issue3966-conf-coeff.smt2
regress1/nl/issue4791-llr.smt2
regress1/nl/issue5372-2-no-m-presolve.smt2
+ regress1/nl/issue5660-mb-success.smt2
regress1/nl/issue5662-nl-tc.smt2
regress1/nl/issue5662-nl-tc-min.smt2
regress1/nl/metitarski-1025.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/proofs/issue6625-unsat-core-proofs.smt2
regress1/proofs/macro-res-exp-crowding-lit-inside-unit.smt2
regress1/proofs/macro-res-exp-singleton-after-elimCrowd.smt2
+ regress1/proofs/qgu-fuzz-1-strings-pp.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/cee-npnt-dd.smt2
regress1/quantifiers/cee-os-delta.smt2
regress1/quantifiers/cdt-0208-to.smt2
+ regress1/quantifiers/choice-move-delta-relt.smt2
regress1/quantifiers/const.cvc.smt2
regress1/quantifiers/constfunc.cvc.smt2
regress1/quantifiers/ddatv-delta2.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/issue5378-witness.smt2
regress1/quantifiers/issue5469-aext.smt2
regress1/quantifiers/issue5506-qe.smt2
regress1/quantifiers/issue5507-qe.smt2
regress1/quantifiers/issue5658-qe.smt2
+ regress1/quantifiers/issue5735-subtypes.smt2
+ regress1/quantifiers/issue5735-2-subtypes.smt2
regress1/quantifiers/issue5766-wrong-sel-trigger.smt2
regress1/quantifiers/issue5899-qe.smt2
+ regress1/quantifiers/issue6607-witness-te.smt2
+ regress1/quantifiers/issue6638-sygus-inst.smt2
+ regress1/quantifiers/issue6642-em-types.smt2
regress1/quantifiers/issue6699-nc-shadow.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/quaternion_ds1_symm_0428.fof.smt2
regress1/quantifiers/qs-has-term.smt2
regress1/quantifiers/recfact.cvc.smt2
+ regress1/quantifiers/rel-trigger-unusable.smt2
regress1/quantifiers/repair-const-nterm.smt2
regress1/quantifiers/rew-to-0211-dd.smt2
regress1/quantifiers/ricart-agrawala6.smt2
regress1/quantifiers/set-choice-koikonomou.cvc.smt2
+ regress1/quantifiers/set3.smt2
regress1/quantifiers/set8.smt2
regress1/quantifiers/seu169+1.smt2
regress1/quantifiers/seq-solved-enum.smt2
regress1/quantifiers/smtlib46f14a.smt2
regress1/quantifiers/smtlibe99bbe.smt2
regress1/quantifiers/smtlibf957ea.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/issue6101-2.smt2
regress1/strings/issue6132-non-unique-skolem.smt2
regress1/strings/issue6142-repl-inv-rew.smt2
+ regress1/strings/issue6180-proxy-vars.smt2
+ regress1/strings/issue6180-2-proxy-vars.smt2
+ regress1/strings/issue6184-unsat-core.smt2
regress1/strings/issue6191-replace-all.smt2
regress1/strings/issue6203-1-substr-ctn-strip.smt2
regress1/strings/issue6203-2-re-ccache.smt2
regress1/strings/issue6604-2.smt2
regress1/strings/issue6635-rre.smt2
regress1/strings/issue6653-2-update-c-len.smt2
+ regress1/strings/issue6653-3-seq.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/nt6-dd.smt2
regress1/strings/nterm-re-inter-sigma.smt2
regress1/strings/open-pf-merge.smt2
+ regress1/strings/pattern1.smt2
regress1/strings/pierre150331.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/strings/rev-ex5.smt2
regress1/strings/rew-020618.smt2
regress1/strings/rew-check1.smt2
+ regress1/strings/seq-cardinality.smt2
regress1/strings/seq-quant-infinite-branch.smt2
regress1/strings/simple-re-consume.smt2
regress1/strings/stoi-400million.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-abduct-test-ccore.smt2
- regress1/sygus-abduct-test-user.smt2
regress1/sygus/VC22_a.sy
- regress1/sygus/abd-simple-conj-4.smt2
- regress1/sygus/abduction_1255.corecstrs.readable.smt2
- regress1/sygus/abduction_streq.readable.smt2
- regress1/sygus/abduction-no-pbe-sym-break.smt2
regress1/sygus/abv.sy
regress1/sygus/array-grammar-store.sy
regress1/sygus/array_search_5-Q-easy.sy
+ regress1/sygus/array-uc.sy
regress1/sygus/bvudiv-by-2.sy
regress1/sygus/cegar1.sy
regress1/sygus/cegis-unif-inv-eq-fair.sy
regress1/sygus/trivial-stream.sy
regress1/sygus/twolets1.sy
regress1/sygus/twolets2-orig.sy
- regress1/sygus/uf-abduct.smt2
regress1/sygus/unbdd_inv_gen_winf1.sy
regress1/sygus/univ_2-long-repeat.sy
- regress1/sygus/yoni-true-sol.smt2
regress1/sym/q-constant.smt2
regress1/sym/q-function.smt2
regress1/sym/qf-function.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
regress2/push-pop/DRAGON_4_e2_2799_e3_1915.lus.ic3.1.min.smt2
regress2/quantifiers/AdditiveMethods_AdditiveMethods..ctor.smt2
regress2/quantifiers/cee-event-wrong-sat.smt2
+ regress2/quantifiers/exp-trivially-dd3.smt2
regress2/quantifiers/gn-wrong-091018.smt2
regress2/quantifiers/issue3481-unsat1.smt2
regress2/quantifiers/javafe.ast.StandardPrettyPrint.319.smt2
regress2/sygus/pbe_bvurem.sy
regress2/sygus/process-10-vars-2fun.sy
regress2/sygus/process-arg-invariance.sy
+ regress2/sygus/qgu-bools.sy
regress2/sygus/real-grammar-neg.sy
regress2/sygus/sets-fun-test.sy
regress2/sygus/sumn_recur_synth.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
- # TODO: fix models (projects #276)
- regress1/fmf/ko-bound-set.cvc.smt2
# results in an assertion failure (see issue #1650).
regress1/ho/hoa0102.smt2
# after disallowing solving for terms with quantifiers
regress1/ho/nested_lambdas-AGT034^2.smt2
regress1/ho/nested_lambdas-sat-SYO056^1-delta.smt2
regress1/ho/SYO056^1.p
- # slow on some builds after changes to tangent planes
- regress1/nl/approx-sqrt-unsat.smt2
# times out after update to circuit propagator
regress1/nl/dumortier_llibre_artes_ex_5_13.transcendental.k2.smt2
# times out after update to tangent planes
regress1/quantifiers/macro-subtype-param.smt2
# times out with competition build, ok with other builds:
regress1/quantifiers/model_6_1_bv.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
+ # 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
- regress2/quantifiers/exp-trivially-dd3.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