summaryrefslogtreecommitdiff
path: root/test/regress/regress1/quantifiers
ModeNameSize
-rw-r--r--006-cbqi-ite.smt211492logplain
-rw-r--r--015-psyco-pp.smt212621logplain
-rw-r--r--AdditiveMethods_OwnedResults.Mz.smt242191logplain
-rw-r--r--Arrays_Q1-noinfer.smt24185logplain
-rw-r--r--NUM878.smt2167logplain
-rw-r--r--RND-small.smt2535logplain
-rw-r--r--RNDPRE_4_1-dd-nqe.smt2293logplain
-rw-r--r--RND_4_1-existing-inst.smt2245logplain
-rw-r--r--RND_4_16.smt24299logplain
-rw-r--r--anti-sk-simp.smt2280logplain
-rw-r--r--ari118-bv-2occ-x.smt2209logplain
-rw-r--r--arith-rec-fun.smt2157logplain
-rw-r--r--arith-snorm.smt233949logplain
-rw-r--r--array-unsat-simp3.smt2980logplain
-rw-r--r--bi-artm-s.smt2875logplain
-rw-r--r--bignum_quant.smt2406logplain
-rw-r--r--bug802.smt2119495logplain
-rw-r--r--bug822.smt2142205logplain
-rw-r--r--bug_743.smt222192logplain
-rw-r--r--burns13.smt22612logplain
-rw-r--r--burns4.smt21412logplain
-rw-r--r--cbqi-sdlx-fixpoint-3-dd.smt2369logplain
-rw-r--r--cdt-0208-to.smt2143805logplain
-rw-r--r--const.cvc67logplain
-rw-r--r--constfunc.cvc140logplain
-rw-r--r--dump-inst-i.smt2779logplain
-rw-r--r--dump-inst-proof.smt2918logplain
-rw-r--r--dump-inst.smt2480logplain
-rw-r--r--ext-ex-deq-trigger.smt2667logplain
-rw-r--r--extract-nproc.smt2382logplain
-rw-r--r--florian-case-ax.smt26650logplain
-rw-r--r--fp-cegqi-unsat.smt2943logplain
-rw-r--r--gauss_init_0030.fof.smt27666logplain
-rw-r--r--horn-simple.smt2302logplain
-rw-r--r--infer-arith-trigger-eq.smt228909logplain
-rw-r--r--inst-max-level-segf.smt214232logplain
-rw-r--r--inst-prop-simp.smt2462logplain
-rw-r--r--intersection-example-onelane.proof-node22337.smt21702logplain
-rw-r--r--is-even.smt2260logplain
-rw-r--r--isaplanner-goal20.smt22612logplain
-rw-r--r--javafe.ast.StmtVec.009.smt231334logplain
-rw-r--r--lra-vts-inf.smt28164logplain
-rw-r--r--macro-subtype-param.smt2657logplain
-rw-r--r--mix-coeff.smt2201logplain
-rw-r--r--model_6_1_bv.smt21200logplain
-rw-r--r--mutualrec2.cvc497logplain
-rw-r--r--nested9_true-unreach-call.i_575.smt2776logplain
-rw-r--r--nl-pow-trick.smt2490logplain
-rw-r--r--nra-interleave-inst.smt21442logplain
-rw-r--r--opisavailable-12.smt215872logplain
-rw-r--r--parametric-lists.smt21218logplain
-rw-r--r--psyco-001-bv.smt22802logplain
-rw-r--r--psyco-107-bv.smt26192logplain
-rw-r--r--psyco-196.smt215431logplain
-rw-r--r--qbv-disequality3.smt2257logplain
-rw-r--r--qbv-simple-2vars-vo.smt2350logplain
-rw-r--r--qbv-subcall.smt2827logplain
-rw-r--r--qbv-test-invert-bvashr-0.smt2253logplain
-rw-r--r--qbv-test-invert-bvashr-1.smt2253logplain
-rw-r--r--qbv-test-invert-bvcomp.smt2315logplain
-rw-r--r--qbv-test-invert-bvlshr-1.smt2253logplain
-rw-r--r--qbv-test-invert-bvmul-neq.smt2246logplain
-rw-r--r--qbv-test-invert-bvmul.smt2252logplain
-rw-r--r--qbv-test-invert-bvudiv-0-neq.smt2285logplain
-rw-r--r--qbv-test-invert-bvudiv-0.smt2287logplain
-rw-r--r--qbv-test-invert-bvudiv-1-neq.smt2305logplain
-rw-r--r--qbv-test-invert-bvudiv-1.smt2307logplain
-rw-r--r--qbv-test-invert-bvurem-1-neq.smt2247logplain
-rw-r--r--qbv-test-invert-bvurem-1.smt2253logplain
-rw-r--r--qbv-test-urem-rewrite.smt2253logplain
-rw-r--r--qcft-javafe.filespace.TreeWalker.006.smt237428logplain
-rw-r--r--qcft-smtlib3dbc51.smt278822logplain
-rw-r--r--qe-partial.smt2349logplain
-rw-r--r--qe.smt2196logplain
-rw-r--r--quant-wf-int-ind.smt2296logplain
-rw-r--r--quaternion_ds1_symm_0428.fof.smt27507logplain
-rw-r--r--recfact.cvc189logplain
-rw-r--r--rel-trigger-unusable.smt21564logplain
-rw-r--r--repair-const-nterm.smt2311logplain
-rw-r--r--rew-to-0211-dd.smt219565logplain
-rw-r--r--ricart-agrawala6.smt23989logplain
-rw-r--r--set-choice-koikonomou.cvc209logplain
-rw-r--r--set3.smt21423logplain
-rw-r--r--set8.smt21445logplain
-rw-r--r--small-pipeline-fixpoint-3.smt27130logplain
-rw-r--r--smtcomp-qbv-053118.smt2584logplain
-rw-r--r--smtlib384a03.smt243696logplain
-rw-r--r--smtlib46f14a.smt243323logplain
-rw-r--r--smtlibe99bbe.smt272882logplain
-rw-r--r--smtlibf957ea.smt243937logplain
-rw-r--r--stream-x2014-09-18-unsat.smt217666logplain
-rw-r--r--subtype-param-unk.smt2719logplain
-rw-r--r--subtype-param.smt2679logplain
-rw-r--r--sygus-infer-nested.smt2200logplain
-rw-r--r--symmetric_unsat_7.smt21591logplain
-rw-r--r--z3.620661-no-fv-trigger.smt23453logplain
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback