summaryrefslogtreecommitdiff
path: root/test/regress/regress0/quantifiers
ModeNameSize
-rw-r--r--006-cbqi-ite.smt211492logplain
-rw-r--r--ARI176e1.smt2150logplain
-rw-r--r--AdditiveMethods_AdditiveMethods..ctor.smt245830logplain
-rw-r--r--AdditiveMethods_OwnedResults.Mz.smt242191logplain
-rw-r--r--Arrays_Q1-noinfer.smt24185logplain
-rw-r--r--Makefile148logplain
-rw-r--r--Makefile.am4477logplain
-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_16.smt24299logplain
-rw-r--r--agg-rew-test-cf.smt2180logplain
-rw-r--r--agg-rew-test.smt2174logplain
-rw-r--r--anti-sk-simp.smt2280logplain
-rw-r--r--ari056.smt2133logplain
-rw-r--r--ari118-bv-2occ-x.smt2209logplain
-rw-r--r--array-unsat-simp3.smt2980logplain
-rw-r--r--bi-artm-s.smt2875logplain
-rw-r--r--bignum_quant.smt2406logplain
-rw-r--r--bug269.smt2490logplain
-rw-r--r--bug290.smt2710logplain
-rw-r--r--bug291.smt2452logplain
-rw-r--r--bug291.smt2.expect56logplain
-rw-r--r--bug749-rounding.smt2283logplain
-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-lia-dt-simp.smt2257logplain
-rw-r--r--cbqi-sdlx-fixpoint-3-dd.smt2369logplain
-rw-r--r--cdt-0208-to.smt2143805logplain
-rw-r--r--clock-10.smt2161logplain
-rw-r--r--clock-3.smt2160logplain
-rw-r--r--delta-simp.smt2181logplain
-rw-r--r--double-pattern.smt2179logplain
-rw-r--r--ex3.smt2258logplain
-rw-r--r--ex6.smt2349logplain
-rw-r--r--ext-ex-deq-trigger.smt2667logplain
-rw-r--r--extract-nproc.smt2382logplain
-rw-r--r--floor.smt2138logplain
-rw-r--r--florian-case-ax.smt26650logplain
-rw-r--r--gauss_init_0030.fof.smt27666logplain
-rw-r--r--inst-max-level-segf.smt214232logplain
-rw-r--r--intersection-example-onelane.proof-node22337.smt21702logplain
-rw-r--r--is-even-pred.smt2225logplain
-rw-r--r--is-even.smt2260logplain
-rw-r--r--is-int.smt2263logplain
-rw-r--r--javafe.ast.ArrayInit.35.smt295882logplain
-rw-r--r--javafe.ast.StandardPrettyPrint.319.smt2134345logplain
-rw-r--r--javafe.ast.StmtVec.009.smt231334logplain
-rw-r--r--javafe.ast.WhileStmt.447.smt293917logplain
-rw-r--r--javafe.tc.CheckCompilationUnit.001.smt275099logplain
-rw-r--r--javafe.tc.FlowInsensitiveChecks.682.smt2160472logplain
-rw-r--r--lra-triv-gn.smt2187logplain
-rw-r--r--macro-subtype-param.smt2657logplain
-rw-r--r--macros-int-real.smt2198logplain
-rw-r--r--macros-real-arg.smt2310logplain
-rw-r--r--matching-lia-1arg.smt2178logplain
-rw-r--r--mix-coeff.smt2201logplain
-rw-r--r--mix-complete-strat.smt2338logplain
-rw-r--r--mix-match.smt2191logplain
-rw-r--r--mix-simp.smt2177logplain
-rw-r--r--model_6_1_bv.smt21200logplain
-rw-r--r--nested-delta.smt2180logplain
-rw-r--r--nested-inf.smt2152logplain
-rw-r--r--nested9_true-unreach-call.i_575.smt2776logplain
-rw-r--r--opisavailable-12.smt215872logplain
-rw-r--r--parametric-lists.smt21218logplain
-rw-r--r--partial-trigger.smt2232logplain
-rw-r--r--psyco-001-bv.smt22802logplain
-rw-r--r--psyco-107-bv.smt26192logplain
-rw-r--r--psyco-196.smt215431logplain
-rw-r--r--pure_dt_cbqi.smt2246logplain
-rw-r--r--qbv-disequality3.smt2257logplain
-rw-r--r--qbv-inequality2.smt2247logplain
-rw-r--r--qbv-multi-lit-uge.smt2281logplain
-rw-r--r--qbv-simp.smt2261logplain
-rw-r--r--qbv-simple-2vars-vo.smt2350logplain
-rw-r--r--qbv-test-invert-bvadd-neq.smt2250logplain
-rw-r--r--qbv-test-invert-bvand-neq.smt2246logplain
-rw-r--r--qbv-test-invert-bvand.smt2252logplain
-rw-r--r--qbv-test-invert-bvashr-0-neq.smt2251logplain
-rw-r--r--qbv-test-invert-bvashr-0.smt2253logplain
-rw-r--r--qbv-test-invert-bvashr-1-neq.smt2247logplain
-rw-r--r--qbv-test-invert-bvashr-1.smt2253logplain
-rw-r--r--qbv-test-invert-bvcomp.smt2315logplain
-rw-r--r--qbv-test-invert-bvlshr-0-neq.smt2251logplain
-rw-r--r--qbv-test-invert-bvlshr-0.smt2253logplain
-rw-r--r--qbv-test-invert-bvlshr-1-neq.smt2247logplain
-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-bvor-neq.smt2245logplain
-rw-r--r--qbv-test-invert-bvor.smt2251logplain
-rw-r--r--qbv-test-invert-bvshl-0-neq.smt2246logplain
-rw-r--r--qbv-test-invert-bvshl-0.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-bvult-1.smt2214logplain
-rw-r--r--qbv-test-invert-bvurem-1-neq.smt2247logplain
-rw-r--r--qbv-test-invert-bvurem-1.smt2253logplain
-rw-r--r--qbv-test-invert-bvxor-neq.smt2234logplain
-rw-r--r--qbv-test-invert-bvxor.smt2232logplain
-rw-r--r--qbv-test-invert-concat-0-neq.smt2252logplain
-rw-r--r--qbv-test-invert-concat-0.smt2254logplain
-rw-r--r--qbv-test-invert-concat-1-neq.smt2252logplain
-rw-r--r--qbv-test-invert-concat-1.smt2254logplain
-rw-r--r--qbv-test-invert-sign-extend.smt2263logplain
-rw-r--r--qbv-test-urem-rewrite.smt2253logplain
-rw-r--r--qcf-rel-dom-opt.smt2822logplain
-rw-r--r--qcft-javafe.filespace.TreeWalker.006.smt237428logplain
-rw-r--r--qcft-smtlib3dbc51.smt278822logplain
-rw-r--r--quaternion_ds1_symm_0428.fof.smt27507logplain
-rw-r--r--refcount24.cvc6720logplain
-rw-r--r--rew-to-0211-dd.smt219565logplain
-rw-r--r--rew-to-scala.smt22850logplain
-rw-r--r--ricart-agrawala6.smt23989logplain
-rw-r--r--set3.smt21385logplain
-rw-r--r--set8.smt21445logplain
-rw-r--r--simp-len.smt2245logplain
-rw-r--r--simp-typ-test.smt2185logplain
-rw-r--r--small-bug1-fixpoint-3.smt28607logplain
-rw-r--r--small-pipeline-fixpoint-3.smt27130logplain
-rw-r--r--smtlib384a03.smt243696logplain
-rw-r--r--smtlib46f14a.smt243323logplain
-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--symmetric_unsat_7.smt21534logplain
-rw-r--r--z3.620661-no-fv-trigger.smt23453logplain
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback