/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
f993-loss-easy.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
issue2970-string-var-elim.smt2
issue3250-syg-inf-q.smt2
issue3316.smt2
issue3317.smt2
issue3481.smt2
issue3537.smt2
issue3628.smt2
issue3664.smt2
issue3724-quant.smt2
issue3765-quant-dd.smt2
issue3765.smt2
issue993.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
rel-trigger-unusable.smt2
repair-const-nterm.smt2
rew-to-0211-dd.smt2
ricart-agrawala6.smt2
set-choice-koikonomou.cvc
set3.smt2
set8.smt2
seu169+1.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
var-eq-trigger-simple.smt2
var-eq-trigger.smt2
z3.620661-no-fv-trigger.smt2