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

author	Mathias Preiner <mathias.preiner@gmail.com>
	Tue, 5 Apr 2022 20:38:57 +0000 (13:38 -0700)
committer	GitHub <noreply@github.com>
	Tue, 5 Apr 2022 20:38:57 +0000 (20:38 +0000)
commit	d01e59c13b7337e68806be72145b3e45e4cad89c
tree	cc2cc63cc1279dfce3213a33a197d62d52bef417	tree
parent	2a1fa5d6732600b0e675539d4dcd95f57b1577a8	commit \| diff

Update copyright headers for release 1.0 (#8539)

1742 files changed:

CMakeLists.txt		diff \| blob \| history
cmake/CMakeGraphVizOptions.cmake.in		diff \| blob \| history
cmake/ConfigCompetition.cmake		diff \| blob \| history
cmake/ConfigDebug.cmake		diff \| blob \| history
cmake/ConfigProduction.cmake		diff \| blob \| history
cmake/ConfigTesting.cmake		diff \| blob \| history
cmake/ConfigureCvc5.cmake		diff \| blob \| history
cmake/FindANTLR3.cmake		diff \| blob \| history
cmake/FindCLN.cmake		diff \| blob \| history
cmake/FindCVC5PythonicAPI.cmake		diff \| blob \| history
cmake/FindCaDiCaL.cmake		diff \| blob \| history
cmake/FindCoCoA.cmake		diff \| blob \| history
cmake/FindCryptoMiniSat.cmake		diff \| blob \| history
cmake/FindDrat2Er.cmake		diff \| blob \| history
cmake/FindDummy.cmake.template		diff \| blob \| history
cmake/FindEditline.cmake		diff \| blob \| history
cmake/FindGLPK.cmake		diff \| blob \| history
cmake/FindGMP.cmake		diff \| blob \| history
cmake/FindGTest.cmake		diff \| blob \| history
cmake/FindHamcrest.cmake		diff \| blob \| history
cmake/FindJUnit.cmake		diff \| blob \| history
cmake/FindKissat.cmake		diff \| blob \| history
cmake/FindLFSC.cmake		diff \| blob \| history
cmake/FindPoly.cmake		diff \| blob \| history
cmake/FindSphinx.cmake		diff \| blob \| history
cmake/FindSymFPU.cmake		diff \| blob \| history
cmake/FindValgrind.cmake		diff \| blob \| history
cmake/Helpers.cmake		diff \| blob \| history
cmake/IWYU.cmake		diff \| blob \| history
cmake/Toolchain-aarch64.cmake		diff \| blob \| history
cmake/Toolchain-mingw64.cmake		diff \| blob \| history
cmake/cvc5Config.cmake.in		diff \| blob \| history
cmake/deps-helper.cmake		diff \| blob \| history
cmake/fuzzing-murxla.cmake		diff \| blob \| history
cmake/target-graphs.cmake		diff \| blob \| history
cmake/version.cmake		diff \| blob \| history
contrib/get-authors		diff \| blob \| history
contrib/update-copyright.pl		diff \| blob \| history
examples/CMakeLists.txt		diff \| blob \| history
examples/SimpleVC.java		diff \| blob \| history
examples/api/cpp/CMakeLists.txt		diff \| blob \| history
examples/api/cpp/bags.cpp		diff \| blob \| history
examples/api/cpp/bitvectors.cpp		diff \| blob \| history
examples/api/cpp/bitvectors_and_arrays.cpp		diff \| blob \| history
examples/api/cpp/combination.cpp		diff \| blob \| history
examples/api/cpp/datatypes.cpp		diff \| blob \| history
examples/api/cpp/extract.cpp		diff \| blob \| history
examples/api/cpp/floating_point_arith.cpp		diff \| blob \| history
examples/api/cpp/helloworld.cpp		diff \| blob \| history
examples/api/cpp/linear_arith.cpp		diff \| blob \| history
examples/api/cpp/quickstart.cpp		diff \| blob \| history
examples/api/cpp/relations.cpp		diff \| blob \| history
examples/api/cpp/sequences.cpp		diff \| blob \| history
examples/api/cpp/sets.cpp		diff \| blob \| history
examples/api/cpp/strings.cpp		diff \| blob \| history
examples/api/cpp/sygus-fun.cpp		diff \| blob \| history
examples/api/cpp/sygus-grammar.cpp		diff \| blob \| history
examples/api/cpp/sygus-inv.cpp		diff \| blob \| history
examples/api/cpp/transcendentals.cpp		diff \| blob \| history
examples/api/cpp/utils.cpp		diff \| blob \| history
examples/api/cpp/utils.h		diff \| blob \| history
examples/api/java/Bags.java		diff \| blob \| history
examples/api/java/BitVectors.java		diff \| blob \| history
examples/api/java/BitVectorsAndArrays.java		diff \| blob \| history
examples/api/java/CMakeLists.txt		diff \| blob \| history
examples/api/java/Combination.java		diff \| blob \| history
examples/api/java/Datatypes.java		diff \| blob \| history
examples/api/java/Exceptions.java		diff \| blob \| history
examples/api/java/Extract.java		diff \| blob \| history
examples/api/java/FloatingPointArith.java		diff \| blob \| history
examples/api/java/HelloWorld.java		diff \| blob \| history
examples/api/java/LinearArith.java		diff \| blob \| history
examples/api/java/QuickStart.java		diff \| blob \| history
examples/api/java/Relations.java		diff \| blob \| history
examples/api/java/Sequences.java		diff \| blob \| history
examples/api/java/Sets.java		diff \| blob \| history
examples/api/java/Statistics.java		diff \| blob \| history
examples/api/java/Strings.java		diff \| blob \| history
examples/api/java/SygusFun.java		diff \| blob \| history
examples/api/java/SygusGrammar.java		diff \| blob \| history
examples/api/java/SygusInv.java		diff \| blob \| history
examples/api/java/Transcendentals.java		diff \| blob \| history
examples/api/java/UnsatCores.java		diff \| blob \| history
examples/api/java/Utils.java		diff \| blob \| history
examples/api/python/CMakeLists.txt		diff \| blob \| history
examples/api/python/bags.py		diff \| blob \| history
examples/api/python/bitvectors.py		diff \| blob \| history
examples/api/python/bitvectors_and_arrays.py		diff \| blob \| history
examples/api/python/combination.py		diff \| blob \| history
examples/api/python/datatypes.py		diff \| blob \| history
examples/api/python/exceptions.py		diff \| blob \| history
examples/api/python/extract.py		diff \| blob \| history
examples/api/python/floating_point.py		diff \| blob \| history
examples/api/python/helloworld.py		diff \| blob \| history
examples/api/python/id.py		diff \| blob \| history
examples/api/python/linear_arith.py		diff \| blob \| history
examples/api/python/quickstart.py		diff \| blob \| history
examples/api/python/relations.py		diff \| blob \| history
examples/api/python/sequences.py		diff \| blob \| history
examples/api/python/sets.py		diff \| blob \| history
examples/api/python/strings.py		diff \| blob \| history
examples/api/python/sygus-fun.py		diff \| blob \| history
examples/api/python/sygus-grammar.py		diff \| blob \| history
examples/api/python/sygus-inv.py		diff \| blob \| history
examples/api/python/transcendentals.py		diff \| blob \| history
examples/api/python/utils.py		diff \| blob \| history
examples/simple_vc_cxx.cpp		diff \| blob \| history
examples/simple_vc_quant_cxx.cpp		diff \| blob \| history
src/CMakeLists.txt		diff \| blob \| history
src/api/cpp/cvc5.cpp		diff \| blob \| history
src/api/cpp/cvc5.h		diff \| blob \| history
src/api/cpp/cvc5_checks.h		diff \| blob \| history
src/api/cpp/cvc5_kind.h		diff \| blob \| history
src/api/cpp/cvc5_types.cpp		diff \| blob \| history
src/api/cpp/cvc5_types.h		diff \| blob \| history
src/api/java/CMakeLists.txt		diff \| blob \| history
src/api/java/genenums.py.in		diff \| blob \| history
src/api/java/io/github/cvc5/AbstractPointer.java		diff \| blob \| history
src/api/java/io/github/cvc5/CVC5ApiException.java		diff \| blob \| history
src/api/java/io/github/cvc5/CVC5ApiOptionException.java		diff \| blob \| history
src/api/java/io/github/cvc5/CVC5ApiRecoverableException.java		diff \| blob \| history
src/api/java/io/github/cvc5/Datatype.java		diff \| blob \| history
src/api/java/io/github/cvc5/DatatypeConstructor.java		diff \| blob \| history
src/api/java/io/github/cvc5/DatatypeConstructorDecl.java		diff \| blob \| history
src/api/java/io/github/cvc5/DatatypeDecl.java		diff \| blob \| history
src/api/java/io/github/cvc5/DatatypeSelector.java		diff \| blob \| history
src/api/java/io/github/cvc5/Grammar.java		diff \| blob \| history
src/api/java/io/github/cvc5/IPointer.java		diff \| blob \| history
src/api/java/io/github/cvc5/Op.java		diff \| blob \| history
src/api/java/io/github/cvc5/OptionInfo.java		diff \| blob \| history
src/api/java/io/github/cvc5/Pair.java		diff \| blob \| history
src/api/java/io/github/cvc5/Result.java		diff \| blob \| history
src/api/java/io/github/cvc5/Solver.java		diff \| blob \| history
src/api/java/io/github/cvc5/Sort.java		diff \| blob \| history
src/api/java/io/github/cvc5/Stat.java		diff \| blob \| history
src/api/java/io/github/cvc5/Statistics.java		diff \| blob \| history
src/api/java/io/github/cvc5/SynthResult.java		diff \| blob \| history
src/api/java/io/github/cvc5/Term.java		diff \| blob \| history
src/api/java/io/github/cvc5/Triplet.java		diff \| blob \| history
src/api/java/io/github/cvc5/Utils.java		diff \| blob \| history
src/api/java/jni/api_utilities.cpp		diff \| blob \| history
src/api/java/jni/api_utilities.h		diff \| blob \| history
src/api/java/jni/datatype.cpp		diff \| blob \| history
src/api/java/jni/datatype_constructor.cpp		diff \| blob \| history
src/api/java/jni/datatype_constructor_decl.cpp		diff \| blob \| history
src/api/java/jni/datatype_decl.cpp		diff \| blob \| history
src/api/java/jni/datatype_selector.cpp		diff \| blob \| history
src/api/java/jni/grammar.cpp		diff \| blob \| history
src/api/java/jni/op.cpp		diff \| blob \| history
src/api/java/jni/option_info.cpp		diff \| blob \| history
src/api/java/jni/result.cpp		diff \| blob \| history
src/api/java/jni/solver.cpp		diff \| blob \| history
src/api/java/jni/sort.cpp		diff \| blob \| history
src/api/java/jni/stat.cpp		diff \| blob \| history
src/api/java/jni/statistics.cpp		diff \| blob \| history
src/api/java/jni/synth_result.cpp		diff \| blob \| history
src/api/java/jni/term.cpp		diff \| blob \| history
src/api/parseenums.py		diff \| blob \| history
src/api/python/CMakeLists.txt		diff \| blob \| history
src/api/python/genenums.py.in		diff \| blob \| history
src/api/python/setup.py.in		diff \| blob \| history
src/base/CMakeLists.txt		diff \| blob \| history
src/base/check.cpp		diff \| blob \| history
src/base/check.h		diff \| blob \| history
src/base/collect_tags.py		diff \| blob \| history
src/base/configuration.cpp		diff \| blob \| history
src/base/configuration.h		diff \| blob \| history
src/base/configuration_private.h		diff \| blob \| history
src/base/cvc5config.h.in		diff \| blob \| history
src/base/exception.cpp		diff \| blob \| history
src/base/exception.h		diff \| blob \| history
src/base/listener.cpp		diff \| blob \| history
src/base/listener.h		diff \| blob \| history
src/base/map_util.h		diff \| blob \| history
src/base/modal_exception.h		diff \| blob \| history
src/base/output.cpp		diff \| blob \| history
src/base/output.h		diff \| blob \| history
src/base/versioninfo.cpp.in		diff \| blob \| history
src/context/CMakeLists.txt		diff \| blob \| history
src/context/cdhashmap.h		diff \| blob \| history
src/context/cdhashmap_forward.h		diff \| blob \| history
src/context/cdhashset.h		diff \| blob \| history
src/context/cdhashset_forward.h		diff \| blob \| history
src/context/cdinsert_hashmap.h		diff \| blob \| history
src/context/cdinsert_hashmap_forward.h		diff \| blob \| history
src/context/cdlist.h		diff \| blob \| history
src/context/cdlist_forward.h		diff \| blob \| history
src/context/cdmaybe.h		diff \| blob \| history
src/context/cdo.h		diff \| blob \| history
src/context/cdqueue.h		diff \| blob \| history
src/context/cdtrail_queue.h		diff \| blob \| history
src/context/context.cpp		diff \| blob \| history
src/context/context.h		diff \| blob \| history
src/context/context_mm.cpp		diff \| blob \| history
src/context/context_mm.h		diff \| blob \| history
src/decision/assertion_list.cpp		diff \| blob \| history
src/decision/assertion_list.h		diff \| blob \| history
src/decision/decision_engine.cpp		diff \| blob \| history
src/decision/decision_engine.h		diff \| blob \| history
src/decision/justification_strategy.cpp		diff \| blob \| history
src/decision/justification_strategy.h		diff \| blob \| history
src/decision/justify_info.cpp		diff \| blob \| history
src/decision/justify_info.h		diff \| blob \| history
src/decision/justify_stack.cpp		diff \| blob \| history
src/decision/justify_stack.h		diff \| blob \| history
src/decision/justify_stats.cpp		diff \| blob \| history
src/decision/justify_stats.h		diff \| blob \| history
src/expr/CMakeLists.txt		diff \| blob \| history
src/expr/algorithm/flatten.h		diff \| blob \| history
src/expr/annotation_elim_node_converter.cpp		diff \| blob \| history
src/expr/annotation_elim_node_converter.h		diff \| blob \| history
src/expr/array_store_all.cpp		diff \| blob \| history
src/expr/array_store_all.h		diff \| blob \| history
src/expr/ascription_type.cpp		diff \| blob \| history
src/expr/ascription_type.h		diff \| blob \| history
src/expr/attribute.cpp		diff \| blob \| history
src/expr/attribute.h		diff \| blob \| history
src/expr/attribute_internals.h		diff \| blob \| history
src/expr/attribute_unique_id.h		diff \| blob \| history
src/expr/bound_var_manager.cpp		diff \| blob \| history
src/expr/bound_var_manager.h		diff \| blob \| history
src/expr/cardinality_constraint.cpp		diff \| blob \| history
src/expr/cardinality_constraint.h		diff \| blob \| history
src/expr/codatatype_bound_variable.cpp		diff \| blob \| history
src/expr/codatatype_bound_variable.h		diff \| blob \| history
src/expr/datatype_index.cpp		diff \| blob \| history
src/expr/datatype_index.h		diff \| blob \| history
src/expr/dtype.cpp		diff \| blob \| history
src/expr/dtype.h		diff \| blob \| history
src/expr/dtype_cons.cpp		diff \| blob \| history
src/expr/dtype_cons.h		diff \| blob \| history
src/expr/dtype_selector.cpp		diff \| blob \| history
src/expr/dtype_selector.h		diff \| blob \| history
src/expr/emptybag.cpp		diff \| blob \| history
src/expr/emptybag.h		diff \| blob \| history
src/expr/emptyset.cpp		diff \| blob \| history
src/expr/emptyset.h		diff \| blob \| history
src/expr/kind_map.h		diff \| blob \| history
src/expr/kind_template.cpp		diff \| blob \| history
src/expr/kind_template.h		diff \| blob \| history
src/expr/match_trie.cpp		diff \| blob \| history
src/expr/match_trie.h		diff \| blob \| history
src/expr/metakind_template.cpp		diff \| blob \| history
src/expr/metakind_template.h		diff \| blob \| history
src/expr/mkexpr		diff \| blob \| history
src/expr/mkkind		diff \| blob \| history
src/expr/mkmetakind		diff \| blob \| history
src/expr/nary_match_trie.cpp		diff \| blob \| history
src/expr/nary_match_trie.h		diff \| blob \| history
src/expr/nary_term_util.cpp		diff \| blob \| history
src/expr/nary_term_util.h		diff \| blob \| history
src/expr/node.cpp		diff \| blob \| history
src/expr/node.h		diff \| blob \| history
src/expr/node_algorithm.cpp		diff \| blob \| history
src/expr/node_algorithm.h		diff \| blob \| history
src/expr/node_builder.cpp		diff \| blob \| history
src/expr/node_builder.h		diff \| blob \| history
src/expr/node_converter.cpp		diff \| blob \| history
src/expr/node_converter.h		diff \| blob \| history
src/expr/node_manager_attributes.h		diff \| blob \| history
src/expr/node_manager_template.cpp		diff \| blob \| history
src/expr/node_manager_template.h		diff \| blob \| history
src/expr/node_self_iterator.h		diff \| blob \| history
src/expr/node_traversal.cpp		diff \| blob \| history
src/expr/node_traversal.h		diff \| blob \| history
src/expr/node_trie.cpp		diff \| blob \| history
src/expr/node_trie.h		diff \| blob \| history
src/expr/node_trie_algorithm.cpp		diff \| blob \| history
src/expr/node_trie_algorithm.h		diff \| blob \| history
src/expr/node_value.cpp		diff \| blob \| history
src/expr/node_value.h		diff \| blob \| history
src/expr/node_visitor.h		diff \| blob \| history
src/expr/sequence.cpp		diff \| blob \| history
src/expr/sequence.h		diff \| blob \| history
src/expr/skolem_manager.cpp		diff \| blob \| history
src/expr/skolem_manager.h		diff \| blob \| history
src/expr/subs.cpp		diff \| blob \| history
src/expr/subs.h		diff \| blob \| history
src/expr/subtype_elim_node_converter.cpp		diff \| blob \| history
src/expr/subtype_elim_node_converter.h		diff \| blob \| history
src/expr/sygus_datatype.cpp		diff \| blob \| history
src/expr/sygus_datatype.h		diff \| blob \| history
src/expr/symbol_manager.cpp		diff \| blob \| history
src/expr/symbol_manager.h		diff \| blob \| history
src/expr/symbol_table.cpp		diff \| blob \| history
src/expr/symbol_table.h		diff \| blob \| history
src/expr/term_canonize.cpp		diff \| blob \| history
src/expr/term_canonize.h		diff \| blob \| history
src/expr/term_context.cpp		diff \| blob \| history
src/expr/term_context.h		diff \| blob \| history
src/expr/term_context_node.cpp		diff \| blob \| history
src/expr/term_context_node.h		diff \| blob \| history
src/expr/term_context_stack.cpp		diff \| blob \| history
src/expr/term_context_stack.h		diff \| blob \| history
src/expr/type_checker.h		diff \| blob \| history
src/expr/type_checker_template.cpp		diff \| blob \| history
src/expr/type_checker_util.h		diff \| blob \| history
src/expr/type_matcher.cpp		diff \| blob \| history
src/expr/type_matcher.h		diff \| blob \| history
src/expr/type_node.cpp		diff \| blob \| history
src/expr/type_node.h		diff \| blob \| history
src/expr/type_properties_template.cpp		diff \| blob \| history
src/expr/type_properties_template.h		diff \| blob \| history
src/expr/variadic_trie.cpp		diff \| blob \| history
src/expr/variadic_trie.h		diff \| blob \| history
src/include/cvc5_private.h		diff \| blob \| history
src/include/cvc5_private_library.h		diff \| blob \| history
src/include/cvc5_public.h		diff \| blob \| history
src/include/cvc5parser_private.h		diff \| blob \| history
src/include/cvc5parser_public.h		diff \| blob \| history
src/lib/clock_gettime.c		diff \| blob \| history
src/lib/clock_gettime.h		diff \| blob \| history
src/lib/ffs.c		diff \| blob \| history
src/lib/ffs.h		diff \| blob \| history
src/lib/replacements.h		diff \| blob \| history
src/lib/strtok_r.c		diff \| blob \| history
src/lib/strtok_r.h		diff \| blob \| history
src/main/CMakeLists.txt		diff \| blob \| history
src/main/command_executor.cpp		diff \| blob \| history
src/main/command_executor.h		diff \| blob \| history
src/main/driver_unified.cpp		diff \| blob \| history
src/main/interactive_shell.cpp		diff \| blob \| history
src/main/interactive_shell.h		diff \| blob \| history
src/main/main.cpp		diff \| blob \| history
src/main/main.h		diff \| blob \| history
src/main/options.h		diff \| blob \| history
src/main/options_template.cpp		diff \| blob \| history
src/main/signal_handlers.cpp		diff \| blob \| history
src/main/signal_handlers.h		diff \| blob \| history
src/main/time_limit.cpp		diff \| blob \| history
src/main/time_limit.h		diff \| blob \| history
src/omt/bitvector_optimizer.cpp		diff \| blob \| history
src/omt/bitvector_optimizer.h		diff \| blob \| history
src/omt/integer_optimizer.cpp		diff \| blob \| history
src/omt/integer_optimizer.h		diff \| blob \| history
src/omt/omt_optimizer.cpp		diff \| blob \| history
src/omt/omt_optimizer.h		diff \| blob \| history
src/options/didyoumean_test.cpp		diff \| blob \| history
src/options/io_utils.cpp		diff \| blob \| history
src/options/io_utils.h		diff \| blob \| history
src/options/language.cpp		diff \| blob \| history
src/options/language.h		diff \| blob \| history
src/options/managed_streams.cpp		diff \| blob \| history
src/options/managed_streams.h		diff \| blob \| history
src/options/mkoptions.py		diff \| blob \| history
src/options/module_template.cpp		diff \| blob \| history
src/options/module_template.h		diff \| blob \| history
src/options/option_exception.cpp		diff \| blob \| history
src/options/option_exception.h		diff \| blob \| history
src/options/options_handler.cpp		diff \| blob \| history
src/options/options_handler.h		diff \| blob \| history
src/options/options_listener.h		diff \| blob \| history
src/options/options_public.h		diff \| blob \| history
src/options/options_public_template.cpp		diff \| blob \| history
src/options/options_template.cpp		diff \| blob \| history
src/options/options_template.h		diff \| blob \| history
src/parser/CMakeLists.txt		diff \| blob \| history
src/parser/antlr_input.cpp		diff \| blob \| history
src/parser/antlr_input.h		diff \| blob \| history
src/parser/antlr_input_imports.cpp		diff \| blob \| history
src/parser/antlr_line_buffered_input.cpp		diff \| blob \| history
src/parser/antlr_line_buffered_input.h		diff \| blob \| history
src/parser/bounded_token_buffer.cpp		diff \| blob \| history
src/parser/bounded_token_buffer.h		diff \| blob \| history
src/parser/bounded_token_factory.cpp		diff \| blob \| history
src/parser/bounded_token_factory.h		diff \| blob \| history
src/parser/input.cpp		diff \| blob \| history
src/parser/input.h		diff \| blob \| history
src/parser/line_buffer.cpp		diff \| blob \| history
src/parser/line_buffer.h		diff \| blob \| history
src/parser/parse_op.cpp		diff \| blob \| history
src/parser/parse_op.h		diff \| blob \| history
src/parser/parser.cpp		diff \| blob \| history
src/parser/parser.h		diff \| blob \| history
src/parser/parser_builder.cpp		diff \| blob \| history
src/parser/parser_builder.h		diff \| blob \| history
src/parser/parser_exception.h		diff \| blob \| history
src/parser/smt2/Smt2.g		diff \| blob \| history
src/parser/smt2/smt2.cpp		diff \| blob \| history
src/parser/smt2/smt2.h		diff \| blob \| history
src/parser/smt2/smt2_input.cpp		diff \| blob \| history
src/parser/smt2/smt2_input.h		diff \| blob \| history
src/parser/smt2/sygus_input.cpp		diff \| blob \| history
src/parser/smt2/sygus_input.h		diff \| blob \| history
src/parser/tptp/Tptp.g		diff \| blob \| history
src/parser/tptp/tptp.cpp		diff \| blob \| history
src/parser/tptp/tptp.h		diff \| blob \| history
src/parser/tptp/tptp_input.cpp		diff \| blob \| history
src/parser/tptp/tptp_input.h		diff \| blob \| history
src/preprocessing/assertion_pipeline.cpp		diff \| blob \| history
src/preprocessing/assertion_pipeline.h		diff \| blob \| history
src/preprocessing/learned_literal_manager.cpp		diff \| blob \| history
src/preprocessing/learned_literal_manager.h		diff \| blob \| history
src/preprocessing/passes/ackermann.cpp		diff \| blob \| history
src/preprocessing/passes/ackermann.h		diff \| blob \| history
src/preprocessing/passes/apply_substs.cpp		diff \| blob \| history
src/preprocessing/passes/apply_substs.h		diff \| blob \| history
src/preprocessing/passes/bool_to_bv.cpp		diff \| blob \| history
src/preprocessing/passes/bool_to_bv.h		diff \| blob \| history
src/preprocessing/passes/bv_eager_atoms.cpp		diff \| blob \| history
src/preprocessing/passes/bv_eager_atoms.h		diff \| blob \| history
src/preprocessing/passes/bv_gauss.cpp		diff \| blob \| history
src/preprocessing/passes/bv_gauss.h		diff \| blob \| history
src/preprocessing/passes/bv_intro_pow2.cpp		diff \| blob \| history
src/preprocessing/passes/bv_intro_pow2.h		diff \| blob \| history
src/preprocessing/passes/bv_to_bool.cpp		diff \| blob \| history
src/preprocessing/passes/bv_to_bool.h		diff \| blob \| history
src/preprocessing/passes/bv_to_int.cpp		diff \| blob \| history
src/preprocessing/passes/bv_to_int.h		diff \| blob \| history
src/preprocessing/passes/extended_rewriter_pass.cpp		diff \| blob \| history
src/preprocessing/passes/extended_rewriter_pass.h		diff \| blob \| history
src/preprocessing/passes/foreign_theory_rewrite.cpp		diff \| blob \| history
src/preprocessing/passes/foreign_theory_rewrite.h		diff \| blob \| history
src/preprocessing/passes/fun_def_fmf.cpp		diff \| blob \| history
src/preprocessing/passes/fun_def_fmf.h		diff \| blob \| history
src/preprocessing/passes/global_negate.cpp		diff \| blob \| history
src/preprocessing/passes/global_negate.h		diff \| blob \| history
src/preprocessing/passes/ho_elim.cpp		diff \| blob \| history
src/preprocessing/passes/ho_elim.h		diff \| blob \| history
src/preprocessing/passes/int_to_bv.cpp		diff \| blob \| history
src/preprocessing/passes/int_to_bv.h		diff \| blob \| history
src/preprocessing/passes/ite_removal.cpp		diff \| blob \| history
src/preprocessing/passes/ite_removal.h		diff \| blob \| history
src/preprocessing/passes/ite_simp.cpp		diff \| blob \| history
src/preprocessing/passes/ite_simp.h		diff \| blob \| history
src/preprocessing/passes/learned_rewrite.cpp		diff \| blob \| history
src/preprocessing/passes/learned_rewrite.h		diff \| blob \| history
src/preprocessing/passes/miplib_trick.cpp		diff \| blob \| history
src/preprocessing/passes/miplib_trick.h		diff \| blob \| history
src/preprocessing/passes/nl_ext_purify.cpp		diff \| blob \| history
src/preprocessing/passes/nl_ext_purify.h		diff \| blob \| history
src/preprocessing/passes/non_clausal_simp.cpp		diff \| blob \| history
src/preprocessing/passes/non_clausal_simp.h		diff \| blob \| history
src/preprocessing/passes/pseudo_boolean_processor.cpp		diff \| blob \| history
src/preprocessing/passes/pseudo_boolean_processor.h		diff \| blob \| history
src/preprocessing/passes/quantifiers_preprocess.cpp		diff \| blob \| history
src/preprocessing/passes/quantifiers_preprocess.h		diff \| blob \| history
src/preprocessing/passes/real_to_int.cpp		diff \| blob \| history
src/preprocessing/passes/real_to_int.h		diff \| blob \| history
src/preprocessing/passes/rewrite.cpp		diff \| blob \| history
src/preprocessing/passes/rewrite.h		diff \| blob \| history
src/preprocessing/passes/sep_skolem_emp.cpp		diff \| blob \| history
src/preprocessing/passes/sep_skolem_emp.h		diff \| blob \| history
src/preprocessing/passes/sort_infer.cpp		diff \| blob \| history
src/preprocessing/passes/sort_infer.h		diff \| blob \| history
src/preprocessing/passes/static_learning.cpp		diff \| blob \| history
src/preprocessing/passes/static_learning.h		diff \| blob \| history
src/preprocessing/passes/strings_eager_pp.cpp		diff \| blob \| history
src/preprocessing/passes/strings_eager_pp.h		diff \| blob \| history
src/preprocessing/passes/sygus_inference.cpp		diff \| blob \| history
src/preprocessing/passes/sygus_inference.h		diff \| blob \| history
src/preprocessing/passes/synth_rew_rules.cpp		diff \| blob \| history
src/preprocessing/passes/synth_rew_rules.h		diff \| blob \| history
src/preprocessing/passes/theory_preprocess.cpp		diff \| blob \| history
src/preprocessing/passes/theory_preprocess.h		diff \| blob \| history
src/preprocessing/passes/theory_rewrite_eq.cpp		diff \| blob \| history
src/preprocessing/passes/theory_rewrite_eq.h		diff \| blob \| history
src/preprocessing/passes/unconstrained_simplifier.cpp		diff \| blob \| history
src/preprocessing/passes/unconstrained_simplifier.h		diff \| blob \| history
src/preprocessing/preprocessing_pass.cpp		diff \| blob \| history
src/preprocessing/preprocessing_pass.h		diff \| blob \| history
src/preprocessing/preprocessing_pass_context.cpp		diff \| blob \| history
src/preprocessing/preprocessing_pass_context.h		diff \| blob \| history
src/preprocessing/preprocessing_pass_registry.cpp		diff \| blob \| history
src/preprocessing/preprocessing_pass_registry.h		diff \| blob \| history
src/preprocessing/util/ite_utilities.cpp		diff \| blob \| history
src/preprocessing/util/ite_utilities.h		diff \| blob \| history
src/printer/ast/ast_printer.cpp		diff \| blob \| history
src/printer/ast/ast_printer.h		diff \| blob \| history
src/printer/let_binding.cpp		diff \| blob \| history
src/printer/let_binding.h		diff \| blob \| history
src/printer/printer.cpp		diff \| blob \| history
src/printer/printer.h		diff \| blob \| history
src/printer/smt2/smt2_printer.cpp		diff \| blob \| history
src/printer/smt2/smt2_printer.h		diff \| blob \| history
src/printer/tptp/tptp_printer.cpp		diff \| blob \| history
src/printer/tptp/tptp_printer.h		diff \| blob \| history
src/proof/alethe/alethe_node_converter.cpp		diff \| blob \| history
src/proof/alethe/alethe_node_converter.h		diff \| blob \| history
src/proof/alethe/alethe_nosubtype_node_converter.cpp		diff \| blob \| history
src/proof/alethe/alethe_nosubtype_node_converter.h		diff \| blob \| history
src/proof/alethe/alethe_post_processor.cpp		diff \| blob \| history
src/proof/alethe/alethe_post_processor.h		diff \| blob \| history
src/proof/alethe/alethe_printer.cpp		diff \| blob \| history
src/proof/alethe/alethe_printer.h		diff \| blob \| history
src/proof/alethe/alethe_proof_rule.cpp		diff \| blob \| history
src/proof/alethe/alethe_proof_rule.h		diff \| blob \| history
src/proof/annotation_proof_generator.cpp		diff \| blob \| history
src/proof/annotation_proof_generator.h		diff \| blob \| history
src/proof/assumption_proof_generator.cpp		diff \| blob \| history
src/proof/assumption_proof_generator.h		diff \| blob \| history
src/proof/buffered_proof_generator.cpp		diff \| blob \| history
src/proof/buffered_proof_generator.h		diff \| blob \| history
src/proof/clause_id.h		diff \| blob \| history
src/proof/conv_proof_generator.cpp		diff \| blob \| history
src/proof/conv_proof_generator.h		diff \| blob \| history
src/proof/conv_seq_proof_generator.cpp		diff \| blob \| history
src/proof/conv_seq_proof_generator.h		diff \| blob \| history
src/proof/dot/dot_printer.cpp		diff \| blob \| history
src/proof/dot/dot_printer.h		diff \| blob \| history
src/proof/eager_proof_generator.cpp		diff \| blob \| history
src/proof/eager_proof_generator.h		diff \| blob \| history
src/proof/lazy_proof.cpp		diff \| blob \| history
src/proof/lazy_proof.h		diff \| blob \| history
src/proof/lazy_proof_chain.cpp		diff \| blob \| history
src/proof/lazy_proof_chain.h		diff \| blob \| history
src/proof/lazy_tree_proof_generator.cpp		diff \| blob \| history
src/proof/lazy_tree_proof_generator.h		diff \| blob \| history
src/proof/lfsc/lfsc_list_sc_node_converter.cpp		diff \| blob \| history
src/proof/lfsc/lfsc_list_sc_node_converter.h		diff \| blob \| history
src/proof/lfsc/lfsc_node_converter.cpp		diff \| blob \| history
src/proof/lfsc/lfsc_node_converter.h		diff \| blob \| history
src/proof/lfsc/lfsc_post_processor.cpp		diff \| blob \| history
src/proof/lfsc/lfsc_post_processor.h		diff \| blob \| history
src/proof/lfsc/lfsc_print_channel.cpp		diff \| blob \| history
src/proof/lfsc/lfsc_print_channel.h		diff \| blob \| history
src/proof/lfsc/lfsc_printer.cpp		diff \| blob \| history
src/proof/lfsc/lfsc_printer.h		diff \| blob \| history
src/proof/lfsc/lfsc_util.cpp		diff \| blob \| history
src/proof/lfsc/lfsc_util.h		diff \| blob \| history
src/proof/method_id.cpp		diff \| blob \| history
src/proof/method_id.h		diff \| blob \| history
src/proof/print_expr.cpp		diff \| blob \| history
src/proof/print_expr.h		diff \| blob \| history
src/proof/proof.cpp		diff \| blob \| history
src/proof/proof.h		diff \| blob \| history
src/proof/proof_checker.cpp		diff \| blob \| history
src/proof/proof_checker.h		diff \| blob \| history
src/proof/proof_ensure_closed.cpp		diff \| blob \| history
src/proof/proof_ensure_closed.h		diff \| blob \| history
src/proof/proof_generator.cpp		diff \| blob \| history
src/proof/proof_generator.h		diff \| blob \| history
src/proof/proof_letify.cpp		diff \| blob \| history
src/proof/proof_letify.h		diff \| blob \| history
src/proof/proof_node.cpp		diff \| blob \| history
src/proof/proof_node.h		diff \| blob \| history
src/proof/proof_node_algorithm.cpp		diff \| blob \| history
src/proof/proof_node_algorithm.h		diff \| blob \| history
src/proof/proof_node_manager.cpp		diff \| blob \| history
src/proof/proof_node_manager.h		diff \| blob \| history
src/proof/proof_node_to_sexpr.cpp		diff \| blob \| history
src/proof/proof_node_to_sexpr.h		diff \| blob \| history
src/proof/proof_node_updater.cpp		diff \| blob \| history
src/proof/proof_node_updater.h		diff \| blob \| history
src/proof/proof_rule.cpp		diff \| blob \| history
src/proof/proof_rule.h		diff \| blob \| history
src/proof/proof_set.h		diff \| blob \| history
src/proof/proof_step_buffer.cpp		diff \| blob \| history
src/proof/proof_step_buffer.h		diff \| blob \| history
src/proof/theory_proof_step_buffer.cpp		diff \| blob \| history
src/proof/theory_proof_step_buffer.h		diff \| blob \| history
src/proof/trust_node.cpp		diff \| blob \| history
src/proof/trust_node.h		diff \| blob \| history
src/proof/unsat_core.cpp		diff \| blob \| history
src/proof/unsat_core.h		diff \| blob \| history
src/prop/cadical.cpp		diff \| blob \| history
src/prop/cadical.h		diff \| blob \| history
src/prop/cnf_stream.cpp		diff \| blob \| history
src/prop/cnf_stream.h		diff \| blob \| history
src/prop/cryptominisat.cpp		diff \| blob \| history
src/prop/cryptominisat.h		diff \| blob \| history
src/prop/kissat.cpp		diff \| blob \| history
src/prop/kissat.h		diff \| blob \| history
src/prop/minisat/minisat.cpp		diff \| blob \| history
src/prop/minisat/minisat.h		diff \| blob \| history
src/prop/opt_clauses_manager.cpp		diff \| blob \| history
src/prop/opt_clauses_manager.h		diff \| blob \| history
src/prop/proof_cnf_stream.cpp		diff \| blob \| history
src/prop/proof_cnf_stream.h		diff \| blob \| history
src/prop/proof_post_processor.cpp		diff \| blob \| history
src/prop/proof_post_processor.h		diff \| blob \| history
src/prop/prop_engine.cpp		diff \| blob \| history
src/prop/prop_engine.h		diff \| blob \| history
src/prop/prop_proof_manager.cpp		diff \| blob \| history
src/prop/prop_proof_manager.h		diff \| blob \| history
src/prop/registrar.h		diff \| blob \| history
src/prop/sat_proof_manager.cpp		diff \| blob \| history
src/prop/sat_proof_manager.h		diff \| blob \| history
src/prop/sat_solver.h		diff \| blob \| history
src/prop/sat_solver_factory.cpp		diff \| blob \| history
src/prop/sat_solver_factory.h		diff \| blob \| history
src/prop/sat_solver_types.cpp		diff \| blob \| history
src/prop/sat_solver_types.h		diff \| blob \| history
src/prop/skolem_def_manager.cpp		diff \| blob \| history
src/prop/skolem_def_manager.h		diff \| blob \| history
src/prop/theory_proxy.cpp		diff \| blob \| history
src/prop/theory_proxy.h		diff \| blob \| history
src/prop/zero_level_learner.cpp		diff \| blob \| history
src/prop/zero_level_learner.h		diff \| blob \| history
src/smt/abduction_solver.cpp		diff \| blob \| history
src/smt/abduction_solver.h		diff \| blob \| history
src/smt/abstract_values.cpp		diff \| blob \| history
src/smt/abstract_values.h		diff \| blob \| history
src/smt/assertions.cpp		diff \| blob \| history
src/smt/assertions.h		diff \| blob \| history
src/smt/check_models.cpp		diff \| blob \| history
src/smt/check_models.h		diff \| blob \| history
src/smt/command.cpp		diff \| blob \| history
src/smt/command.h		diff \| blob \| history
src/smt/difficulty_post_processor.cpp		diff \| blob \| history
src/smt/difficulty_post_processor.h		diff \| blob \| history
src/smt/env.cpp		diff \| blob \| history
src/smt/env.h		diff \| blob \| history
src/smt/env_obj.cpp		diff \| blob \| history
src/smt/env_obj.h		diff \| blob \| history
src/smt/expand_definitions.cpp		diff \| blob \| history
src/smt/expand_definitions.h		diff \| blob \| history
src/smt/interpolation_solver.cpp		diff \| blob \| history
src/smt/interpolation_solver.h		diff \| blob \| history
src/smt/listeners.cpp		diff \| blob \| history
src/smt/listeners.h		diff \| blob \| history
src/smt/logic_exception.h		diff \| blob \| history
src/smt/model.cpp		diff \| blob \| history
src/smt/model.h		diff \| blob \| history
src/smt/model_blocker.cpp		diff \| blob \| history
src/smt/model_blocker.h		diff \| blob \| history
src/smt/model_core_builder.cpp		diff \| blob \| history
src/smt/model_core_builder.h		diff \| blob \| history
src/smt/optimization_solver.cpp		diff \| blob \| history
src/smt/optimization_solver.h		diff \| blob \| history
src/smt/preprocess_proof_generator.cpp		diff \| blob \| history
src/smt/preprocess_proof_generator.h		diff \| blob \| history
src/smt/preprocessor.cpp		diff \| blob \| history
src/smt/preprocessor.h		diff \| blob \| history
src/smt/print_benchmark.cpp		diff \| blob \| history
src/smt/print_benchmark.h		diff \| blob \| history
src/smt/process_assertions.cpp		diff \| blob \| history
src/smt/process_assertions.h		diff \| blob \| history
src/smt/proof_final_callback.cpp		diff \| blob \| history
src/smt/proof_final_callback.h		diff \| blob \| history
src/smt/proof_manager.cpp		diff \| blob \| history
src/smt/proof_manager.h		diff \| blob \| history
src/smt/proof_post_processor.cpp		diff \| blob \| history
src/smt/proof_post_processor.h		diff \| blob \| history
src/smt/quant_elim_solver.cpp		diff \| blob \| history
src/smt/quant_elim_solver.h		diff \| blob \| history
src/smt/set_defaults.cpp		diff \| blob \| history
src/smt/set_defaults.h		diff \| blob \| history
src/smt/smt_mode.cpp		diff \| blob \| history
src/smt/smt_mode.h		diff \| blob \| history
src/smt/smt_solver.cpp		diff \| blob \| history
src/smt/smt_solver.h		diff \| blob \| history
src/smt/smt_statistics_registry.cpp		diff \| blob \| history
src/smt/smt_statistics_registry.h		diff \| blob \| history
src/smt/solver_engine.cpp		diff \| blob \| history
src/smt/solver_engine.h		diff \| blob \| history
src/smt/solver_engine_scope.cpp		diff \| blob \| history
src/smt/solver_engine_scope.h		diff \| blob \| history
src/smt/solver_engine_state.cpp		diff \| blob \| history
src/smt/solver_engine_state.h		diff \| blob \| history
src/smt/solver_engine_stats.cpp		diff \| blob \| history
src/smt/solver_engine_stats.h		diff \| blob \| history
src/smt/sygus_solver.cpp		diff \| blob \| history
src/smt/sygus_solver.h		diff \| blob \| history
src/smt/term_formula_removal.cpp		diff \| blob \| history
src/smt/term_formula_removal.h		diff \| blob \| history
src/smt/unsat_core_manager.cpp		diff \| blob \| history
src/smt/unsat_core_manager.h		diff \| blob \| history
src/smt/witness_form.cpp		diff \| blob \| history
src/smt/witness_form.h		diff \| blob \| history
src/smt_util/boolean_simplification.cpp		diff \| blob \| history
src/smt_util/boolean_simplification.h		diff \| blob \| history
src/theory/CMakeLists.txt		diff \| blob \| history
src/theory/arith/approx_simplex.cpp		diff \| blob \| history
src/theory/arith/approx_simplex.h		diff \| blob \| history
src/theory/arith/arith_evaluator.cpp		diff \| blob \| history
src/theory/arith/arith_evaluator.h		diff \| blob \| history
src/theory/arith/arith_ite_utils.cpp		diff \| blob \| history
src/theory/arith/arith_ite_utils.h		diff \| blob \| history
src/theory/arith/arith_msum.cpp		diff \| blob \| history
src/theory/arith/arith_msum.h		diff \| blob \| history
src/theory/arith/arith_poly_norm.cpp		diff \| blob \| history
src/theory/arith/arith_poly_norm.h		diff \| blob \| history
src/theory/arith/arith_preprocess.cpp		diff \| blob \| history
src/theory/arith/arith_preprocess.h		diff \| blob \| history
src/theory/arith/arith_rewriter.cpp		diff \| blob \| history
src/theory/arith/arith_rewriter.h		diff \| blob \| history
src/theory/arith/arith_state.cpp		diff \| blob \| history
src/theory/arith/arith_state.h		diff \| blob \| history
src/theory/arith/arith_static_learner.cpp		diff \| blob \| history
src/theory/arith/arith_static_learner.h		diff \| blob \| history
src/theory/arith/arith_utilities.cpp		diff \| blob \| history
src/theory/arith/arith_utilities.h		diff \| blob \| history
src/theory/arith/arithvar.cpp		diff \| blob \| history
src/theory/arith/arithvar.h		diff \| blob \| history
src/theory/arith/arithvar_node_map.h		diff \| blob \| history
src/theory/arith/attempt_solution_simplex.cpp		diff \| blob \| history
src/theory/arith/attempt_solution_simplex.h		diff \| blob \| history
src/theory/arith/bound_counts.h		diff \| blob \| history
src/theory/arith/bound_inference.cpp		diff \| blob \| history
src/theory/arith/bound_inference.h		diff \| blob \| history
src/theory/arith/branch_and_bound.cpp		diff \| blob \| history
src/theory/arith/branch_and_bound.h		diff \| blob \| history
src/theory/arith/callbacks.cpp		diff \| blob \| history
src/theory/arith/callbacks.h		diff \| blob \| history
src/theory/arith/congruence_manager.cpp		diff \| blob \| history
src/theory/arith/congruence_manager.h		diff \| blob \| history
src/theory/arith/constraint.cpp		diff \| blob \| history
src/theory/arith/constraint.h		diff \| blob \| history
src/theory/arith/constraint_forward.h		diff \| blob \| history
src/theory/arith/cut_log.cpp		diff \| blob \| history
src/theory/arith/cut_log.h		diff \| blob \| history
src/theory/arith/delta_rational.cpp		diff \| blob \| history
src/theory/arith/delta_rational.h		diff \| blob \| history
src/theory/arith/dio_solver.cpp		diff \| blob \| history
src/theory/arith/dio_solver.h		diff \| blob \| history
src/theory/arith/dual_simplex.cpp		diff \| blob \| history
src/theory/arith/dual_simplex.h		diff \| blob \| history
src/theory/arith/equality_solver.cpp		diff \| blob \| history
src/theory/arith/equality_solver.h		diff \| blob \| history
src/theory/arith/error_set.cpp		diff \| blob \| history
src/theory/arith/error_set.h		diff \| blob \| history
src/theory/arith/fc_simplex.cpp		diff \| blob \| history
src/theory/arith/fc_simplex.h		diff \| blob \| history
src/theory/arith/infer_bounds.cpp		diff \| blob \| history
src/theory/arith/infer_bounds.h		diff \| blob \| history
src/theory/arith/inference_manager.cpp		diff \| blob \| history
src/theory/arith/inference_manager.h		diff \| blob \| history
src/theory/arith/linear_equality.cpp		diff \| blob \| history
src/theory/arith/linear_equality.h		diff \| blob \| history
src/theory/arith/matrix.cpp		diff \| blob \| history
src/theory/arith/matrix.h		diff \| blob \| history
src/theory/arith/nl/coverings/cdcac.cpp		diff \| blob \| history
src/theory/arith/nl/coverings/cdcac.h		diff \| blob \| history
src/theory/arith/nl/coverings/cdcac_utils.cpp		diff \| blob \| history
src/theory/arith/nl/coverings/cdcac_utils.h		diff \| blob \| history
src/theory/arith/nl/coverings/cocoa_converter.cpp		diff \| blob \| history
src/theory/arith/nl/coverings/cocoa_converter.h		diff \| blob \| history
src/theory/arith/nl/coverings/constraints.cpp		diff \| blob \| history
src/theory/arith/nl/coverings/constraints.h		diff \| blob \| history
src/theory/arith/nl/coverings/lazard_evaluation.cpp		diff \| blob \| history
src/theory/arith/nl/coverings/lazard_evaluation.h		diff \| blob \| history
src/theory/arith/nl/coverings/projections.cpp		diff \| blob \| history
src/theory/arith/nl/coverings/projections.h		diff \| blob \| history
src/theory/arith/nl/coverings/proof_checker.cpp		diff \| blob \| history
src/theory/arith/nl/coverings/proof_checker.h		diff \| blob \| history
src/theory/arith/nl/coverings/proof_generator.cpp		diff \| blob \| history
src/theory/arith/nl/coverings/proof_generator.h		diff \| blob \| history
src/theory/arith/nl/coverings/variable_ordering.cpp		diff \| blob \| history
src/theory/arith/nl/coverings/variable_ordering.h		diff \| blob \| history
src/theory/arith/nl/coverings_solver.cpp		diff \| blob \| history
src/theory/arith/nl/coverings_solver.h		diff \| blob \| history
src/theory/arith/nl/equality_substitution.cpp		diff \| blob \| history
src/theory/arith/nl/equality_substitution.h		diff \| blob \| history
src/theory/arith/nl/ext/constraint.cpp		diff \| blob \| history
src/theory/arith/nl/ext/constraint.h		diff \| blob \| history
src/theory/arith/nl/ext/ext_state.cpp		diff \| blob \| history
src/theory/arith/nl/ext/ext_state.h		diff \| blob \| history
src/theory/arith/nl/ext/factoring_check.cpp		diff \| blob \| history
src/theory/arith/nl/ext/factoring_check.h		diff \| blob \| history
src/theory/arith/nl/ext/monomial.cpp		diff \| blob \| history
src/theory/arith/nl/ext/monomial.h		diff \| blob \| history
src/theory/arith/nl/ext/monomial_bounds_check.cpp		diff \| blob \| history
src/theory/arith/nl/ext/monomial_bounds_check.h		diff \| blob \| history
src/theory/arith/nl/ext/monomial_check.cpp		diff \| blob \| history
src/theory/arith/nl/ext/monomial_check.h		diff \| blob \| history
src/theory/arith/nl/ext/proof_checker.cpp		diff \| blob \| history
src/theory/arith/nl/ext/proof_checker.h		diff \| blob \| history
src/theory/arith/nl/ext/split_zero_check.cpp		diff \| blob \| history
src/theory/arith/nl/ext/split_zero_check.h		diff \| blob \| history
src/theory/arith/nl/ext/tangent_plane_check.cpp		diff \| blob \| history
src/theory/arith/nl/ext/tangent_plane_check.h		diff \| blob \| history
src/theory/arith/nl/ext_theory_callback.cpp		diff \| blob \| history
src/theory/arith/nl/ext_theory_callback.h		diff \| blob \| history
src/theory/arith/nl/iand_solver.cpp		diff \| blob \| history
src/theory/arith/nl/iand_solver.h		diff \| blob \| history
src/theory/arith/nl/iand_utils.cpp		diff \| blob \| history
src/theory/arith/nl/iand_utils.h		diff \| blob \| history
src/theory/arith/nl/icp/candidate.cpp		diff \| blob \| history
src/theory/arith/nl/icp/candidate.h		diff \| blob \| history
src/theory/arith/nl/icp/contraction_origins.cpp		diff \| blob \| history
src/theory/arith/nl/icp/contraction_origins.h		diff \| blob \| history
src/theory/arith/nl/icp/icp_solver.cpp		diff \| blob \| history
src/theory/arith/nl/icp/icp_solver.h		diff \| blob \| history
src/theory/arith/nl/icp/intersection.cpp		diff \| blob \| history
src/theory/arith/nl/icp/intersection.h		diff \| blob \| history
src/theory/arith/nl/icp/interval.h		diff \| blob \| history
src/theory/arith/nl/nl_lemma_utils.cpp		diff \| blob \| history
src/theory/arith/nl/nl_lemma_utils.h		diff \| blob \| history
src/theory/arith/nl/nl_model.cpp		diff \| blob \| history
src/theory/arith/nl/nl_model.h		diff \| blob \| history
src/theory/arith/nl/nonlinear_extension.cpp		diff \| blob \| history
src/theory/arith/nl/nonlinear_extension.h		diff \| blob \| history
src/theory/arith/nl/poly_conversion.cpp		diff \| blob \| history
src/theory/arith/nl/poly_conversion.h		diff \| blob \| history
src/theory/arith/nl/pow2_solver.cpp		diff \| blob \| history
src/theory/arith/nl/pow2_solver.h		diff \| blob \| history
src/theory/arith/nl/stats.cpp		diff \| blob \| history
src/theory/arith/nl/stats.h		diff \| blob \| history
src/theory/arith/nl/strategy.cpp		diff \| blob \| history
src/theory/arith/nl/strategy.h		diff \| blob \| history
src/theory/arith/nl/transcendental/exponential_solver.cpp		diff \| blob \| history
src/theory/arith/nl/transcendental/exponential_solver.h		diff \| blob \| history
src/theory/arith/nl/transcendental/proof_checker.cpp		diff \| blob \| history
src/theory/arith/nl/transcendental/proof_checker.h		diff \| blob \| history
src/theory/arith/nl/transcendental/sine_solver.cpp		diff \| blob \| history
src/theory/arith/nl/transcendental/sine_solver.h		diff \| blob \| history
src/theory/arith/nl/transcendental/taylor_generator.cpp		diff \| blob \| history
src/theory/arith/nl/transcendental/taylor_generator.h		diff \| blob \| history
src/theory/arith/nl/transcendental/transcendental_solver.cpp		diff \| blob \| history
src/theory/arith/nl/transcendental/transcendental_solver.h		diff \| blob \| history
src/theory/arith/nl/transcendental/transcendental_state.cpp		diff \| blob \| history
src/theory/arith/nl/transcendental/transcendental_state.h		diff \| blob \| history
src/theory/arith/normal_form.cpp		diff \| blob \| history
src/theory/arith/normal_form.h		diff \| blob \| history
src/theory/arith/operator_elim.cpp		diff \| blob \| history
src/theory/arith/operator_elim.h		diff \| blob \| history
src/theory/arith/partial_model.cpp		diff \| blob \| history
src/theory/arith/partial_model.h		diff \| blob \| history
src/theory/arith/pp_rewrite_eq.cpp		diff \| blob \| history
src/theory/arith/pp_rewrite_eq.h		diff \| blob \| history
src/theory/arith/proof_checker.cpp		diff \| blob \| history
src/theory/arith/proof_checker.h		diff \| blob \| history
src/theory/arith/rewriter/addition.cpp		diff \| blob \| history
src/theory/arith/rewriter/addition.h		diff \| blob \| history
src/theory/arith/rewriter/node_utils.cpp		diff \| blob \| history
src/theory/arith/rewriter/node_utils.h		diff \| blob \| history
src/theory/arith/rewriter/ordering.h		diff \| blob \| history
src/theory/arith/rewriter/rewrite_atom.cpp		diff \| blob \| history
src/theory/arith/rewriter/rewrite_atom.h		diff \| blob \| history
src/theory/arith/rewrites.cpp		diff \| blob \| history
src/theory/arith/rewrites.h		diff \| blob \| history
src/theory/arith/simplex.cpp		diff \| blob \| history
src/theory/arith/simplex.h		diff \| blob \| history
src/theory/arith/simplex_update.cpp		diff \| blob \| history
src/theory/arith/simplex_update.h		diff \| blob \| history
src/theory/arith/soi_simplex.cpp		diff \| blob \| history
src/theory/arith/soi_simplex.h		diff \| blob \| history
src/theory/arith/tableau.cpp		diff \| blob \| history
src/theory/arith/tableau.h		diff \| blob \| history
src/theory/arith/tableau_sizes.cpp		diff \| blob \| history
src/theory/arith/tableau_sizes.h		diff \| blob \| history
src/theory/arith/theory_arith.cpp		diff \| blob \| history
src/theory/arith/theory_arith.h		diff \| blob \| history
src/theory/arith/theory_arith_private.cpp		diff \| blob \| history
src/theory/arith/theory_arith_private.h		diff \| blob \| history
src/theory/arith/theory_arith_type_rules.cpp		diff \| blob \| history
src/theory/arith/theory_arith_type_rules.h		diff \| blob \| history
src/theory/arith/type_enumerator.h		diff \| blob \| history
src/theory/arrays/array_info.cpp		diff \| blob \| history
src/theory/arrays/array_info.h		diff \| blob \| history
src/theory/arrays/inference_manager.cpp		diff \| blob \| history
src/theory/arrays/inference_manager.h		diff \| blob \| history
src/theory/arrays/proof_checker.cpp		diff \| blob \| history
src/theory/arrays/proof_checker.h		diff \| blob \| history
src/theory/arrays/skolem_cache.cpp		diff \| blob \| history
src/theory/arrays/skolem_cache.h		diff \| blob \| history
src/theory/arrays/theory_arrays.cpp		diff \| blob \| history
src/theory/arrays/theory_arrays.h		diff \| blob \| history
src/theory/arrays/theory_arrays_rewriter.cpp		diff \| blob \| history
src/theory/arrays/theory_arrays_rewriter.h		diff \| blob \| history
src/theory/arrays/theory_arrays_type_rules.cpp		diff \| blob \| history
src/theory/arrays/theory_arrays_type_rules.h		diff \| blob \| history
src/theory/arrays/type_enumerator.cpp		diff \| blob \| history
src/theory/arrays/type_enumerator.h		diff \| blob \| history
src/theory/arrays/union_find.cpp		diff \| blob \| history
src/theory/arrays/union_find.h		diff \| blob \| history
src/theory/assertion.cpp		diff \| blob \| history
src/theory/assertion.h		diff \| blob \| history
src/theory/atom_requests.cpp		diff \| blob \| history
src/theory/atom_requests.h		diff \| blob \| history
src/theory/bags/bag_make_op.cpp		diff \| blob \| history
src/theory/bags/bag_make_op.h		diff \| blob \| history
src/theory/bags/bag_reduction.cpp		diff \| blob \| history
src/theory/bags/bag_reduction.h		diff \| blob \| history
src/theory/bags/bag_solver.cpp		diff \| blob \| history
src/theory/bags/bag_solver.h		diff \| blob \| history
src/theory/bags/bags_rewriter.cpp		diff \| blob \| history
src/theory/bags/bags_rewriter.h		diff \| blob \| history
src/theory/bags/bags_statistics.cpp		diff \| blob \| history
src/theory/bags/bags_statistics.h		diff \| blob \| history
src/theory/bags/bags_utils.cpp		diff \| blob \| history
src/theory/bags/bags_utils.h		diff \| blob \| history
src/theory/bags/card_solver.cpp		diff \| blob \| history
src/theory/bags/card_solver.h		diff \| blob \| history
src/theory/bags/infer_info.cpp		diff \| blob \| history
src/theory/bags/infer_info.h		diff \| blob \| history
src/theory/bags/inference_generator.cpp		diff \| blob \| history
src/theory/bags/inference_generator.h		diff \| blob \| history
src/theory/bags/inference_manager.cpp		diff \| blob \| history
src/theory/bags/inference_manager.h		diff \| blob \| history
src/theory/bags/rewrites.cpp		diff \| blob \| history
src/theory/bags/rewrites.h		diff \| blob \| history
src/theory/bags/solver_state.cpp		diff \| blob \| history
src/theory/bags/solver_state.h		diff \| blob \| history
src/theory/bags/strategy.cpp		diff \| blob \| history
src/theory/bags/strategy.h		diff \| blob \| history
src/theory/bags/term_registry.cpp		diff \| blob \| history
src/theory/bags/term_registry.h		diff \| blob \| history
src/theory/bags/theory_bags.cpp		diff \| blob \| history
src/theory/bags/theory_bags.h		diff \| blob \| history
src/theory/bags/theory_bags_type_enumerator.cpp		diff \| blob \| history
src/theory/bags/theory_bags_type_enumerator.h		diff \| blob \| history
src/theory/bags/theory_bags_type_rules.cpp		diff \| blob \| history
src/theory/bags/theory_bags_type_rules.h		diff \| blob \| history
src/theory/booleans/circuit_propagator.cpp		diff \| blob \| history
src/theory/booleans/circuit_propagator.h		diff \| blob \| history
src/theory/booleans/proof_checker.cpp		diff \| blob \| history
src/theory/booleans/proof_checker.h		diff \| blob \| history
src/theory/booleans/proof_circuit_propagator.cpp		diff \| blob \| history
src/theory/booleans/proof_circuit_propagator.h		diff \| blob \| history
src/theory/booleans/theory_bool.cpp		diff \| blob \| history
src/theory/booleans/theory_bool.h		diff \| blob \| history
src/theory/booleans/theory_bool_rewriter.cpp		diff \| blob \| history
src/theory/booleans/theory_bool_rewriter.h		diff \| blob \| history
src/theory/booleans/theory_bool_type_rules.cpp		diff \| blob \| history
src/theory/booleans/theory_bool_type_rules.h		diff \| blob \| history
src/theory/booleans/type_enumerator.h		diff \| blob \| history
src/theory/builtin/proof_checker.cpp		diff \| blob \| history
src/theory/builtin/proof_checker.h		diff \| blob \| history
src/theory/builtin/theory_builtin.cpp		diff \| blob \| history
src/theory/builtin/theory_builtin.h		diff \| blob \| history
src/theory/builtin/theory_builtin_rewriter.cpp		diff \| blob \| history
src/theory/builtin/theory_builtin_rewriter.h		diff \| blob \| history
src/theory/builtin/theory_builtin_type_rules.cpp		diff \| blob \| history
src/theory/builtin/theory_builtin_type_rules.h		diff \| blob \| history
src/theory/builtin/type_enumerator.cpp		diff \| blob \| history
src/theory/builtin/type_enumerator.h		diff \| blob \| history
src/theory/bv/bitblast/bitblast_proof_generator.cpp		diff \| blob \| history
src/theory/bv/bitblast/bitblast_proof_generator.h		diff \| blob \| history
src/theory/bv/bitblast/bitblast_strategies_template.h		diff \| blob \| history
src/theory/bv/bitblast/bitblast_utils.h		diff \| blob \| history
src/theory/bv/bitblast/bitblaster.h		diff \| blob \| history
src/theory/bv/bitblast/node_bitblaster.cpp		diff \| blob \| history
src/theory/bv/bitblast/node_bitblaster.h		diff \| blob \| history
src/theory/bv/bitblast/proof_bitblaster.cpp		diff \| blob \| history
src/theory/bv/bitblast/proof_bitblaster.h		diff \| blob \| history
src/theory/bv/bv_solver.h		diff \| blob \| history
src/theory/bv/bv_solver_bitblast.cpp		diff \| blob \| history
src/theory/bv/bv_solver_bitblast.h		diff \| blob \| history
src/theory/bv/bv_solver_bitblast_internal.cpp		diff \| blob \| history
src/theory/bv/bv_solver_bitblast_internal.h		diff \| blob \| history
src/theory/bv/int_blaster.cpp		diff \| blob \| history
src/theory/bv/int_blaster.h		diff \| blob \| history
src/theory/bv/proof_checker.cpp		diff \| blob \| history
src/theory/bv/proof_checker.h		diff \| blob \| history
src/theory/bv/theory_bv.cpp		diff \| blob \| history
src/theory/bv/theory_bv.h		diff \| blob \| history
src/theory/bv/theory_bv_rewrite_rules.h		diff \| blob \| history
src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h		diff \| blob \| history
src/theory/bv/theory_bv_rewrite_rules_core.h		diff \| blob \| history
src/theory/bv/theory_bv_rewrite_rules_normalization.h		diff \| blob \| history
src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h		diff \| blob \| history
src/theory/bv/theory_bv_rewrite_rules_simplification.h		diff \| blob \| history
src/theory/bv/theory_bv_rewriter.cpp		diff \| blob \| history
src/theory/bv/theory_bv_rewriter.h		diff \| blob \| history
src/theory/bv/theory_bv_type_rules.cpp		diff \| blob \| history
src/theory/bv/theory_bv_type_rules.h		diff \| blob \| history
src/theory/bv/theory_bv_utils.cpp		diff \| blob \| history
src/theory/bv/theory_bv_utils.h		diff \| blob \| history
src/theory/bv/type_enumerator.h		diff \| blob \| history
src/theory/care_graph.h		diff \| blob \| history
src/theory/care_pair_argument_callback.cpp		diff \| blob \| history
src/theory/care_pair_argument_callback.h		diff \| blob \| history
src/theory/combination_care_graph.cpp		diff \| blob \| history
src/theory/combination_care_graph.h		diff \| blob \| history
src/theory/combination_engine.cpp		diff \| blob \| history
src/theory/combination_engine.h		diff \| blob \| history
src/theory/datatypes/datatypes_rewriter.cpp		diff \| blob \| history
src/theory/datatypes/datatypes_rewriter.h		diff \| blob \| history
src/theory/datatypes/infer_proof_cons.cpp		diff \| blob \| history
src/theory/datatypes/infer_proof_cons.h		diff \| blob \| history
src/theory/datatypes/inference.cpp		diff \| blob \| history
src/theory/datatypes/inference.h		diff \| blob \| history
src/theory/datatypes/inference_manager.cpp		diff \| blob \| history
src/theory/datatypes/inference_manager.h		diff \| blob \| history
src/theory/datatypes/proof_checker.cpp		diff \| blob \| history
src/theory/datatypes/proof_checker.h		diff \| blob \| history
src/theory/datatypes/sygus_datatype_utils.cpp		diff \| blob \| history
src/theory/datatypes/sygus_datatype_utils.h		diff \| blob \| history
src/theory/datatypes/sygus_extension.cpp		diff \| blob \| history
src/theory/datatypes/sygus_extension.h		diff \| blob \| history
src/theory/datatypes/sygus_simple_sym.cpp		diff \| blob \| history
src/theory/datatypes/sygus_simple_sym.h		diff \| blob \| history
src/theory/datatypes/theory_datatypes.cpp		diff \| blob \| history
src/theory/datatypes/theory_datatypes.h		diff \| blob \| history
src/theory/datatypes/theory_datatypes_type_rules.cpp		diff \| blob \| history
src/theory/datatypes/theory_datatypes_type_rules.h		diff \| blob \| history
src/theory/datatypes/theory_datatypes_utils.cpp		diff \| blob \| history
src/theory/datatypes/theory_datatypes_utils.h		diff \| blob \| history
src/theory/datatypes/tuple_project_op.cpp		diff \| blob \| history
src/theory/datatypes/tuple_project_op.h		diff \| blob \| history
src/theory/datatypes/tuple_utils.cpp		diff \| blob \| history
src/theory/datatypes/tuple_utils.h		diff \| blob \| history
src/theory/datatypes/type_enumerator.cpp		diff \| blob \| history
src/theory/datatypes/type_enumerator.h		diff \| blob \| history
src/theory/decision_manager.cpp		diff \| blob \| history
src/theory/decision_manager.h		diff \| blob \| history
src/theory/decision_strategy.cpp		diff \| blob \| history
src/theory/decision_strategy.h		diff \| blob \| history
src/theory/difficulty_manager.cpp		diff \| blob \| history
src/theory/difficulty_manager.h		diff \| blob \| history
src/theory/ee_manager.cpp		diff \| blob \| history
src/theory/ee_manager.h		diff \| blob \| history
src/theory/ee_manager_central.cpp		diff \| blob \| history
src/theory/ee_manager_central.h		diff \| blob \| history
src/theory/ee_manager_distributed.cpp		diff \| blob \| history
src/theory/ee_manager_distributed.h		diff \| blob \| history
src/theory/ee_setup_info.h		diff \| blob \| history
src/theory/engine_output_channel.cpp		diff \| blob \| history
src/theory/engine_output_channel.h		diff \| blob \| history
src/theory/evaluator.cpp		diff \| blob \| history
src/theory/evaluator.h		diff \| blob \| history
src/theory/ext_theory.cpp		diff \| blob \| history
src/theory/ext_theory.h		diff \| blob \| history
src/theory/fp/fp_expand_defs.cpp		diff \| blob \| history
src/theory/fp/fp_expand_defs.h		diff \| blob \| history
src/theory/fp/fp_word_blaster.cpp		diff \| blob \| history
src/theory/fp/fp_word_blaster.h		diff \| blob \| history
src/theory/fp/theory_fp.cpp		diff \| blob \| history
src/theory/fp/theory_fp.h		diff \| blob \| history
src/theory/fp/theory_fp_rewriter.cpp		diff \| blob \| history
src/theory/fp/theory_fp_rewriter.h		diff \| blob \| history
src/theory/fp/theory_fp_type_rules.cpp		diff \| blob \| history
src/theory/fp/theory_fp_type_rules.h		diff \| blob \| history
src/theory/fp/type_enumerator.h		diff \| blob \| history
src/theory/incomplete_id.cpp		diff \| blob \| history
src/theory/incomplete_id.h		diff \| blob \| history
src/theory/inference_id.cpp		diff \| blob \| history
src/theory/inference_id.h		diff \| blob \| history
src/theory/inference_id_proof_annotator.cpp		diff \| blob \| history
src/theory/inference_id_proof_annotator.h		diff \| blob \| history
src/theory/inference_manager_buffered.cpp		diff \| blob \| history
src/theory/inference_manager_buffered.h		diff \| blob \| history
src/theory/interrupted.h		diff \| blob \| history
src/theory/logic_info.cpp		diff \| blob \| history
src/theory/logic_info.h		diff \| blob \| history
src/theory/mkrewriter		diff \| blob \| history
src/theory/mktheorytraits		diff \| blob \| history
src/theory/model_manager.cpp		diff \| blob \| history
src/theory/model_manager.h		diff \| blob \| history
src/theory/model_manager_distributed.cpp		diff \| blob \| history
src/theory/model_manager_distributed.h		diff \| blob \| history
src/theory/output_channel.cpp		diff \| blob \| history
src/theory/output_channel.h		diff \| blob \| history
src/theory/quantifiers/alpha_equivalence.cpp		diff \| blob \| history
src/theory/quantifiers/alpha_equivalence.h		diff \| blob \| history
src/theory/quantifiers/bv_inverter.cpp		diff \| blob \| history
src/theory/quantifiers/bv_inverter.h		diff \| blob \| history
src/theory/quantifiers/bv_inverter_utils.cpp		diff \| blob \| history
src/theory/quantifiers/bv_inverter_utils.h		diff \| blob \| history
src/theory/quantifiers/candidate_rewrite_database.cpp		diff \| blob \| history
src/theory/quantifiers/candidate_rewrite_database.h		diff \| blob \| history
src/theory/quantifiers/candidate_rewrite_filter.cpp		diff \| blob \| history
src/theory/quantifiers/candidate_rewrite_filter.h		diff \| blob \| history
src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp		diff \| blob \| history
src/theory/quantifiers/cegqi/ceg_arith_instantiator.h		diff \| blob \| history
src/theory/quantifiers/cegqi/ceg_bv_instantiator.cpp		diff \| blob \| history
src/theory/quantifiers/cegqi/ceg_bv_instantiator.h		diff \| blob \| history
src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.cpp		diff \| blob \| history
src/theory/quantifiers/cegqi/ceg_bv_instantiator_utils.h		diff \| blob \| history
src/theory/quantifiers/cegqi/ceg_dt_instantiator.cpp		diff \| blob \| history
src/theory/quantifiers/cegqi/ceg_dt_instantiator.h		diff \| blob \| history
src/theory/quantifiers/cegqi/ceg_instantiator.cpp		diff \| blob \| history
src/theory/quantifiers/cegqi/ceg_instantiator.h		diff \| blob \| history
src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp		diff \| blob \| history
src/theory/quantifiers/cegqi/inst_strategy_cegqi.h		diff \| blob \| history
src/theory/quantifiers/cegqi/nested_qe.cpp		diff \| blob \| history
src/theory/quantifiers/cegqi/nested_qe.h		diff \| blob \| history
src/theory/quantifiers/cegqi/vts_term_cache.cpp		diff \| blob \| history
src/theory/quantifiers/cegqi/vts_term_cache.h		diff \| blob \| history
src/theory/quantifiers/conjecture_generator.cpp		diff \| blob \| history
src/theory/quantifiers/conjecture_generator.h		diff \| blob \| history
src/theory/quantifiers/dynamic_rewrite.cpp		diff \| blob \| history
src/theory/quantifiers/dynamic_rewrite.h		diff \| blob \| history
src/theory/quantifiers/ematching/candidate_generator.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/candidate_generator.h		diff \| blob \| history
src/theory/quantifiers/ematching/ho_trigger.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/ho_trigger.h		diff \| blob \| history
src/theory/quantifiers/ematching/im_generator.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/im_generator.h		diff \| blob \| history
src/theory/quantifiers/ematching/inst_match_generator.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/inst_match_generator.h		diff \| blob \| history
src/theory/quantifiers/ematching/inst_match_generator_multi.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/inst_match_generator_multi.h		diff \| blob \| history
src/theory/quantifiers/ematching/inst_match_generator_multi_linear.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/inst_match_generator_multi_linear.h		diff \| blob \| history
src/theory/quantifiers/ematching/inst_match_generator_simple.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/inst_match_generator_simple.h		diff \| blob \| history
src/theory/quantifiers/ematching/inst_strategy.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/inst_strategy.h		diff \| blob \| history
src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/inst_strategy_e_matching.h		diff \| blob \| history
src/theory/quantifiers/ematching/inst_strategy_e_matching_user.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/inst_strategy_e_matching_user.h		diff \| blob \| history
src/theory/quantifiers/ematching/instantiation_engine.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/instantiation_engine.h		diff \| blob \| history
src/theory/quantifiers/ematching/pattern_term_selector.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/pattern_term_selector.h		diff \| blob \| history
src/theory/quantifiers/ematching/relational_match_generator.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/relational_match_generator.h		diff \| blob \| history
src/theory/quantifiers/ematching/trigger.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/trigger.h		diff \| blob \| history
src/theory/quantifiers/ematching/trigger_database.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/trigger_database.h		diff \| blob \| history
src/theory/quantifiers/ematching/trigger_term_info.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/trigger_term_info.h		diff \| blob \| history
src/theory/quantifiers/ematching/trigger_trie.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/trigger_trie.h		diff \| blob \| history
src/theory/quantifiers/ematching/var_match_generator.cpp		diff \| blob \| history
src/theory/quantifiers/ematching/var_match_generator.h		diff \| blob \| history
src/theory/quantifiers/entailment_check.cpp		diff \| blob \| history
src/theory/quantifiers/entailment_check.h		diff \| blob \| history
src/theory/quantifiers/equality_query.cpp		diff \| blob \| history
src/theory/quantifiers/equality_query.h		diff \| blob \| history
src/theory/quantifiers/expr_miner.cpp		diff \| blob \| history
src/theory/quantifiers/expr_miner.h		diff \| blob \| history
src/theory/quantifiers/expr_miner_manager.cpp		diff \| blob \| history
src/theory/quantifiers/expr_miner_manager.h		diff \| blob \| history
src/theory/quantifiers/extended_rewrite.cpp		diff \| blob \| history
src/theory/quantifiers/extended_rewrite.h		diff \| blob \| history
src/theory/quantifiers/first_order_model.cpp		diff \| blob \| history
src/theory/quantifiers/first_order_model.h		diff \| blob \| history
src/theory/quantifiers/fmf/bounded_integers.cpp		diff \| blob \| history
src/theory/quantifiers/fmf/bounded_integers.h		diff \| blob \| history
src/theory/quantifiers/fmf/first_order_model_fmc.cpp		diff \| blob \| history
src/theory/quantifiers/fmf/first_order_model_fmc.h		diff \| blob \| history
src/theory/quantifiers/fmf/full_model_check.cpp		diff \| blob \| history
src/theory/quantifiers/fmf/full_model_check.h		diff \| blob \| history
src/theory/quantifiers/fmf/model_builder.cpp		diff \| blob \| history
src/theory/quantifiers/fmf/model_builder.h		diff \| blob \| history
src/theory/quantifiers/fmf/model_engine.cpp		diff \| blob \| history
src/theory/quantifiers/fmf/model_engine.h		diff \| blob \| history
src/theory/quantifiers/fun_def_evaluator.cpp		diff \| blob \| history
src/theory/quantifiers/fun_def_evaluator.h		diff \| blob \| history
src/theory/quantifiers/ho_term_database.cpp		diff \| blob \| history
src/theory/quantifiers/ho_term_database.h		diff \| blob \| history
src/theory/quantifiers/index_trie.cpp		diff \| blob \| history
src/theory/quantifiers/index_trie.h		diff \| blob \| history
src/theory/quantifiers/inst_match.cpp		diff \| blob \| history
src/theory/quantifiers/inst_match.h		diff \| blob \| history
src/theory/quantifiers/inst_match_trie.cpp		diff \| blob \| history
src/theory/quantifiers/inst_match_trie.h		diff \| blob \| history
src/theory/quantifiers/inst_strategy_enumerative.cpp		diff \| blob \| history
src/theory/quantifiers/inst_strategy_enumerative.h		diff \| blob \| history
src/theory/quantifiers/inst_strategy_pool.cpp		diff \| blob \| history
src/theory/quantifiers/inst_strategy_pool.h		diff \| blob \| history
src/theory/quantifiers/instantiate.cpp		diff \| blob \| history
src/theory/quantifiers/instantiate.h		diff \| blob \| history
src/theory/quantifiers/instantiation_list.cpp		diff \| blob \| history
src/theory/quantifiers/instantiation_list.h		diff \| blob \| history
src/theory/quantifiers/lazy_trie.cpp		diff \| blob \| history
src/theory/quantifiers/lazy_trie.h		diff \| blob \| history
src/theory/quantifiers/master_eq_notify.cpp		diff \| blob \| history
src/theory/quantifiers/master_eq_notify.h		diff \| blob \| history
src/theory/quantifiers/proof_checker.cpp		diff \| blob \| history
src/theory/quantifiers/proof_checker.h		diff \| blob \| history
src/theory/quantifiers/quant_bound_inference.cpp		diff \| blob \| history
src/theory/quantifiers/quant_bound_inference.h		diff \| blob \| history
src/theory/quantifiers/quant_conflict_find.cpp		diff \| blob \| history
src/theory/quantifiers/quant_conflict_find.h		diff \| blob \| history
src/theory/quantifiers/quant_module.cpp		diff \| blob \| history
src/theory/quantifiers/quant_module.h		diff \| blob \| history
src/theory/quantifiers/quant_relevance.cpp		diff \| blob \| history
src/theory/quantifiers/quant_relevance.h		diff \| blob \| history
src/theory/quantifiers/quant_rep_bound_ext.cpp		diff \| blob \| history
src/theory/quantifiers/quant_rep_bound_ext.h		diff \| blob \| history
src/theory/quantifiers/quant_split.cpp		diff \| blob \| history
src/theory/quantifiers/quant_split.h		diff \| blob \| history
src/theory/quantifiers/quant_util.cpp		diff \| blob \| history
src/theory/quantifiers/quant_util.h		diff \| blob \| history
src/theory/quantifiers/quantifiers_attributes.cpp		diff \| blob \| history
src/theory/quantifiers/quantifiers_attributes.h		diff \| blob \| history
src/theory/quantifiers/quantifiers_inference_manager.cpp		diff \| blob \| history
src/theory/quantifiers/quantifiers_inference_manager.h		diff \| blob \| history
src/theory/quantifiers/quantifiers_macros.cpp		diff \| blob \| history
src/theory/quantifiers/quantifiers_macros.h		diff \| blob \| history
src/theory/quantifiers/quantifiers_modules.cpp		diff \| blob \| history
src/theory/quantifiers/quantifiers_modules.h		diff \| blob \| history
src/theory/quantifiers/quantifiers_preprocess.cpp		diff \| blob \| history
src/theory/quantifiers/quantifiers_preprocess.h		diff \| blob \| history
src/theory/quantifiers/quantifiers_registry.cpp		diff \| blob \| history
src/theory/quantifiers/quantifiers_registry.h		diff \| blob \| history
src/theory/quantifiers/quantifiers_rewriter.cpp		diff \| blob \| history
src/theory/quantifiers/quantifiers_rewriter.h		diff \| blob \| history
src/theory/quantifiers/quantifiers_state.cpp		diff \| blob \| history
src/theory/quantifiers/quantifiers_state.h		diff \| blob \| history
src/theory/quantifiers/quantifiers_statistics.cpp		diff \| blob \| history
src/theory/quantifiers/quantifiers_statistics.h		diff \| blob \| history
src/theory/quantifiers/query_generator.cpp		diff \| blob \| history
src/theory/quantifiers/query_generator.h		diff \| blob \| history
src/theory/quantifiers/query_generator_sample_sat.cpp		diff \| blob \| history
src/theory/quantifiers/query_generator_sample_sat.h		diff \| blob \| history
src/theory/quantifiers/query_generator_unsat.cpp		diff \| blob \| history
src/theory/quantifiers/query_generator_unsat.h		diff \| blob \| history
src/theory/quantifiers/relevant_domain.cpp		diff \| blob \| history
src/theory/quantifiers/relevant_domain.h		diff \| blob \| history
src/theory/quantifiers/single_inv_partition.cpp		diff \| blob \| history
src/theory/quantifiers/single_inv_partition.h		diff \| blob \| history
src/theory/quantifiers/skolemize.cpp		diff \| blob \| history
src/theory/quantifiers/skolemize.h		diff \| blob \| history
src/theory/quantifiers/solution_filter.cpp		diff \| blob \| history
src/theory/quantifiers/solution_filter.h		diff \| blob \| history
src/theory/quantifiers/sygus/ce_guided_single_inv.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/ce_guided_single_inv.h		diff \| blob \| history
src/theory/quantifiers/sygus/cegis.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/cegis.h		diff \| blob \| history
src/theory/quantifiers/sygus/cegis_core_connective.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/cegis_core_connective.h		diff \| blob \| history
src/theory/quantifiers/sygus/cegis_unif.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/cegis_unif.h		diff \| blob \| history
src/theory/quantifiers/sygus/enum_stream_substitution.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/enum_stream_substitution.h		diff \| blob \| history
src/theory/quantifiers/sygus/enum_val_generator.h		diff \| blob \| history
src/theory/quantifiers/sygus/enum_value_manager.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/enum_value_manager.h		diff \| blob \| history
src/theory/quantifiers/sygus/example_eval_cache.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/example_eval_cache.h		diff \| blob \| history
src/theory/quantifiers/sygus/example_infer.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/example_infer.h		diff \| blob \| history
src/theory/quantifiers/sygus/example_min_eval.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/example_min_eval.h		diff \| blob \| history
src/theory/quantifiers/sygus/rcons_obligation.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/rcons_obligation.h		diff \| blob \| history
src/theory/quantifiers/sygus/rcons_type_info.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/rcons_type_info.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_abduct.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_abduct.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_enumerator.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_enumerator.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_enumerator_callback.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_enumerator_callback.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_eval_unfold.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_eval_unfold.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_explain.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_explain.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_grammar_cons.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_grammar_cons.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_grammar_norm.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_grammar_norm.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_grammar_red.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_grammar_red.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_interpol.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_interpol.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_invariance.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_invariance.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_module.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_module.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_pbe.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_pbe.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_process_conj.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_process_conj.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_qe_preproc.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_qe_preproc.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_random_enumerator.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_random_enumerator.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_reconstruct.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_reconstruct.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_repair_const.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_repair_const.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_stats.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_stats.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_unif.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_unif.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_unif_io.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_unif_io.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_unif_rl.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_unif_rl.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_unif_strat.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_unif_strat.h		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_utils.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/sygus_utils.h		diff \| blob \| history
src/theory/quantifiers/sygus/synth_conjecture.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/synth_conjecture.h		diff \| blob \| history
src/theory/quantifiers/sygus/synth_engine.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/synth_engine.h		diff \| blob \| history
src/theory/quantifiers/sygus/synth_verify.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/synth_verify.h		diff \| blob \| history
src/theory/quantifiers/sygus/template_infer.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/template_infer.h		diff \| blob \| history
src/theory/quantifiers/sygus/term_database_sygus.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/term_database_sygus.h		diff \| blob \| history
src/theory/quantifiers/sygus/transition_inference.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/transition_inference.h		diff \| blob \| history
src/theory/quantifiers/sygus/type_info.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/type_info.h		diff \| blob \| history
src/theory/quantifiers/sygus/type_node_id_trie.cpp		diff \| blob \| history
src/theory/quantifiers/sygus/type_node_id_trie.h		diff \| blob \| history
src/theory/quantifiers/sygus_inst.cpp		diff \| blob \| history
src/theory/quantifiers/sygus_inst.h		diff \| blob \| history
src/theory/quantifiers/sygus_sampler.cpp		diff \| blob \| history
src/theory/quantifiers/sygus_sampler.h		diff \| blob \| history
src/theory/quantifiers/term_database.cpp		diff \| blob \| history
src/theory/quantifiers/term_database.h		diff \| blob \| history
src/theory/quantifiers/term_enumeration.cpp		diff \| blob \| history
src/theory/quantifiers/term_enumeration.h		diff \| blob \| history
src/theory/quantifiers/term_pools.cpp		diff \| blob \| history
src/theory/quantifiers/term_pools.h		diff \| blob \| history
src/theory/quantifiers/term_registry.cpp		diff \| blob \| history
src/theory/quantifiers/term_registry.h		diff \| blob \| history
src/theory/quantifiers/term_tuple_enumerator.cpp		diff \| blob \| history
src/theory/quantifiers/term_tuple_enumerator.h		diff \| blob \| history
src/theory/quantifiers/term_util.cpp		diff \| blob \| history
src/theory/quantifiers/term_util.h		diff \| blob \| history
src/theory/quantifiers/theory_quantifiers.cpp		diff \| blob \| history
src/theory/quantifiers/theory_quantifiers.h		diff \| blob \| history
src/theory/quantifiers/theory_quantifiers_type_rules.cpp		diff \| blob \| history
src/theory/quantifiers/theory_quantifiers_type_rules.h		diff \| blob \| history
src/theory/quantifiers_engine.cpp		diff \| blob \| history
src/theory/quantifiers_engine.h		diff \| blob \| history
src/theory/relevance_manager.cpp		diff \| blob \| history
src/theory/relevance_manager.h		diff \| blob \| history
src/theory/rep_set.cpp		diff \| blob \| history
src/theory/rep_set.h		diff \| blob \| history
src/theory/rewriter.cpp		diff \| blob \| history
src/theory/rewriter.h		diff \| blob \| history
src/theory/rewriter_attributes.h		diff \| blob \| history
src/theory/rewriter_tables_template.h		diff \| blob \| history
src/theory/sep/theory_sep.cpp		diff \| blob \| history
src/theory/sep/theory_sep.h		diff \| blob \| history
src/theory/sep/theory_sep_rewriter.cpp		diff \| blob \| history
src/theory/sep/theory_sep_rewriter.h		diff \| blob \| history
src/theory/sep/theory_sep_type_rules.cpp		diff \| blob \| history
src/theory/sep/theory_sep_type_rules.h		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/inference_manager.h		diff \| blob \| history
src/theory/sets/normal_form.h		diff \| blob \| history
src/theory/sets/rels_utils.cpp		diff \| blob \| history
src/theory/sets/rels_utils.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/skolem_cache.cpp		diff \| blob \| history
src/theory/sets/skolem_cache.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/term_registry.h		diff \| blob \| history
src/theory/sets/theory_sets.cpp		diff \| blob \| history
src/theory/sets/theory_sets.h		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_rewriter.h		diff \| blob \| history
src/theory/sets/theory_sets_type_enumerator.cpp		diff \| blob \| history
src/theory/sets/theory_sets_type_enumerator.h		diff \| blob \| history
src/theory/sets/theory_sets_type_rules.cpp		diff \| blob \| history
src/theory/sets/theory_sets_type_rules.h		diff \| blob \| history
src/theory/shared_solver.cpp		diff \| blob \| history
src/theory/shared_solver.h		diff \| blob \| history
src/theory/shared_solver_distributed.cpp		diff \| blob \| history
src/theory/shared_solver_distributed.h		diff \| blob \| history
src/theory/shared_terms_database.cpp		diff \| blob \| history
src/theory/shared_terms_database.h		diff \| blob \| history
src/theory/skolem_lemma.cpp		diff \| blob \| history
src/theory/skolem_lemma.h		diff \| blob \| history
src/theory/smt_engine_subsolver.cpp		diff \| blob \| history
src/theory/smt_engine_subsolver.h		diff \| blob \| history
src/theory/sort_inference.cpp		diff \| blob \| history
src/theory/sort_inference.h		diff \| blob \| history
src/theory/strings/arith_entail.cpp		diff \| blob \| history
src/theory/strings/arith_entail.h		diff \| blob \| history
src/theory/strings/array_core_solver.cpp		diff \| blob \| history
src/theory/strings/array_core_solver.h		diff \| blob \| history
src/theory/strings/array_solver.cpp		diff \| blob \| history
src/theory/strings/array_solver.h		diff \| blob \| history
src/theory/strings/base_solver.cpp		diff \| blob \| history
src/theory/strings/base_solver.h		diff \| blob \| history
src/theory/strings/core_solver.cpp		diff \| blob \| history
src/theory/strings/core_solver.h		diff \| blob \| history
src/theory/strings/eager_solver.cpp		diff \| blob \| history
src/theory/strings/eager_solver.h		diff \| blob \| history
src/theory/strings/eqc_info.cpp		diff \| blob \| history
src/theory/strings/eqc_info.h		diff \| blob \| history
src/theory/strings/extf_solver.cpp		diff \| blob \| history
src/theory/strings/extf_solver.h		diff \| blob \| history
src/theory/strings/infer_info.cpp		diff \| blob \| history
src/theory/strings/infer_info.h		diff \| blob \| history
src/theory/strings/infer_proof_cons.cpp		diff \| blob \| history
src/theory/strings/infer_proof_cons.h		diff \| blob \| history
src/theory/strings/inference_manager.cpp		diff \| blob \| history
src/theory/strings/inference_manager.h		diff \| blob \| history
src/theory/strings/normal_form.cpp		diff \| blob \| history
src/theory/strings/normal_form.h		diff \| blob \| history
src/theory/strings/proof_checker.cpp		diff \| blob \| history
src/theory/strings/proof_checker.h		diff \| blob \| history
src/theory/strings/regexp_elim.cpp		diff \| blob \| history
src/theory/strings/regexp_elim.h		diff \| blob \| history
src/theory/strings/regexp_entail.cpp		diff \| blob \| history
src/theory/strings/regexp_entail.h		diff \| blob \| history
src/theory/strings/regexp_enumerator.cpp		diff \| blob \| history
src/theory/strings/regexp_enumerator.h		diff \| blob \| history
src/theory/strings/regexp_operation.cpp		diff \| blob \| history
src/theory/strings/regexp_operation.h		diff \| blob \| history
src/theory/strings/regexp_solver.cpp		diff \| blob \| history
src/theory/strings/regexp_solver.h		diff \| blob \| history
src/theory/strings/rewrites.cpp		diff \| blob \| history
src/theory/strings/rewrites.h		diff \| blob \| history
src/theory/strings/seq_unit_op.cpp		diff \| blob \| history
src/theory/strings/seq_unit_op.h		diff \| blob \| history
src/theory/strings/sequences_rewriter.cpp		diff \| blob \| history
src/theory/strings/sequences_rewriter.h		diff \| blob \| history
src/theory/strings/sequences_stats.cpp		diff \| blob \| history
src/theory/strings/sequences_stats.h		diff \| blob \| history
src/theory/strings/skolem_cache.cpp		diff \| blob \| history
src/theory/strings/skolem_cache.h		diff \| blob \| history
src/theory/strings/solver_state.cpp		diff \| blob \| history
src/theory/strings/solver_state.h		diff \| blob \| history
src/theory/strings/strategy.cpp		diff \| blob \| history
src/theory/strings/strategy.h		diff \| blob \| history
src/theory/strings/strings_entail.cpp		diff \| blob \| history
src/theory/strings/strings_entail.h		diff \| blob \| history
src/theory/strings/strings_fmf.cpp		diff \| blob \| history
src/theory/strings/strings_fmf.h		diff \| blob \| history
src/theory/strings/strings_rewriter.cpp		diff \| blob \| history
src/theory/strings/strings_rewriter.h		diff \| blob \| history
src/theory/strings/term_registry.cpp		diff \| blob \| history
src/theory/strings/term_registry.h		diff \| blob \| history
src/theory/strings/theory_strings.cpp		diff \| blob \| history
src/theory/strings/theory_strings.h		diff \| blob \| history
src/theory/strings/theory_strings_preprocess.cpp		diff \| blob \| history
src/theory/strings/theory_strings_preprocess.h		diff \| blob \| history
src/theory/strings/theory_strings_type_rules.cpp		diff \| blob \| history
src/theory/strings/theory_strings_type_rules.h		diff \| blob \| history
src/theory/strings/theory_strings_utils.cpp		diff \| blob \| history
src/theory/strings/theory_strings_utils.h		diff \| blob \| history
src/theory/strings/type_enumerator.cpp		diff \| blob \| history
src/theory/strings/type_enumerator.h		diff \| blob \| history
src/theory/strings/word.cpp		diff \| blob \| history
src/theory/strings/word.h		diff \| blob \| history
src/theory/subs_minimize.cpp		diff \| blob \| history
src/theory/subs_minimize.h		diff \| blob \| history
src/theory/substitutions.cpp		diff \| blob \| history
src/theory/substitutions.h		diff \| blob \| history
src/theory/term_registration_visitor.cpp		diff \| blob \| history
src/theory/term_registration_visitor.h		diff \| blob \| history
src/theory/theory.cpp		diff \| blob \| history
src/theory/theory.h		diff \| blob \| history
src/theory/theory_engine.cpp		diff \| blob \| history
src/theory/theory_engine.h		diff \| blob \| history
src/theory/theory_engine_proof_generator.cpp		diff \| blob \| history
src/theory/theory_engine_proof_generator.h		diff \| blob \| history
src/theory/theory_eq_notify.h		diff \| blob \| history
src/theory/theory_id.cpp		diff \| blob \| history
src/theory/theory_id.h		diff \| blob \| history
src/theory/theory_inference.cpp		diff \| blob \| history
src/theory/theory_inference.h		diff \| blob \| history
src/theory/theory_inference_manager.cpp		diff \| blob \| history
src/theory/theory_inference_manager.h		diff \| blob \| history
src/theory/theory_model.cpp		diff \| blob \| history
src/theory/theory_model.h		diff \| blob \| history
src/theory/theory_model_builder.cpp		diff \| blob \| history
src/theory/theory_model_builder.h		diff \| blob \| history
src/theory/theory_preprocessor.cpp		diff \| blob \| history
src/theory/theory_preprocessor.h		diff \| blob \| history
src/theory/theory_rewriter.cpp		diff \| blob \| history
src/theory/theory_rewriter.h		diff \| blob \| history
src/theory/theory_state.cpp		diff \| blob \| history
src/theory/theory_state.h		diff \| blob \| history
src/theory/theory_traits_template.h		diff \| blob \| history
src/theory/trust_substitutions.cpp		diff \| blob \| history
src/theory/trust_substitutions.h		diff \| blob \| history
src/theory/type_enumerator.h		diff \| blob \| history
src/theory/type_enumerator_template.cpp		diff \| blob \| history
src/theory/type_set.cpp		diff \| blob \| history
src/theory/type_set.h		diff \| blob \| history
src/theory/uf/cardinality_extension.cpp		diff \| blob \| history
src/theory/uf/cardinality_extension.h		diff \| blob \| history
src/theory/uf/eq_proof.cpp		diff \| blob \| history
src/theory/uf/eq_proof.h		diff \| blob \| history
src/theory/uf/equality_engine.cpp		diff \| blob \| history
src/theory/uf/equality_engine.h		diff \| blob \| history
src/theory/uf/equality_engine_iterator.cpp		diff \| blob \| history
src/theory/uf/equality_engine_iterator.h		diff \| blob \| history
src/theory/uf/equality_engine_notify.h		diff \| blob \| history
src/theory/uf/equality_engine_types.h		diff \| blob \| history
src/theory/uf/function_const.cpp		diff \| blob \| history
src/theory/uf/function_const.h		diff \| blob \| history
src/theory/uf/ho_extension.cpp		diff \| blob \| history
src/theory/uf/ho_extension.h		diff \| blob \| history
src/theory/uf/lambda_lift.cpp		diff \| blob \| history
src/theory/uf/lambda_lift.h		diff \| blob \| history
src/theory/uf/proof_checker.cpp		diff \| blob \| history
src/theory/uf/proof_checker.h		diff \| blob \| history
src/theory/uf/proof_equality_engine.cpp		diff \| blob \| history
src/theory/uf/proof_equality_engine.h		diff \| blob \| history
src/theory/uf/symmetry_breaker.cpp		diff \| blob \| history
src/theory/uf/symmetry_breaker.h		diff \| blob \| history
src/theory/uf/theory_uf.cpp		diff \| blob \| history
src/theory/uf/theory_uf.h		diff \| blob \| history
src/theory/uf/theory_uf_model.cpp		diff \| blob \| history
src/theory/uf/theory_uf_model.h		diff \| blob \| history
src/theory/uf/theory_uf_rewriter.cpp		diff \| blob \| history
src/theory/uf/theory_uf_rewriter.h		diff \| blob \| history
src/theory/uf/theory_uf_type_rules.cpp		diff \| blob \| history
src/theory/uf/theory_uf_type_rules.h		diff \| blob \| history
src/theory/uf/type_enumerator.cpp		diff \| blob \| history
src/theory/uf/type_enumerator.h		diff \| blob \| history
src/theory/valuation.cpp		diff \| blob \| history
src/theory/valuation.h		diff \| blob \| history
src/util/CMakeLists.txt		diff \| blob \| history
src/util/bin_heap.h		diff \| blob \| history
src/util/bitvector.cpp		diff \| blob \| history
src/util/bitvector.h		diff \| blob \| history
src/util/bool.h		diff \| blob \| history
src/util/cardinality.cpp		diff \| blob \| history
src/util/cardinality.h		diff \| blob \| history
src/util/cardinality_class.cpp		diff \| blob \| history
src/util/cardinality_class.h		diff \| blob \| history
src/util/dense_map.h		diff \| blob \| history
src/util/didyoumean.cpp		diff \| blob \| history
src/util/didyoumean.h		diff \| blob \| history
src/util/divisible.cpp		diff \| blob \| history
src/util/divisible.h		diff \| blob \| history
src/util/floatingpoint.cpp		diff \| blob \| history
src/util/floatingpoint.h		diff \| blob \| history
src/util/floatingpoint_literal_symfpu.cpp		diff \| blob \| history
src/util/floatingpoint_literal_symfpu.h		diff \| blob \| history
src/util/floatingpoint_literal_symfpu_traits.cpp		diff \| blob \| history
src/util/floatingpoint_literal_symfpu_traits.h		diff \| blob \| history
src/util/floatingpoint_size.cpp		diff \| blob \| history
src/util/floatingpoint_size.h		diff \| blob \| history
src/util/gmp_util.h		diff \| blob \| history
src/util/hash.h		diff \| blob \| history
src/util/iand.h		diff \| blob \| history
src/util/index.cpp		diff \| blob \| history
src/util/index.h		diff \| blob \| history
src/util/indexed_root_predicate.h		diff \| blob \| history
src/util/integer.h.in		diff \| blob \| history
src/util/integer_cln_imp.cpp		diff \| blob \| history
src/util/integer_cln_imp.h		diff \| blob \| history
src/util/integer_gmp_imp.cpp		diff \| blob \| history
src/util/integer_gmp_imp.h		diff \| blob \| history
src/util/ostream_util.cpp		diff \| blob \| history
src/util/ostream_util.h		diff \| blob \| history
src/util/poly_util.cpp		diff \| blob \| history
src/util/poly_util.h		diff \| blob \| history
src/util/random.cpp		diff \| blob \| history
src/util/random.h		diff \| blob \| history
src/util/rational.h.in		diff \| blob \| history
src/util/rational_cln_imp.cpp		diff \| blob \| history
src/util/rational_cln_imp.h		diff \| blob \| history
src/util/rational_gmp_imp.cpp		diff \| blob \| history
src/util/rational_gmp_imp.h		diff \| blob \| history
src/util/real_algebraic_number.h.in		diff \| blob \| history
src/util/real_algebraic_number_poly_imp.cpp		diff \| blob \| history
src/util/real_algebraic_number_poly_imp.h		diff \| blob \| history
src/util/regexp.cpp		diff \| blob \| history
src/util/regexp.h		diff \| blob \| history
src/util/resource_manager.cpp		diff \| blob \| history
src/util/resource_manager.h		diff \| blob \| history
src/util/result.cpp		diff \| blob \| history
src/util/result.h		diff \| blob \| history
src/util/roundingmode.cpp		diff \| blob \| history
src/util/roundingmode.h		diff \| blob \| history
src/util/safe_print.cpp		diff \| blob \| history
src/util/safe_print.h		diff \| blob \| history
src/util/sampler.cpp		diff \| blob \| history
src/util/sampler.h		diff \| blob \| history
src/util/sexpr.cpp		diff \| blob \| history
src/util/sexpr.h		diff \| blob \| history
src/util/smt2_quote_string.cpp		diff \| blob \| history
src/util/smt2_quote_string.h		diff \| blob \| history
src/util/statistics_public.cpp		diff \| blob \| history
src/util/statistics_public.h		diff \| blob \| history
src/util/statistics_registry.cpp		diff \| blob \| history
src/util/statistics_registry.h		diff \| blob \| history
src/util/statistics_stats.cpp		diff \| blob \| history
src/util/statistics_stats.h		diff \| blob \| history
src/util/statistics_value.cpp		diff \| blob \| history
src/util/statistics_value.h		diff \| blob \| history
src/util/string.cpp		diff \| blob \| history
src/util/string.h		diff \| blob \| history
src/util/synth_result.cpp		diff \| blob \| history
src/util/synth_result.h		diff \| blob \| history
src/util/uninterpreted_sort_value.cpp		diff \| blob \| history
src/util/uninterpreted_sort_value.h		diff \| blob \| history
src/util/utility.cpp		diff \| blob \| history
src/util/utility.h		diff \| blob \| history
test/CMakeLists.txt		diff \| blob \| history
test/api/CMakeLists.txt		diff \| blob \| history
test/api/cpp/CMakeLists.txt		diff \| blob \| history
test/api/cpp/boilerplate.cpp		diff \| blob \| history
test/api/cpp/issue4889.cpp		diff \| blob \| history
test/api/cpp/issue5074.cpp		diff \| blob \| history
test/api/cpp/issue6111.cpp		diff \| blob \| history
test/api/cpp/ouroborous.cpp		diff \| blob \| history
test/api/cpp/proj-issue306.cpp		diff \| blob \| history
test/api/cpp/proj-issue334.cpp		diff \| blob \| history
test/api/cpp/proj-issue344.cpp		diff \| blob \| history
test/api/cpp/proj-issue345.cpp		diff \| blob \| history
test/api/cpp/proj-issue377.cpp		diff \| blob \| history
test/api/cpp/proj-issue395.cpp		diff \| blob \| history
test/api/cpp/proj-issue399.cpp		diff \| blob \| history
test/api/cpp/proj-issue445.cpp		diff \| blob \| history
test/api/cpp/proj-issue484.cpp		diff \| blob \| history
test/api/cpp/reset_assertions.cpp		diff \| blob \| history
test/api/cpp/sep_log_api.cpp		diff \| blob \| history
test/api/cpp/smt2_compliance.cpp		diff \| blob \| history
test/api/cpp/two_solvers.cpp		diff \| blob \| history
test/api/python/CMakeLists.txt		diff \| blob \| history
test/api/python/boilerplate.py		diff \| blob \| history
test/api/python/issue4889.py		diff \| blob \| history
test/api/python/issue5074.py		diff \| blob \| history
test/api/python/issue6111.py		diff \| blob \| history
test/api/python/proj-issue306.py		diff \| blob \| history
test/api/python/reset_assertions.py		diff \| blob \| history
test/api/python/sep_log_api.py		diff \| blob \| history
test/api/python/two_solvers.py		diff \| blob \| history
test/binary/CMakeLists.txt		diff \| blob \| history
test/binary/interactive_shell.py		diff \| blob \| history
test/regress/cli/run_regression.py		diff \| blob \| history
test/unit/CMakeLists.txt		diff \| blob \| history
test/unit/api/CMakeLists.txt		diff \| blob \| history
test/unit/api/cpp/CMakeLists.txt		diff \| blob \| history
test/unit/api/cpp/datatype_api_black.cpp		diff \| blob \| history
test/unit/api/cpp/grammar_black.cpp		diff \| blob \| history
test/unit/api/cpp/op_black.cpp		diff \| blob \| history
test/unit/api/cpp/op_white.cpp		diff \| blob \| history
test/unit/api/cpp/parametric_datatype_black.cpp		diff \| blob \| history
test/unit/api/cpp/result_black.cpp		diff \| blob \| history
test/unit/api/cpp/solver_black.cpp		diff \| blob \| history
test/unit/api/cpp/solver_white.cpp		diff \| blob \| history
test/unit/api/cpp/sort_black.cpp		diff \| blob \| history
test/unit/api/cpp/synth_result_black.cpp		diff \| blob \| history
test/unit/api/cpp/term_black.cpp		diff \| blob \| history
test/unit/api/cpp/term_white.cpp		diff \| blob \| history
test/unit/api/cpp/theory_arith_nl_black.cpp		diff \| blob \| history
test/unit/api/cpp/theory_uf_ho_black.cpp		diff \| blob \| history
test/unit/api/java/CMakeLists.txt		diff \| blob \| history
test/unit/api/java/DatatypeTest.java		diff \| blob \| history
test/unit/api/java/GrammarTest.java		diff \| blob \| history
test/unit/api/java/OpTest.java		diff \| blob \| history
test/unit/api/java/ResultTest.java		diff \| blob \| history
test/unit/api/java/SolverTest.java		diff \| blob \| history
test/unit/api/java/SortTest.java		diff \| blob \| history
test/unit/api/java/SynthResultTest.java		diff \| blob \| history
test/unit/api/java/TermTest.java		diff \| blob \| history
test/unit/api/python/CMakeLists.txt		diff \| blob \| history
test/unit/api/python/test_datatype_api.py		diff \| blob \| history
test/unit/api/python/test_grammar.py		diff \| blob \| history
test/unit/api/python/test_op.py		diff \| blob \| history
test/unit/api/python/test_result.py		diff \| blob \| history
test/unit/api/python/test_solver.py		diff \| blob \| history
test/unit/api/python/test_sort.py		diff \| blob \| history
test/unit/api/python/test_synth_result.py		diff \| blob \| history
test/unit/api/python/test_term.py		diff \| blob \| history
test/unit/api/python/test_to_python_obj.py		diff \| blob \| history
test/unit/base/CMakeLists.txt		diff \| blob \| history
test/unit/base/map_util_black.cpp		diff \| blob \| history
test/unit/context/CMakeLists.txt		diff \| blob \| history
test/unit/context/cdhashmap_black.cpp		diff \| blob \| history
test/unit/context/cdhashmap_white.cpp		diff \| blob \| history
test/unit/context/cdlist_black.cpp		diff \| blob \| history
test/unit/context/cdo_black.cpp		diff \| blob \| history
test/unit/context/context_black.cpp		diff \| blob \| history
test/unit/context/context_mm_black.cpp		diff \| blob \| history
test/unit/context/context_white.cpp		diff \| blob \| history
test/unit/main/CMakeLists.txt		diff \| blob \| history
test/unit/main/interactive_shell_black.cpp		diff \| blob \| history
test/unit/node/CMakeLists.txt		diff \| blob \| history
test/unit/node/attribute_black.cpp		diff \| blob \| history
test/unit/node/attribute_white.cpp		diff \| blob \| history
test/unit/node/kind_black.cpp		diff \| blob \| history
test/unit/node/kind_map_black.cpp		diff \| blob \| history
test/unit/node/node_algorithm_black.cpp		diff \| blob \| history
test/unit/node/node_algorithms_black.cpp		diff \| blob \| history
test/unit/node/node_black.cpp		diff \| blob \| history
test/unit/node/node_builder_black.cpp		diff \| blob \| history
test/unit/node/node_manager_black.cpp		diff \| blob \| history
test/unit/node/node_manager_white.cpp		diff \| blob \| history
test/unit/node/node_self_iterator_black.cpp		diff \| blob \| history
test/unit/node/node_traversal_black.cpp		diff \| blob \| history
test/unit/node/node_white.cpp		diff \| blob \| history
test/unit/node/symbol_table_black.cpp		diff \| blob \| history
test/unit/node/type_cardinality_black.cpp		diff \| blob \| history
test/unit/node/type_node_white.cpp		diff \| blob \| history
test/unit/options/CMakeLists.txt		diff \| blob \| history
test/unit/options/options_black.cpp		diff \| blob \| history
test/unit/parser/CMakeLists.txt		diff \| blob \| history
test/unit/parser/parser_black.cpp		diff \| blob \| history
test/unit/parser/parser_builder_black.cpp		diff \| blob \| history
test/unit/preprocessing/CMakeLists.txt		diff \| blob \| history
test/unit/preprocessing/pass_bv_gauss_white.cpp		diff \| blob \| history
test/unit/preprocessing/pass_foreign_theory_rewrite_white.cpp		diff \| blob \| history
test/unit/printer/CMakeLists.txt		diff \| blob \| history
test/unit/printer/smt2_printer_black.cpp		diff \| blob \| history
test/unit/proof/CMakeLists.txt		diff \| blob \| history
test/unit/proof/lfsc_node_converter_black.cpp		diff \| blob \| history
test/unit/prop/CMakeLists.txt		diff \| blob \| history
test/unit/prop/cnf_stream_white.cpp		diff \| blob \| history
test/unit/test.h		diff \| blob \| history
test/unit/test_api.h		diff \| blob \| history
test/unit/test_context.h		diff \| blob \| history
test/unit/test_env.h		diff \| blob \| history
test/unit/test_node.h		diff \| blob \| history
test/unit/test_smt.h		diff \| blob \| history
test/unit/theory/CMakeLists.txt		diff \| blob \| history
test/unit/theory/arith_poly_white.cpp		diff \| blob \| history
test/unit/theory/evaluator_white.cpp		diff \| blob \| history
test/unit/theory/logic_info_white.cpp		diff \| blob \| history
test/unit/theory/regexp_operation_black.cpp		diff \| blob \| history
test/unit/theory/sequences_rewriter_white.cpp		diff \| blob \| history
test/unit/theory/strings_rewriter_white.cpp		diff \| blob \| history
test/unit/theory/theory_arith_coverings_white.cpp		diff \| blob \| history
test/unit/theory/theory_arith_pow2_white.cpp		diff \| blob \| history
test/unit/theory/theory_arith_rewriter_black.cpp		diff \| blob \| history
test/unit/theory/theory_arith_white.cpp		diff \| blob \| history
test/unit/theory/theory_bags_normal_form_white.cpp		diff \| blob \| history
test/unit/theory/theory_bags_rewriter_white.cpp		diff \| blob \| history
test/unit/theory/theory_bags_type_rules_white.cpp		diff \| blob \| history
test/unit/theory/theory_black.cpp		diff \| blob \| history
test/unit/theory/theory_bv_int_blaster_white.cpp		diff \| blob \| history
test/unit/theory/theory_bv_opt_white.cpp		diff \| blob \| history
test/unit/theory/theory_bv_rewriter_white.cpp		diff \| blob \| history
test/unit/theory/theory_bv_white.cpp		diff \| blob \| history
test/unit/theory/theory_engine_white.cpp		diff \| blob \| history
test/unit/theory/theory_int_opt_white.cpp		diff \| blob \| history
test/unit/theory/theory_opt_multigoal_white.cpp		diff \| blob \| history
test/unit/theory/theory_quantifiers_bv_instantiator_white.cpp		diff \| blob \| history
test/unit/theory/theory_quantifiers_bv_inverter_white.cpp		diff \| blob \| history
test/unit/theory/theory_sets_rewriter_white.cpp		diff \| blob \| history
test/unit/theory/theory_sets_type_enumerator_white.cpp		diff \| blob \| history
test/unit/theory/theory_sets_type_rules_white.cpp		diff \| blob \| history
test/unit/theory/theory_strings_skolem_cache_black.cpp		diff \| blob \| history
test/unit/theory/theory_strings_utils_white.cpp		diff \| blob \| history
test/unit/theory/theory_strings_word_white.cpp		diff \| blob \| history
test/unit/theory/theory_white.cpp		diff \| blob \| history
test/unit/theory/type_enumerator_white.cpp		diff \| blob \| history
test/unit/util/CMakeLists.txt		diff \| blob \| history
test/unit/util/array_store_all_white.cpp		diff \| blob \| history
test/unit/util/assert_white.cpp		diff \| blob \| history
test/unit/util/binary_heap_black.cpp		diff \| blob \| history
test/unit/util/bitvector_black.cpp		diff \| blob \| history
test/unit/util/boolean_simplification_black.cpp		diff \| blob \| history
test/unit/util/cardinality_black.cpp		diff \| blob \| history
test/unit/util/check_white.cpp		diff \| blob \| history
test/unit/util/configuration_black.cpp		diff \| blob \| history
test/unit/util/datatype_black.cpp		diff \| blob \| history
test/unit/util/didyoumean_black.cpp		diff \| blob \| history
test/unit/util/exception_black.cpp		diff \| blob \| history
test/unit/util/floatingpoint_black.cpp		diff \| blob \| history
test/unit/util/integer_black.cpp		diff \| blob \| history
test/unit/util/integer_white.cpp		diff \| blob \| history
test/unit/util/output_black.cpp		diff \| blob \| history
test/unit/util/rational_black.cpp		diff \| blob \| history
test/unit/util/rational_white.cpp		diff \| blob \| history
test/unit/util/real_algebraic_number_black.cpp		diff \| blob \| history
test/unit/util/stats_black.cpp		diff \| blob \| history

RSS Atom