From d01e59c13b7337e68806be72145b3e45e4cad89c Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Tue, 5 Apr 2022 13:38:57 -0700 Subject: [PATCH] Update copyright headers for release 1.0 (#8539) --- CMakeLists.txt | 2 +- cmake/CMakeGraphVizOptions.cmake.in | 2 +- cmake/ConfigCompetition.cmake | 4 +-- cmake/ConfigDebug.cmake | 4 +-- cmake/ConfigProduction.cmake | 4 +-- cmake/ConfigTesting.cmake | 2 +- cmake/ConfigureCvc5.cmake | 4 +-- cmake/FindANTLR3.cmake | 4 +-- cmake/FindCLN.cmake | 4 +-- cmake/FindCVC5PythonicAPI.cmake | 4 +-- cmake/FindCaDiCaL.cmake | 4 +-- cmake/FindCoCoA.cmake | 4 +-- cmake/FindCryptoMiniSat.cmake | 4 +-- cmake/FindDrat2Er.cmake | 2 +- cmake/FindDummy.cmake.template | 2 +- cmake/FindEditline.cmake | 4 +-- cmake/FindGLPK.cmake | 2 +- cmake/FindGMP.cmake | 2 +- cmake/FindGTest.cmake | 4 +-- cmake/FindHamcrest.cmake | 2 +- cmake/FindJUnit.cmake | 4 +-- cmake/FindKissat.cmake | 4 +-- cmake/FindLFSC.cmake | 2 +- cmake/FindPoly.cmake | 4 +-- cmake/FindSphinx.cmake | 2 +- cmake/FindSymFPU.cmake | 4 +-- cmake/FindValgrind.cmake | 2 +- cmake/Helpers.cmake | 4 +-- cmake/IWYU.cmake | 2 +- cmake/Toolchain-aarch64.cmake | 4 +-- cmake/Toolchain-mingw64.cmake | 4 +-- cmake/cvc5Config.cmake.in | 4 +-- cmake/deps-helper.cmake | 4 +-- cmake/fuzzing-murxla.cmake | 4 +-- cmake/target-graphs.cmake | 2 +- cmake/version.cmake | 4 +-- contrib/get-authors | 4 +++ contrib/update-copyright.pl | 5 ++-- examples/CMakeLists.txt | 4 +-- examples/SimpleVC.java | 4 +-- examples/api/cpp/CMakeLists.txt | 4 +-- examples/api/cpp/bags.cpp | 1 + examples/api/cpp/bitvectors.cpp | 4 +-- examples/api/cpp/bitvectors_and_arrays.cpp | 4 +-- examples/api/cpp/combination.cpp | 4 +-- examples/api/cpp/datatypes.cpp | 2 +- examples/api/cpp/extract.cpp | 4 +-- examples/api/cpp/floating_point_arith.cpp | 4 +-- examples/api/cpp/helloworld.cpp | 4 +-- examples/api/cpp/linear_arith.cpp | 4 +-- examples/api/cpp/quickstart.cpp | 4 +-- examples/api/cpp/relations.cpp | 4 +-- examples/api/cpp/sequences.cpp | 4 +-- examples/api/cpp/sets.cpp | 4 +-- examples/api/cpp/strings.cpp | 4 +-- examples/api/cpp/sygus-fun.cpp | 4 +-- examples/api/cpp/sygus-grammar.cpp | 4 +-- examples/api/cpp/sygus-inv.cpp | 4 +-- examples/api/cpp/transcendentals.cpp | 4 +-- examples/api/cpp/utils.cpp | 4 +-- examples/api/cpp/utils.h | 4 +-- examples/api/java/Bags.java | 2 +- examples/api/java/BitVectors.java | 4 +-- examples/api/java/BitVectorsAndArrays.java | 4 +-- examples/api/java/CMakeLists.txt | 4 +-- examples/api/java/Combination.java | 4 +-- examples/api/java/Datatypes.java | 4 +-- examples/api/java/Exceptions.java | 4 +-- examples/api/java/Extract.java | 4 +-- examples/api/java/FloatingPointArith.java | 4 +-- examples/api/java/HelloWorld.java | 4 +-- examples/api/java/LinearArith.java | 4 +-- examples/api/java/QuickStart.java | 4 +-- examples/api/java/Relations.java | 4 +-- examples/api/java/Sequences.java | 4 +-- examples/api/java/Sets.java | 4 +-- examples/api/java/Statistics.java | 4 +-- examples/api/java/Strings.java | 4 +-- examples/api/java/SygusFun.java | 4 +-- examples/api/java/SygusGrammar.java | 4 +-- examples/api/java/SygusInv.java | 4 +-- examples/api/java/Transcendentals.java | 4 +-- examples/api/java/UnsatCores.java | 4 +-- examples/api/java/Utils.java | 2 +- examples/api/python/CMakeLists.txt | 4 +-- examples/api/python/bags.py | 4 +-- examples/api/python/bitvectors.py | 4 +-- examples/api/python/bitvectors_and_arrays.py | 4 +-- examples/api/python/combination.py | 4 +-- examples/api/python/datatypes.py | 4 +-- examples/api/python/exceptions.py | 4 +-- examples/api/python/extract.py | 4 +-- examples/api/python/floating_point.py | 4 +-- examples/api/python/helloworld.py | 4 +-- examples/api/python/id.py | 2 +- examples/api/python/linear_arith.py | 4 +-- examples/api/python/quickstart.py | 4 +-- examples/api/python/relations.py | 4 +-- examples/api/python/sequences.py | 4 +-- examples/api/python/sets.py | 4 +-- examples/api/python/strings.py | 4 +-- examples/api/python/sygus-fun.py | 4 +-- examples/api/python/sygus-grammar.py | 4 +-- examples/api/python/sygus-inv.py | 4 +-- examples/api/python/transcendentals.py | 4 +-- examples/api/python/utils.py | 4 +-- examples/simple_vc_cxx.cpp | 4 +-- examples/simple_vc_quant_cxx.cpp | 4 +-- src/CMakeLists.txt | 2 +- src/api/cpp/cvc5.cpp | 4 +-- src/api/cpp/cvc5.h | 4 +-- src/api/cpp/cvc5_checks.h | 4 +-- src/api/cpp/cvc5_kind.h | 4 +-- src/api/cpp/cvc5_types.cpp | 2 +- src/api/cpp/cvc5_types.h | 4 +-- src/api/java/CMakeLists.txt | 4 +-- src/api/java/genenums.py.in | 4 +-- .../java/io/github/cvc5/AbstractPointer.java | 4 +-- .../java/io/github/cvc5/CVC5ApiException.java | 4 +-- .../github/cvc5/CVC5ApiOptionException.java | 4 +-- .../cvc5/CVC5ApiRecoverableException.java | 4 +-- src/api/java/io/github/cvc5/Datatype.java | 4 +-- .../io/github/cvc5/DatatypeConstructor.java | 4 +-- .../github/cvc5/DatatypeConstructorDecl.java | 4 +-- src/api/java/io/github/cvc5/DatatypeDecl.java | 4 +-- .../java/io/github/cvc5/DatatypeSelector.java | 4 +-- src/api/java/io/github/cvc5/Grammar.java | 4 +-- src/api/java/io/github/cvc5/IPointer.java | 4 +-- src/api/java/io/github/cvc5/Op.java | 4 +-- src/api/java/io/github/cvc5/OptionInfo.java | 4 +-- src/api/java/io/github/cvc5/Pair.java | 4 +-- src/api/java/io/github/cvc5/Result.java | 4 +-- src/api/java/io/github/cvc5/Solver.java | 4 +-- src/api/java/io/github/cvc5/Sort.java | 4 +-- src/api/java/io/github/cvc5/Stat.java | 4 +-- src/api/java/io/github/cvc5/Statistics.java | 4 +-- src/api/java/io/github/cvc5/SynthResult.java | 4 +-- src/api/java/io/github/cvc5/Term.java | 4 +-- src/api/java/io/github/cvc5/Triplet.java | 4 +-- src/api/java/io/github/cvc5/Utils.java | 4 +-- src/api/java/jni/api_utilities.cpp | 2 +- src/api/java/jni/api_utilities.h | 4 +-- src/api/java/jni/datatype.cpp | 4 +-- src/api/java/jni/datatype_constructor.cpp | 4 +-- .../java/jni/datatype_constructor_decl.cpp | 4 +-- src/api/java/jni/datatype_decl.cpp | 4 +-- src/api/java/jni/datatype_selector.cpp | 4 +-- src/api/java/jni/grammar.cpp | 4 +-- src/api/java/jni/op.cpp | 4 +-- src/api/java/jni/option_info.cpp | 4 +-- src/api/java/jni/result.cpp | 4 +-- src/api/java/jni/solver.cpp | 4 +-- src/api/java/jni/sort.cpp | 4 +-- src/api/java/jni/stat.cpp | 4 +-- src/api/java/jni/statistics.cpp | 4 +-- src/api/java/jni/synth_result.cpp | 4 +-- src/api/java/jni/term.cpp | 4 +-- src/api/parseenums.py | 4 +-- src/api/python/CMakeLists.txt | 4 +-- src/api/python/genenums.py.in | 4 +-- src/api/python/setup.py.in | 4 +-- src/base/CMakeLists.txt | 4 +-- src/base/check.cpp | 2 +- src/base/check.h | 4 +-- src/base/collect_tags.py | 2 +- src/base/configuration.cpp | 6 ++--- src/base/configuration.h | 8 +++--- src/base/configuration_private.h | 4 +-- src/base/cvc5config.h.in | 13 +++++++++ src/base/exception.cpp | 2 +- src/base/exception.h | 4 +-- src/base/listener.cpp | 2 +- src/base/listener.h | 4 +-- src/base/map_util.h | 4 +-- src/base/modal_exception.h | 2 +- src/base/output.cpp | 2 +- src/base/output.h | 4 +-- src/base/versioninfo.cpp.in | 4 +-- src/context/CMakeLists.txt | 4 +-- src/context/cdhashmap.h | 4 +-- src/context/cdhashmap_forward.h | 4 +-- src/context/cdhashset.h | 2 +- src/context/cdhashset_forward.h | 4 +-- src/context/cdinsert_hashmap.h | 4 +-- src/context/cdinsert_hashmap_forward.h | 4 +-- src/context/cdlist.h | 4 +-- src/context/cdlist_forward.h | 4 +-- src/context/cdmaybe.h | 2 +- src/context/cdo.h | 4 +-- src/context/cdqueue.h | 2 +- src/context/cdtrail_queue.h | 4 +-- src/context/context.cpp | 2 +- src/context/context.h | 2 +- src/context/context_mm.cpp | 4 +-- src/context/context_mm.h | 2 +- src/decision/assertion_list.cpp | 4 +-- src/decision/assertion_list.h | 4 +-- src/decision/decision_engine.cpp | 4 +-- src/decision/decision_engine.h | 4 +-- src/decision/justification_strategy.cpp | 4 +-- src/decision/justification_strategy.h | 2 +- src/decision/justify_info.cpp | 2 +- src/decision/justify_info.h | 2 +- src/decision/justify_stack.cpp | 4 +-- src/decision/justify_stack.h | 2 +- src/decision/justify_stats.cpp | 4 +-- src/decision/justify_stats.h | 2 +- src/expr/CMakeLists.txt | 2 +- src/expr/algorithm/flatten.h | 2 +- src/expr/annotation_elim_node_converter.cpp | 4 +-- src/expr/annotation_elim_node_converter.h | 2 +- src/expr/array_store_all.cpp | 2 +- src/expr/array_store_all.h | 4 +-- src/expr/ascription_type.cpp | 4 +-- src/expr/ascription_type.h | 2 +- src/expr/attribute.cpp | 2 +- src/expr/attribute.h | 4 +-- src/expr/attribute_internals.h | 2 +- src/expr/attribute_unique_id.h | 4 +-- src/expr/bound_var_manager.cpp | 4 +-- src/expr/bound_var_manager.h | 4 +-- src/expr/cardinality_constraint.cpp | 4 +-- src/expr/cardinality_constraint.h | 2 +- src/expr/codatatype_bound_variable.cpp | 4 +-- src/expr/codatatype_bound_variable.h | 2 +- src/expr/datatype_index.cpp | 2 +- src/expr/datatype_index.h | 2 +- src/expr/dtype.cpp | 4 +-- src/expr/dtype.h | 4 +-- src/expr/dtype_cons.cpp | 4 +-- src/expr/dtype_cons.h | 4 +-- src/expr/dtype_selector.cpp | 4 +-- src/expr/dtype_selector.h | 4 +-- src/expr/emptybag.cpp | 4 +-- src/expr/emptybag.h | 4 +-- src/expr/emptyset.cpp | 2 +- src/expr/emptyset.h | 4 +-- src/expr/kind_map.h | 4 +-- src/expr/kind_template.cpp | 4 +-- src/expr/kind_template.h | 4 +-- src/expr/match_trie.cpp | 4 +-- src/expr/match_trie.h | 4 +-- src/expr/metakind_template.cpp | 4 +-- src/expr/metakind_template.h | 4 +-- src/expr/mkexpr | 2 +- src/expr/mkkind | 2 +- src/expr/mkmetakind | 2 +- src/expr/nary_match_trie.cpp | 4 +-- src/expr/nary_match_trie.h | 4 +-- src/expr/nary_term_util.cpp | 4 +-- src/expr/nary_term_util.h | 2 +- src/expr/node.cpp | 2 +- src/expr/node.h | 2 +- src/expr/node_algorithm.cpp | 2 +- src/expr/node_algorithm.h | 2 +- src/expr/node_builder.cpp | 2 +- src/expr/node_builder.h | 2 +- src/expr/node_converter.cpp | 4 +-- src/expr/node_converter.h | 2 +- src/expr/node_manager_attributes.h | 4 +-- src/expr/node_manager_template.cpp | 4 +-- src/expr/node_manager_template.h | 2 +- src/expr/node_self_iterator.h | 4 +-- src/expr/node_traversal.cpp | 2 +- src/expr/node_traversal.h | 4 +-- src/expr/node_trie.cpp | 2 +- src/expr/node_trie.h | 4 +-- src/expr/node_trie_algorithm.cpp | 2 +- src/expr/node_trie_algorithm.h | 2 +- src/expr/node_value.cpp | 10 +++---- src/expr/node_value.h | 10 +++---- src/expr/node_visitor.h | 2 +- src/expr/sequence.cpp | 4 +-- src/expr/sequence.h | 2 +- src/expr/skolem_manager.cpp | 4 +-- src/expr/skolem_manager.h | 4 +-- src/expr/subs.cpp | 4 +-- src/expr/subs.h | 4 +-- src/expr/subtype_elim_node_converter.cpp | 4 +-- src/expr/subtype_elim_node_converter.h | 2 +- src/expr/sygus_datatype.cpp | 4 +-- src/expr/sygus_datatype.h | 4 +-- src/expr/symbol_manager.cpp | 4 +-- src/expr/symbol_manager.h | 4 +-- src/expr/symbol_table.cpp | 4 +-- src/expr/symbol_table.h | 2 +- src/expr/term_canonize.cpp | 4 +-- src/expr/term_canonize.h | 4 +-- src/expr/term_context.cpp | 4 +-- src/expr/term_context.h | 4 +-- src/expr/term_context_node.cpp | 4 +-- src/expr/term_context_node.h | 4 +-- src/expr/term_context_stack.cpp | 2 +- src/expr/term_context_stack.h | 4 +-- src/expr/type_checker.h | 4 +-- src/expr/type_checker_template.cpp | 4 +-- src/expr/type_checker_util.h | 2 +- src/expr/type_matcher.cpp | 4 +-- src/expr/type_matcher.h | 4 +-- src/expr/type_node.cpp | 4 +-- src/expr/type_node.h | 4 +-- src/expr/type_properties_template.cpp | 4 +-- src/expr/type_properties_template.h | 4 +-- src/expr/variadic_trie.cpp | 2 +- src/expr/variadic_trie.h | 2 +- src/include/cvc5_private.h | 4 +-- src/include/cvc5_private_library.h | 4 +-- src/include/cvc5_public.h | 4 +-- src/include/cvc5parser_private.h | 4 +-- src/include/cvc5parser_public.h | 4 +-- src/lib/clock_gettime.c | 2 +- src/lib/clock_gettime.h | 4 +-- src/lib/ffs.c | 2 +- src/lib/ffs.h | 4 +-- src/lib/replacements.h | 4 +-- src/lib/strtok_r.c | 2 +- src/lib/strtok_r.h | 4 +-- src/main/CMakeLists.txt | 2 +- src/main/command_executor.cpp | 4 +-- src/main/command_executor.h | 4 +-- src/main/driver_unified.cpp | 4 +-- src/main/interactive_shell.cpp | 4 +-- src/main/interactive_shell.h | 4 +-- src/main/main.cpp | 4 +-- src/main/main.h | 4 +-- src/main/options.h | 4 +-- src/main/options_template.cpp | 4 +-- src/main/signal_handlers.cpp | 4 +-- src/main/signal_handlers.h | 4 +-- src/main/time_limit.cpp | 4 +-- src/main/time_limit.h | 4 +-- src/omt/bitvector_optimizer.cpp | 4 +-- src/omt/bitvector_optimizer.h | 4 +-- src/omt/integer_optimizer.cpp | 4 +-- src/omt/integer_optimizer.h | 4 +-- src/omt/omt_optimizer.cpp | 4 +-- src/omt/omt_optimizer.h | 4 +-- src/options/didyoumean_test.cpp | 4 +-- src/options/io_utils.cpp | 2 +- src/options/io_utils.h | 2 +- src/options/language.cpp | 4 +-- src/options/language.h | 4 +-- src/options/managed_streams.cpp | 4 +-- src/options/managed_streams.h | 2 +- src/options/mkoptions.py | 4 +-- src/options/module_template.cpp | 4 +-- src/options/module_template.h | 4 +-- src/options/option_exception.cpp | 2 +- src/options/option_exception.h | 4 +-- src/options/options_handler.cpp | 4 +-- src/options/options_handler.h | 4 +-- src/options/options_listener.h | 4 +-- src/options/options_public.h | 2 +- src/options/options_public_template.cpp | 4 +-- src/options/options_template.cpp | 4 +-- src/options/options_template.h | 4 +-- src/parser/CMakeLists.txt | 4 +-- src/parser/antlr_input.cpp | 4 +-- src/parser/antlr_input.h | 2 +- src/parser/antlr_input_imports.cpp | 4 +-- src/parser/antlr_line_buffered_input.cpp | 4 +-- src/parser/antlr_line_buffered_input.h | 4 +-- src/parser/bounded_token_buffer.cpp | 2 +- src/parser/bounded_token_buffer.h | 4 +-- src/parser/bounded_token_factory.cpp | 2 +- src/parser/bounded_token_factory.h | 4 +-- src/parser/input.cpp | 4 +-- src/parser/input.h | 2 +- src/parser/line_buffer.cpp | 2 +- src/parser/line_buffer.h | 4 +-- src/parser/parse_op.cpp | 4 +-- src/parser/parse_op.h | 4 +-- src/parser/parser.cpp | 4 +-- src/parser/parser.h | 2 +- src/parser/parser_builder.cpp | 4 +-- src/parser/parser_builder.h | 4 +-- src/parser/parser_exception.h | 2 +- src/parser/smt2/Smt2.g | 6 ++--- src/parser/smt2/smt2.cpp | 4 +-- src/parser/smt2/smt2.h | 4 +-- src/parser/smt2/smt2_input.cpp | 4 +-- src/parser/smt2/smt2_input.h | 4 +-- src/parser/smt2/sygus_input.cpp | 4 +-- src/parser/smt2/sygus_input.h | 4 +-- src/parser/tptp/Tptp.g | 6 ++--- src/parser/tptp/tptp.cpp | 2 +- src/parser/tptp/tptp.h | 4 +-- src/parser/tptp/tptp_input.cpp | 4 +-- src/parser/tptp/tptp_input.h | 4 +-- src/preprocessing/assertion_pipeline.cpp | 4 +-- src/preprocessing/assertion_pipeline.h | 2 +- src/preprocessing/learned_literal_manager.cpp | 2 +- src/preprocessing/learned_literal_manager.h | 4 +-- src/preprocessing/passes/ackermann.cpp | 2 +- src/preprocessing/passes/ackermann.h | 4 +-- src/preprocessing/passes/apply_substs.cpp | 4 +-- src/preprocessing/passes/apply_substs.h | 4 +-- src/preprocessing/passes/bool_to_bv.cpp | 4 +-- src/preprocessing/passes/bool_to_bv.h | 4 +-- src/preprocessing/passes/bv_eager_atoms.cpp | 4 +-- src/preprocessing/passes/bv_eager_atoms.h | 4 +-- src/preprocessing/passes/bv_gauss.cpp | 2 +- src/preprocessing/passes/bv_gauss.h | 2 +- src/preprocessing/passes/bv_intro_pow2.cpp | 2 +- src/preprocessing/passes/bv_intro_pow2.h | 4 +-- src/preprocessing/passes/bv_to_bool.cpp | 2 +- src/preprocessing/passes/bv_to_bool.h | 4 +-- src/preprocessing/passes/bv_to_int.cpp | 4 +-- src/preprocessing/passes/bv_to_int.h | 5 ++-- .../passes/extended_rewriter_pass.cpp | 4 +-- .../passes/extended_rewriter_pass.h | 4 +-- .../passes/foreign_theory_rewrite.cpp | 4 +-- .../passes/foreign_theory_rewrite.h | 4 +-- src/preprocessing/passes/fun_def_fmf.cpp | 2 +- src/preprocessing/passes/fun_def_fmf.h | 4 +-- src/preprocessing/passes/global_negate.cpp | 4 +-- src/preprocessing/passes/global_negate.h | 4 +-- src/preprocessing/passes/ho_elim.cpp | 4 +-- src/preprocessing/passes/ho_elim.h | 4 +-- src/preprocessing/passes/int_to_bv.cpp | 4 +-- src/preprocessing/passes/int_to_bv.h | 4 +-- src/preprocessing/passes/ite_removal.cpp | 2 +- src/preprocessing/passes/ite_removal.h | 4 +-- src/preprocessing/passes/ite_simp.cpp | 4 +-- src/preprocessing/passes/ite_simp.h | 4 +-- src/preprocessing/passes/learned_rewrite.cpp | 4 +-- src/preprocessing/passes/learned_rewrite.h | 2 +- src/preprocessing/passes/miplib_trick.cpp | 4 +-- src/preprocessing/passes/miplib_trick.h | 4 +-- src/preprocessing/passes/nl_ext_purify.cpp | 4 +-- src/preprocessing/passes/nl_ext_purify.h | 4 +-- src/preprocessing/passes/non_clausal_simp.cpp | 2 +- src/preprocessing/passes/non_clausal_simp.h | 2 +- .../passes/pseudo_boolean_processor.cpp | 4 +-- .../passes/pseudo_boolean_processor.h | 4 +-- .../passes/quantifiers_preprocess.cpp | 4 +-- .../passes/quantifiers_preprocess.h | 4 +-- src/preprocessing/passes/real_to_int.cpp | 2 +- src/preprocessing/passes/real_to_int.h | 4 +-- src/preprocessing/passes/rewrite.cpp | 4 +-- src/preprocessing/passes/rewrite.h | 4 +-- src/preprocessing/passes/sep_skolem_emp.cpp | 2 +- src/preprocessing/passes/sep_skolem_emp.h | 4 +-- src/preprocessing/passes/sort_infer.cpp | 4 +-- src/preprocessing/passes/sort_infer.h | 4 +-- src/preprocessing/passes/static_learning.cpp | 4 +-- src/preprocessing/passes/static_learning.h | 4 +-- src/preprocessing/passes/strings_eager_pp.cpp | 4 +-- src/preprocessing/passes/strings_eager_pp.h | 4 +-- src/preprocessing/passes/sygus_inference.cpp | 2 +- src/preprocessing/passes/sygus_inference.h | 4 +-- src/preprocessing/passes/synth_rew_rules.cpp | 4 +-- src/preprocessing/passes/synth_rew_rules.h | 4 +-- .../passes/theory_preprocess.cpp | 4 +-- src/preprocessing/passes/theory_preprocess.h | 4 +-- .../passes/theory_rewrite_eq.cpp | 4 +-- src/preprocessing/passes/theory_rewrite_eq.h | 4 +-- .../passes/unconstrained_simplifier.cpp | 2 +- .../passes/unconstrained_simplifier.h | 2 +- src/preprocessing/preprocessing_pass.cpp | 4 +-- src/preprocessing/preprocessing_pass.h | 4 +-- .../preprocessing_pass_context.cpp | 4 +-- .../preprocessing_pass_context.h | 4 +-- .../preprocessing_pass_registry.cpp | 4 +-- .../preprocessing_pass_registry.h | 4 +-- src/preprocessing/util/ite_utilities.cpp | 2 +- src/preprocessing/util/ite_utilities.h | 2 +- src/printer/ast/ast_printer.cpp | 2 +- src/printer/ast/ast_printer.h | 2 +- src/printer/let_binding.cpp | 4 +-- src/printer/let_binding.h | 4 +-- src/printer/printer.cpp | 4 +-- src/printer/printer.h | 2 +- src/printer/smt2/smt2_printer.cpp | 2 +- src/printer/smt2/smt2_printer.h | 4 +-- src/printer/tptp/tptp_printer.cpp | 2 +- src/printer/tptp/tptp_printer.h | 4 +-- src/proof/alethe/alethe_node_converter.cpp | 2 +- src/proof/alethe/alethe_node_converter.h | 2 +- .../alethe_nosubtype_node_converter.cpp | 4 +-- .../alethe/alethe_nosubtype_node_converter.h | 2 +- src/proof/alethe/alethe_post_processor.cpp | 4 +-- src/proof/alethe/alethe_post_processor.h | 2 +- src/proof/alethe/alethe_printer.cpp | 2 +- src/proof/alethe/alethe_printer.h | 2 +- src/proof/alethe/alethe_proof_rule.cpp | 4 +-- src/proof/alethe/alethe_proof_rule.h | 4 +-- src/proof/annotation_proof_generator.cpp | 2 +- src/proof/annotation_proof_generator.h | 2 +- src/proof/assumption_proof_generator.cpp | 2 +- src/proof/assumption_proof_generator.h | 2 +- src/proof/buffered_proof_generator.cpp | 2 +- src/proof/buffered_proof_generator.h | 2 +- src/proof/clause_id.h | 4 +-- src/proof/conv_proof_generator.cpp | 4 +-- src/proof/conv_proof_generator.h | 4 +-- src/proof/conv_seq_proof_generator.cpp | 4 +-- src/proof/conv_seq_proof_generator.h | 4 +-- src/proof/dot/dot_printer.cpp | 4 +-- src/proof/dot/dot_printer.h | 4 +-- src/proof/eager_proof_generator.cpp | 2 +- src/proof/eager_proof_generator.h | 2 +- src/proof/lazy_proof.cpp | 4 +-- src/proof/lazy_proof.h | 4 +-- src/proof/lazy_proof_chain.cpp | 2 +- src/proof/lazy_proof_chain.h | 4 +-- src/proof/lazy_tree_proof_generator.cpp | 2 +- src/proof/lazy_tree_proof_generator.h | 4 +-- .../lfsc/lfsc_list_sc_node_converter.cpp | 2 +- src/proof/lfsc/lfsc_list_sc_node_converter.h | 2 +- src/proof/lfsc/lfsc_node_converter.cpp | 4 +-- src/proof/lfsc/lfsc_node_converter.h | 2 +- src/proof/lfsc/lfsc_post_processor.cpp | 27 ++++++++++--------- src/proof/lfsc/lfsc_post_processor.h | 27 ++++++++++--------- src/proof/lfsc/lfsc_print_channel.cpp | 4 +-- src/proof/lfsc/lfsc_print_channel.h | 2 +- src/proof/lfsc/lfsc_printer.cpp | 4 +-- src/proof/lfsc/lfsc_printer.h | 2 +- src/proof/lfsc/lfsc_util.cpp | 4 +-- src/proof/lfsc/lfsc_util.h | 4 +-- src/proof/method_id.cpp | 4 +-- src/proof/method_id.h | 4 +-- src/proof/print_expr.cpp | 2 +- src/proof/print_expr.h | 2 +- src/proof/proof.cpp | 4 +-- src/proof/proof.h | 4 +-- src/proof/proof_checker.cpp | 4 +-- src/proof/proof_checker.h | 2 +- src/proof/proof_ensure_closed.cpp | 4 +-- src/proof/proof_ensure_closed.h | 2 +- src/proof/proof_generator.cpp | 2 +- src/proof/proof_generator.h | 2 +- src/proof/proof_letify.cpp | 2 +- src/proof/proof_letify.h | 2 +- src/proof/proof_node.cpp | 4 +-- src/proof/proof_node.h | 2 +- src/proof/proof_node_algorithm.cpp | 4 +-- src/proof/proof_node_algorithm.h | 2 +- src/proof/proof_node_manager.cpp | 4 +-- src/proof/proof_node_manager.h | 2 +- src/proof/proof_node_to_sexpr.cpp | 4 +-- src/proof/proof_node_to_sexpr.h | 2 +- src/proof/proof_node_updater.cpp | 4 +-- src/proof/proof_node_updater.h | 2 +- src/proof/proof_rule.cpp | 2 +- src/proof/proof_rule.h | 4 +-- src/proof/proof_set.h | 2 +- src/proof/proof_step_buffer.cpp | 4 +-- src/proof/proof_step_buffer.h | 2 +- src/proof/theory_proof_step_buffer.cpp | 4 +-- src/proof/theory_proof_step_buffer.h | 2 +- src/proof/trust_node.cpp | 2 +- src/proof/trust_node.h | 2 +- src/proof/unsat_core.cpp | 4 +-- src/proof/unsat_core.h | 4 +-- src/prop/cadical.cpp | 4 +-- src/prop/cadical.h | 4 +-- src/prop/cnf_stream.cpp | 4 +-- src/prop/cnf_stream.h | 4 +-- src/prop/cryptominisat.cpp | 4 +-- src/prop/cryptominisat.h | 4 +-- src/prop/kissat.cpp | 4 +-- src/prop/kissat.h | 4 +-- src/prop/minisat/minisat.cpp | 4 +-- src/prop/minisat/minisat.h | 4 +-- src/prop/opt_clauses_manager.cpp | 4 +-- src/prop/opt_clauses_manager.h | 2 +- src/prop/proof_cnf_stream.cpp | 2 +- src/prop/proof_cnf_stream.h | 2 +- src/prop/proof_post_processor.cpp | 4 +-- src/prop/proof_post_processor.h | 4 +-- src/prop/prop_engine.cpp | 4 +-- src/prop/prop_engine.h | 2 +- src/prop/prop_proof_manager.cpp | 4 +-- src/prop/prop_proof_manager.h | 4 +-- src/prop/registrar.h | 4 +-- src/prop/sat_proof_manager.cpp | 4 +-- src/prop/sat_proof_manager.h | 4 +-- src/prop/sat_solver.h | 4 +-- src/prop/sat_solver_factory.cpp | 4 +-- src/prop/sat_solver_factory.h | 4 +-- src/prop/sat_solver_types.cpp | 2 +- src/prop/sat_solver_types.h | 2 +- src/prop/skolem_def_manager.cpp | 4 +-- src/prop/skolem_def_manager.h | 4 +-- src/prop/theory_proxy.cpp | 4 +-- src/prop/theory_proxy.h | 4 +-- src/prop/zero_level_learner.cpp | 2 +- src/prop/zero_level_learner.h | 4 +-- src/smt/abduction_solver.cpp | 4 +-- src/smt/abduction_solver.h | 2 +- src/smt/abstract_values.cpp | 4 +-- src/smt/abstract_values.h | 4 +-- src/smt/assertions.cpp | 4 +-- src/smt/assertions.h | 2 +- src/smt/check_models.cpp | 4 +-- src/smt/check_models.h | 4 +-- src/smt/command.cpp | 4 +-- src/smt/command.h | 4 +-- src/smt/difficulty_post_processor.cpp | 4 +-- src/smt/difficulty_post_processor.h | 2 +- src/smt/env.cpp | 4 +-- src/smt/env.h | 4 +-- src/smt/env_obj.cpp | 4 +-- src/smt/env_obj.h | 4 +-- src/smt/expand_definitions.cpp | 4 +-- src/smt/expand_definitions.h | 4 +-- src/smt/interpolation_solver.cpp | 2 +- src/smt/interpolation_solver.h | 4 +-- src/smt/listeners.cpp | 4 +-- src/smt/listeners.h | 4 +-- src/smt/logic_exception.h | 4 +-- src/smt/model.cpp | 4 +-- src/smt/model.h | 4 +-- src/smt/model_blocker.cpp | 4 +-- src/smt/model_blocker.h | 4 +-- src/smt/model_core_builder.cpp | 4 +-- src/smt/model_core_builder.h | 4 +-- src/smt/optimization_solver.cpp | 4 +-- src/smt/optimization_solver.h | 2 +- src/smt/preprocess_proof_generator.cpp | 4 +-- src/smt/preprocess_proof_generator.h | 4 +-- src/smt/preprocessor.cpp | 4 +-- src/smt/preprocessor.h | 4 +-- src/smt/print_benchmark.cpp | 4 +-- src/smt/print_benchmark.h | 2 +- src/smt/process_assertions.cpp | 4 +-- src/smt/process_assertions.h | 4 +-- src/smt/proof_final_callback.cpp | 4 +-- src/smt/proof_final_callback.h | 2 +- src/smt/proof_manager.cpp | 4 +-- src/smt/proof_manager.h | 4 +-- src/smt/proof_post_processor.cpp | 4 +-- src/smt/proof_post_processor.h | 4 +-- src/smt/quant_elim_solver.cpp | 4 +-- src/smt/quant_elim_solver.h | 4 +-- src/smt/set_defaults.cpp | 4 +-- src/smt/set_defaults.h | 4 +-- src/smt/smt_mode.cpp | 2 +- src/smt/smt_mode.h | 4 +-- src/smt/smt_solver.cpp | 4 +-- src/smt/smt_solver.h | 4 +-- src/smt/smt_statistics_registry.cpp | 4 +-- src/smt/smt_statistics_registry.h | 4 +-- src/smt/solver_engine.cpp | 4 +-- src/smt/solver_engine.h | 4 +-- src/smt/solver_engine_scope.cpp | 4 +-- src/smt/solver_engine_scope.h | 4 +-- src/smt/solver_engine_state.cpp | 4 +-- src/smt/solver_engine_state.h | 4 +-- src/smt/solver_engine_stats.cpp | 4 +-- src/smt/solver_engine_stats.h | 4 +-- src/smt/sygus_solver.cpp | 4 +-- src/smt/sygus_solver.h | 4 +-- src/smt/term_formula_removal.cpp | 2 +- src/smt/term_formula_removal.h | 2 +- src/smt/unsat_core_manager.cpp | 4 +-- src/smt/unsat_core_manager.h | 4 +-- src/smt/witness_form.cpp | 4 +-- src/smt/witness_form.h | 4 +-- src/smt_util/boolean_simplification.cpp | 2 +- src/smt_util/boolean_simplification.h | 2 +- src/theory/CMakeLists.txt | 2 +- src/theory/arith/approx_simplex.cpp | 4 +-- src/theory/arith/approx_simplex.h | 4 +-- src/theory/arith/arith_evaluator.cpp | 14 ++++++++++ src/theory/arith/arith_evaluator.h | 14 ++++++++++ src/theory/arith/arith_ite_utils.cpp | 4 +-- src/theory/arith/arith_ite_utils.h | 4 +-- src/theory/arith/arith_msum.cpp | 4 +-- src/theory/arith/arith_msum.h | 4 +-- src/theory/arith/arith_poly_norm.cpp | 4 +-- src/theory/arith/arith_poly_norm.h | 4 +-- src/theory/arith/arith_preprocess.cpp | 4 +-- src/theory/arith/arith_preprocess.h | 4 +-- src/theory/arith/arith_rewriter.cpp | 4 +-- src/theory/arith/arith_rewriter.h | 4 +-- src/theory/arith/arith_state.cpp | 4 +-- src/theory/arith/arith_state.h | 4 +-- src/theory/arith/arith_static_learner.cpp | 2 +- src/theory/arith/arith_static_learner.h | 2 +- src/theory/arith/arith_utilities.cpp | 2 +- src/theory/arith/arith_utilities.h | 2 +- src/theory/arith/arithvar.cpp | 2 +- src/theory/arith/arithvar.h | 2 +- src/theory/arith/arithvar_node_map.h | 4 +-- src/theory/arith/attempt_solution_simplex.cpp | 4 +-- src/theory/arith/attempt_solution_simplex.h | 4 +-- src/theory/arith/bound_counts.h | 2 +- src/theory/arith/bound_inference.cpp | 4 +-- src/theory/arith/bound_inference.h | 4 +-- src/theory/arith/branch_and_bound.cpp | 4 +-- src/theory/arith/branch_and_bound.h | 4 +-- src/theory/arith/callbacks.cpp | 4 +-- src/theory/arith/callbacks.h | 2 +- src/theory/arith/congruence_manager.cpp | 2 +- src/theory/arith/congruence_manager.h | 2 +- src/theory/arith/constraint.cpp | 4 +-- src/theory/arith/constraint.h | 4 +-- src/theory/arith/constraint_forward.h | 4 +-- src/theory/arith/cut_log.cpp | 4 +-- src/theory/arith/cut_log.h | 2 +- src/theory/arith/delta_rational.cpp | 2 +- src/theory/arith/delta_rational.h | 4 +-- src/theory/arith/dio_solver.cpp | 4 +-- src/theory/arith/dio_solver.h | 4 +-- src/theory/arith/dual_simplex.cpp | 4 +-- src/theory/arith/dual_simplex.h | 4 +-- src/theory/arith/equality_solver.cpp | 4 +-- src/theory/arith/equality_solver.h | 4 +-- src/theory/arith/error_set.cpp | 4 +-- src/theory/arith/error_set.h | 4 +-- src/theory/arith/fc_simplex.cpp | 4 +-- src/theory/arith/fc_simplex.h | 4 +-- src/theory/arith/infer_bounds.cpp | 4 +-- src/theory/arith/infer_bounds.h | 4 +-- src/theory/arith/inference_manager.cpp | 4 +-- src/theory/arith/inference_manager.h | 4 +-- src/theory/arith/linear_equality.cpp | 4 +-- src/theory/arith/linear_equality.h | 4 +-- src/theory/arith/matrix.cpp | 2 +- src/theory/arith/matrix.h | 4 +-- src/theory/arith/nl/coverings/cdcac.cpp | 4 +-- src/theory/arith/nl/coverings/cdcac.h | 4 +-- src/theory/arith/nl/coverings/cdcac_utils.cpp | 4 +-- src/theory/arith/nl/coverings/cdcac_utils.h | 4 +-- .../arith/nl/coverings/cocoa_converter.cpp | 2 +- .../arith/nl/coverings/cocoa_converter.h | 2 +- src/theory/arith/nl/coverings/constraints.cpp | 4 +-- src/theory/arith/nl/coverings/constraints.h | 4 +-- .../arith/nl/coverings/lazard_evaluation.cpp | 17 ++++++++++++ .../arith/nl/coverings/lazard_evaluation.h | 4 +-- src/theory/arith/nl/coverings/projections.cpp | 4 +-- src/theory/arith/nl/coverings/projections.h | 4 +-- .../arith/nl/coverings/proof_checker.cpp | 4 +-- src/theory/arith/nl/coverings/proof_checker.h | 4 +-- .../arith/nl/coverings/proof_generator.cpp | 4 +-- .../arith/nl/coverings/proof_generator.h | 4 +-- .../arith/nl/coverings/variable_ordering.cpp | 4 +-- .../arith/nl/coverings/variable_ordering.h | 4 +-- src/theory/arith/nl/coverings_solver.cpp | 4 +-- src/theory/arith/nl/coverings_solver.h | 4 +-- src/theory/arith/nl/equality_substitution.cpp | 4 +-- src/theory/arith/nl/equality_substitution.h | 2 +- src/theory/arith/nl/ext/constraint.cpp | 4 +-- src/theory/arith/nl/ext/constraint.h | 4 +-- src/theory/arith/nl/ext/ext_state.cpp | 4 +-- src/theory/arith/nl/ext/ext_state.h | 2 +- src/theory/arith/nl/ext/factoring_check.cpp | 2 +- src/theory/arith/nl/ext/factoring_check.h | 4 +-- src/theory/arith/nl/ext/monomial.cpp | 2 +- src/theory/arith/nl/ext/monomial.h | 4 +-- .../arith/nl/ext/monomial_bounds_check.cpp | 2 +- .../arith/nl/ext/monomial_bounds_check.h | 2 +- src/theory/arith/nl/ext/monomial_check.cpp | 2 +- src/theory/arith/nl/ext/monomial_check.h | 2 +- src/theory/arith/nl/ext/proof_checker.cpp | 4 +-- src/theory/arith/nl/ext/proof_checker.h | 4 +-- src/theory/arith/nl/ext/split_zero_check.cpp | 4 +-- src/theory/arith/nl/ext/split_zero_check.h | 4 +-- .../arith/nl/ext/tangent_plane_check.cpp | 4 +-- src/theory/arith/nl/ext/tangent_plane_check.h | 4 +-- src/theory/arith/nl/ext_theory_callback.cpp | 4 +-- src/theory/arith/nl/ext_theory_callback.h | 4 +-- src/theory/arith/nl/iand_solver.cpp | 2 +- src/theory/arith/nl/iand_solver.h | 4 +-- src/theory/arith/nl/iand_utils.cpp | 2 +- src/theory/arith/nl/iand_utils.h | 2 +- src/theory/arith/nl/icp/candidate.cpp | 4 +-- src/theory/arith/nl/icp/candidate.h | 4 +-- .../arith/nl/icp/contraction_origins.cpp | 2 +- src/theory/arith/nl/icp/contraction_origins.h | 4 +-- src/theory/arith/nl/icp/icp_solver.cpp | 4 +-- src/theory/arith/nl/icp/icp_solver.h | 4 +-- src/theory/arith/nl/icp/intersection.cpp | 4 +-- src/theory/arith/nl/icp/intersection.h | 4 +-- src/theory/arith/nl/icp/interval.h | 4 +-- src/theory/arith/nl/nl_lemma_utils.cpp | 4 +-- src/theory/arith/nl/nl_lemma_utils.h | 4 +-- src/theory/arith/nl/nl_model.cpp | 4 +-- src/theory/arith/nl/nl_model.h | 4 +-- src/theory/arith/nl/nonlinear_extension.cpp | 2 +- src/theory/arith/nl/nonlinear_extension.h | 2 +- src/theory/arith/nl/poly_conversion.cpp | 4 +-- src/theory/arith/nl/poly_conversion.h | 4 +-- src/theory/arith/nl/pow2_solver.cpp | 4 +-- src/theory/arith/nl/pow2_solver.h | 4 +-- src/theory/arith/nl/stats.cpp | 2 +- src/theory/arith/nl/stats.h | 4 +-- src/theory/arith/nl/strategy.cpp | 4 +-- src/theory/arith/nl/strategy.h | 4 +-- .../nl/transcendental/exponential_solver.cpp | 2 +- .../nl/transcendental/exponential_solver.h | 4 +-- .../arith/nl/transcendental/proof_checker.cpp | 4 +-- .../arith/nl/transcendental/proof_checker.h | 4 +-- .../arith/nl/transcendental/sine_solver.cpp | 2 +- .../arith/nl/transcendental/sine_solver.h | 4 +-- .../nl/transcendental/taylor_generator.cpp | 4 +-- .../nl/transcendental/taylor_generator.h | 4 +-- .../transcendental/transcendental_solver.cpp | 4 +-- .../nl/transcendental/transcendental_solver.h | 4 +-- .../transcendental/transcendental_state.cpp | 4 +-- .../nl/transcendental/transcendental_state.h | 4 +-- src/theory/arith/normal_form.cpp | 2 +- src/theory/arith/normal_form.h | 4 +-- src/theory/arith/operator_elim.cpp | 4 +-- src/theory/arith/operator_elim.h | 2 +- src/theory/arith/partial_model.cpp | 4 +-- src/theory/arith/partial_model.h | 4 +-- src/theory/arith/pp_rewrite_eq.cpp | 4 +-- src/theory/arith/pp_rewrite_eq.h | 4 +-- src/theory/arith/proof_checker.cpp | 4 +-- src/theory/arith/proof_checker.h | 4 +-- src/theory/arith/rewriter/addition.cpp | 2 +- src/theory/arith/rewriter/addition.h | 2 +- src/theory/arith/rewriter/node_utils.cpp | 2 +- src/theory/arith/rewriter/node_utils.h | 2 +- src/theory/arith/rewriter/ordering.h | 2 +- src/theory/arith/rewriter/rewrite_atom.cpp | 2 +- src/theory/arith/rewriter/rewrite_atom.h | 2 +- src/theory/arith/rewrites.cpp | 2 +- src/theory/arith/rewrites.h | 4 +-- src/theory/arith/simplex.cpp | 4 +-- src/theory/arith/simplex.h | 2 +- src/theory/arith/simplex_update.cpp | 4 +-- src/theory/arith/simplex_update.h | 4 +-- src/theory/arith/soi_simplex.cpp | 4 +-- src/theory/arith/soi_simplex.h | 4 +-- src/theory/arith/tableau.cpp | 4 +-- src/theory/arith/tableau.h | 4 +-- src/theory/arith/tableau_sizes.cpp | 2 +- src/theory/arith/tableau_sizes.h | 2 +- src/theory/arith/theory_arith.cpp | 4 +-- src/theory/arith/theory_arith.h | 4 +-- src/theory/arith/theory_arith_private.cpp | 4 +-- src/theory/arith/theory_arith_private.h | 4 +-- src/theory/arith/theory_arith_type_rules.cpp | 4 +-- src/theory/arith/theory_arith_type_rules.h | 4 +-- src/theory/arith/type_enumerator.h | 2 +- src/theory/arrays/array_info.cpp | 4 +-- src/theory/arrays/array_info.h | 4 +-- src/theory/arrays/inference_manager.cpp | 4 +-- src/theory/arrays/inference_manager.h | 4 +-- src/theory/arrays/proof_checker.cpp | 4 +-- src/theory/arrays/proof_checker.h | 4 +-- src/theory/arrays/skolem_cache.cpp | 4 +-- src/theory/arrays/skolem_cache.h | 4 +-- src/theory/arrays/theory_arrays.cpp | 2 +- src/theory/arrays/theory_arrays.h | 2 +- src/theory/arrays/theory_arrays_rewriter.cpp | 4 +-- src/theory/arrays/theory_arrays_rewriter.h | 4 +-- .../arrays/theory_arrays_type_rules.cpp | 4 +-- src/theory/arrays/theory_arrays_type_rules.h | 4 +-- src/theory/arrays/type_enumerator.cpp | 2 +- src/theory/arrays/type_enumerator.h | 4 +-- src/theory/arrays/union_find.cpp | 4 +-- src/theory/arrays/union_find.h | 4 +-- src/theory/assertion.cpp | 2 +- src/theory/assertion.h | 4 +-- src/theory/atom_requests.cpp | 4 +-- src/theory/atom_requests.h | 4 +-- src/theory/bags/bag_make_op.cpp | 4 +-- src/theory/bags/bag_make_op.h | 4 +-- src/theory/bags/bag_reduction.cpp | 4 +-- src/theory/bags/bag_reduction.h | 2 +- src/theory/bags/bag_solver.cpp | 4 +-- src/theory/bags/bag_solver.h | 4 +-- src/theory/bags/bags_rewriter.cpp | 4 +-- src/theory/bags/bags_rewriter.h | 4 +-- src/theory/bags/bags_statistics.cpp | 4 +-- src/theory/bags/bags_statistics.h | 4 +-- src/theory/bags/bags_utils.cpp | 4 +-- src/theory/bags/bags_utils.h | 2 +- src/theory/bags/card_solver.cpp | 4 +-- src/theory/bags/card_solver.h | 4 +-- src/theory/bags/infer_info.cpp | 4 +-- src/theory/bags/infer_info.h | 4 +-- src/theory/bags/inference_generator.cpp | 4 +-- src/theory/bags/inference_generator.h | 4 +-- src/theory/bags/inference_manager.cpp | 4 +-- src/theory/bags/inference_manager.h | 4 +-- src/theory/bags/rewrites.cpp | 2 +- src/theory/bags/rewrites.h | 4 +-- src/theory/bags/solver_state.cpp | 4 +-- src/theory/bags/solver_state.h | 4 +-- src/theory/bags/strategy.cpp | 4 +-- src/theory/bags/strategy.h | 4 +-- src/theory/bags/term_registry.cpp | 4 +-- src/theory/bags/term_registry.h | 4 +-- src/theory/bags/theory_bags.cpp | 4 +-- src/theory/bags/theory_bags.h | 4 +-- .../bags/theory_bags_type_enumerator.cpp | 4 +-- src/theory/bags/theory_bags_type_enumerator.h | 4 +-- src/theory/bags/theory_bags_type_rules.cpp | 4 +-- src/theory/bags/theory_bags_type_rules.h | 4 +-- src/theory/booleans/circuit_propagator.cpp | 2 +- src/theory/booleans/circuit_propagator.h | 4 +-- src/theory/booleans/proof_checker.cpp | 2 +- src/theory/booleans/proof_checker.h | 4 +-- .../booleans/proof_circuit_propagator.cpp | 4 +-- .../booleans/proof_circuit_propagator.h | 4 +-- src/theory/booleans/theory_bool.cpp | 2 +- src/theory/booleans/theory_bool.h | 4 +-- src/theory/booleans/theory_bool_rewriter.cpp | 2 +- src/theory/booleans/theory_bool_rewriter.h | 4 +-- .../booleans/theory_bool_type_rules.cpp | 4 +-- src/theory/booleans/theory_bool_type_rules.h | 4 +-- src/theory/booleans/type_enumerator.h | 4 +-- src/theory/builtin/proof_checker.cpp | 4 +-- src/theory/builtin/proof_checker.h | 4 +-- src/theory/builtin/theory_builtin.cpp | 4 +-- src/theory/builtin/theory_builtin.h | 4 +-- .../builtin/theory_builtin_rewriter.cpp | 4 +-- src/theory/builtin/theory_builtin_rewriter.h | 9 +++---- .../builtin/theory_builtin_type_rules.cpp | 4 +-- .../builtin/theory_builtin_type_rules.h | 4 +-- src/theory/builtin/type_enumerator.cpp | 4 +-- src/theory/builtin/type_enumerator.h | 4 +-- .../bv/bitblast/bitblast_proof_generator.cpp | 2 +- .../bv/bitblast/bitblast_proof_generator.h | 4 +-- .../bitblast/bitblast_strategies_template.h | 4 +-- src/theory/bv/bitblast/bitblast_utils.h | 4 +-- src/theory/bv/bitblast/bitblaster.h | 2 +- src/theory/bv/bitblast/node_bitblaster.cpp | 2 +- src/theory/bv/bitblast/node_bitblaster.h | 2 +- src/theory/bv/bitblast/proof_bitblaster.cpp | 4 +-- src/theory/bv/bitblast/proof_bitblaster.h | 4 +-- src/theory/bv/bv_solver.h | 4 +-- src/theory/bv/bv_solver_bitblast.cpp | 4 +-- src/theory/bv/bv_solver_bitblast.h | 4 +-- src/theory/bv/bv_solver_bitblast_internal.cpp | 4 +-- src/theory/bv/bv_solver_bitblast_internal.h | 2 +- src/theory/bv/int_blaster.cpp | 4 +-- src/theory/bv/int_blaster.h | 4 +-- src/theory/bv/proof_checker.cpp | 4 +-- src/theory/bv/proof_checker.h | 4 +-- src/theory/bv/theory_bv.cpp | 4 +-- src/theory/bv/theory_bv.h | 4 +-- src/theory/bv/theory_bv_rewrite_rules.h | 7 ++--- ...ory_bv_rewrite_rules_constant_evaluation.h | 6 ++--- src/theory/bv/theory_bv_rewrite_rules_core.h | 7 ++--- .../theory_bv_rewrite_rules_normalization.h | 6 ++--- ...ry_bv_rewrite_rules_operator_elimination.h | 9 +++---- .../theory_bv_rewrite_rules_simplification.h | 7 ++--- src/theory/bv/theory_bv_rewriter.cpp | 9 +++---- src/theory/bv/theory_bv_rewriter.h | 9 +++---- src/theory/bv/theory_bv_type_rules.cpp | 2 +- src/theory/bv/theory_bv_type_rules.h | 4 +-- src/theory/bv/theory_bv_utils.cpp | 2 +- src/theory/bv/theory_bv_utils.h | 4 +-- src/theory/bv/type_enumerator.h | 4 +-- src/theory/care_graph.h | 2 +- src/theory/care_pair_argument_callback.cpp | 2 +- src/theory/care_pair_argument_callback.h | 2 +- src/theory/combination_care_graph.cpp | 2 +- src/theory/combination_care_graph.h | 4 +-- src/theory/combination_engine.cpp | 4 +-- src/theory/combination_engine.h | 4 +-- src/theory/datatypes/datatypes_rewriter.cpp | 2 +- src/theory/datatypes/datatypes_rewriter.h | 4 +-- src/theory/datatypes/infer_proof_cons.cpp | 4 +-- src/theory/datatypes/infer_proof_cons.h | 4 +-- src/theory/datatypes/inference.cpp | 4 +-- src/theory/datatypes/inference.h | 4 +-- src/theory/datatypes/inference_manager.cpp | 4 +-- src/theory/datatypes/inference_manager.h | 4 +-- src/theory/datatypes/proof_checker.cpp | 4 +-- src/theory/datatypes/proof_checker.h | 4 +-- src/theory/datatypes/sygus_datatype_utils.cpp | 4 +-- src/theory/datatypes/sygus_datatype_utils.h | 4 +-- src/theory/datatypes/sygus_extension.cpp | 4 +-- src/theory/datatypes/sygus_extension.h | 4 +-- src/theory/datatypes/sygus_simple_sym.cpp | 4 +-- src/theory/datatypes/sygus_simple_sym.h | 4 +-- src/theory/datatypes/theory_datatypes.cpp | 4 +-- src/theory/datatypes/theory_datatypes.h | 2 +- .../datatypes/theory_datatypes_type_rules.cpp | 4 +-- .../datatypes/theory_datatypes_type_rules.h | 4 +-- .../datatypes/theory_datatypes_utils.cpp | 4 +-- src/theory/datatypes/theory_datatypes_utils.h | 2 +- src/theory/datatypes/tuple_project_op.cpp | 2 +- src/theory/datatypes/tuple_project_op.h | 4 +-- src/theory/datatypes/tuple_utils.cpp | 4 +-- src/theory/datatypes/tuple_utils.h | 4 +-- src/theory/datatypes/type_enumerator.cpp | 4 +-- src/theory/datatypes/type_enumerator.h | 2 +- src/theory/decision_manager.cpp | 4 +-- src/theory/decision_manager.h | 4 +-- src/theory/decision_strategy.cpp | 4 +-- src/theory/decision_strategy.h | 4 +-- src/theory/difficulty_manager.cpp | 4 +-- src/theory/difficulty_manager.h | 2 +- src/theory/ee_manager.cpp | 2 +- src/theory/ee_manager.h | 4 +-- src/theory/ee_manager_central.cpp | 2 +- src/theory/ee_manager_central.h | 2 +- src/theory/ee_manager_distributed.cpp | 2 +- src/theory/ee_manager_distributed.h | 4 +-- src/theory/ee_setup_info.h | 4 +-- src/theory/engine_output_channel.cpp | 4 +-- src/theory/engine_output_channel.h | 4 +-- src/theory/evaluator.cpp | 4 +-- src/theory/evaluator.h | 2 +- src/theory/ext_theory.cpp | 4 +-- src/theory/ext_theory.h | 4 +-- src/theory/fp/fp_expand_defs.cpp | 4 +-- src/theory/fp/fp_expand_defs.h | 4 +-- src/theory/fp/fp_word_blaster.cpp | 4 +-- src/theory/fp/fp_word_blaster.h | 4 +-- src/theory/fp/theory_fp.cpp | 4 +-- src/theory/fp/theory_fp.h | 4 +-- src/theory/fp/theory_fp_rewriter.cpp | 4 +-- src/theory/fp/theory_fp_rewriter.h | 4 +-- src/theory/fp/theory_fp_type_rules.cpp | 2 +- src/theory/fp/theory_fp_type_rules.h | 4 +-- src/theory/fp/type_enumerator.h | 4 +-- src/theory/incomplete_id.cpp | 4 +-- src/theory/incomplete_id.h | 4 +-- src/theory/inference_id.cpp | 4 +-- src/theory/inference_id.h | 2 +- src/theory/inference_id_proof_annotator.cpp | 2 +- src/theory/inference_id_proof_annotator.h | 2 +- src/theory/inference_manager_buffered.cpp | 4 +-- src/theory/inference_manager_buffered.h | 4 +-- src/theory/interrupted.h | 4 +-- src/theory/logic_info.cpp | 4 +-- src/theory/logic_info.h | 2 +- src/theory/mkrewriter | 2 +- src/theory/mktheorytraits | 2 +- src/theory/model_manager.cpp | 4 +-- src/theory/model_manager.h | 4 +-- src/theory/model_manager_distributed.cpp | 4 +-- src/theory/model_manager_distributed.h | 4 +-- src/theory/output_channel.cpp | 2 +- src/theory/output_channel.h | 2 +- src/theory/quantifiers/alpha_equivalence.cpp | 4 +-- src/theory/quantifiers/alpha_equivalence.h | 4 +-- src/theory/quantifiers/bv_inverter.cpp | 2 +- src/theory/quantifiers/bv_inverter.h | 4 +-- src/theory/quantifiers/bv_inverter_utils.cpp | 2 +- src/theory/quantifiers/bv_inverter_utils.h | 4 +-- .../candidate_rewrite_database.cpp | 4 +-- .../quantifiers/candidate_rewrite_database.h | 4 +-- .../quantifiers/candidate_rewrite_filter.cpp | 4 +-- .../quantifiers/candidate_rewrite_filter.h | 4 +-- .../cegqi/ceg_arith_instantiator.cpp | 4 +-- .../cegqi/ceg_arith_instantiator.h | 4 +-- .../quantifiers/cegqi/ceg_bv_instantiator.cpp | 4 +-- .../quantifiers/cegqi/ceg_bv_instantiator.h | 2 +- .../cegqi/ceg_bv_instantiator_utils.cpp | 4 +-- .../cegqi/ceg_bv_instantiator_utils.h | 2 +- .../quantifiers/cegqi/ceg_dt_instantiator.cpp | 4 +-- .../quantifiers/cegqi/ceg_dt_instantiator.h | 4 +-- .../quantifiers/cegqi/ceg_instantiator.cpp | 4 +-- .../quantifiers/cegqi/ceg_instantiator.h | 4 +-- .../quantifiers/cegqi/inst_strategy_cegqi.cpp | 4 +-- .../quantifiers/cegqi/inst_strategy_cegqi.h | 4 +-- src/theory/quantifiers/cegqi/nested_qe.cpp | 4 +-- src/theory/quantifiers/cegqi/nested_qe.h | 4 +-- .../quantifiers/cegqi/vts_term_cache.cpp | 4 +-- src/theory/quantifiers/cegqi/vts_term_cache.h | 4 +-- .../quantifiers/conjecture_generator.cpp | 4 +-- src/theory/quantifiers/conjecture_generator.h | 2 +- src/theory/quantifiers/dynamic_rewrite.cpp | 4 +-- src/theory/quantifiers/dynamic_rewrite.h | 4 +-- .../ematching/candidate_generator.cpp | 4 +-- .../ematching/candidate_generator.h | 2 +- .../quantifiers/ematching/ho_trigger.cpp | 4 +-- src/theory/quantifiers/ematching/ho_trigger.h | 4 +-- .../quantifiers/ematching/im_generator.cpp | 4 +-- .../quantifiers/ematching/im_generator.h | 4 +-- .../ematching/inst_match_generator.cpp | 4 +-- .../ematching/inst_match_generator.h | 4 +-- .../ematching/inst_match_generator_multi.cpp | 2 +- .../ematching/inst_match_generator_multi.h | 4 +-- .../inst_match_generator_multi_linear.cpp | 4 +-- .../inst_match_generator_multi_linear.h | 4 +-- .../ematching/inst_match_generator_simple.cpp | 4 +-- .../ematching/inst_match_generator_simple.h | 4 +-- .../quantifiers/ematching/inst_strategy.cpp | 4 +-- .../quantifiers/ematching/inst_strategy.h | 4 +-- .../ematching/inst_strategy_e_matching.cpp | 4 +-- .../ematching/inst_strategy_e_matching.h | 2 +- .../inst_strategy_e_matching_user.cpp | 4 +-- .../ematching/inst_strategy_e_matching_user.h | 4 +-- .../ematching/instantiation_engine.cpp | 4 +-- .../ematching/instantiation_engine.h | 4 +-- .../ematching/pattern_term_selector.cpp | 2 +- .../ematching/pattern_term_selector.h | 4 +-- .../ematching/relational_match_generator.cpp | 4 +-- .../ematching/relational_match_generator.h | 2 +- src/theory/quantifiers/ematching/trigger.cpp | 4 +-- src/theory/quantifiers/ematching/trigger.h | 4 +-- .../ematching/trigger_database.cpp | 4 +-- .../quantifiers/ematching/trigger_database.h | 2 +- .../ematching/trigger_term_info.cpp | 4 +-- .../quantifiers/ematching/trigger_term_info.h | 4 +-- .../quantifiers/ematching/trigger_trie.cpp | 4 +-- .../quantifiers/ematching/trigger_trie.h | 4 +-- .../ematching/var_match_generator.cpp | 4 +-- .../ematching/var_match_generator.h | 4 +-- src/theory/quantifiers/entailment_check.cpp | 4 +-- src/theory/quantifiers/entailment_check.h | 2 +- src/theory/quantifiers/equality_query.cpp | 4 +-- src/theory/quantifiers/equality_query.h | 4 +-- src/theory/quantifiers/expr_miner.cpp | 4 +-- src/theory/quantifiers/expr_miner.h | 4 +-- src/theory/quantifiers/expr_miner_manager.cpp | 2 +- src/theory/quantifiers/expr_miner_manager.h | 4 +-- src/theory/quantifiers/extended_rewrite.cpp | 4 +-- src/theory/quantifiers/extended_rewrite.h | 4 +-- src/theory/quantifiers/first_order_model.cpp | 4 +-- src/theory/quantifiers/first_order_model.h | 4 +-- .../quantifiers/fmf/bounded_integers.cpp | 4 +-- src/theory/quantifiers/fmf/bounded_integers.h | 4 +-- .../quantifiers/fmf/first_order_model_fmc.cpp | 4 +-- .../quantifiers/fmf/first_order_model_fmc.h | 4 +-- .../quantifiers/fmf/full_model_check.cpp | 2 +- src/theory/quantifiers/fmf/full_model_check.h | 2 +- src/theory/quantifiers/fmf/model_builder.cpp | 4 +-- src/theory/quantifiers/fmf/model_builder.h | 4 +-- src/theory/quantifiers/fmf/model_engine.cpp | 4 +-- src/theory/quantifiers/fmf/model_engine.h | 4 +-- src/theory/quantifiers/fun_def_evaluator.cpp | 2 +- src/theory/quantifiers/fun_def_evaluator.h | 4 +-- src/theory/quantifiers/ho_term_database.cpp | 4 +-- src/theory/quantifiers/ho_term_database.h | 4 +-- src/theory/quantifiers/index_trie.cpp | 4 +-- src/theory/quantifiers/index_trie.h | 4 +-- src/theory/quantifiers/inst_match.cpp | 4 +-- src/theory/quantifiers/inst_match.h | 4 +-- src/theory/quantifiers/inst_match_trie.cpp | 4 +-- src/theory/quantifiers/inst_match_trie.h | 4 +-- .../quantifiers/inst_strategy_enumerative.cpp | 4 +-- .../quantifiers/inst_strategy_enumerative.h | 4 +-- src/theory/quantifiers/inst_strategy_pool.cpp | 4 +-- src/theory/quantifiers/inst_strategy_pool.h | 4 +-- src/theory/quantifiers/instantiate.cpp | 4 +-- src/theory/quantifiers/instantiate.h | 4 +-- src/theory/quantifiers/instantiation_list.cpp | 4 +-- src/theory/quantifiers/instantiation_list.h | 4 +-- src/theory/quantifiers/lazy_trie.cpp | 4 +-- src/theory/quantifiers/lazy_trie.h | 4 +-- src/theory/quantifiers/master_eq_notify.cpp | 2 +- src/theory/quantifiers/master_eq_notify.h | 2 +- src/theory/quantifiers/proof_checker.cpp | 4 +-- src/theory/quantifiers/proof_checker.h | 4 +-- .../quantifiers/quant_bound_inference.cpp | 4 +-- .../quantifiers/quant_bound_inference.h | 4 +-- .../quantifiers/quant_conflict_find.cpp | 4 +-- src/theory/quantifiers/quant_conflict_find.h | 4 +-- src/theory/quantifiers/quant_module.cpp | 4 +-- src/theory/quantifiers/quant_module.h | 4 +-- src/theory/quantifiers/quant_relevance.cpp | 4 +-- src/theory/quantifiers/quant_relevance.h | 2 +- .../quantifiers/quant_rep_bound_ext.cpp | 4 +-- src/theory/quantifiers/quant_rep_bound_ext.h | 4 +-- src/theory/quantifiers/quant_split.cpp | 4 +-- src/theory/quantifiers/quant_split.h | 4 +-- src/theory/quantifiers/quant_util.cpp | 4 +-- src/theory/quantifiers/quant_util.h | 4 +-- .../quantifiers/quantifiers_attributes.cpp | 2 +- .../quantifiers/quantifiers_attributes.h | 4 +-- .../quantifiers_inference_manager.cpp | 4 +-- .../quantifiers_inference_manager.h | 4 +-- src/theory/quantifiers/quantifiers_macros.cpp | 4 +-- src/theory/quantifiers/quantifiers_macros.h | 4 +-- .../quantifiers/quantifiers_modules.cpp | 4 +-- src/theory/quantifiers/quantifiers_modules.h | 4 +-- .../quantifiers/quantifiers_preprocess.cpp | 4 +-- .../quantifiers/quantifiers_preprocess.h | 4 +-- .../quantifiers/quantifiers_registry.cpp | 4 +-- src/theory/quantifiers/quantifiers_registry.h | 4 +-- .../quantifiers/quantifiers_rewriter.cpp | 2 +- src/theory/quantifiers/quantifiers_rewriter.h | 2 +- src/theory/quantifiers/quantifiers_state.cpp | 4 +-- src/theory/quantifiers/quantifiers_state.h | 4 +-- .../quantifiers/quantifiers_statistics.cpp | 4 +-- .../quantifiers/quantifiers_statistics.h | 4 +-- src/theory/quantifiers/query_generator.cpp | 2 +- src/theory/quantifiers/query_generator.h | 4 +-- .../query_generator_sample_sat.cpp | 4 +-- .../quantifiers/query_generator_sample_sat.h | 4 +-- .../quantifiers/query_generator_unsat.cpp | 2 +- .../quantifiers/query_generator_unsat.h | 2 +- src/theory/quantifiers/relevant_domain.cpp | 4 +-- src/theory/quantifiers/relevant_domain.h | 4 +-- .../quantifiers/single_inv_partition.cpp | 4 +-- src/theory/quantifiers/single_inv_partition.h | 4 +-- src/theory/quantifiers/skolemize.cpp | 2 +- src/theory/quantifiers/skolemize.h | 4 +-- src/theory/quantifiers/solution_filter.cpp | 4 +-- src/theory/quantifiers/solution_filter.h | 4 +-- .../sygus/ce_guided_single_inv.cpp | 4 +-- .../quantifiers/sygus/ce_guided_single_inv.h | 4 +-- src/theory/quantifiers/sygus/cegis.cpp | 4 +-- src/theory/quantifiers/sygus/cegis.h | 2 +- .../sygus/cegis_core_connective.cpp | 2 +- .../quantifiers/sygus/cegis_core_connective.h | 4 +-- src/theory/quantifiers/sygus/cegis_unif.cpp | 4 +-- src/theory/quantifiers/sygus/cegis_unif.h | 2 +- .../sygus/enum_stream_substitution.cpp | 2 +- .../sygus/enum_stream_substitution.h | 2 +- .../quantifiers/sygus/enum_val_generator.h | 2 +- .../quantifiers/sygus/enum_value_manager.cpp | 4 +-- .../quantifiers/sygus/enum_value_manager.h | 2 +- .../quantifiers/sygus/example_eval_cache.cpp | 4 +-- .../quantifiers/sygus/example_eval_cache.h | 4 +-- .../quantifiers/sygus/example_infer.cpp | 4 +-- src/theory/quantifiers/sygus/example_infer.h | 4 +-- .../quantifiers/sygus/example_min_eval.cpp | 4 +-- .../quantifiers/sygus/example_min_eval.h | 4 +-- .../quantifiers/sygus/rcons_obligation.cpp | 2 +- .../quantifiers/sygus/rcons_obligation.h | 4 +-- .../quantifiers/sygus/rcons_type_info.cpp | 2 +- .../quantifiers/sygus/rcons_type_info.h | 4 +-- src/theory/quantifiers/sygus/sygus_abduct.cpp | 4 +-- src/theory/quantifiers/sygus/sygus_abduct.h | 4 +-- .../quantifiers/sygus/sygus_enumerator.cpp | 4 +-- .../quantifiers/sygus/sygus_enumerator.h | 4 +-- .../sygus/sygus_enumerator_callback.cpp | 4 +-- .../sygus/sygus_enumerator_callback.h | 4 +-- .../quantifiers/sygus/sygus_eval_unfold.cpp | 4 +-- .../quantifiers/sygus/sygus_eval_unfold.h | 4 +-- .../quantifiers/sygus/sygus_explain.cpp | 4 +-- src/theory/quantifiers/sygus/sygus_explain.h | 4 +-- .../quantifiers/sygus/sygus_grammar_cons.cpp | 2 +- .../quantifiers/sygus/sygus_grammar_cons.h | 4 +-- .../quantifiers/sygus/sygus_grammar_norm.cpp | 4 +-- .../quantifiers/sygus/sygus_grammar_norm.h | 2 +- .../quantifiers/sygus/sygus_grammar_red.cpp | 4 +-- .../quantifiers/sygus/sygus_grammar_red.h | 4 +-- .../quantifiers/sygus/sygus_interpol.cpp | 4 +-- src/theory/quantifiers/sygus/sygus_interpol.h | 4 +-- .../quantifiers/sygus/sygus_invariance.cpp | 4 +-- .../quantifiers/sygus/sygus_invariance.h | 4 +-- src/theory/quantifiers/sygus/sygus_module.cpp | 4 +-- src/theory/quantifiers/sygus/sygus_module.h | 4 +-- src/theory/quantifiers/sygus/sygus_pbe.cpp | 4 +-- src/theory/quantifiers/sygus/sygus_pbe.h | 4 +-- .../quantifiers/sygus/sygus_process_conj.cpp | 4 +-- .../quantifiers/sygus/sygus_process_conj.h | 4 +-- .../quantifiers/sygus/sygus_qe_preproc.cpp | 4 +-- .../quantifiers/sygus/sygus_qe_preproc.h | 4 +-- .../sygus/sygus_random_enumerator.cpp | 2 +- .../sygus/sygus_random_enumerator.h | 2 +- .../quantifiers/sygus/sygus_reconstruct.cpp | 4 +-- .../quantifiers/sygus/sygus_reconstruct.h | 4 +-- .../quantifiers/sygus/sygus_repair_const.cpp | 4 +-- .../quantifiers/sygus/sygus_repair_const.h | 4 +-- src/theory/quantifiers/sygus/sygus_stats.cpp | 4 +-- src/theory/quantifiers/sygus/sygus_stats.h | 4 +-- src/theory/quantifiers/sygus/sygus_unif.cpp | 4 +-- src/theory/quantifiers/sygus/sygus_unif.h | 4 +-- .../quantifiers/sygus/sygus_unif_io.cpp | 4 +-- src/theory/quantifiers/sygus/sygus_unif_io.h | 4 +-- .../quantifiers/sygus/sygus_unif_rl.cpp | 2 +- src/theory/quantifiers/sygus/sygus_unif_rl.h | 2 +- .../quantifiers/sygus/sygus_unif_strat.cpp | 2 +- .../quantifiers/sygus/sygus_unif_strat.h | 4 +-- src/theory/quantifiers/sygus/sygus_utils.cpp | 4 +-- src/theory/quantifiers/sygus/sygus_utils.h | 4 +-- .../quantifiers/sygus/synth_conjecture.cpp | 4 +-- .../quantifiers/sygus/synth_conjecture.h | 4 +-- src/theory/quantifiers/sygus/synth_engine.cpp | 2 +- src/theory/quantifiers/sygus/synth_engine.h | 4 +-- src/theory/quantifiers/sygus/synth_verify.cpp | 4 +-- src/theory/quantifiers/sygus/synth_verify.h | 2 +- .../quantifiers/sygus/template_infer.cpp | 4 +-- src/theory/quantifiers/sygus/template_infer.h | 4 +-- .../quantifiers/sygus/term_database_sygus.cpp | 2 +- .../quantifiers/sygus/term_database_sygus.h | 4 +-- .../sygus/transition_inference.cpp | 4 +-- .../quantifiers/sygus/transition_inference.h | 4 +-- src/theory/quantifiers/sygus/type_info.cpp | 4 +-- src/theory/quantifiers/sygus/type_info.h | 4 +-- .../quantifiers/sygus/type_node_id_trie.cpp | 4 +-- .../quantifiers/sygus/type_node_id_trie.h | 4 +-- src/theory/quantifiers/sygus_inst.cpp | 4 +-- src/theory/quantifiers/sygus_inst.h | 4 +-- src/theory/quantifiers/sygus_sampler.cpp | 4 +-- src/theory/quantifiers/sygus_sampler.h | 4 +-- src/theory/quantifiers/term_database.cpp | 4 +-- src/theory/quantifiers/term_database.h | 4 +-- src/theory/quantifiers/term_enumeration.cpp | 4 +-- src/theory/quantifiers/term_enumeration.h | 4 +-- src/theory/quantifiers/term_pools.cpp | 4 +-- src/theory/quantifiers/term_pools.h | 4 +-- src/theory/quantifiers/term_registry.cpp | 4 +-- src/theory/quantifiers/term_registry.h | 4 +-- .../quantifiers/term_tuple_enumerator.cpp | 4 +-- .../quantifiers/term_tuple_enumerator.h | 4 +-- src/theory/quantifiers/term_util.cpp | 4 +-- src/theory/quantifiers/term_util.h | 4 +-- src/theory/quantifiers/theory_quantifiers.cpp | 4 +-- src/theory/quantifiers/theory_quantifiers.h | 2 +- .../theory_quantifiers_type_rules.cpp | 4 +-- .../theory_quantifiers_type_rules.h | 4 +-- src/theory/quantifiers_engine.cpp | 4 +-- src/theory/quantifiers_engine.h | 2 +- src/theory/relevance_manager.cpp | 4 +-- src/theory/relevance_manager.h | 4 +-- src/theory/rep_set.cpp | 4 +-- src/theory/rep_set.h | 2 +- src/theory/rewriter.cpp | 4 +-- src/theory/rewriter.h | 4 +-- src/theory/rewriter_attributes.h | 2 +- src/theory/rewriter_tables_template.h | 4 +-- src/theory/sep/theory_sep.cpp | 4 +-- src/theory/sep/theory_sep.h | 2 +- src/theory/sep/theory_sep_rewriter.cpp | 6 ++--- src/theory/sep/theory_sep_rewriter.h | 9 +++---- src/theory/sep/theory_sep_type_rules.cpp | 4 +-- src/theory/sep/theory_sep_type_rules.h | 4 +-- src/theory/sets/cardinality_extension.cpp | 2 +- src/theory/sets/cardinality_extension.h | 4 +-- src/theory/sets/inference_manager.cpp | 4 +-- src/theory/sets/inference_manager.h | 4 +-- src/theory/sets/normal_form.h | 4 +-- src/theory/sets/rels_utils.cpp | 4 +-- src/theory/sets/rels_utils.h | 4 +-- src/theory/sets/singleton_op.cpp | 4 +-- src/theory/sets/singleton_op.h | 4 +-- src/theory/sets/skolem_cache.cpp | 4 +-- src/theory/sets/skolem_cache.h | 4 +-- src/theory/sets/solver_state.cpp | 4 +-- src/theory/sets/solver_state.h | 4 +-- src/theory/sets/term_registry.cpp | 4 +-- src/theory/sets/term_registry.h | 4 +-- src/theory/sets/theory_sets.cpp | 4 +-- src/theory/sets/theory_sets.h | 2 +- src/theory/sets/theory_sets_private.cpp | 2 +- src/theory/sets/theory_sets_private.h | 4 +-- src/theory/sets/theory_sets_rels.cpp | 4 +-- src/theory/sets/theory_sets_rels.h | 4 +-- src/theory/sets/theory_sets_rewriter.cpp | 4 +-- src/theory/sets/theory_sets_rewriter.h | 4 +-- .../sets/theory_sets_type_enumerator.cpp | 2 +- src/theory/sets/theory_sets_type_enumerator.h | 4 +-- src/theory/sets/theory_sets_type_rules.cpp | 4 +-- src/theory/sets/theory_sets_type_rules.h | 4 +-- src/theory/shared_solver.cpp | 2 +- src/theory/shared_solver.h | 2 +- src/theory/shared_solver_distributed.cpp | 2 +- src/theory/shared_solver_distributed.h | 4 +-- src/theory/shared_terms_database.cpp | 2 +- src/theory/shared_terms_database.h | 2 +- src/theory/skolem_lemma.cpp | 2 +- src/theory/skolem_lemma.h | 4 +-- src/theory/smt_engine_subsolver.cpp | 4 +-- src/theory/smt_engine_subsolver.h | 4 +-- src/theory/sort_inference.cpp | 2 +- src/theory/sort_inference.h | 4 +-- src/theory/strings/arith_entail.cpp | 2 +- src/theory/strings/arith_entail.h | 4 +-- src/theory/strings/array_core_solver.cpp | 4 +-- src/theory/strings/array_core_solver.h | 4 +-- src/theory/strings/array_solver.cpp | 4 +-- src/theory/strings/array_solver.h | 4 +-- src/theory/strings/base_solver.cpp | 2 +- src/theory/strings/base_solver.h | 4 +-- src/theory/strings/core_solver.cpp | 4 +-- src/theory/strings/core_solver.h | 2 +- src/theory/strings/eager_solver.cpp | 4 +-- src/theory/strings/eager_solver.h | 4 +-- src/theory/strings/eqc_info.cpp | 4 +-- src/theory/strings/eqc_info.h | 4 +-- src/theory/strings/extf_solver.cpp | 4 +-- src/theory/strings/extf_solver.h | 4 +-- src/theory/strings/infer_info.cpp | 2 +- src/theory/strings/infer_info.h | 4 +-- src/theory/strings/infer_proof_cons.cpp | 4 +-- src/theory/strings/infer_proof_cons.h | 4 +-- src/theory/strings/inference_manager.cpp | 2 +- src/theory/strings/inference_manager.h | 2 +- src/theory/strings/normal_form.cpp | 2 +- src/theory/strings/normal_form.h | 4 +-- src/theory/strings/proof_checker.cpp | 4 +-- src/theory/strings/proof_checker.h | 4 +-- src/theory/strings/regexp_elim.cpp | 4 +-- src/theory/strings/regexp_elim.h | 4 +-- src/theory/strings/regexp_entail.cpp | 4 +-- src/theory/strings/regexp_entail.h | 2 +- src/theory/strings/regexp_enumerator.cpp | 2 +- src/theory/strings/regexp_enumerator.h | 2 +- src/theory/strings/regexp_operation.cpp | 2 +- src/theory/strings/regexp_operation.h | 2 +- src/theory/strings/regexp_solver.cpp | 2 +- src/theory/strings/regexp_solver.h | 4 +-- src/theory/strings/rewrites.cpp | 2 +- src/theory/strings/rewrites.h | 4 +-- src/theory/strings/seq_unit_op.cpp | 2 +- src/theory/strings/seq_unit_op.h | 4 +-- src/theory/strings/sequences_rewriter.cpp | 2 +- src/theory/strings/sequences_rewriter.h | 2 +- src/theory/strings/sequences_stats.cpp | 4 +-- src/theory/strings/sequences_stats.h | 2 +- src/theory/strings/skolem_cache.cpp | 4 +-- src/theory/strings/skolem_cache.h | 4 +-- src/theory/strings/solver_state.cpp | 4 +-- src/theory/strings/solver_state.h | 4 +-- src/theory/strings/strategy.cpp | 4 +-- src/theory/strings/strategy.h | 4 +-- src/theory/strings/strings_entail.cpp | 2 +- src/theory/strings/strings_entail.h | 4 +-- src/theory/strings/strings_fmf.cpp | 4 +-- src/theory/strings/strings_fmf.h | 4 +-- src/theory/strings/strings_rewriter.cpp | 4 +-- src/theory/strings/strings_rewriter.h | 4 +-- src/theory/strings/term_registry.cpp | 2 +- src/theory/strings/term_registry.h | 4 +-- src/theory/strings/theory_strings.cpp | 4 +-- src/theory/strings/theory_strings.h | 4 +-- .../strings/theory_strings_preprocess.cpp | 2 +- .../strings/theory_strings_preprocess.h | 4 +-- .../strings/theory_strings_type_rules.cpp | 2 +- .../strings/theory_strings_type_rules.h | 4 +-- src/theory/strings/theory_strings_utils.cpp | 4 +-- src/theory/strings/theory_strings_utils.h | 4 +-- src/theory/strings/type_enumerator.cpp | 2 +- src/theory/strings/type_enumerator.h | 4 +-- src/theory/strings/word.cpp | 4 +-- src/theory/strings/word.h | 4 +-- src/theory/subs_minimize.cpp | 2 +- src/theory/subs_minimize.h | 4 +-- src/theory/substitutions.cpp | 4 +-- src/theory/substitutions.h | 4 +-- src/theory/term_registration_visitor.cpp | 4 +-- src/theory/term_registration_visitor.h | 4 +-- src/theory/theory.cpp | 4 +-- src/theory/theory.h | 2 +- src/theory/theory_engine.cpp | 2 +- src/theory/theory_engine.h | 2 +- src/theory/theory_engine_proof_generator.cpp | 4 +-- src/theory/theory_engine_proof_generator.h | 4 +-- src/theory/theory_eq_notify.h | 2 +- src/theory/theory_id.cpp | 4 +-- src/theory/theory_id.h | 2 +- src/theory/theory_inference.cpp | 4 +-- src/theory/theory_inference.h | 4 +-- src/theory/theory_inference_manager.cpp | 2 +- src/theory/theory_inference_manager.h | 2 +- src/theory/theory_model.cpp | 4 +-- src/theory/theory_model.h | 4 +-- src/theory/theory_model_builder.cpp | 4 +-- src/theory/theory_model_builder.h | 4 +-- src/theory/theory_preprocessor.cpp | 4 +-- src/theory/theory_preprocessor.h | 4 +-- src/theory/theory_rewriter.cpp | 4 +-- src/theory/theory_rewriter.h | 2 +- src/theory/theory_state.cpp | 4 +-- src/theory/theory_state.h | 2 +- src/theory/theory_traits_template.h | 4 +-- src/theory/trust_substitutions.cpp | 2 +- src/theory/trust_substitutions.h | 4 +-- src/theory/type_enumerator.h | 2 +- src/theory/type_enumerator_template.cpp | 4 +-- src/theory/type_set.cpp | 4 +-- src/theory/type_set.h | 4 +-- src/theory/uf/cardinality_extension.cpp | 2 +- src/theory/uf/cardinality_extension.h | 2 +- src/theory/uf/eq_proof.cpp | 4 +-- src/theory/uf/eq_proof.h | 4 +-- src/theory/uf/equality_engine.cpp | 2 +- src/theory/uf/equality_engine.h | 2 +- src/theory/uf/equality_engine_iterator.cpp | 2 +- src/theory/uf/equality_engine_iterator.h | 4 +-- src/theory/uf/equality_engine_notify.h | 2 +- src/theory/uf/equality_engine_types.h | 2 +- src/theory/uf/function_const.cpp | 4 +-- src/theory/uf/function_const.h | 4 +-- src/theory/uf/ho_extension.cpp | 4 +-- src/theory/uf/ho_extension.h | 4 +-- src/theory/uf/lambda_lift.cpp | 4 +-- src/theory/uf/lambda_lift.h | 2 +- src/theory/uf/proof_checker.cpp | 4 +-- src/theory/uf/proof_checker.h | 4 +-- src/theory/uf/proof_equality_engine.cpp | 4 +-- src/theory/uf/proof_equality_engine.h | 4 +-- src/theory/uf/symmetry_breaker.cpp | 4 +-- src/theory/uf/symmetry_breaker.h | 4 +-- src/theory/uf/theory_uf.cpp | 2 +- src/theory/uf/theory_uf.h | 4 +-- src/theory/uf/theory_uf_model.cpp | 2 +- src/theory/uf/theory_uf_model.h | 4 +-- src/theory/uf/theory_uf_rewriter.cpp | 4 +-- src/theory/uf/theory_uf_rewriter.h | 4 +-- src/theory/uf/theory_uf_type_rules.cpp | 4 +-- src/theory/uf/theory_uf_type_rules.h | 4 +-- src/theory/uf/type_enumerator.cpp | 4 +-- src/theory/uf/type_enumerator.h | 4 +-- src/theory/valuation.cpp | 2 +- src/theory/valuation.h | 2 +- src/util/CMakeLists.txt | 4 +-- src/util/bin_heap.h | 4 +-- src/util/bitvector.cpp | 2 +- src/util/bitvector.h | 2 +- src/util/bool.h | 4 +-- src/util/cardinality.cpp | 2 +- src/util/cardinality.h | 2 +- src/util/cardinality_class.cpp | 2 +- src/util/cardinality_class.h | 4 +-- src/util/dense_map.h | 2 +- src/util/didyoumean.cpp | 4 +-- src/util/didyoumean.h | 4 +-- src/util/divisible.cpp | 7 ++--- src/util/divisible.h | 9 +++---- src/util/floatingpoint.cpp | 2 +- src/util/floatingpoint.h | 2 +- src/util/floatingpoint_literal_symfpu.cpp | 4 +-- src/util/floatingpoint_literal_symfpu.h | 4 +-- .../floatingpoint_literal_symfpu_traits.cpp | 4 +-- .../floatingpoint_literal_symfpu_traits.h | 4 +-- src/util/floatingpoint_size.cpp | 2 +- src/util/floatingpoint_size.h | 2 +- src/util/gmp_util.h | 9 +++---- src/util/hash.h | 9 +++---- src/util/iand.h | 4 +-- src/util/index.cpp | 2 +- src/util/index.h | 4 +-- src/util/indexed_root_predicate.h | 4 +-- src/util/integer.h.in | 4 +-- src/util/integer_cln_imp.cpp | 2 +- src/util/integer_cln_imp.h | 2 +- src/util/integer_gmp_imp.cpp | 4 +-- src/util/integer_gmp_imp.h | 2 +- src/util/ostream_util.cpp | 2 +- src/util/ostream_util.h | 4 +-- src/util/poly_util.cpp | 4 +-- src/util/poly_util.h | 4 +-- src/util/random.cpp | 2 +- src/util/random.h | 4 +-- src/util/rational.h.in | 4 +-- src/util/rational_cln_imp.cpp | 4 +-- src/util/rational_cln_imp.h | 4 +-- src/util/rational_gmp_imp.cpp | 4 +-- src/util/rational_gmp_imp.h | 2 +- src/util/real_algebraic_number.h.in | 4 +-- src/util/real_algebraic_number_poly_imp.cpp | 4 +-- src/util/real_algebraic_number_poly_imp.h | 4 +-- src/util/regexp.cpp | 2 +- src/util/regexp.h | 2 +- src/util/resource_manager.cpp | 4 +-- src/util/resource_manager.h | 2 +- src/util/result.cpp | 4 +-- src/util/result.h | 4 +-- src/util/roundingmode.cpp | 2 +- src/util/roundingmode.h | 4 +-- src/util/safe_print.cpp | 2 +- src/util/safe_print.h | 4 +-- src/util/sampler.cpp | 4 +-- src/util/sampler.h | 4 +-- src/util/sexpr.cpp | 4 +-- src/util/sexpr.h | 4 +-- src/util/smt2_quote_string.cpp | 4 +-- src/util/smt2_quote_string.h | 4 +-- src/util/statistics_public.cpp | 4 +-- src/util/statistics_public.h | 4 +-- src/util/statistics_registry.cpp | 4 +-- src/util/statistics_registry.h | 4 +-- src/util/statistics_stats.cpp | 4 +-- src/util/statistics_stats.h | 4 +-- src/util/statistics_value.cpp | 2 +- src/util/statistics_value.h | 4 +-- src/util/string.cpp | 2 +- src/util/string.h | 4 +-- src/util/synth_result.cpp | 4 +-- src/util/synth_result.h | 4 +-- src/util/uninterpreted_sort_value.cpp | 4 +-- src/util/uninterpreted_sort_value.h | 4 +-- src/util/utility.cpp | 4 +-- src/util/utility.h | 2 +- test/CMakeLists.txt | 4 +-- test/api/CMakeLists.txt | 4 +-- test/api/cpp/CMakeLists.txt | 4 +-- test/api/cpp/boilerplate.cpp | 4 +-- test/api/cpp/issue4889.cpp | 4 +-- test/api/cpp/issue5074.cpp | 4 +-- test/api/cpp/issue6111.cpp | 4 +-- test/api/cpp/ouroborous.cpp | 4 +-- test/api/cpp/proj-issue306.cpp | 4 +-- test/api/cpp/proj-issue334.cpp | 4 +-- test/api/cpp/proj-issue344.cpp | 5 ++-- test/api/cpp/proj-issue345.cpp | 5 ++-- test/api/cpp/proj-issue377.cpp | 5 ++-- test/api/cpp/proj-issue395.cpp | 4 +-- test/api/cpp/proj-issue399.cpp | 4 +-- test/api/cpp/proj-issue445.cpp | 4 +-- test/api/cpp/proj-issue484.cpp | 4 +-- test/api/cpp/reset_assertions.cpp | 4 +-- test/api/cpp/sep_log_api.cpp | 4 +-- test/api/cpp/smt2_compliance.cpp | 4 +-- test/api/cpp/two_solvers.cpp | 4 +-- test/api/python/CMakeLists.txt | 4 +-- test/api/python/boilerplate.py | 8 +++--- test/api/python/issue4889.py | 8 +++--- test/api/python/issue5074.py | 8 +++--- test/api/python/issue6111.py | 8 +++--- test/api/python/proj-issue306.py | 8 +++--- test/api/python/reset_assertions.py | 8 +++--- test/api/python/sep_log_api.py | 8 +++--- test/api/python/two_solvers.py | 8 +++--- test/binary/CMakeLists.txt | 4 +-- test/binary/interactive_shell.py | 4 +-- test/regress/cli/run_regression.py | 4 +-- test/unit/CMakeLists.txt | 4 +-- test/unit/api/CMakeLists.txt | 4 +-- test/unit/api/cpp/CMakeLists.txt | 4 +-- test/unit/api/cpp/datatype_api_black.cpp | 4 +-- test/unit/api/cpp/grammar_black.cpp | 4 +-- test/unit/api/cpp/op_black.cpp | 4 +-- test/unit/api/cpp/op_white.cpp | 4 +-- .../api/cpp/parametric_datatype_black.cpp | 4 +-- test/unit/api/cpp/result_black.cpp | 4 +-- test/unit/api/cpp/solver_black.cpp | 4 +-- test/unit/api/cpp/solver_white.cpp | 4 +-- test/unit/api/cpp/sort_black.cpp | 2 +- test/unit/api/cpp/synth_result_black.cpp | 4 +-- test/unit/api/cpp/term_black.cpp | 4 +-- test/unit/api/cpp/term_white.cpp | 4 +-- test/unit/api/cpp/theory_arith_nl_black.cpp | 4 +-- test/unit/api/cpp/theory_uf_ho_black.cpp | 4 +-- test/unit/api/java/CMakeLists.txt | 4 +-- test/unit/api/java/DatatypeTest.java | 4 +-- test/unit/api/java/GrammarTest.java | 4 +-- test/unit/api/java/OpTest.java | 4 +-- test/unit/api/java/ResultTest.java | 4 +-- test/unit/api/java/SolverTest.java | 4 +-- test/unit/api/java/SortTest.java | 4 +-- test/unit/api/java/SynthResultTest.java | 4 +-- test/unit/api/java/TermTest.java | 4 +-- test/unit/api/python/CMakeLists.txt | 4 +-- test/unit/api/python/test_datatype_api.py | 4 +-- test/unit/api/python/test_grammar.py | 4 +-- test/unit/api/python/test_op.py | 4 +-- test/unit/api/python/test_result.py | 4 +-- test/unit/api/python/test_solver.py | 4 +-- test/unit/api/python/test_sort.py | 4 +-- test/unit/api/python/test_synth_result.py | 2 +- test/unit/api/python/test_term.py | 4 +-- test/unit/api/python/test_to_python_obj.py | 4 +-- test/unit/base/CMakeLists.txt | 4 +-- test/unit/base/map_util_black.cpp | 4 +-- test/unit/context/CMakeLists.txt | 4 +-- test/unit/context/cdhashmap_black.cpp | 4 +-- test/unit/context/cdhashmap_white.cpp | 2 +- test/unit/context/cdlist_black.cpp | 4 +-- test/unit/context/cdo_black.cpp | 2 +- test/unit/context/context_black.cpp | 4 +-- test/unit/context/context_mm_black.cpp | 4 +-- test/unit/context/context_white.cpp | 2 +- test/unit/main/CMakeLists.txt | 4 +-- test/unit/main/interactive_shell_black.cpp | 4 +-- test/unit/node/CMakeLists.txt | 4 +-- test/unit/node/attribute_black.cpp | 2 +- test/unit/node/attribute_white.cpp | 4 +-- test/unit/node/kind_black.cpp | 2 +- test/unit/node/kind_map_black.cpp | 4 +-- test/unit/node/node_algorithm_black.cpp | 2 +- test/unit/node/node_algorithms_black.cpp | 4 +-- test/unit/node/node_black.cpp | 2 +- test/unit/node/node_builder_black.cpp | 2 +- test/unit/node/node_manager_black.cpp | 4 +-- test/unit/node/node_manager_white.cpp | 4 +-- test/unit/node/node_self_iterator_black.cpp | 2 +- test/unit/node/node_traversal_black.cpp | 2 +- test/unit/node/node_white.cpp | 2 +- test/unit/node/symbol_table_black.cpp | 4 +-- test/unit/node/type_cardinality_black.cpp | 4 +-- test/unit/node/type_node_white.cpp | 4 +-- test/unit/options/CMakeLists.txt | 2 +- test/unit/options/options_black.cpp | 2 +- test/unit/parser/CMakeLists.txt | 4 +-- test/unit/parser/parser_black.cpp | 4 +-- test/unit/parser/parser_builder_black.cpp | 4 +-- test/unit/preprocessing/CMakeLists.txt | 4 +-- .../preprocessing/pass_bv_gauss_white.cpp | 2 +- .../pass_foreign_theory_rewrite_white.cpp | 4 +-- test/unit/printer/CMakeLists.txt | 4 +-- test/unit/printer/smt2_printer_black.cpp | 4 +-- test/unit/proof/CMakeLists.txt | 17 ++++++++++++ test/unit/proof/lfsc_node_converter_black.cpp | 4 +-- test/unit/prop/CMakeLists.txt | 4 +-- test/unit/prop/cnf_stream_white.cpp | 2 +- test/unit/test.h | 2 +- test/unit/test_api.h | 4 +-- test/unit/test_context.h | 4 +-- test/unit/test_env.h | 4 +-- test/unit/test_node.h | 4 +-- test/unit/test_smt.h | 2 +- test/unit/theory/CMakeLists.txt | 4 +-- test/unit/theory/arith_poly_white.cpp | 4 +-- test/unit/theory/evaluator_white.cpp | 4 +-- test/unit/theory/logic_info_white.cpp | 4 +-- test/unit/theory/regexp_operation_black.cpp | 4 +-- test/unit/theory/sequences_rewriter_white.cpp | 4 +-- test/unit/theory/strings_rewriter_white.cpp | 4 +-- .../theory/theory_arith_coverings_white.cpp | 4 +-- test/unit/theory/theory_arith_pow2_white.cpp | 4 +-- .../theory/theory_arith_rewriter_black.cpp | 4 +-- test/unit/theory/theory_arith_white.cpp | 4 +-- .../theory/theory_bags_normal_form_white.cpp | 4 +-- .../theory/theory_bags_rewriter_white.cpp | 4 +-- .../theory/theory_bags_type_rules_white.cpp | 4 +-- test/unit/theory/theory_black.cpp | 4 +-- .../theory/theory_bv_int_blaster_white.cpp | 4 +-- test/unit/theory/theory_bv_opt_white.cpp | 4 +-- test/unit/theory/theory_bv_rewriter_white.cpp | 4 +-- test/unit/theory/theory_bv_white.cpp | 4 +-- test/unit/theory/theory_engine_white.cpp | 2 +- test/unit/theory/theory_int_opt_white.cpp | 4 +-- .../theory/theory_opt_multigoal_white.cpp | 4 +-- ...eory_quantifiers_bv_instantiator_white.cpp | 4 +-- .../theory_quantifiers_bv_inverter_white.cpp | 2 +- .../theory/theory_sets_rewriter_white.cpp | 2 +- .../theory_sets_type_enumerator_white.cpp | 2 +- .../theory/theory_sets_type_rules_white.cpp | 4 +-- .../theory_strings_skolem_cache_black.cpp | 2 +- .../theory/theory_strings_utils_white.cpp | 4 +-- .../unit/theory/theory_strings_word_white.cpp | 2 +- test/unit/theory/theory_white.cpp | 4 +-- test/unit/theory/type_enumerator_white.cpp | 4 +-- test/unit/util/CMakeLists.txt | 4 +-- test/unit/util/array_store_all_white.cpp | 4 +-- test/unit/util/assert_white.cpp | 2 +- test/unit/util/binary_heap_black.cpp | 2 +- test/unit/util/bitvector_black.cpp | 4 +-- .../util/boolean_simplification_black.cpp | 4 +-- test/unit/util/cardinality_black.cpp | 2 +- test/unit/util/check_white.cpp | 2 +- test/unit/util/configuration_black.cpp | 4 +-- test/unit/util/datatype_black.cpp | 2 +- test/unit/util/didyoumean_black.cpp | 4 +-- test/unit/util/exception_black.cpp | 2 +- test/unit/util/floatingpoint_black.cpp | 2 +- test/unit/util/integer_black.cpp | 4 +-- test/unit/util/integer_white.cpp | 2 +- test/unit/util/output_black.cpp | 4 +-- test/unit/util/rational_black.cpp | 2 +- test/unit/util/rational_white.cpp | 2 +- .../unit/util/real_algebraic_number_black.cpp | 2 +- test/unit/util/stats_black.cpp | 4 +-- 1742 files changed, 3179 insertions(+), 3142 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 56e83b1c8..83bd70992 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -4,7 +4,7 @@ # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. diff --git a/cmake/CMakeGraphVizOptions.cmake.in b/cmake/CMakeGraphVizOptions.cmake.in index d3be598b3..4ca946e11 100644 --- a/cmake/CMakeGraphVizOptions.cmake.in +++ b/cmake/CMakeGraphVizOptions.cmake.in @@ -4,7 +4,7 @@ # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. diff --git a/cmake/ConfigCompetition.cmake b/cmake/ConfigCompetition.cmake index 8ce9296ec..a152a87c0 100644 --- a/cmake/ConfigCompetition.cmake +++ b/cmake/ConfigCompetition.cmake @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Aina Niemetz, Andres Noetzli, Mathias Preiner +# Mathias Preiner, Aina Niemetz, Andres Noetzli # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. diff --git a/cmake/ConfigDebug.cmake b/cmake/ConfigDebug.cmake index 39ec7e77f..87a872bf3 100644 --- a/cmake/ConfigDebug.cmake +++ b/cmake/ConfigDebug.cmake @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Aina Niemetz, Mathias Preiner +# Mathias Preiner, Aina Niemetz # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. diff --git a/cmake/ConfigProduction.cmake b/cmake/ConfigProduction.cmake index 38cceea92..1176f2880 100644 --- a/cmake/ConfigProduction.cmake +++ b/cmake/ConfigProduction.cmake @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Aina Niemetz +# Aina Niemetz, Mathias Preiner # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. diff --git a/cmake/ConfigTesting.cmake b/cmake/ConfigTesting.cmake index 623c1a9da..9af2fb5d0 100644 --- a/cmake/ConfigTesting.cmake +++ b/cmake/ConfigTesting.cmake @@ -4,7 +4,7 @@ # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. diff --git a/cmake/ConfigureCvc5.cmake b/cmake/ConfigureCvc5.cmake index 7de13f046..d36d6ee77 100644 --- a/cmake/ConfigureCvc5.cmake +++ b/cmake/ConfigureCvc5.cmake @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Mathias Preiner, Gereon Kremer, Makai Mann +# Mathias Preiner, Gereon Kremer, Aina Niemetz # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. diff --git a/cmake/FindANTLR3.cmake b/cmake/FindANTLR3.cmake index a1812e695..f91286a69 100644 --- a/cmake/FindANTLR3.cmake +++ b/cmake/FindANTLR3.cmake @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Gereon Kremer, Andrew V. Jones +# Gereon Kremer, Andres Noetzli, Mathias Preiner # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. diff --git a/cmake/FindCLN.cmake b/cmake/FindCLN.cmake index 8b6a7f865..f9cd66419 100644 --- a/cmake/FindCLN.cmake +++ b/cmake/FindCLN.cmake @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Gereon Kremer, Mathias Preiner +# Gereon Kremer, Mathias Preiner, Andrew V. Jones # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. diff --git a/cmake/FindCVC5PythonicAPI.cmake b/cmake/FindCVC5PythonicAPI.cmake index 43d6254c8..7d2dfb58c 100644 --- a/cmake/FindCVC5PythonicAPI.cmake +++ b/cmake/FindCVC5PythonicAPI.cmake @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Gereon Kremer, Aina Niemetz +# Gereon Kremer, Alex Ozdemir # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. diff --git a/cmake/FindCaDiCaL.cmake b/cmake/FindCaDiCaL.cmake index f0e0f5652..5e94a7ee0 100644 --- a/cmake/FindCaDiCaL.cmake +++ b/cmake/FindCaDiCaL.cmake @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Gereon Kremer, Mathias Preiner +# Gereon Kremer, Mathias Preiner, Andres Noetzli # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. diff --git a/cmake/FindCoCoA.cmake b/cmake/FindCoCoA.cmake index d84bf0f2c..c6232807a 100644 --- a/cmake/FindCoCoA.cmake +++ b/cmake/FindCoCoA.cmake @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Gereon Kremer +# Gereon Kremer, Andres Noetzli # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. diff --git a/cmake/FindCryptoMiniSat.cmake b/cmake/FindCryptoMiniSat.cmake index b88eaa33e..48c287d65 100644 --- a/cmake/FindCryptoMiniSat.cmake +++ b/cmake/FindCryptoMiniSat.cmake @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Gereon Kremer, Mathias Preiner +# Gereon Kremer, Mathias Preiner, Andrew V. Jones # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. diff --git a/cmake/FindDrat2Er.cmake b/cmake/FindDrat2Er.cmake index daa0ec6a5..353023e7a 100644 --- a/cmake/FindDrat2Er.cmake +++ b/cmake/FindDrat2Er.cmake @@ -4,7 +4,7 @@ # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. diff --git a/cmake/FindDummy.cmake.template b/cmake/FindDummy.cmake.template index a9d75bc9a..65177e9eb 100644 --- a/cmake/FindDummy.cmake.template +++ b/cmake/FindDummy.cmake.template @@ -4,7 +4,7 @@ # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. diff --git a/cmake/FindEditline.cmake b/cmake/FindEditline.cmake index 1038424a3..b884a9de4 100644 --- a/cmake/FindEditline.cmake +++ b/cmake/FindEditline.cmake @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Andrew V. Jones, Mathias Preiner +# Andrew V. Jones, Mathias Preiner, Gereon Kremer # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. diff --git a/cmake/FindGLPK.cmake b/cmake/FindGLPK.cmake index 7489a7ac3..fe8213225 100644 --- a/cmake/FindGLPK.cmake +++ b/cmake/FindGLPK.cmake @@ -4,7 +4,7 @@ # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. diff --git a/cmake/FindGMP.cmake b/cmake/FindGMP.cmake index b6db90054..c4ed3fc20 100644 --- a/cmake/FindGMP.cmake +++ b/cmake/FindGMP.cmake @@ -4,7 +4,7 @@ # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. diff --git a/cmake/FindGTest.cmake b/cmake/FindGTest.cmake index d36829784..b75e0f624 100644 --- a/cmake/FindGTest.cmake +++ b/cmake/FindGTest.cmake @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Gereon Kremer +# Gereon Kremer, Mathias Preiner # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. diff --git a/cmake/FindHamcrest.cmake b/cmake/FindHamcrest.cmake index a2ed92796..283633e38 100644 --- a/cmake/FindHamcrest.cmake +++ b/cmake/FindHamcrest.cmake @@ -4,7 +4,7 @@ # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. diff --git a/cmake/FindJUnit.cmake b/cmake/FindJUnit.cmake index 1532042a4..f88240600 100644 --- a/cmake/FindJUnit.cmake +++ b/cmake/FindJUnit.cmake @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Mathias Preiner, Mudathir Mohamed +# Mudathir Mohamed, Mathias Preiner # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. diff --git a/cmake/FindKissat.cmake b/cmake/FindKissat.cmake index e257d2b3d..ff355cbec 100644 --- a/cmake/FindKissat.cmake +++ b/cmake/FindKissat.cmake @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Gereon Kremer, Aina Niemetz +# Gereon Kremer, Mathias Preiner, Aina Niemetz # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. diff --git a/cmake/FindLFSC.cmake b/cmake/FindLFSC.cmake index cad90df45..757306a1e 100644 --- a/cmake/FindLFSC.cmake +++ b/cmake/FindLFSC.cmake @@ -4,7 +4,7 @@ # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. diff --git a/cmake/FindPoly.cmake b/cmake/FindPoly.cmake index 9c72afc23..01100f3a0 100644 --- a/cmake/FindPoly.cmake +++ b/cmake/FindPoly.cmake @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Gereon Kremer +# Gereon Kremer, Andres Noetzli, Mathias Preiner # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. diff --git a/cmake/FindSphinx.cmake b/cmake/FindSphinx.cmake index c0521eb44..cc22438e4 100644 --- a/cmake/FindSphinx.cmake +++ b/cmake/FindSphinx.cmake @@ -4,7 +4,7 @@ # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. diff --git a/cmake/FindSymFPU.cmake b/cmake/FindSymFPU.cmake index 65191156a..a633e2528 100644 --- a/cmake/FindSymFPU.cmake +++ b/cmake/FindSymFPU.cmake @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Gereon Kremer, Mathias Preiner +# Gereon Kremer, Mathias Preiner, Aina Niemetz # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. diff --git a/cmake/FindValgrind.cmake b/cmake/FindValgrind.cmake index 590509761..ae1439fa6 100644 --- a/cmake/FindValgrind.cmake +++ b/cmake/FindValgrind.cmake @@ -4,7 +4,7 @@ # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. diff --git a/cmake/Helpers.cmake b/cmake/Helpers.cmake index 465967f21..34487bbc6 100644 --- a/cmake/Helpers.cmake +++ b/cmake/Helpers.cmake @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Mathias Preiner, Aina Niemetz, Andres Noetzli +# Mathias Preiner, Aina Niemetz, Andrew V. Jones # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. diff --git a/cmake/IWYU.cmake b/cmake/IWYU.cmake index 5eb9271c9..9ff426940 100644 --- a/cmake/IWYU.cmake +++ b/cmake/IWYU.cmake @@ -4,7 +4,7 @@ # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. diff --git a/cmake/Toolchain-aarch64.cmake b/cmake/Toolchain-aarch64.cmake index 55012c6be..cec586246 100644 --- a/cmake/Toolchain-aarch64.cmake +++ b/cmake/Toolchain-aarch64.cmake @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Mathias Preiner +# Mathias Preiner, Andres Noetzli, Gereon Kremer # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. diff --git a/cmake/Toolchain-mingw64.cmake b/cmake/Toolchain-mingw64.cmake index c4c2473cf..6bd3443ff 100644 --- a/cmake/Toolchain-mingw64.cmake +++ b/cmake/Toolchain-mingw64.cmake @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Mathias Preiner, Gereon Kremer +# Mathias Preiner, Andres Noetzli # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. diff --git a/cmake/cvc5Config.cmake.in b/cmake/cvc5Config.cmake.in index 11217e087..10676b164 100644 --- a/cmake/cvc5Config.cmake.in +++ b/cmake/cvc5Config.cmake.in @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Mudathir Mohamed, Mathias Preiner, Andres Noetzli +# Mudathir Mohamed, Mathias Preiner, Aina Niemetz # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. diff --git a/cmake/deps-helper.cmake b/cmake/deps-helper.cmake index 9a92928b6..d9c554c22 100644 --- a/cmake/deps-helper.cmake +++ b/cmake/deps-helper.cmake @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Gereon Kremer +# Gereon Kremer, Mathias Preiner, Andrew V. Jones # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. diff --git a/cmake/fuzzing-murxla.cmake b/cmake/fuzzing-murxla.cmake index 7f3919f3e..061e07e2f 100644 --- a/cmake/fuzzing-murxla.cmake +++ b/cmake/fuzzing-murxla.cmake @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Gereon Kremer +# Gereon Kremer, Mathias Preiner # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. diff --git a/cmake/target-graphs.cmake b/cmake/target-graphs.cmake index ad1023cd7..7ec643ea0 100644 --- a/cmake/target-graphs.cmake +++ b/cmake/target-graphs.cmake @@ -4,7 +4,7 @@ # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. diff --git a/cmake/version.cmake b/cmake/version.cmake index 87ba19933..4353ba70f 100644 --- a/cmake/version.cmake +++ b/cmake/version.cmake @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Aina Niemetz, Mathias Preiner +# Gereon Kremer, Mathias Preiner, Aina Niemetz # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. diff --git a/contrib/get-authors b/contrib/get-authors index 3bec55130..c066e86d8 100755 --- a/contrib/get-authors +++ b/contrib/get-authors @@ -72,6 +72,10 @@ while [ $# -gt 0 ]; do sed 's/FabianWolff/Fabian Wolff/' | \ sed 's/mudathirmahgoub/Mudathir Mohamed/' | \ sed 's/mcjuneho/Michael Chang/' | \ + sed 's/MikolasJanota/Mikolas Janota/' | \ + sed 's/Ouyancheng/Yancheng Ou/' | \ + sed 's/Lachnitt/Hanna Lachnitt/' | \ + sed 's/vinciusb/Vinícius Braga Freire/' | \ # Determine top three contributors sort | uniq -c | sort -rn | head -n3 | \ diff --git a/contrib/update-copyright.pl b/contrib/update-copyright.pl index a9bf1fe0b..25e8813f7 100755 --- a/contrib/update-copyright.pl +++ b/contrib/update-copyright.pl @@ -1,7 +1,7 @@ #!/usr/bin/perl -w # # update-copyright.pl -# Copyright (c) 2009-2021 The cvc5 Project +# Copyright (c) 2009-2022 The cvc5 Project # # usage: update-copyright [-m] [files/directories...] # update-copyright [-h | --help] @@ -42,6 +42,7 @@ $excluded_paths .= '|cmake/FindCython.cmake'; $excluded_paths .= '|cmake/FindPythonExtensions.cmake'; $excluded_paths .= '|cmake/UseCython.cmake'; $excluded_paths .= '|cmake/targetLinkLibrariesWithDynamicLookup.cmake'; +$excluded_paths .= '|cmake/version-base.cmake'; # minisat license $excluded_paths .= '|src/prop/(bv)?minisat/core/.*'; $excluded_paths .= '|src/prop/(bv)?minisat/mtl/.*'; @@ -51,7 +52,7 @@ $excluded_paths .= ')$'; # Years of copyright for the template. E.g., the string # "1985, 1987, 1992, 1997, 2008" or "2006-2009" or whatever. -my $years = '2009-2021'; +my $years = '2009-2022'; my $standard_template = < diff --git a/test/api/cpp/proj-issue345.cpp b/test/api/cpp/proj-issue345.cpp index 1bef8a05b..95544c726 100644 --- a/test/api/cpp/proj-issue345.cpp +++ b/test/api/cpp/proj-issue345.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Yoni Zohar + * Yoni Zohar, Mathias Preiner, Andrew Reynolds * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. @@ -14,7 +14,6 @@ * */ - #include "api/cpp/cvc5.h" #include diff --git a/test/api/cpp/proj-issue377.cpp b/test/api/cpp/proj-issue377.cpp index 3206fb82b..472b659f7 100644 --- a/test/api/cpp/proj-issue377.cpp +++ b/test/api/cpp/proj-issue377.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Yoni Zohar + * Andrew Reynolds, Mathias Preiner * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. @@ -14,7 +14,6 @@ * */ - #include "api/cpp/cvc5.h" #include diff --git a/test/api/cpp/proj-issue395.cpp b/test/api/cpp/proj-issue395.cpp index 9706d0916..6d0695b41 100644 --- a/test/api/cpp/proj-issue395.cpp +++ b/test/api/cpp/proj-issue395.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Andres Noetzli + * Andres Noetzli, Mathias Preiner * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/api/cpp/proj-issue399.cpp b/test/api/cpp/proj-issue399.cpp index 270c8247a..e06f9c6a0 100644 --- a/test/api/cpp/proj-issue399.cpp +++ b/test/api/cpp/proj-issue399.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Andres Noetzli + * Andres Noetzli, Mathias Preiner * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/api/cpp/proj-issue445.cpp b/test/api/cpp/proj-issue445.cpp index 116486f55..14f998e5f 100644 --- a/test/api/cpp/proj-issue445.cpp +++ b/test/api/cpp/proj-issue445.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Andres Noetzli + * Andres Noetzli, Mathias Preiner * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/api/cpp/proj-issue484.cpp b/test/api/cpp/proj-issue484.cpp index 3698e420f..412739b13 100644 --- a/test/api/cpp/proj-issue484.cpp +++ b/test/api/cpp/proj-issue484.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Andrew Reynolds + * Andrew Reynolds, Mathias Preiner * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/api/cpp/reset_assertions.cpp b/test/api/cpp/reset_assertions.cpp index 72ce5fb64..735249d5d 100644 --- a/test/api/cpp/reset_assertions.cpp +++ b/test/api/cpp/reset_assertions.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Andres Noetzli, Mudathir Mohamed, Aina Niemetz + * Andres Noetzli, Mathias Preiner, Mudathir Mohamed * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/api/cpp/sep_log_api.cpp b/test/api/cpp/sep_log_api.cpp index 5bcc7f8e0..1985b3c3e 100644 --- a/test/api/cpp/sep_log_api.cpp +++ b/test/api/cpp/sep_log_api.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Andrew V. Jones, Andres Noetzli, Andrew Reynolds + * Andrew V. Jones, Andres Noetzli, Mathias Preiner * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/api/cpp/smt2_compliance.cpp b/test/api/cpp/smt2_compliance.cpp index 6b8866cae..06c5cb304 100644 --- a/test/api/cpp/smt2_compliance.cpp +++ b/test/api/cpp/smt2_compliance.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Aina Niemetz, Morgan Deters, Tim King + * Aina Niemetz, Morgan Deters, Gereon Kremer * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/api/cpp/two_solvers.cpp b/test/api/cpp/two_solvers.cpp index 45886670b..e6d162493 100644 --- a/test/api/cpp/two_solvers.cpp +++ b/test/api/cpp/two_solvers.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Andres Noetzli, Morgan Deters, Aina Niemetz + * Morgan Deters, Andrew Reynolds, Andres Noetzli * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/api/python/CMakeLists.txt b/test/api/python/CMakeLists.txt index 966cfc06b..439b96bfd 100644 --- a/test/api/python/CMakeLists.txt +++ b/test/api/python/CMakeLists.txt @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Yoni Zohar, Aina Niemetz, Mathias Preiner +# Yoni Zohar, Aina Niemetz # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. diff --git a/test/api/python/boilerplate.py b/test/api/python/boilerplate.py index ee3e6ca57..4e0f6515c 100644 --- a/test/api/python/boilerplate.py +++ b/test/api/python/boilerplate.py @@ -1,14 +1,14 @@ -############################################################################## +############################################################################### # Top contributors (to current version): -# Yoni Zohar +# Andrew Reynolds, Alex Ozdemir # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. -# ############################################################################ +# ############################################################################# # # A simple start-up/tear-down test for cvc5. # diff --git a/test/api/python/issue4889.py b/test/api/python/issue4889.py index 929739ab0..d5cf8665b 100644 --- a/test/api/python/issue4889.py +++ b/test/api/python/issue4889.py @@ -1,14 +1,14 @@ -############################################################################## +############################################################################### # Top contributors (to current version): -# Yoni Zohar +# Yoni Zohar, Alex Ozdemir, Aina Niemetz # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. -# ############################################################################ +# ############################################################################# # # Test for issue #4889 ## diff --git a/test/api/python/issue5074.py b/test/api/python/issue5074.py index 5dd3f01a6..312448215 100644 --- a/test/api/python/issue5074.py +++ b/test/api/python/issue5074.py @@ -1,14 +1,14 @@ -############################################################################## +############################################################################### # Top contributors (to current version): -# Yoni Zohar +# Aina Niemetz, Alex Ozdemir, Yoni Zohar # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. -# ############################################################################ +# ############################################################################# # # Test for issue #5074 ## diff --git a/test/api/python/issue6111.py b/test/api/python/issue6111.py index 146a403a3..89334c7f2 100644 --- a/test/api/python/issue6111.py +++ b/test/api/python/issue6111.py @@ -1,14 +1,14 @@ -############################################################################## +############################################################################### # Top contributors (to current version): -# Yoni Zohar +# Yoni Zohar, Aina Niemetz, Alex Ozdemir # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. -# ############################################################################ +# ############################################################################# # # Test for issue #6111 ## diff --git a/test/api/python/proj-issue306.py b/test/api/python/proj-issue306.py index 9487ff3b0..e03724149 100644 --- a/test/api/python/proj-issue306.py +++ b/test/api/python/proj-issue306.py @@ -1,14 +1,14 @@ -############################################################################## +############################################################################### # Top contributors (to current version): -# Yoni Zohar +# Yoni Zohar, Alex Ozdemir, Aina Niemetz # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. -# ############################################################################ +# ############################################################################# # ## diff --git a/test/api/python/reset_assertions.py b/test/api/python/reset_assertions.py index 8883ea798..7946f49b7 100644 --- a/test/api/python/reset_assertions.py +++ b/test/api/python/reset_assertions.py @@ -1,14 +1,14 @@ -############################################################################## +############################################################################### # Top contributors (to current version): -# Yoni Zohar +# Yoni Zohar, Alex Ozdemir, Aina Niemetz # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. -# ############################################################################ +# ############################################################################# # # A simple test for SolverEngine::resetAssertions() # diff --git a/test/api/python/sep_log_api.py b/test/api/python/sep_log_api.py index 27d5eb41c..d1b4ccd0e 100644 --- a/test/api/python/sep_log_api.py +++ b/test/api/python/sep_log_api.py @@ -1,14 +1,14 @@ -############################################################################## +############################################################################### # Top contributors (to current version): -# Yoni Zohar +# Yoni Zohar, Aina Niemetz, Alex Ozdemir # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. -# ############################################################################ +# ############################################################################# # # Two tests to validate the use of the separation logic API. # diff --git a/test/api/python/two_solvers.py b/test/api/python/two_solvers.py index 7692d907c..93d97a539 100644 --- a/test/api/python/two_solvers.py +++ b/test/api/python/two_solvers.py @@ -1,14 +1,14 @@ -############################################################################## +############################################################################### # Top contributors (to current version): -# Yoni Zohar +# Andrew Reynolds, Alex Ozdemir # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. -# ############################################################################ +# ############################################################################# # # A simple test of multiple SmtEngines. ## diff --git a/test/binary/CMakeLists.txt b/test/binary/CMakeLists.txt index 39186813b..36359e084 100644 --- a/test/binary/CMakeLists.txt +++ b/test/binary/CMakeLists.txt @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Aina Niemetz, Andrew V. Jones, Gereon Kremer +# Yoni Zohar, Andrew V. Jones, Aina Niemetz # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. diff --git a/test/binary/interactive_shell.py b/test/binary/interactive_shell.py index 6577ce13e..534f82048 100644 --- a/test/binary/interactive_shell.py +++ b/test/binary/interactive_shell.py @@ -1,11 +1,11 @@ #!/usr/bin/env python3 ############################################################################### # Top contributors (to current version): -# Andrew V. Jones +# Andrew V. Jones, Mathias Preiner, Aina Niemetz # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. diff --git a/test/regress/cli/run_regression.py b/test/regress/cli/run_regression.py index 8ef0da532..c4c87fecd 100755 --- a/test/regress/cli/run_regression.py +++ b/test/regress/cli/run_regression.py @@ -1,11 +1,11 @@ #!/usr/bin/env python3 ############################################################################### # Top contributors (to current version): -# Andres Noetzli, Mathias Preiner, Yoni Zohar +# Andres Noetzli, Aina Niemetz, Yoni Zohar # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. diff --git a/test/unit/CMakeLists.txt b/test/unit/CMakeLists.txt index 12ef89983..038a508c6 100644 --- a/test/unit/CMakeLists.txt +++ b/test/unit/CMakeLists.txt @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Aina Niemetz, Mathias Preiner, Gereon Kremer +# Aina Niemetz, Mathias Preiner, Andres Noetzli # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. diff --git a/test/unit/api/CMakeLists.txt b/test/unit/api/CMakeLists.txt index 0701c3ca6..297c6322a 100644 --- a/test/unit/api/CMakeLists.txt +++ b/test/unit/api/CMakeLists.txt @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Aina Niemetz, Andres Noetzli +# Yoni Zohar, Mudathir Mohamed, Aina Niemetz # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. diff --git a/test/unit/api/cpp/CMakeLists.txt b/test/unit/api/cpp/CMakeLists.txt index cf6816981..7d2657ea1 100644 --- a/test/unit/api/cpp/CMakeLists.txt +++ b/test/unit/api/cpp/CMakeLists.txt @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Aina Niemetz +# Gereon Kremer, Andrew Reynolds # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. diff --git a/test/unit/api/cpp/datatype_api_black.cpp b/test/unit/api/cpp/datatype_api_black.cpp index b29e232e0..2a66a3b55 100644 --- a/test/unit/api/cpp/datatype_api_black.cpp +++ b/test/unit/api/cpp/datatype_api_black.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Andrew Reynolds, Aina Niemetz, Andres Noetzli + * Andrew Reynolds, Aina Niemetz, Yoni Zohar * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/api/cpp/grammar_black.cpp b/test/unit/api/cpp/grammar_black.cpp index be05d39c8..5340f0f7a 100644 --- a/test/unit/api/cpp/grammar_black.cpp +++ b/test/unit/api/cpp/grammar_black.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Aina Niemetz, Abdalrhman Mohamed + * Aina Niemetz, Andrew Reynolds * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/api/cpp/op_black.cpp b/test/unit/api/cpp/op_black.cpp index ff4296de6..8b6157016 100644 --- a/test/unit/api/cpp/op_black.cpp +++ b/test/unit/api/cpp/op_black.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Makai Mann, Aina Niemetz + * Andres Noetzli, Mathias Preiner, Aina Niemetz * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/api/cpp/op_white.cpp b/test/unit/api/cpp/op_white.cpp index c74ee150f..29df830f6 100644 --- a/test/unit/api/cpp/op_white.cpp +++ b/test/unit/api/cpp/op_white.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Aina Niemetz, Makai Mann + * Aina Niemetz, Andres Noetzli * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/api/cpp/parametric_datatype_black.cpp b/test/unit/api/cpp/parametric_datatype_black.cpp index 80c1fbc52..f8a089c6a 100644 --- a/test/unit/api/cpp/parametric_datatype_black.cpp +++ b/test/unit/api/cpp/parametric_datatype_black.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Andrew Reynolds + * Andrew Reynolds, Mathias Preiner * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/api/cpp/result_black.cpp b/test/unit/api/cpp/result_black.cpp index befaaf7d8..d062a17b2 100644 --- a/test/unit/api/cpp/result_black.cpp +++ b/test/unit/api/cpp/result_black.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Aina Niemetz + * Aina Niemetz, Mathias Preiner, Andrew Reynolds * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp index bcbbe0ac0..fbbf71595 100644 --- a/test/unit/api/cpp/solver_black.cpp +++ b/test/unit/api/cpp/solver_black.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Aina Niemetz, Mudathir Mohamed, Andrew Reynolds + * Aina Niemetz, Andrew Reynolds, Mathias Preiner * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/api/cpp/solver_white.cpp b/test/unit/api/cpp/solver_white.cpp index 3cc89434b..35911b4e8 100644 --- a/test/unit/api/cpp/solver_white.cpp +++ b/test/unit/api/cpp/solver_white.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Aina Niemetz, Makai Mann, Andrew Reynolds + * Aina Niemetz, Mathias Preiner, Andrew Reynolds * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/api/cpp/sort_black.cpp b/test/unit/api/cpp/sort_black.cpp index c42253dd9..38b781def 100644 --- a/test/unit/api/cpp/sort_black.cpp +++ b/test/unit/api/cpp/sort_black.cpp @@ -4,7 +4,7 @@ * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/api/cpp/synth_result_black.cpp b/test/unit/api/cpp/synth_result_black.cpp index b45240343..8ba5b0215 100644 --- a/test/unit/api/cpp/synth_result_black.cpp +++ b/test/unit/api/cpp/synth_result_black.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Andrew Reynolds + * Andrew Reynolds, Mathias Preiner, Aina Niemetz * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/api/cpp/term_black.cpp b/test/unit/api/cpp/term_black.cpp index a10740597..93a5b73f6 100644 --- a/test/unit/api/cpp/term_black.cpp +++ b/test/unit/api/cpp/term_black.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Aina Niemetz, Makai Mann, Andrew Reynolds + * Aina Niemetz, Gereon Kremer, Mathias Preiner * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/api/cpp/term_white.cpp b/test/unit/api/cpp/term_white.cpp index 043cde805..083b63c6b 100644 --- a/test/unit/api/cpp/term_white.cpp +++ b/test/unit/api/cpp/term_white.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Makai Mann, Aina Niemetz, Andrew Reynolds + * Aina Niemetz, Makai Mann, Mathias Preiner * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/api/cpp/theory_arith_nl_black.cpp b/test/unit/api/cpp/theory_arith_nl_black.cpp index 18b426269..bf461ef66 100644 --- a/test/unit/api/cpp/theory_arith_nl_black.cpp +++ b/test/unit/api/cpp/theory_arith_nl_black.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Gereon Kremer + * Gereon Kremer, Andrew Reynolds * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/api/cpp/theory_uf_ho_black.cpp b/test/unit/api/cpp/theory_uf_ho_black.cpp index fc1d5fbaa..0de0af4a1 100644 --- a/test/unit/api/cpp/theory_uf_ho_black.cpp +++ b/test/unit/api/cpp/theory_uf_ho_black.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Andrew Reynolds + * Andrew Reynolds, Mathias Preiner * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/api/java/CMakeLists.txt b/test/unit/api/java/CMakeLists.txt index 697dff605..ec8c6194b 100644 --- a/test/unit/api/java/CMakeLists.txt +++ b/test/unit/api/java/CMakeLists.txt @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Mudathir Mohamed +# Mudathir Mohamed, Gereon Kremer, Andrew Reynolds # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. diff --git a/test/unit/api/java/DatatypeTest.java b/test/unit/api/java/DatatypeTest.java index 01e2d2989..0ed846778 100644 --- a/test/unit/api/java/DatatypeTest.java +++ b/test/unit/api/java/DatatypeTest.java @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Andrew Reynolds, Aina Niemetz, Andres Noetzli, Mudathir Mohamed + * Mudathir Mohamed, Andrew Reynolds, Aina Niemetz * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/api/java/GrammarTest.java b/test/unit/api/java/GrammarTest.java index f72190a09..41b3c989b 100644 --- a/test/unit/api/java/GrammarTest.java +++ b/test/unit/api/java/GrammarTest.java @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Aina Niemetz, Abdalrhman Mohamed, Mudathir Mohamed + * Mudathir Mohamed, Andrew Reynolds, Andres Noetzli * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/api/java/OpTest.java b/test/unit/api/java/OpTest.java index 7530de371..6ee172862 100644 --- a/test/unit/api/java/OpTest.java +++ b/test/unit/api/java/OpTest.java @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Makai Mann, Aina Niemetz, Mudathir Mohamed + * Andres Noetzli, Mudathir Mohamed, Aina Niemetz * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/api/java/ResultTest.java b/test/unit/api/java/ResultTest.java index cca0c4244..ab4569a74 100644 --- a/test/unit/api/java/ResultTest.java +++ b/test/unit/api/java/ResultTest.java @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Aina Niemetz, Mudathir Mohamed + * Mudathir Mohamed, Andrew Reynolds, Mathias Preiner * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java index 4cfbfcb88..de2a8db6b 100644 --- a/test/unit/api/java/SolverTest.java +++ b/test/unit/api/java/SolverTest.java @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Aina Niemetz, Mudathir Mohamed, Andrew Reynolds + * Mudathir Mohamed, Andrew Reynolds, Aina Niemetz * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/api/java/SortTest.java b/test/unit/api/java/SortTest.java index 2255153ab..beb301357 100644 --- a/test/unit/api/java/SortTest.java +++ b/test/unit/api/java/SortTest.java @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Aina Niemetz, Andrew Reynolds, Mathias Preiner, Mudathir Mohamed + * Mudathir Mohamed, Aina Niemetz, Mathias Preiner * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/api/java/SynthResultTest.java b/test/unit/api/java/SynthResultTest.java index 8ea1e61ef..06330cc3f 100644 --- a/test/unit/api/java/SynthResultTest.java +++ b/test/unit/api/java/SynthResultTest.java @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Andrew Reynolds + * Andrew Reynolds, Mudathir Mohamed, Andres Noetzli * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/api/java/TermTest.java b/test/unit/api/java/TermTest.java index 5f88904a4..b7302b7f3 100644 --- a/test/unit/api/java/TermTest.java +++ b/test/unit/api/java/TermTest.java @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Aina Niemetz, Makai Mann, Andrew Reynolds, Mudathir Mohamed + * Mudathir Mohamed, Andres Noetzli, Aina Niemetz * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/api/python/CMakeLists.txt b/test/unit/api/python/CMakeLists.txt index fe68f1eea..add579bc5 100644 --- a/test/unit/api/python/CMakeLists.txt +++ b/test/unit/api/python/CMakeLists.txt @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Yoni Zohar, Aina Niemetz, Mathias Preiner +# Gereon Kremer, Aina Niemetz, Yoni Zohar # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. diff --git a/test/unit/api/python/test_datatype_api.py b/test/unit/api/python/test_datatype_api.py index a2b79ca7e..9caedd3f8 100644 --- a/test/unit/api/python/test_datatype_api.py +++ b/test/unit/api/python/test_datatype_api.py @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Yoni Zohar +# Yoni Zohar, Andrew Reynolds, Aina Niemetz # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. diff --git a/test/unit/api/python/test_grammar.py b/test/unit/api/python/test_grammar.py index 1c00da13c..464f51648 100644 --- a/test/unit/api/python/test_grammar.py +++ b/test/unit/api/python/test_grammar.py @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Yoni Zohar, Makai Mann, Mudathir Mohamed +# Yoni Zohar, Andrew Reynolds, Alex Ozdemir # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. diff --git a/test/unit/api/python/test_op.py b/test/unit/api/python/test_op.py index 710f93ff4..c8cde5bb1 100644 --- a/test/unit/api/python/test_op.py +++ b/test/unit/api/python/test_op.py @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Yoni Zohar +# Aina Niemetz, Andres Noetzli, Yoni Zohar # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. diff --git a/test/unit/api/python/test_result.py b/test/unit/api/python/test_result.py index 72e4ba314..195e193a8 100644 --- a/test/unit/api/python/test_result.py +++ b/test/unit/api/python/test_result.py @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Yoni Zohar +# Yoni Zohar, Andrew Reynolds, Alex Ozdemir # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. diff --git a/test/unit/api/python/test_solver.py b/test/unit/api/python/test_solver.py index 019edc251..6f02bbe87 100644 --- a/test/unit/api/python/test_solver.py +++ b/test/unit/api/python/test_solver.py @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Yoni Zohar, Ying Sheng +# Ying Sheng, Yoni Zohar, Aina Niemetz # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. diff --git a/test/unit/api/python/test_sort.py b/test/unit/api/python/test_sort.py index b70ba22d3..75384aac4 100644 --- a/test/unit/api/python/test_sort.py +++ b/test/unit/api/python/test_sort.py @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Yoni Zohar, Makai Mann +# Yoni Zohar, Aina Niemetz, Makai Mann # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. diff --git a/test/unit/api/python/test_synth_result.py b/test/unit/api/python/test_synth_result.py index 4248efa0d..892e641a1 100644 --- a/test/unit/api/python/test_synth_result.py +++ b/test/unit/api/python/test_synth_result.py @@ -4,7 +4,7 @@ # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. diff --git a/test/unit/api/python/test_term.py b/test/unit/api/python/test_term.py index 9416c3a1f..f166ecd0a 100644 --- a/test/unit/api/python/test_term.py +++ b/test/unit/api/python/test_term.py @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Yoni Zohar, Makai Mann, Andres Noetzli +# Yoni Zohar, Aina Niemetz, Andres Noetzli # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. diff --git a/test/unit/api/python/test_to_python_obj.py b/test/unit/api/python/test_to_python_obj.py index 42f8bccbf..518867f9d 100644 --- a/test/unit/api/python/test_to_python_obj.py +++ b/test/unit/api/python/test_to_python_obj.py @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Makai Mann, Andres Noetzli, Mudathir Mohamed +# Makai Mann, Alex Ozdemir, Aina Niemetz # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. diff --git a/test/unit/base/CMakeLists.txt b/test/unit/base/CMakeLists.txt index 89f28390e..d7effc11f 100644 --- a/test/unit/base/CMakeLists.txt +++ b/test/unit/base/CMakeLists.txt @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Aina Niemetz +# Mathias Preiner, Aina Niemetz # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. diff --git a/test/unit/base/map_util_black.cpp b/test/unit/base/map_util_black.cpp index 5ef8c747c..521490628 100644 --- a/test/unit/base/map_util_black.cpp +++ b/test/unit/base/map_util_black.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Aina Niemetz, Tim King + * Aina Niemetz, Mathias Preiner, Tim King * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/context/CMakeLists.txt b/test/unit/context/CMakeLists.txt index 565b828de..e3fd51ad4 100644 --- a/test/unit/context/CMakeLists.txt +++ b/test/unit/context/CMakeLists.txt @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Aina Niemetz +# Mathias Preiner, Aina Niemetz # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. diff --git a/test/unit/context/cdhashmap_black.cpp b/test/unit/context/cdhashmap_black.cpp index fde9517d0..daeadb004 100644 --- a/test/unit/context/cdhashmap_black.cpp +++ b/test/unit/context/cdhashmap_black.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Aina Niemetz, Morgan Deters + * Aina Niemetz, Andrew Reynolds, Mathias Preiner * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/context/cdhashmap_white.cpp b/test/unit/context/cdhashmap_white.cpp index 038bc0138..4389598c6 100644 --- a/test/unit/context/cdhashmap_white.cpp +++ b/test/unit/context/cdhashmap_white.cpp @@ -4,7 +4,7 @@ * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/context/cdlist_black.cpp b/test/unit/context/cdlist_black.cpp index 2772e1503..2c331c41b 100644 --- a/test/unit/context/cdlist_black.cpp +++ b/test/unit/context/cdlist_black.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Aina Niemetz, Morgan Deters + * Aina Niemetz, Andres Noetzli, Morgan Deters * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/context/cdo_black.cpp b/test/unit/context/cdo_black.cpp index 564d5f73e..45da7db9d 100644 --- a/test/unit/context/cdo_black.cpp +++ b/test/unit/context/cdo_black.cpp @@ -4,7 +4,7 @@ * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/context/context_black.cpp b/test/unit/context/context_black.cpp index 12efc52ca..f1c094ae5 100644 --- a/test/unit/context/context_black.cpp +++ b/test/unit/context/context_black.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Aina Niemetz, Morgan Deters, Dejan Jovanovic + * Aina Niemetz, Andres Noetzli, Morgan Deters * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/context/context_mm_black.cpp b/test/unit/context/context_mm_black.cpp index 8c9101be5..058fdb8ef 100644 --- a/test/unit/context/context_mm_black.cpp +++ b/test/unit/context/context_mm_black.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Aina Niemetz, Dejan Jovanovic, Andres Noetzli + * Aina Niemetz, Dejan Jovanovic, Morgan Deters * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/context/context_white.cpp b/test/unit/context/context_white.cpp index 2fef425b3..8a7e669e8 100644 --- a/test/unit/context/context_white.cpp +++ b/test/unit/context/context_white.cpp @@ -4,7 +4,7 @@ * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/main/CMakeLists.txt b/test/unit/main/CMakeLists.txt index b15e89bbd..e39d4f827 100644 --- a/test/unit/main/CMakeLists.txt +++ b/test/unit/main/CMakeLists.txt @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Aina Niemetz +# Mathias Preiner, Aina Niemetz # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. diff --git a/test/unit/main/interactive_shell_black.cpp b/test/unit/main/interactive_shell_black.cpp index 1d3cbedcd..134c5fcdf 100644 --- a/test/unit/main/interactive_shell_black.cpp +++ b/test/unit/main/interactive_shell_black.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Aina Niemetz, Christopher L. Conway, Andrew Reynolds + * Aina Niemetz, Andres Noetzli, Christopher L. Conway * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/node/CMakeLists.txt b/test/unit/node/CMakeLists.txt index 989e408d2..b269501a8 100644 --- a/test/unit/node/CMakeLists.txt +++ b/test/unit/node/CMakeLists.txt @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Aina Niemetz +# Mathias Preiner, Gereon Kremer, Aina Niemetz # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. diff --git a/test/unit/node/attribute_black.cpp b/test/unit/node/attribute_black.cpp index 543e9f6a4..2b8e2b006 100644 --- a/test/unit/node/attribute_black.cpp +++ b/test/unit/node/attribute_black.cpp @@ -4,7 +4,7 @@ * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/node/attribute_white.cpp b/test/unit/node/attribute_white.cpp index c36746d91..5c7664e19 100644 --- a/test/unit/node/attribute_white.cpp +++ b/test/unit/node/attribute_white.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Aina Niemetz, Morgan Deters + * Aina Niemetz, Gereon Kremer, Morgan Deters * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/node/kind_black.cpp b/test/unit/node/kind_black.cpp index 28097cbba..a287ec1dd 100644 --- a/test/unit/node/kind_black.cpp +++ b/test/unit/node/kind_black.cpp @@ -4,7 +4,7 @@ * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/node/kind_map_black.cpp b/test/unit/node/kind_map_black.cpp index 47d6d1288..848122634 100644 --- a/test/unit/node/kind_map_black.cpp +++ b/test/unit/node/kind_map_black.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Aina Niemetz, Gereon Kremer + * Aina Niemetz, Gereon Kremer, Mathias Preiner * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/node/node_algorithm_black.cpp b/test/unit/node/node_algorithm_black.cpp index 517e1aab7..6c6ce1fe3 100644 --- a/test/unit/node/node_algorithm_black.cpp +++ b/test/unit/node/node_algorithm_black.cpp @@ -4,7 +4,7 @@ * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/node/node_algorithms_black.cpp b/test/unit/node/node_algorithms_black.cpp index 96440d4da..b1c5d1645 100644 --- a/test/unit/node/node_algorithms_black.cpp +++ b/test/unit/node/node_algorithms_black.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Gereon Kremer + * Gereon Kremer, Aina Niemetz * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/node/node_black.cpp b/test/unit/node/node_black.cpp index 8fd74b420..039d591cd 100644 --- a/test/unit/node/node_black.cpp +++ b/test/unit/node/node_black.cpp @@ -4,7 +4,7 @@ * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/node/node_builder_black.cpp b/test/unit/node/node_builder_black.cpp index 10bce9cd3..f066d36d8 100644 --- a/test/unit/node/node_builder_black.cpp +++ b/test/unit/node/node_builder_black.cpp @@ -4,7 +4,7 @@ * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/node/node_manager_black.cpp b/test/unit/node/node_manager_black.cpp index cfdffe116..ec0ee24f9 100644 --- a/test/unit/node/node_manager_black.cpp +++ b/test/unit/node/node_manager_black.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Aina Niemetz, Dejan Jovanovic, Andrew Reynolds + * Aina Niemetz, Dejan Jovanovic, Christopher L. Conway * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/node/node_manager_white.cpp b/test/unit/node/node_manager_white.cpp index 0b206ebc8..c90625175 100644 --- a/test/unit/node/node_manager_white.cpp +++ b/test/unit/node/node_manager_white.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Aina Niemetz, Andres Noetzli, Andrew Reynolds + * Aina Niemetz, Andres Noetzli, Mathias Preiner * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/node/node_self_iterator_black.cpp b/test/unit/node/node_self_iterator_black.cpp index d7f5fa492..55731b54c 100644 --- a/test/unit/node/node_self_iterator_black.cpp +++ b/test/unit/node/node_self_iterator_black.cpp @@ -4,7 +4,7 @@ * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/node/node_traversal_black.cpp b/test/unit/node/node_traversal_black.cpp index 012fe3532..da187159a 100644 --- a/test/unit/node/node_traversal_black.cpp +++ b/test/unit/node/node_traversal_black.cpp @@ -4,7 +4,7 @@ * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/node/node_white.cpp b/test/unit/node/node_white.cpp index 8ed563320..edc9a2855 100644 --- a/test/unit/node/node_white.cpp +++ b/test/unit/node/node_white.cpp @@ -4,7 +4,7 @@ * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/node/symbol_table_black.cpp b/test/unit/node/symbol_table_black.cpp index 9710a38f7..3d5ba7cfa 100644 --- a/test/unit/node/symbol_table_black.cpp +++ b/test/unit/node/symbol_table_black.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Aina Niemetz, Morgan Deters, Christopher L. Conway + * Aina Niemetz, Mathias Preiner, Morgan Deters * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/node/type_cardinality_black.cpp b/test/unit/node/type_cardinality_black.cpp index 84bf0c788..937396691 100644 --- a/test/unit/node/type_cardinality_black.cpp +++ b/test/unit/node/type_cardinality_black.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Aina Niemetz, Morgan Deters + * Aina Niemetz, Morgan Deters, Andrew Reynolds * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/node/type_node_white.cpp b/test/unit/node/type_node_white.cpp index a5367680d..83e74e078 100644 --- a/test/unit/node/type_node_white.cpp +++ b/test/unit/node/type_node_white.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Aina Niemetz, Andrew Reynolds + * Aina Niemetz, Andres Noetzli * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/options/CMakeLists.txt b/test/unit/options/CMakeLists.txt index da7ac4371..5f25c6699 100644 --- a/test/unit/options/CMakeLists.txt +++ b/test/unit/options/CMakeLists.txt @@ -4,7 +4,7 @@ # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. diff --git a/test/unit/options/options_black.cpp b/test/unit/options/options_black.cpp index 4a4b7b26d..064e56f49 100644 --- a/test/unit/options/options_black.cpp +++ b/test/unit/options/options_black.cpp @@ -4,7 +4,7 @@ * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/parser/CMakeLists.txt b/test/unit/parser/CMakeLists.txt index 890a38f76..f9cb9beed 100644 --- a/test/unit/parser/CMakeLists.txt +++ b/test/unit/parser/CMakeLists.txt @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Aina Niemetz +# Mathias Preiner, Aina Niemetz # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. diff --git a/test/unit/parser/parser_black.cpp b/test/unit/parser/parser_black.cpp index 5de730b45..904f3d463 100644 --- a/test/unit/parser/parser_black.cpp +++ b/test/unit/parser/parser_black.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Aina Niemetz, Christopher L. Conway, Morgan Deters + * Aina Niemetz, Christopher L. Conway, Gereon Kremer * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/parser/parser_builder_black.cpp b/test/unit/parser/parser_builder_black.cpp index 95d16cd0d..1dab98d80 100644 --- a/test/unit/parser/parser_builder_black.cpp +++ b/test/unit/parser/parser_builder_black.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Aina Niemetz, Christopher L. Conway, Tim King + * Aina Niemetz, Mathias Preiner, Andres Noetzli * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/preprocessing/CMakeLists.txt b/test/unit/preprocessing/CMakeLists.txt index 0cebfb604..46042c1e2 100644 --- a/test/unit/preprocessing/CMakeLists.txt +++ b/test/unit/preprocessing/CMakeLists.txt @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Aina Niemetz +# Mathias Preiner, Aina Niemetz # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. diff --git a/test/unit/preprocessing/pass_bv_gauss_white.cpp b/test/unit/preprocessing/pass_bv_gauss_white.cpp index 18d6eabec..78da6031e 100644 --- a/test/unit/preprocessing/pass_bv_gauss_white.cpp +++ b/test/unit/preprocessing/pass_bv_gauss_white.cpp @@ -4,7 +4,7 @@ * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/preprocessing/pass_foreign_theory_rewrite_white.cpp b/test/unit/preprocessing/pass_foreign_theory_rewrite_white.cpp index f42187267..e4e6c35f7 100644 --- a/test/unit/preprocessing/pass_foreign_theory_rewrite_white.cpp +++ b/test/unit/preprocessing/pass_foreign_theory_rewrite_white.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Aina Niemetz, Yoni Zohar + * Aina Niemetz, Mathias Preiner, Andrew Reynolds * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/printer/CMakeLists.txt b/test/unit/printer/CMakeLists.txt index 1b3e3c130..4df862a1c 100644 --- a/test/unit/printer/CMakeLists.txt +++ b/test/unit/printer/CMakeLists.txt @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Aina Niemetz +# Mathias Preiner, Aina Niemetz # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. diff --git a/test/unit/printer/smt2_printer_black.cpp b/test/unit/printer/smt2_printer_black.cpp index 99a043116..cddf93ae4 100644 --- a/test/unit/printer/smt2_printer_black.cpp +++ b/test/unit/printer/smt2_printer_black.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Aina Niemetz, Andres Noetzli + * Aina Niemetz, Gereon Kremer, Andres Noetzli * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/proof/CMakeLists.txt b/test/unit/proof/CMakeLists.txt index 749948e39..d1a1f9d48 100644 --- a/test/unit/proof/CMakeLists.txt +++ b/test/unit/proof/CMakeLists.txt @@ -1 +1,18 @@ +############################################################################### +# Top contributors (to current version): +# Andrew Reynolds +# +# This file is part of the cvc5 project. +# +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS +# in the top-level source directory and their institutional affiliations. +# All rights reserved. See the file COPYING in the top-level source +# directory for licensing information. +# ############################################################################# +# +# [[ Add one-line brief description here ]] +# +# [[ Add lengthier description here ]] +# \todo document this file +## cvc5_add_unit_test_black(lfsc_node_converter_black proof) diff --git a/test/unit/proof/lfsc_node_converter_black.cpp b/test/unit/proof/lfsc_node_converter_black.cpp index 8a776d85a..7885193db 100644 --- a/test/unit/proof/lfsc_node_converter_black.cpp +++ b/test/unit/proof/lfsc_node_converter_black.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Alex Ozdemir + * Andrew Reynolds, Mathias Preiner * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/prop/CMakeLists.txt b/test/unit/prop/CMakeLists.txt index 57143bf90..51956b61b 100644 --- a/test/unit/prop/CMakeLists.txt +++ b/test/unit/prop/CMakeLists.txt @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Aina Niemetz +# Mathias Preiner, Aina Niemetz # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. diff --git a/test/unit/prop/cnf_stream_white.cpp b/test/unit/prop/cnf_stream_white.cpp index 29c6f123c..e8795b3ce 100644 --- a/test/unit/prop/cnf_stream_white.cpp +++ b/test/unit/prop/cnf_stream_white.cpp @@ -4,7 +4,7 @@ * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/test.h b/test/unit/test.h index 8e680de4b..7469caf8e 100644 --- a/test/unit/test.h +++ b/test/unit/test.h @@ -4,7 +4,7 @@ * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/test_api.h b/test/unit/test_api.h index 95b7c3b17..d7660d04f 100644 --- a/test/unit/test_api.h +++ b/test/unit/test_api.h @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Aina Niemetz + * Aina Niemetz, Mathias Preiner * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/test_context.h b/test/unit/test_context.h index 455319c6b..ffcce6ce5 100644 --- a/test/unit/test_context.h +++ b/test/unit/test_context.h @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Aina Niemetz + * Aina Niemetz, Mathias Preiner * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/test_env.h b/test/unit/test_env.h index 376fd75db..699e3cf57 100644 --- a/test/unit/test_env.h +++ b/test/unit/test_env.h @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Aina Niemetz, Andrew Reynolds + * Gereon Kremer, Andres Noetzli * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/test_node.h b/test/unit/test_node.h index b6f43b394..020def8e8 100644 --- a/test/unit/test_node.h +++ b/test/unit/test_node.h @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Aina Niemetz, Andrew Reynolds + * Aina Niemetz, Andres Noetzli, Andrew Reynolds * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/test_smt.h b/test/unit/test_smt.h index 7d57d0b47..4ff66bdd6 100644 --- a/test/unit/test_smt.h +++ b/test/unit/test_smt.h @@ -4,7 +4,7 @@ * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt index 82cd3cb58..ea6730179 100644 --- a/test/unit/theory/CMakeLists.txt +++ b/test/unit/theory/CMakeLists.txt @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Aina Niemetz, Yoni Zohar, Yancheng Ou +# Mathias Preiner, Gereon Kremer, Yoni Zohar # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. diff --git a/test/unit/theory/arith_poly_white.cpp b/test/unit/theory/arith_poly_white.cpp index c8f38e43d..4162ba611 100644 --- a/test/unit/theory/arith_poly_white.cpp +++ b/test/unit/theory/arith_poly_white.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Andrew Reynolds + * Andrew Reynolds, Aina Niemetz, Andres Noetzli * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/theory/evaluator_white.cpp b/test/unit/theory/evaluator_white.cpp index fd8b85f90..06106de2c 100644 --- a/test/unit/theory/evaluator_white.cpp +++ b/test/unit/theory/evaluator_white.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Aina Niemetz, Andres Noetzli + * Aina Niemetz, Andrew Reynolds, Andres Noetzli * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/theory/logic_info_white.cpp b/test/unit/theory/logic_info_white.cpp index cc6ea757f..be4572e3c 100644 --- a/test/unit/theory/logic_info_white.cpp +++ b/test/unit/theory/logic_info_white.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Aina Niemetz, Morgan Deters, Andres Noetzli + * Morgan Deters, Aina Niemetz, Mathias Preiner * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/theory/regexp_operation_black.cpp b/test/unit/theory/regexp_operation_black.cpp index 01999f527..98d471ab4 100644 --- a/test/unit/theory/regexp_operation_black.cpp +++ b/test/unit/theory/regexp_operation_black.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Aina Niemetz, Andres Noetzli + * Andres Noetzli, Aina Niemetz, Andrew Reynolds * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/theory/sequences_rewriter_white.cpp b/test/unit/theory/sequences_rewriter_white.cpp index 15ec507b2..04c7d2502 100644 --- a/test/unit/theory/sequences_rewriter_white.cpp +++ b/test/unit/theory/sequences_rewriter_white.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Aina Niemetz, Andres Noetzli, Andrew Reynolds + * Andres Noetzli, Aina Niemetz, Andrew Reynolds * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/theory/strings_rewriter_white.cpp b/test/unit/theory/strings_rewriter_white.cpp index e868a2062..9236e0440 100644 --- a/test/unit/theory/strings_rewriter_white.cpp +++ b/test/unit/theory/strings_rewriter_white.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Aina Niemetz + * Aina Niemetz, Mathias Preiner * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/theory/theory_arith_coverings_white.cpp b/test/unit/theory/theory_arith_coverings_white.cpp index e4d4c1e09..cdc8282fb 100644 --- a/test/unit/theory/theory_arith_coverings_white.cpp +++ b/test/unit/theory/theory_arith_coverings_white.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Gereon Kremer + * Gereon Kremer, Andres Noetzli, Andrew Reynolds * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/theory/theory_arith_pow2_white.cpp b/test/unit/theory/theory_arith_pow2_white.cpp index 714eff579..1a60682bb 100644 --- a/test/unit/theory/theory_arith_pow2_white.cpp +++ b/test/unit/theory/theory_arith_pow2_white.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Yoni Zohar + * Yoni Zohar, Aina Niemetz, Andres Noetzli * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/theory/theory_arith_rewriter_black.cpp b/test/unit/theory/theory_arith_rewriter_black.cpp index 88af6b021..ec6277c14 100644 --- a/test/unit/theory/theory_arith_rewriter_black.cpp +++ b/test/unit/theory/theory_arith_rewriter_black.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Aina Niemetz + * Gereon Kremer, Aina Niemetz * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/theory/theory_arith_white.cpp b/test/unit/theory/theory_arith_white.cpp index a358e5b60..8285c07e1 100644 --- a/test/unit/theory/theory_arith_white.cpp +++ b/test/unit/theory/theory_arith_white.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Aina Niemetz, Tim King, Gereon Kremer + * Aina Niemetz, Andres Noetzli, Tim King * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/theory/theory_bags_normal_form_white.cpp b/test/unit/theory/theory_bags_normal_form_white.cpp index 469f532b0..37222a589 100644 --- a/test/unit/theory/theory_bags_normal_form_white.cpp +++ b/test/unit/theory/theory_bags_normal_form_white.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Aina Niemetz, Mudathir Mohamed + * Aina Niemetz, Andres Noetzli, Mudathir Mohamed * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/theory/theory_bags_rewriter_white.cpp b/test/unit/theory/theory_bags_rewriter_white.cpp index 0ef2a564b..121d26171 100644 --- a/test/unit/theory/theory_bags_rewriter_white.cpp +++ b/test/unit/theory/theory_bags_rewriter_white.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Aina Niemetz, Mudathir Mohamed, Andrew Reynolds + * Mudathir Mohamed, Aina Niemetz, Andres Noetzli * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/theory/theory_bags_type_rules_white.cpp b/test/unit/theory/theory_bags_type_rules_white.cpp index 815bcb67f..e98b248a8 100644 --- a/test/unit/theory/theory_bags_type_rules_white.cpp +++ b/test/unit/theory/theory_bags_type_rules_white.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Aina Niemetz, Mudathir Mohamed + * Aina Niemetz, Mudathir Mohamed, Andres Noetzli * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/theory/theory_black.cpp b/test/unit/theory/theory_black.cpp index de936112e..cd65445b8 100644 --- a/test/unit/theory/theory_black.cpp +++ b/test/unit/theory/theory_black.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Aina Niemetz + * Aina Niemetz, Andres Noetzli * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/theory/theory_bv_int_blaster_white.cpp b/test/unit/theory/theory_bv_int_blaster_white.cpp index ae96889ef..f1f3a4289 100644 --- a/test/unit/theory/theory_bv_int_blaster_white.cpp +++ b/test/unit/theory/theory_bv_int_blaster_white.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Yoni Zohar + * Yoni Zohar, Makai Mann, Andres Noetzli * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/theory/theory_bv_opt_white.cpp b/test/unit/theory/theory_bv_opt_white.cpp index d4deaab2c..dae852049 100644 --- a/test/unit/theory/theory_bv_opt_white.cpp +++ b/test/unit/theory/theory_bv_opt_white.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Yancheng Ou + * Yancheng Ou, Aina Niemetz, Michael Chang * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/theory/theory_bv_rewriter_white.cpp b/test/unit/theory/theory_bv_rewriter_white.cpp index c22bc3458..a3ca50346 100644 --- a/test/unit/theory/theory_bv_rewriter_white.cpp +++ b/test/unit/theory/theory_bv_rewriter_white.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Aina Niemetz + * Aina Niemetz, Andres Noetzli * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/theory/theory_bv_white.cpp b/test/unit/theory/theory_bv_white.cpp index 90ab3facd..6a6295a45 100644 --- a/test/unit/theory/theory_bv_white.cpp +++ b/test/unit/theory/theory_bv_white.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Aina Niemetz, Abdalrhman Mohamed, Mathias Preiner + * Aina Niemetz, Andrew Reynolds * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/theory/theory_engine_white.cpp b/test/unit/theory/theory_engine_white.cpp index 0f643397d..6a54baa30 100644 --- a/test/unit/theory/theory_engine_white.cpp +++ b/test/unit/theory/theory_engine_white.cpp @@ -4,7 +4,7 @@ * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/theory/theory_int_opt_white.cpp b/test/unit/theory/theory_int_opt_white.cpp index 40ecd376a..d6573f3a7 100644 --- a/test/unit/theory/theory_int_opt_white.cpp +++ b/test/unit/theory/theory_int_opt_white.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Michael Chang, Yancheng Ou + * Michael Chang, Yancheng Ou, Aina Niemetz * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/theory/theory_opt_multigoal_white.cpp b/test/unit/theory/theory_opt_multigoal_white.cpp index 0f46f6a6e..1c2fdc442 100644 --- a/test/unit/theory/theory_opt_multigoal_white.cpp +++ b/test/unit/theory/theory_opt_multigoal_white.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Yancheng Ou + * Yancheng Ou, Aina Niemetz, Andrew Reynolds * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/theory/theory_quantifiers_bv_instantiator_white.cpp b/test/unit/theory/theory_quantifiers_bv_instantiator_white.cpp index 249969b79..92f21d31c 100644 --- a/test/unit/theory/theory_quantifiers_bv_instantiator_white.cpp +++ b/test/unit/theory/theory_quantifiers_bv_instantiator_white.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Aina Niemetz, Mathias Preiner, Andres Noetzli + * Aina Niemetz, Mathias Preiner * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp b/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp index 528aadbc7..e6450c39b 100644 --- a/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp +++ b/test/unit/theory/theory_quantifiers_bv_inverter_white.cpp @@ -4,7 +4,7 @@ * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/theory/theory_sets_rewriter_white.cpp b/test/unit/theory/theory_sets_rewriter_white.cpp index 4d6fc035d..8a1af2667 100644 --- a/test/unit/theory/theory_sets_rewriter_white.cpp +++ b/test/unit/theory/theory_sets_rewriter_white.cpp @@ -4,7 +4,7 @@ * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/theory/theory_sets_type_enumerator_white.cpp b/test/unit/theory/theory_sets_type_enumerator_white.cpp index 2d8909e01..5402f668e 100644 --- a/test/unit/theory/theory_sets_type_enumerator_white.cpp +++ b/test/unit/theory/theory_sets_type_enumerator_white.cpp @@ -4,7 +4,7 @@ * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/theory/theory_sets_type_rules_white.cpp b/test/unit/theory/theory_sets_type_rules_white.cpp index f73311e34..c5b8a3bd3 100644 --- a/test/unit/theory/theory_sets_type_rules_white.cpp +++ b/test/unit/theory/theory_sets_type_rules_white.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Aina Niemetz, Mudathir Mohamed + * Aina Niemetz, Mudathir Mohamed, Mathias Preiner * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/theory/theory_strings_skolem_cache_black.cpp b/test/unit/theory/theory_strings_skolem_cache_black.cpp index e30912422..04742cfdb 100644 --- a/test/unit/theory/theory_strings_skolem_cache_black.cpp +++ b/test/unit/theory/theory_strings_skolem_cache_black.cpp @@ -4,7 +4,7 @@ * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/theory/theory_strings_utils_white.cpp b/test/unit/theory/theory_strings_utils_white.cpp index 4fef34066..300864afe 100644 --- a/test/unit/theory/theory_strings_utils_white.cpp +++ b/test/unit/theory/theory_strings_utils_white.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Andres Noetzli + * Andres Noetzli, Mathias Preiner * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/theory/theory_strings_word_white.cpp b/test/unit/theory/theory_strings_word_white.cpp index 6ee23cc56..570821e1b 100644 --- a/test/unit/theory/theory_strings_word_white.cpp +++ b/test/unit/theory/theory_strings_word_white.cpp @@ -4,7 +4,7 @@ * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/theory/theory_white.cpp b/test/unit/theory/theory_white.cpp index d9f22b11e..635815abb 100644 --- a/test/unit/theory/theory_white.cpp +++ b/test/unit/theory/theory_white.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Aina Niemetz, Dejan Jovanovic + * Aina Niemetz, Dejan Jovanovic, Gereon Kremer * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/theory/type_enumerator_white.cpp b/test/unit/theory/type_enumerator_white.cpp index 2fbd5bbd9..745df9a41 100644 --- a/test/unit/theory/type_enumerator_white.cpp +++ b/test/unit/theory/type_enumerator_white.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Aina Niemetz, Andrew Reynolds, Morgan Deters + * Aina Niemetz, Andres Noetzli, Andrew Reynolds * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/util/CMakeLists.txt b/test/unit/util/CMakeLists.txt index 03348f6e1..cd72b3fee 100644 --- a/test/unit/util/CMakeLists.txt +++ b/test/unit/util/CMakeLists.txt @@ -1,10 +1,10 @@ ############################################################################### # Top contributors (to current version): -# Aina Niemetz, Yoni Zohar, Gereon Kremer +# Mathias Preiner, Gereon Kremer, Aina Niemetz # # This file is part of the cvc5 project. # -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS +# Copyright (c) 2009-2022 by the authors listed in the file AUTHORS # in the top-level source directory and their institutional affiliations. # All rights reserved. See the file COPYING in the top-level source # directory for licensing information. diff --git a/test/unit/util/array_store_all_white.cpp b/test/unit/util/array_store_all_white.cpp index 0ceb256be..0f4016698 100644 --- a/test/unit/util/array_store_all_white.cpp +++ b/test/unit/util/array_store_all_white.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Aina Niemetz + * Aina Niemetz, Andres Noetzli, Mathias Preiner * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/util/assert_white.cpp b/test/unit/util/assert_white.cpp index 28fdbecb9..665f8c851 100644 --- a/test/unit/util/assert_white.cpp +++ b/test/unit/util/assert_white.cpp @@ -4,7 +4,7 @@ * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/util/binary_heap_black.cpp b/test/unit/util/binary_heap_black.cpp index 3de0d2047..fba7a7acd 100644 --- a/test/unit/util/binary_heap_black.cpp +++ b/test/unit/util/binary_heap_black.cpp @@ -4,7 +4,7 @@ * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/util/bitvector_black.cpp b/test/unit/util/bitvector_black.cpp index 967e8b347..83dfcb71d 100644 --- a/test/unit/util/bitvector_black.cpp +++ b/test/unit/util/bitvector_black.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Aina Niemetz + * Aina Niemetz, Alex Ozdemir * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/util/boolean_simplification_black.cpp b/test/unit/util/boolean_simplification_black.cpp index 28fc06f7b..f6d48b7d2 100644 --- a/test/unit/util/boolean_simplification_black.cpp +++ b/test/unit/util/boolean_simplification_black.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Aina Niemetz, Morgan Deters, Andrew Reynolds + * Aina Niemetz, Andres Noetzli, Andrew Reynolds * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/util/cardinality_black.cpp b/test/unit/util/cardinality_black.cpp index 7f8f31c9c..7b8ec172b 100644 --- a/test/unit/util/cardinality_black.cpp +++ b/test/unit/util/cardinality_black.cpp @@ -4,7 +4,7 @@ * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/util/check_white.cpp b/test/unit/util/check_white.cpp index 15d2371fa..b331fe97f 100644 --- a/test/unit/util/check_white.cpp +++ b/test/unit/util/check_white.cpp @@ -4,7 +4,7 @@ * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/util/configuration_black.cpp b/test/unit/util/configuration_black.cpp index 237aec700..f0d51aa6d 100644 --- a/test/unit/util/configuration_black.cpp +++ b/test/unit/util/configuration_black.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Morgan Deters, Aina Niemetz + * Aina Niemetz, Morgan Deters, Mathias Preiner * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/util/datatype_black.cpp b/test/unit/util/datatype_black.cpp index b3ad83f83..da41b41e6 100644 --- a/test/unit/util/datatype_black.cpp +++ b/test/unit/util/datatype_black.cpp @@ -4,7 +4,7 @@ * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/util/didyoumean_black.cpp b/test/unit/util/didyoumean_black.cpp index d60fed62f..bc927f417 100644 --- a/test/unit/util/didyoumean_black.cpp +++ b/test/unit/util/didyoumean_black.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Aina Niemetz, Andres Noetzli, Gereon Kremer + * Gereon Kremer * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/util/exception_black.cpp b/test/unit/util/exception_black.cpp index c8f0ab05f..cff49aab9 100644 --- a/test/unit/util/exception_black.cpp +++ b/test/unit/util/exception_black.cpp @@ -4,7 +4,7 @@ * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/util/floatingpoint_black.cpp b/test/unit/util/floatingpoint_black.cpp index 09d934f63..df6375533 100644 --- a/test/unit/util/floatingpoint_black.cpp +++ b/test/unit/util/floatingpoint_black.cpp @@ -4,7 +4,7 @@ * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/util/integer_black.cpp b/test/unit/util/integer_black.cpp index 4b11ad7f4..be62b8659 100644 --- a/test/unit/util/integer_black.cpp +++ b/test/unit/util/integer_black.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Aina Niemetz, Tim King + * Aina Niemetz, Tim King, Gereon Kremer * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/util/integer_white.cpp b/test/unit/util/integer_white.cpp index 92426d6cb..e5410de02 100644 --- a/test/unit/util/integer_white.cpp +++ b/test/unit/util/integer_white.cpp @@ -4,7 +4,7 @@ * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/util/output_black.cpp b/test/unit/util/output_black.cpp index 5b26a3624..4b179ff03 100644 --- a/test/unit/util/output_black.cpp +++ b/test/unit/util/output_black.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Aina Niemetz, Morgan Deters, Mathias Preiner + * Aina Niemetz, Gereon Kremer, Morgan Deters * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/util/rational_black.cpp b/test/unit/util/rational_black.cpp index 442c89a9b..0b10bef2a 100644 --- a/test/unit/util/rational_black.cpp +++ b/test/unit/util/rational_black.cpp @@ -4,7 +4,7 @@ * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/util/rational_white.cpp b/test/unit/util/rational_white.cpp index 2b05cf5c4..534f90bc8 100644 --- a/test/unit/util/rational_white.cpp +++ b/test/unit/util/rational_white.cpp @@ -4,7 +4,7 @@ * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/util/real_algebraic_number_black.cpp b/test/unit/util/real_algebraic_number_black.cpp index b90e8d364..45f33707c 100644 --- a/test/unit/util/real_algebraic_number_black.cpp +++ b/test/unit/util/real_algebraic_number_black.cpp @@ -4,7 +4,7 @@ * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. diff --git a/test/unit/util/stats_black.cpp b/test/unit/util/stats_black.cpp index cf01d39d6..21886dbd8 100644 --- a/test/unit/util/stats_black.cpp +++ b/test/unit/util/stats_black.cpp @@ -1,10 +1,10 @@ /****************************************************************************** * Top contributors (to current version): - * Aina Niemetz, Andres Noetzli, Gereon Kremer + * Gereon Kremer, Aina Niemetz * * This file is part of the cvc5 project. * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * Copyright (c) 2009-2022 by the authors listed in the file AUTHORS * in the top-level source directory and their institutional affiliations. * All rights reserved. See the file COPYING in the top-level source * directory for licensing information. -- 2.30.2