diff --git a/examples/lib_usage.ml b/examples/lib_usage.ml index b753cc537..eaa8ed329 100644 --- a/examples/lib_usage.ml +++ b/examples/lib_usage.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/licenses/free-header.txt b/licenses/free-header.txt index e9902cace..1fad4fbce 100644 --- a/licenses/free-header.txt +++ b/licenses/free-header.txt @@ -1,6 +1,6 @@ Alt-Ergo: The SMT Solver For Software Verification - Copyright (C) 2013-2024 --- OCamlPro SAS + Copyright (C) --- OCamlPro SAS This is an exceptional free release of Alt-Ergo dual-licensed under the OCamlPro-Non-Commercial-License and diff --git a/licenses/header.txt b/licenses/header.txt index e491f1d72..08eb03611 100644 --- a/licenses/header.txt +++ b/licenses/header.txt @@ -1,6 +1,6 @@ Alt-Ergo: The SMT Solver For Software Verification - Copyright (C) 2013-2024 --- OCamlPro SAS + Copyright (C) --- OCamlPro SAS This file is distributed under the terms of OCamlPro Non-Commercial Purpose License, version 1. @@ -11,14 +11,5 @@ --------------------------------------------------------------- - The Alt-Ergo theorem prover - - Sylvain Conchon, Evelyne Contejean, Francois Bobot - Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout - - CNRS - INRIA - Universite Paris Sud - - --------------------------------------------------------------- - More details can be found in the directory licenses/ diff --git a/licenses/old-header.txt b/licenses/old-header.txt new file mode 100644 index 000000000..afce6f13d --- /dev/null +++ b/licenses/old-header.txt @@ -0,0 +1,24 @@ + + Alt-Ergo: The SMT Solver For Software Verification + Copyright (C) --- OCamlPro SAS + + This file is distributed under the terms of OCamlPro + Non-Commercial Purpose License, version 1. + + As an exception, Alt-Ergo Club members at the Gold level can + use this file under the terms of the Apache Software License + version 2.0. + + --------------------------------------------------------------- + + The Alt-Ergo theorem prover + + Sylvain Conchon, Evelyne Contejean, Francois Bobot + Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout + + CNRS - INRIA - Universite Paris Sud + + --------------------------------------------------------------- + + More details can be found in the directory licenses/ + diff --git a/rsc/extra/headers/alt-ergo_header_ocamlpro.txt b/rsc/extra/headers/alt-ergo_header_ocamlpro.txt index e636c5a03..8d56dd67f 100644 --- a/rsc/extra/headers/alt-ergo_header_ocamlpro.txt +++ b/rsc/extra/headers/alt-ergo_header_ocamlpro.txt @@ -1,8 +1,8 @@ - - Alt-Ergo: The SMT Solver For Software Verification - Copyright (C) 2013-2017 --- OCamlPro SAS - + + Alt-Ergo: The SMT Solver For Software Verification + Copyright (C) 2013-2017 --- OCamlPro SAS + This file is distributed under the terms of the license indicated in the file 'License.OCamlPro'. If 'License.OCamlPro' is not present, please contact us to clarify licensing. - + diff --git a/rsc/extra/ocamldot/ocamldot.mll b/rsc/extra/ocamldot/ocamldot.mll index 64427bf38..dab5d447d 100644 --- a/rsc/extra/ocamldot/ocamldot.mll +++ b/rsc/extra/ocamldot/ocamldot.mll @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/rsc/extra/ocpchecker/ocp_checker.ml b/rsc/extra/ocpchecker/ocp_checker.ml index 840d5b2c8..a2893a0fd 100644 --- a/rsc/extra/ocpchecker/ocp_checker.ml +++ b/rsc/extra/ocpchecker/ocp_checker.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/bin/common/config.ml b/src/bin/common/config.ml index c68e805f6..70f0c4388 100644 --- a/src/bin/common/config.ml +++ b/src/bin/common/config.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/bin/common/input_frontend.ml b/src/bin/common/input_frontend.ml index 61fbfe256..93a498290 100644 --- a/src/bin/common/input_frontend.ml +++ b/src/bin/common/input_frontend.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/bin/common/input_frontend.mli b/src/bin/common/input_frontend.mli index cf28b0af4..3d1d9284b 100644 --- a/src/bin/common/input_frontend.mli +++ b/src/bin/common/input_frontend.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/bin/common/myDynlink.ml b/src/bin/common/myDynlink.ml index 2bfa44e0e..209e32e7d 100644 --- a/src/bin/common/myDynlink.ml +++ b/src/bin/common/myDynlink.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/bin/common/myDynlink.mli b/src/bin/common/myDynlink.mli index fe548a206..fa8f32182 100644 --- a/src/bin/common/myDynlink.mli +++ b/src/bin/common/myDynlink.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/bin/common/parse_command.ml b/src/bin/common/parse_command.ml index 72aec20d1..964b9dc76 100644 --- a/src/bin/common/parse_command.ml +++ b/src/bin/common/parse_command.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/bin/common/parse_command.mli b/src/bin/common/parse_command.mli index 6dc9a254c..d0423c22d 100644 --- a/src/bin/common/parse_command.mli +++ b/src/bin/common/parse_command.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/bin/common/signals_profiling.ml b/src/bin/common/signals_profiling.ml index 49ee39a8f..ba4439fca 100644 --- a/src/bin/common/signals_profiling.ml +++ b/src/bin/common/signals_profiling.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/bin/common/signals_profiling.mli b/src/bin/common/signals_profiling.mli index 73129dc14..c4bd50ea1 100644 --- a/src/bin/common/signals_profiling.mli +++ b/src/bin/common/signals_profiling.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/bin/common/solving_loop.ml b/src/bin/common/solving_loop.ml index 16d21904b..80e4da051 100644 --- a/src/bin/common/solving_loop.ml +++ b/src/bin/common/solving_loop.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/bin/common/solving_loop.mli b/src/bin/common/solving_loop.mli index b98b57cc4..cc4791656 100644 --- a/src/bin/common/solving_loop.mli +++ b/src/bin/common/solving_loop.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/bin/js/main_text_js.ml b/src/bin/js/main_text_js.ml index fde7c12d1..dcd118cd3 100644 --- a/src/bin/js/main_text_js.ml +++ b/src/bin/js/main_text_js.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/bin/js/options_interface.ml b/src/bin/js/options_interface.ml index 1e7495f00..1b5ffc870 100644 --- a/src/bin/js/options_interface.ml +++ b/src/bin/js/options_interface.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/bin/js/options_interface.mli b/src/bin/js/options_interface.mli index b9d879257..faa5d5df9 100644 --- a/src/bin/js/options_interface.mli +++ b/src/bin/js/options_interface.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/bin/js/worker_example.ml b/src/bin/js/worker_example.ml index c940136fc..7690eb839 100644 --- a/src/bin/js/worker_example.ml +++ b/src/bin/js/worker_example.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/bin/js/worker_interface.ml b/src/bin/js/worker_interface.ml index 4db8c6df4..00cf8362b 100644 --- a/src/bin/js/worker_interface.ml +++ b/src/bin/js/worker_interface.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/bin/js/worker_interface.mli b/src/bin/js/worker_interface.mli index 97774ee38..31cf87017 100644 --- a/src/bin/js/worker_interface.mli +++ b/src/bin/js/worker_interface.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/bin/js/worker_js.ml b/src/bin/js/worker_js.ml index e6d46dc25..4d79920db 100644 --- a/src/bin/js/worker_js.ml +++ b/src/bin/js/worker_js.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/bin/text/main_text.ml b/src/bin/text/main_text.ml index 2592ee2e9..ee4860fad 100644 --- a/src/bin/text/main_text.ml +++ b/src/bin/text/main_text.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/bin/text/main_text.mli b/src/bin/text/main_text.mli index 4cc4779e0..d1fe33fd0 100644 --- a/src/bin/text/main_text.mli +++ b/src/bin/text/main_text.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/frontend/cnf.ml b/src/lib/frontend/cnf.ml index 7e46fb420..687f4f600 100644 --- a/src/lib/frontend/cnf.ml +++ b/src/lib/frontend/cnf.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/frontend/cnf.mli b/src/lib/frontend/cnf.mli index 81048d3da..1ad8054be 100644 --- a/src/lib/frontend/cnf.mli +++ b/src/lib/frontend/cnf.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/frontend/d_cnf.ml b/src/lib/frontend/d_cnf.ml index 0aed56e5f..76c0ec75f 100644 --- a/src/lib/frontend/d_cnf.ml +++ b/src/lib/frontend/d_cnf.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) @@ -12,15 +12,6 @@ (* *) (* --------------------------------------------------------------- *) (* *) -(* The Alt-Ergo theorem prover *) -(* *) -(* Sylvain Conchon, Evelyne Contejean, Francois Bobot *) -(* Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout *) -(* *) -(* CNRS - INRIA - Universite Paris Sud *) -(* *) -(* --------------------------------------------------------------- *) -(* *) (* More details can be found in the directory licenses/ *) (* *) (**************************************************************************) diff --git a/src/lib/frontend/d_cnf.mli b/src/lib/frontend/d_cnf.mli index 6e8ee8b37..abb36451c 100644 --- a/src/lib/frontend/d_cnf.mli +++ b/src/lib/frontend/d_cnf.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) @@ -12,15 +12,6 @@ (* *) (* --------------------------------------------------------------- *) (* *) -(* The Alt-Ergo theorem prover *) -(* *) -(* Sylvain Conchon, Evelyne Contejean, Francois Bobot *) -(* Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout *) -(* *) -(* CNRS - INRIA - Universite Paris Sud *) -(* *) -(* --------------------------------------------------------------- *) -(* *) (* More details can be found in the directory licenses/ *) (* *) (**************************************************************************) diff --git a/src/lib/frontend/d_loop.ml b/src/lib/frontend/d_loop.ml index 4cd23c0e7..c11592a12 100644 --- a/src/lib/frontend/d_loop.ml +++ b/src/lib/frontend/d_loop.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) 2022-2024 --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) @@ -12,15 +12,6 @@ (* *) (* --------------------------------------------------------------- *) (* *) -(* The Alt-Ergo theorem prover *) -(* *) -(* Sylvain Conchon, Evelyne Contejean, Francois Bobot *) -(* Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout *) -(* *) -(* CNRS - INRIA - Universite Paris Sud *) -(* *) -(* --------------------------------------------------------------- *) -(* *) (* More details can be found in the directory licenses/ *) (* *) (**************************************************************************) diff --git a/src/lib/frontend/d_state_option.ml b/src/lib/frontend/d_state_option.ml index 967e8234b..d655bfcd3 100644 --- a/src/lib/frontend/d_state_option.ml +++ b/src/lib/frontend/d_state_option.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) 2022-2024 --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) @@ -12,15 +12,6 @@ (* *) (* --------------------------------------------------------------- *) (* *) -(* The Alt-Ergo theorem prover *) -(* *) -(* Sylvain Conchon, Evelyne Contejean, Francois Bobot *) -(* Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout *) -(* *) -(* CNRS - INRIA - Universite Paris Sud *) -(* *) -(* --------------------------------------------------------------- *) -(* *) (* More details can be found in the directory licenses/ *) (* *) (**************************************************************************) diff --git a/src/lib/frontend/d_state_option.mli b/src/lib/frontend/d_state_option.mli index 0b8d50a4b..1c31f6ddf 100644 --- a/src/lib/frontend/d_state_option.mli +++ b/src/lib/frontend/d_state_option.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) 2022-2024 --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) @@ -12,15 +12,6 @@ (* *) (* --------------------------------------------------------------- *) (* *) -(* The Alt-Ergo theorem prover *) -(* *) -(* Sylvain Conchon, Evelyne Contejean, Francois Bobot *) -(* Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout *) -(* *) -(* CNRS - INRIA - Universite Paris Sud *) -(* *) -(* --------------------------------------------------------------- *) -(* *) (* More details can be found in the directory licenses/ *) (* *) (**************************************************************************) diff --git a/src/lib/frontend/frontend.ml b/src/lib/frontend/frontend.ml index 2ad207956..d2d437024 100644 --- a/src/lib/frontend/frontend.ml +++ b/src/lib/frontend/frontend.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/frontend/frontend.mli b/src/lib/frontend/frontend.mli index 51114b18f..ec4401d02 100644 --- a/src/lib/frontend/frontend.mli +++ b/src/lib/frontend/frontend.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/frontend/input.ml b/src/lib/frontend/input.ml index 1c29b15c8..09d0f7c62 100644 --- a/src/lib/frontend/input.ml +++ b/src/lib/frontend/input.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/frontend/input.mli b/src/lib/frontend/input.mli index 3fcb67228..28a9355e0 100644 --- a/src/lib/frontend/input.mli +++ b/src/lib/frontend/input.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/frontend/models.ml b/src/lib/frontend/models.ml index 7b39d1bc6..8c885caac 100644 --- a/src/lib/frontend/models.ml +++ b/src/lib/frontend/models.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) @@ -12,15 +12,6 @@ (* *) (* --------------------------------------------------------------- *) (* *) -(* The Alt-Ergo theorem prover *) -(* *) -(* Sylvain Conchon, Evelyne Contejean, Francois Bobot *) -(* Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout *) -(* *) -(* CNRS - INRIA - Universite Paris Sud *) -(* *) -(* --------------------------------------------------------------- *) -(* *) (* More details can be found in the directory licenses/ *) (* *) (**************************************************************************) diff --git a/src/lib/frontend/models.mli b/src/lib/frontend/models.mli index 01446b215..75b21ef84 100644 --- a/src/lib/frontend/models.mli +++ b/src/lib/frontend/models.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) 2022-2024 --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) @@ -12,15 +12,6 @@ (* *) (* --------------------------------------------------------------- *) (* *) -(* The Alt-Ergo theorem prover *) -(* *) -(* Sylvain Conchon, Evelyne Contejean, Francois Bobot *) -(* Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout *) -(* *) -(* CNRS - INRIA - Universite Paris Sud *) -(* *) -(* --------------------------------------------------------------- *) -(* *) (* More details can be found in the directory licenses/ *) (* *) (**************************************************************************) diff --git a/src/lib/frontend/parsed_interface.ml b/src/lib/frontend/parsed_interface.ml index 48ab8e5b5..c34012d9b 100644 --- a/src/lib/frontend/parsed_interface.ml +++ b/src/lib/frontend/parsed_interface.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/frontend/parsed_interface.mli b/src/lib/frontend/parsed_interface.mli index 7c76454a3..ea45881c2 100644 --- a/src/lib/frontend/parsed_interface.mli +++ b/src/lib/frontend/parsed_interface.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/frontend/typechecker.ml b/src/lib/frontend/typechecker.ml index 7619b28c4..afdf3c048 100644 --- a/src/lib/frontend/typechecker.ml +++ b/src/lib/frontend/typechecker.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/frontend/typechecker.mli b/src/lib/frontend/typechecker.mli index fab9d0f07..d5337fa95 100644 --- a/src/lib/frontend/typechecker.mli +++ b/src/lib/frontend/typechecker.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/reasoners/ac.ml b/src/lib/reasoners/ac.ml index 8773ca4ac..95645ba25 100644 --- a/src/lib/reasoners/ac.ml +++ b/src/lib/reasoners/ac.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/reasoners/ac.mli b/src/lib/reasoners/ac.mli index 1219fb9f6..992118898 100644 --- a/src/lib/reasoners/ac.mli +++ b/src/lib/reasoners/ac.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/reasoners/adt.ml b/src/lib/reasoners/adt.ml index 8ce4dad0a..3d0522fc3 100644 --- a/src/lib/reasoners/adt.ml +++ b/src/lib/reasoners/adt.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/reasoners/adt.mli b/src/lib/reasoners/adt.mli index 81d7267b5..fea79eb1e 100644 --- a/src/lib/reasoners/adt.mli +++ b/src/lib/reasoners/adt.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/reasoners/adt_rel.ml b/src/lib/reasoners/adt_rel.ml index bc6dbd60f..6355fd1a0 100644 --- a/src/lib/reasoners/adt_rel.ml +++ b/src/lib/reasoners/adt_rel.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/reasoners/adt_rel.mli b/src/lib/reasoners/adt_rel.mli index 71cfa717c..f68d130ca 100644 --- a/src/lib/reasoners/adt_rel.mli +++ b/src/lib/reasoners/adt_rel.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/reasoners/arith.ml b/src/lib/reasoners/arith.ml index 2a0b2bbeb..01ab0206e 100644 --- a/src/lib/reasoners/arith.ml +++ b/src/lib/reasoners/arith.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/reasoners/arith.mli b/src/lib/reasoners/arith.mli index 0ae71c7bc..ce95a86b2 100644 --- a/src/lib/reasoners/arith.mli +++ b/src/lib/reasoners/arith.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/reasoners/arrays_rel.ml b/src/lib/reasoners/arrays_rel.ml index eee96ab00..9e7ec07ff 100644 --- a/src/lib/reasoners/arrays_rel.ml +++ b/src/lib/reasoners/arrays_rel.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/reasoners/arrays_rel.mli b/src/lib/reasoners/arrays_rel.mli index 71cfa717c..f68d130ca 100644 --- a/src/lib/reasoners/arrays_rel.mli +++ b/src/lib/reasoners/arrays_rel.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/reasoners/bitlist.ml b/src/lib/reasoners/bitlist.ml index a663b106f..eb6d7102e 100644 --- a/src/lib/reasoners/bitlist.ml +++ b/src/lib/reasoners/bitlist.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) @@ -12,15 +12,6 @@ (* *) (* --------------------------------------------------------------- *) (* *) -(* The Alt-Ergo theorem prover *) -(* *) -(* Sylvain Conchon, Evelyne Contejean, Francois Bobot *) -(* Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout *) -(* *) -(* CNRS - INRIA - Universite Paris Sud *) -(* *) -(* --------------------------------------------------------------- *) -(* *) (* More details can be found in the directory licenses/ *) (* *) (**************************************************************************) diff --git a/src/lib/reasoners/bitlist.mli b/src/lib/reasoners/bitlist.mli index 3ba3ee19d..15e96a600 100644 --- a/src/lib/reasoners/bitlist.mli +++ b/src/lib/reasoners/bitlist.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) @@ -12,15 +12,6 @@ (* *) (* --------------------------------------------------------------- *) (* *) -(* The Alt-Ergo theorem prover *) -(* *) -(* Sylvain Conchon, Evelyne Contejean, Francois Bobot *) -(* Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout *) -(* *) -(* CNRS - INRIA - Universite Paris Sud *) -(* *) -(* --------------------------------------------------------------- *) -(* *) (* More details can be found in the directory licenses/ *) (* *) (**************************************************************************) diff --git a/src/lib/reasoners/bitv.ml b/src/lib/reasoners/bitv.ml index f79165947..c877db96a 100644 --- a/src/lib/reasoners/bitv.ml +++ b/src/lib/reasoners/bitv.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/reasoners/bitv.mli b/src/lib/reasoners/bitv.mli index b0c25c7f9..3b5064cb1 100644 --- a/src/lib/reasoners/bitv.mli +++ b/src/lib/reasoners/bitv.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/reasoners/bitv_rel.ml b/src/lib/reasoners/bitv_rel.ml index c72a450c4..866517318 100644 --- a/src/lib/reasoners/bitv_rel.ml +++ b/src/lib/reasoners/bitv_rel.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) @@ -12,15 +12,6 @@ (* *) (* --------------------------------------------------------------- *) (* *) -(* The Alt-Ergo theorem prover *) -(* *) -(* Sylvain Conchon, Evelyne Contejean, Francois Bobot *) -(* Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout *) -(* *) -(* CNRS - INRIA - Universite Paris Sud *) -(* *) -(* --------------------------------------------------------------- *) -(* *) (* More details can be found in the directory licenses/ *) (* *) (**************************************************************************) diff --git a/src/lib/reasoners/bitv_rel.mli b/src/lib/reasoners/bitv_rel.mli index d3946e42d..ffd2a6ce0 100644 --- a/src/lib/reasoners/bitv_rel.mli +++ b/src/lib/reasoners/bitv_rel.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) @@ -12,15 +12,6 @@ (* *) (* --------------------------------------------------------------- *) (* *) -(* The Alt-Ergo theorem prover *) -(* *) -(* Sylvain Conchon, Evelyne Contejean, Francois Bobot *) -(* Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout *) -(* *) -(* CNRS - INRIA - Universite Paris Sud *) -(* *) -(* --------------------------------------------------------------- *) -(* *) (* More details can be found in the directory licenses/ *) (* *) (**************************************************************************) diff --git a/src/lib/reasoners/ccx.ml b/src/lib/reasoners/ccx.ml index cdd871f51..5642c89d4 100644 --- a/src/lib/reasoners/ccx.ml +++ b/src/lib/reasoners/ccx.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/reasoners/ccx.mli b/src/lib/reasoners/ccx.mli index cf835774b..c121d46c3 100644 --- a/src/lib/reasoners/ccx.mli +++ b/src/lib/reasoners/ccx.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/reasoners/fun_sat.ml b/src/lib/reasoners/fun_sat.ml index 43230d58b..d382b2f3b 100644 --- a/src/lib/reasoners/fun_sat.ml +++ b/src/lib/reasoners/fun_sat.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/reasoners/fun_sat.mli b/src/lib/reasoners/fun_sat.mli index ed66906ce..2ecf02fa1 100644 --- a/src/lib/reasoners/fun_sat.mli +++ b/src/lib/reasoners/fun_sat.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/reasoners/fun_sat_frontend.ml b/src/lib/reasoners/fun_sat_frontend.ml index fc3f792da..abeb97259 100644 --- a/src/lib/reasoners/fun_sat_frontend.ml +++ b/src/lib/reasoners/fun_sat_frontend.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) 2022-2024 --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) @@ -12,15 +12,6 @@ (* *) (* --------------------------------------------------------------- *) (* *) -(* The Alt-Ergo theorem prover *) -(* *) -(* Sylvain Conchon, Evelyne Contejean, Francois Bobot *) -(* Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout *) -(* *) -(* CNRS - INRIA - Universite Paris Sud *) -(* *) -(* --------------------------------------------------------------- *) -(* *) (* More details can be found in the directory licenses/ *) (* *) (**************************************************************************) diff --git a/src/lib/reasoners/fun_sat_frontend.mli b/src/lib/reasoners/fun_sat_frontend.mli index 85f61900f..969066852 100644 --- a/src/lib/reasoners/fun_sat_frontend.mli +++ b/src/lib/reasoners/fun_sat_frontend.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) @@ -12,15 +12,6 @@ (* *) (* --------------------------------------------------------------- *) (* *) -(* The Alt-Ergo theorem prover *) -(* *) -(* Sylvain Conchon, Evelyne Contejean, Francois Bobot *) -(* Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout *) -(* *) -(* CNRS - INRIA - Universite Paris Sud *) -(* *) -(* --------------------------------------------------------------- *) -(* *) (* More details can be found in the directory licenses/ *) (* *) (**************************************************************************) diff --git a/src/lib/reasoners/inequalities.ml b/src/lib/reasoners/inequalities.ml index 19ac2bb96..9eb3edcf0 100644 --- a/src/lib/reasoners/inequalities.ml +++ b/src/lib/reasoners/inequalities.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/reasoners/inequalities.mli b/src/lib/reasoners/inequalities.mli index f4ed0dbe4..9bd5a58ec 100644 --- a/src/lib/reasoners/inequalities.mli +++ b/src/lib/reasoners/inequalities.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/reasoners/instances.ml b/src/lib/reasoners/instances.ml index 630122687..6f9f7af11 100644 --- a/src/lib/reasoners/instances.ml +++ b/src/lib/reasoners/instances.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/reasoners/instances.mli b/src/lib/reasoners/instances.mli index 1b8112f53..75749ad9a 100644 --- a/src/lib/reasoners/instances.mli +++ b/src/lib/reasoners/instances.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/reasoners/intervalCalculus.ml b/src/lib/reasoners/intervalCalculus.ml index 6e6f95c30..aeb8ca415 100644 --- a/src/lib/reasoners/intervalCalculus.ml +++ b/src/lib/reasoners/intervalCalculus.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/reasoners/intervalCalculus.mli b/src/lib/reasoners/intervalCalculus.mli index 876ede9a0..e1c92cf9f 100644 --- a/src/lib/reasoners/intervalCalculus.mli +++ b/src/lib/reasoners/intervalCalculus.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/reasoners/intervals.ml b/src/lib/reasoners/intervals.ml index 306965467..243e1ca45 100644 --- a/src/lib/reasoners/intervals.ml +++ b/src/lib/reasoners/intervals.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/reasoners/intervals.mli b/src/lib/reasoners/intervals.mli index 3bf1ed2e4..04b7b569e 100644 --- a/src/lib/reasoners/intervals.mli +++ b/src/lib/reasoners/intervals.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/reasoners/intervals_intf.ml b/src/lib/reasoners/intervals_intf.ml index fafea1a00..8a3990e2b 100644 --- a/src/lib/reasoners/intervals_intf.ml +++ b/src/lib/reasoners/intervals_intf.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2023 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/reasoners/ite_rel.ml b/src/lib/reasoners/ite_rel.ml index bdd889c52..2d7c90759 100644 --- a/src/lib/reasoners/ite_rel.ml +++ b/src/lib/reasoners/ite_rel.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/reasoners/ite_rel.mli b/src/lib/reasoners/ite_rel.mli index 71cfa717c..f68d130ca 100644 --- a/src/lib/reasoners/ite_rel.mli +++ b/src/lib/reasoners/ite_rel.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/reasoners/matching.ml b/src/lib/reasoners/matching.ml index fcbded8c9..e7faf625e 100644 --- a/src/lib/reasoners/matching.ml +++ b/src/lib/reasoners/matching.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/reasoners/matching.mli b/src/lib/reasoners/matching.mli index 979527735..ac57eac60 100644 --- a/src/lib/reasoners/matching.mli +++ b/src/lib/reasoners/matching.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/reasoners/matching_types.mli b/src/lib/reasoners/matching_types.mli index 75917f115..554892ec7 100644 --- a/src/lib/reasoners/matching_types.mli +++ b/src/lib/reasoners/matching_types.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/reasoners/polynome.ml b/src/lib/reasoners/polynome.ml index aace67b6e..a189b0971 100644 --- a/src/lib/reasoners/polynome.ml +++ b/src/lib/reasoners/polynome.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/reasoners/polynome.mli b/src/lib/reasoners/polynome.mli index e1851da14..fdcfff5e6 100644 --- a/src/lib/reasoners/polynome.mli +++ b/src/lib/reasoners/polynome.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/reasoners/records.ml b/src/lib/reasoners/records.ml index 350d42420..0dc89702e 100644 --- a/src/lib/reasoners/records.ml +++ b/src/lib/reasoners/records.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/reasoners/records.mli b/src/lib/reasoners/records.mli index 77451e0f0..4283685e5 100644 --- a/src/lib/reasoners/records.mli +++ b/src/lib/reasoners/records.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/reasoners/records_rel.ml b/src/lib/reasoners/records_rel.ml index 7951d9085..0463fac01 100644 --- a/src/lib/reasoners/records_rel.ml +++ b/src/lib/reasoners/records_rel.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/reasoners/records_rel.mli b/src/lib/reasoners/records_rel.mli index 71cfa717c..f68d130ca 100644 --- a/src/lib/reasoners/records_rel.mli +++ b/src/lib/reasoners/records_rel.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/reasoners/rel_utils.ml b/src/lib/reasoners/rel_utils.ml index 762047102..5bf0b2ee1 100644 --- a/src/lib/reasoners/rel_utils.ml +++ b/src/lib/reasoners/rel_utils.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) @@ -12,15 +12,6 @@ (* *) (* --------------------------------------------------------------- *) (* *) -(* The Alt-Ergo theorem prover *) -(* *) -(* Sylvain Conchon, Evelyne Contejean, Francois Bobot *) -(* Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout *) -(* *) -(* CNRS - INRIA - Universite Paris Sud *) -(* *) -(* --------------------------------------------------------------- *) -(* *) (* More details can be found in the directory licenses/ *) (* *) (**************************************************************************) diff --git a/src/lib/reasoners/relation.ml b/src/lib/reasoners/relation.ml index 12971f1ce..d36a88526 100644 --- a/src/lib/reasoners/relation.ml +++ b/src/lib/reasoners/relation.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/reasoners/relation.mli b/src/lib/reasoners/relation.mli index 71cfa717c..f68d130ca 100644 --- a/src/lib/reasoners/relation.mli +++ b/src/lib/reasoners/relation.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/reasoners/sat_solver.ml b/src/lib/reasoners/sat_solver.ml index 2af2ef929..3849bcf76 100644 --- a/src/lib/reasoners/sat_solver.ml +++ b/src/lib/reasoners/sat_solver.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/reasoners/sat_solver.mli b/src/lib/reasoners/sat_solver.mli index 7e823f990..9dcc4a08c 100644 --- a/src/lib/reasoners/sat_solver.mli +++ b/src/lib/reasoners/sat_solver.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/reasoners/sat_solver_sig.ml b/src/lib/reasoners/sat_solver_sig.ml index 2503604b7..7cd83c09d 100644 --- a/src/lib/reasoners/sat_solver_sig.ml +++ b/src/lib/reasoners/sat_solver_sig.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/reasoners/sat_solver_sig.mli b/src/lib/reasoners/sat_solver_sig.mli index eb6ed3836..08ee926fc 100644 --- a/src/lib/reasoners/sat_solver_sig.mli +++ b/src/lib/reasoners/sat_solver_sig.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/reasoners/satml.ml b/src/lib/reasoners/satml.ml index 9502b3726..8dde0fe60 100644 --- a/src/lib/reasoners/satml.ml +++ b/src/lib/reasoners/satml.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/reasoners/satml.mli b/src/lib/reasoners/satml.mli index 78ee0da0e..8772104d0 100644 --- a/src/lib/reasoners/satml.mli +++ b/src/lib/reasoners/satml.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/reasoners/satml_frontend.ml b/src/lib/reasoners/satml_frontend.ml index 5ea24d382..8c676fe68 100644 --- a/src/lib/reasoners/satml_frontend.ml +++ b/src/lib/reasoners/satml_frontend.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/reasoners/satml_frontend.mli b/src/lib/reasoners/satml_frontend.mli index 85f61900f..b56091b72 100644 --- a/src/lib/reasoners/satml_frontend.mli +++ b/src/lib/reasoners/satml_frontend.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/reasoners/satml_frontend_hybrid.ml b/src/lib/reasoners/satml_frontend_hybrid.ml index 265aa89ad..a25fb4ee4 100644 --- a/src/lib/reasoners/satml_frontend_hybrid.ml +++ b/src/lib/reasoners/satml_frontend_hybrid.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/reasoners/satml_frontend_hybrid.mli b/src/lib/reasoners/satml_frontend_hybrid.mli index af2f3885a..0cf35c131 100644 --- a/src/lib/reasoners/satml_frontend_hybrid.mli +++ b/src/lib/reasoners/satml_frontend_hybrid.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/reasoners/shostak.ml b/src/lib/reasoners/shostak.ml index 971c215cd..8b308859b 100644 --- a/src/lib/reasoners/shostak.ml +++ b/src/lib/reasoners/shostak.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/reasoners/shostak.mli b/src/lib/reasoners/shostak.mli index 0067e7df9..42d9d7bfa 100644 --- a/src/lib/reasoners/shostak.mli +++ b/src/lib/reasoners/shostak.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/reasoners/sig.mli b/src/lib/reasoners/sig.mli index 3e05ceb83..3050e1f23 100644 --- a/src/lib/reasoners/sig.mli +++ b/src/lib/reasoners/sig.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/reasoners/sig_rel.mli b/src/lib/reasoners/sig_rel.mli index a4d4bb080..c82f9fc80 100644 --- a/src/lib/reasoners/sig_rel.mli +++ b/src/lib/reasoners/sig_rel.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/reasoners/th_util.ml b/src/lib/reasoners/th_util.ml index df1bc5e75..318c81609 100644 --- a/src/lib/reasoners/th_util.ml +++ b/src/lib/reasoners/th_util.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/reasoners/th_util.mli b/src/lib/reasoners/th_util.mli index f11c76985..523c8367e 100644 --- a/src/lib/reasoners/th_util.mli +++ b/src/lib/reasoners/th_util.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/reasoners/theory.ml b/src/lib/reasoners/theory.ml index e38d91224..31973c37d 100644 --- a/src/lib/reasoners/theory.ml +++ b/src/lib/reasoners/theory.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/reasoners/theory.mli b/src/lib/reasoners/theory.mli index 6c7491a63..8a2387e53 100644 --- a/src/lib/reasoners/theory.mli +++ b/src/lib/reasoners/theory.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/reasoners/uf.ml b/src/lib/reasoners/uf.ml index 5c0d366e0..935d2c323 100644 --- a/src/lib/reasoners/uf.ml +++ b/src/lib/reasoners/uf.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/reasoners/uf.mli b/src/lib/reasoners/uf.mli index 8ffd416fb..aa027060a 100644 --- a/src/lib/reasoners/uf.mli +++ b/src/lib/reasoners/uf.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/reasoners/use.ml b/src/lib/reasoners/use.ml index 2dce9b653..b02fef1fe 100644 --- a/src/lib/reasoners/use.ml +++ b/src/lib/reasoners/use.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/reasoners/use.mli b/src/lib/reasoners/use.mli index 6bd94c755..76a9329c6 100644 --- a/src/lib/reasoners/use.mli +++ b/src/lib/reasoners/use.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/structures/commands.ml b/src/lib/structures/commands.ml index 69a3ec983..f06b4a5dd 100644 --- a/src/lib/structures/commands.ml +++ b/src/lib/structures/commands.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/structures/commands.mli b/src/lib/structures/commands.mli index ab6ae77e2..bc1cafb49 100644 --- a/src/lib/structures/commands.mli +++ b/src/lib/structures/commands.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/structures/errors.ml b/src/lib/structures/errors.ml index 08fc1f65e..e5bc26035 100644 --- a/src/lib/structures/errors.ml +++ b/src/lib/structures/errors.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/structures/errors.mli b/src/lib/structures/errors.mli index 4a3b45137..7f1794c17 100644 --- a/src/lib/structures/errors.mli +++ b/src/lib/structures/errors.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/structures/explanation.ml b/src/lib/structures/explanation.ml index 5be9df795..2896e7b75 100644 --- a/src/lib/structures/explanation.ml +++ b/src/lib/structures/explanation.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/structures/explanation.mli b/src/lib/structures/explanation.mli index 30ad73d07..7d4008eb7 100644 --- a/src/lib/structures/explanation.mli +++ b/src/lib/structures/explanation.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/structures/expr.ml b/src/lib/structures/expr.ml index 7fe63c872..39313bf07 100644 --- a/src/lib/structures/expr.ml +++ b/src/lib/structures/expr.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/structures/expr.mli b/src/lib/structures/expr.mli index c2281e53b..8c639480c 100644 --- a/src/lib/structures/expr.mli +++ b/src/lib/structures/expr.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/structures/fpa_rounding.ml b/src/lib/structures/fpa_rounding.ml index eb9ca47a5..3c04170b3 100644 --- a/src/lib/structures/fpa_rounding.ml +++ b/src/lib/structures/fpa_rounding.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/structures/fpa_rounding.mli b/src/lib/structures/fpa_rounding.mli index 5a7975495..ad69bf1cf 100644 --- a/src/lib/structures/fpa_rounding.mli +++ b/src/lib/structures/fpa_rounding.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/structures/id.ml b/src/lib/structures/id.ml index f92990420..b8666d20a 100644 --- a/src/lib/structures/id.ml +++ b/src/lib/structures/id.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) @@ -12,15 +12,6 @@ (* *) (* --------------------------------------------------------------- *) (* *) -(* The Alt-Ergo theorem prover *) -(* *) -(* Sylvain Conchon, Evelyne Contejean, Francois Bobot *) -(* Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout *) -(* *) -(* CNRS - INRIA - Universite Paris Sud *) -(* *) -(* --------------------------------------------------------------- *) -(* *) (* More details can be found in the directory licenses/ *) (* *) (**************************************************************************) diff --git a/src/lib/structures/id.mli b/src/lib/structures/id.mli index 0726a0e43..5666a0a8a 100644 --- a/src/lib/structures/id.mli +++ b/src/lib/structures/id.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) @@ -12,15 +12,6 @@ (* *) (* --------------------------------------------------------------- *) (* *) -(* The Alt-Ergo theorem prover *) -(* *) -(* Sylvain Conchon, Evelyne Contejean, Francois Bobot *) -(* Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout *) -(* *) -(* CNRS - INRIA - Universite Paris Sud *) -(* *) -(* --------------------------------------------------------------- *) -(* *) (* More details can be found in the directory licenses/ *) (* *) (**************************************************************************) diff --git a/src/lib/structures/literal.ml b/src/lib/structures/literal.ml index 583b379fc..d9ca0669c 100644 --- a/src/lib/structures/literal.ml +++ b/src/lib/structures/literal.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/structures/literal.mli b/src/lib/structures/literal.mli index db7c505aa..4680c9e05 100644 --- a/src/lib/structures/literal.mli +++ b/src/lib/structures/literal.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/structures/modelMap.ml b/src/lib/structures/modelMap.ml index d4d4134bf..e84898223 100644 --- a/src/lib/structures/modelMap.ml +++ b/src/lib/structures/modelMap.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) @@ -12,15 +12,6 @@ (* *) (* --------------------------------------------------------------- *) (* *) -(* The Alt-Ergo theorem prover *) -(* *) -(* Sylvain Conchon, Evelyne Contejean, Francois Bobot *) -(* Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout *) -(* *) -(* CNRS - INRIA - Universite Paris Sud *) -(* *) -(* --------------------------------------------------------------- *) -(* *) (* More details can be found in the directory licenses/ *) (* *) (**************************************************************************) diff --git a/src/lib/structures/modelMap.mli b/src/lib/structures/modelMap.mli index 994a9df54..aa823bca1 100644 --- a/src/lib/structures/modelMap.mli +++ b/src/lib/structures/modelMap.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) 2022-2024 --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) @@ -12,15 +12,6 @@ (* *) (* --------------------------------------------------------------- *) (* *) -(* The Alt-Ergo theorem prover *) -(* *) -(* Sylvain Conchon, Evelyne Contejean, Francois Bobot *) -(* Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout *) -(* *) -(* CNRS - INRIA - Universite Paris Sud *) -(* *) -(* --------------------------------------------------------------- *) -(* *) (* More details can be found in the directory licenses/ *) (* *) (**************************************************************************) diff --git a/src/lib/structures/objective.ml b/src/lib/structures/objective.ml index 63d6cca64..be8ff8160 100644 --- a/src/lib/structures/objective.ml +++ b/src/lib/structures/objective.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) 2022-2024 --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) @@ -12,15 +12,6 @@ (* *) (* --------------------------------------------------------------- *) (* *) -(* The Alt-Ergo theorem prover *) -(* *) -(* Sylvain Conchon, Evelyne Contejean, Francois Bobot *) -(* Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout *) -(* *) -(* CNRS - INRIA - Universite Paris Sud *) -(* *) -(* --------------------------------------------------------------- *) -(* *) (* More details can be found in the directory licenses/ *) (* *) (**************************************************************************) diff --git a/src/lib/structures/objective.mli b/src/lib/structures/objective.mli index 8bbed662b..d5f79cf56 100644 --- a/src/lib/structures/objective.mli +++ b/src/lib/structures/objective.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) 2022-2024 --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) @@ -12,15 +12,6 @@ (* *) (* --------------------------------------------------------------- *) (* *) -(* The Alt-Ergo theorem prover *) -(* *) -(* Sylvain Conchon, Evelyne Contejean, Francois Bobot *) -(* Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout *) -(* *) -(* CNRS - INRIA - Universite Paris Sud *) -(* *) -(* --------------------------------------------------------------- *) -(* *) (* More details can be found in the directory licenses/ *) (* *) (**************************************************************************) diff --git a/src/lib/structures/parsed.ml b/src/lib/structures/parsed.ml index 5005841ae..d58dde682 100644 --- a/src/lib/structures/parsed.ml +++ b/src/lib/structures/parsed.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/structures/parsed.mli b/src/lib/structures/parsed.mli index a2764baf3..5c7e177de 100644 --- a/src/lib/structures/parsed.mli +++ b/src/lib/structures/parsed.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/structures/profiling.ml b/src/lib/structures/profiling.ml index b8b44a0ac..308ea1230 100644 --- a/src/lib/structures/profiling.ml +++ b/src/lib/structures/profiling.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/structures/profiling.mli b/src/lib/structures/profiling.mli index 813bbe0cf..ae5f466a5 100644 --- a/src/lib/structures/profiling.mli +++ b/src/lib/structures/profiling.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/structures/satml_types.ml b/src/lib/structures/satml_types.ml index 39221eb8a..be109c2de 100644 --- a/src/lib/structures/satml_types.ml +++ b/src/lib/structures/satml_types.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/structures/satml_types.mli b/src/lib/structures/satml_types.mli index 929d223a3..ebdb6bd07 100644 --- a/src/lib/structures/satml_types.mli +++ b/src/lib/structures/satml_types.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/structures/symbols.ml b/src/lib/structures/symbols.ml index 0ad3687b0..5fde2df38 100644 --- a/src/lib/structures/symbols.ml +++ b/src/lib/structures/symbols.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/structures/symbols.mli b/src/lib/structures/symbols.mli index 17dd313f5..0aedea950 100644 --- a/src/lib/structures/symbols.mli +++ b/src/lib/structures/symbols.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/structures/ty.ml b/src/lib/structures/ty.ml index 5461ea7f7..3304f60a4 100644 --- a/src/lib/structures/ty.ml +++ b/src/lib/structures/ty.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/structures/ty.mli b/src/lib/structures/ty.mli index d636faff9..688662695 100644 --- a/src/lib/structures/ty.mli +++ b/src/lib/structures/ty.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/structures/typed.ml b/src/lib/structures/typed.ml index 0c4fa051e..eb2dc0381 100644 --- a/src/lib/structures/typed.ml +++ b/src/lib/structures/typed.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/structures/typed.mli b/src/lib/structures/typed.mli index 281afdab2..525e2712f 100644 --- a/src/lib/structures/typed.mli +++ b/src/lib/structures/typed.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/structures/uid.ml b/src/lib/structures/uid.ml index 2394e0570..66d877467 100644 --- a/src/lib/structures/uid.ml +++ b/src/lib/structures/uid.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) 2022-2024 --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/structures/uid.mli b/src/lib/structures/uid.mli index 11d6570ed..866357b3a 100644 --- a/src/lib/structures/uid.mli +++ b/src/lib/structures/uid.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/structures/var.ml b/src/lib/structures/var.ml index 29937366b..a451f569b 100644 --- a/src/lib/structures/var.ml +++ b/src/lib/structures/var.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/structures/var.mli b/src/lib/structures/var.mli index 60a4ad20c..128eb2eb1 100644 --- a/src/lib/structures/var.mli +++ b/src/lib/structures/var.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/structures/xliteral.ml b/src/lib/structures/xliteral.ml index d7f016445..b11106e4e 100644 --- a/src/lib/structures/xliteral.ml +++ b/src/lib/structures/xliteral.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/structures/xliteral.mli b/src/lib/structures/xliteral.mli index bd60c345a..4abdbd29b 100644 --- a/src/lib/structures/xliteral.mli +++ b/src/lib/structures/xliteral.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/util/emap.ml b/src/lib/util/emap.ml index 89852c476..6cca01bfb 100644 --- a/src/lib/util/emap.ml +++ b/src/lib/util/emap.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/util/emap.mli b/src/lib/util/emap.mli index e0678aab0..539e2b33b 100644 --- a/src/lib/util/emap.mli +++ b/src/lib/util/emap.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/util/gc_debug.ml b/src/lib/util/gc_debug.ml index 29ba4e9db..b63e79108 100644 --- a/src/lib/util/gc_debug.ml +++ b/src/lib/util/gc_debug.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/util/gc_debug.mli b/src/lib/util/gc_debug.mli index 2b0435286..5fa64511e 100644 --- a/src/lib/util/gc_debug.mli +++ b/src/lib/util/gc_debug.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/util/hconsing.ml b/src/lib/util/hconsing.ml index 30c4d620b..1874e3935 100644 --- a/src/lib/util/hconsing.ml +++ b/src/lib/util/hconsing.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/util/hconsing.mli b/src/lib/util/hconsing.mli index 6065aa93f..aaf0ad868 100644 --- a/src/lib/util/hconsing.mli +++ b/src/lib/util/hconsing.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/util/heap.ml b/src/lib/util/heap.ml index da5e77aad..3d29b5cd1 100644 --- a/src/lib/util/heap.ml +++ b/src/lib/util/heap.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/util/heap.mli b/src/lib/util/heap.mli index d532b1ee9..6ab433151 100644 --- a/src/lib/util/heap.mli +++ b/src/lib/util/heap.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/util/hstring.ml b/src/lib/util/hstring.ml index 733faa68e..069c99265 100644 --- a/src/lib/util/hstring.ml +++ b/src/lib/util/hstring.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/util/hstring.mli b/src/lib/util/hstring.mli index b4fed65a7..6bff164b1 100644 --- a/src/lib/util/hstring.mli +++ b/src/lib/util/hstring.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/util/lists.ml b/src/lib/util/lists.ml index b6ce0252d..71418290c 100644 --- a/src/lib/util/lists.ml +++ b/src/lib/util/lists.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/util/lists.mli b/src/lib/util/lists.mli index df2ee3f08..d09854113 100644 --- a/src/lib/util/lists.mli +++ b/src/lib/util/lists.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/util/loc.ml b/src/lib/util/loc.ml index 48b644f98..e30609f58 100644 --- a/src/lib/util/loc.ml +++ b/src/lib/util/loc.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/util/loc.mli b/src/lib/util/loc.mli index 204fd1542..cba921924 100644 --- a/src/lib/util/loc.mli +++ b/src/lib/util/loc.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/util/myUnix.ml b/src/lib/util/myUnix.ml index fd1d98bad..e1431da06 100644 --- a/src/lib/util/myUnix.ml +++ b/src/lib/util/myUnix.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/util/myUnix.mli b/src/lib/util/myUnix.mli index c1106a1d5..eaa30251d 100644 --- a/src/lib/util/myUnix.mli +++ b/src/lib/util/myUnix.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/util/my_zip.ml b/src/lib/util/my_zip.ml index bd9a05d59..d3efd8fd1 100644 --- a/src/lib/util/my_zip.ml +++ b/src/lib/util/my_zip.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/util/my_zip.mli b/src/lib/util/my_zip.mli index 6f6ab0e54..65ff2a6b6 100644 --- a/src/lib/util/my_zip.mli +++ b/src/lib/util/my_zip.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/util/numbers.ml b/src/lib/util/numbers.ml index 5aeb62afa..f2924243e 100644 --- a/src/lib/util/numbers.ml +++ b/src/lib/util/numbers.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/util/numbers.mli b/src/lib/util/numbers.mli index 7a2c4c937..f2cc11ccd 100644 --- a/src/lib/util/numbers.mli +++ b/src/lib/util/numbers.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/util/options.ml b/src/lib/util/options.ml index aadce882b..d1131cb2a 100644 --- a/src/lib/util/options.ml +++ b/src/lib/util/options.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/util/options.mli b/src/lib/util/options.mli index 332114777..bd1017508 100644 --- a/src/lib/util/options.mli +++ b/src/lib/util/options.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/util/printer.ml b/src/lib/util/printer.ml index 8aeac0c7e..fba40ff4d 100644 --- a/src/lib/util/printer.ml +++ b/src/lib/util/printer.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/util/printer.mli b/src/lib/util/printer.mli index b8aaf58ef..91855f137 100644 --- a/src/lib/util/printer.mli +++ b/src/lib/util/printer.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/util/steps.ml b/src/lib/util/steps.ml index c4d1aba82..9af0484da 100644 --- a/src/lib/util/steps.ml +++ b/src/lib/util/steps.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/util/steps.mli b/src/lib/util/steps.mli index 235e7a3b0..4996aa575 100644 --- a/src/lib/util/steps.mli +++ b/src/lib/util/steps.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/util/theories.ml b/src/lib/util/theories.ml index 1c9490c2e..8e2aaf32f 100644 --- a/src/lib/util/theories.ml +++ b/src/lib/util/theories.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) 2022-2024 --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) @@ -12,15 +12,6 @@ (* *) (* --------------------------------------------------------------- *) (* *) -(* The Alt-Ergo theorem prover *) -(* *) -(* Sylvain Conchon, Evelyne Contejean, Francois Bobot *) -(* Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout *) -(* *) -(* CNRS - INRIA - Universite Paris Sud *) -(* *) -(* --------------------------------------------------------------- *) -(* *) (* More details can be found in the directory licenses/ *) (* *) (**************************************************************************) diff --git a/src/lib/util/timers.ml b/src/lib/util/timers.ml index 6fa3c1764..b7235a3e8 100644 --- a/src/lib/util/timers.ml +++ b/src/lib/util/timers.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/util/timers.mli b/src/lib/util/timers.mli index e01ea9aaa..d7143847f 100644 --- a/src/lib/util/timers.mli +++ b/src/lib/util/timers.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/util/uqueue.ml b/src/lib/util/uqueue.ml index 00aa6224d..ccf96a15a 100644 --- a/src/lib/util/uqueue.ml +++ b/src/lib/util/uqueue.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) @@ -12,15 +12,6 @@ (* *) (* --------------------------------------------------------------- *) (* *) -(* The Alt-Ergo theorem prover *) -(* *) -(* Sylvain Conchon, Evelyne Contejean, Francois Bobot *) -(* Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout *) -(* *) -(* CNRS - INRIA - Universite Paris Sud *) -(* *) -(* --------------------------------------------------------------- *) -(* *) (* More details can be found in the directory licenses/ *) (* *) (**************************************************************************) diff --git a/src/lib/util/uqueue.mli b/src/lib/util/uqueue.mli index 94b41dea7..9d446d5bc 100644 --- a/src/lib/util/uqueue.mli +++ b/src/lib/util/uqueue.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) 2022-2024 --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) @@ -12,15 +12,6 @@ (* *) (* --------------------------------------------------------------- *) (* *) -(* The Alt-Ergo theorem prover *) -(* *) -(* Sylvain Conchon, Evelyne Contejean, Francois Bobot *) -(* Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout *) -(* *) -(* CNRS - INRIA - Universite Paris Sud *) -(* *) -(* --------------------------------------------------------------- *) -(* *) (* More details can be found in the directory licenses/ *) (* *) (**************************************************************************) diff --git a/src/lib/util/util.ml b/src/lib/util/util.ml index afb881b3c..876eea711 100644 --- a/src/lib/util/util.ml +++ b/src/lib/util/util.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/util/util.mli b/src/lib/util/util.mli index 3beb24965..2ce5175ed 100644 --- a/src/lib/util/util.mli +++ b/src/lib/util/util.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/util/vec.ml b/src/lib/util/vec.ml index fa1f911a3..3f4af8ff7 100644 --- a/src/lib/util/vec.ml +++ b/src/lib/util/vec.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/util/vec.mli b/src/lib/util/vec.mli index 6f9bda061..29aa26e21 100644 --- a/src/lib/util/vec.mli +++ b/src/lib/util/vec.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/util/version.ml b/src/lib/util/version.ml index 3b78f1064..197de931b 100644 --- a/src/lib/util/version.ml +++ b/src/lib/util/version.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/lib/util/version.mli b/src/lib/util/version.mli index af7278671..8e49b7f32 100644 --- a/src/lib/util/version.mli +++ b/src/lib/util/version.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/parsers/native_lexer.mll b/src/parsers/native_lexer.mll index 58367ab55..a66bab262 100644 --- a/src/parsers/native_lexer.mll +++ b/src/parsers/native_lexer.mll @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/parsers/native_parser.mly b/src/parsers/native_parser.mly index d6d9f7824..f595138b7 100644 --- a/src/parsers/native_parser.mly +++ b/src/parsers/native_parser.mly @@ -1,7 +1,7 @@ /**************************************************************************/ /* */ /* Alt-Ergo: The SMT Solver For Software Verification */ -/* Copyright (C) 2013-2024 --- OCamlPro SAS */ +/* Copyright (C) --- OCamlPro SAS */ /* */ /* This file is distributed under the terms of OCamlPro */ /* Non-Commercial Purpose License, version 1. */ diff --git a/src/parsers/parsers.ml b/src/parsers/parsers.ml index c157e2566..51bd7286c 100644 --- a/src/parsers/parsers.ml +++ b/src/parsers/parsers.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/parsers/parsers.mli b/src/parsers/parsers.mli index 5a109fddb..0784de5bc 100644 --- a/src/parsers/parsers.mli +++ b/src/parsers/parsers.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/parsers/psmt2_to_alt_ergo.ml b/src/parsers/psmt2_to_alt_ergo.ml index 4fbdbf7ea..d642b7bb7 100644 --- a/src/parsers/psmt2_to_alt_ergo.ml +++ b/src/parsers/psmt2_to_alt_ergo.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/parsers/psmt2_to_alt_ergo.mli b/src/parsers/psmt2_to_alt_ergo.mli index 5a1358e32..073fd20a2 100644 --- a/src/parsers/psmt2_to_alt_ergo.mli +++ b/src/parsers/psmt2_to_alt_ergo.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/plugins/fm-simplex/fmSimplexIneqs.ml b/src/plugins/fm-simplex/fmSimplexIneqs.ml index 745403ae1..4497777c6 100644 --- a/src/plugins/fm-simplex/fmSimplexIneqs.ml +++ b/src/plugins/fm-simplex/fmSimplexIneqs.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/plugins/fm-simplex/fmSimplexIneqs.mli b/src/plugins/fm-simplex/fmSimplexIneqs.mli index fb768f6aa..99fb60a27 100644 --- a/src/plugins/fm-simplex/fmSimplexIneqs.mli +++ b/src/plugins/fm-simplex/fmSimplexIneqs.mli @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/plugins/fm-simplex/simplex.ml b/src/plugins/fm-simplex/simplex.ml index e1910e55a..0e8621aec 100644 --- a/src/plugins/fm-simplex/simplex.ml +++ b/src/plugins/fm-simplex/simplex.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/plugins/fm-simplex/simplex_cache.ml b/src/plugins/fm-simplex/simplex_cache.ml index 4d3da1ed0..f5a0be6a5 100644 --- a/src/plugins/fm-simplex/simplex_cache.ml +++ b/src/plugins/fm-simplex/simplex_cache.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) diff --git a/src/prelude.ml b/src/prelude.ml index 5cfa26301..f79f104a1 100644 --- a/src/prelude.ml +++ b/src/prelude.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) @@ -12,15 +12,6 @@ (* *) (* --------------------------------------------------------------- *) (* *) -(* The Alt-Ergo theorem prover *) -(* *) -(* Sylvain Conchon, Evelyne Contejean, Francois Bobot *) -(* Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout *) -(* *) -(* CNRS - INRIA - Universite Paris Sud *) -(* *) -(* --------------------------------------------------------------- *) -(* *) (* More details can be found in the directory licenses/ *) (* *) (**************************************************************************) diff --git a/tools/gentest.ml b/tools/gentest.ml index a5c889da3..787986ef6 100644 --- a/tools/gentest.ml +++ b/tools/gentest.ml @@ -1,7 +1,7 @@ (**************************************************************************) (* *) (* Alt-Ergo: The SMT Solver For Software Verification *) -(* Copyright (C) 2013-2024 --- OCamlPro SAS *) +(* Copyright (C) --- OCamlPro SAS *) (* *) (* This file is distributed under the terms of OCamlPro *) (* Non-Commercial Purpose License, version 1. *) @@ -12,15 +12,6 @@ (* *) (* --------------------------------------------------------------- *) (* *) -(* The Alt-Ergo theorem prover *) -(* *) -(* Sylvain Conchon, Evelyne Contejean, Francois Bobot *) -(* Mohamed Iguernelala, Stephane Lescuyer, Alain Mebsout *) -(* *) -(* CNRS - INRIA - Universite Paris Sud *) -(* *) -(* --------------------------------------------------------------- *) -(* *) (* More details can be found in the directory licenses/ *) (* *) (**************************************************************************)