/test/regress/regress1/quantifiers/

• ../
• 006-cbqi-ite.smt2
• 015-psyco-pp.smt2
• AdditiveMethods_OwnedResults.Mz.smt2
• Arrays_Q1-noinfer.smt2
• NUM878.smt2
• RND-small.smt2
• RNDPRE_4_1-dd-nqe.smt2
• RND_4_1-existing-inst.smt2
• RND_4_16.smt2
• anti-sk-simp.smt2
• ari118-bv-2occ-x.smt2
• arith-rec-fun.smt2
• arith-snorm.smt2
• array-unsat-simp3.smt2
• bi-artm-s.smt2
• bignum_quant.smt2
• bug802.smt2
• bug822.smt2
• bug_743.smt2
• burns13.smt2
• burns4.smt2
• cbqi-sdlx-fixpoint-3-dd.smt2
• cdt-0208-to.smt2
• const.cvc
• constfunc.cvc
• dump-inst-i.smt2
• dump-inst-proof.smt2
• dump-inst.smt2
• ext-ex-deq-trigger.smt2
• extract-nproc.smt2
• florian-case-ax.smt2
• fp-cegqi-unsat.smt2
• gauss_init_0030.fof.smt2
• horn-simple.smt2
• infer-arith-trigger-eq.smt2
• inst-max-level-segf.smt2
• inst-prop-simp.smt2
• intersection-example-onelane.proof-node22337.smt2
• is-even.smt2
• isaplanner-goal20.smt2
• javafe.ast.StmtVec.009.smt2
• lra-vts-inf.smt2
• macro-subtype-param.smt2
• mix-coeff.smt2
• model_6_1_bv.smt2
• mutualrec2.cvc
• nested9_true-unreach-call.i_575.smt2
• nl-pow-trick.smt2
• nra-interleave-inst.smt2
• opisavailable-12.smt2
• parametric-lists.smt2
• psyco-001-bv.smt2
• psyco-107-bv.smt2
• psyco-196.smt2
• qbv-disequality3.smt2
• qbv-simple-2vars-vo.smt2
• qbv-subcall.smt2
• qbv-test-invert-bvashr-0.smt2
• qbv-test-invert-bvashr-1.smt2
• qbv-test-invert-bvcomp.smt2
• qbv-test-invert-bvlshr-1.smt2
• qbv-test-invert-bvmul-neq.smt2
• qbv-test-invert-bvmul.smt2
• qbv-test-invert-bvudiv-0-neq.smt2
• qbv-test-invert-bvudiv-0.smt2
• qbv-test-invert-bvudiv-1-neq.smt2
• qbv-test-invert-bvudiv-1.smt2
• qbv-test-invert-bvurem-1-neq.smt2
• qbv-test-invert-bvurem-1.smt2
• qbv-test-urem-rewrite.smt2
• qcft-javafe.filespace.TreeWalker.006.smt2
• qcft-smtlib3dbc51.smt2
• qe-partial.smt2
• qe.smt2
• quant-wf-int-ind.smt2
• quaternion_ds1_symm_0428.fof.smt2
• recfact.cvc
• repair-const-nterm.smt2
• rew-to-0211-dd.smt2
• ricart-agrawala6.smt2
• set-choice-koikonomou.cvc
• set3.smt2
• set8.smt2
• small-pipeline-fixpoint-3.smt2
• smtcomp-qbv-053118.smt2
• smtlib384a03.smt2
• smtlib46f14a.smt2
• smtlibe99bbe.smt2
• smtlibf957ea.smt2
• stream-x2014-09-18-unsat.smt2
• subtype-param-unk.smt2
• subtype-param.smt2
• sygus-infer-nested.smt2
• symmetric_unsat_7.smt2
• z3.620661-no-fv-trigger.smt2