git.libre-soc.org Git - cvc5.git/commit

author	Andrew Reynolds <andrew.j.reynolds@gmail.com>
	Thu, 15 Feb 2018 21:31:48 +0000 (15:31 -0600)
committer	Aina Niemetz <aina.niemetz@gmail.com>
	Thu, 15 Feb 2018 21:31:48 +0000 (13:31 -0800)
commit	55037e0bcef45c795f28ff3fcf6c1055af465c70
tree	397d89bd10e541e1206c5dafdb8cf731feb34730	tree
parent	52a39aca19b7238d08c3cebcfa46436a73194008	commit \| diff

Refactor regressions (#1581)

1366 files changed:

test/Makefile.am		diff \| blob \| history
test/regress/regress0/Makefile.am		diff \| blob \| history
test/regress/regress0/arith/Makefile.am		diff \| blob \| history
test/regress/regress0/arith/bug547.1.smt2	[deleted file]	blob \| history
test/regress/regress0/arith/bug716.0.smt2	[deleted file]	blob \| history
test/regress/regress0/arith/bug716.1.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/div.03.smt2	[deleted file]	blob \| history
test/regress/regress0/arith/div.06.smt2	[deleted file]	blob \| history
test/regress/regress0/arith/div.08.smt2	[deleted file]	blob \| history
test/regress/regress0/arith/div.09.smt2	[deleted file]	blob \| history
test/regress/regress0/arith/integers/Makefile.am		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-001.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-002.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-003.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-004.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-005.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-006.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-007.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-008.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-009.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-010.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-011.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-012.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-013.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-016.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-017.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-018.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-019.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-020.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-022.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-024.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-026.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-027.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-028.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-029.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-030.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-031.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-032.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-033.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-034.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-035.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-036.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-037.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-038.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-039.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-040.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-041.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-043.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-044.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-045.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-046.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-047.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-048.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-049.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-050.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-051.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-052.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-053.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-054.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-055.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-056.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-057.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-058.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-059.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-060.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-061.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-062.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-063.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-064.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-065.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-066.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-067.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-068.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-069.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-070.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-071.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-072.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-073.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-074.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-075.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-076.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-077.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-078.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-080.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-081.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-082.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-083.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-084.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-085.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-086.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-087.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-088.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-089.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-090.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-091.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-092.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-093.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-094.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-095.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-096.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-097.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-098.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-099.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-100.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/miplib-opt1217--27.smt2	[deleted file]	blob \| history
test/regress/regress0/arith/miplib-pp08a-3000.smt2	[deleted file]	blob \| history
test/regress/regress0/arith/miplib3.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/mod.02.smt2	[deleted file]	blob \| history
test/regress/regress0/arith/mod.03.smt2	[deleted file]	blob \| history
test/regress/regress0/arith/mult.02.smt2	[deleted file]	blob \| history
test/regress/regress0/arith/problem__003.smt2	[deleted file]	blob \| history
test/regress/regress0/arrayinuf_error.smt2	[deleted file]	blob \| history
test/regress/regress0/arrays/Makefile.am		diff \| blob \| history
test/regress/regress0/arrays/constarr3.cvc	[deleted file]	blob \| history
test/regress/regress0/arrays/constarr3.smt2	[deleted file]	blob \| history
test/regress/regress0/arrays/parsing_ringer.cvc	[deleted file]	blob \| history
test/regress/regress0/aufbv/Makefile.am		diff \| blob \| history
test/regress/regress0/aufbv/bug580.smt2	[deleted file]	blob \| history
test/regress/regress0/auflia/bug337.smt2	[deleted file]	blob \| history
test/regress/regress0/boolean-terms-kernel2.smt2	[deleted file]	blob \| history
test/regress/regress0/boolean.cvc	[deleted file]	blob \| history
test/regress/regress0/bug216.smt2	[deleted file]	blob \| history
test/regress/regress0/bug216.smt2.expect	[deleted file]	blob \| history
test/regress/regress0/bug296.smt2	[deleted file]	blob \| history
test/regress/regress0/bug472.smt2	[deleted file]	blob \| history
test/regress/regress0/bug507.smt2	[deleted file]	blob \| history
test/regress/regress0/bug512.smt2	[deleted file]	blob \| history
test/regress/regress0/bug516.smt2	[deleted file]	blob \| history
test/regress/regress0/bug520.smt2	[deleted file]	blob \| history
test/regress/regress0/bug543.smt2	[deleted file]	blob \| history
test/regress/regress0/bug567.smt2	[deleted file]	blob \| history
test/regress/regress0/bug585.cvc	[deleted file]	blob \| history
test/regress/regress0/bug590.smt2	[deleted file]	blob \| history
test/regress/regress0/bug590.smt2.expect	[deleted file]	blob \| history
test/regress/regress0/bug593.smt2	[deleted file]	blob \| history
test/regress/regress0/bug681.smt2	[deleted file]	blob \| history
test/regress/regress0/bv/Makefile.am		diff \| blob \| history
test/regress/regress0/bv/bench_38.delta.smt2	[deleted file]	blob \| history
test/regress/regress0/bv/bug787.smt2	[deleted file]	blob \| history
test/regress/regress0/bv/bug_extract_mult_leading_bit.smt2	[deleted file]	blob \| history
test/regress/regress0/bv/bv-int-collapse2-sat.smt2	[deleted file]	blob \| history
test/regress/regress0/bv/bv2nat-ground.smt2	[deleted file]	blob \| history
test/regress/regress0/bv/bv2nat-simp-range-sat.smt2	[deleted file]	blob \| history
test/regress/regress0/bv/cmu-rdk-3.smt2	[deleted file]	blob \| history
test/regress/regress0/bv/decision-weight00.smt2	[deleted file]	blob \| history
test/regress/regress0/bv/divtest.smt2	[deleted file]	blob \| history
test/regress/regress0/bv/unsound1.smt2	[deleted file]	blob \| history
test/regress/regress0/crash_burn_locusts.smt2	[deleted file]	blob \| history
test/regress/regress0/datatypes/Makefile.am		diff \| blob \| history
test/regress/regress0/datatypes/acyclicity-sr-ground096.smt2	[deleted file]	blob \| history
test/regress/regress0/datatypes/bug341.cvc	[deleted file]	blob \| history
test/regress/regress0/datatypes/dt-color-2.6.smt2	[deleted file]	blob \| history
test/regress/regress0/datatypes/dt-param-card4-unsat.smt2	[deleted file]	blob \| history
test/regress/regress0/datatypes/error.cvc	[deleted file]	blob \| history
test/regress/regress0/datatypes/rec5.cvc	[deleted file]	blob \| history
test/regress/regress0/decision/Makefile.am		diff \| blob \| history
test/regress/regress0/decision/quant-Arrays_Q1-noinfer.smt2	[deleted file]	blob \| history
test/regress/regress0/decision/quant-Arrays_Q1-noinfer.smt2.expect	[deleted file]	blob \| history
test/regress/regress0/decision/quant-ex1.disable_miniscope.smt2	[deleted file]	blob \| history
test/regress/regress0/decision/quant-ex1.disable_miniscope.smt2.expect	[deleted file]	blob \| history
test/regress/regress0/decision/quant-symmetric_unsat_7.smt2	[deleted file]	blob \| history
test/regress/regress0/decision/quant-symmetric_unsat_7.smt2.expect	[deleted file]	blob \| history
test/regress/regress0/error.cvc	[deleted file]	blob \| history
test/regress/regress0/errorcrash.smt2	[deleted file]	blob \| history
test/regress/regress0/fmf/ALG008-1.smt2	[deleted file]	blob \| history
test/regress/regress0/fmf/LeftistHeap.scala-8-ncm.smt2	[deleted file]	blob \| history
test/regress/regress0/fmf/Makefile.am		diff \| blob \| history
test/regress/regress0/fmf/PUZ001+1.smt2	[deleted file]	blob \| history
test/regress/regress0/fmf/agree466.smt2	[deleted file]	blob \| history
test/regress/regress0/fmf/agree467.smt2	[deleted file]	blob \| history
test/regress/regress0/fmf/alg202+1.smt2	[deleted file]	blob \| history
test/regress/regress0/fmf/am-bad-model.cvc	[deleted file]	blob \| history
test/regress/regress0/fmf/bound-int-alt.smt2	[deleted file]	blob \| history
test/regress/regress0/fmf/bug0909.smt2	[deleted file]	blob \| history
test/regress/regress0/fmf/bug651.smt2	[deleted file]	blob \| history
test/regress/regress0/fmf/bug723-irrelevant-funs.smt2	[deleted file]	blob \| history
test/regress/regress0/fmf/bug764.smt2	[deleted file]	blob \| history
test/regress/regress0/fmf/cons-sets-bounds.smt2	[deleted file]	blob \| history
test/regress/regress0/fmf/constr-ground-to.smt2	[deleted file]	blob \| history
test/regress/regress0/fmf/datatypes-ufinite-nested.smt2	[deleted file]	blob \| history
test/regress/regress0/fmf/datatypes-ufinite.smt2	[deleted file]	blob \| history
test/regress/regress0/fmf/dt-proper-model.smt2	[deleted file]	blob \| history
test/regress/regress0/fmf/fc-pigeonhole19.smt2	[deleted file]	blob \| history
test/regress/regress0/fmf/fib-core.smt2	[deleted file]	blob \| history
test/regress/regress0/fmf/fmf-bound-2dim.smt2	[deleted file]	blob \| history
test/regress/regress0/fmf/fmf-bound-int.smt2	[deleted file]	blob \| history
test/regress/regress0/fmf/fmf-fun-no-elim-ext-arith.smt2	[deleted file]	blob \| history
test/regress/regress0/fmf/fmf-fun-no-elim-ext-arith2.smt2	[deleted file]	blob \| history
test/regress/regress0/fmf/fmf-strange-bounds.smt2	[deleted file]	blob \| history
test/regress/regress0/fmf/forall_unit_data.smt2	[deleted file]	blob \| history
test/regress/regress0/fmf/fore19-exp2-core.smt2	[deleted file]	blob \| history
test/regress/regress0/fmf/german169.smt2	[deleted file]	blob \| history
test/regress/regress0/fmf/german73.smt2	[deleted file]	blob \| history
test/regress/regress0/fmf/issue916-fmf-or.smt2	[deleted file]	blob \| history
test/regress/regress0/fmf/jasmin-cdt-crash.smt2	[deleted file]	blob \| history
test/regress/regress0/fmf/ko-bound-set.cvc	[deleted file]	blob \| history
test/regress/regress0/fmf/loopy_coda.smt2	[deleted file]	blob \| history
test/regress/regress0/fmf/lst-no-self-rev-exp.smt2	[deleted file]	blob \| history
test/regress/regress0/fmf/memory_model-R_cpp-dd.cvc	[deleted file]	blob \| history
test/regress/regress0/fmf/nun-0208-to.smt2	[deleted file]	blob \| history
test/regress/regress0/fmf/pow2-bool.smt2	[deleted file]	blob \| history
test/regress/regress0/fmf/refcount24.cvc.smt2	[deleted file]	blob \| history
test/regress/regress0/fmf/sc-crash-052316.smt2	[deleted file]	blob \| history
test/regress/regress0/fmf/with-ind-104-core.smt2	[deleted file]	blob \| history
test/regress/regress0/ho/Makefile.am		diff \| blob \| history
test/regress/regress0/ho/auth0068.smt2	[deleted file]	blob \| history
test/regress/regress0/ho/fta0409.smt2	[deleted file]	blob \| history
test/regress/regress0/ho/ho-exponential-model.smt2	[deleted file]	blob \| history
test/regress/regress0/ho/ho-matching-enum-2.smt2	[deleted file]	blob \| history
test/regress/regress0/ho/ho-std-fmf.smt2	[deleted file]	blob \| history
test/regress/regress0/ho/hoa0102.smt2	[deleted file]	blob \| history
test/regress/regress0/hole6.cvc	[deleted file]	blob \| history
test/regress/regress0/issue1048-arrays-int-real.smt2	[deleted file]	blob \| history
test/regress/regress0/ite5.smt2	[deleted file]	blob \| history
test/regress/regress0/nl/Makefile.am		diff \| blob \| history
test/regress/regress0/nl/bug698.smt2	[deleted file]	blob \| history
test/regress/regress0/nl/coeff-unsat-base.smt2	[deleted file]	blob \| history
test/regress/regress0/nl/coeff-unsat.smt2	[deleted file]	blob \| history
test/regress/regress0/nl/combine.smt2	[deleted file]	blob \| history
test/regress/regress0/nl/disj-eval.smt2	[deleted file]	blob \| history
test/regress/regress0/nl/dist-big.smt2	[deleted file]	blob \| history
test/regress/regress0/nl/div-mod-partial.smt2	[deleted file]	blob \| history
test/regress/regress0/nl/metitarski-1025.smt2	[deleted file]	blob \| history
test/regress/regress0/nl/metitarski-3-4.smt2	[deleted file]	blob \| history
test/regress/regress0/nl/metitarski_3_4_2e.smt2	[deleted file]	blob \| history
test/regress/regress0/nl/nl-help-unsat-quant.smt2	[deleted file]	blob \| history
test/regress/regress0/nl/nl-unk-quant.smt2	[deleted file]	blob \| history
test/regress/regress0/nl/nt-lemmas-bad.smt2	[deleted file]	blob \| history
test/regress/regress0/nl/nta/NAVIGATION2.smt2	[deleted file]	blob \| history
test/regress/regress0/nl/nta/arrowsmith-050317.smt2	[deleted file]	blob \| history
test/regress/regress0/nl/nta/bad-050217.smt2	[deleted file]	blob \| history
test/regress/regress0/nl/nta/cos-bound.smt2	[deleted file]	blob \| history
test/regress/regress0/nl/nta/cos1-tc.smt2	[deleted file]	blob \| history
test/regress/regress0/nl/nta/dumortier-050317.smt2	[deleted file]	blob \| history
test/regress/regress0/nl/nta/dumortier_llibre_artes_ex_5_13.transcendental.k2.smt2	[deleted file]	blob \| history
test/regress/regress0/nl/nta/exp-4.5-lt.smt2	[deleted file]	blob \| history
test/regress/regress0/nl/nta/exp1-lb.smt2	[deleted file]	blob \| history
test/regress/regress0/nl/nta/exp_monotone.smt2	[deleted file]	blob \| history
test/regress/regress0/nl/nta/shifting.smt2	[deleted file]	blob \| history
test/regress/regress0/nl/nta/shifting2.smt2	[deleted file]	blob \| history
test/regress/regress0/nl/nta/sin-compare-across-phase.smt2	[deleted file]	blob \| history
test/regress/regress0/nl/nta/sin-compare.smt2	[deleted file]	blob \| history
test/regress/regress0/nl/nta/sin-init-tangents.smt2	[deleted file]	blob \| history
test/regress/regress0/nl/nta/sin-sign.smt2	[deleted file]	blob \| history
test/regress/regress0/nl/nta/sin-sym2.smt2	[deleted file]	blob \| history
test/regress/regress0/nl/nta/sin1-lb.smt2	[deleted file]	blob \| history
test/regress/regress0/nl/nta/sin1-sat.smt2	[deleted file]	blob \| history
test/regress/regress0/nl/nta/sin1-ub.smt2	[deleted file]	blob \| history
test/regress/regress0/nl/nta/sin2-lb.smt2	[deleted file]	blob \| history
test/regress/regress0/nl/nta/sin2-ub.smt2	[deleted file]	blob \| history
test/regress/regress0/nl/nta/sugar-ident-2.smt2	[deleted file]	blob \| history
test/regress/regress0/nl/nta/sugar-ident-3.smt2	[deleted file]	blob \| history
test/regress/regress0/nl/nta/sugar-ident.smt2	[deleted file]	blob \| history
test/regress/regress0/nl/nta/tan-rewrite2.smt2	[deleted file]	blob \| history
test/regress/regress0/nl/ones.smt2	[deleted file]	blob \| history
test/regress/regress0/nl/poly-1025.smt2	[deleted file]	blob \| history
test/regress/regress0/nl/quant-nl.smt2	[deleted file]	blob \| history
test/regress/regress0/nl/red-exp.smt2	[deleted file]	blob \| history
test/regress/regress0/nl/rewriting-sums.smt2	[deleted file]	blob \| history
test/regress/regress0/nl/simple-mono-unsat.smt2	[deleted file]	blob \| history
test/regress/regress0/nl/simple-mono.smt2	[deleted file]	blob \| history
test/regress/regress0/nl/sqrt-problem-1.smt2	[deleted file]	blob \| history
test/regress/regress0/nl/zero-subset.smt2	[deleted file]	blob \| history
test/regress/regress0/non-fatal-errors.smt2	[deleted file]	blob \| history
test/regress/regress0/push-pop/Makefile.am		diff \| blob \| history
test/regress/regress0/push-pop/arith/Makefile	[deleted file]	blob \| history
test/regress/regress0/push-pop/arith/Makefile.am	[deleted file]	blob \| history
test/regress/regress0/push-pop/arith/fuzz_3_1.smt2	[deleted file]	blob \| history
test/regress/regress0/push-pop/arith/fuzz_3_10.smt2	[deleted file]	blob \| history
test/regress/regress0/push-pop/arith/fuzz_3_11.smt2	[deleted file]	blob \| history
test/regress/regress0/push-pop/arith/fuzz_3_12.smt2	[deleted file]	blob \| history
test/regress/regress0/push-pop/arith/fuzz_3_13.smt2	[deleted file]	blob \| history
test/regress/regress0/push-pop/arith/fuzz_3_14.smt2	[deleted file]	blob \| history
test/regress/regress0/push-pop/arith/fuzz_3_15.smt2	[deleted file]	blob \| history
test/regress/regress0/push-pop/arith/fuzz_3_2.smt2	[deleted file]	blob \| history
test/regress/regress0/push-pop/arith/fuzz_3_3.smt2	[deleted file]	blob \| history
test/regress/regress0/push-pop/arith/fuzz_3_4.smt2	[deleted file]	blob \| history
test/regress/regress0/push-pop/arith/fuzz_3_5.smt2	[deleted file]	blob \| history
test/regress/regress0/push-pop/arith/fuzz_3_6.smt2	[deleted file]	blob \| history
test/regress/regress0/push-pop/arith/fuzz_3_7.smt2	[deleted file]	blob \| history
test/regress/regress0/push-pop/arith/fuzz_3_8.smt2	[deleted file]	blob \| history
test/regress/regress0/push-pop/arith/fuzz_3_9.smt2	[deleted file]	blob \| history
test/regress/regress0/push-pop/arith/fuzz_5_1.smt2	[deleted file]	blob \| history
test/regress/regress0/push-pop/arith/fuzz_5_2.smt2	[deleted file]	blob \| history
test/regress/regress0/push-pop/arith/fuzz_5_3.smt2	[deleted file]	blob \| history
test/regress/regress0/push-pop/arith/fuzz_5_4.smt2	[deleted file]	blob \| history
test/regress/regress0/push-pop/arith/fuzz_5_5.smt2	[deleted file]	blob \| history
test/regress/regress0/push-pop/arith/fuzz_5_6.smt2	[deleted file]	blob \| history
test/regress/regress0/push-pop/arith_lra_01.smt2	[deleted file]	blob \| history
test/regress/regress0/push-pop/arith_lra_02.smt2	[deleted file]	blob \| history
test/regress/regress0/push-pop/boolean/Makefile.am		diff \| blob \| history
test/regress/regress0/push-pop/boolean/fuzz_1.smt2	[deleted file]	blob \| history
test/regress/regress0/push-pop/boolean/fuzz_10.smt2	[deleted file]	blob \| history
test/regress/regress0/push-pop/boolean/fuzz_11.smt2	[deleted file]	blob \| history
test/regress/regress0/push-pop/boolean/fuzz_15.smt2	[deleted file]	blob \| history
test/regress/regress0/push-pop/boolean/fuzz_16.smt2	[deleted file]	blob \| history
test/regress/regress0/push-pop/boolean/fuzz_19.smt2	[deleted file]	blob \| history
test/regress/regress0/push-pop/boolean/fuzz_1_to_52_merged.smt2	[deleted file]	blob \| history
test/regress/regress0/push-pop/boolean/fuzz_20.smt2	[deleted file]	blob \| history
test/regress/regress0/push-pop/boolean/fuzz_23.smt2	[deleted file]	blob \| history
test/regress/regress0/push-pop/boolean/fuzz_24.smt2	[deleted file]	blob \| history
test/regress/regress0/push-pop/boolean/fuzz_25.smt2	[deleted file]	blob \| history
test/regress/regress0/push-pop/boolean/fuzz_26.smt2	[deleted file]	blob \| history
test/regress/regress0/push-pop/boolean/fuzz_28.smt2	[deleted file]	blob \| history
test/regress/regress0/push-pop/boolean/fuzz_29.smt2	[deleted file]	blob \| history
test/regress/regress0/push-pop/boolean/fuzz_30.smt2	[deleted file]	blob \| history
test/regress/regress0/push-pop/boolean/fuzz_32.smt2	[deleted file]	blob \| history
test/regress/regress0/push-pop/boolean/fuzz_34.smt2	[deleted file]	blob \| history
test/regress/regress0/push-pop/boolean/fuzz_35.smt2	[deleted file]	blob \| history
test/regress/regress0/push-pop/boolean/fuzz_37.smt2	[deleted file]	blob \| history
test/regress/regress0/push-pop/boolean/fuzz_39.smt2	[deleted file]	blob \| history
test/regress/regress0/push-pop/boolean/fuzz_4.smt2	[deleted file]	blob \| history
test/regress/regress0/push-pop/boolean/fuzz_40.smt2	[deleted file]	blob \| history
test/regress/regress0/push-pop/boolean/fuzz_41.smt2	[deleted file]	blob \| history
test/regress/regress0/push-pop/boolean/fuzz_42.smt2	[deleted file]	blob \| history
test/regress/regress0/push-pop/boolean/fuzz_43.smt2	[deleted file]	blob \| history
test/regress/regress0/push-pop/boolean/fuzz_44.smt2	[deleted file]	blob \| history
test/regress/regress0/push-pop/boolean/fuzz_45.smt2	[deleted file]	blob \| history
test/regress/regress0/push-pop/boolean/fuzz_5.smt2	[deleted file]	blob \| history
test/regress/regress0/push-pop/boolean/fuzz_51.smt2	[deleted file]	blob \| history
test/regress/regress0/push-pop/boolean/fuzz_52.smt2	[deleted file]	blob \| history
test/regress/regress0/push-pop/boolean/fuzz_6.smt2	[deleted file]	blob \| history
test/regress/regress0/push-pop/boolean/fuzz_7.smt2	[deleted file]	blob \| history
test/regress/regress0/push-pop/boolean/fuzz_8.smt2	[deleted file]	blob \| history
test/regress/regress0/push-pop/boolean/fuzz_9.smt2	[deleted file]	blob \| history
test/regress/regress0/push-pop/bug-fmf-fun-skolem.smt2	[deleted file]	blob \| history
test/regress/regress0/push-pop/bug216.smt2	[deleted file]	blob \| history
test/regress/regress0/push-pop/bug216.smt2.expect	[deleted file]	blob \| history
test/regress/regress0/push-pop/bug326.smt2	[deleted file]	blob \| history
test/regress/regress0/push-pop/bug396.smt2	[deleted file]	blob \| history
test/regress/regress0/push-pop/bug674.smt2	[deleted file]	blob \| history
test/regress/regress0/push-pop/bug694-Unapply1.scala-0.smt2	[deleted file]	blob \| history
test/regress/regress0/push-pop/bug765.smt2	[deleted file]	blob \| history
test/regress/regress0/push-pop/fmf-fun-dbu.smt2	[deleted file]	blob \| history
test/regress/regress0/push-pop/quant-fun-proc-unmacro.smt2	[deleted file]	blob \| history
test/regress/regress0/push-pop/quant-fun-proc.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/006-cbqi-ite.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/AdditiveMethods_AdditiveMethods..ctor.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/AdditiveMethods_OwnedResults.Mz.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/Arrays_Q1-noinfer.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/Makefile.am		diff \| blob \| history
test/regress/regress0/quantifiers/NUM878.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/RND-small.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/RNDPRE_4_1-dd-nqe.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/RND_4_16.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/anti-sk-simp.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/ari118-bv-2occ-x.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/array-unsat-simp3.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/bi-artm-s.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/bignum_quant.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/bug822.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/bug_743.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/burns13.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/burns4.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/cbqi-sdlx-fixpoint-3-dd.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/cdt-0208-to.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/ext-ex-deq-trigger.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/extract-nproc.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/florian-case-ax.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/gauss_init_0030.fof.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/inst-max-level-segf.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/intersection-example-onelane.proof-node22337.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/is-even.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/javafe.ast.ArrayInit.35.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/javafe.ast.StandardPrettyPrint.319.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/javafe.ast.StmtVec.009.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/javafe.ast.WhileStmt.447.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/javafe.tc.CheckCompilationUnit.001.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/javafe.tc.FlowInsensitiveChecks.682.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/macro-subtype-param.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/mix-coeff.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/model_6_1_bv.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/nested9_true-unreach-call.i_575.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/opisavailable-12.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/parametric-lists.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/psyco-001-bv.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/psyco-107-bv.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/psyco-196.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/qbv-disequality3.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/qbv-simple-2vars-vo.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/qbv-test-invert-bvashr-0.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/qbv-test-invert-bvashr-1.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/qbv-test-invert-bvcomp.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-1.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/qbv-test-invert-bvmul-neq.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/qbv-test-invert-bvmul.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/qbv-test-invert-bvudiv-0-neq.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/qbv-test-invert-bvudiv-0.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/qbv-test-invert-bvudiv-1-neq.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/qbv-test-invert-bvudiv-1.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/qbv-test-invert-bvurem-1-neq.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/qbv-test-invert-bvurem-1.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/qbv-test-urem-rewrite.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/qcft-javafe.filespace.TreeWalker.006.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/qcft-smtlib3dbc51.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/quaternion_ds1_symm_0428.fof.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/refcount24.cvc	[deleted file]	blob \| history
test/regress/regress0/quantifiers/rew-to-0211-dd.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/ricart-agrawala6.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/set3.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/set8.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/small-bug1-fixpoint-3.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/small-pipeline-fixpoint-3.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/smtlib384a03.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/smtlib46f14a.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/smtlibf957ea.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/stream-x2014-09-18-unsat.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/subtype-param-unk.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/subtype-param.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/symmetric_unsat_7.smt2	[deleted file]	blob \| history
test/regress/regress0/quantifiers/z3.620661-no-fv-trigger.smt2	[deleted file]	blob \| history
test/regress/regress0/rels/Makefile.am		diff \| blob \| history
test/regress/regress0/rels/addr_book_1.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/addr_book_1_1.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/bv1-unit.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/bv1-unitb.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/bv1.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/bv1p-sat.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/bv1p.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/bv2.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/garbage_collect.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/iden_1_1.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/join-eq-structure-and.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/join-eq-structure.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/join-eq-structure_0_1.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/joinImg_0_1.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/joinImg_0_2.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/joinImg_1.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/joinImg_1_1.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/joinImg_2.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/joinImg_2_1.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/prod-mod-eq.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/prod-mod-eq2.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/rel_complex_3.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/rel_complex_4.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/rel_complex_5.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/rel_mix_0_1.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/rel_pressure_0.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/rel_tc_10_1.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/rel_tc_4.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/rel_tc_4_1.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/rel_tc_5_1.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/rel_tc_6.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/rel_tc_9_1.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/rel_tp_2.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/rel_tp_join_2_1.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/set-strat.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/strat.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/strat_0_1.cvc	[deleted file]	blob \| history
test/regress/regress0/rewriterules/Makefile.am		diff \| blob \| history
test/regress/regress0/rewriterules/datatypes2.smt2	[deleted file]	blob \| history
test/regress/regress0/rewriterules/datatypes3.smt2	[deleted file]	blob \| history
test/regress/regress0/rewriterules/datatypes_clark_quantification.smt2	[deleted file]	blob \| history
test/regress/regress0/rewriterules/datatypes_sat.smt2	[deleted file]	blob \| history
test/regress/regress0/rewriterules/length_gen.smt2	[deleted file]	blob \| history
test/regress/regress0/rewriterules/length_gen_010.smt2	[deleted file]	blob \| history
test/regress/regress0/rewriterules/length_gen_010_lemma.smt2	[deleted file]	blob \| history
test/regress/regress0/rewriterules/length_gen_020.smt2	[deleted file]	blob \| history
test/regress/regress0/rewriterules/length_gen_020_sat.smt2	[deleted file]	blob \| history
test/regress/regress0/rewriterules/length_gen_040.smt2	[deleted file]	blob \| history
test/regress/regress0/rewriterules/length_gen_040_lemma.smt2	[deleted file]	blob \| history
test/regress/regress0/rewriterules/length_gen_040_lemma_trigger.smt2	[deleted file]	blob \| history
test/regress/regress0/rewriterules/length_gen_080.smt2	[deleted file]	blob \| history
test/regress/regress0/rewriterules/length_gen_1280.smt2	[deleted file]	blob \| history
test/regress/regress0/rewriterules/length_gen_1280_lemma_trigger.smt2	[deleted file]	blob \| history
test/regress/regress0/rewriterules/length_gen_160.smt2	[deleted file]	blob \| history
test/regress/regress0/rewriterules/length_gen_160_lemma.smt2	[deleted file]	blob \| history
test/regress/regress0/rewriterules/length_gen_160_lemma_trigger.smt2	[deleted file]	blob \| history
test/regress/regress0/rewriterules/length_gen_160_sat.smt2	[deleted file]	blob \| history
test/regress/regress0/rewriterules/length_gen_2560.smt2	[deleted file]	blob \| history
test/regress/regress0/rewriterules/length_gen_2560_sat.smt2	[deleted file]	blob \| history
test/regress/regress0/rewriterules/length_gen_640.smt2	[deleted file]	blob \| history
test/regress/regress0/rewriterules/length_gen_640_lemma.smt2	[deleted file]	blob \| history
test/regress/regress0/rewriterules/length_gen_640_sat.smt2	[deleted file]	blob \| history
test/regress/regress0/rewriterules/length_gen_inv_1280.smt2	[deleted file]	blob \| history
test/regress/regress0/rewriterules/length_gen_inv_160.smt2	[deleted file]	blob \| history
test/regress/regress0/rewriterules/length_trick3.smt2	[deleted file]	blob \| history
test/regress/regress0/rewriterules/length_trick3_int.smt2	[deleted file]	blob \| history
test/regress/regress0/rewriterules/native_datatypes2.smt2	[deleted file]	blob \| history
test/regress/regress0/rewriterules/reachability_back_to_the_future_extended.smt2	[deleted file]	blob \| history
test/regress/regress0/rewriterules/reachability_bbttf_eT_arrays.smt2	[deleted file]	blob \| history
test/regress/regress0/rewriterules/reachability_bttf_ext_Thomas.smt2	[deleted file]	blob \| history
test/regress/regress0/rewriterules/set_A_new_fast_tableau-base.smt2	[deleted file]	blob \| history
test/regress/regress0/rewriterules/set_A_new_fast_tableau-base_sat.smt2	[deleted file]	blob \| history
test/regress/regress0/rewriterules/test_efficient_ematching.smt2	[deleted file]	blob \| history
test/regress/regress0/rewriterules/test_guards.smt2	[deleted file]	blob \| history
test/regress/regress0/rewriterules/why3_vstte10_max_sum_harness2.smt2	[deleted file]	blob \| history
test/regress/regress0/rewriterules/why3_vstte10_max_sum_harness2_rr.smt2	[deleted file]	blob \| history
test/regress/regress0/rewriterules/why3_vstte10_max_sum_harness3.smt2	[deleted file]	blob \| history
test/regress/regress0/rewriterules/why3_vstte10_max_sum_harness3_rr.smt2	[deleted file]	blob \| history
test/regress/regress0/sep/Makefile.am		diff \| blob \| history
test/regress/regress0/sep/chain-int.smt2	[deleted file]	blob \| history
test/regress/regress0/sep/crash1220.smt2	[deleted file]	blob \| history
test/regress/regress0/sep/dispose-list-4-init.smt2	[deleted file]	blob \| history
test/regress/regress0/sep/emp2-quant-unsat.smt2	[deleted file]	blob \| history
test/regress/regress0/sep/finite-witness-sat.smt2	[deleted file]	blob \| history
test/regress/regress0/sep/fmf-nemp-2.smt2	[deleted file]	blob \| history
test/regress/regress0/sep/pto-04.smt2	[deleted file]	blob \| history
test/regress/regress0/sep/quant_wand.smt2	[deleted file]	blob \| history
test/regress/regress0/sep/sep-02.smt2	[deleted file]	blob \| history
test/regress/regress0/sep/sep-03.smt2	[deleted file]	blob \| history
test/regress/regress0/sep/sep-find2.smt2	[deleted file]	blob \| history
test/regress/regress0/sep/sep-fmf-priority.smt2	[deleted file]	blob \| history
test/regress/regress0/sep/sep-neg-1refine.smt2	[deleted file]	blob \| history
test/regress/regress0/sep/sep-neg-nstrict.smt2	[deleted file]	blob \| history
test/regress/regress0/sep/sep-neg-nstrict2.smt2	[deleted file]	blob \| history
test/regress/regress0/sep/sep-neg-simple.smt2	[deleted file]	blob \| history
test/regress/regress0/sep/sep-neg-swap.smt2	[deleted file]	blob \| history
test/regress/regress0/sep/sep-nterm-again.smt2	[deleted file]	blob \| history
test/regress/regress0/sep/sep-nterm-val-model.smt2	[deleted file]	blob \| history
test/regress/regress0/sep/simple-neg-sat.smt2	[deleted file]	blob \| history
test/regress/regress0/sep/wand-0526-sat.smt2	[deleted file]	blob \| history
test/regress/regress0/sep/wand-false.smt2	[deleted file]	blob \| history
test/regress/regress0/sep/wand-nterm-simp.smt2	[deleted file]	blob \| history
test/regress/regress0/sep/wand-nterm-simp2.smt2	[deleted file]	blob \| history
test/regress/regress0/sep/wand-simp-sat.smt2	[deleted file]	blob \| history
test/regress/regress0/sep/wand-simp-sat2.smt2	[deleted file]	blob \| history
test/regress/regress0/sep/wand-simp-unsat.smt2	[deleted file]	blob \| history
test/regress/regress0/sets/Makefile.am		diff \| blob \| history
test/regress/regress0/sets/arjun-set-univ.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/card-3.smt2	[deleted file]	blob \| history
test/regress/regress0/sets/card-4.smt2	[deleted file]	blob \| history
test/regress/regress0/sets/card-5.smt2	[deleted file]	blob \| history
test/regress/regress0/sets/card-6.smt2	[deleted file]	blob \| history
test/regress/regress0/sets/card-7.smt2	[deleted file]	blob \| history
test/regress/regress0/sets/copy_check_heap_access_33_4.smt2	[deleted file]	blob \| history
test/regress/regress0/sets/feb3/ListElts.hs.fqout.cvc4.317.smt2	[deleted file]	blob \| history
test/regress/regress0/sets/fuzz14418.smt2	[deleted file]	blob \| history
test/regress/regress0/sets/fuzz15201.smt2	[deleted file]	blob \| history
test/regress/regress0/sets/fuzz31811.smt2	[deleted file]	blob \| history
test/regress/regress0/sets/jan24/insert_invariant_37_2.smt2	[deleted file]	blob \| history
test/regress/regress0/sets/jan24/remove_check_free_31_6.smt2	[deleted file]	blob \| history
test/regress/regress0/sets/jan27/ListElem.hs.fqout.cvc4.38.smt2	[deleted file]	blob \| history
test/regress/regress0/sets/jan27/deepmeas0.hs.fqout.cvc4.41.smt2	[deleted file]	blob \| history
test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.cvc4.3577.smt2	[deleted file]	blob \| history
test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.cvc4.10.smt2	[deleted file]	blob \| history
test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.cvc4.1832.smt2	[deleted file]	blob \| history
test/regress/regress0/sets/mar2014/UniqueZipper.hs.1030minimized.cvc4.smt2	[deleted file]	blob \| history
test/regress/regress0/sets/mar2014/UniqueZipper.hs.1030minimized2.cvc4.smt2	[deleted file]	blob \| history
test/regress/regress0/sets/mar2014/lemmabug-ListElts317minimized.smt2	[deleted file]	blob \| history
test/regress/regress0/sets/setofsets-disequal.smt2	[deleted file]	blob \| history
test/regress/regress0/sets/sets-tuple-poly.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/sharingbug.smt2	[deleted file]	blob \| history
test/regress/regress0/sets/univ-set-uf-elim.smt2	[deleted file]	blob \| history
test/regress/regress0/simple-rdl-definefun.smt2	[deleted file]	blob \| history
test/regress/regress0/simplification_bug4.smt2	[deleted file]	blob \| history
test/regress/regress0/simplification_bug4.smt2.expect	[deleted file]	blob \| history
test/regress/regress0/sqrt2-sort-inf-unk.smt2	[deleted file]	blob \| history
test/regress/regress0/strings/Makefile.am		diff \| blob \| history
test/regress/regress0/strings/artemis-0512-nonterm.smt2	[deleted file]	blob \| history
test/regress/regress0/strings/at001.smt2	[deleted file]	blob \| history
test/regress/regress0/strings/bug615.smt2	[deleted file]	blob \| history
test/regress/regress0/strings/bug682.smt2	[deleted file]	blob \| history
test/regress/regress0/strings/bug686dd.smt2	[deleted file]	blob \| history
test/regress/regress0/strings/bug768.smt2	[deleted file]	blob \| history
test/regress/regress0/strings/bug799-min.smt2	[deleted file]	blob \| history
test/regress/regress0/strings/chapman150408.smt2	[deleted file]	blob \| history
test/regress/regress0/strings/cmu-2db2-extf-reg.smt2	[deleted file]	blob \| history
test/regress/regress0/strings/cmu-disagree-0707-dd.smt2	[deleted file]	blob \| history
test/regress/regress0/strings/cmu-inc-nlpp-071516.smt2	[deleted file]	blob \| history
test/regress/regress0/strings/cmu-substr-rw.smt2	[deleted file]	blob \| history
test/regress/regress0/strings/crash-1019.smt2	[deleted file]	blob \| history
test/regress/regress0/strings/csp-prefix-exp-bug.smt2	[deleted file]	blob \| history
test/regress/regress0/strings/fmf001.smt2	[deleted file]	blob \| history
test/regress/regress0/strings/fmf002.smt2	[deleted file]	blob \| history
test/regress/regress0/strings/gm-inc-071516-2.smt2	[deleted file]	blob \| history
test/regress/regress0/strings/idof-handg.smt2	[deleted file]	blob \| history
test/regress/regress0/strings/idof-nconst-index.smt2	[deleted file]	blob \| history
test/regress/regress0/strings/idof-neg-index.smt2	[deleted file]	blob \| history
test/regress/regress0/strings/idof-triv.smt2	[deleted file]	blob \| history
test/regress/regress0/strings/ilc-l-nt.smt2	[deleted file]	blob \| history
test/regress/regress0/strings/issue1105.smt2	[deleted file]	blob \| history
test/regress/regress0/strings/kaluza-fl.smt2	[deleted file]	blob \| history
test/regress/regress0/strings/loop002.smt2	[deleted file]	blob \| history
test/regress/regress0/strings/loop003.smt2	[deleted file]	blob \| history
test/regress/regress0/strings/loop004.smt2	[deleted file]	blob \| history
test/regress/regress0/strings/loop005.smt2	[deleted file]	blob \| history
test/regress/regress0/strings/loop006.smt2	[deleted file]	blob \| history
test/regress/regress0/strings/loop007.smt2	[deleted file]	blob \| history
test/regress/regress0/strings/loop008.smt2	[deleted file]	blob \| history
test/regress/regress0/strings/loop009.smt2	[deleted file]	blob \| history
test/regress/regress0/strings/nf-ff-contains-abs.smt2	[deleted file]	blob \| history
test/regress/regress0/strings/norn-360.smt2	[deleted file]	blob \| history
test/regress/regress0/strings/norn-ab.smt2	[deleted file]	blob \| history
test/regress/regress0/strings/norn-dis-0707-3.smt2	[deleted file]	blob \| history
test/regress/regress0/strings/norn-nel-bug-052116.smt2	[deleted file]	blob \| history
test/regress/regress0/strings/norn-simp-rew-sat.smt2	[deleted file]	blob \| history
test/regress/regress0/strings/pierre150331.smt2	[deleted file]	blob \| history
test/regress/regress0/strings/regexp001.smt2	[deleted file]	blob \| history
test/regress/regress0/strings/regexp002.smt2	[deleted file]	blob \| history
test/regress/regress0/strings/regexp003.smt2	[deleted file]	blob \| history
test/regress/regress0/strings/reloop.smt2	[deleted file]	blob \| history
test/regress/regress0/strings/repl-empty-sem.smt2	[deleted file]	blob \| history
test/regress/regress0/strings/repl-soundness-sem.smt2	[deleted file]	blob \| history
test/regress/regress0/strings/str001.smt2	[deleted file]	blob \| history
test/regress/regress0/strings/str002.smt2	[deleted file]	blob \| history
test/regress/regress0/strings/str006.smt2	[deleted file]	blob \| history
test/regress/regress0/strings/str007.smt2	[deleted file]	blob \| history
test/regress/regress0/strings/strings-index-empty.smt2	[deleted file]	blob \| history
test/regress/regress0/strings/strip-endpt-sound.smt2	[deleted file]	blob \| history
test/regress/regress0/strings/substr001.smt2	[deleted file]	blob \| history
test/regress/regress0/strings/type002.smt2	[deleted file]	blob \| history
test/regress/regress0/strings/type003.smt2	[deleted file]	blob \| history
test/regress/regress0/strings/username_checker_min.smt2	[deleted file]	blob \| history
test/regress/regress0/subranges.cvc	[deleted file]	blob \| history
test/regress/regress0/sygus/Base16_1.sy	[deleted file]	blob \| history
test/regress/regress0/sygus/Makefile.am		diff \| blob \| history
test/regress/regress0/sygus/array_search_2.sy	[deleted file]	blob \| history
test/regress/regress0/sygus/array_sum_2_5.sy	[deleted file]	blob \| history
test/regress/regress0/sygus/cegar1.sy	[deleted file]	blob \| history
test/regress/regress0/sygus/cggmp.sy	[deleted file]	blob \| history
test/regress/regress0/sygus/clock-inc-tuple.sy	[deleted file]	blob \| history
test/regress/regress0/sygus/commutative.sy	[deleted file]	blob \| history
test/regress/regress0/sygus/constant.sy	[deleted file]	blob \| history
test/regress/regress0/sygus/dt-test-ns.sy	[deleted file]	blob \| history
test/regress/regress0/sygus/dup-op.sy	[deleted file]	blob \| history
test/regress/regress0/sygus/enum-test.sy	[deleted file]	blob \| history
test/regress/regress0/sygus/fg_polynomial3.sy	[deleted file]	blob \| history
test/regress/regress0/sygus/hd-01-d1-prog.sy	[deleted file]	blob \| history
test/regress/regress0/sygus/hd-19-d1-prog-dup-op.sy	[deleted file]	blob \| history
test/regress/regress0/sygus/icfp_14.12-flip-args.sy	[deleted file]	blob \| history
test/regress/regress0/sygus/icfp_14.12.sy	[deleted file]	blob \| history
test/regress/regress0/sygus/icfp_28_10.sy	[deleted file]	blob \| history
test/regress/regress0/sygus/icfp_easy-ite.sy	[deleted file]	blob \| history
test/regress/regress0/sygus/inv-example.sy	[deleted file]	blob \| history
test/regress/regress0/sygus/inv-unused.sy	[deleted file]	blob \| history
test/regress/regress0/sygus/list-head-x.sy	[deleted file]	blob \| history
test/regress/regress0/sygus/max.smt2	[deleted file]	blob \| history
test/regress/regress0/sygus/max.sy	[deleted file]	blob \| history
test/regress/regress0/sygus/max2-univ.sy	[deleted file]	blob \| history
test/regress/regress0/sygus/multi-fun-polynomial2.sy	[deleted file]	blob \| history
test/regress/regress0/sygus/nflat-fwd-3.sy	[deleted file]	blob \| history
test/regress/regress0/sygus/nflat-fwd.sy	[deleted file]	blob \| history
test/regress/regress0/sygus/nia-max-square-ns.sy	[deleted file]	blob \| history
test/regress/regress0/sygus/no-flat-simp.sy	[deleted file]	blob \| history
test/regress/regress0/sygus/no-mention.sy	[deleted file]	blob \| history
test/regress/regress0/sygus/no-syntax-test-no-si.sy	[deleted file]	blob \| history
test/regress/regress0/sygus/process-10-vars-2fun.sy	[deleted file]	blob \| history
test/regress/regress0/sygus/process-10-vars.sy	[deleted file]	blob \| history
test/regress/regress0/sygus/qe.sy	[deleted file]	blob \| history
test/regress/regress0/sygus/real-grammar-neg.sy	[deleted file]	blob \| history
test/regress/regress0/sygus/strings-concat-3-args.sy	[deleted file]	blob \| history
test/regress/regress0/sygus/strings-double-rec.sy	[deleted file]	blob \| history
test/regress/regress0/sygus/strings-small.sy	[deleted file]	blob \| history
test/regress/regress0/sygus/strings-template-infer-unused.sy	[deleted file]	blob \| history
test/regress/regress0/sygus/strings-template-infer.sy	[deleted file]	blob \| history
test/regress/regress0/sygus/strings-trivial-simp.sy	[deleted file]	blob \| history
test/regress/regress0/sygus/strings-trivial-two-type.sy	[deleted file]	blob \| history
test/regress/regress0/sygus/strings-trivial.sy	[deleted file]	blob \| history
test/regress/regress0/sygus/sygus-dt.sy	[deleted file]	blob \| history
test/regress/regress0/sygus/tl-type-0.sy	[deleted file]	blob \| history
test/regress/regress0/sygus/tl-type-4x.sy	[deleted file]	blob \| history
test/regress/regress0/sygus/tl-type.sy	[deleted file]	blob \| history
test/regress/regress0/sygus/triv-type-mismatch-si.sy	[deleted file]	blob \| history
test/regress/regress0/sygus/twolets1.sy	[deleted file]	blob \| history
test/regress/regress0/sygus/twolets2-orig.sy	[deleted file]	blob \| history
test/regress/regress0/sygus/unbdd_inv_gen_winf1.sy	[deleted file]	blob \| history
test/regress/regress0/test12.cvc	[deleted file]	blob \| history
test/regress/regress0/trim.cvc	[deleted file]	blob \| history
test/regress/regress0/uf/Makefile.am		diff \| blob \| history
test/regress/regress0/uf/gensys_brn001.smt2	[deleted file]	blob \| history
test/regress/regress0/uf/proof00.smt2	[deleted file]	blob \| history
test/regress/regress0/uflia/DRAGON_11_e1_2450.ec.minimized.smt2	[deleted file]	blob \| history
test/regress/regress0/uflia/DRAGON_11_e1_2450.ec.minimized.smt2.expect	[deleted file]	blob \| history
test/regress/regress0/uflia/FIREFLY_3_e2_2236_e7_3681.ec.core.smt2	[deleted file]	blob \| history
test/regress/regress0/uflia/FIREFLY_3_e2_2236_e7_3681.ec.core.smt2.expect	[deleted file]	blob \| history
test/regress/regress0/uflia/FIREFLY_luke_1b_e2_3049_e7_1173.ec.minimized.smt2	[deleted file]	blob \| history
test/regress/regress0/uflia/Makefile.am		diff \| blob \| history
test/regress/regress0/uflia/javafe.ast.StandardPrettyPrint.319_no_forall.smt2	[deleted file]	blob \| history
test/regress/regress0/uflia/javafe.ast.WhileStmt.447_no_forall.smt2	[deleted file]	blob \| history
test/regress/regress0/uflia/microwave21.ec.minimized.smt2	[deleted file]	blob \| history
test/regress/regress0/uflia/simple_cyclic2.smt2	[deleted file]	blob \| history
test/regress/regress0/uflia/simplify.javafe.ast.ArrayInit.35_without_quantification2.smt2	[deleted file]	blob \| history
test/regress/regress0/uflia/speed2_e8_449_e8_517.ec.smt2	[deleted file]	blob \| history
test/regress/regress0/uflia/speed2_e8_449_e8_517.ec.smt2.expect	[deleted file]	blob \| history
test/regress/regress0/uflia/stalmark_e7_27_e7_31.ec.smt2	[deleted file]	blob \| history
test/regress/regress0/uflia/stalmark_e7_27_e7_31.ec.smt2.expect	[deleted file]	blob \| history
test/regress/regress0/uflra/Makefile.am		diff \| blob \| history
test/regress/regress0/uflra/bug800.smt2	[deleted file]	blob \| history
test/regress/regress0/unconstrained/Makefile.am		diff \| blob \| history
test/regress/regress0/unconstrained/bvdiv2.smt2	[deleted file]	blob \| history
test/regress/regress0/unconstrained/uf2.smt2	[deleted file]	blob \| history
test/regress/regress1/Makefile.am		diff \| blob \| history
test/regress/regress1/arith/Makefile.am	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-001.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-002.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-003.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-004.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-005.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-006.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-007.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-008.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-009.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-010.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-011.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-012.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-013.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-016.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-017.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-018.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-019.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-020.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-022.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-024.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-026.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-027.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-028.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-029.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-030.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-031.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-032.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-033.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-034.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-035.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-036.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-037.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-038.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-039.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-040.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-041.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-043.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-044.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-045.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-046.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-047.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-048.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-049.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-050.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-051.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-052.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-053.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-054.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-055.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-056.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-057.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-058.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-059.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-060.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-061.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-062.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-063.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-064.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-065.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-066.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-067.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-068.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-069.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-070.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-071.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-072.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-073.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-074.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-075.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-076.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-077.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-078.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-080.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-081.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-082.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-083.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-084.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-085.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-086.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-087.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-088.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-089.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-090.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-091.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-092.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-093.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-094.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-095.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-096.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-097.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-099.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-100.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/bug547.1.smt2	[new file with mode: 0644]	blob
test/regress/regress1/arith/bug716.0.smt2	[new file with mode: 0644]	blob
test/regress/regress1/arith/bug716.1.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/div.03.smt2	[new file with mode: 0644]	blob
test/regress/regress1/arith/div.06.smt2	[new file with mode: 0644]	blob
test/regress/regress1/arith/div.08.smt2	[new file with mode: 0644]	blob
test/regress/regress1/arith/div.09.smt2	[new file with mode: 0644]	blob
test/regress/regress1/arith/miplib3.cvc	[new file with mode: 0644]	blob
test/regress/regress1/arith/mod.02.smt2	[new file with mode: 0644]	blob
test/regress/regress1/arith/mod.03.smt2	[new file with mode: 0644]	blob
test/regress/regress1/arith/mult.02.smt2	[new file with mode: 0644]	blob
test/regress/regress1/arith/problem__003.smt2	[new file with mode: 0644]	blob
test/regress/regress1/arrayinuf_error.smt2	[new file with mode: 0644]	blob
test/regress/regress1/aufbv/Makefile.am		diff \| blob \| history
test/regress/regress1/aufbv/bug580.smt2	[new file with mode: 0644]	blob
test/regress/regress1/auflia/Makefile.am		diff \| blob \| history
test/regress/regress1/auflia/bug337.smt2	[new file with mode: 0644]	blob
test/regress/regress1/boolean-terms-kernel2.smt2	[new file with mode: 0644]	blob
test/regress/regress1/boolean.cvc	[new file with mode: 0644]	blob
test/regress/regress1/bug216.smt2	[new file with mode: 0644]	blob
test/regress/regress1/bug216.smt2.expect	[new file with mode: 0644]	blob
test/regress/regress1/bug296.smt2	[new file with mode: 0644]	blob
test/regress/regress1/bug472.smt2	[new file with mode: 0644]	blob
test/regress/regress1/bug507.smt2	[new file with mode: 0644]	blob
test/regress/regress1/bug512.smt2	[new file with mode: 0644]	blob
test/regress/regress1/bug516.smt2	[new file with mode: 0644]	blob
test/regress/regress1/bug520.smt2	[new file with mode: 0644]	blob
test/regress/regress1/bug543.smt2	[new file with mode: 0644]	blob
test/regress/regress1/bug567.smt2	[new file with mode: 0644]	blob
test/regress/regress1/bug585.cvc	[new file with mode: 0644]	blob
test/regress/regress1/bug590.smt2	[new file with mode: 0644]	blob
test/regress/regress1/bug590.smt2.expect	[new file with mode: 0644]	blob
test/regress/regress1/bug593.smt2	[new file with mode: 0644]	blob
test/regress/regress1/bug681.smt2	[new file with mode: 0644]	blob
test/regress/regress1/bug694-Unapply1.scala-0.smt2	[new file with mode: 0644]	blob
test/regress/regress1/bug800.smt2	[new file with mode: 0644]	blob
test/regress/regress1/bv/Makefile.am		diff \| blob \| history
test/regress/regress1/bv/bench_38.delta.smt2	[new file with mode: 0644]	blob
test/regress/regress1/bv/bug787.smt2	[new file with mode: 0644]	blob
test/regress/regress1/bv/bug_extract_mult_leading_bit.smt2	[new file with mode: 0644]	blob
test/regress/regress1/bv/bv-int-collapse2-sat.smt2	[new file with mode: 0644]	blob
test/regress/regress1/bv/bv2nat-ground.smt2	[new file with mode: 0644]	blob
test/regress/regress1/bv/bv2nat-simp-range-sat.smt2	[new file with mode: 0644]	blob
test/regress/regress1/bv/cmu-rdk-3.smt2	[new file with mode: 0644]	blob
test/regress/regress1/bv/decision-weight00.smt2	[new file with mode: 0644]	blob
test/regress/regress1/bv/divtest.smt2	[new file with mode: 0644]	blob
test/regress/regress1/bv/unsound1.smt2	[new file with mode: 0644]	blob
test/regress/regress1/bvdiv2.smt2	[new file with mode: 0644]	blob
test/regress/regress1/constarr3.cvc	[new file with mode: 0644]	blob
test/regress/regress1/constarr3.smt2	[new file with mode: 0644]	blob
test/regress/regress1/crash_burn_locusts.smt2	[new file with mode: 0644]	blob
test/regress/regress1/datatypes/Makefile.am		diff \| blob \| history
test/regress/regress1/datatypes/acyclicity-sr-ground096.smt2	[new file with mode: 0644]	blob
test/regress/regress1/datatypes/dt-color-2.6.smt2	[new file with mode: 0644]	blob
test/regress/regress1/datatypes/dt-param-card4-unsat.smt2	[new file with mode: 0644]	blob
test/regress/regress1/datatypes/error.cvc	[new file with mode: 0644]	blob
test/regress/regress1/decision/Makefile.am		diff \| blob \| history
test/regress/regress1/decision/quant-Arrays_Q1-noinfer.smt2	[new file with mode: 0644]	blob
test/regress/regress1/decision/quant-Arrays_Q1-noinfer.smt2.expect	[new file with mode: 0644]	blob
test/regress/regress1/decision/quant-symmetric_unsat_7.smt2	[new file with mode: 0644]	blob
test/regress/regress1/decision/quant-symmetric_unsat_7.smt2.expect	[new file with mode: 0644]	blob
test/regress/regress1/error.cvc	[new file with mode: 0644]	blob
test/regress/regress1/errorcrash.smt2	[new file with mode: 0644]	blob
test/regress/regress1/fmf-fun-dbu.smt2	[new file with mode: 0644]	blob
test/regress/regress1/fmf/ALG008-1.smt2	[new file with mode: 0644]	blob
test/regress/regress1/fmf/ForElimination-scala-9.smt2	[deleted file]	blob \| history
test/regress/regress1/fmf/LeftistHeap.scala-8-ncm.smt2	[new file with mode: 0644]	blob
test/regress/regress1/fmf/Makefile.am		diff \| blob \| history
test/regress/regress1/fmf/PUZ001+1.smt2	[new file with mode: 0644]	blob
test/regress/regress1/fmf/agree466.smt2	[new file with mode: 0644]	blob
test/regress/regress1/fmf/agree467.smt2	[new file with mode: 0644]	blob
test/regress/regress1/fmf/alg202+1.smt2	[new file with mode: 0644]	blob
test/regress/regress1/fmf/am-bad-model.cvc	[new file with mode: 0644]	blob
test/regress/regress1/fmf/bound-int-alt.smt2	[new file with mode: 0644]	blob
test/regress/regress1/fmf/bug0909.smt2	[new file with mode: 0644]	blob
test/regress/regress1/fmf/bug651.smt2	[new file with mode: 0644]	blob
test/regress/regress1/fmf/bug723-irrelevant-funs.smt2	[new file with mode: 0644]	blob
test/regress/regress1/fmf/bug764.smt2	[new file with mode: 0644]	blob
test/regress/regress1/fmf/cons-sets-bounds.smt2	[new file with mode: 0644]	blob
test/regress/regress1/fmf/constr-ground-to.smt2	[new file with mode: 0644]	blob
test/regress/regress1/fmf/datatypes-ufinite-nested.smt2	[new file with mode: 0644]	blob
test/regress/regress1/fmf/datatypes-ufinite.smt2	[new file with mode: 0644]	blob
test/regress/regress1/fmf/dt-proper-model.smt2	[new file with mode: 0644]	blob
test/regress/regress1/fmf/fc-pigeonhole19.smt2	[new file with mode: 0644]	blob
test/regress/regress1/fmf/fib-core.smt2	[new file with mode: 0644]	blob
test/regress/regress1/fmf/fmf-bound-2dim.smt2	[new file with mode: 0644]	blob
test/regress/regress1/fmf/fmf-bound-int.smt2	[new file with mode: 0644]	blob
test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith.smt2	[new file with mode: 0644]	blob
test/regress/regress1/fmf/fmf-fun-no-elim-ext-arith2.smt2	[new file with mode: 0644]	blob
test/regress/regress1/fmf/fmf-strange-bounds.smt2	[new file with mode: 0644]	blob
test/regress/regress1/fmf/forall_unit_data.smt2	[new file with mode: 0644]	blob
test/regress/regress1/fmf/fore19-exp2-core.smt2	[new file with mode: 0644]	blob
test/regress/regress1/fmf/german169.smt2	[new file with mode: 0644]	blob
test/regress/regress1/fmf/german73.smt2	[new file with mode: 0644]	blob
test/regress/regress1/fmf/issue916-fmf-or.smt2	[new file with mode: 0644]	blob
test/regress/regress1/fmf/jasmin-cdt-crash.smt2	[new file with mode: 0644]	blob
test/regress/regress1/fmf/ko-bound-set.cvc	[new file with mode: 0644]	blob
test/regress/regress1/fmf/loopy_coda.smt2	[new file with mode: 0644]	blob
test/regress/regress1/fmf/lst-no-self-rev-exp.smt2	[new file with mode: 0644]	blob
test/regress/regress1/fmf/memory_model-R_cpp-dd.cvc	[new file with mode: 0644]	blob
test/regress/regress1/fmf/nun-0208-to.smt2	[new file with mode: 0644]	blob
test/regress/regress1/fmf/nunchaku2309663.nun.min.smt2	[deleted file]	blob \| history
test/regress/regress1/fmf/pow2-bool.smt2	[new file with mode: 0644]	blob
test/regress/regress1/fmf/refcount24.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/fmf/sc-crash-052316.smt2	[new file with mode: 0644]	blob
test/regress/regress1/fmf/with-ind-104-core.smt2	[new file with mode: 0644]	blob
test/regress/regress1/gensys_brn001.smt2	[new file with mode: 0644]	blob
test/regress/regress1/ho/Makefile.am	[new file with mode: 0644]	blob
test/regress/regress1/ho/auth0068.smt2	[new file with mode: 0644]	blob
test/regress/regress1/ho/fta0409.smt2	[new file with mode: 0644]	blob
test/regress/regress1/ho/ho-exponential-model.smt2	[new file with mode: 0644]	blob
test/regress/regress1/ho/ho-matching-enum-2.smt2	[new file with mode: 0644]	blob
test/regress/regress1/ho/ho-std-fmf.smt2	[new file with mode: 0644]	blob
test/regress/regress1/ho/hoa0102.smt2	[new file with mode: 0644]	blob
test/regress/regress1/hole6.cvc	[new file with mode: 0644]	blob
test/regress/regress1/issue1048-arrays-int-real.smt2	[new file with mode: 0644]	blob
test/regress/regress1/ite5.smt2	[new file with mode: 0644]	blob
test/regress/regress1/nl/Makefile.am		diff \| blob \| history
test/regress/regress1/nl/NAVIGATION2.smt2	[new file with mode: 0644]	blob
test/regress/regress1/nl/arrowsmith-050317.smt2	[new file with mode: 0644]	blob
test/regress/regress1/nl/bad-050217.smt2	[new file with mode: 0644]	blob
test/regress/regress1/nl/bug698.smt2	[new file with mode: 0644]	blob
test/regress/regress1/nl/coeff-unsat-base.smt2	[new file with mode: 0644]	blob
test/regress/regress1/nl/coeff-unsat.smt2	[new file with mode: 0644]	blob
test/regress/regress1/nl/combine.smt2	[new file with mode: 0644]	blob
test/regress/regress1/nl/cos-bound.smt2	[new file with mode: 0644]	blob
test/regress/regress1/nl/cos1-tc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/nl/disj-eval.smt2	[new file with mode: 0644]	blob
test/regress/regress1/nl/dist-big.smt2	[new file with mode: 0644]	blob
test/regress/regress1/nl/div-mod-partial.smt2	[new file with mode: 0644]	blob
test/regress/regress1/nl/dumortier_llibre_artes_ex_5_13.transcendental.k2.smt2	[new file with mode: 0644]	blob
test/regress/regress1/nl/exp-4.5-lt.smt2	[new file with mode: 0644]	blob
test/regress/regress1/nl/exp1-lb.smt2	[new file with mode: 0644]	blob
test/regress/regress1/nl/exp_monotone.smt2	[new file with mode: 0644]	blob
test/regress/regress1/nl/metitarski-1025.smt2	[new file with mode: 0644]	blob
test/regress/regress1/nl/metitarski-3-4.smt2	[new file with mode: 0644]	blob
test/regress/regress1/nl/metitarski_3_4_2e.smt2	[new file with mode: 0644]	blob
test/regress/regress1/nl/nl-help-unsat-quant.smt2	[new file with mode: 0644]	blob
test/regress/regress1/nl/nl-unk-quant.smt2	[new file with mode: 0644]	blob
test/regress/regress1/nl/ones.smt2	[new file with mode: 0644]	blob
test/regress/regress1/nl/poly-1025.smt2	[new file with mode: 0644]	blob
test/regress/regress1/nl/quant-nl.smt2	[new file with mode: 0644]	blob
test/regress/regress1/nl/red-exp.smt2	[new file with mode: 0644]	blob
test/regress/regress1/nl/rewriting-sums.smt2	[new file with mode: 0644]	blob
test/regress/regress1/nl/shifting.smt2	[new file with mode: 0644]	blob
test/regress/regress1/nl/shifting2.smt2	[new file with mode: 0644]	blob
test/regress/regress1/nl/siegel-nl-bases.smt2	[deleted file]	blob \| history
test/regress/regress1/nl/simple-mono-unsat.smt2	[new file with mode: 0644]	blob
test/regress/regress1/nl/simple-mono.smt2	[new file with mode: 0644]	blob
test/regress/regress1/nl/sin-compare-across-phase.smt2	[new file with mode: 0644]	blob
test/regress/regress1/nl/sin-compare.smt2	[new file with mode: 0644]	blob
test/regress/regress1/nl/sin-init-tangents.smt2	[new file with mode: 0644]	blob
test/regress/regress1/nl/sin-sign.smt2	[new file with mode: 0644]	blob
test/regress/regress1/nl/sin-sym2.smt2	[new file with mode: 0644]	blob
test/regress/regress1/nl/sin1-lb.smt2	[new file with mode: 0644]	blob
test/regress/regress1/nl/sin1-sat.smt2	[new file with mode: 0644]	blob
test/regress/regress1/nl/sin1-ub.smt2	[new file with mode: 0644]	blob
test/regress/regress1/nl/sin2-lb.smt2	[new file with mode: 0644]	blob
test/regress/regress1/nl/sin2-ub.smt2	[new file with mode: 0644]	blob
test/regress/regress1/nl/sqrt-problem-1.smt2	[new file with mode: 0644]	blob
test/regress/regress1/nl/sugar-ident-2.smt2	[new file with mode: 0644]	blob
test/regress/regress1/nl/sugar-ident-3.smt2	[new file with mode: 0644]	blob
test/regress/regress1/nl/sugar-ident.smt2	[new file with mode: 0644]	blob
test/regress/regress1/nl/tan-rewrite2.smt2	[new file with mode: 0644]	blob
test/regress/regress1/nl/zero-subset.smt2	[new file with mode: 0644]	blob
test/regress/regress1/non-fatal-errors.smt2	[new file with mode: 0644]	blob
test/regress/regress1/parsing_ringer.cvc	[new file with mode: 0644]	blob
test/regress/regress1/proof00.smt2	[new file with mode: 0644]	blob
test/regress/regress1/push-pop/Makefile.am	[new file with mode: 0644]	blob
test/regress/regress1/push-pop/arith_lra_01.smt2	[new file with mode: 0644]	blob
test/regress/regress1/push-pop/arith_lra_02.smt2	[new file with mode: 0644]	blob
test/regress/regress1/push-pop/bug-fmf-fun-skolem.smt2	[new file with mode: 0644]	blob
test/regress/regress1/push-pop/bug216.smt2	[new file with mode: 0644]	blob
test/regress/regress1/push-pop/bug216.smt2.expect	[new file with mode: 0644]	blob
test/regress/regress1/push-pop/bug326.smt2	[new file with mode: 0644]	blob
test/regress/regress1/push-pop/fuzz_1.smt2	[new file with mode: 0644]	blob
test/regress/regress1/push-pop/fuzz_10.smt2	[new file with mode: 0644]	blob
test/regress/regress1/push-pop/fuzz_11.smt2	[new file with mode: 0644]	blob
test/regress/regress1/push-pop/fuzz_15.smt2	[new file with mode: 0644]	blob
test/regress/regress1/push-pop/fuzz_16.smt2	[new file with mode: 0644]	blob
test/regress/regress1/push-pop/fuzz_19.smt2	[new file with mode: 0644]	blob
test/regress/regress1/push-pop/fuzz_1_to_52_merged.smt2	[new file with mode: 0644]	blob
test/regress/regress1/push-pop/fuzz_20.smt2	[new file with mode: 0644]	blob
test/regress/regress1/push-pop/fuzz_23.smt2	[new file with mode: 0644]	blob
test/regress/regress1/push-pop/fuzz_24.smt2	[new file with mode: 0644]	blob
test/regress/regress1/push-pop/fuzz_25.smt2	[new file with mode: 0644]	blob
test/regress/regress1/push-pop/fuzz_26.smt2	[new file with mode: 0644]	blob
test/regress/regress1/push-pop/fuzz_28.smt2	[new file with mode: 0644]	blob
test/regress/regress1/push-pop/fuzz_29.smt2	[new file with mode: 0644]	blob
test/regress/regress1/push-pop/fuzz_30.smt2	[new file with mode: 0644]	blob
test/regress/regress1/push-pop/fuzz_32.smt2	[new file with mode: 0644]	blob
test/regress/regress1/push-pop/fuzz_34.smt2	[new file with mode: 0644]	blob
test/regress/regress1/push-pop/fuzz_35.smt2	[new file with mode: 0644]	blob
test/regress/regress1/push-pop/fuzz_37.smt2	[new file with mode: 0644]	blob
test/regress/regress1/push-pop/fuzz_39.smt2	[new file with mode: 0644]	blob
test/regress/regress1/push-pop/fuzz_3_1.smt2	[new file with mode: 0644]	blob
test/regress/regress1/push-pop/fuzz_3_10.smt2	[new file with mode: 0644]	blob
test/regress/regress1/push-pop/fuzz_3_11.smt2	[new file with mode: 0644]	blob
test/regress/regress1/push-pop/fuzz_3_12.smt2	[new file with mode: 0644]	blob
test/regress/regress1/push-pop/fuzz_3_13.smt2	[new file with mode: 0644]	blob
test/regress/regress1/push-pop/fuzz_3_14.smt2	[new file with mode: 0644]	blob
test/regress/regress1/push-pop/fuzz_3_15.smt2	[new file with mode: 0644]	blob
test/regress/regress1/push-pop/fuzz_3_2.smt2	[new file with mode: 0644]	blob
test/regress/regress1/push-pop/fuzz_3_3.smt2	[new file with mode: 0644]	blob
test/regress/regress1/push-pop/fuzz_3_4.smt2	[new file with mode: 0644]	blob
test/regress/regress1/push-pop/fuzz_3_5.smt2	[new file with mode: 0644]	blob
test/regress/regress1/push-pop/fuzz_3_6.smt2	[new file with mode: 0644]	blob
test/regress/regress1/push-pop/fuzz_3_7.smt2	[new file with mode: 0644]	blob
test/regress/regress1/push-pop/fuzz_3_8.smt2	[new file with mode: 0644]	blob
test/regress/regress1/push-pop/fuzz_3_9.smt2	[new file with mode: 0644]	blob
test/regress/regress1/push-pop/fuzz_4.smt2	[new file with mode: 0644]	blob
test/regress/regress1/push-pop/fuzz_40.smt2	[new file with mode: 0644]	blob
test/regress/regress1/push-pop/fuzz_41.smt2	[new file with mode: 0644]	blob
test/regress/regress1/push-pop/fuzz_42.smt2	[new file with mode: 0644]	blob
test/regress/regress1/push-pop/fuzz_43.smt2	[new file with mode: 0644]	blob
test/regress/regress1/push-pop/fuzz_44.smt2	[new file with mode: 0644]	blob
test/regress/regress1/push-pop/fuzz_45.smt2	[new file with mode: 0644]	blob
test/regress/regress1/push-pop/fuzz_5.smt2	[new file with mode: 0644]	blob
test/regress/regress1/push-pop/fuzz_51.smt2	[new file with mode: 0644]	blob
test/regress/regress1/push-pop/fuzz_52.smt2	[new file with mode: 0644]	blob
test/regress/regress1/push-pop/fuzz_5_1.smt2	[new file with mode: 0644]	blob
test/regress/regress1/push-pop/fuzz_5_2.smt2	[new file with mode: 0644]	blob
test/regress/regress1/push-pop/fuzz_5_3.smt2	[new file with mode: 0644]	blob
test/regress/regress1/push-pop/fuzz_5_4.smt2	[new file with mode: 0644]	blob
test/regress/regress1/push-pop/fuzz_5_5.smt2	[new file with mode: 0644]	blob
test/regress/regress1/push-pop/fuzz_5_6.smt2	[new file with mode: 0644]	blob
test/regress/regress1/push-pop/fuzz_6.smt2	[new file with mode: 0644]	blob
test/regress/regress1/push-pop/fuzz_7.smt2	[new file with mode: 0644]	blob
test/regress/regress1/push-pop/fuzz_8.smt2	[new file with mode: 0644]	blob
test/regress/regress1/push-pop/fuzz_9.smt2	[new file with mode: 0644]	blob
test/regress/regress1/push-pop/quant-fun-proc-unmacro.smt2	[new file with mode: 0644]	blob
test/regress/regress1/push-pop/quant-fun-proc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/006-cbqi-ite.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/AdditiveMethods_OwnedResults.Mz.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/Arrays_Q1-noinfer.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/Makefile.am		diff \| blob \| history
test/regress/regress1/quantifiers/NUM878.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/RND-small.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/RNDPRE_4_1-dd-nqe.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/RND_4_16.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/anti-sk-simp.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/ari118-bv-2occ-x.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/array-unsat-simp3.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/bi-artm-s.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/bignum_quant.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/bug822.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/bug_743.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/burns13.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/burns4.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/cbqi-sdlx-fixpoint-3-dd.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/cdt-0208-to.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/ext-ex-deq-trigger.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/extract-nproc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/florian-case-ax.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/gauss_init_0030.fof.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/inst-max-level-segf.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/intersection-example-onelane.proof-node22337.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/is-even.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/javafe.ast.StmtVec.009.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/macro-subtype-param.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/mix-coeff.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/model_6_1_bv.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/nested9_true-unreach-call.i_575.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/opisavailable-12.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/parametric-lists.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/psyco-001-bv.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/psyco-107-bv.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/psyco-196.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/qbv-disequality3.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/qbv-simple-2vars-vo.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/qbv-test-invert-bvashr-0.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/qbv-test-invert-bvashr-1.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/qbv-test-invert-bvcomp.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/qbv-test-invert-bvlshr-1.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/qbv-test-invert-bvmul-neq.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/qbv-test-invert-bvmul.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-0-neq.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-0.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-1-neq.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/qbv-test-invert-bvudiv-1.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/qbv-test-invert-bvurem-1-neq.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/qbv-test-invert-bvurem-1.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/qbv-test-urem-rewrite.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/qcft-javafe.filespace.TreeWalker.006.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/qcft-smtlib3dbc51.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/quaternion_ds1_symm_0428.fof.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/rew-to-0211-dd.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/ricart-agrawala6.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/set3.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/set8.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/small-pipeline-fixpoint-3.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/smtlib384a03.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/smtlib46f14a.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/smtlibf957ea.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/stream-x2014-09-18-unsat.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/subtype-param-unk.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/subtype-param.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/symmetric_unsat_7.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/z3.620661-no-fv-trigger.smt2	[new file with mode: 0644]	blob
test/regress/regress1/rels/Makefile.am	[new file with mode: 0644]	blob
test/regress/regress1/rels/addr_book_1.cvc	[new file with mode: 0644]	blob
test/regress/regress1/rels/addr_book_1_1.cvc	[new file with mode: 0644]	blob
test/regress/regress1/rels/bv1-unit.cvc	[new file with mode: 0644]	blob
test/regress/regress1/rels/bv1-unitb.cvc	[new file with mode: 0644]	blob
test/regress/regress1/rels/bv1.cvc	[new file with mode: 0644]	blob
test/regress/regress1/rels/bv1p-sat.cvc	[new file with mode: 0644]	blob
test/regress/regress1/rels/bv1p.cvc	[new file with mode: 0644]	blob
test/regress/regress1/rels/bv2.cvc	[new file with mode: 0644]	blob
test/regress/regress1/rels/garbage_collect.cvc	[new file with mode: 0644]	blob
test/regress/regress1/rels/iden_1_1.cvc	[new file with mode: 0644]	blob
test/regress/regress1/rels/join-eq-structure-and.cvc	[new file with mode: 0644]	blob
test/regress/regress1/rels/join-eq-structure.cvc	[new file with mode: 0644]	blob
test/regress/regress1/rels/join-eq-structure_0_1.cvc	[new file with mode: 0644]	blob
test/regress/regress1/rels/joinImg_0_1.cvc	[new file with mode: 0644]	blob
test/regress/regress1/rels/joinImg_0_2.cvc	[new file with mode: 0644]	blob
test/regress/regress1/rels/joinImg_1.cvc	[new file with mode: 0644]	blob
test/regress/regress1/rels/joinImg_1_1.cvc	[new file with mode: 0644]	blob
test/regress/regress1/rels/joinImg_2.cvc	[new file with mode: 0644]	blob
test/regress/regress1/rels/joinImg_2_1.cvc	[new file with mode: 0644]	blob
test/regress/regress1/rels/prod-mod-eq.cvc	[new file with mode: 0644]	blob
test/regress/regress1/rels/prod-mod-eq2.cvc	[new file with mode: 0644]	blob
test/regress/regress1/rels/rel_complex_3.cvc	[new file with mode: 0644]	blob
test/regress/regress1/rels/rel_complex_4.cvc	[new file with mode: 0644]	blob
test/regress/regress1/rels/rel_complex_5.cvc	[new file with mode: 0644]	blob
test/regress/regress1/rels/rel_mix_0_1.cvc	[new file with mode: 0644]	blob
test/regress/regress1/rels/rel_pressure_0.cvc	[new file with mode: 0644]	blob
test/regress/regress1/rels/rel_tc_10_1.cvc	[new file with mode: 0644]	blob
test/regress/regress1/rels/rel_tc_4.cvc	[new file with mode: 0644]	blob
test/regress/regress1/rels/rel_tc_4_1.cvc	[new file with mode: 0644]	blob
test/regress/regress1/rels/rel_tc_5_1.cvc	[new file with mode: 0644]	blob
test/regress/regress1/rels/rel_tc_6.cvc	[new file with mode: 0644]	blob
test/regress/regress1/rels/rel_tc_9_1.cvc	[new file with mode: 0644]	blob
test/regress/regress1/rels/rel_tp_2.cvc	[new file with mode: 0644]	blob
test/regress/regress1/rels/rel_tp_join_2_1.cvc	[new file with mode: 0644]	blob
test/regress/regress1/rels/set-strat.cvc	[new file with mode: 0644]	blob
test/regress/regress1/rels/strat.cvc	[new file with mode: 0644]	blob
test/regress/regress1/rels/strat_0_1.cvc	[new file with mode: 0644]	blob
test/regress/regress1/rewriterules/Makefile.am		diff \| blob \| history
test/regress/regress1/rewriterules/datatypes2.smt2	[new file with mode: 0644]	blob
test/regress/regress1/rewriterules/datatypes3.smt2	[new file with mode: 0644]	blob
test/regress/regress1/rewriterules/datatypes_clark_quantification.smt2	[new file with mode: 0644]	blob
test/regress/regress1/rewriterules/datatypes_sat.smt2	[new file with mode: 0644]	blob
test/regress/regress1/rewriterules/length_gen.smt2	[new file with mode: 0644]	blob
test/regress/regress1/rewriterules/length_gen_010.smt2	[new file with mode: 0644]	blob
test/regress/regress1/rewriterules/length_gen_010_lemma.smt2	[new file with mode: 0644]	blob
test/regress/regress1/rewriterules/length_gen_020.smt2	[new file with mode: 0644]	blob
test/regress/regress1/rewriterules/length_gen_020_sat.smt2	[new file with mode: 0644]	blob
test/regress/regress1/rewriterules/length_gen_040.smt2	[new file with mode: 0644]	blob
test/regress/regress1/rewriterules/length_gen_040_lemma.smt2	[new file with mode: 0644]	blob
test/regress/regress1/rewriterules/length_gen_040_lemma_trigger.smt2	[new file with mode: 0644]	blob
test/regress/regress1/rewriterules/length_gen_080.smt2	[new file with mode: 0644]	blob
test/regress/regress1/rewriterules/length_gen_160_lemma.smt2	[new file with mode: 0644]	blob
test/regress/regress1/rewriterules/length_gen_inv_160.smt2	[new file with mode: 0644]	blob
test/regress/regress1/rewriterules/length_trick3.smt2	[new file with mode: 0644]	blob
test/regress/regress1/rewriterules/length_trick3_int.smt2	[new file with mode: 0644]	blob
test/regress/regress1/rewriterules/set_A_new_fast_tableau-base.smt2	[new file with mode: 0644]	blob
test/regress/regress1/rewriterules/set_A_new_fast_tableau-base_sat.smt2	[new file with mode: 0644]	blob
test/regress/regress1/rewriterules/test_guards.smt2	[new file with mode: 0644]	blob
test/regress/regress1/rewriterules/why3_vstte10_max_sum_harness2.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sep/Makefile.am		diff \| blob \| history
test/regress/regress1/sep/chain-int.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sep/crash1220.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sep/dispose-list-4-init.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sep/emp2-quant-unsat.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sep/finite-witness-sat.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sep/fmf-nemp-2.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sep/pto-04.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sep/quant_wand.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sep/sep-02.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sep/sep-03.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sep/sep-find2.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sep/sep-fmf-priority.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sep/sep-neg-1refine.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sep/sep-neg-nstrict.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sep/sep-neg-nstrict2.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sep/sep-neg-simple.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sep/sep-neg-swap.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sep/sep-nterm-again.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sep/sep-nterm-val-model.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sep/simple-neg-sat.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sep/wand-0526-sat.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sep/wand-false.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sep/wand-nterm-simp.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sep/wand-nterm-simp2.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sep/wand-simp-sat.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sep/wand-simp-sat2.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sep/wand-simp-unsat.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sets/ListElem.hs.fqout.cvc4.38.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sets/ListElts.hs.fqout.cvc4.317.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sets/Makefile.am		diff \| blob \| history
test/regress/regress1/sets/TalkingAboutSets.hs.fqout.cvc4.3577.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sets/UniqueZipper.hs.1030minimized.cvc4.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sets/UniqueZipper.hs.1030minimized2.cvc4.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sets/UniqueZipper.hs.fqout.cvc4.10.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sets/UniqueZipper.hs.fqout.cvc4.1832.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sets/arjun-set-univ.cvc	[new file with mode: 0644]	blob
test/regress/regress1/sets/card-3.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sets/card-4.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sets/card-5.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sets/card-6.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sets/card-7.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sets/copy_check_heap_access_33_4.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sets/deepmeas0.hs.fqout.cvc4.41.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sets/fuzz14418.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sets/fuzz15201.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sets/fuzz31811.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sets/insert_invariant_37_2.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sets/lemmabug-ListElts317minimized.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sets/remove_check_free_31_6.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sets/setofsets-disequal.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sets/sets-tuple-poly.cvc	[new file with mode: 0644]	blob
test/regress/regress1/sets/sharingbug.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sets/univ-set-uf-elim.smt2	[new file with mode: 0644]	blob
test/regress/regress1/simple-rdl-definefun.smt2	[new file with mode: 0644]	blob
test/regress/regress1/simplification_bug4.smt2	[new file with mode: 0644]	blob
test/regress/regress1/simplification_bug4.smt2.expect	[new file with mode: 0644]	blob
test/regress/regress1/sqrt2-sort-inf-unk.smt2	[new file with mode: 0644]	blob
test/regress/regress1/strings/Makefile.am		diff \| blob \| history
test/regress/regress1/strings/artemis-0512-nonterm.smt2	[new file with mode: 0644]	blob
test/regress/regress1/strings/at001.smt2	[new file with mode: 0644]	blob
test/regress/regress1/strings/bug615.smt2	[new file with mode: 0644]	blob
test/regress/regress1/strings/bug682.smt2	[new file with mode: 0644]	blob
test/regress/regress1/strings/bug686dd.smt2	[new file with mode: 0644]	blob
test/regress/regress1/strings/bug768.smt2	[new file with mode: 0644]	blob
test/regress/regress1/strings/bug799-min.smt2	[new file with mode: 0644]	blob
test/regress/regress1/strings/chapman150408.smt2	[new file with mode: 0644]	blob
test/regress/regress1/strings/cmu-2db2-extf-reg.smt2	[new file with mode: 0644]	blob
test/regress/regress1/strings/cmu-dis-0707-3.smt2	[deleted file]	blob \| history
test/regress/regress1/strings/cmu-disagree-0707-dd.smt2	[new file with mode: 0644]	blob
test/regress/regress1/strings/cmu-inc-nlpp-071516.smt2	[new file with mode: 0644]	blob
test/regress/regress1/strings/cmu-prereg-fmf.smt2	[deleted file]	blob \| history
test/regress/regress1/strings/cmu-repl-len-nterm.smt2	[deleted file]	blob \| history
test/regress/regress1/strings/cmu-substr-rw.smt2	[new file with mode: 0644]	blob
test/regress/regress1/strings/crash-1019.smt2	[new file with mode: 0644]	blob
test/regress/regress1/strings/csp-prefix-exp-bug.smt2	[new file with mode: 0644]	blob
test/regress/regress1/strings/fmf001.smt2	[new file with mode: 0644]	blob
test/regress/regress1/strings/fmf002.smt2	[new file with mode: 0644]	blob
test/regress/regress1/strings/gm-inc-071516-2.smt2	[new file with mode: 0644]	blob
test/regress/regress1/strings/idof-handg.smt2	[new file with mode: 0644]	blob
test/regress/regress1/strings/idof-nconst-index.smt2	[new file with mode: 0644]	blob
test/regress/regress1/strings/idof-neg-index.smt2	[new file with mode: 0644]	blob
test/regress/regress1/strings/idof-triv.smt2	[new file with mode: 0644]	blob
test/regress/regress1/strings/ilc-l-nt.smt2	[new file with mode: 0644]	blob
test/regress/regress1/strings/issue1105.smt2	[new file with mode: 0644]	blob
test/regress/regress1/strings/kaluza-fl.smt2	[new file with mode: 0644]	blob
test/regress/regress1/strings/loop002.smt2	[new file with mode: 0644]	blob
test/regress/regress1/strings/loop003.smt2	[new file with mode: 0644]	blob
test/regress/regress1/strings/loop004.smt2	[new file with mode: 0644]	blob
test/regress/regress1/strings/loop005.smt2	[new file with mode: 0644]	blob
test/regress/regress1/strings/loop006.smt2	[new file with mode: 0644]	blob
test/regress/regress1/strings/loop007.smt2	[new file with mode: 0644]	blob
test/regress/regress1/strings/loop008.smt2	[new file with mode: 0644]	blob
test/regress/regress1/strings/loop009.smt2	[new file with mode: 0644]	blob
test/regress/regress1/strings/nf-ff-contains-abs.smt2	[new file with mode: 0644]	blob
test/regress/regress1/strings/norn-360.smt2	[new file with mode: 0644]	blob
test/regress/regress1/strings/norn-ab.smt2	[new file with mode: 0644]	blob
test/regress/regress1/strings/norn-nel-bug-052116.smt2	[new file with mode: 0644]	blob
test/regress/regress1/strings/norn-simp-rew-sat.smt2	[new file with mode: 0644]	blob
test/regress/regress1/strings/pierre150331.smt2	[new file with mode: 0644]	blob
test/regress/regress1/strings/regexp001.smt2	[new file with mode: 0644]	blob
test/regress/regress1/strings/regexp002.smt2	[new file with mode: 0644]	blob
test/regress/regress1/strings/regexp003.smt2	[new file with mode: 0644]	blob
test/regress/regress1/strings/reloop.smt2	[new file with mode: 0644]	blob
test/regress/regress1/strings/repl-empty-sem.smt2	[new file with mode: 0644]	blob
test/regress/regress1/strings/repl-soundness-sem.smt2	[new file with mode: 0644]	blob
test/regress/regress1/strings/str001.smt2	[new file with mode: 0644]	blob
test/regress/regress1/strings/str002.smt2	[new file with mode: 0644]	blob
test/regress/regress1/strings/str006.smt2	[new file with mode: 0644]	blob
test/regress/regress1/strings/str007.smt2	[new file with mode: 0644]	blob
test/regress/regress1/strings/strings-index-empty.smt2	[new file with mode: 0644]	blob
test/regress/regress1/strings/strip-endpt-sound.smt2	[new file with mode: 0644]	blob
test/regress/regress1/strings/substr001.smt2	[new file with mode: 0644]	blob
test/regress/regress1/strings/type002.smt2	[new file with mode: 0644]	blob
test/regress/regress1/strings/type003.smt2	[new file with mode: 0644]	blob
test/regress/regress1/strings/username_checker_min.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sygus/Base16_1.sy	[new file with mode: 0644]	blob
test/regress/regress1/sygus/MPwL_d1s3.sy	[deleted file]	blob \| history
test/regress/regress1/sygus/Makefile.am		diff \| blob \| history
test/regress/regress1/sygus/array_search_2.sy	[new file with mode: 0644]	blob
test/regress/regress1/sygus/array_sum_2_5.sy	[new file with mode: 0644]	blob
test/regress/regress1/sygus/array_sum_dd.sy	[deleted file]	blob \| history
test/regress/regress1/sygus/cegar1.sy	[new file with mode: 0644]	blob
test/regress/regress1/sygus/cggmp.sy	[new file with mode: 0644]	blob
test/regress/regress1/sygus/clock-inc-tuple.sy	[new file with mode: 0644]	blob
test/regress/regress1/sygus/commutative.sy	[new file with mode: 0644]	blob
test/regress/regress1/sygus/constant.sy	[new file with mode: 0644]	blob
test/regress/regress1/sygus/dt-test-ns.sy	[new file with mode: 0644]	blob
test/regress/regress1/sygus/dup-op.sy	[new file with mode: 0644]	blob
test/regress/regress1/sygus/enum-test.sy	[new file with mode: 0644]	blob
test/regress/regress1/sygus/fg_polynomial3.sy	[new file with mode: 0644]	blob
test/regress/regress1/sygus/hd-01-d1-prog.sy	[new file with mode: 0644]	blob
test/regress/regress1/sygus/hd-19-d1-prog-dup-op.sy	[new file with mode: 0644]	blob
test/regress/regress1/sygus/icfp_14.12-flip-args.sy	[new file with mode: 0644]	blob
test/regress/regress1/sygus/icfp_14.12.sy	[new file with mode: 0644]	blob
test/regress/regress1/sygus/icfp_28_10.sy	[new file with mode: 0644]	blob
test/regress/regress1/sygus/icfp_easy-ite.sy	[new file with mode: 0644]	blob
test/regress/regress1/sygus/icfp_easy_mt_ite.sy	[deleted file]	blob \| history
test/regress/regress1/sygus/inv-example.sy	[new file with mode: 0644]	blob
test/regress/regress1/sygus/inv-unused.sy	[new file with mode: 0644]	blob
test/regress/regress1/sygus/inv_gen_n_c11.sy	[deleted file]	blob \| history
test/regress/regress1/sygus/list-head-x.sy	[new file with mode: 0644]	blob
test/regress/regress1/sygus/lustre-real.sy	[deleted file]	blob \| history
test/regress/regress1/sygus/max.sy	[new file with mode: 0644]	blob
test/regress/regress1/sygus/mpg_guard1-dd.sy	[deleted file]	blob \| history
test/regress/regress1/sygus/multi-fun-polynomial2.sy	[new file with mode: 0644]	blob
test/regress/regress1/sygus/nflat-fwd-3.sy	[new file with mode: 0644]	blob
test/regress/regress1/sygus/nflat-fwd.sy	[new file with mode: 0644]	blob
test/regress/regress1/sygus/nia-max-square-ns.sy	[new file with mode: 0644]	blob
test/regress/regress1/sygus/nia-max-square.sy	[deleted file]	blob \| history
test/regress/regress1/sygus/no-flat-simp.sy	[new file with mode: 0644]	blob
test/regress/regress1/sygus/no-mention.sy	[new file with mode: 0644]	blob
test/regress/regress1/sygus/process-10-vars.sy	[new file with mode: 0644]	blob
test/regress/regress1/sygus/process-arg-invariance.sy	[deleted file]	blob \| history
test/regress/regress1/sygus/qe.sy	[new file with mode: 0644]	blob
test/regress/regress1/sygus/strings-concat-3-args.sy	[new file with mode: 0644]	blob
test/regress/regress1/sygus/strings-double-rec.sy	[new file with mode: 0644]	blob
test/regress/regress1/sygus/strings-small.sy	[new file with mode: 0644]	blob
test/regress/regress1/sygus/strings-template-infer-unused.sy	[new file with mode: 0644]	blob
test/regress/regress1/sygus/strings-template-infer.sy	[new file with mode: 0644]	blob
test/regress/regress1/sygus/strings-trivial-simp.sy	[new file with mode: 0644]	blob
test/regress/regress1/sygus/strings-trivial-two-type.sy	[new file with mode: 0644]	blob
test/regress/regress1/sygus/strings-trivial.sy	[new file with mode: 0644]	blob
test/regress/regress1/sygus/sygus-dt.sy	[new file with mode: 0644]	blob
test/regress/regress1/sygus/three.sy	[deleted file]	blob \| history
test/regress/regress1/sygus/tl-type-0.sy	[new file with mode: 0644]	blob
test/regress/regress1/sygus/tl-type-4x.sy	[new file with mode: 0644]	blob
test/regress/regress1/sygus/tl-type.sy	[new file with mode: 0644]	blob
test/regress/regress1/sygus/triv-type-mismatch-si.sy	[new file with mode: 0644]	blob
test/regress/regress1/sygus/twolets1.sy	[new file with mode: 0644]	blob
test/regress/regress1/sygus/twolets2-orig.sy	[new file with mode: 0644]	blob
test/regress/regress1/sygus/unbdd_inv_gen_winf1.sy	[new file with mode: 0644]	blob
test/regress/regress1/test12.cvc	[new file with mode: 0644]	blob
test/regress/regress1/trim.cvc	[new file with mode: 0644]	blob
test/regress/regress1/uf2.smt2	[new file with mode: 0644]	blob
test/regress/regress1/uflia/DRAGON_11_e1_2450.ec.minimized.smt2	[new file with mode: 0644]	blob
test/regress/regress1/uflia/DRAGON_11_e1_2450.ec.minimized.smt2.expect	[new file with mode: 0644]	blob
test/regress/regress1/uflia/FIREFLY_3_e2_2236_e7_3681.ec.core.smt2	[new file with mode: 0644]	blob
test/regress/regress1/uflia/FIREFLY_3_e2_2236_e7_3681.ec.core.smt2.expect	[new file with mode: 0644]	blob
test/regress/regress1/uflia/FIREFLY_luke_1b_e2_3049_e7_1173.ec.minimized.smt2	[new file with mode: 0644]	blob
test/regress/regress1/uflia/Makefile.am	[new file with mode: 0644]	blob
test/regress/regress1/uflia/microwave21.ec.minimized.smt2	[new file with mode: 0644]	blob
test/regress/regress1/uflia/simple_cyclic2.smt2	[new file with mode: 0644]	blob
test/regress/regress1/uflia/speed2_e8_449_e8_517.ec.smt2	[new file with mode: 0644]	blob
test/regress/regress1/uflia/speed2_e8_449_e8_517.ec.smt2.expect	[new file with mode: 0644]	blob
test/regress/regress1/uflia/stalmark_e7_27_e7_31.ec.smt2	[new file with mode: 0644]	blob
test/regress/regress1/uflia/stalmark_e7_27_e7_31.ec.smt2.expect	[new file with mode: 0644]	blob
test/regress/regress2/Makefile.am		diff \| blob \| history
test/regress/regress2/arith/Makefile.am		diff \| blob \| history
test/regress/regress2/arith/arith-int-098.cvc	[new file with mode: 0644]	blob
test/regress/regress2/arith/miplib-opt1217--27.smt2	[new file with mode: 0644]	blob
test/regress/regress2/arith/miplib-pp08a-3000.smt2	[new file with mode: 0644]	blob
test/regress/regress2/bug396.smt2	[new file with mode: 0644]	blob
test/regress/regress2/bug674.smt2	[new file with mode: 0644]	blob
test/regress/regress2/bug765.smt2	[new file with mode: 0644]	blob
test/regress/regress2/javafe.ast.StandardPrettyPrint.319_no_forall.smt2	[new file with mode: 0644]	blob
test/regress/regress2/javafe.ast.WhileStmt.447_no_forall.smt2	[new file with mode: 0644]	blob
test/regress/regress2/nl/Makefile.am	[new file with mode: 0644]	blob
test/regress/regress2/nl/dumortier-050317.smt2	[new file with mode: 0644]	blob
test/regress/regress2/nl/nt-lemmas-bad.smt2	[new file with mode: 0644]	blob
test/regress/regress2/nl/siegel-nl-bases.smt2	[new file with mode: 0644]	blob
test/regress/regress2/quantifiers/AdditiveMethods_AdditiveMethods..ctor.smt2	[new file with mode: 0644]	blob
test/regress/regress2/quantifiers/ForElimination-scala-9.smt2	[new file with mode: 0644]	blob
test/regress/regress2/quantifiers/Makefile.am	[new file with mode: 0644]	blob
test/regress/regress2/quantifiers/javafe.ast.ArrayInit.35.smt2	[new file with mode: 0644]	blob
test/regress/regress2/quantifiers/javafe.ast.StandardPrettyPrint.319.smt2	[new file with mode: 0644]	blob
test/regress/regress2/quantifiers/javafe.ast.WhileStmt.447.smt2	[new file with mode: 0644]	blob
test/regress/regress2/quantifiers/javafe.tc.CheckCompilationUnit.001.smt2	[new file with mode: 0644]	blob
test/regress/regress2/quantifiers/javafe.tc.FlowInsensitiveChecks.682.smt2	[new file with mode: 0644]	blob
test/regress/regress2/quantifiers/nunchaku2309663.nun.min.smt2	[new file with mode: 0644]	blob
test/regress/regress2/quantifiers/small-bug1-fixpoint-3.smt2	[new file with mode: 0644]	blob
test/regress/regress2/simplify.javafe.ast.ArrayInit.35_without_quantification2.smt2	[new file with mode: 0644]	blob
test/regress/regress2/strings/Makefile.am	[new file with mode: 0644]	blob
test/regress/regress2/strings/cmu-dis-0707-3.smt2	[new file with mode: 0644]	blob
test/regress/regress2/strings/cmu-prereg-fmf.smt2	[new file with mode: 0644]	blob
test/regress/regress2/strings/cmu-repl-len-nterm.smt2	[new file with mode: 0644]	blob
test/regress/regress2/strings/norn-dis-0707-3.smt2	[new file with mode: 0644]	blob
test/regress/regress2/sygus/MPwL_d1s3.sy	[new file with mode: 0644]	blob
test/regress/regress2/sygus/Makefile.am	[new file with mode: 0644]	blob
test/regress/regress2/sygus/array_sum_dd.sy	[new file with mode: 0644]	blob
test/regress/regress2/sygus/icfp_easy_mt_ite.sy	[new file with mode: 0644]	blob
test/regress/regress2/sygus/inv_gen_n_c11.sy	[new file with mode: 0644]	blob
test/regress/regress2/sygus/lustre-real.sy	[new file with mode: 0644]	blob
test/regress/regress2/sygus/max2-univ.sy	[new file with mode: 0644]	blob
test/regress/regress2/sygus/mpg_guard1-dd.sy	[new file with mode: 0644]	blob
test/regress/regress2/sygus/nia-max-square.sy	[new file with mode: 0644]	blob
test/regress/regress2/sygus/no-syntax-test-no-si.sy	[new file with mode: 0644]	blob
test/regress/regress2/sygus/process-10-vars-2fun.sy	[new file with mode: 0644]	blob
test/regress/regress2/sygus/process-arg-invariance.sy	[new file with mode: 0644]	blob
test/regress/regress2/sygus/real-grammar-neg.sy	[new file with mode: 0644]	blob
test/regress/regress2/sygus/three.sy	[new file with mode: 0644]	blob

RSS Atom