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

author	Mathias Preiner <mathias.preiner@gmail.com>
	Wed, 22 Sep 2021 20:38:46 +0000 (13:38 -0700)
committer	GitHub <noreply@github.com>
	Wed, 22 Sep 2021 20:38:46 +0000 (20:38 +0000)
commit	e116c00719a7574064c09da4abb10b3297415c90
tree	e71e489d7c591067eeab793a80d139e47718befe	tree
parent	ba259d66be877de3cc77e4f62083905ace942c82	commit \| diff

Remove CVC language support (#7219)

This commit removes the support for the CVC language and converts all *.cvc regression tests to SMT-LIBv2.

661 files changed:

examples/api/cpp/combination.cpp		diff \| blob \| history
examples/api/python/combination.py		diff \| blob \| history
src/CMakeLists.txt		diff \| blob \| history
src/expr/dtype.cpp		diff \| blob \| history
src/expr/dtype_cons.cpp		diff \| blob \| history
src/expr/dtype_selector.cpp		diff \| blob \| history
src/main/CMakeLists.txt		diff \| blob \| history
src/main/driver_unified.cpp		diff \| blob \| history
src/main/interactive_shell.cpp		diff \| blob \| history
src/options/language.cpp		diff \| blob \| history
src/options/language.h		diff \| blob \| history
src/parser/CMakeLists.txt		diff \| blob \| history
src/parser/antlr_input.cpp		diff \| blob \| history
src/parser/cvc/Cvc.g	[deleted file]	blob \| history
src/parser/cvc/README	[deleted file]	blob \| history
src/parser/cvc/cvc.cpp	[deleted file]	blob \| history
src/parser/cvc/cvc.h	[deleted file]	blob \| history
src/parser/cvc/cvc_input.cpp	[deleted file]	blob \| history
src/parser/cvc/cvc_input.h	[deleted file]	blob \| history
src/parser/parser_builder.cpp		diff \| blob \| history
src/parser/smt2/smt2.cpp		diff \| blob \| history
src/printer/cvc/cvc_printer.cpp	[deleted file]	blob \| history
src/printer/cvc/cvc_printer.h	[deleted file]	blob \| history
src/printer/printer.cpp		diff \| blob \| history
test/api/interactive_shell.py		diff \| blob \| history
test/api/ouroborous.cpp		diff \| blob \| history
test/regress/CMakeLists.txt		diff \| blob \| history
test/regress/regress0/arith/arith.01.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/arith.01.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/arith/arith.02.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/arith.02.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/arith/arith.03.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/arith.03.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/arith/bug549.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/bug549.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/arith/integers/arith-int-014.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-014.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/arith/integers/arith-int-015.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-015.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/arith/integers/arith-int-021.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-021.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/arith/integers/arith-int-023.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-023.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/arith/integers/arith-int-025.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-025.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/arith/integers/arith-int-042.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-042.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/arith/integers/arith-int-042.min.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-042.min.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/arith/integers/arith-int-079.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-int-079.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/arith/integers/arith-interval.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/integers/arith-interval.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/arith/miplib.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/miplib.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/arith/miplib2.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/miplib2.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/arith/miplib4.cvc	[deleted file]	blob \| history
test/regress/regress0/arith/miplib4.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/arrays/constarr.cvc	[deleted file]	blob \| history
test/regress/regress0/arrays/constarr.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/arrays/constarr2.cvc	[deleted file]	blob \| history
test/regress/regress0/arrays/constarr2.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/boolean-prec.cvc	[deleted file]	blob \| history
test/regress/regress0/boolean-prec.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/boolean-terms.cvc	[deleted file]	blob \| history
test/regress/regress0/boolean-terms.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/bug274.cvc	[deleted file]	blob \| history
test/regress/regress0/bug274.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/bug310.cvc	[deleted file]	blob \| history
test/regress/regress0/bug310.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/bug32.cvc	[deleted file]	blob \| history
test/regress/regress0/bug32.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/bug322.cvc	[deleted file]	blob \| history
test/regress/regress0/bug322.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/bug322b.cvc	[deleted file]	blob \| history
test/regress/regress0/bug322b.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/bug486.cvc	[deleted file]	blob \| history
test/regress/regress0/bug486.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/bug586.cvc	[deleted file]	blob \| history
test/regress/regress0/bug586.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/bug595.cvc	[deleted file]	blob \| history
test/regress/regress0/bug595.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/bug596.cvc	[deleted file]	blob \| history
test/regress/regress0/bug596.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/bug596b.cvc	[deleted file]	blob \| history
test/regress/regress0/bug596b.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/bug605.cvc	[deleted file]	blob \| history
test/regress/regress0/bug605.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/bv/bvcomp.cvc	[deleted file]	blob \| history
test/regress/regress0/bv/bvcomp.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/bv/bvsimple.cvc	[deleted file]	blob \| history
test/regress/regress0/bv/bvsimple.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/bv/div_mod.cvc	[deleted file]	blob \| history
test/regress/regress0/bv/div_mod.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/bv/sizecheck.cvc	[deleted file]	blob \| history
test/regress/regress0/bv/sizecheck.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/cvc-rerror-print.cvc	[deleted file]	blob \| history
test/regress/regress0/cvc-rerror-print.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/cvc3-bug15.cvc	[deleted file]	blob \| history
test/regress/regress0/cvc3-bug15.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/cvc3.userdoc.01.cvc	[deleted file]	blob \| history
test/regress/regress0/cvc3.userdoc.01.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/cvc3.userdoc.02.cvc	[deleted file]	blob \| history
test/regress/regress0/cvc3.userdoc.02.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/cvc3.userdoc.03.cvc	[deleted file]	blob \| history
test/regress/regress0/cvc3.userdoc.03.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/cvc3.userdoc.04.cvc	[deleted file]	blob \| history
test/regress/regress0/cvc3.userdoc.04.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/cvc3.userdoc.05.cvc	[deleted file]	blob \| history
test/regress/regress0/cvc3.userdoc.05.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/cvc3.userdoc.06.cvc	[deleted file]	blob \| history
test/regress/regress0/cvc3.userdoc.06.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/datatypes/Test1-tup-mp.cvc	[deleted file]	blob \| history
test/regress/regress0/datatypes/Test1-tup-mp.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/datatypes/boolean-equality.cvc	[deleted file]	blob \| history
test/regress/regress0/datatypes/boolean-equality.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/datatypes/boolean-terms-datatype.cvc	[deleted file]	blob \| history
test/regress/regress0/datatypes/boolean-terms-datatype.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/datatypes/boolean-terms-parametric-datatype-1.cvc	[deleted file]	blob \| history
test/regress/regress0/datatypes/boolean-terms-parametric-datatype-1.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/datatypes/boolean-terms-record.cvc	[deleted file]	blob \| history
test/regress/regress0/datatypes/boolean-terms-record.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/datatypes/boolean-terms-rewrite.cvc	[deleted file]	blob \| history
test/regress/regress0/datatypes/boolean-terms-rewrite.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/datatypes/boolean-terms-tuple.cvc	[deleted file]	blob \| history
test/regress/regress0/datatypes/boolean-terms-tuple.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/datatypes/bug286.cvc	[deleted file]	blob \| history
test/regress/regress0/datatypes/bug286.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/datatypes/bug438.cvc	[deleted file]	blob \| history
test/regress/regress0/datatypes/bug438.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/datatypes/bug438b.cvc	[deleted file]	blob \| history
test/regress/regress0/datatypes/bug438b.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/datatypes/datatype-dump.cvc	[deleted file]	blob \| history
test/regress/regress0/datatypes/datatype-dump.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/datatypes/datatype.cvc	[deleted file]	blob \| history
test/regress/regress0/datatypes/datatype.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/datatypes/datatype0.cvc	[deleted file]	blob \| history
test/regress/regress0/datatypes/datatype0.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/datatypes/datatype1.cvc	[deleted file]	blob \| history
test/regress/regress0/datatypes/datatype1.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/datatypes/datatype13.cvc	[deleted file]	blob \| history
test/regress/regress0/datatypes/datatype13.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/datatypes/datatype2.cvc	[deleted file]	blob \| history
test/regress/regress0/datatypes/datatype2.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/datatypes/datatype3.cvc	[deleted file]	blob \| history
test/regress/regress0/datatypes/datatype3.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/datatypes/datatype4.cvc	[deleted file]	blob \| history
test/regress/regress0/datatypes/datatype4.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/datatypes/empty_tuprec.cvc	[deleted file]	blob \| history
test/regress/regress0/datatypes/empty_tuprec.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/datatypes/issue2838.cvc	[deleted file]	blob \| history
test/regress/regress0/datatypes/issue2838.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/datatypes/mutually-recursive.cvc	[deleted file]	blob \| history
test/regress/regress0/datatypes/mutually-recursive.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/datatypes/pair-bool-bool.cvc	[deleted file]	blob \| history
test/regress/regress0/datatypes/pair-bool-bool.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/datatypes/parametric-alt-list.cvc	[deleted file]	blob \| history
test/regress/regress0/datatypes/parametric-alt-list.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/datatypes/rec1.cvc	[deleted file]	blob \| history
test/regress/regress0/datatypes/rec1.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/datatypes/rec2.cvc	[deleted file]	blob \| history
test/regress/regress0/datatypes/rec2.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/datatypes/rec4.cvc	[deleted file]	blob \| history
test/regress/regress0/datatypes/rec4.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/datatypes/rewriter.cvc	[deleted file]	blob \| history
test/regress/regress0/datatypes/rewriter.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/datatypes/some-boolean-tests.cvc	[deleted file]	blob \| history
test/regress/regress0/datatypes/some-boolean-tests.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/datatypes/tree-get-value.cvc	[deleted file]	blob \| history
test/regress/regress0/datatypes/tree-get-value.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/datatypes/tuple-model.cvc	[deleted file]	blob \| history
test/regress/regress0/datatypes/tuple-model.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/datatypes/tuple-no-clash.cvc	[deleted file]	blob \| history
test/regress/regress0/datatypes/tuple-no-clash.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/datatypes/tuple-record-bug.cvc	[deleted file]	blob \| history
test/regress/regress0/datatypes/tuple-record-bug.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/datatypes/tuple.cvc	[deleted file]	blob \| history
test/regress/regress0/datatypes/tuple.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/datatypes/typed_v10l30054.cvc	[deleted file]	blob \| history
test/regress/regress0/datatypes/typed_v10l30054.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/datatypes/typed_v1l80005.cvc	[deleted file]	blob \| history
test/regress/regress0/datatypes/typed_v1l80005.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/datatypes/typed_v2l30079.cvc	[deleted file]	blob \| history
test/regress/regress0/datatypes/typed_v2l30079.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/datatypes/typed_v3l20092.cvc	[deleted file]	blob \| history
test/regress/regress0/datatypes/typed_v3l20092.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/datatypes/typed_v5l30069.cvc	[deleted file]	blob \| history
test/regress/regress0/datatypes/typed_v5l30069.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/datatypes/v10l40099.cvc	[deleted file]	blob \| history
test/regress/regress0/datatypes/v10l40099.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/datatypes/v2l40025.cvc	[deleted file]	blob \| history
test/regress/regress0/datatypes/v2l40025.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/datatypes/v3l60006.cvc	[deleted file]	blob \| history
test/regress/regress0/datatypes/v3l60006.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/datatypes/v5l30058.cvc	[deleted file]	blob \| history
test/regress/regress0/datatypes/v5l30058.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/datatypes/wrong-sel-simp.cvc	[deleted file]	blob \| history
test/regress/regress0/datatypes/wrong-sel-simp.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/expect/scrub.06.cvc	[deleted file]	blob \| history
test/regress/regress0/expect/scrub.06.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/fmf/bug-041417-set-options.cvc	[deleted file]	blob \| history
test/regress/regress0/fmf/bug-041417-set-options.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/fmf/quant_real_univ.cvc	[deleted file]	blob \| history
test/regress/regress0/fmf/quant_real_univ.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/ite.cvc	[deleted file]	blob \| history
test/regress/regress0/ite.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/let.cvc	[deleted file]	blob \| history
test/regress/regress0/let.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/logops.01.cvc	[deleted file]	blob \| history
test/regress/regress0/logops.01.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/logops.02.cvc	[deleted file]	blob \| history
test/regress/regress0/logops.02.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/logops.03.cvc	[deleted file]	blob \| history
test/regress/regress0/logops.03.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/logops.04.cvc	[deleted file]	blob \| history
test/regress/regress0/logops.04.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/logops.05.cvc	[deleted file]	blob \| history
test/regress/regress0/logops.05.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/precedence/and-not.cvc	[deleted file]	blob \| history
test/regress/regress0/precedence/and-not.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/precedence/and-xor.cvc	[deleted file]	blob \| history
test/regress/regress0/precedence/and-xor.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/precedence/bool-cmp.cvc	[deleted file]	blob \| history
test/regress/regress0/precedence/bool-cmp.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/precedence/cmp-plus.cvc	[deleted file]	blob \| history
test/regress/regress0/precedence/cmp-plus.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/precedence/eq-fun.cvc	[deleted file]	blob \| history
test/regress/regress0/precedence/eq-fun.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/precedence/iff-assoc.cvc	[deleted file]	blob \| history
test/regress/regress0/precedence/iff-assoc.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/precedence/iff-implies.cvc	[deleted file]	blob \| history
test/regress/regress0/precedence/iff-implies.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/precedence/implies-assoc.cvc	[deleted file]	blob \| history
test/regress/regress0/precedence/implies-assoc.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/precedence/implies-iff.cvc	[deleted file]	blob \| history
test/regress/regress0/precedence/implies-iff.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/precedence/implies-or.cvc	[deleted file]	blob \| history
test/regress/regress0/precedence/implies-or.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/precedence/not-and.cvc	[deleted file]	blob \| history
test/regress/regress0/precedence/not-and.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/precedence/not-eq.cvc	[deleted file]	blob \| history
test/regress/regress0/precedence/not-eq.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/precedence/or-implies.cvc	[deleted file]	blob \| history
test/regress/regress0/precedence/or-implies.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/precedence/or-xor.cvc	[deleted file]	blob \| history
test/regress/regress0/precedence/or-xor.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/precedence/plus-mult.cvc	[deleted file]	blob \| history
test/regress/regress0/precedence/plus-mult.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/precedence/xor-and.cvc	[deleted file]	blob \| history
test/regress/regress0/precedence/xor-and.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/precedence/xor-assoc.cvc	[deleted file]	blob \| history
test/regress/regress0/precedence/xor-assoc.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/precedence/xor-or.cvc	[deleted file]	blob \| history
test/regress/regress0/precedence/xor-or.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/preprocess/preprocess_00.cvc	[deleted file]	blob \| history
test/regress/regress0/preprocess/preprocess_00.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/preprocess/preprocess_01.cvc	[deleted file]	blob \| history
test/regress/regress0/preprocess/preprocess_01.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/preprocess/preprocess_02.cvc	[deleted file]	blob \| history
test/regress/regress0/preprocess/preprocess_02.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/preprocess/preprocess_03.cvc	[deleted file]	blob \| history
test/regress/regress0/preprocess/preprocess_03.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/preprocess/preprocess_04.cvc	[deleted file]	blob \| history
test/regress/regress0/preprocess/preprocess_04.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/preprocess/preprocess_05.cvc	[deleted file]	blob \| history
test/regress/regress0/preprocess/preprocess_05.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/preprocess/preprocess_06.cvc	[deleted file]	blob \| history
test/regress/regress0/preprocess/preprocess_06.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/preprocess/preprocess_07.cvc	[deleted file]	blob \| history
test/regress/regress0/preprocess/preprocess_07.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/preprocess/preprocess_08.cvc	[deleted file]	blob \| history
test/regress/regress0/preprocess/preprocess_08.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/preprocess/preprocess_09.cvc	[deleted file]	blob \| history
test/regress/regress0/preprocess/preprocess_09.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/preprocess/preprocess_10.cvc	[deleted file]	blob \| history
test/regress/regress0/preprocess/preprocess_10.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/preprocess/preprocess_11.cvc	[deleted file]	blob \| history
test/regress/regress0/preprocess/preprocess_11.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/preprocess/preprocess_12.cvc	[deleted file]	blob \| history
test/regress/regress0/preprocess/preprocess_12.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/preprocess/preprocess_13.cvc	[deleted file]	blob \| history
test/regress/regress0/preprocess/preprocess_13.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/preprocess/preprocess_14.cvc	[deleted file]	blob \| history
test/regress/regress0/preprocess/preprocess_14.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/preprocess/preprocess_15.cvc	[deleted file]	blob \| history
test/regress/regress0/preprocess/preprocess_15.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/print_lambda.cvc	[deleted file]	blob \| history
test/regress/regress0/print_lambda.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/print_model.cvc	[deleted file]	blob \| history
test/regress/regress0/print_model.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/printer/tuples_and_records.cvc	[deleted file]	blob \| history
test/regress/regress0/printer/tuples_and_records.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/push-pop/bug233.cvc	[deleted file]	blob \| history
test/regress/regress0/push-pop/bug233.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/push-pop/incremental-subst-bug.cvc	[deleted file]	blob \| history
test/regress/regress0/push-pop/incremental-subst-bug.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/push-pop/test.00.cvc	[deleted file]	blob \| history
test/regress/regress0/push-pop/test.00.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/push-pop/test.01.cvc	[deleted file]	blob \| history
test/regress/regress0/push-pop/test.01.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/push-pop/units.cvc	[deleted file]	blob \| history
test/regress/regress0/push-pop/units.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/quantifiers/cegqi-nl-simp.cvc	[deleted file]	blob \| history
test/regress/regress0/quantifiers/cegqi-nl-simp.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/rels/addr_book_0.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/addr_book_0.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/rels/atom_univ2.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/atom_univ2.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/rels/card_transpose.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/card_transpose.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/rels/iden_0.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/iden_0.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/rels/iden_1.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/iden_1.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/rels/join-eq-u-sat.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/join-eq-u-sat.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/rels/join-eq-u.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/join-eq-u.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/rels/joinImg_0.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/joinImg_0.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/rels/oneLoc_no_quant-int_0_1.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/oneLoc_no_quant-int_0_1.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/rels/rel_1tup_0.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/rel_1tup_0.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/rels/rel_complex_0.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/rel_complex_0.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/rels/rel_complex_1.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/rel_complex_1.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/rels/rel_conflict_0.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/rel_conflict_0.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/rels/rel_join_0.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/rel_join_0.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/rels/rel_join_0_1.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/rel_join_0_1.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/rels/rel_join_1.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/rel_join_1.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/rels/rel_join_1_1.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/rel_join_1_1.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/rels/rel_join_2.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/rel_join_2.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/rels/rel_join_2_1.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/rel_join_2_1.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/rels/rel_join_3.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/rel_join_3.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/rels/rel_join_3_1.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/rel_join_3_1.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/rels/rel_join_4.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/rel_join_4.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/rels/rel_join_5.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/rel_join_5.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/rels/rel_join_6.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/rel_join_6.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/rels/rel_join_7.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/rel_join_7.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/rels/rel_product_0.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/rel_product_0.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/rels/rel_product_0_1.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/rel_product_0_1.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/rels/rel_product_1.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/rel_product_1.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/rels/rel_product_1_1.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/rel_product_1_1.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/rels/rel_symbolic_1.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/rel_symbolic_1.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/rels/rel_symbolic_1_1.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/rel_symbolic_1_1.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/rels/rel_symbolic_2_1.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/rel_symbolic_2_1.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/rels/rel_symbolic_3_1.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/rel_symbolic_3_1.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/rels/rel_tc_11.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/rel_tc_11.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/rels/rel_tc_2_1.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/rel_tc_2_1.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/rels/rel_tc_3.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/rel_tc_3.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/rels/rel_tc_3_1.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/rel_tc_3_1.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/rels/rel_tc_7.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/rel_tc_7.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/rels/rel_tc_8.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/rel_tc_8.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/rels/rel_tp_3_1.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/rel_tp_3_1.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/rels/rel_tp_join_0.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/rel_tp_join_0.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/rels/rel_tp_join_1.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/rel_tp_join_1.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/rels/rel_tp_join_2.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/rel_tp_join_2.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/rels/rel_tp_join_3.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/rel_tp_join_3.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/rels/rel_tp_join_eq_0.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/rel_tp_join_eq_0.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/rels/rel_tp_join_int_0.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/rel_tp_join_int_0.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/rels/rel_tp_join_pro_0.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/rel_tp_join_pro_0.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/rels/rel_tp_join_var_0.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/rel_tp_join_var_0.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/rels/rel_transpose_0.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/rel_transpose_0.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/rels/rel_transpose_1.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/rel_transpose_1.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/rels/rel_transpose_1_1.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/rel_transpose_1_1.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/rels/rel_transpose_3.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/rel_transpose_3.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/rels/rel_transpose_4.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/rel_transpose_4.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/rels/rel_transpose_5.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/rel_transpose_5.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/rels/rel_transpose_6.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/rel_transpose_6.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/rels/rel_transpose_7.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/rel_transpose_7.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/rels/rels-sharing-simp.cvc	[deleted file]	blob \| history
test/regress/regress0/rels/rels-sharing-simp.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/sets/card-3sets.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/card-3sets.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/sets/complement.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/complement.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/sets/complement2.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/complement2.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/sets/complement3.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/complement3.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/sets/cvc-sample.cvc	[deleted file]	blob \| history
test/regress/regress0/sets/cvc-sample.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/simple.cvc	[deleted file]	blob \| history
test/regress/regress0/simple.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/smallcnf.cvc	[deleted file]	blob \| history
test/regress/regress0/smallcnf.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/strings/parser-syms.cvc	[deleted file]	blob \| history
test/regress/regress0/strings/parser-syms.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/strings/regexp-native-simple.cvc	[deleted file]	blob \| history
test/regress/regress0/strings/regexp-native-simple.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/strings/strings-charat.cvc	[deleted file]	blob \| history
test/regress/regress0/strings/strings-charat.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/strings/strings-native-simple.cvc	[deleted file]	blob \| history
test/regress/regress0/strings/strings-native-simple.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/test11.cvc	[deleted file]	blob \| history
test/regress/regress0/test11.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/test9.cvc	[deleted file]	blob \| history
test/regress/regress0/test9.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/uf/simple.01.cvc	[deleted file]	blob \| history
test/regress/regress0/uf/simple.01.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/uf/simple.02.cvc	[deleted file]	blob \| history
test/regress/regress0/uf/simple.02.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/uf/simple.03.cvc	[deleted file]	blob \| history
test/regress/regress0/uf/simple.03.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/uf/simple.04.cvc	[deleted file]	blob \| history
test/regress/regress0/uf/simple.04.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/uf20-03.cvc	[deleted file]	blob \| history
test/regress/regress0/uf20-03.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/uflra/bug293.cvc	[deleted file]	blob \| history
test/regress/regress0/uflra/bug293.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/uflra/simple.01.cvc	[deleted file]	blob \| history
test/regress/regress0/uflra/simple.01.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/uflra/simple.02.cvc	[deleted file]	blob \| history
test/regress/regress0/uflra/simple.02.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/uflra/simple.03.cvc	[deleted file]	blob \| history
test/regress/regress0/uflra/simple.03.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/uflra/simple.04.cvc	[deleted file]	blob \| history
test/regress/regress0/uflra/simple.04.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/wiki.01.cvc	[deleted file]	blob \| history
test/regress/regress0/wiki.01.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/wiki.02.cvc	[deleted file]	blob \| history
test/regress/regress0/wiki.02.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/wiki.03.cvc	[deleted file]	blob \| history
test/regress/regress0/wiki.03.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/wiki.04.cvc	[deleted file]	blob \| history
test/regress/regress0/wiki.04.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/wiki.05.cvc	[deleted file]	blob \| history
test/regress/regress0/wiki.05.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/wiki.06.cvc	[deleted file]	blob \| history
test/regress/regress0/wiki.06.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/wiki.07.cvc	[deleted file]	blob \| history
test/regress/regress0/wiki.07.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/wiki.08.cvc	[deleted file]	blob \| history
test/regress/regress0/wiki.08.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/wiki.09.cvc	[deleted file]	blob \| history
test/regress/regress0/wiki.09.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/wiki.10.cvc	[deleted file]	blob \| history
test/regress/regress0/wiki.10.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/wiki.11.cvc	[deleted file]	blob \| history
test/regress/regress0/wiki.11.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/wiki.12.cvc	[deleted file]	blob \| history
test/regress/regress0/wiki.12.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/wiki.13.cvc	[deleted file]	blob \| history
test/regress/regress0/wiki.13.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/wiki.14.cvc	[deleted file]	blob \| history
test/regress/regress0/wiki.14.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/wiki.15.cvc	[deleted file]	blob \| history
test/regress/regress0/wiki.15.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/wiki.16.cvc	[deleted file]	blob \| history
test/regress/regress0/wiki.16.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/wiki.17.cvc	[deleted file]	blob \| history
test/regress/regress0/wiki.17.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/wiki.18.cvc	[deleted file]	blob \| history
test/regress/regress0/wiki.18.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/wiki.19.cvc	[deleted file]	blob \| history
test/regress/regress0/wiki.19.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/wiki.20.cvc	[deleted file]	blob \| history
test/regress/regress0/wiki.20.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress0/wiki.21.cvc	[deleted file]	blob \| history
test/regress/regress0/wiki.21.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-004.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-004.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-011.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-011.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-012.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-012.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-013.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-013.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-022.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-022.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-024.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-024.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-047.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-047.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-048.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-048.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-050.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-050.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-084.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-084.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-085.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-085.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/arith/arith-int-097.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/arith-int-097.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/arith/bug716.1.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/bug716.1.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/arith/bug716.2.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/bug716.2.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/arith/miplib3.cvc	[deleted file]	blob \| history
test/regress/regress1/arith/miplib3.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/boolean.cvc	[deleted file]	blob \| history
test/regress/regress1/boolean.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/bug425.cvc	[deleted file]	blob \| history
test/regress/regress1/bug425.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/constarr3.cvc	[deleted file]	blob \| history
test/regress/regress1/constarr3.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/datatypes/error.cvc	[deleted file]	blob \| history
test/regress/regress1/error.cvc	[deleted file]	blob \| history
test/regress/regress1/fmf/am-bad-model.cvc	[deleted file]	blob \| history
test/regress/regress1/fmf/am-bad-model.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/fmf/ko-bound-set.cvc	[deleted file]	blob \| history
test/regress/regress1/fmf/ko-bound-set.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/fmf/memory_model-R_cpp-dd.cvc	[deleted file]	blob \| history
test/regress/regress1/fmf/memory_model-R_cpp-dd.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/hole6.cvc	[deleted file]	blob \| history
test/regress/regress1/hole6.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/parsing_ringer.cvc	[deleted file]	blob \| history
test/regress/regress1/quantifiers/const.cvc	[deleted file]	blob \| history
test/regress/regress1/quantifiers/const.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/constfunc.cvc	[deleted file]	blob \| history
test/regress/regress1/quantifiers/constfunc.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/mutualrec2.cvc	[deleted file]	blob \| history
test/regress/regress1/quantifiers/mutualrec2.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/recfact.cvc	[deleted file]	blob \| history
test/regress/regress1/quantifiers/recfact.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/quantifiers/set-choice-koikonomou.cvc	[deleted file]	blob \| history
test/regress/regress1/quantifiers/set-choice-koikonomou.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/rels/addr_book_1.cvc	[deleted file]	blob \| history
test/regress/regress1/rels/addr_book_1.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/rels/addr_book_1_1.cvc	[deleted file]	blob \| history
test/regress/regress1/rels/addr_book_1_1.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/rels/bv1-unit.cvc	[deleted file]	blob \| history
test/regress/regress1/rels/bv1-unit.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/rels/bv1-unitb.cvc	[deleted file]	blob \| history
test/regress/regress1/rels/bv1-unitb.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/rels/bv1.cvc	[deleted file]	blob \| history
test/regress/regress1/rels/bv1.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/rels/bv1p-sat.cvc	[deleted file]	blob \| history
test/regress/regress1/rels/bv1p-sat.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/rels/bv1p.cvc	[deleted file]	blob \| history
test/regress/regress1/rels/bv1p.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/rels/bv2.cvc	[deleted file]	blob \| history
test/regress/regress1/rels/bv2.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/rels/garbage_collect.cvc	[deleted file]	blob \| history
test/regress/regress1/rels/garbage_collect.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/rels/iden_1_1.cvc	[deleted file]	blob \| history
test/regress/regress1/rels/iden_1_1.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/rels/join-eq-structure-and.cvc	[deleted file]	blob \| history
test/regress/regress1/rels/join-eq-structure-and.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/rels/join-eq-structure.cvc	[deleted file]	blob \| history
test/regress/regress1/rels/join-eq-structure.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/rels/joinImg_0_1.cvc	[deleted file]	blob \| history
test/regress/regress1/rels/joinImg_0_1.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/rels/joinImg_0_2.cvc	[deleted file]	blob \| history
test/regress/regress1/rels/joinImg_0_2.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/rels/joinImg_1.cvc	[deleted file]	blob \| history
test/regress/regress1/rels/joinImg_1.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/rels/joinImg_1_1.cvc	[deleted file]	blob \| history
test/regress/regress1/rels/joinImg_1_1.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/rels/joinImg_2.cvc	[deleted file]	blob \| history
test/regress/regress1/rels/joinImg_2.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/rels/joinImg_2_1.cvc	[deleted file]	blob \| history
test/regress/regress1/rels/joinImg_2_1.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/rels/prod-mod-eq.cvc	[deleted file]	blob \| history
test/regress/regress1/rels/prod-mod-eq.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/rels/prod-mod-eq2.cvc	[deleted file]	blob \| history
test/regress/regress1/rels/prod-mod-eq2.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/rels/rel_complex_3.cvc	[deleted file]	blob \| history
test/regress/regress1/rels/rel_complex_3.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/rels/rel_complex_4.cvc	[deleted file]	blob \| history
test/regress/regress1/rels/rel_complex_4.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/rels/rel_complex_5.cvc	[deleted file]	blob \| history
test/regress/regress1/rels/rel_complex_5.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/rels/rel_mix_0_1.cvc	[deleted file]	blob \| history
test/regress/regress1/rels/rel_mix_0_1.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/rels/rel_pressure_0.cvc	[deleted file]	blob \| history
test/regress/regress1/rels/rel_pressure_0.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/rels/rel_tc_10_1.cvc	[deleted file]	blob \| history
test/regress/regress1/rels/rel_tc_10_1.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/rels/rel_tc_4.cvc	[deleted file]	blob \| history
test/regress/regress1/rels/rel_tc_4.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/rels/rel_tc_4_1.cvc	[deleted file]	blob \| history
test/regress/regress1/rels/rel_tc_4_1.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/rels/rel_tc_5_1.cvc	[deleted file]	blob \| history
test/regress/regress1/rels/rel_tc_5_1.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/rels/rel_tc_6.cvc	[deleted file]	blob \| history
test/regress/regress1/rels/rel_tc_6.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/rels/rel_tc_9_1.cvc	[deleted file]	blob \| history
test/regress/regress1/rels/rel_tc_9_1.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/rels/rel_tp_2.cvc	[deleted file]	blob \| history
test/regress/regress1/rels/rel_tp_2.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/rels/rel_tp_join_2_1.cvc	[deleted file]	blob \| history
test/regress/regress1/rels/rel_tp_join_2_1.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/rels/set-strat.cvc	[deleted file]	blob \| history
test/regress/regress1/rels/set-strat.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/rels/strat.cvc	[deleted file]	blob \| history
test/regress/regress1/rels/strat.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sets/arjun-set-univ.cvc	[deleted file]	blob \| history
test/regress/regress1/sets/arjun-set-univ.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sets/choose.cvc	[deleted file]	blob \| history
test/regress/regress1/sets/choose.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/sets/sets-tuple-poly.cvc	[deleted file]	blob \| history
test/regress/regress1/sets/sets-tuple-poly.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/test12.cvc	[deleted file]	blob \| history
test/regress/regress1/test12.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress1/trim.cvc	[deleted file]	blob \| history
test/regress/regress1/trim.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress2/arith/arith-int-098.cvc	[deleted file]	blob \| history
test/regress/regress2/arith/arith-int-098.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress2/hole7.cvc	[deleted file]	blob \| history
test/regress/regress2/hole7.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress2/hole8.cvc	[deleted file]	blob \| history
test/regress/regress2/hole8.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress2/typed_v1l50016-simp.cvc	[deleted file]	blob \| history
test/regress/regress2/typed_v1l50016-simp.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress3/hole10.cvc	[deleted file]	blob \| history
test/regress/regress3/hole10.cvc.smt2	[new file with mode: 0644]	blob
test/regress/regress3/hole9.cvc	[deleted file]	blob \| history
test/regress/regress3/hole9.cvc.smt2	[new file with mode: 0644]	blob
test/regress/run_regression.py		diff \| blob \| history
test/unit/node/node_black.cpp		diff \| blob \| history
test/unit/parser/parser_black.cpp		diff \| blob \| history
test/unit/parser/parser_builder_black.cpp		diff \| blob \| history
test/unit/util/boolean_simplification_black.cpp		diff \| blob \| history

RSS Atom