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.smt2168logplain
-rw-r--r--RND-small.smt2517logplain
-rw-r--r--RNDPRE_4_1-dd-nqe.smt2294logplain
-rw-r--r--RND_4_1-existing-inst.smt2245logplain
-rw-r--r--RND_4_16.smt24299logplain
-rw-r--r--anti-sk-simp.smt2261logplain
-rw-r--r--ari118-bv-2occ-x.smt2210logplain
-rw-r--r--arith-rec-fun.smt2157logplain
-rw-r--r--arith-snorm.smt233900logplain
-rw-r--r--array-unsat-simp3.smt2980logplain
-rw-r--r--bi-artm-s.smt2865logplain
-rw-r--r--bignum_quant.smt2406logplain
-rw-r--r--bug802.smt2119495logplain
-rw-r--r--bug822.smt2142205logplain
-rw-r--r--bug_743.smt222198logplain
-rw-r--r--burns13.smt22612logplain
-rw-r--r--burns4.smt21412logplain
-rw-r--r--cbqi-sdlx-fixpoint-3-dd.smt2370logplain
-rw-r--r--cdt-0208-to.smt2143800logplain
-rw-r--r--const.cvc67logplain
-rw-r--r--constfunc.cvc140logplain
-rw-r--r--dt-tc-opt-small.smt2427logplain
-rw-r--r--dump-inst-i.smt2795logplain
-rw-r--r--dump-inst-proof.smt2942logplain
-rw-r--r--dump-inst.smt2497logplain
-rw-r--r--eqrange_ex_1.smt29551logplain
-rw-r--r--ext-ex-deq-trigger.smt2657logplain
-rw-r--r--extract-nproc.smt2384logplain
-rw-r--r--f993-loss-easy.smt23232logplain
-rw-r--r--florian-case-ax.smt26650logplain
-rw-r--r--fp-cegqi-unsat.smt2924logplain
-rw-r--r--gauss_init_0030.fof.smt27666logplain
-rw-r--r--horn-simple.smt2314logplain
-rw-r--r--infer-arith-trigger-eq.smt228852logplain
-rw-r--r--inst-max-level-segf.smt214232logplain
-rw-r--r--inst-prop-simp.smt2418logplain
-rw-r--r--intersection-example-onelane.proof-node22337.smt21706logplain
-rw-r--r--is-even.smt2250logplain
-rw-r--r--isaplanner-goal20.smt22612logplain
-rw-r--r--issue2970-string-var-elim.smt2309logplain
-rw-r--r--issue3250-syg-inf-q.smt2379logplain
-rw-r--r--issue3316.smt21208logplain
-rw-r--r--issue3317.smt22434logplain
-rw-r--r--issue3481.smt215321logplain
-rw-r--r--issue3537.smt22010logplain
-rw-r--r--issue3628.smt2339logplain
-rw-r--r--issue3664.smt2160logplain
-rw-r--r--issue3724-quant.smt21713logplain
-rw-r--r--issue3765-quant-dd.smt2308logplain
-rw-r--r--issue3765.smt2386logplain
-rw-r--r--issue4021-ind-opts.smt2399logplain
-rw-r--r--issue4062-cegqi-aux.smt2263logplain
-rw-r--r--issue4243-prereg-inc.smt2346logplain
-rw-r--r--issue4290-cegqi-r.smt2476logplain
-rw-r--r--issue4328-nqe.smt2244logplain
-rw-r--r--issue4400-2-already-conf.smt21995logplain
-rw-r--r--issue4412-cegqi-type.smt2120logplain
-rw-r--r--issue4420-order-sensitive.smt22336logplain
-rw-r--r--issue4433-nqe.smt2217logplain
-rw-r--r--issue4620-erq-witness-unsound.smt2124logplain
-rw-r--r--issue4685-wrewrite.smt2185logplain
-rw-r--r--issue4849-nqe.smt2221logplain
-rw-r--r--issue5019-cegqi-i.smt2233logplain
-rw-r--r--issue5279-nqe.smt2143logplain
-rw-r--r--issue5365-nqe.smt2396logplain
-rw-r--r--issue5378-witness.smt2171logplain
-rw-r--r--issue5469-aext.smt2290logplain
-rw-r--r--issue5470-aext.smt2181logplain
-rw-r--r--issue5471-aext.smt2272logplain
-rw-r--r--issue5482-rtf-no-fv.smt2374logplain
-rw-r--r--issue5484-qe.smt2508logplain
-rw-r--r--issue5484b-qe.smt2620logplain
-rw-r--r--issue5506-qe.smt2128logplain
-rw-r--r--issue5507-qe.smt2828logplain
-rw-r--r--issue5658-qe.smt2128logplain
-rw-r--r--issue5766-wrong-sel-trigger.smt2556logplain
-rw-r--r--issue5899-qe.smt26899logplain
-rw-r--r--issue6699-nc-shadow.smt2225logplain
-rw-r--r--issue993.smt23585logplain
-rw-r--r--javafe.ast.StmtVec.009.smt231334logplain
-rw-r--r--lia-witness-div-pp.smt2993logplain
-rw-r--r--lra-vts-inf.smt28166logplain
-rw-r--r--macro-geo-small-3.smt2531logplain
-rw-r--r--macro-subtype-param.smt2647logplain
-rw-r--r--min-ppgt-em-incomplete.smt2993logplain
-rw-r--r--min-ppgt-em-incomplete2.smt21327logplain
-rw-r--r--mix-coeff.smt2201logplain
-rw-r--r--model_6_1_bv.smt21201logplain
-rw-r--r--mutualrec2.cvc497logplain
-rw-r--r--nested9_true-unreach-call.i_575.smt2777logplain
-rw-r--r--nl-pow-trick.smt2516logplain
-rw-r--r--nra-interleave-inst.smt21443logplain
-rw-r--r--opisavailable-12.smt215872logplain
-rw-r--r--parametric-lists.smt21051logplain
-rw-r--r--pool-example.smt2320logplain
-rw-r--r--prenex-scholl-smt08_RNDPRE_RNDPRE_4_6.smt21666logplain
-rw-r--r--psyco-001-bv.smt22802logplain
-rw-r--r--psyco-107-bv.smt26194logplain
-rw-r--r--psyco-196.smt215413logplain
-rw-r--r--qbv-disequality3.smt2260logplain
-rw-r--r--qbv-simple-2vars-vo.smt2355logplain
-rw-r--r--qbv-subcall.smt2860logplain
-rw-r--r--qbv-test-invert-bvashr-0.smt2256logplain
-rw-r--r--qbv-test-invert-bvashr-1.smt2256logplain
-rw-r--r--qbv-test-invert-bvcomp.smt2295logplain
-rw-r--r--qbv-test-invert-bvlshr-1.smt2256logplain
-rw-r--r--qbv-test-invert-bvmul-neq.smt2249logplain
-rw-r--r--qbv-test-invert-bvmul.smt2255logplain
-rw-r--r--qbv-test-invert-bvudiv-0-neq.smt2288logplain
-rw-r--r--qbv-test-invert-bvudiv-0.smt2290logplain
-rw-r--r--qbv-test-invert-bvudiv-1-neq.smt2288logplain
-rw-r--r--qbv-test-invert-bvudiv-1.smt2290logplain
-rw-r--r--qbv-test-invert-bvurem-1-neq.smt2250logplain
-rw-r--r--qbv-test-invert-bvurem-1.smt2256logplain
-rw-r--r--qbv-test-urem-rewrite.smt2256logplain
-rw-r--r--qcft-javafe.filespace.TreeWalker.006.smt237428logplain
-rw-r--r--qcft-smtlib3dbc51.smt278822logplain
-rw-r--r--qe-partial.smt2333logplain
-rw-r--r--qe.smt2155logplain
-rw-r--r--qid-debug-inst.smt2452logplain
-rw-r--r--qid.smt2439logplain
-rw-r--r--qs-has-term.smt26784logplain
-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--seq-solved-enum.smt2393logplain
-rw-r--r--seq-unsolved-ematch.smt2317logplain
-rw-r--r--set-choice-koikonomou.cvc212logplain
-rw-r--r--set3.smt21423logplain
-rw-r--r--set8.smt21445logplain
-rw-r--r--seu169+1.smt22049logplain
-rw-r--r--small-pipeline-fixpoint-3.smt27113logplain
-rw-r--r--smtcomp-qbv-053118.smt2617logplain
-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.smt217655logplain
-rw-r--r--subtype-param-unk.smt2691logplain
-rw-r--r--subtype-param.smt2651logplain
-rw-r--r--sygus-infer-nested.smt2185logplain
-rw-r--r--sygus-inst-nia-psyco-060.smt23801logplain
-rw-r--r--sygus-inst-ufnia-sat-t3_rw1505.smt23322logplain
-rw-r--r--symmetric_unsat_7.smt21593logplain
-rw-r--r--tpp-unit-fail-qbv.smt2250logplain
-rw-r--r--var-eq-trigger-simple.smt2311logplain
-rw-r--r--var-eq-trigger.smt264627logplain
-rw-r--r--z3.620661-no-fv-trigger.smt23453logplain
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback