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

author	Aina Niemetz <aina.niemetz@gmail.com>
	Mon, 8 Nov 2021 20:49:14 +0000 (12:49 -0800)
committer	GitHub <noreply@github.com>
	Mon, 8 Nov 2021 20:49:14 +0000 (12:49 -0800)
commit	f2fb0be98861642e0e33ff3c5dc763e8aa5fe769
tree	afcb1c6dd0f9395b6714ebff47bf52c855b4ed2e	tree
parent	20d8fe633c1f113dceade2df232a35db03e6288c	commit \| diff

sets: Rename kinds with a more consistent naming scheme. (#7595)

This prefixes sets kinds with SET_ and relation kinds with
RELATION_. It also prefixes the corresponding SMT-LIB operators with
'set.' and relation operators with 'rel.'.

329 files changed:

examples/api/cpp/sets.cpp		diff \| blob \| history
examples/api/python/sets.py		diff \| blob \| history
examples/sets-translate/sets-translate-example-input.smt2		diff \| blob \| history
examples/sets-translate/sets_translate.cpp		diff \| blob \| history
src/api/cpp/cvc5.cpp		diff \| blob \| history
src/api/cpp/cvc5.h		diff \| blob \| history
src/api/cpp/cvc5_kind.h		diff \| blob \| history
src/api/parsekinds.py		diff \| blob \| history
src/expr/node.h		diff \| blob \| history
src/expr/node_manager.cpp		diff \| blob \| history
src/parser/parser.cpp		diff \| blob \| history
src/parser/parser.h		diff \| blob \| history
src/parser/smt2/Smt2.g		diff \| blob \| history
src/parser/smt2/smt2.cpp		diff \| blob \| history
src/printer/smt2/smt2_printer.cpp		diff \| blob \| history
src/proof/alethe/alethe_post_processor.cpp		diff \| blob \| history
src/proof/lfsc/lfsc_node_converter.cpp		diff \| blob \| history
src/theory/bags/bags_rewriter.cpp		diff \| blob \| history
src/theory/bags/normal_form.cpp		diff \| blob \| history
src/theory/bags/theory_bags_type_rules.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/trigger_term_info.cpp		diff \| blob \| history
src/theory/quantifiers/fmf/bounded_integers.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_grammar_cons.cpp		diff \| blob \| history
src/theory/quantifiers/term_database.cpp		diff \| blob \| history
src/theory/quantifiers/term_util.cpp		diff \| blob \| history
src/theory/sep/theory_sep.cpp		diff \| blob \| history
src/theory/sets/cardinality_extension.cpp		diff \| blob \| history
src/theory/sets/cardinality_extension.h		diff \| blob \| history
src/theory/sets/inference_manager.cpp		diff \| blob \| history
src/theory/sets/kinds		diff \| blob \| history
src/theory/sets/normal_form.h		diff \| blob \| history
src/theory/sets/singleton_op.cpp		diff \| blob \| history
src/theory/sets/singleton_op.h		diff \| blob \| history
src/theory/sets/solver_state.cpp		diff \| blob \| history
src/theory/sets/solver_state.h		diff \| blob \| history
src/theory/sets/term_registry.cpp		diff \| blob \| history
src/theory/sets/theory_sets.cpp		diff \| blob \| history
src/theory/sets/theory_sets_private.cpp		diff \| blob \| history
src/theory/sets/theory_sets_private.h		diff \| blob \| history
src/theory/sets/theory_sets_rels.cpp		diff \| blob \| history
src/theory/sets/theory_sets_rels.h		diff \| blob \| history
src/theory/sets/theory_sets_rewriter.cpp		diff \| blob \| history
src/theory/sets/theory_sets_type_rules.cpp		diff \| blob \| history
src/theory/theory_model.h		diff \| blob \| history
test/python/unit/api/test_term.py		diff \| blob \| history
test/regress/regress0/bug586.cvc.smt2		diff \| blob \| history
test/regress/regress0/bug605.cvc.smt2		diff \| blob \| history
test/regress/regress0/cores/issue4971-1.smt2		diff \| blob \| history
test/regress/regress0/datatypes/conqueue-dt-enum-iloop.smt2		diff \| blob \| history
test/regress/regress0/datatypes/dt-2.6.smt2		diff \| blob \| history
test/regress/regress0/datatypes/dt-match-pat-param-2.6.smt2		diff \| blob \| history
test/regress/regress0/datatypes/dt-param-2.6.smt2		diff \| blob \| history
test/regress/regress0/datatypes/dt-sel-2.6.smt2		diff \| blob \| history
test/regress/regress0/datatypes/issue5280-no-nrec.smt2		diff \| blob \| history
test/regress/regress0/fmf/bounded_sets.smt2		diff \| blob \| history
test/regress/regress0/fmf/fmf-strange-bounds-2.smt2		diff \| blob \| history
test/regress/regress0/fmf/quant_real_univ.cvc.smt2		diff \| blob \| history
test/regress/regress0/ho/fta0144-alpha-eq.smt2		diff \| blob \| history
test/regress/regress0/parser/declarefun-emptyset-uf.smt2		diff \| blob \| history
test/regress/regress0/rels/addr_book_0.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/atom_univ2.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/card_transpose.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/iden_0.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/iden_1.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/join-eq-u-sat.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/join-eq-u.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/joinImg_0.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/oneLoc_no_quant-int_0_1.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/qgu-fuzz-relations-1-dd.smt2		diff \| blob \| history
test/regress/regress0/rels/qgu-fuzz-relations-1.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_1tup_0.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_complex_0.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_complex_1.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_conflict_0.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_join_0.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_join_0_1.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_join_1.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_join_1_1.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_join_2.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_join_2_1.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_join_3.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_join_3_1.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_join_4.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_join_5.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_join_6.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_join_7.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_product_0.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_product_0_1.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_product_1.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_product_1_1.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_symbolic_1.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_symbolic_1_1.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_symbolic_2_1.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_symbolic_3_1.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_tc_11.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_tc_2_1.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_tc_3.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_tc_3_1.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_tc_7.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_tc_8.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_tp_3_1.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_tp_join_0.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_tp_join_1.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_tp_join_2.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_tp_join_3.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_tp_join_eq_0.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_tp_join_int_0.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_tp_join_pro_0.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_tp_join_var_0.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_transpose_0.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_transpose_1.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_transpose_1_1.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_transpose_3.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_transpose_4.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_transpose_5.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_transpose_6.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/rel_transpose_7.cvc.smt2		diff \| blob \| history
test/regress/regress0/rels/relations-ops.smt2		diff \| blob \| history
test/regress/regress0/rels/rels-sharing-simp.cvc.smt2		diff \| blob \| history
test/regress/regress0/sets/abt-min.smt2		diff \| blob \| history
test/regress/regress0/sets/abt-te-exh.smt2		diff \| blob \| history
test/regress/regress0/sets/abt-te-exh2.smt2		diff \| blob \| history
test/regress/regress0/sets/card-2.smt2		diff \| blob \| history
test/regress/regress0/sets/card-3sets.cvc.smt2		diff \| blob \| history
test/regress/regress0/sets/card.smt2		diff \| blob \| history
test/regress/regress0/sets/card3-ground.smt2		diff \| blob \| history
test/regress/regress0/sets/comp-qf-error.smt2		diff \| blob \| history
test/regress/regress0/sets/complement.cvc.smt2		diff \| blob \| history
test/regress/regress0/sets/complement2.cvc.smt2		diff \| blob \| history
test/regress/regress0/sets/complement3.cvc.smt2		diff \| blob \| history
test/regress/regress0/sets/cvc-sample.cvc.smt2		diff \| blob \| history
test/regress/regress0/sets/dt-simp-mem.smt2		diff \| blob \| history
test/regress/regress0/sets/emptyset.smt2		diff \| blob \| history
test/regress/regress0/sets/eqtest.smt2		diff \| blob \| history
test/regress/regress0/sets/error1.smt2		diff \| blob \| history
test/regress/regress0/sets/error2.smt2		diff \| blob \| history
test/regress/regress0/sets/insert.smt2		diff \| blob \| history
test/regress/regress0/sets/int-real-univ-unsat.smt2		diff \| blob \| history
test/regress/regress0/sets/int-real-univ.smt2		diff \| blob \| history
test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.cvc4.47.smt2		diff \| blob \| history
test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.small.smt2		diff \| blob \| history
test/regress/regress0/sets/jan27/ListConcat.hs.fqout.177minimized.smt2		diff \| blob \| history
test/regress/regress0/sets/jan27/ListConcat.hs.fqout.cvc4.177.smt2		diff \| blob \| history
test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.3577minimized.smt2		diff \| blob \| history
test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized10.smt2		diff \| blob \| history
test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized1832.smt2		diff \| blob \| history
test/regress/regress0/sets/mar2014/sharing-preregister.smt2		diff \| blob \| history
test/regress/regress0/sets/mar2014/small.smt2		diff \| blob \| history
test/regress/regress0/sets/mar2014/smaller.smt2		diff \| blob \| history
test/regress/regress0/sets/nonvar-univ.smt2		diff \| blob \| history
test/regress/regress0/sets/pre-proc-univ.smt2		diff \| blob \| history
test/regress/regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2		diff \| blob \| history
test/regress/regress0/sets/setel-eq.smt2		diff \| blob \| history
test/regress/regress0/sets/sets-deq-dd.smt2		diff \| blob \| history
test/regress/regress0/sets/sets-equal.smt2		diff \| blob \| history
test/regress/regress0/sets/sets-extr.smt2		diff \| blob \| history
test/regress/regress0/sets/sets-inter.smt2		diff \| blob \| history
test/regress/regress0/sets/sets-new.smt2		diff \| blob \| history
test/regress/regress0/sets/sets-of-sets-subtypes.smt2		diff \| blob \| history
test/regress/regress0/sets/sets-poly-int-real.smt2		diff \| blob \| history
test/regress/regress0/sets/sets-poly-nonint.smt2		diff \| blob \| history
test/regress/regress0/sets/sets-sample.smt2		diff \| blob \| history
test/regress/regress0/sets/sets-sharing.smt2		diff \| blob \| history
test/regress/regress0/sets/sets-union.smt2		diff \| blob \| history
test/regress/regress0/sets/sharing-simp.smt2		diff \| blob \| history
test/regress/regress0/sets/union-1a-flip.smt2		diff \| blob \| history
test/regress/regress0/sets/union-1a.smt2		diff \| blob \| history
test/regress/regress0/sets/union-1b-flip.smt2		diff \| blob \| history
test/regress/regress0/sets/union-1b.smt2		diff \| blob \| history
test/regress/regress0/sets/union-2.smt2		diff \| blob \| history
test/regress/regress0/sets/univset-simp.smt2		diff \| blob \| history
test/regress/regress0/tptp/Axioms/BOO004-0.ax		diff \| blob \| history
test/regress/regress0/tptp/Axioms/SYN000+0.ax		diff \| blob \| history
test/regress/regress0/tptp/Axioms/SYN000-0.ax		diff \| blob \| history
test/regress/regress0/tptp/BOO003-4.p		diff \| blob \| history
test/regress/regress0/tptp/BOO027-1.p		diff \| blob \| history
test/regress/regress0/tptp/KRS018+1.p		diff \| blob \| history
test/regress/regress0/tptp/KRS063+1.p		diff \| blob \| history
test/regress/regress0/tptp/MGT019+2.p		diff \| blob \| history
test/regress/regress0/tptp/MGT031-1.p		diff \| blob \| history
test/regress/regress0/tptp/MGT041-2.p		diff \| blob \| history
test/regress/regress0/tptp/NLP114-1.p		diff \| blob \| history
test/regress/regress0/tptp/SYN000-1.p		diff \| blob \| history
test/regress/regress0/tptp/SYN075+1.p		diff \| blob \| history
test/regress/regress0/tptp/SYN075-1.p		diff \| blob \| history
test/regress/regress1/bug567.smt2		diff \| blob \| history
test/regress/regress1/datatypes/non-simple-rec-set.smt2		diff \| blob \| history
test/regress/regress1/fmf/agree467.smt2		diff \| blob \| history
test/regress/regress1/fmf/cons-sets-bounds.smt2		diff \| blob \| history
test/regress/regress1/fmf/fmf-strange-bounds.smt2		diff \| blob \| history
test/regress/regress1/fmf/ko-bound-set.cvc.smt2		diff \| blob \| history
test/regress/regress1/fmf/memory_model-R_cpp-dd.cvc.smt2		diff \| blob \| history
test/regress/regress1/fmf/radu-quant-set.smt2		diff \| blob \| history
test/regress/regress1/ho/hoa0102.smt2		diff \| blob \| history
test/regress/regress1/quantifiers/bug822.smt2		diff \| blob \| history
test/regress/regress1/quantifiers/bug_743.smt2		diff \| blob \| history
test/regress/regress1/quantifiers/cdt-0208-to.smt2		diff \| blob \| history
test/regress/regress1/quantifiers/inst-max-level-segf.smt2		diff \| blob \| history
test/regress/regress1/quantifiers/set-choice-koikonomou.cvc.smt2		diff \| blob \| history
test/regress/regress1/quantifiers/set3.smt2		diff \| blob \| history
test/regress/regress1/quantifiers/set8.smt2		diff \| blob \| history
test/regress/regress1/quantifiers/seu169+1.smt2		diff \| blob \| history
test/regress/regress1/quantifiers/stream-x2014-09-18-unsat.smt2		diff \| blob \| history
test/regress/regress1/rels/addr_book_1.cvc.smt2		diff \| blob \| history
test/regress/regress1/rels/addr_book_1_1.cvc.smt2		diff \| blob \| history
test/regress/regress1/rels/bv1-unit.cvc.smt2		diff \| blob \| history
test/regress/regress1/rels/bv1-unitb.cvc.smt2		diff \| blob \| history
test/regress/regress1/rels/bv1.cvc.smt2		diff \| blob \| history
test/regress/regress1/rels/bv1p-sat.cvc.smt2		diff \| blob \| history
test/regress/regress1/rels/bv1p.cvc.smt2		diff \| blob \| history
test/regress/regress1/rels/bv2.cvc.smt2		diff \| blob \| history
test/regress/regress1/rels/garbage_collect.cvc.smt2		diff \| blob \| history
test/regress/regress1/rels/iden_1_1.cvc.smt2		diff \| blob \| history
test/regress/regress1/rels/join-eq-structure-and.cvc.smt2		diff \| blob \| history
test/regress/regress1/rels/join-eq-structure.cvc.smt2		diff \| blob \| history
test/regress/regress1/rels/joinImg_0_1.cvc.smt2		diff \| blob \| history
test/regress/regress1/rels/joinImg_0_2.cvc.smt2		diff \| blob \| history
test/regress/regress1/rels/joinImg_1.cvc.smt2		diff \| blob \| history
test/regress/regress1/rels/joinImg_1_1.cvc.smt2		diff \| blob \| history
test/regress/regress1/rels/joinImg_2.cvc.smt2		diff \| blob \| history
test/regress/regress1/rels/joinImg_2_1.cvc.smt2		diff \| blob \| history
test/regress/regress1/rels/prod-mod-eq.cvc.smt2		diff \| blob \| history
test/regress/regress1/rels/prod-mod-eq2.cvc.smt2		diff \| blob \| history
test/regress/regress1/rels/qgu-fuzz-relations-2.smt2		diff \| blob \| history
test/regress/regress1/rels/qgu-fuzz-relations-3-upwards.smt2		diff \| blob \| history
test/regress/regress1/rels/rel_complex_3.cvc.smt2		diff \| blob \| history
test/regress/regress1/rels/rel_complex_4.cvc.smt2		diff \| blob \| history
test/regress/regress1/rels/rel_complex_5.cvc.smt2		diff \| blob \| history
test/regress/regress1/rels/rel_mix_0_1.cvc.smt2		diff \| blob \| history
test/regress/regress1/rels/rel_pressure_0.cvc.smt2		diff \| blob \| history
test/regress/regress1/rels/rel_tc_10_1.cvc.smt2		diff \| blob \| history
test/regress/regress1/rels/rel_tc_4.cvc.smt2		diff \| blob \| history
test/regress/regress1/rels/rel_tc_4_1.cvc.smt2		diff \| blob \| history
test/regress/regress1/rels/rel_tc_5_1.cvc.smt2		diff \| blob \| history
test/regress/regress1/rels/rel_tc_6.cvc.smt2		diff \| blob \| history
test/regress/regress1/rels/rel_tc_9_1.cvc.smt2		diff \| blob \| history
test/regress/regress1/rels/rel_tp_2.cvc.smt2		diff \| blob \| history
test/regress/regress1/rels/rel_tp_join_2_1.cvc.smt2		diff \| blob \| history
test/regress/regress1/rels/set-strat.cvc.smt2		diff \| blob \| history
test/regress/regress1/rels/strat.cvc.smt2		diff \| blob \| history
test/regress/regress1/sets/ListElem.hs.fqout.cvc4.38.smt2		diff \| blob \| history
test/regress/regress1/sets/ListElts.hs.fqout.cvc4.317.smt2		diff \| blob \| history
test/regress/regress1/sets/TalkingAboutSets.hs.fqout.cvc4.3577.smt2		diff \| blob \| history
test/regress/regress1/sets/UniqueZipper.hs.1030minimized.cvc4.smt2		diff \| blob \| history
test/regress/regress1/sets/UniqueZipper.hs.1030minimized2.cvc4.smt2		diff \| blob \| history
test/regress/regress1/sets/UniqueZipper.hs.fqout.cvc4.10.smt2		diff \| blob \| history
test/regress/regress1/sets/UniqueZipper.hs.fqout.cvc4.1832.smt2		diff \| blob \| history
test/regress/regress1/sets/arjun-set-univ.cvc.smt2		diff \| blob \| history
test/regress/regress1/sets/card-3.smt2		diff \| blob \| history
test/regress/regress1/sets/card-4.smt2		diff \| blob \| history
test/regress/regress1/sets/card-5.smt2		diff \| blob \| history
test/regress/regress1/sets/card-6.smt2		diff \| blob \| history
test/regress/regress1/sets/card-7.smt2		diff \| blob \| history
test/regress/regress1/sets/card-vc6-minimized.smt2		diff \| blob \| history
test/regress/regress1/sets/choose.cvc.smt2		diff \| blob \| history
test/regress/regress1/sets/choose1.smt2		diff \| blob \| history
test/regress/regress1/sets/choose2.smt2		diff \| blob \| history
test/regress/regress1/sets/choose3.smt2		diff \| blob \| history
test/regress/regress1/sets/choose4.smt2		diff \| blob \| history
test/regress/regress1/sets/comp-intersect.smt2		diff \| blob \| history
test/regress/regress1/sets/comp-odd.smt2		diff \| blob \| history
test/regress/regress1/sets/comp-pos-member.smt2		diff \| blob \| history
test/regress/regress1/sets/comp-positive.smt2		diff \| blob \| history
test/regress/regress1/sets/copy_check_heap_access_33_4.smt2		diff \| blob \| history
test/regress/regress1/sets/deepmeas0.hs.fqout.cvc4.41.smt2		diff \| blob \| history
test/regress/regress1/sets/finite-type/bug3663.smt2		diff \| blob \| history
test/regress/regress1/sets/finite-type/sets-card-arrcolor.smt2		diff \| blob \| history
test/regress/regress1/sets/finite-type/sets-card-arrunit.smt2		diff \| blob \| history
test/regress/regress1/sets/finite-type/sets-card-bool-1.smt2		diff \| blob \| history
test/regress/regress1/sets/finite-type/sets-card-bool-2.smt2		diff \| blob \| history
test/regress/regress1/sets/finite-type/sets-card-bool-3.smt2		diff \| blob \| history
test/regress/regress1/sets/finite-type/sets-card-bool-4.smt2		diff \| blob \| history
test/regress/regress1/sets/finite-type/sets-card-bool-rec.smt2		diff \| blob \| history
test/regress/regress1/sets/finite-type/sets-card-bv-1.smt2		diff \| blob \| history
test/regress/regress1/sets/finite-type/sets-card-bv-2.smt2		diff \| blob \| history
test/regress/regress1/sets/finite-type/sets-card-bv-3.smt2		diff \| blob \| history
test/regress/regress1/sets/finite-type/sets-card-bv-4.smt2		diff \| blob \| history
test/regress/regress1/sets/finite-type/sets-card-color-sat.smt2		diff \| blob \| history
test/regress/regress1/sets/finite-type/sets-card-color.smt2		diff \| blob \| history
test/regress/regress1/sets/finite-type/sets-card-datatype-1.smt2		diff \| blob \| history
test/regress/regress1/sets/finite-type/sets-card-datatype-2.smt2		diff \| blob \| history
test/regress/regress1/sets/finite-type/sets-card-neg-mem-union-1.smt2		diff \| blob \| history
test/regress/regress1/sets/finite-type/sets-card-neg-mem-union-2.smt2		diff \| blob \| history
test/regress/regress1/sets/fuzz14418.smt2		diff \| blob \| history
test/regress/regress1/sets/fuzz15201.smt2		diff \| blob \| history
test/regress/regress1/sets/fuzz31811.smt2		diff \| blob \| history
test/regress/regress1/sets/infinite-type/sets-card-array-int-1.smt2		diff \| blob \| history
test/regress/regress1/sets/infinite-type/sets-card-array-int-2.smt2		diff \| blob \| history
test/regress/regress1/sets/infinite-type/sets-card-int-1.smt2		diff \| blob \| history
test/regress/regress1/sets/infinite-type/sets-card-int-2.smt2		diff \| blob \| history
test/regress/regress1/sets/insert_invariant_37_2.smt2		diff \| blob \| history
test/regress/regress1/sets/is_singleton1.smt2		diff \| blob \| history
test/regress/regress1/sets/issue2568.smt2		diff \| blob \| history
test/regress/regress1/sets/issue2904.smt2		diff \| blob \| history
test/regress/regress1/sets/issue4124-need-check.smt2		diff \| blob \| history
test/regress/regress1/sets/issue4370-2-lemma-ee-iter.smt2		diff \| blob \| history
test/regress/regress1/sets/issue4370-4-lemma-ee-iter.smt2		diff \| blob \| history
test/regress/regress1/sets/issue4391-card-lasso.smt2		diff \| blob \| history
test/regress/regress1/sets/issue5271.smt2		diff \| blob \| history
test/regress/regress1/sets/issue5309.smt2		diff \| blob \| history
test/regress/regress1/sets/issue5342.smt2		diff \| blob \| history
test/regress/regress1/sets/issue5342_difference_version.smt2		diff \| blob \| history
test/regress/regress1/sets/issue5705-cg-subtyping.smt2		diff \| blob \| history
test/regress/regress1/sets/issue5942-witness.smt2		diff \| blob \| history
test/regress/regress1/sets/lemmabug-ListElts317minimized.smt2		diff \| blob \| history
test/regress/regress1/sets/remove_check_free_31_6.smt2		diff \| blob \| history
test/regress/regress1/sets/set-comp-sat.smt2		diff \| blob \| history
test/regress/regress1/sets/setofsets-disequal.smt2		diff \| blob \| history
test/regress/regress1/sets/sets-tuple-poly.cvc.smt2		diff \| blob \| history
test/regress/regress1/sets/sets-uc-wrong.smt2		diff \| blob \| history
test/regress/regress1/sets/sharingbug.smt2		diff \| blob \| history
test/regress/regress1/sets/univ-set-uf-elim.smt2		diff \| blob \| history
test/regress/regress1/strings/issue6184-unsat-core.smt2		diff \| blob \| history
test/regress/regress1/sygus/sets-pred-test.sy		diff \| blob \| history
test/regress/regress1/sym/sym-setAB.smt2		diff \| blob \| history
test/regress/regress1/sym/sym1.smt2		diff \| blob \| history
test/regress/regress1/sym/sym3.smt2		diff \| blob \| history
test/regress/regress1/sym/sym5.smt2		diff \| blob \| history
test/regress/regress1/trim.cvc.smt2		diff \| blob \| history
test/regress/regress2/bug812.smt2		diff \| blob \| history
test/regress/regress2/ho/auth0068.smt2		diff \| blob \| history
test/regress/regress2/sygus/sets-fun-test.sy		diff \| blob \| history
test/regress/regress4/sets-card-neg-mem-union-2.smt2		diff \| blob \| history
test/unit/api/java/SolverTest.java		diff \| blob \| history
test/unit/api/java/TermTest.java		diff \| blob \| history
test/unit/api/solver_black.cpp		diff \| blob \| history
test/unit/api/term_black.cpp		diff \| blob \| history
test/unit/theory/theory_bags_normal_form_white.cpp		diff \| blob \| history
test/unit/theory/theory_sets_type_rules_white.cpp		diff \| blob \| history

RSS Atom