regress0/parser/bv_nat.smt2
regress0/parser/constraint.smt2
regress0/parser/declarefun-emptyset-uf.smt2
+ regress0/parser/define_sort.smt2
regress0/parser/force_logic_set_logic.smt2
regress0/parser/force_logic_success.smt2
regress0/parser/issue5163.smt2
regress1/bug681.smt2
regress1/bug694-Unapply1.scala-0.smt2
regress1/bug800.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/intersection_min1.smt2
+ regress1/bags/intersection_min2.smt2
+ regress1/bags/issue5759.smt2
regress1/bags/subbag1.smt2
regress1/bags/subbag2.smt2
regress1/bags/union_disjoint.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/error.cvc
regress1/errorcrash.smt2
regress1/fmf-fun-dbu.smt2
regress1/issue3990-sort-inference.smt2
regress1/issue4273-ext-rew-cache.smt2
regress1/issue4335-unsat-core.smt2
- regress1/issue5739-rtf-processed.smt2
+ regress1/issue5739-rtf-processed.smt2
regress1/lemmas/clocksynchro_5clocks.main_invar.base.smtv1.smt2
regress1/lemmas/pursuit-safety-8.smtv1.smt2
regress1/lemmas/simple_startup_9nodes.abstract.base.smtv1.smt2
regress1/quantifiers/RNDPRE_4_1-dd-nqe.smt2
regress1/quantifiers/RND_4_1-existing-inst.smt2
regress1/quantifiers/RND_4_16.smt2
- regress1/quantifiers/anti-sk-simp.smt2
regress1/quantifiers/ari118-bv-2occ-x.smt2
regress1/quantifiers/arith-rec-fun.smt2
regress1/quantifiers/array-unsat-simp3.smt2
regress1/quantifiers/constfunc.cvc
regress1/quantifiers/dt-tc-opt-small.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/javafe.ast.StmtVec.009.smt2
regress1/quantifiers/lia-witness-div-pp.smt2
regress1/quantifiers/lra-vts-inf.smt2
+ regress1/quantifiers/min-ppgt-em-incomplete.smt2
+ regress1/quantifiers/min-ppgt-em-incomplete2.smt2
regress1/quantifiers/mix-coeff.smt2
regress1/quantifiers/mutualrec2.cvc
regress1/quantifiers/nested9_true-unreach-call.i_575.smt2
regress1/quantifiers/qid-debug-inst.smt2
regress1/quantifiers/quant-wf-int-ind.smt2
regress1/quantifiers/quaternion_ds1_symm_0428.fof.smt2
+ regress1/quantifiers/qs-has-term.smt2
regress1/quantifiers/recfact.cvc
regress1/quantifiers/repair-const-nterm.smt2
regress1/quantifiers/rew-to-0211-dd.smt2
regress1/quantifiers/smtlibf957ea.smt2
regress1/quantifiers/sygus-infer-nested.smt2
regress1/quantifiers/symmetric_unsat_7.smt2
+ regress1/quantifiers/tpp-unit-fail-qbv.smt2
regress1/quantifiers/var-eq-trigger.smt2
regress1/quantifiers/var-eq-trigger-simple.smt2
regress1/quantifiers/z3.620661-no-fv-trigger.smt2
regress1/nl/NAVIGATION2.smt2
# sat or unknown in different builds
regress1/nl/issue3307.smt2
+ # waiting until we enable proofs in master
+ regress1/proofs/macro-res-exp-crowding-lit-inside-unit.smt2
+ # slow with sygus-inference after removing anti-skolemization
+ regress1/quantifiers/anti-sk-simp.smt2
# no longer support snorm option
regress1/quantifiers/arith-snorm.smt2
+ # until we have support for minimizing instantiations based on unsat core
+ regress1/quantifiers/dump-inst-proof.smt2
# ajreynol: different error messages on production and debug:
regress1/quantifiers/macro-subtype-param.smt2
# times out with competition build, ok with other builds: