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

author	Aina Niemetz <aina.niemetz@gmail.com>
	Wed, 2 Jun 2021 17:16:26 +0000 (10:16 -0700)
committer	GitHub <noreply@github.com>
	Wed, 2 Jun 2021 17:16:26 +0000 (17:16 +0000)
commit	dde15bdbf752246fe7cb504df22261e0ad3835db
tree	ff0b646059dc67c68e24abcc3af5fb3ceeabdc41	tree
parent	338982182dbdabecf6f3b06e659621cf43bed916	commit \| diff

Remove redundant logic ALL_SUPPORTED. (#6664)

310 files changed:

NEWS		diff \| blob \| history
src/theory/logic_info.cpp		diff \| blob \| history
test/api/sep_log_api.cpp		diff \| blob \| history
test/python/unit/api/test_solver.py		diff \| blob \| history
test/regress/regress0/bug521.minimized.smt2		diff \| blob \| history
test/regress/regress0/bug541.smt2		diff \| blob \| history
test/regress/regress0/bv/bv-int-collapse1.smt2		diff \| blob \| history
test/regress/regress0/bv/bv-int-collapse2.smt2		diff \| blob \| history
test/regress/regress0/bv/bv2nat-simp-range.smt2		diff \| blob \| history
test/regress/regress0/datatypes/bug597-rbt.smt2		diff \| blob \| history
test/regress/regress0/datatypes/bug604.smt2		diff \| blob \| history
test/regress/regress0/datatypes/bug625.smt2		diff \| blob \| history
test/regress/regress0/datatypes/cdt-model-cade15.smt2		diff \| blob \| history
test/regress/regress0/datatypes/cdt-non-canon-stream.smt2		diff \| blob \| history
test/regress/regress0/datatypes/coda_simp_model.smt2		diff \| blob \| history
test/regress/regress0/datatypes/conqueue-dt-enum-iloop.smt2		diff \| blob \| history
test/regress/regress0/datatypes/dt-different-params.smt2		diff \| blob \| history
test/regress/regress0/datatypes/dt-param-card4-bool-sat.smt2		diff \| blob \| history
test/regress/regress0/datatypes/is_test.smt2		diff \| blob \| history
test/regress/regress0/datatypes/pair-real-bool.smt2		diff \| blob \| history
test/regress/regress0/datatypes/sc-cdt1.smt2		diff \| blob \| history
test/regress/regress0/datatypes/stream-singleton.smt2		diff \| blob \| history
test/regress/regress0/datatypes/tenum-bug.smt2		diff \| blob \| history
test/regress/regress0/datatypes/tuple-no-clash.cvc		diff \| blob \| history
test/regress/regress0/decision/bug374b.smt2		diff \| blob \| history
test/regress/regress0/fmf/fd-false.smt2		diff \| blob \| history
test/regress/regress0/fmf/fmc_unsound_model.smt2		diff \| blob \| history
test/regress/regress0/fmf/forall_unit_data2.smt2		diff \| blob \| history
test/regress/regress0/fmf/krs-sat.smt2		diff \| blob \| history
test/regress/regress0/fmf/sc_bad_model_1221.smt2		diff \| blob \| history
test/regress/regress0/fmf/syn002-si-real-int.smt2		diff \| blob \| history
test/regress/regress0/fmf/tail_rec.smt2		diff \| blob \| history
test/regress/regress0/hung10_itesdk_output1.smt2		diff \| blob \| history
test/regress/regress0/hung13sdk_output1.smt2		diff \| blob \| history
test/regress/regress0/push-pop/bug654-dd.smt2		diff \| blob \| history
test/regress/regress0/quantifiers/cbqi-lia-dt-simp.smt2		diff \| blob \| history
test/regress/regress0/quantifiers/is-even-pred.smt2		diff \| blob \| history
test/regress/regress0/quantifiers/matching-lia-1arg.smt2		diff \| blob \| history
test/regress/regress0/quantifiers/mix-match.smt2		diff \| blob \| history
test/regress/regress0/quantifiers/partial-trigger.smt2		diff \| blob \| history
test/regress/regress0/quantifiers/pure_dt_cbqi.smt2		diff \| blob \| history
test/regress/regress0/quantifiers/rew-to-scala.smt2		diff \| blob \| history
test/regress/regress0/quantifiers/simp-len.smt2		diff \| blob \| history
test/regress/regress0/rec-fun-const-parse-bug.smt2		diff \| blob \| history
test/regress/regress0/rels/addr_book_0.cvc		diff \| blob \| history
test/regress/regress0/rels/atom_univ2.cvc		diff \| blob \| history
test/regress/regress0/rels/card_transpose.cvc		diff \| blob \| history
test/regress/regress0/rels/iden_0.cvc		diff \| blob \| history
test/regress/regress0/rels/iden_1.cvc		diff \| blob \| history
test/regress/regress0/rels/join-eq-u-sat.cvc		diff \| blob \| history
test/regress/regress0/rels/join-eq-u.cvc		diff \| blob \| history
test/regress/regress0/rels/joinImg_0.cvc		diff \| blob \| history
test/regress/regress0/rels/rel_1tup_0.cvc		diff \| blob \| history
test/regress/regress0/rels/rel_complex_0.cvc		diff \| blob \| history
test/regress/regress0/rels/rel_complex_1.cvc		diff \| blob \| history
test/regress/regress0/rels/rel_conflict_0.cvc		diff \| blob \| history
test/regress/regress0/rels/rel_join_0.cvc		diff \| blob \| history
test/regress/regress0/rels/rel_join_0_1.cvc		diff \| blob \| history
test/regress/regress0/rels/rel_join_1.cvc		diff \| blob \| history
test/regress/regress0/rels/rel_join_1_1.cvc		diff \| blob \| history
test/regress/regress0/rels/rel_join_2.cvc		diff \| blob \| history
test/regress/regress0/rels/rel_join_2_1.cvc		diff \| blob \| history
test/regress/regress0/rels/rel_join_3.cvc		diff \| blob \| history
test/regress/regress0/rels/rel_join_3_1.cvc		diff \| blob \| history
test/regress/regress0/rels/rel_join_4.cvc		diff \| blob \| history
test/regress/regress0/rels/rel_join_5.cvc		diff \| blob \| history
test/regress/regress0/rels/rel_join_6.cvc		diff \| blob \| history
test/regress/regress0/rels/rel_join_7.cvc		diff \| blob \| history
test/regress/regress0/rels/rel_product_0.cvc		diff \| blob \| history
test/regress/regress0/rels/rel_product_0_1.cvc		diff \| blob \| history
test/regress/regress0/rels/rel_product_1.cvc		diff \| blob \| history
test/regress/regress0/rels/rel_product_1_1.cvc		diff \| blob \| history
test/regress/regress0/rels/rel_symbolic_1.cvc		diff \| blob \| history
test/regress/regress0/rels/rel_symbolic_1_1.cvc		diff \| blob \| history
test/regress/regress0/rels/rel_symbolic_2_1.cvc		diff \| blob \| history
test/regress/regress0/rels/rel_symbolic_3_1.cvc		diff \| blob \| history
test/regress/regress0/rels/rel_tc_11.cvc		diff \| blob \| history
test/regress/regress0/rels/rel_tc_2_1.cvc		diff \| blob \| history
test/regress/regress0/rels/rel_tc_3.cvc		diff \| blob \| history
test/regress/regress0/rels/rel_tc_3_1.cvc		diff \| blob \| history
test/regress/regress0/rels/rel_tc_7.cvc		diff \| blob \| history
test/regress/regress0/rels/rel_tc_8.cvc		diff \| blob \| history
test/regress/regress0/rels/rel_tp_3_1.cvc		diff \| blob \| history
test/regress/regress0/rels/rel_tp_join_0.cvc		diff \| blob \| history
test/regress/regress0/rels/rel_tp_join_1.cvc		diff \| blob \| history
test/regress/regress0/rels/rel_tp_join_2.cvc		diff \| blob \| history
test/regress/regress0/rels/rel_tp_join_3.cvc		diff \| blob \| history
test/regress/regress0/rels/rel_tp_join_eq_0.cvc		diff \| blob \| history
test/regress/regress0/rels/rel_tp_join_int_0.cvc		diff \| blob \| history
test/regress/regress0/rels/rel_tp_join_pro_0.cvc		diff \| blob \| history
test/regress/regress0/rels/rel_tp_join_var_0.cvc		diff \| blob \| history
test/regress/regress0/rels/rel_transpose_0.cvc		diff \| blob \| history
test/regress/regress0/rels/rel_transpose_1.cvc		diff \| blob \| history
test/regress/regress0/rels/rel_transpose_1_1.cvc		diff \| blob \| history
test/regress/regress0/rels/rel_transpose_3.cvc		diff \| blob \| history
test/regress/regress0/rels/rel_transpose_4.cvc		diff \| blob \| history
test/regress/regress0/rels/rel_transpose_5.cvc		diff \| blob \| history
test/regress/regress0/rels/rel_transpose_6.cvc		diff \| blob \| history
test/regress/regress0/rels/rel_transpose_7.cvc		diff \| blob \| history
test/regress/regress0/rels/rels-sharing-simp.cvc		diff \| blob \| history
test/regress/regress0/sep/dispose-1.smt2		diff \| blob \| history
test/regress/regress0/sep/dup-nemp.smt2		diff \| blob \| history
test/regress/regress0/sep/issue5343-err.smt2		diff \| blob \| history
test/regress/regress0/sep/nspatial-simp.smt2		diff \| blob \| history
test/regress/regress0/sep/pto-01.smt2		diff \| blob \| history
test/regress/regress0/sep/pto-02.smt2		diff \| blob \| history
test/regress/regress0/sep/sep-01.smt2		diff \| blob \| history
test/regress/regress0/sep/sep-plus1.smt2		diff \| blob \| history
test/regress/regress0/sep/sep-simp-unsat-emp.smt2		diff \| blob \| history
test/regress/regress0/sep/simple-080420-const-sets.smt2		diff \| blob \| history
test/regress/regress0/sep/skolem_emp.smt2		diff \| blob \| history
test/regress/regress0/sep/trees-1.smt2		diff \| blob \| history
test/regress/regress0/sep/wand-crash.smt2		diff \| blob \| history
test/regress/regress0/sets/card-3sets.cvc		diff \| blob \| history
test/regress/regress0/sets/card3-ground.smt2		diff \| blob \| history
test/regress/regress0/sets/complement.cvc		diff \| blob \| history
test/regress/regress0/sets/complement2.cvc		diff \| blob \| history
test/regress/regress0/sets/complement3.cvc		diff \| blob \| history
test/regress/regress0/sets/cvc-sample.cvc		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/error2.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/setel-eq.smt2		diff \| blob \| history
test/regress/regress0/sets/sets-equal.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-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/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/strings/idof-rewrites.smt2		diff \| blob \| history
test/regress/regress0/strings/ilc-like.smt2		diff \| blob \| history
test/regress/regress0/strings/indexof-sym-simp.smt2		diff \| blob \| history
test/regress/regress0/strings/issue1189.smt2		diff \| blob \| history
test/regress/regress0/strings/tolower-simple.smt2		diff \| blob \| history
test/regress/regress0/sygus/dt-sel-parse1.sy		diff \| blob \| history
test/regress/regress1/bug507.smt2		diff \| blob \| history
test/regress/regress1/bug516.smt2		diff \| blob \| history
test/regress/regress1/bug519.smt2		diff \| blob \| history
test/regress/regress1/bug521.smt2		diff \| blob \| history
test/regress/regress1/bug543.smt2		diff \| blob \| history
test/regress/regress1/bug567.smt2		diff \| blob \| history
test/regress/regress1/bug681.smt2		diff \| blob \| history
test/regress/regress1/bv/bv-int-collapse2-sat.smt2		diff \| blob \| history
test/regress/regress1/bv/bv2nat-simp-range-sat.smt2		diff \| blob \| history
test/regress/regress1/bv/cmu-rdk-3.smt2		diff \| blob \| history
test/regress/regress1/datatypes/dt-param-card4-unsat.smt2		diff \| blob \| history
test/regress/regress1/datatypes/manos-model.smt2		diff \| blob \| history
test/regress/regress1/fmf/LeftistHeap.scala-8-ncm.smt2		diff \| blob \| history
test/regress/regress1/fmf/bug0909.smt2		diff \| blob \| history
test/regress/regress1/fmf/bug723-irrelevant-funs.smt2		diff \| blob \| history
test/regress/regress1/fmf/datatypes-ufinite-nested.smt2		diff \| blob \| history
test/regress/regress1/fmf/datatypes-ufinite.smt2		diff \| blob \| history
test/regress/regress1/fmf/dt-proper-model.smt2		diff \| blob \| history
test/regress/regress1/fmf/fib-core.smt2		diff \| blob \| history
test/regress/regress1/fmf/forall_unit_data.smt2		diff \| blob \| history
test/regress/regress1/fmf/fore19-exp2-core.smt2		diff \| blob \| history
test/regress/regress1/fmf/german169.smt2		diff \| blob \| history
test/regress/regress1/fmf/german73.smt2		diff \| blob \| history
test/regress/regress1/fmf/jasmin-cdt-crash.smt2		diff \| blob \| history
test/regress/regress1/fmf/loopy_coda.smt2		diff \| blob \| history
test/regress/regress1/fmf/lst-no-self-rev-exp.smt2		diff \| blob \| history
test/regress/regress1/fmf/nun-0208-to.smt2		diff \| blob \| history
test/regress/regress1/fmf/radu-quant-set.smt2		diff \| blob \| history
test/regress/regress1/fmf/refcount24.cvc.smt2		diff \| blob \| history
test/regress/regress1/fmf/sc-crash-052316.smt2		diff \| blob \| history
test/regress/regress1/fmf/with-ind-104-core.smt2		diff \| blob \| history
test/regress/regress1/push-pop/bug-fmf-fun-skolem.smt2		diff \| blob \| history
test/regress/regress1/quantifiers/anti-sk-simp.smt2		diff \| blob \| history
test/regress/regress1/quantifiers/bi-artm-s.smt2		diff \| blob \| history
test/regress/regress1/quantifiers/cdt-0208-to.smt2		diff \| blob \| history
test/regress/regress1/quantifiers/ext-ex-deq-trigger.smt2		diff \| blob \| history
test/regress/regress1/quantifiers/is-even.smt2		diff \| blob \| history
test/regress/regress1/quantifiers/macro-subtype-param.smt2		diff \| blob \| history
test/regress/regress1/quantifiers/parametric-lists.smt2		diff \| blob \| history
test/regress/regress1/quantifiers/stream-x2014-09-18-unsat.smt2		diff \| blob \| history
test/regress/regress1/quantifiers/subtype-param-unk.smt2		diff \| blob \| history
test/regress/regress1/quantifiers/subtype-param.smt2		diff \| blob \| history
test/regress/regress1/rels/addr_book_1.cvc		diff \| blob \| history
test/regress/regress1/rels/addr_book_1_1.cvc		diff \| blob \| history
test/regress/regress1/rels/bv1-unit.cvc		diff \| blob \| history
test/regress/regress1/rels/bv1-unitb.cvc		diff \| blob \| history
test/regress/regress1/rels/bv1.cvc		diff \| blob \| history
test/regress/regress1/rels/bv1p-sat.cvc		diff \| blob \| history
test/regress/regress1/rels/bv1p.cvc		diff \| blob \| history
test/regress/regress1/rels/bv2.cvc		diff \| blob \| history
test/regress/regress1/rels/iden_1_1.cvc		diff \| blob \| history
test/regress/regress1/rels/join-eq-structure-and.cvc		diff \| blob \| history
test/regress/regress1/rels/join-eq-structure.cvc		diff \| blob \| history
test/regress/regress1/rels/joinImg_0_1.cvc		diff \| blob \| history
test/regress/regress1/rels/joinImg_0_2.cvc		diff \| blob \| history
test/regress/regress1/rels/joinImg_1.cvc		diff \| blob \| history
test/regress/regress1/rels/joinImg_1_1.cvc		diff \| blob \| history
test/regress/regress1/rels/joinImg_2.cvc		diff \| blob \| history
test/regress/regress1/rels/joinImg_2_1.cvc		diff \| blob \| history
test/regress/regress1/rels/prod-mod-eq.cvc		diff \| blob \| history
test/regress/regress1/rels/prod-mod-eq2.cvc		diff \| blob \| history
test/regress/regress1/rels/rel_complex_3.cvc		diff \| blob \| history
test/regress/regress1/rels/rel_complex_4.cvc		diff \| blob \| history
test/regress/regress1/rels/rel_complex_5.cvc		diff \| blob \| history
test/regress/regress1/rels/rel_mix_0_1.cvc		diff \| blob \| history
test/regress/regress1/rels/rel_pressure_0.cvc		diff \| blob \| history
test/regress/regress1/rels/rel_tc_10_1.cvc		diff \| blob \| history
test/regress/regress1/rels/rel_tc_4.cvc		diff \| blob \| history
test/regress/regress1/rels/rel_tc_4_1.cvc		diff \| blob \| history
test/regress/regress1/rels/rel_tc_5_1.cvc		diff \| blob \| history
test/regress/regress1/rels/rel_tc_6.cvc		diff \| blob \| history
test/regress/regress1/rels/rel_tc_9_1.cvc		diff \| blob \| history
test/regress/regress1/rels/rel_tp_2.cvc		diff \| blob \| history
test/regress/regress1/rels/rel_tp_join_2_1.cvc		diff \| blob \| history
test/regress/regress1/rels/set-strat.cvc		diff \| blob \| history
test/regress/regress1/rels/strat.cvc		diff \| blob \| history
test/regress/regress1/sep/chain-int.smt2		diff \| blob \| history
test/regress/regress1/sep/crash1220.smt2		diff \| blob \| history
test/regress/regress1/sep/dispose-list-4-init.smt2		diff \| blob \| history
test/regress/regress1/sep/emp2-quant-unsat.smt2		diff \| blob \| history
test/regress/regress1/sep/finite-witness-sat.smt2		diff \| blob \| history
test/regress/regress1/sep/fmf-nemp-2.smt2		diff \| blob \| history
test/regress/regress1/sep/loop-1220.smt2		diff \| blob \| history
test/regress/regress1/sep/pto-04.smt2		diff \| blob \| history
test/regress/regress1/sep/quant_wand.smt2		diff \| blob \| history
test/regress/regress1/sep/sep-02.smt2		diff \| blob \| history
test/regress/regress1/sep/sep-03.smt2		diff \| blob \| history
test/regress/regress1/sep/sep-fmf-priority.smt2		diff \| blob \| history
test/regress/regress1/sep/sep-neg-1refine.smt2		diff \| blob \| history
test/regress/regress1/sep/sep-neg-nstrict.smt2		diff \| blob \| history
test/regress/regress1/sep/sep-neg-nstrict2.smt2		diff \| blob \| history
test/regress/regress1/sep/sep-neg-simple.smt2		diff \| blob \| history
test/regress/regress1/sep/sep-neg-swap.smt2		diff \| blob \| history
test/regress/regress1/sep/sep-nterm-again.smt2		diff \| blob \| history
test/regress/regress1/sep/sep-nterm-val-model.smt2		diff \| blob \| history
test/regress/regress1/sep/sep-simp-unc.smt2		diff \| blob \| history
test/regress/regress1/sep/simple-neg-sat.smt2		diff \| blob \| history
test/regress/regress1/sep/split-find-unsat-w-emp.smt2		diff \| blob \| history
test/regress/regress1/sep/split-find-unsat.smt2		diff \| blob \| history
test/regress/regress1/sep/wand-0526-sat.smt2		diff \| blob \| history
test/regress/regress1/sep/wand-false.smt2		diff \| blob \| history
test/regress/regress1/sep/wand-nterm-simp.smt2		diff \| blob \| history
test/regress/regress1/sep/wand-nterm-simp2.smt2		diff \| blob \| history
test/regress/regress1/sep/wand-simp-sat.smt2		diff \| blob \| history
test/regress/regress1/sep/wand-simp-sat2.smt2		diff \| blob \| history
test/regress/regress1/sep/wand-simp-unsat.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/deepmeas0.hs.fqout.cvc4.41.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-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-datatype-1.smt2		diff \| blob \| history
test/regress/regress1/sets/finite-type/sets-card-datatype-2.smt2		diff \| blob \| history
test/regress/regress1/sets/is_singleton1.smt2		diff \| blob \| history
test/regress/regress1/sets/issue2904.smt2		diff \| blob \| history
test/regress/regress1/sets/lemmabug-ListElts317minimized.smt2		diff \| blob \| history
test/regress/regress1/sets/sets-tuple-poly.cvc		diff \| blob \| history
test/regress/regress1/strings/cmu-2db2-extf-reg.smt2		diff \| blob \| history
test/regress/regress1/strings/cmu-5042-0707-2.smt2		diff \| blob \| history
test/regress/regress1/strings/cmu-inc-nlpp-071516.smt2		diff \| blob \| history
test/regress/regress1/strings/cmu-substr-rw.smt2		diff \| blob \| history
test/regress/regress1/strings/crash-1019.smt2		diff \| blob \| history
test/regress/regress1/strings/gm-inc-071516-2.smt2		diff \| blob \| history
test/regress/regress1/strings/idof-handg.smt2		diff \| blob \| history
test/regress/regress1/strings/idof-nconst-index.smt2		diff \| blob \| history
test/regress/regress1/strings/idof-neg-index.smt2		diff \| blob \| history
test/regress/regress1/strings/idof-triv.smt2		diff \| blob \| history
test/regress/regress1/strings/ilc-l-nt.smt2		diff \| blob \| history
test/regress/regress1/strings/issue3090.smt2		diff \| blob \| history
test/regress/regress1/strings/issue3217.smt2		diff \| blob \| history
test/regress/regress1/strings/issue3272.smt2		diff \| blob \| history
test/regress/regress1/strings/issue3357.smt2		diff \| blob \| history
test/regress/regress1/strings/tolower-find.smt2		diff \| blob \| history
test/regress/regress1/sygus/clock-inc-tuple.sy		diff \| blob \| history
test/regress/regress1/sygus/error1-dt.sy		diff \| blob \| history
test/regress/regress1/sygus/extract.sy		diff \| blob \| history
test/regress/regress1/sygus/issue3461.sy		diff \| blob \| history
test/regress/regress1/sygus/list-head-x.sy		diff \| blob \| history
test/regress/regress2/bug394.smt2		diff \| blob \| history
test/regress/regress2/bug674.smt2		diff \| blob \| history
test/regress/regress2/bug765.smt2		diff \| blob \| history
test/regress/regress2/issue6495-dup-pat-term.smt2		diff \| blob \| history
test/regress/regress2/quantifiers/nunchaku2309663.nun.min.smt2		diff \| blob \| history
test/regress/regress2/strings/cmu-dis-0707-3.smt2		diff \| blob \| history
test/regress/regress2/strings/cmu-disagree-0707-dd.smt2		diff \| blob \| history
test/regress/regress2/strings/cmu-prereg-fmf.smt2		diff \| blob \| history
test/regress/regress2/strings/cmu-repl-len-nterm.smt2		diff \| blob \| history
test/regress/regress2/strings/issue3203.smt2		diff \| blob \| history
test/regress/regress3/quantifiers/ForElimination-scala-9.smt2		diff \| blob \| history
test/regress/regress4/bug396.smt2		diff \| blob \| history
test/unit/api/solver_black.cpp		diff \| blob \| history
test/unit/theory/logic_info_white.cpp		diff \| blob \| history

RSS Atom