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

author	Morgan Deters <mdeters@cs.nyu.edu>
	Mon, 11 Nov 2013 16:04:48 +0000 (11:04 -0500)
committer	Morgan Deters <mdeters@cs.nyu.edu>
	Mon, 11 Nov 2013 16:04:48 +0000 (11:04 -0500)
commit	36e939d31e8ac8fe2866f996af44ea268447c295
tree	4f626fb54d0c2fd21a70149cf14f1b125c494bb4	tree
parent	3ac85900def24af684565f77fe80589595998ad2	commit \| diff

Change exit status to be more consistent with other command-line tools: 0 success, nonzero error

415 files changed:

NEWS		diff \| blob \| history
src/main/driver_unified.cpp		diff \| blob \| history
test/regress/regress0/arith/arith.01.cvc		diff \| blob \| history
test/regress/regress0/arith/arith.02.cvc		diff \| blob \| history
test/regress/regress0/arith/arith.03.cvc		diff \| blob \| history
test/regress/regress0/arith/div.02.smt2		diff \| blob \| history
test/regress/regress0/arith/div.03.smt2		diff \| blob \| history
test/regress/regress0/arith/div.05.smt2		diff \| blob \| history
test/regress/regress0/arith/div.06.smt2		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-001.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-002.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-003.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-004.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-005.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-006.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-007.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-008.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-009.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-010.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-011.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-012.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-013.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-014.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-015.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-016.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-017.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-018.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-019.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-020.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-021.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-022.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-023.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-024.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-025.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-026.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-027.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-028.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-029.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-030.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-031.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-032.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-033.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-034.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-035.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-036.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-037.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-038.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-039.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-040.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-041.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-042.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-042.min.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-043.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-044.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-045.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-046.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-047.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-048.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-049.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-050.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-051.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-052.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-053.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-054.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-055.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-056.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-057.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-058.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-059.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-060.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-061.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-062.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-063.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-064.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-065.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-066.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-067.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-068.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-069.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-070.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-071.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-072.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-073.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-074.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-075.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-076.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-077.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-078.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-079.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-080.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-081.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-082.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-083.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-084.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-085.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-086.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-087.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-088.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-089.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-090.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-091.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-092.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-093.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-094.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-095.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-096.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-097.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-098.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-099.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-int-100.cvc		diff \| blob \| history
test/regress/regress0/arith/integers/arith-interval.cvc		diff \| blob \| history
test/regress/regress0/arith/miplib-opt1217--27.smt.expect		diff \| blob \| history
test/regress/regress0/arith/miplib-opt1217--27.smt2		diff \| blob \| history
test/regress/regress0/arith/miplib-pp08a-3000.smt.expect		diff \| blob \| history
test/regress/regress0/arith/miplib-pp08a-3000.smt2		diff \| blob \| history
test/regress/regress0/arith/miplib.cvc		diff \| blob \| history
test/regress/regress0/arith/miplib2.cvc		diff \| blob \| history
test/regress/regress0/arith/miplib3.cvc		diff \| blob \| history
test/regress/regress0/arith/miplib4.cvc		diff \| blob \| history
test/regress/regress0/arith/mod.01.smt2		diff \| blob \| history
test/regress/regress0/arith/mod.02.smt2		diff \| blob \| history
test/regress/regress0/arith/mod.03.smt2		diff \| blob \| history
test/regress/regress0/arith/mult.01.smt2		diff \| blob \| history
test/regress/regress0/boolean-prec.cvc		diff \| blob \| history
test/regress/regress0/boolean-terms.cvc		diff \| blob \| history
test/regress/regress0/boolean.cvc		diff \| blob \| history
test/regress/regress0/bug216.smt2.expect		diff \| blob \| history
test/regress/regress0/bug217.smt2		diff \| blob \| history
test/regress/regress0/bug274.cvc		diff \| blob \| history
test/regress/regress0/bug310.cvc		diff \| blob \| history
test/regress/regress0/bug32.cvc		diff \| blob \| history
test/regress/regress0/bug322.cvc		diff \| blob \| history
test/regress/regress0/bug322b.cvc		diff \| blob \| history
test/regress/regress0/bug382.smt2		diff \| blob \| history
test/regress/regress0/bug411.smt2		diff \| blob \| history
test/regress/regress0/bug421.smt2		diff \| blob \| history
test/regress/regress0/bug421b.smt2		diff \| blob \| history
test/regress/regress0/bug425.cvc		diff \| blob \| history
test/regress/regress0/bug480.smt2		diff \| blob \| history
test/regress/regress0/bug486.cvc		diff \| blob \| history
test/regress/regress0/bug512.minimized.smt2		diff \| blob \| history
test/regress/regress0/bug512.smt2		diff \| blob \| history
test/regress/regress0/bug516.smt2		diff \| blob \| history
test/regress/regress0/bug519.smt2		diff \| blob \| history
test/regress/regress0/bug522.smt2		diff \| blob \| history
test/regress/regress0/bv/bvcomp.cvc		diff \| blob \| history
test/regress/regress0/bv/bvsimple.cvc		diff \| blob \| history
test/regress/regress0/bv/sizecheck.cvc		diff \| blob \| history
test/regress/regress0/cvc3-bug15.cvc		diff \| blob \| history
test/regress/regress0/datatypes/boolean-equality.cvc		diff \| blob \| history
test/regress/regress0/datatypes/boolean-terms-datatype.cvc		diff \| blob \| history
test/regress/regress0/datatypes/boolean-terms-parametric-datatype-1.cvc		diff \| blob \| history
test/regress/regress0/datatypes/boolean-terms-parametric-datatype-2.cvc		diff \| blob \| history
test/regress/regress0/datatypes/boolean-terms-record.cvc		diff \| blob \| history
test/regress/regress0/datatypes/boolean-terms-rewrite.cvc		diff \| blob \| history
test/regress/regress0/datatypes/boolean-terms-tuple.cvc		diff \| blob \| history
test/regress/regress0/datatypes/bug286.cvc		diff \| blob \| history
test/regress/regress0/datatypes/bug341.cvc		diff \| blob \| history
test/regress/regress0/datatypes/bug438.cvc		diff \| blob \| history
test/regress/regress0/datatypes/bug438b.cvc		diff \| blob \| history
test/regress/regress0/datatypes/datatype-dump.cvc		diff \| blob \| history
test/regress/regress0/datatypes/datatype.cvc		diff \| blob \| history
test/regress/regress0/datatypes/datatype0.cvc		diff \| blob \| history
test/regress/regress0/datatypes/datatype1.cvc		diff \| blob \| history
test/regress/regress0/datatypes/datatype13.cvc		diff \| blob \| history
test/regress/regress0/datatypes/datatype2.cvc		diff \| blob \| history
test/regress/regress0/datatypes/datatype3.cvc		diff \| blob \| history
test/regress/regress0/datatypes/datatype4.cvc		diff \| blob \| history
test/regress/regress0/datatypes/empty_tuprec.cvc		diff \| blob \| history
test/regress/regress0/datatypes/mutually-recursive.cvc		diff \| blob \| history
test/regress/regress0/datatypes/rec1.cvc		diff \| blob \| history
test/regress/regress0/datatypes/rec2.cvc		diff \| blob \| history
test/regress/regress0/datatypes/rec4.cvc		diff \| blob \| history
test/regress/regress0/datatypes/rec5.cvc		diff \| blob \| history
test/regress/regress0/datatypes/rewriter.cvc		diff \| blob \| history
test/regress/regress0/datatypes/some-boolean-tests.cvc		diff \| blob \| history
test/regress/regress0/datatypes/tuple-model.cvc		diff \| blob \| history
test/regress/regress0/datatypes/tuple.cvc		diff \| blob \| history
test/regress/regress0/datatypes/typed_v10l30054.cvc		diff \| blob \| history
test/regress/regress0/datatypes/typed_v1l80005.cvc		diff \| blob \| history
test/regress/regress0/datatypes/typed_v2l30079.cvc		diff \| blob \| history
test/regress/regress0/datatypes/typed_v3l20092.cvc		diff \| blob \| history
test/regress/regress0/datatypes/typed_v5l30069.cvc		diff \| blob \| history
test/regress/regress0/datatypes/v10l40099.cvc		diff \| blob \| history
test/regress/regress0/datatypes/v2l40025.cvc		diff \| blob \| history
test/regress/regress0/datatypes/v3l60006.cvc		diff \| blob \| history
test/regress/regress0/datatypes/v5l30058.cvc		diff \| blob \| history
test/regress/regress0/datatypes/wrong-sel-simp.cvc		diff \| blob \| history
test/regress/regress0/decision/aufbv-fuzz01.smt.expect		diff \| blob \| history
test/regress/regress0/decision/bitvec0.delta01.smt.expect		diff \| blob \| history
test/regress/regress0/decision/bitvec0.smt.expect		diff \| blob \| history
test/regress/regress0/decision/bitvec5.smt.expect		diff \| blob \| history
test/regress/regress0/decision/bug347.smt.expect		diff \| blob \| history
test/regress/regress0/decision/bug374a.smt.expect		diff \| blob \| history
test/regress/regress0/decision/bug374b.smt2.expect		diff \| blob \| history
test/regress/regress0/decision/just_sat.expect		diff \| blob \| history
test/regress/regress0/decision/just_unsat.expect		diff \| blob \| history
test/regress/regress0/decision/pp-regfile.delta01.smt.expect		diff \| blob \| history
test/regress/regress0/decision/pp-regfile.delta02.smt.expect		diff \| blob \| history
test/regress/regress0/decision/quant-Arrays_Q1-noinfer.smt2.expect		diff \| blob \| history
test/regress/regress0/decision/quant-ex1.disable_miniscope.smt2.expect		diff \| blob \| history
test/regress/regress0/decision/quant-ex1.smt2.expect		diff \| blob \| history
test/regress/regress0/decision/quant-symmetric_unsat_7.smt2.expect		diff \| blob \| history
test/regress/regress0/decision/uflia-xs-09-16-3-4-1-5.delta03.smt.expect		diff \| blob \| history
test/regress/regress0/decision/uflia-xs-09-16-3-4-1-5.smt.expect		diff \| blob \| history
test/regress/regress0/decision/wchains010ue.delta02.smt.expect		diff \| blob \| history
test/regress/regress0/decision/wchains010ue.smt.expect		diff \| blob \| history
test/regress/regress0/fmf/ALG008-1.smt2		diff \| blob \| history
test/regress/regress0/fmf/Arrow_Order-smtlib.778341.smt		diff \| blob \| history
test/regress/regress0/fmf/Hoare-z3.931718.smt		diff \| blob \| history
test/regress/regress0/fmf/PUZ001+1.smt2		diff \| blob \| history
test/regress/regress0/fmf/QEpres-uf.855035.smt		diff \| blob \| history
test/regress/regress0/fmf/agree466.smt2		diff \| blob \| history
test/regress/regress0/fmf/agree467.smt2		diff \| blob \| history
test/regress/regress0/fmf/array_card.smt2		diff \| blob \| history
test/regress/regress0/fmf/bug0909.smt2		diff \| blob \| history
test/regress/regress0/fmf/german169.smt2		diff \| blob \| history
test/regress/regress0/fmf/german73.smt2		diff \| blob \| history
test/regress/regress0/fmf/refcount24.cvc.smt2		diff \| blob \| history
test/regress/regress0/get-value-incremental.smt2		diff \| blob \| history
test/regress/regress0/hole6.cvc		diff \| blob \| history
test/regress/regress0/ite.cvc		diff \| blob \| history
test/regress/regress0/let.cvc		diff \| blob \| history
test/regress/regress0/logops.01.cvc		diff \| blob \| history
test/regress/regress0/logops.02.cvc		diff \| blob \| history
test/regress/regress0/logops.03.cvc		diff \| blob \| history
test/regress/regress0/logops.04.cvc		diff \| blob \| history
test/regress/regress0/logops.05.cvc		diff \| blob \| history
test/regress/regress0/precedence/and-not.cvc		diff \| blob \| history
test/regress/regress0/precedence/and-xor.cvc		diff \| blob \| history
test/regress/regress0/precedence/bool-cmp.cvc		diff \| blob \| history
test/regress/regress0/precedence/cmp-plus.cvc		diff \| blob \| history
test/regress/regress0/precedence/eq-fun.cvc		diff \| blob \| history
test/regress/regress0/precedence/iff-assoc.cvc		diff \| blob \| history
test/regress/regress0/precedence/iff-implies.cvc		diff \| blob \| history
test/regress/regress0/precedence/implies-assoc.cvc		diff \| blob \| history
test/regress/regress0/precedence/implies-iff.cvc		diff \| blob \| history
test/regress/regress0/precedence/implies-or.cvc		diff \| blob \| history
test/regress/regress0/precedence/not-and.cvc		diff \| blob \| history
test/regress/regress0/precedence/not-eq.cvc		diff \| blob \| history
test/regress/regress0/precedence/or-implies.cvc		diff \| blob \| history
test/regress/regress0/precedence/or-xor.cvc		diff \| blob \| history
test/regress/regress0/precedence/plus-mult.cvc		diff \| blob \| history
test/regress/regress0/precedence/xor-and.cvc		diff \| blob \| history
test/regress/regress0/precedence/xor-assoc.cvc		diff \| blob \| history
test/regress/regress0/precedence/xor-or.cvc		diff \| blob \| history
test/regress/regress0/preprocess/preprocess_00.cvc		diff \| blob \| history
test/regress/regress0/preprocess/preprocess_01.cvc		diff \| blob \| history
test/regress/regress0/preprocess/preprocess_02.cvc		diff \| blob \| history
test/regress/regress0/preprocess/preprocess_03.cvc		diff \| blob \| history
test/regress/regress0/preprocess/preprocess_04.cvc		diff \| blob \| history
test/regress/regress0/preprocess/preprocess_05.cvc		diff \| blob \| history
test/regress/regress0/preprocess/preprocess_06.cvc		diff \| blob \| history
test/regress/regress0/preprocess/preprocess_07.cvc		diff \| blob \| history
test/regress/regress0/preprocess/preprocess_08.cvc		diff \| blob \| history
test/regress/regress0/preprocess/preprocess_09.cvc		diff \| blob \| history
test/regress/regress0/preprocess/preprocess_10.cvc		diff \| blob \| history
test/regress/regress0/preprocess/preprocess_11.cvc		diff \| blob \| history
test/regress/regress0/preprocess/preprocess_12.cvc		diff \| blob \| history
test/regress/regress0/preprocess/preprocess_13.cvc		diff \| blob \| history
test/regress/regress0/preprocess/preprocess_14.cvc		diff \| blob \| history
test/regress/regress0/preprocess/preprocess_15.cvc		diff \| blob \| history
test/regress/regress0/print_lambda.cvc		diff \| blob \| history
test/regress/regress0/push-pop/arith/fuzz_3_1.smt2		diff \| blob \| history
test/regress/regress0/push-pop/arith/fuzz_3_10.smt2		diff \| blob \| history
test/regress/regress0/push-pop/arith/fuzz_3_11.smt2		diff \| blob \| history
test/regress/regress0/push-pop/arith/fuzz_3_12.smt2		diff \| blob \| history
test/regress/regress0/push-pop/arith/fuzz_3_13.smt2		diff \| blob \| history
test/regress/regress0/push-pop/arith/fuzz_3_14.smt2		diff \| blob \| history
test/regress/regress0/push-pop/arith/fuzz_3_15.smt2		diff \| blob \| history
test/regress/regress0/push-pop/arith/fuzz_3_2.smt2		diff \| blob \| history
test/regress/regress0/push-pop/arith/fuzz_3_3.smt2		diff \| blob \| history
test/regress/regress0/push-pop/arith/fuzz_3_4.smt2		diff \| blob \| history
test/regress/regress0/push-pop/arith/fuzz_3_5.smt2		diff \| blob \| history
test/regress/regress0/push-pop/arith/fuzz_3_6.smt2		diff \| blob \| history
test/regress/regress0/push-pop/arith/fuzz_3_7.smt2		diff \| blob \| history
test/regress/regress0/push-pop/arith/fuzz_3_8.smt2		diff \| blob \| history
test/regress/regress0/push-pop/arith/fuzz_3_9.smt2		diff \| blob \| history
test/regress/regress0/push-pop/arith/fuzz_5_1.smt2		diff \| blob \| history
test/regress/regress0/push-pop/arith/fuzz_5_2.smt2		diff \| blob \| history
test/regress/regress0/push-pop/arith/fuzz_5_3.smt2		diff \| blob \| history
test/regress/regress0/push-pop/arith/fuzz_5_4.smt2		diff \| blob \| history
test/regress/regress0/push-pop/arith/fuzz_5_5.smt2		diff \| blob \| history
test/regress/regress0/push-pop/arith/fuzz_5_6.smt2		diff \| blob \| history
test/regress/regress0/push-pop/arith_lra_01.smt2		diff \| blob \| history
test/regress/regress0/push-pop/arith_lra_02.smt2		diff \| blob \| history
test/regress/regress0/push-pop/boolean/fuzz_1.smt2		diff \| blob \| history
test/regress/regress0/push-pop/boolean/fuzz_10.smt2		diff \| blob \| history
test/regress/regress0/push-pop/boolean/fuzz_11.smt2		diff \| blob \| history
test/regress/regress0/push-pop/boolean/fuzz_12.smt2		diff \| blob \| history
test/regress/regress0/push-pop/boolean/fuzz_13.smt2		diff \| blob \| history
test/regress/regress0/push-pop/boolean/fuzz_14.smt2		diff \| blob \| history
test/regress/regress0/push-pop/boolean/fuzz_15.smt2		diff \| blob \| history
test/regress/regress0/push-pop/boolean/fuzz_16.smt2		diff \| blob \| history
test/regress/regress0/push-pop/boolean/fuzz_18.smt2		diff \| blob \| history
test/regress/regress0/push-pop/boolean/fuzz_19.smt2		diff \| blob \| history
test/regress/regress0/push-pop/boolean/fuzz_1_to_52_merged.smt2		diff \| blob \| history
test/regress/regress0/push-pop/boolean/fuzz_2.smt2		diff \| blob \| history
test/regress/regress0/push-pop/boolean/fuzz_20.smt2		diff \| blob \| history
test/regress/regress0/push-pop/boolean/fuzz_21.smt2		diff \| blob \| history
test/regress/regress0/push-pop/boolean/fuzz_22.smt2		diff \| blob \| history
test/regress/regress0/push-pop/boolean/fuzz_23.smt2		diff \| blob \| history
test/regress/regress0/push-pop/boolean/fuzz_24.smt2		diff \| blob \| history
test/regress/regress0/push-pop/boolean/fuzz_25.smt2		diff \| blob \| history
test/regress/regress0/push-pop/boolean/fuzz_26.smt2		diff \| blob \| history
test/regress/regress0/push-pop/boolean/fuzz_27.smt2		diff \| blob \| history
test/regress/regress0/push-pop/boolean/fuzz_28.smt2		diff \| blob \| history
test/regress/regress0/push-pop/boolean/fuzz_29.smt2		diff \| blob \| history
test/regress/regress0/push-pop/boolean/fuzz_3.smt2		diff \| blob \| history
test/regress/regress0/push-pop/boolean/fuzz_30.smt2		diff \| blob \| history
test/regress/regress0/push-pop/boolean/fuzz_31.smt2		diff \| blob \| history
test/regress/regress0/push-pop/boolean/fuzz_32.smt2		diff \| blob \| history
test/regress/regress0/push-pop/boolean/fuzz_33.smt2		diff \| blob \| history
test/regress/regress0/push-pop/boolean/fuzz_34.smt2		diff \| blob \| history
test/regress/regress0/push-pop/boolean/fuzz_35.smt2		diff \| blob \| history
test/regress/regress0/push-pop/boolean/fuzz_36.smt2		diff \| blob \| history
test/regress/regress0/push-pop/boolean/fuzz_37.smt2		diff \| blob \| history
test/regress/regress0/push-pop/boolean/fuzz_38.smt2		diff \| blob \| history
test/regress/regress0/push-pop/boolean/fuzz_39.smt2		diff \| blob \| history
test/regress/regress0/push-pop/boolean/fuzz_4.smt2		diff \| blob \| history
test/regress/regress0/push-pop/boolean/fuzz_40.smt2		diff \| blob \| history
test/regress/regress0/push-pop/boolean/fuzz_41.smt2		diff \| blob \| history
test/regress/regress0/push-pop/boolean/fuzz_42.smt2		diff \| blob \| history
test/regress/regress0/push-pop/boolean/fuzz_43.smt2		diff \| blob \| history
test/regress/regress0/push-pop/boolean/fuzz_44.smt2		diff \| blob \| history
test/regress/regress0/push-pop/boolean/fuzz_45.smt2		diff \| blob \| history
test/regress/regress0/push-pop/boolean/fuzz_46.smt2		diff \| blob \| history
test/regress/regress0/push-pop/boolean/fuzz_47.smt2		diff \| blob \| history
test/regress/regress0/push-pop/boolean/fuzz_48.smt2		diff \| blob \| history
test/regress/regress0/push-pop/boolean/fuzz_49.smt2		diff \| blob \| history
test/regress/regress0/push-pop/boolean/fuzz_5.smt2		diff \| blob \| history
test/regress/regress0/push-pop/boolean/fuzz_50.smt2		diff \| blob \| history
test/regress/regress0/push-pop/boolean/fuzz_51.smt2		diff \| blob \| history
test/regress/regress0/push-pop/boolean/fuzz_52.smt2		diff \| blob \| history
test/regress/regress0/push-pop/boolean/fuzz_6.smt2		diff \| blob \| history
test/regress/regress0/push-pop/boolean/fuzz_7.smt2		diff \| blob \| history
test/regress/regress0/push-pop/boolean/fuzz_8.smt2		diff \| blob \| history
test/regress/regress0/push-pop/boolean/fuzz_9.smt2		diff \| blob \| history
test/regress/regress0/push-pop/bug216.smt2.expect		diff \| blob \| history
test/regress/regress0/push-pop/bug233.cvc		diff \| blob \| history
test/regress/regress0/push-pop/bug326.smt2		diff \| blob \| history
test/regress/regress0/push-pop/bug396.smt2		diff \| blob \| history
test/regress/regress0/push-pop/incremental-subst-bug.cvc		diff \| blob \| history
test/regress/regress0/push-pop/test.00.cvc		diff \| blob \| history
test/regress/regress0/push-pop/test.01.cvc		diff \| blob \| history
test/regress/regress0/push-pop/tiny_bug.smt2		diff \| blob \| history
test/regress/regress0/push-pop/units.cvc		diff \| blob \| history
test/regress/regress0/quantifiers/array-unsat-simp3.smt2.expect		diff \| blob \| history
test/regress/regress0/quantifiers/bug291.smt2.expect		diff \| blob \| history
test/regress/regress0/quantifiers/ex1.smt2.expect		diff \| blob \| history
test/regress/regress0/quantifiers/ex7.smt2.expect		diff \| blob \| history
test/regress/regress0/queries0.cvc		diff \| blob \| history
test/regress/regress0/simple.cvc		diff \| blob \| history
test/regress/regress0/simplification_bug3.cvc		diff \| blob \| history
test/regress/regress0/simplification_bug4.smt2.expect		diff \| blob \| history
test/regress/regress0/smallcnf.cvc		diff \| blob \| history
test/regress/regress0/smt2output.smt2		diff \| blob \| history
test/regress/regress0/subranges.cvc		diff \| blob \| history
test/regress/regress0/test11.cvc		diff \| blob \| history
test/regress/regress0/test12.cvc		diff \| blob \| history
test/regress/regress0/test9.cvc		diff \| blob \| history
test/regress/regress0/uf/simple.01.cvc		diff \| blob \| history
test/regress/regress0/uf/simple.02.cvc		diff \| blob \| history
test/regress/regress0/uf/simple.03.cvc		diff \| blob \| history
test/regress/regress0/uf/simple.04.cvc		diff \| blob \| history
test/regress/regress0/uf20-03.cvc		diff \| blob \| history
test/regress/regress0/uflia/DRAGON_11_e1_2450.ec.minimized.smt2.expect		diff \| blob \| history
test/regress/regress0/uflia/FIREFLY_3_e2_2236_e7_3681.ec.core.smt2.expect		diff \| blob \| history
test/regress/regress0/uflia/check01.smt2		diff \| blob \| history
test/regress/regress0/uflia/check02.smt2.expect		diff \| blob \| history
test/regress/regress0/uflia/check03.smt2.expect		diff \| blob \| history
test/regress/regress0/uflia/check04.smt2.expect		diff \| blob \| history
test/regress/regress0/uflia/speed2_e8_449_e8_517.ec.smt2.expect		diff \| blob \| history
test/regress/regress0/uflia/stalmark_e7_27_e7_31.ec.minimized.smt2.expect		diff \| blob \| history
test/regress/regress0/uflia/stalmark_e7_27_e7_31.ec.smt2.expect		diff \| blob \| history
test/regress/regress0/uflia/tiny.smt2.expect		diff \| blob \| history
test/regress/regress0/uflra/bug293.cvc		diff \| blob \| history
test/regress/regress0/uflra/simple.01.cvc		diff \| blob \| history
test/regress/regress0/uflra/simple.02.cvc		diff \| blob \| history
test/regress/regress0/uflra/simple.03.cvc		diff \| blob \| history
test/regress/regress0/uflra/simple.04.cvc		diff \| blob \| history
test/regress/regress0/wiki.01.cvc		diff \| blob \| history
test/regress/regress0/wiki.02.cvc		diff \| blob \| history
test/regress/regress0/wiki.03.cvc		diff \| blob \| history
test/regress/regress0/wiki.04.cvc		diff \| blob \| history
test/regress/regress0/wiki.05.cvc		diff \| blob \| history
test/regress/regress0/wiki.06.cvc		diff \| blob \| history
test/regress/regress0/wiki.07.cvc		diff \| blob \| history
test/regress/regress0/wiki.08.cvc		diff \| blob \| history
test/regress/regress0/wiki.09.cvc		diff \| blob \| history
test/regress/regress0/wiki.10.cvc		diff \| blob \| history
test/regress/regress0/wiki.11.cvc		diff \| blob \| history
test/regress/regress0/wiki.12.cvc		diff \| blob \| history
test/regress/regress0/wiki.13.cvc		diff \| blob \| history
test/regress/regress0/wiki.14.cvc		diff \| blob \| history
test/regress/regress0/wiki.15.cvc		diff \| blob \| history
test/regress/regress0/wiki.16.cvc		diff \| blob \| history
test/regress/regress0/wiki.17.cvc		diff \| blob \| history
test/regress/regress0/wiki.18.cvc		diff \| blob \| history
test/regress/regress0/wiki.19.cvc		diff \| blob \| history
test/regress/regress0/wiki.20.cvc		diff \| blob \| history
test/regress/regress0/wiki.21.cvc		diff \| blob \| history
test/regress/regress1/FIREFLY_3_e2_2236_e7_3681.ec.minimized.smt2.expect		diff \| blob \| history
test/regress/regress1/GEO123+1.minimized.smt2		diff \| blob \| history
test/regress/regress1/bug394.smt2		diff \| blob \| history
test/regress/regress1/hole7.cvc		diff \| blob \| history
test/regress/regress1/hole8.cvc		diff \| blob \| history
test/regress/regress1/typed_v1l50016-simp.cvc		diff \| blob \| history
test/regress/regress1/uflia-error0.smt2.expect		diff \| blob \| history
test/regress/regress1/xs-09-16-3-4-1-5.decn.smt.expect		diff \| blob \| history
test/regress/regress2/bug497.cvc		diff \| blob \| history
test/regress/regress2/hole9.cvc		diff \| blob \| history
test/regress/regress2/pp-regfile.smt.expect		diff \| blob \| history
test/regress/regress3/hole10.cvc		diff \| blob \| history
test/regress/run_regression		diff \| blob \| history

RSS Atom