diff --git a/LICENSE b/LICENSE
new file mode 100644
index 0000000000000000000000000000000000000000..2418ba1b5fb52ae5c981bd3b1378bf601d20a746
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,31 @@
+Copyright (c) 2009-2013 EPFL, Lausanne, unless otherwise specified. All rights
+reserved.
+
+This software was developed by the Laboratory for Automated Reasoning and
+Analysis (LARA) of the Swiss Federal Institute of Technology (EPFL), Lausanne,
+Switzerland.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+ 1. Redistributions of source code must retain the above copyright notice,
+ this list of conditions and the following disclaimer.
+
+ 2. Redistributions in binary form must reproduce the above copyright notice,
+ this list of conditions and the following disclaimer in the documentation
+ and/or other materials provided with the distribution.
+
+THIS SOFTWARE IS PROVIDED BY THE REGENTS AND CONTRIBUTORS ''AS IS'' AND ANY
+EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+DISCLAIMED. IN NO EVENT SHALL THE REGENTS OR CONTRIBUTORS BE LIABLE FOR ANY
+DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
+(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
+LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON
+ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+
+The views and conclusions contained in the software and documentation are those
+of the authors and should not be interpreted as representing official policies,
+either expressed or implied, of EPFL.
diff --git a/library/src/main/scala/leon/Annotations.scala b/library/src/main/scala/leon/Annotations.scala
index 85e8c00e0379c42f000b61ac14861190bb46963a..a441066401489312eefcb1261da1722a9184f561 100644
--- a/library/src/main/scala/leon/Annotations.scala
+++ b/library/src/main/scala/leon/Annotations.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
object Annotations {
diff --git a/library/src/main/scala/leon/Utils.scala b/library/src/main/scala/leon/Utils.scala
index 366cc39750b9779ebb1637f88b12bf9f86936fb4..ab3e84eb52acb45abc724f9935f0268142f1fc8f 100644
--- a/library/src/main/scala/leon/Utils.scala
+++ b/library/src/main/scala/leon/Utils.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
object Utils {
diff --git a/src/main/java/leon/codegen/runtime/CaseClass.java b/src/main/java/leon/codegen/runtime/CaseClass.java
index bbbdb92f8a41797e455477c5974424f1d2c15718..8cda1d23aa6e74705525bacd35bc529e1a8fb3fc 100644
--- a/src/main/java/leon/codegen/runtime/CaseClass.java
+++ b/src/main/java/leon/codegen/runtime/CaseClass.java
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon.codegen.runtime;
public interface CaseClass {
diff --git a/src/main/java/leon/codegen/runtime/LeonCodeGenEvaluationException.java b/src/main/java/leon/codegen/runtime/LeonCodeGenEvaluationException.java
index f4ba02da88eb58be609efdec67261b2bd76b8141..d4d5c358856dfe20b7e0e5d5704a7f1e19b1244f 100644
--- a/src/main/java/leon/codegen/runtime/LeonCodeGenEvaluationException.java
+++ b/src/main/java/leon/codegen/runtime/LeonCodeGenEvaluationException.java
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon.codegen.runtime;
/** Such exceptions are thrown when the evaluator is asked to do something it
diff --git a/src/main/java/leon/codegen/runtime/LeonCodeGenRuntimeException.java b/src/main/java/leon/codegen/runtime/LeonCodeGenRuntimeException.java
index 8a3e6b86adab93792c76cc282e48133a453c32e4..88af910a27bca036050d804564804cfef9be1f9c 100644
--- a/src/main/java/leon/codegen/runtime/LeonCodeGenRuntimeException.java
+++ b/src/main/java/leon/codegen/runtime/LeonCodeGenRuntimeException.java
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon.codegen.runtime;
/** Such exceptions are thrown when the evaluator encounters a runtime error,
diff --git a/src/main/java/leon/codegen/runtime/Map.java b/src/main/java/leon/codegen/runtime/Map.java
index 0bdb221c1939dd3ba995e05ec437d24c3f4a2fc6..cd9c2eb6aa428f762193b112640085d177913ee2 100644
--- a/src/main/java/leon/codegen/runtime/Map.java
+++ b/src/main/java/leon/codegen/runtime/Map.java
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon.codegen.runtime;
import java.util.Arrays;
diff --git a/src/main/java/leon/codegen/runtime/Set.java b/src/main/java/leon/codegen/runtime/Set.java
index b38ba90706efbebe08d93e3ea9bc20590718a57a..f271679532f17817a347cabd4381f169f06d00cb 100644
--- a/src/main/java/leon/codegen/runtime/Set.java
+++ b/src/main/java/leon/codegen/runtime/Set.java
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon.codegen.runtime;
import java.util.Arrays;
diff --git a/src/main/java/leon/codegen/runtime/Tuple.java b/src/main/java/leon/codegen/runtime/Tuple.java
index e010870ad1c17cceea99bce2725f6565eb5f7a53..958a2340fc31b6789812adaacc8752b24e6631fb 100644
--- a/src/main/java/leon/codegen/runtime/Tuple.java
+++ b/src/main/java/leon/codegen/runtime/Tuple.java
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon.codegen.runtime;
import java.util.Arrays;
diff --git a/src/main/scala/leon/LeonComponent.scala b/src/main/scala/leon/LeonComponent.scala
index 95f947b94370f3f60587ecd37157e0183b7d6832..e69af9aa7bc9014546b8f2d57c0851dee5771b01 100644
--- a/src/main/scala/leon/LeonComponent.scala
+++ b/src/main/scala/leon/LeonComponent.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
/** A common trait for everything that is important enough to be named,
diff --git a/src/main/scala/leon/LeonContext.scala b/src/main/scala/leon/LeonContext.scala
index cdd1ecf4ec9a3e11e430143cb3dab96542fab468..b271db3a4eba2d37d78ef3445c4d77dc40eeba11 100644
--- a/src/main/scala/leon/LeonContext.scala
+++ b/src/main/scala/leon/LeonContext.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
import purescala.Definitions.Program
diff --git a/src/main/scala/leon/LeonFatalError.scala b/src/main/scala/leon/LeonFatalError.scala
index 6fc773292fd721b996b2cfadbe964de250e6cc3b..8ceb4f3fd1d32b5cd21622bacf15e679eacf6270 100644
--- a/src/main/scala/leon/LeonFatalError.scala
+++ b/src/main/scala/leon/LeonFatalError.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
case class LeonFatalError() extends Exception
diff --git a/src/main/scala/leon/LeonOption.scala b/src/main/scala/leon/LeonOption.scala
index 9859fcc92b151879e2d3f928f0dcf6bb8ba80de4..08ebbbb2cc249b61554a14fe43eaa2eda5d846eb 100644
--- a/src/main/scala/leon/LeonOption.scala
+++ b/src/main/scala/leon/LeonOption.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
/** Describes a command-line option. */
diff --git a/src/main/scala/leon/LeonPhase.scala b/src/main/scala/leon/LeonPhase.scala
index 1812b0239844d2d12a3e41d71c237f69ddd2e5a9..4b00b7566e343075527b2a62c7add4d1af59cb88 100644
--- a/src/main/scala/leon/LeonPhase.scala
+++ b/src/main/scala/leon/LeonPhase.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
import purescala.Definitions.Program
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 7549b1f5570a7583e04e4c731d0ab64f54849dc2..9055d9bee9ce9d42bc81efe872b427db445991e2 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
object Main {
diff --git a/src/main/scala/leon/Pipeline.scala b/src/main/scala/leon/Pipeline.scala
index 4cbf3dce38325928725408e07182c30da5d3a193..80c834506198d3e673a6f5ad8f42f625d4fa0cdc 100644
--- a/src/main/scala/leon/Pipeline.scala
+++ b/src/main/scala/leon/Pipeline.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
abstract class Pipeline[-F, +T] {
diff --git a/src/main/scala/leon/Reporter.scala b/src/main/scala/leon/Reporter.scala
index a9bff0440efd659e2d366a03822feb7a31ca8c8e..83b9aec06b0c5fd8199127553cc170b1730c90d1 100644
--- a/src/main/scala/leon/Reporter.scala
+++ b/src/main/scala/leon/Reporter.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
import purescala.Definitions.Definition
diff --git a/src/main/scala/leon/Settings.scala b/src/main/scala/leon/Settings.scala
index c267ba4d42d76136e30cd635ba056af5da77729a..4271bf85d31b619698752928cacc3c420f0d2202 100644
--- a/src/main/scala/leon/Settings.scala
+++ b/src/main/scala/leon/Settings.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
// typically these settings can be changed through some command-line switch.
diff --git a/src/main/scala/leon/Stopwatch.scala b/src/main/scala/leon/Stopwatch.scala
index b3e060ba5dcb9738c9a5e5aef797904efadb9798..9eab173d92751c8618cdc5d9b4149dc94a0c0ef4 100644
--- a/src/main/scala/leon/Stopwatch.scala
+++ b/src/main/scala/leon/Stopwatch.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
class StopwatchCollection(name: String) {
diff --git a/src/main/scala/leon/SubtypingPhase.scala b/src/main/scala/leon/SubtypingPhase.scala
index 3c542e4a22175d59a495106a963dbf1c983e8c04..8a63663b4080bde72176297814a27ec44ab4bce8 100644
--- a/src/main/scala/leon/SubtypingPhase.scala
+++ b/src/main/scala/leon/SubtypingPhase.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
import purescala.TypeTrees._
diff --git a/src/main/scala/leon/TypeChecking.scala b/src/main/scala/leon/TypeChecking.scala
index 41cda6b80a462276cc0b026bb9423b4a7be40919..2733b8781ecbd3abc66fdb6496ee77b55994deb8 100644
--- a/src/main/scala/leon/TypeChecking.scala
+++ b/src/main/scala/leon/TypeChecking.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
import purescala.Common._
diff --git a/src/main/scala/leon/UnitElimination.scala b/src/main/scala/leon/UnitElimination.scala
index dc58a24bed859b7aa860940ca7d46be04219ae3d..3717cd585cb76c7048f40e733bfe6672ad3511c4 100644
--- a/src/main/scala/leon/UnitElimination.scala
+++ b/src/main/scala/leon/UnitElimination.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
import purescala.Common._
diff --git a/src/main/scala/leon/codegen/CodeGenPhase.scala b/src/main/scala/leon/codegen/CodeGenPhase.scala
index c5e065575ac1bcfe847db65623d8a006818efe04..4a6110d893d190e111f901e1de4850831f5dbd8f 100644
--- a/src/main/scala/leon/codegen/CodeGenPhase.scala
+++ b/src/main/scala/leon/codegen/CodeGenPhase.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package codegen
diff --git a/src/main/scala/leon/codegen/CodeGeneration.scala b/src/main/scala/leon/codegen/CodeGeneration.scala
index c436893e209e2b7e3d3a2cff2c57fbb78bfe9896..9e23300c03f0affd2d51d25862ec88b62f8508ee 100644
--- a/src/main/scala/leon/codegen/CodeGeneration.scala
+++ b/src/main/scala/leon/codegen/CodeGeneration.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package codegen
diff --git a/src/main/scala/leon/codegen/CompilationEnvironment.scala b/src/main/scala/leon/codegen/CompilationEnvironment.scala
index 760904eb18b975857e916d20b6fbb03f32db1ada..52f4ec3e8e1e12e099490ec15cc721dca9e017d5 100644
--- a/src/main/scala/leon/codegen/CompilationEnvironment.scala
+++ b/src/main/scala/leon/codegen/CompilationEnvironment.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package codegen
diff --git a/src/main/scala/leon/codegen/CompilationException.scala b/src/main/scala/leon/codegen/CompilationException.scala
index 236cc586e64b487170ba7f80377d8e690742c120..78948a4510be283ba163a650a9c0b3ec994ce081 100644
--- a/src/main/scala/leon/codegen/CompilationException.scala
+++ b/src/main/scala/leon/codegen/CompilationException.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package codegen
diff --git a/src/main/scala/leon/codegen/CompilationResult.scala b/src/main/scala/leon/codegen/CompilationResult.scala
index dbb267c3c236c4c31f2dc10d50f1ed9ab4861301..50873242ae7aa56b7a158aafb3a2fc24a964e28f 100644
--- a/src/main/scala/leon/codegen/CompilationResult.scala
+++ b/src/main/scala/leon/codegen/CompilationResult.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package codegen
diff --git a/src/main/scala/leon/codegen/CompilationUnit.scala b/src/main/scala/leon/codegen/CompilationUnit.scala
index 0d547d27a72b44f07d7a7105645d5b7bfc50a828..1c5b5eac369b435e2a9970a399dfff74482ac347 100644
--- a/src/main/scala/leon/codegen/CompilationUnit.scala
+++ b/src/main/scala/leon/codegen/CompilationUnit.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package codegen
diff --git a/src/main/scala/leon/codegen/CompiledExpression.scala b/src/main/scala/leon/codegen/CompiledExpression.scala
index 02cc93407643cf4fbcaff043b8e9352af2064bc1..cf5369d89ae0ae26d6eb09113ab8909da18992fe 100644
--- a/src/main/scala/leon/codegen/CompiledExpression.scala
+++ b/src/main/scala/leon/codegen/CompiledExpression.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package codegen
diff --git a/src/main/scala/leon/evaluators/CodeGenEvaluator.scala b/src/main/scala/leon/evaluators/CodeGenEvaluator.scala
index b540a483c2cc1c2c3be0cfe8f280e58d7828c4d1..87314546f58dcddfb45bb180cad14872d0bba8ff 100644
--- a/src/main/scala/leon/evaluators/CodeGenEvaluator.scala
+++ b/src/main/scala/leon/evaluators/CodeGenEvaluator.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package evaluators
diff --git a/src/main/scala/leon/evaluators/DefaultEvaluator.scala b/src/main/scala/leon/evaluators/DefaultEvaluator.scala
index a1f66ae1c8d65367e307a25e9bb553dc74f5e01a..d29f91c508d968e370543d2f276e807d41a50dd3 100644
--- a/src/main/scala/leon/evaluators/DefaultEvaluator.scala
+++ b/src/main/scala/leon/evaluators/DefaultEvaluator.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package evaluators
diff --git a/src/main/scala/leon/evaluators/EvaluationResults.scala b/src/main/scala/leon/evaluators/EvaluationResults.scala
index 598121fd0ccf0c963d204c2df0dbc26f42f6a041..9a3d971238015b0116fc8ff8e6c33b2109757fe5 100644
--- a/src/main/scala/leon/evaluators/EvaluationResults.scala
+++ b/src/main/scala/leon/evaluators/EvaluationResults.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package evaluators
diff --git a/src/main/scala/leon/evaluators/Evaluator.scala b/src/main/scala/leon/evaluators/Evaluator.scala
index a54e406e37ff561f42ac668e7837cd80a7ac0b32..fd907bd0eb180e5419c9bac47849e3c2a55b69f3 100644
--- a/src/main/scala/leon/evaluators/Evaluator.scala
+++ b/src/main/scala/leon/evaluators/Evaluator.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package evaluators
diff --git a/src/main/scala/leon/plugin/AnalysisComponent.scala b/src/main/scala/leon/plugin/AnalysisComponent.scala
index 783d86b5c3ed153a9903f45fb5fd16375824d44b..49a62fcb4b521e308b42a33477feef70f9557287 100644
--- a/src/main/scala/leon/plugin/AnalysisComponent.scala
+++ b/src/main/scala/leon/plugin/AnalysisComponent.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package plugin
diff --git a/src/main/scala/leon/plugin/CodeExtraction.scala b/src/main/scala/leon/plugin/CodeExtraction.scala
index 06a6ac624ff4c15472da16e081531d120e7ef57e..b03a8438f9dd661caec6d034f5fdf5f51e4162ab 100644
--- a/src/main/scala/leon/plugin/CodeExtraction.scala
+++ b/src/main/scala/leon/plugin/CodeExtraction.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package plugin
diff --git a/src/main/scala/leon/plugin/ExtractionPhase.scala b/src/main/scala/leon/plugin/ExtractionPhase.scala
index c68f7f6b81e792197c3099b0f2eec769ca073a7d..07f9f113fdc980599c28c24638682bd977fc0de0 100644
--- a/src/main/scala/leon/plugin/ExtractionPhase.scala
+++ b/src/main/scala/leon/plugin/ExtractionPhase.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package plugin
diff --git a/src/main/scala/leon/plugin/Extractors.scala b/src/main/scala/leon/plugin/Extractors.scala
index c333df79ff55a43d1131da30756c3776dfc5e502..e407a35086e62215869bcbfdeefd520b60f44d63 100644
--- a/src/main/scala/leon/plugin/Extractors.scala
+++ b/src/main/scala/leon/plugin/Extractors.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package plugin
diff --git a/src/main/scala/leon/plugin/LeonPlugin.scala b/src/main/scala/leon/plugin/LeonPlugin.scala
index 0eebd19c99d5e6749970eb501e6b492b70886ee5..badf32e8ef5d3333f937a6291d4fade2f8603aec 100644
--- a/src/main/scala/leon/plugin/LeonPlugin.scala
+++ b/src/main/scala/leon/plugin/LeonPlugin.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package plugin
diff --git a/src/main/scala/leon/plugin/SimpleReporter.scala b/src/main/scala/leon/plugin/SimpleReporter.scala
index 31cc4d7b132be2dafb1b712bc5355eadba35c46b..549fb2589d47e5557b5ba1ebf415f7c37099f614 100644
--- a/src/main/scala/leon/plugin/SimpleReporter.scala
+++ b/src/main/scala/leon/plugin/SimpleReporter.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package plugin
diff --git a/src/main/scala/leon/plugin/TemporaryInputPhase.scala b/src/main/scala/leon/plugin/TemporaryInputPhase.scala
index 89d26cf128408cbb69ed50849d85c45e0c33d5e6..88717785c466aec2d3505130a4c8e5ca323941b4 100644
--- a/src/main/scala/leon/plugin/TemporaryInputPhase.scala
+++ b/src/main/scala/leon/plugin/TemporaryInputPhase.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package plugin
diff --git a/src/main/scala/leon/purescala/Common.scala b/src/main/scala/leon/purescala/Common.scala
index 16b8959f3930b30fc040ff1263588c3ad38cf9a1..45142714e6ebb1b4f9a4a3d9c778c9400db18e59 100644
--- a/src/main/scala/leon/purescala/Common.scala
+++ b/src/main/scala/leon/purescala/Common.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package purescala
diff --git a/src/main/scala/leon/purescala/DataGen.scala b/src/main/scala/leon/purescala/DataGen.scala
index 0ace125ba2a1e47d82ac9cc62fc6e4e3c11afed0..02e559d03d5bda9d46e09d3c4d5b87f1e609e97b 100644
--- a/src/main/scala/leon/purescala/DataGen.scala
+++ b/src/main/scala/leon/purescala/DataGen.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package purescala
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index 89c31d054f59d3d9ccac36c56d22cc65b31758e5..ae14f7b62a147f54888a6220974020588e06b616 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package purescala
diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala
index 00ce83c66beecb206784ea6c2d559544a599ba38..704d6a7ae3d6f89a67af8b889ce1818d5ef83bf5 100644
--- a/src/main/scala/leon/purescala/Extractors.scala
+++ b/src/main/scala/leon/purescala/Extractors.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package purescala
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index 11e98e534e5f5f15b6b8e51ee322373469404ae5..964d4d90559041c95086922d4c09fa9ae41fc9da 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package purescala
diff --git a/src/main/scala/leon/purescala/ScalaPrinter.scala b/src/main/scala/leon/purescala/ScalaPrinter.scala
index 9e2579f6c2af8f322cd3f24ccccaa32dd226ce09..d7ab7e3a48dd140853f548bf38251fb92435d937 100644
--- a/src/main/scala/leon/purescala/ScalaPrinter.scala
+++ b/src/main/scala/leon/purescala/ScalaPrinter.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon.purescala
/** This pretty-printer only print valid scala syntax */
diff --git a/src/main/scala/leon/purescala/TreeNormalizations.scala b/src/main/scala/leon/purescala/TreeNormalizations.scala
index fb34f35ed507a2b10d93500e52f7dad71a1b5c73..7e450b3e926806aceaf66a5b73b7adb41e9d15cb 100644
--- a/src/main/scala/leon/purescala/TreeNormalizations.scala
+++ b/src/main/scala/leon/purescala/TreeNormalizations.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package purescala
diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index ff38fc75d1b45bb410a3007dee30fcaddf92b032..818d125e4e2041add92b4888437608f0b5072229 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/src/main/scala/leon/purescala/TreeOps.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package purescala
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index b4c1762a693b9211521fbb4b1624a8e99191bb2d..21a23be82a8a50c20720404913f2a6c1d0cfb045 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package purescala
diff --git a/src/main/scala/leon/purescala/TypeTrees.scala b/src/main/scala/leon/purescala/TypeTrees.scala
index 22e1010aeaef831f3957792897d1c639610c8254..96265cf88c6736dbba11b6337c6cde901838d14f 100644
--- a/src/main/scala/leon/purescala/TypeTrees.scala
+++ b/src/main/scala/leon/purescala/TypeTrees.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package purescala
diff --git a/src/main/scala/leon/solvers/IncrementalSolver.scala b/src/main/scala/leon/solvers/IncrementalSolver.scala
index 84215134e83bf1a53d5a7916a2563c97c23046f2..700699e537c7d1a511400565a0cb6990d426761a 100644
--- a/src/main/scala/leon/solvers/IncrementalSolver.scala
+++ b/src/main/scala/leon/solvers/IncrementalSolver.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package solvers
diff --git a/src/main/scala/leon/solvers/InterruptibleSolver.scala b/src/main/scala/leon/solvers/InterruptibleSolver.scala
index 01620279c7f65a01e2d08d63f17c34b9891b6520..e10e8ded91a9f47d232e59f5428347a58316a5a3 100644
--- a/src/main/scala/leon/solvers/InterruptibleSolver.scala
+++ b/src/main/scala/leon/solvers/InterruptibleSolver.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package solvers
diff --git a/src/main/scala/leon/solvers/ParallelSolver.scala b/src/main/scala/leon/solvers/ParallelSolver.scala
index e2a334df1360b121369eec6b7db7f59b0e3fd925..b812f3b7e58b64ab38de723765ee2eb258f24870 100644
--- a/src/main/scala/leon/solvers/ParallelSolver.scala
+++ b/src/main/scala/leon/solvers/ParallelSolver.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package solvers
diff --git a/src/main/scala/leon/solvers/RandomSolver.scala b/src/main/scala/leon/solvers/RandomSolver.scala
index 3ba1a3fa4d55a8605eb6ffca9523bd438ccba882..750270625138871f810c993535b344f701fc025a 100644
--- a/src/main/scala/leon/solvers/RandomSolver.scala
+++ b/src/main/scala/leon/solvers/RandomSolver.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package solvers
diff --git a/src/main/scala/leon/solvers/Solver.scala b/src/main/scala/leon/solvers/Solver.scala
index 01a1e7336bd84a69a90c9c7dd93776602148be2e..5cc012e740e01e703b4cb84695b13300300e4d7b 100644
--- a/src/main/scala/leon/solvers/Solver.scala
+++ b/src/main/scala/leon/solvers/Solver.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package solvers
diff --git a/src/main/scala/leon/solvers/TimeoutSolver.scala b/src/main/scala/leon/solvers/TimeoutSolver.scala
index 22a2570318a8145e7563de48dcf17e690432ebdb..207b3118dd9da9c613a70a1a593e4ff13819bb8f 100644
--- a/src/main/scala/leon/solvers/TimeoutSolver.scala
+++ b/src/main/scala/leon/solvers/TimeoutSolver.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package solvers
diff --git a/src/main/scala/leon/solvers/TrivialSolver.scala b/src/main/scala/leon/solvers/TrivialSolver.scala
index 3451aa759e79d8a02561ef18f4bac3de9fd3d116..c1ae27d2657b4a6a082ff2a370def8705066f567 100644
--- a/src/main/scala/leon/solvers/TrivialSolver.scala
+++ b/src/main/scala/leon/solvers/TrivialSolver.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package solvers
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 1a94e295fb9669242bde48a8e0b7b8550578e1ff..e024b55460ed35db573a500ba517e92e9bcd1e98 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package solvers.z3
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index f736bf1fb8b06c741b647b236fbe1e786abf07d8..1a601470fc500c086fe9e627968cdad53465464f 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package solvers.z3
diff --git a/src/main/scala/leon/solvers/z3/FunctionTemplate.scala b/src/main/scala/leon/solvers/z3/FunctionTemplate.scala
index 95a319a2821c373837e575840a8be1eba64f983b..aacc633764dd0df4dbee24b72d5aa3cb1f531b7d 100644
--- a/src/main/scala/leon/solvers/z3/FunctionTemplate.scala
+++ b/src/main/scala/leon/solvers/z3/FunctionTemplate.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package solvers.z3
diff --git a/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala b/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala
index 379d0bf03c7945a37f585285b54071b7bd99af91..f8d1bd492ba1a451087c3b83baebefe06878ec7e 100644
--- a/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/UninterpretedZ3Solver.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package solvers.z3
diff --git a/src/main/scala/leon/solvers/z3/Z3ModelReconstruction.scala b/src/main/scala/leon/solvers/z3/Z3ModelReconstruction.scala
index 2e65ca7e56f46edb99b4ea91c4b09826c7bd2286..558274db58ea37f712abdcbb1618b872d93e9638 100644
--- a/src/main/scala/leon/solvers/z3/Z3ModelReconstruction.scala
+++ b/src/main/scala/leon/solvers/z3/Z3ModelReconstruction.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package solvers.z3
diff --git a/src/main/scala/leon/synthesis/Algebra.scala b/src/main/scala/leon/synthesis/Algebra.scala
index c92b08980c05a850926fa64878df353c8a07909e..17fab2cfbf36c225d7996c9c13661a34926bc37e 100644
--- a/src/main/scala/leon/synthesis/Algebra.scala
+++ b/src/main/scala/leon/synthesis/Algebra.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon.synthesis
/*
diff --git a/src/main/scala/leon/synthesis/ChooseInfo.scala b/src/main/scala/leon/synthesis/ChooseInfo.scala
index 888e923fb8c358849011e501b837b17aef4619ec..aca20208f721b8b7680be6c790285016324d9cd9 100644
--- a/src/main/scala/leon/synthesis/ChooseInfo.scala
+++ b/src/main/scala/leon/synthesis/ChooseInfo.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package synthesis
diff --git a/src/main/scala/leon/synthesis/CostModel.scala b/src/main/scala/leon/synthesis/CostModel.scala
index 7fd051d8eb862c07a4fd6075b8c68829e378b26f..128529c2521dc5329674f3880abd55362994e3d3 100644
--- a/src/main/scala/leon/synthesis/CostModel.scala
+++ b/src/main/scala/leon/synthesis/CostModel.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package synthesis
diff --git a/src/main/scala/leon/synthesis/FileInterface.scala b/src/main/scala/leon/synthesis/FileInterface.scala
index 0fd787e733a911bcfb129e3151e5925b5ecdf602..aee3f4342f64733e8e2cb6efce066659de971080 100644
--- a/src/main/scala/leon/synthesis/FileInterface.scala
+++ b/src/main/scala/leon/synthesis/FileInterface.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package synthesis
diff --git a/src/main/scala/leon/synthesis/Heuristics.scala b/src/main/scala/leon/synthesis/Heuristics.scala
index 0170430b56e12ee890f51fa088a963f8e68eaffb..20bc9125af4a637f249efefb281e03db85cbadea 100644
--- a/src/main/scala/leon/synthesis/Heuristics.scala
+++ b/src/main/scala/leon/synthesis/Heuristics.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package synthesis
diff --git a/src/main/scala/leon/synthesis/LinearEquations.scala b/src/main/scala/leon/synthesis/LinearEquations.scala
index e86ecf4171489323f10b349c024b223c301337a2..428c9ac69a0e3317d9e0bebcd16a20b3b38168d6 100644
--- a/src/main/scala/leon/synthesis/LinearEquations.scala
+++ b/src/main/scala/leon/synthesis/LinearEquations.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package synthesis
diff --git a/src/main/scala/leon/synthesis/Main.scala b/src/main/scala/leon/synthesis/Main.scala
index a3704d349db726b52bcd657fbecb94d31a67f404..69d6518d7ff8d933af558ef7a58329b18e4ecd05 100644
--- a/src/main/scala/leon/synthesis/Main.scala
+++ b/src/main/scala/leon/synthesis/Main.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package synthesis
diff --git a/src/main/scala/leon/synthesis/ManualSearch.scala b/src/main/scala/leon/synthesis/ManualSearch.scala
index faea80ddc47b08143438e66077c81a39dae92828..4e075254f217c5e5303b448a51d55acfa205e154 100644
--- a/src/main/scala/leon/synthesis/ManualSearch.scala
+++ b/src/main/scala/leon/synthesis/ManualSearch.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package synthesis
diff --git a/src/main/scala/leon/synthesis/ParallelSearch.scala b/src/main/scala/leon/synthesis/ParallelSearch.scala
index dbdbe0517936b7cc8eb0c1666445e5cb0dc88b86..57672fb4f24f1469e1c0eec782d98e28c99226ac 100644
--- a/src/main/scala/leon/synthesis/ParallelSearch.scala
+++ b/src/main/scala/leon/synthesis/ParallelSearch.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package synthesis
diff --git a/src/main/scala/leon/synthesis/Problem.scala b/src/main/scala/leon/synthesis/Problem.scala
index 7810483affb6268979ba5f4d35f82b62db6905cf..57dc87a289e36969a870954a41c23ae24e4a115f 100644
--- a/src/main/scala/leon/synthesis/Problem.scala
+++ b/src/main/scala/leon/synthesis/Problem.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package synthesis
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index 2357241c06fd94b565e38554561f3589179e4d74..21d1e72e49834055ac13fefee7597c89d6557980 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package synthesis
diff --git a/src/main/scala/leon/synthesis/SimpleSearch.scala b/src/main/scala/leon/synthesis/SimpleSearch.scala
index d042fc2e145409d333dc0934ebe66ac43722adae..42546b01abc6328fa3ffb824cfddb1b59f17f741 100644
--- a/src/main/scala/leon/synthesis/SimpleSearch.scala
+++ b/src/main/scala/leon/synthesis/SimpleSearch.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package synthesis
diff --git a/src/main/scala/leon/synthesis/Solution.scala b/src/main/scala/leon/synthesis/Solution.scala
index 965b1f74a7bde5c2c7c8d2bb18dc2919be7274e6..53c25e93bedb89401fc247cbf51dd85cf5e07cb4 100644
--- a/src/main/scala/leon/synthesis/Solution.scala
+++ b/src/main/scala/leon/synthesis/Solution.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package synthesis
diff --git a/src/main/scala/leon/synthesis/SynthesisContext.scala b/src/main/scala/leon/synthesis/SynthesisContext.scala
index 342e1766acc19e5e76def80d3e4161066b8e8210..d12a05c5c99c09b92961bd774b499d1d5f818a2b 100644
--- a/src/main/scala/leon/synthesis/SynthesisContext.scala
+++ b/src/main/scala/leon/synthesis/SynthesisContext.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package synthesis
diff --git a/src/main/scala/leon/synthesis/SynthesisOptions.scala b/src/main/scala/leon/synthesis/SynthesisOptions.scala
index 30f0de4f85ea659c4eacafb5303e42da459200b1..37408d3f7513ea09856baf3f5684d05395fc55a2 100644
--- a/src/main/scala/leon/synthesis/SynthesisOptions.scala
+++ b/src/main/scala/leon/synthesis/SynthesisOptions.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package synthesis
diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala
index 230c250d0245dcc2e5b1272e5dd81a9546ad770b..1251de0efb0662132a82f9073a606e026edc550c 100644
--- a/src/main/scala/leon/synthesis/SynthesisPhase.scala
+++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package synthesis
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index a94debc9eae65b55aa9e7356dcdcee4d916ac064..6e4879944c6d54120bb7af23de6854cca986323b 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package synthesis
diff --git a/src/main/scala/leon/synthesis/Task.scala b/src/main/scala/leon/synthesis/Task.scala
index e2d8d65fcdf3a7ed8c6598d5549ba09c6e05022a..deefa844e63b9d61b3fe6b468233f09458bf0198 100644
--- a/src/main/scala/leon/synthesis/Task.scala
+++ b/src/main/scala/leon/synthesis/Task.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package synthesis
diff --git a/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala b/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala
index 4d6342bae2f63285d66bfb0390e5dbd0df7f86b9..2a7b60bd5a4d1e9cf21d60f3fa664337a6e5d101 100644
--- a/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala
+++ b/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package synthesis
package heuristics
diff --git a/src/main/scala/leon/synthesis/heuristics/ADTLongInduction.scala b/src/main/scala/leon/synthesis/heuristics/ADTLongInduction.scala
index b6b47029634ca4907dbc15b50cf7729cd4835154..0437e52e331160bb91e5fa6a371c9062aea8a7f6 100644
--- a/src/main/scala/leon/synthesis/heuristics/ADTLongInduction.scala
+++ b/src/main/scala/leon/synthesis/heuristics/ADTLongInduction.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package synthesis
package heuristics
diff --git a/src/main/scala/leon/synthesis/heuristics/InnerCaseSplit.scala b/src/main/scala/leon/synthesis/heuristics/InnerCaseSplit.scala
index 8a76cd9f0d7a40e6700fcbe0446328514f8f8346..1f087f1cc80b2b2d0e5fe3472056d9fab5b5bef5 100644
--- a/src/main/scala/leon/synthesis/heuristics/InnerCaseSplit.scala
+++ b/src/main/scala/leon/synthesis/heuristics/InnerCaseSplit.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package synthesis
package heuristics
diff --git a/src/main/scala/leon/synthesis/heuristics/IntInduction.scala b/src/main/scala/leon/synthesis/heuristics/IntInduction.scala
index b94ceffd967931c7db640f42976a68353385734d..7799a01dee767adf61c1d33848ec00b49bd458bc 100644
--- a/src/main/scala/leon/synthesis/heuristics/IntInduction.scala
+++ b/src/main/scala/leon/synthesis/heuristics/IntInduction.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package synthesis
package heuristics
diff --git a/src/main/scala/leon/synthesis/heuristics/OptimisticInjection.scala b/src/main/scala/leon/synthesis/heuristics/OptimisticInjection.scala
index a4308de79ec42d4ac50b24c0dcabae4291385698..da7ccb3b92de4657493b3e7632810a70f62e86e4 100644
--- a/src/main/scala/leon/synthesis/heuristics/OptimisticInjection.scala
+++ b/src/main/scala/leon/synthesis/heuristics/OptimisticInjection.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package synthesis
package heuristics
diff --git a/src/main/scala/leon/synthesis/heuristics/SelectiveInlining.scala b/src/main/scala/leon/synthesis/heuristics/SelectiveInlining.scala
index b906d37e9355e0a2ca4cb6572c3ca175c4f7ac51..255095bfe90b27a042c7f174efbccb265e4f1034 100644
--- a/src/main/scala/leon/synthesis/heuristics/SelectiveInlining.scala
+++ b/src/main/scala/leon/synthesis/heuristics/SelectiveInlining.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package synthesis
package heuristics
diff --git a/src/main/scala/leon/synthesis/package.scala b/src/main/scala/leon/synthesis/package.scala
index e2b05170509759715681ef6005d04d06a3e33b07..6e41da4a0fdf71b71629dfe9e0a2e95d63cf7e36 100644
--- a/src/main/scala/leon/synthesis/package.scala
+++ b/src/main/scala/leon/synthesis/package.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package object synthesis {
diff --git a/src/main/scala/leon/synthesis/rules/ADTDual.scala b/src/main/scala/leon/synthesis/rules/ADTDual.scala
index 57c31c9989593d438a43a696042dadd5f7e46dd1..7f73a8198f7e84ef47f5404dce945191eb391c13 100644
--- a/src/main/scala/leon/synthesis/rules/ADTDual.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTDual.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package synthesis
package rules
diff --git a/src/main/scala/leon/synthesis/rules/ADTSplit.scala b/src/main/scala/leon/synthesis/rules/ADTSplit.scala
index 2837c7abe9dbab250a5f2dea8badcd76645de41c..5203bd60fa88d9300e51d30f54e700d13c5d65fc 100644
--- a/src/main/scala/leon/synthesis/rules/ADTSplit.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTSplit.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package synthesis
package rules
diff --git a/src/main/scala/leon/synthesis/rules/Assert.scala b/src/main/scala/leon/synthesis/rules/Assert.scala
index efafc204d318141d1cdef74a456269cd2cc56af0..240ed46850b200ab3b666296a1e4f8b23e843fd3 100644
--- a/src/main/scala/leon/synthesis/rules/Assert.scala
+++ b/src/main/scala/leon/synthesis/rules/Assert.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package synthesis
package rules
diff --git a/src/main/scala/leon/synthesis/rules/CaseSplit.scala b/src/main/scala/leon/synthesis/rules/CaseSplit.scala
index f22f97be439f1d084c5b1751042ec07337916e54..bd2a859e5c22a61b7619fa32257b8e95632b6698 100644
--- a/src/main/scala/leon/synthesis/rules/CaseSplit.scala
+++ b/src/main/scala/leon/synthesis/rules/CaseSplit.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package synthesis
package rules
diff --git a/src/main/scala/leon/synthesis/rules/Cegis.scala b/src/main/scala/leon/synthesis/rules/Cegis.scala
index d2d5da2500353534fca251008cde9a185d24f3ef..5b6442206faf4dc71628fb30f25dd4bed9571f76 100644
--- a/src/main/scala/leon/synthesis/rules/Cegis.scala
+++ b/src/main/scala/leon/synthesis/rules/Cegis.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package synthesis
package rules
diff --git a/src/main/scala/leon/synthesis/rules/DetupleInput.scala b/src/main/scala/leon/synthesis/rules/DetupleInput.scala
index 736d89df1c87dab35fcf81c63d75ee4eb4611a80..5bb4045b088aa225cf7b7f34824bb953945911b3 100644
--- a/src/main/scala/leon/synthesis/rules/DetupleInput.scala
+++ b/src/main/scala/leon/synthesis/rules/DetupleInput.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package synthesis
package rules
diff --git a/src/main/scala/leon/synthesis/rules/DetupleOutput.scala b/src/main/scala/leon/synthesis/rules/DetupleOutput.scala
index 3d475f336668bd80d6b4edbb0a89b3632ccba49a..6c026ad806554e9af4208f95321a126938e2e569 100644
--- a/src/main/scala/leon/synthesis/rules/DetupleOutput.scala
+++ b/src/main/scala/leon/synthesis/rules/DetupleOutput.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package synthesis
package rules
diff --git a/src/main/scala/leon/synthesis/rules/Disunification.scala b/src/main/scala/leon/synthesis/rules/Disunification.scala
index b496a4dd41b459ca195b76098ef09caa1c2e91ac..9c8ecada31b758ad8ea43e61873abaf8de5b9ac3 100644
--- a/src/main/scala/leon/synthesis/rules/Disunification.scala
+++ b/src/main/scala/leon/synthesis/rules/Disunification.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package synthesis
package rules
diff --git a/src/main/scala/leon/synthesis/rules/EqualitySplit.scala b/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
index ae6d6da241d570469541574515eff6850af462aa..5d643659a75ae74d2a68cc845dc439505d237b18 100644
--- a/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
+++ b/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package synthesis
package rules
diff --git a/src/main/scala/leon/synthesis/rules/Ground.scala b/src/main/scala/leon/synthesis/rules/Ground.scala
index 73b1a81a56441138f53f9f939919aa4fa8b86720..af1f48622508f8258b0732b111a51c552ab31986 100644
--- a/src/main/scala/leon/synthesis/rules/Ground.scala
+++ b/src/main/scala/leon/synthesis/rules/Ground.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package synthesis
package rules
diff --git a/src/main/scala/leon/synthesis/rules/InequalitySplit.scala b/src/main/scala/leon/synthesis/rules/InequalitySplit.scala
index 6c9e07d73e95c07d259c0b34f274d8a06b0e844e..443040f7fb70a2a728fd2cb43b106d992dd8153c 100644
--- a/src/main/scala/leon/synthesis/rules/InequalitySplit.scala
+++ b/src/main/scala/leon/synthesis/rules/InequalitySplit.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package synthesis
package rules
diff --git a/src/main/scala/leon/synthesis/rules/IntegerEquation.scala b/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
index 60101558d83417f88ab7e864ffad59ff3ca57abb..06a2398fd180f466722cd35b129677c42e2ec844 100644
--- a/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
+++ b/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package synthesis
package rules
diff --git a/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala b/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
index 2c02d10ab7bd4892f995042cbfc9f38248242a18..34902c9cbeb170ec481024a1e5d82cb643f37530 100644
--- a/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
+++ b/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package synthesis
package rules
diff --git a/src/main/scala/leon/synthesis/rules/OnePoint.scala b/src/main/scala/leon/synthesis/rules/OnePoint.scala
index 1b44bbd06369beabe1449b6eb58f4e6595141f4c..d372a21d43d15908149c826ab46949faa9bf1c17 100644
--- a/src/main/scala/leon/synthesis/rules/OnePoint.scala
+++ b/src/main/scala/leon/synthesis/rules/OnePoint.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package synthesis
package rules
diff --git a/src/main/scala/leon/synthesis/rules/OptimisticGround.scala b/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
index aeefe055eeac384a596f3e87306557247b2e86bf..e0935fefc344f28b6154b6eeb72e5857900a4e5c 100644
--- a/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
+++ b/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package synthesis
package rules
diff --git a/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala b/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala
index 2572aebccb6712f17ddd6e867e306be6f3592a59..4d5e0add31e2394feb10a96e73af1ac8340e3c1d 100644
--- a/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala
+++ b/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package synthesis
package rules
diff --git a/src/main/scala/leon/synthesis/rules/Unification.scala b/src/main/scala/leon/synthesis/rules/Unification.scala
index 005f13eedbb1461d0240bac9f3d98220970ef53f..bce329f13aa9726c534a8f806b7252e2d4053af5 100644
--- a/src/main/scala/leon/synthesis/rules/Unification.scala
+++ b/src/main/scala/leon/synthesis/rules/Unification.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package synthesis
package rules
diff --git a/src/main/scala/leon/synthesis/rules/UnusedInput.scala b/src/main/scala/leon/synthesis/rules/UnusedInput.scala
index a3b21fc28a1128562276886e668c947a505e3f75..56b869f50a19701b901989227b0632013dc9a29c 100644
--- a/src/main/scala/leon/synthesis/rules/UnusedInput.scala
+++ b/src/main/scala/leon/synthesis/rules/UnusedInput.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package synthesis
package rules
diff --git a/src/main/scala/leon/synthesis/search/AndOrGraph.scala b/src/main/scala/leon/synthesis/search/AndOrGraph.scala
index 50a7ab859b7f0a980c1e3a922d0b9fd6f306286b..6fd4f3ca86c43c0a701f6a5e2aa9dfddd17aaf68 100644
--- a/src/main/scala/leon/synthesis/search/AndOrGraph.scala
+++ b/src/main/scala/leon/synthesis/search/AndOrGraph.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon.synthesis.search
trait AOTask[S] {
diff --git a/src/main/scala/leon/synthesis/search/AndOrGraphDotConverter.scala b/src/main/scala/leon/synthesis/search/AndOrGraphDotConverter.scala
index 062ada1d740988396d7e25ca4c3bead66607440e..6290f5c1782ece2de7587b4b7bb78fa9755ea8d0 100644
--- a/src/main/scala/leon/synthesis/search/AndOrGraphDotConverter.scala
+++ b/src/main/scala/leon/synthesis/search/AndOrGraphDotConverter.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon.synthesis.search
class AndOrGraphDotConverter[AT <: AOAndTask[S],
diff --git a/src/main/scala/leon/synthesis/search/AndOrGraphParallelSearch.scala b/src/main/scala/leon/synthesis/search/AndOrGraphParallelSearch.scala
index 4ff6259669e7b397bd0fb33eefab21358fbbb894..786d1970dd137eef4bd33e6971a5bcee1ff438e9 100644
--- a/src/main/scala/leon/synthesis/search/AndOrGraphParallelSearch.scala
+++ b/src/main/scala/leon/synthesis/search/AndOrGraphParallelSearch.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon.synthesis.search
import akka.actor._
diff --git a/src/main/scala/leon/synthesis/search/AndOrGraphPartialSolution.scala b/src/main/scala/leon/synthesis/search/AndOrGraphPartialSolution.scala
index 3f9fbdb685d7a07543305c2c58a741002a4e45eb..beda712ac056a9a7cc867af23a876e6d49e895a2 100644
--- a/src/main/scala/leon/synthesis/search/AndOrGraphPartialSolution.scala
+++ b/src/main/scala/leon/synthesis/search/AndOrGraphPartialSolution.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon.synthesis.search
class AndOrGraphPartialSolution[AT <: AOAndTask[S],
diff --git a/src/main/scala/leon/synthesis/search/AndOrGraphSearch.scala b/src/main/scala/leon/synthesis/search/AndOrGraphSearch.scala
index 00593edefa93efddc6ac5f882d9463bd8351b142..42643d7a701fb5a59e19d6ab02f24b51f213c247 100644
--- a/src/main/scala/leon/synthesis/search/AndOrGraphSearch.scala
+++ b/src/main/scala/leon/synthesis/search/AndOrGraphSearch.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon.synthesis.search
abstract class AndOrGraphSearch[AT <: AOAndTask[S],
diff --git a/src/main/scala/leon/synthesis/search/Cost.scala b/src/main/scala/leon/synthesis/search/Cost.scala
index 0ec8ff140ef1d8f3b5c7737842363247b3040c9e..5f7ce459f53a443480b67066827ce522a132a6c1 100644
--- a/src/main/scala/leon/synthesis/search/Cost.scala
+++ b/src/main/scala/leon/synthesis/search/Cost.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon.synthesis.search
trait Cost extends Ordered[Cost] {
diff --git a/src/main/scala/leon/synthesis/utils/Benchmarks.scala b/src/main/scala/leon/synthesis/utils/Benchmarks.scala
index 04998922b5d4b16e8f4ec38613121515774aa809..08226d925d00753ea7a5b6123e383a64c3d281c0 100644
--- a/src/main/scala/leon/synthesis/utils/Benchmarks.scala
+++ b/src/main/scala/leon/synthesis/utils/Benchmarks.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon.synthesis.utils
import leon._
diff --git a/src/main/scala/leon/synthesis/utils/SynthesisProblemExtractionPhase.scala b/src/main/scala/leon/synthesis/utils/SynthesisProblemExtractionPhase.scala
index c31a04a6a99003d96b3c83514a1fb88ac1f4a5d3..a6abacc5d16fe345e01e9255cc929e9c1c4fe5f6 100644
--- a/src/main/scala/leon/synthesis/utils/SynthesisProblemExtractionPhase.scala
+++ b/src/main/scala/leon/synthesis/utils/SynthesisProblemExtractionPhase.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package synthesis
package utils
diff --git a/src/main/scala/leon/termination/SCC.scala b/src/main/scala/leon/termination/SCC.scala
index c0c8f75887133be3897123b66bea9f9d7b9d6464..54a13ec41d1c3585976885e8e86fd5ef9117301a 100644
--- a/src/main/scala/leon/termination/SCC.scala
+++ b/src/main/scala/leon/termination/SCC.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package termination
diff --git a/src/main/scala/leon/termination/SimpleTerminationChecker.scala b/src/main/scala/leon/termination/SimpleTerminationChecker.scala
index 43d18726fbffd9af99d4b6643db3f36fdb1004e5..98303cd74948897246a79157ca0f078350544a9a 100644
--- a/src/main/scala/leon/termination/SimpleTerminationChecker.scala
+++ b/src/main/scala/leon/termination/SimpleTerminationChecker.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package termination
diff --git a/src/main/scala/leon/termination/TerminationChecker.scala b/src/main/scala/leon/termination/TerminationChecker.scala
index ed54acea4cdb6ebdd10041bedae9e104c606a7b7..442f59ab8c6318dfdcea4040b310228e2eeff06e 100644
--- a/src/main/scala/leon/termination/TerminationChecker.scala
+++ b/src/main/scala/leon/termination/TerminationChecker.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package termination
diff --git a/src/main/scala/leon/termination/TerminationPhase.scala b/src/main/scala/leon/termination/TerminationPhase.scala
index b59be31842d3ce4a49a7cff98a185c8f3f126b85..ca44e64339f01bace0b4cdb4a1d68e8b9e94a72b 100644
--- a/src/main/scala/leon/termination/TerminationPhase.scala
+++ b/src/main/scala/leon/termination/TerminationPhase.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package termination
diff --git a/src/main/scala/leon/termination/TerminationReport.scala b/src/main/scala/leon/termination/TerminationReport.scala
index 4a4af2a6e95f091f65abf038e3bb2c6a8a120461..9004d3f103b9c2fe7cdedddec594ec08e201ac55 100644
--- a/src/main/scala/leon/termination/TerminationReport.scala
+++ b/src/main/scala/leon/termination/TerminationReport.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package termination
diff --git a/src/main/scala/leon/testgen/CallGraph.scala b/src/main/scala/leon/testgen/CallGraph.scala
index 2e87d83247a421c29e2eeb894fc08cab6801961c..a81a56ee213223187769fda525fd8d1aeb23fc69 100644
--- a/src/main/scala/leon/testgen/CallGraph.scala
+++ b/src/main/scala/leon/testgen/CallGraph.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon.testgen
import leon.purescala.Definitions._
diff --git a/src/main/scala/leon/testgen/TestGeneration.scala b/src/main/scala/leon/testgen/TestGeneration.scala
index 27426910ba3e68c4d926efa1745834bfdf3f424e..7073f68f74a67e211b2061e9cf3f29d0bc10d4d8 100644
--- a/src/main/scala/leon/testgen/TestGeneration.scala
+++ b/src/main/scala/leon/testgen/TestGeneration.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package testgen
diff --git a/src/main/scala/leon/verification/AnalysisPhase.scala b/src/main/scala/leon/verification/AnalysisPhase.scala
index fe953a272b53085bc0c15935b32026b6854aa4f3..193ebcb75fb4d917c910e9d0ed5745999b7559c8 100644
--- a/src/main/scala/leon/verification/AnalysisPhase.scala
+++ b/src/main/scala/leon/verification/AnalysisPhase.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package verification
diff --git a/src/main/scala/leon/verification/DefaultTactic.scala b/src/main/scala/leon/verification/DefaultTactic.scala
index cdc752a50930dc3cecd6230a7555cf998371ea0b..d866afdb4ac00650b4783dc519353d79a12fa3e9 100644
--- a/src/main/scala/leon/verification/DefaultTactic.scala
+++ b/src/main/scala/leon/verification/DefaultTactic.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package verification
diff --git a/src/main/scala/leon/verification/InductionTactic.scala b/src/main/scala/leon/verification/InductionTactic.scala
index ba7a210f1b12a7328b1a22cfd1e9fafdc6b2aaba..26d9de252f9eed3826a8d4db34f7cbe4e0ac1f4d 100644
--- a/src/main/scala/leon/verification/InductionTactic.scala
+++ b/src/main/scala/leon/verification/InductionTactic.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package verification
diff --git a/src/main/scala/leon/verification/Tactic.scala b/src/main/scala/leon/verification/Tactic.scala
index 3a00f2ab7f9a7dfcd731b0e48273af09de60f544..dc31d71e17a3ace3bc11e161d6c7e5c4630546ee 100644
--- a/src/main/scala/leon/verification/Tactic.scala
+++ b/src/main/scala/leon/verification/Tactic.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package verification
diff --git a/src/main/scala/leon/verification/VerificationCondition.scala b/src/main/scala/leon/verification/VerificationCondition.scala
index fee77a683fe344916f5a036cb826a394d16fa96a..48b6a2e223efb5775f04972c9d647058a46be530 100644
--- a/src/main/scala/leon/verification/VerificationCondition.scala
+++ b/src/main/scala/leon/verification/VerificationCondition.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon.verification
import leon.purescala.Trees._
diff --git a/src/main/scala/leon/verification/VerificationContext.scala b/src/main/scala/leon/verification/VerificationContext.scala
index 87300c40cc8d179ab726de6ce1ad9795e50a4be8..aede661c0e32e23d08e1c9057856f4c72cf2c4a1 100644
--- a/src/main/scala/leon/verification/VerificationContext.scala
+++ b/src/main/scala/leon/verification/VerificationContext.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package verification
diff --git a/src/main/scala/leon/verification/VerificationReport.scala b/src/main/scala/leon/verification/VerificationReport.scala
index e40693199da6951cf4103618bbb342f501a2422f..34245e544eeacf48587fe6966364bc1d6d4ba052 100644
--- a/src/main/scala/leon/verification/VerificationReport.scala
+++ b/src/main/scala/leon/verification/VerificationReport.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package verification
diff --git a/src/main/scala/leon/xlang/ArrayTransformation.scala b/src/main/scala/leon/xlang/ArrayTransformation.scala
index 4a9017597ff67ecee4a0d5f9c7972afc37ab564f..fb930993103cb6f70cf92b50a10db3999b9eca43 100644
--- a/src/main/scala/leon/xlang/ArrayTransformation.scala
+++ b/src/main/scala/leon/xlang/ArrayTransformation.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon.xlang
import leon.TransformationPhase
diff --git a/src/main/scala/leon/xlang/EpsilonElimination.scala b/src/main/scala/leon/xlang/EpsilonElimination.scala
index d36207822991b6fc2e25230d6ab837a13afce632..7a9d3245f59650d53e8b42fe75146e66f2b11198 100644
--- a/src/main/scala/leon/xlang/EpsilonElimination.scala
+++ b/src/main/scala/leon/xlang/EpsilonElimination.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon.xlang
import leon.TransformationPhase
diff --git a/src/main/scala/leon/xlang/FunctionClosure.scala b/src/main/scala/leon/xlang/FunctionClosure.scala
index c6fc16e1f785867c3b54a7f2da2ae87313b2f791..0feb5476c83f3b6858c0b11d60837038eca2198d 100644
--- a/src/main/scala/leon/xlang/FunctionClosure.scala
+++ b/src/main/scala/leon/xlang/FunctionClosure.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package xlang
diff --git a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
index aeda95f09de30c6b001f2f8f827ae60d3bfa3d1e..e68aa363801fbd3bf4a1b0f03bc65f20f903c800 100644
--- a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
+++ b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package xlang
diff --git a/src/main/scala/leon/xlang/TreeOps.scala b/src/main/scala/leon/xlang/TreeOps.scala
index 5eb20b284178ad8009b1caad89c4b86e6240c23e..0e8c362aa589e9b872209c3db89ed94e05bbc24e 100644
--- a/src/main/scala/leon/xlang/TreeOps.scala
+++ b/src/main/scala/leon/xlang/TreeOps.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package xlang
diff --git a/src/main/scala/leon/xlang/Trees.scala b/src/main/scala/leon/xlang/Trees.scala
index 2773078e7faa0dadc8dd31f6579b4cf57aae5805..97313acf18bcc977a8aa06481b732c1195b87446 100644
--- a/src/main/scala/leon/xlang/Trees.scala
+++ b/src/main/scala/leon/xlang/Trees.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package xlang
diff --git a/src/main/scala/leon/xlang/XlangAnalysisPhase.scala b/src/main/scala/leon/xlang/XlangAnalysisPhase.scala
index 318e481cdfd698a7c3eb78e1ad5f724efc8af254..13c8d619fd658f21de48466370dbb5b0f7fe9a38 100644
--- a/src/main/scala/leon/xlang/XlangAnalysisPhase.scala
+++ b/src/main/scala/leon/xlang/XlangAnalysisPhase.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package xlang
diff --git a/src/main/scala/leon/z3plugins/bapa/AST.scala b/src/main/scala/leon/z3plugins/bapa/AST.scala
index 2f2a328f3785f7f0f6a492fd5290d703faa6b8f2..6169a9f741617c3b546d63e3c9c3855cbb98b16f 100644
--- a/src/main/scala/leon/z3plugins/bapa/AST.scala
+++ b/src/main/scala/leon/z3plugins/bapa/AST.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package purescala.z3plugins.bapa
import z3.scala._
diff --git a/src/main/scala/leon/z3plugins/bapa/BAPATheory.scala b/src/main/scala/leon/z3plugins/bapa/BAPATheory.scala
index da9d93fe4710b8d7fe151583cb623abcb3434af6..19355501b93398ad233079aead6f809783170365 100644
--- a/src/main/scala/leon/z3plugins/bapa/BAPATheory.scala
+++ b/src/main/scala/leon/z3plugins/bapa/BAPATheory.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
/********************************************************************
WARNING : THIS VERSION IS NOT USED (AND CERTAINLY NOT MAINTAINED).
diff --git a/src/main/scala/leon/z3plugins/bapa/BAPATheoryBubbles.scala b/src/main/scala/leon/z3plugins/bapa/BAPATheoryBubbles.scala
index 16a792d8fe2bbf7e359c3c808fd5a9a9f5827bcf..e59fcbe546d2b7fd2a33f3ecdd0b921193a3b1d5 100644
--- a/src/main/scala/leon/z3plugins/bapa/BAPATheoryBubbles.scala
+++ b/src/main/scala/leon/z3plugins/bapa/BAPATheoryBubbles.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package purescala.z3plugins.bapa
import scala.collection.mutable.{Stack, ArrayBuffer, Set => MutableSet, HashMap => MutableMap}
diff --git a/src/main/scala/leon/z3plugins/bapa/BAPATheoryEqc.scala b/src/main/scala/leon/z3plugins/bapa/BAPATheoryEqc.scala
index 92fb7d267ab666922d9280e544967a5655e9a43f..41270464800275d5d1ff30df0eed9685bb241a3f 100644
--- a/src/main/scala/leon/z3plugins/bapa/BAPATheoryEqc.scala
+++ b/src/main/scala/leon/z3plugins/bapa/BAPATheoryEqc.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
/********************************************************************
WARNING : THIS VERSION IS NOT USED (AND CERTAINLY NOT MAINTAINED).
diff --git a/src/main/scala/leon/z3plugins/bapa/Bubbles.scala b/src/main/scala/leon/z3plugins/bapa/Bubbles.scala
index f5a97d146f5add7300be6b43d95e936d9a26751b..a60c99016a1a7f9cc35cd19177e321cee049d12e 100644
--- a/src/main/scala/leon/z3plugins/bapa/Bubbles.scala
+++ b/src/main/scala/leon/z3plugins/bapa/Bubbles.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package purescala.z3plugins.bapa
import scala.collection.mutable.{HashSet => MutableSet, HashMap => MutableMap, ArrayBuffer}
diff --git a/src/main/scala/leon/z3plugins/bapa/NormalForms.scala b/src/main/scala/leon/z3plugins/bapa/NormalForms.scala
index b1f931247a46df9fe219f3218c6b47ab3d9f4ec5..df3e7a55b9860e295d03f0b53e1efdde15c1f13f 100644
--- a/src/main/scala/leon/z3plugins/bapa/NormalForms.scala
+++ b/src/main/scala/leon/z3plugins/bapa/NormalForms.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package purescala.z3plugins.bapa
import z3.scala.Z3Context
diff --git a/src/main/scala/leon/z3plugins/bapa/PrettyPrinter.scala b/src/main/scala/leon/z3plugins/bapa/PrettyPrinter.scala
index 6b4c1ea31f699e0a496b7ea0bdafacbfb50ca21a..9330832d8d24d2c4fb2d090acad843a8b33fb9c1 100644
--- a/src/main/scala/leon/z3plugins/bapa/PrettyPrinter.scala
+++ b/src/main/scala/leon/z3plugins/bapa/PrettyPrinter.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package purescala.z3plugins.bapa
import scala.text.{Document, DocBreak}
diff --git a/src/main/scala/leon/z3plugins/bapa/VennRegions.scala b/src/main/scala/leon/z3plugins/bapa/VennRegions.scala
index 4f5f3e616fffd849612be4f726954ebe636f54a8..3e8dde3ca4f3ea4f71a00b2c4308925b8df8567a 100644
--- a/src/main/scala/leon/z3plugins/bapa/VennRegions.scala
+++ b/src/main/scala/leon/z3plugins/bapa/VennRegions.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package purescala.z3plugins.bapa
import scala.collection.mutable.{ArrayBuffer,HashMap}
diff --git a/src/test/resources/regression/verification/purescala/error/InstanceOf1.scala b/src/test/resources/regression/verification/purescala/error/InstanceOf1.scala
index a1974b4bcf8c92f320f8357297536a6053c11b98..a9f9fa5d8fd6b24b46eff039c70d2bb51b2b82a7 100644
--- a/src/test/resources/regression/verification/purescala/error/InstanceOf1.scala
+++ b/src/test/resources/regression/verification/purescala/error/InstanceOf1.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
object InstanceOf1 {
abstract class A
diff --git a/src/test/resources/regression/verification/purescala/invalid/Choose1.scala b/src/test/resources/regression/verification/purescala/invalid/Choose1.scala
index a0ac78daffe87cd730f1fe9e0477c175f52abb0d..663c15d4e87c729a52311dd064cc939ac976030a 100644
--- a/src/test/resources/regression/verification/purescala/invalid/Choose1.scala
+++ b/src/test/resources/regression/verification/purescala/invalid/Choose1.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
import leon.Annotations._
import leon.Utils._
diff --git a/src/test/resources/regression/verification/purescala/invalid/FiniteSort.scala b/src/test/resources/regression/verification/purescala/invalid/FiniteSort.scala
index 4020135aca5f042d07a693cbdbe1f7dce8195361..f7b0ea17a96c1b4771bfcbf0e7f5428e9d85fc95 100644
--- a/src/test/resources/regression/verification/purescala/invalid/FiniteSort.scala
+++ b/src/test/resources/regression/verification/purescala/invalid/FiniteSort.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
import leon.Utils._
object FiniteSorting {
diff --git a/src/test/resources/regression/verification/purescala/invalid/InsertionSort.scala b/src/test/resources/regression/verification/purescala/invalid/InsertionSort.scala
index fd9d8d7b6b216de3ac120daed8a798c7eecf7813..d8c2d029e818ace24d9be936dd6e64396f938915 100644
--- a/src/test/resources/regression/verification/purescala/invalid/InsertionSort.scala
+++ b/src/test/resources/regression/verification/purescala/invalid/InsertionSort.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
import scala.collection.immutable.Set
import leon.Annotations._
import leon.Utils._
diff --git a/src/test/resources/regression/verification/purescala/invalid/ListOperations.scala b/src/test/resources/regression/verification/purescala/invalid/ListOperations.scala
index a4fc4f8dc44a90f59a772b52b1a05053316e94d2..b3b8a2f90ebbf941b9ef9b73ebb839e3df1cbf99 100644
--- a/src/test/resources/regression/verification/purescala/invalid/ListOperations.scala
+++ b/src/test/resources/regression/verification/purescala/invalid/ListOperations.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
import scala.collection.immutable.Set
import leon.Annotations._
import leon.Utils._
diff --git a/src/test/resources/regression/verification/purescala/invalid/MyTuple1.scala b/src/test/resources/regression/verification/purescala/invalid/MyTuple1.scala
index f2b06b5b28e405bfb2487875c8e964b8f212792c..200bf2086a8a1991e918431cf6cae9557d4e2ee7 100644
--- a/src/test/resources/regression/verification/purescala/invalid/MyTuple1.scala
+++ b/src/test/resources/regression/verification/purescala/invalid/MyTuple1.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
object MyTuple1 {
def foo(): Int = {
diff --git a/src/test/resources/regression/verification/purescala/invalid/MyTuple2.scala b/src/test/resources/regression/verification/purescala/invalid/MyTuple2.scala
index 22b62dc75b75b3193cb2f304118a89afbc90eb91..b190043bfb697f83192ee383485ac25279015159 100644
--- a/src/test/resources/regression/verification/purescala/invalid/MyTuple2.scala
+++ b/src/test/resources/regression/verification/purescala/invalid/MyTuple2.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
object MyTuple2 {
abstract class A
diff --git a/src/test/resources/regression/verification/purescala/invalid/MyTuple3.scala b/src/test/resources/regression/verification/purescala/invalid/MyTuple3.scala
index da9f85b16a48f0676d1f15741ad47536e14b57ab..5a6d37dd3a7a4f147ccb26d7279d54237bdc837c 100644
--- a/src/test/resources/regression/verification/purescala/invalid/MyTuple3.scala
+++ b/src/test/resources/regression/verification/purescala/invalid/MyTuple3.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
object MyTuple3 {
def foo(t: (Int, Int)): (Int, Int) = {
diff --git a/src/test/resources/regression/verification/purescala/invalid/PropositionalLogic.scala b/src/test/resources/regression/verification/purescala/invalid/PropositionalLogic.scala
index a35c3ef9be56871900d5e9474b385f0896edccd4..3018379ccd3bbc179305459524689fdb06996dc8 100644
--- a/src/test/resources/regression/verification/purescala/invalid/PropositionalLogic.scala
+++ b/src/test/resources/regression/verification/purescala/invalid/PropositionalLogic.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
import scala.collection.immutable.Set
import leon.Utils._
import leon.Annotations._
diff --git a/src/test/resources/regression/verification/purescala/invalid/RedBlackTree.scala b/src/test/resources/regression/verification/purescala/invalid/RedBlackTree.scala
index 3baf9d0151310ef2cc28c44607f597b0c95a163c..f5478d73479e17f58b0a708420440ae4b03c4b3f 100644
--- a/src/test/resources/regression/verification/purescala/invalid/RedBlackTree.scala
+++ b/src/test/resources/regression/verification/purescala/invalid/RedBlackTree.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
import scala.collection.immutable.Set
import leon.Annotations._
import leon.Utils._
diff --git a/src/test/resources/regression/verification/purescala/invalid/Unit1.scala b/src/test/resources/regression/verification/purescala/invalid/Unit1.scala
index 789a8f058cd8145a0dd3b7bb0d72d44fb92ee94e..ed3d6fcd394be796169577860de048e2395d6bfa 100644
--- a/src/test/resources/regression/verification/purescala/invalid/Unit1.scala
+++ b/src/test/resources/regression/verification/purescala/invalid/Unit1.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
object Unit1 {
def foo(u: Unit): Unit = ({
diff --git a/src/test/resources/regression/verification/purescala/valid/AmortizedQueue.scala b/src/test/resources/regression/verification/purescala/valid/AmortizedQueue.scala
index dd5a75f89735805a74612665e487aa8fa99ec397..81979fa4d18b20f0c957fad851bdce15971ee820 100644
--- a/src/test/resources/regression/verification/purescala/valid/AmortizedQueue.scala
+++ b/src/test/resources/regression/verification/purescala/valid/AmortizedQueue.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
import scala.collection.immutable.Set
import leon.Utils._
import leon.Annotations._
diff --git a/src/test/resources/regression/verification/purescala/valid/AssociativeList.scala b/src/test/resources/regression/verification/purescala/valid/AssociativeList.scala
index 0356d8ec0b4b56a3c6cc78171477f8c5810cbf37..ad450a93c81a006986ebd20b7f2a47cb761c0450 100644
--- a/src/test/resources/regression/verification/purescala/valid/AssociativeList.scala
+++ b/src/test/resources/regression/verification/purescala/valid/AssociativeList.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
import scala.collection.immutable.Set
import leon.Utils._
import leon.Annotations._
diff --git a/src/test/resources/regression/verification/purescala/valid/BestRealTypes.scala b/src/test/resources/regression/verification/purescala/valid/BestRealTypes.scala
index e78cb0b0d1bce0cb54a13a839f9e4032a3eef31c..c68eb99b23affb0a41537f38fd50460cb2ccdba6 100644
--- a/src/test/resources/regression/verification/purescala/valid/BestRealTypes.scala
+++ b/src/test/resources/regression/verification/purescala/valid/BestRealTypes.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
import leon.Utils._
/** This benchmarks tests some potential issues with the legacy "bestRealType" function, which was original introduced to work around
diff --git a/src/test/resources/regression/verification/purescala/valid/CaseObject1.scala b/src/test/resources/regression/verification/purescala/valid/CaseObject1.scala
index 90dcdf064faab6e20dbfe6744d5c7bdadf72c324..4398b99c19c7f82a85fb6384eff229c697bc91be 100644
--- a/src/test/resources/regression/verification/purescala/valid/CaseObject1.scala
+++ b/src/test/resources/regression/verification/purescala/valid/CaseObject1.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
object CaseObject1 {
abstract sealed class A
diff --git a/src/test/resources/regression/verification/purescala/valid/Choose1.scala b/src/test/resources/regression/verification/purescala/valid/Choose1.scala
index 620b87811a0f867454168e1933ad48693603e83b..ebcf96f1799a578d3784240d0a9ecdfe6851f9e6 100644
--- a/src/test/resources/regression/verification/purescala/valid/Choose1.scala
+++ b/src/test/resources/regression/verification/purescala/valid/Choose1.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
import leon.Annotations._
import leon.Utils._
diff --git a/src/test/resources/regression/verification/purescala/valid/Field1.scala b/src/test/resources/regression/verification/purescala/valid/Field1.scala
index 116557ab7b883d01a10168aeaf529d5300ee5f19..f24e3896cb90cf3fbd6b34d4b13fd425f595c618 100644
--- a/src/test/resources/regression/verification/purescala/valid/Field1.scala
+++ b/src/test/resources/regression/verification/purescala/valid/Field1.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
object Field1 {
abstract sealed class A
diff --git a/src/test/resources/regression/verification/purescala/valid/Field2.scala b/src/test/resources/regression/verification/purescala/valid/Field2.scala
index 9a96610235a68754b84e58f73f5e435ce642ebc9..dd62e0a556e712a4040e64bd8166a6f3614e4ed8 100644
--- a/src/test/resources/regression/verification/purescala/valid/Field2.scala
+++ b/src/test/resources/regression/verification/purescala/valid/Field2.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
object Field2 {
abstract sealed class A
diff --git a/src/test/resources/regression/verification/purescala/valid/FiniteSort.scala b/src/test/resources/regression/verification/purescala/valid/FiniteSort.scala
index 5a4e243b833052c0af6bc011e191bb6d28ea42a0..01f2caeeda16345e42173547a42c23f72483ffd7 100644
--- a/src/test/resources/regression/verification/purescala/valid/FiniteSort.scala
+++ b/src/test/resources/regression/verification/purescala/valid/FiniteSort.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
import leon.Utils._
object FiniteSorting {
diff --git a/src/test/resources/regression/verification/purescala/valid/InsertionSort.scala b/src/test/resources/regression/verification/purescala/valid/InsertionSort.scala
index a4fffee353ed4a24c696dc41ebc095c8dc668acf..630518aa3b01d538394353d7258902f94053ec99 100644
--- a/src/test/resources/regression/verification/purescala/valid/InsertionSort.scala
+++ b/src/test/resources/regression/verification/purescala/valid/InsertionSort.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
import scala.collection.immutable.Set
import leon.Annotations._
import leon.Utils._
diff --git a/src/test/resources/regression/verification/purescala/valid/InstanceOf1.scala b/src/test/resources/regression/verification/purescala/valid/InstanceOf1.scala
index 1c52338bbda859f82ef7ea619af088b9c1a1812d..14aaa5a166443760ab8dff802d436410aef2bd21 100644
--- a/src/test/resources/regression/verification/purescala/valid/InstanceOf1.scala
+++ b/src/test/resources/regression/verification/purescala/valid/InstanceOf1.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
object InstanceOf1 {
abstract class A
diff --git a/src/test/resources/regression/verification/purescala/valid/ListOperations.scala b/src/test/resources/regression/verification/purescala/valid/ListOperations.scala
index 27541d9bd0cea5daf7e0fee915ce937cc28fadc9..9f0b8da37fdab144679b9cce226a4a55b2784afd 100644
--- a/src/test/resources/regression/verification/purescala/valid/ListOperations.scala
+++ b/src/test/resources/regression/verification/purescala/valid/ListOperations.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
import scala.collection.immutable.Set
import leon.Annotations._
import leon.Utils._
diff --git a/src/test/resources/regression/verification/purescala/valid/LiteralMaps.scala b/src/test/resources/regression/verification/purescala/valid/LiteralMaps.scala
index dab0d37412a50b2db1293391dc955c4cf7df9dbb..70f1a32eb7c77c364e8cbe72f138328e8f49a106 100644
--- a/src/test/resources/regression/verification/purescala/valid/LiteralMaps.scala
+++ b/src/test/resources/regression/verification/purescala/valid/LiteralMaps.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
object LiteralMaps {
def test(): Map[Int, Int] = {
Map(1 -> 2, 3 -> 4, (5, 6))
diff --git a/src/test/resources/regression/verification/purescala/valid/MergeSort.scala b/src/test/resources/regression/verification/purescala/valid/MergeSort.scala
index c3592319fb3223b43c64480d9ee3a7b63c513973..32c0c2ddb72faf1e9793d5c430d608eba0736de9 100644
--- a/src/test/resources/regression/verification/purescala/valid/MergeSort.scala
+++ b/src/test/resources/regression/verification/purescala/valid/MergeSort.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
import leon.Annotations._
import leon.Utils._
diff --git a/src/test/resources/regression/verification/purescala/valid/MyMap.scala b/src/test/resources/regression/verification/purescala/valid/MyMap.scala
index c71bfcf526ff0c7f0f0c82e8e7ac6732f66b4557..5d039ff9463c7e01c107366820551098a7203ad3 100644
--- a/src/test/resources/regression/verification/purescala/valid/MyMap.scala
+++ b/src/test/resources/regression/verification/purescala/valid/MyMap.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
import leon.Utils._
object MyMap {
diff --git a/src/test/resources/regression/verification/purescala/valid/MySet.scala b/src/test/resources/regression/verification/purescala/valid/MySet.scala
index 3b6fdf42fc82b4e939a5be8976582aeec98fc355..5be8bb6e76cdda433eae19d9bfca52969c62b17c 100644
--- a/src/test/resources/regression/verification/purescala/valid/MySet.scala
+++ b/src/test/resources/regression/verification/purescala/valid/MySet.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
import leon.Utils._
object MySet {
diff --git a/src/test/resources/regression/verification/purescala/valid/MyTuple1.scala b/src/test/resources/regression/verification/purescala/valid/MyTuple1.scala
index 48383898e203c723751a7a53869ac6c8c69ae3b5..65a0ecfba47a23a2c445b9e62c659979da33a0b9 100644
--- a/src/test/resources/regression/verification/purescala/valid/MyTuple1.scala
+++ b/src/test/resources/regression/verification/purescala/valid/MyTuple1.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
object MyTuple1 {
def foo(): Int = {
diff --git a/src/test/resources/regression/verification/purescala/valid/MyTuple2.scala b/src/test/resources/regression/verification/purescala/valid/MyTuple2.scala
index 9fd21eb20b14350d86d06071800ec3b86acc1a84..d9ffb991609073a0bfe3e0c826b7a231fc8ffc3a 100644
--- a/src/test/resources/regression/verification/purescala/valid/MyTuple2.scala
+++ b/src/test/resources/regression/verification/purescala/valid/MyTuple2.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
object MyTuple2 {
abstract class A
diff --git a/src/test/resources/regression/verification/purescala/valid/MyTuple3.scala b/src/test/resources/regression/verification/purescala/valid/MyTuple3.scala
index 2e14c067b78d86d4d915eb72178169d641e9755a..981c83a5b204a3fce2a2b50e2adb30062a923a04 100644
--- a/src/test/resources/regression/verification/purescala/valid/MyTuple3.scala
+++ b/src/test/resources/regression/verification/purescala/valid/MyTuple3.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
object MyTuple3 {
def foo(): Int = {
diff --git a/src/test/resources/regression/verification/purescala/valid/MyTuple4.scala b/src/test/resources/regression/verification/purescala/valid/MyTuple4.scala
index 6fcfed661beca0487da4b02db71677e2dbaac60e..9c68b867e3ffd430c87ec1d98dd39c68e404e2bb 100644
--- a/src/test/resources/regression/verification/purescala/valid/MyTuple4.scala
+++ b/src/test/resources/regression/verification/purescala/valid/MyTuple4.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
object MyTuple4 {
diff --git a/src/test/resources/regression/verification/purescala/valid/MyTuple5.scala b/src/test/resources/regression/verification/purescala/valid/MyTuple5.scala
index 6a55bc8c9cdbc4f70be7a6b79c8d11137ecb0d71..21544dae2c0c15dc767cd4ae548f136bbb084df5 100644
--- a/src/test/resources/regression/verification/purescala/valid/MyTuple5.scala
+++ b/src/test/resources/regression/verification/purescala/valid/MyTuple5.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
object MyTuple1 {
abstract class A
diff --git a/src/test/resources/regression/verification/purescala/valid/MyTuple6.scala b/src/test/resources/regression/verification/purescala/valid/MyTuple6.scala
index a54710fbbe54d9532a5ab4d2ba9906a48ad37acc..562fdcb97e8b68abfa0fe6b3c5fa0868096bb787 100644
--- a/src/test/resources/regression/verification/purescala/valid/MyTuple6.scala
+++ b/src/test/resources/regression/verification/purescala/valid/MyTuple6.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
object MyTuple6 {
def foo(t: (Int, Int)): (Int, Int) = {
diff --git a/src/test/resources/regression/verification/purescala/valid/PropositionalLogic.scala b/src/test/resources/regression/verification/purescala/valid/PropositionalLogic.scala
index 5dd7d505749372763c4bcca8aba0695c5b389e51..60c1ef7a2fd62dd7e24c9c5c63a26e12820f813c 100644
--- a/src/test/resources/regression/verification/purescala/valid/PropositionalLogic.scala
+++ b/src/test/resources/regression/verification/purescala/valid/PropositionalLogic.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
import scala.collection.immutable.Set
import leon.Utils._
import leon.Annotations._
diff --git a/src/test/resources/regression/verification/purescala/valid/RedBlackTree.scala b/src/test/resources/regression/verification/purescala/valid/RedBlackTree.scala
index 65d873ad4646bc098d11b8dd95e071ddf72c87ba..3cbe4800d94cf092de210c0a0320fd88f2c51dc3 100644
--- a/src/test/resources/regression/verification/purescala/valid/RedBlackTree.scala
+++ b/src/test/resources/regression/verification/purescala/valid/RedBlackTree.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
import scala.collection.immutable.Set
import leon.Annotations._
import leon.Utils._
diff --git a/src/test/resources/regression/verification/purescala/valid/SearchLinkedList.scala b/src/test/resources/regression/verification/purescala/valid/SearchLinkedList.scala
index 2c137fd4ad6b9d411f7e14b4ada6b834234c9e9e..64230dbd7ca744bff5cf55c554c7f5ce698aaff1 100644
--- a/src/test/resources/regression/verification/purescala/valid/SearchLinkedList.scala
+++ b/src/test/resources/regression/verification/purescala/valid/SearchLinkedList.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
import scala.collection.immutable.Set
import leon.Utils._
import leon.Annotations._
diff --git a/src/test/resources/regression/verification/purescala/valid/Subtyping1.scala b/src/test/resources/regression/verification/purescala/valid/Subtyping1.scala
index 618d4c1c52bdb2df4c2025285a514ead75923d6e..1bffd51adeb32daad7587296ff5d567aa36f2fe9 100644
--- a/src/test/resources/regression/verification/purescala/valid/Subtyping1.scala
+++ b/src/test/resources/regression/verification/purescala/valid/Subtyping1.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
object Subtyping1 {
sealed abstract class Tree
diff --git a/src/test/resources/regression/verification/purescala/valid/Subtyping2.scala b/src/test/resources/regression/verification/purescala/valid/Subtyping2.scala
index c6e79227178fdbd2b54bc2f67d309ce6945bdf73..fc7f2e4cae820fe949687cc23448d0aec92edb8a 100644
--- a/src/test/resources/regression/verification/purescala/valid/Subtyping2.scala
+++ b/src/test/resources/regression/verification/purescala/valid/Subtyping2.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
import leon.Utils._
object Test {
diff --git a/src/test/resources/regression/verification/purescala/valid/SumAndMax.scala b/src/test/resources/regression/verification/purescala/valid/SumAndMax.scala
index 0aa4ce7060a391d34dd047338fcd1f638054843f..629dc6dba22584f8413b7b32ab0457713008f54d 100644
--- a/src/test/resources/regression/verification/purescala/valid/SumAndMax.scala
+++ b/src/test/resources/regression/verification/purescala/valid/SumAndMax.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
import leon.Utils._
import leon.Annotations._
diff --git a/src/test/resources/regression/verification/purescala/valid/Unit1.scala b/src/test/resources/regression/verification/purescala/valid/Unit1.scala
index a7b890d762648cba480c817506c7eee22259860d..0f4d78ae9d2d0e84ac5a3aa5f88089f921ded61a 100644
--- a/src/test/resources/regression/verification/purescala/valid/Unit1.scala
+++ b/src/test/resources/regression/verification/purescala/valid/Unit1.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
object Unit1 {
def foo(): Unit = ({
diff --git a/src/test/resources/regression/verification/purescala/valid/Unit2.scala b/src/test/resources/regression/verification/purescala/valid/Unit2.scala
index ac659589af503a8a79f261f9eb05be095e2e0943..08c96fc22ef7b3c6bb731930d4cae179ed3db3cc 100644
--- a/src/test/resources/regression/verification/purescala/valid/Unit2.scala
+++ b/src/test/resources/regression/verification/purescala/valid/Unit2.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
object Unit2 {
def foo(u: Unit): Unit = {
diff --git a/src/test/resources/regression/verification/xlang/error/Array1.scala b/src/test/resources/regression/verification/xlang/error/Array1.scala
index d0056f18864ba168abb5735daf0db1e0bb76eda5..f8d420de5ee58ef4eacc8930899261b4ffc60516 100644
--- a/src/test/resources/regression/verification/xlang/error/Array1.scala
+++ b/src/test/resources/regression/verification/xlang/error/Array1.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
object Array1 {
def foo(): Int = {
diff --git a/src/test/resources/regression/verification/xlang/error/Array10.scala b/src/test/resources/regression/verification/xlang/error/Array10.scala
index 9973626b83a01c7a8a944bcf808274d7989b3a66..ed596fec617c4fcb92cf9c3d74c27af2d80883d9 100644
--- a/src/test/resources/regression/verification/xlang/error/Array10.scala
+++ b/src/test/resources/regression/verification/xlang/error/Array10.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
object Array10 {
def foo(): Int = {
diff --git a/src/test/resources/regression/verification/xlang/error/Array2.scala b/src/test/resources/regression/verification/xlang/error/Array2.scala
index 9154460c37237761b6c8f2d0ecb0b34fb3ec0bf6..4de4eaf4dd28661a7c09a7e4e933ff107e7327a3 100644
--- a/src/test/resources/regression/verification/xlang/error/Array2.scala
+++ b/src/test/resources/regression/verification/xlang/error/Array2.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
object Array2 {
def foo(): Int = {
diff --git a/src/test/resources/regression/verification/xlang/error/Array3.scala b/src/test/resources/regression/verification/xlang/error/Array3.scala
index a2c2fbd6ddfde2b3cca2dcc08fb61a79f0ae471c..b501eadbd8d6b199914d3540931614d62a3d9b7e 100644
--- a/src/test/resources/regression/verification/xlang/error/Array3.scala
+++ b/src/test/resources/regression/verification/xlang/error/Array3.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
object Array3 {
def foo(): Int = {
diff --git a/src/test/resources/regression/verification/xlang/error/Array4.scala b/src/test/resources/regression/verification/xlang/error/Array4.scala
index 5ab0115af5e8737c6baab851822643490e79334f..bc9b5fd40ab365fba5e8b310ac558d1cc6946fa3 100644
--- a/src/test/resources/regression/verification/xlang/error/Array4.scala
+++ b/src/test/resources/regression/verification/xlang/error/Array4.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
object Array4 {
def foo(a: Array[Int]): Int = {
diff --git a/src/test/resources/regression/verification/xlang/error/Array5.scala b/src/test/resources/regression/verification/xlang/error/Array5.scala
index 005d3d389dd1e748d139283a6fbdcb93aa8d525c..55eef8f26991b0b628a527a37b48e57a1e723eaa 100644
--- a/src/test/resources/regression/verification/xlang/error/Array5.scala
+++ b/src/test/resources/regression/verification/xlang/error/Array5.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
object Array5 {
def foo(a: Array[Int]): Int = {
diff --git a/src/test/resources/regression/verification/xlang/error/Array6.scala b/src/test/resources/regression/verification/xlang/error/Array6.scala
index 15c87a08554c7e9563cbad9b47a881376e45a4c5..818271c0c35d2f480ba9b277fa61121713f7f405 100644
--- a/src/test/resources/regression/verification/xlang/error/Array6.scala
+++ b/src/test/resources/regression/verification/xlang/error/Array6.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
object Array6 {
diff --git a/src/test/resources/regression/verification/xlang/error/Array7.scala b/src/test/resources/regression/verification/xlang/error/Array7.scala
index abb83e1c0bd931bf1d41a132fef6fb74ea25318b..079f2231b65f289310a0b0648da68beae7f50721 100644
--- a/src/test/resources/regression/verification/xlang/error/Array7.scala
+++ b/src/test/resources/regression/verification/xlang/error/Array7.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
object Array7 {
def foo(): Int = {
diff --git a/src/test/resources/regression/verification/xlang/error/Array8.scala b/src/test/resources/regression/verification/xlang/error/Array8.scala
index 89af32efdb89273ecf6b275b5a8f2f787bb73a1f..098c001bba3a50906bdf480299b4feddd94641af 100644
--- a/src/test/resources/regression/verification/xlang/error/Array8.scala
+++ b/src/test/resources/regression/verification/xlang/error/Array8.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
object Array8 {
def foo(a: Array[Int]): Array[Int] = {
diff --git a/src/test/resources/regression/verification/xlang/error/Array9.scala b/src/test/resources/regression/verification/xlang/error/Array9.scala
index 5dc9d3aea24f7c38b8a374659058c9d0ca7fb336..edbd5beb31313133d20c6c8a0e918accdcb25d45 100644
--- a/src/test/resources/regression/verification/xlang/error/Array9.scala
+++ b/src/test/resources/regression/verification/xlang/error/Array9.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
object Array9 {
def foo(a: Array[Int]): Int = {
diff --git a/src/test/resources/regression/verification/xlang/invalid/Array1.scala b/src/test/resources/regression/verification/xlang/invalid/Array1.scala
index a8451250c8f9e9c95684b4ea10490aced2a23f6e..40ba7871a9da2d3d38e33573061b135d72cb3554 100644
--- a/src/test/resources/regression/verification/xlang/invalid/Array1.scala
+++ b/src/test/resources/regression/verification/xlang/invalid/Array1.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
object Array1 {
def foo(): Int = {
diff --git a/src/test/resources/regression/verification/xlang/invalid/Array2.scala b/src/test/resources/regression/verification/xlang/invalid/Array2.scala
index 54ab5e3c27918596af58c427fabedd2016a33db9..5390b44777cc36f7cc778495d19b20bb9e2ed68a 100644
--- a/src/test/resources/regression/verification/xlang/invalid/Array2.scala
+++ b/src/test/resources/regression/verification/xlang/invalid/Array2.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
object Array2 {
def foo(): Int = {
diff --git a/src/test/resources/regression/verification/xlang/invalid/Array3.scala b/src/test/resources/regression/verification/xlang/invalid/Array3.scala
index 0c1bb76fdce099bd095c59d8c03fe8e6508a9776..deb28f736f33fdfb44e540aae7971aaa5b181566 100644
--- a/src/test/resources/regression/verification/xlang/invalid/Array3.scala
+++ b/src/test/resources/regression/verification/xlang/invalid/Array3.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
import leon.Utils._
object Array3 {
diff --git a/src/test/resources/regression/verification/xlang/invalid/Array4.scala b/src/test/resources/regression/verification/xlang/invalid/Array4.scala
index 5b5e7406165ad214a7d5d5fffd85d2d4fce226e0..740f38a96314fb9babbff944fe7a35f0210b50ea 100644
--- a/src/test/resources/regression/verification/xlang/invalid/Array4.scala
+++ b/src/test/resources/regression/verification/xlang/invalid/Array4.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
import leon.Utils._
object Array4 {
diff --git a/src/test/resources/regression/verification/xlang/invalid/Array5.scala b/src/test/resources/regression/verification/xlang/invalid/Array5.scala
index ecb00334971f3ecf19f3b6e6f9c25a5082f2d2d7..4cc49498f6b6510edc7ce23b8511eabad243774d 100644
--- a/src/test/resources/regression/verification/xlang/invalid/Array5.scala
+++ b/src/test/resources/regression/verification/xlang/invalid/Array5.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
import leon.Utils._
object Array4 {
diff --git a/src/test/resources/regression/verification/xlang/invalid/Epsilon1.scala b/src/test/resources/regression/verification/xlang/invalid/Epsilon1.scala
index c3c0a48be96f594fe725518a7289333bb587ef40..51d72f9614baeea05681632fe43e57a214d0f594 100644
--- a/src/test/resources/regression/verification/xlang/invalid/Epsilon1.scala
+++ b/src/test/resources/regression/verification/xlang/invalid/Epsilon1.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
import leon.Utils._
object Epsilon1 {
diff --git a/src/test/resources/regression/verification/xlang/invalid/Epsilon2.scala b/src/test/resources/regression/verification/xlang/invalid/Epsilon2.scala
index 20699fc427e7dce9025e578767f5364ae19aaf88..7ed458cefb9dbdc7f5909a9fe6e703c6556da9a4 100644
--- a/src/test/resources/regression/verification/xlang/invalid/Epsilon2.scala
+++ b/src/test/resources/regression/verification/xlang/invalid/Epsilon2.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
import leon.Utils._
object Epsilon1 {
diff --git a/src/test/resources/regression/verification/xlang/invalid/Epsilon3.scala b/src/test/resources/regression/verification/xlang/invalid/Epsilon3.scala
index 5ff47b6d638cc7270640f0bba95f4cd572f8201a..d76d9a7f75e91054491dfcb087c4d13424876ed3 100644
--- a/src/test/resources/regression/verification/xlang/invalid/Epsilon3.scala
+++ b/src/test/resources/regression/verification/xlang/invalid/Epsilon3.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
import leon.Utils._
object Epsilon3 {
diff --git a/src/test/resources/regression/verification/xlang/invalid/Epsilon4.scala b/src/test/resources/regression/verification/xlang/invalid/Epsilon4.scala
index 6619e59d6f9d9721c4bc7587b47dac79f48bf437..72cb25fc16f65bbe2aa7c2f485588e2a28b71f83 100644
--- a/src/test/resources/regression/verification/xlang/invalid/Epsilon4.scala
+++ b/src/test/resources/regression/verification/xlang/invalid/Epsilon4.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
import leon.Utils._
object Epsilon4 {
diff --git a/src/test/resources/regression/verification/xlang/invalid/Epsilon5.scala b/src/test/resources/regression/verification/xlang/invalid/Epsilon5.scala
index b96fa7564e5dba8a44aeb9d750034153b362ebfe..cd387c1694c5d1f830f2889a99b4245312955db7 100644
--- a/src/test/resources/regression/verification/xlang/invalid/Epsilon5.scala
+++ b/src/test/resources/regression/verification/xlang/invalid/Epsilon5.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
import leon.Utils._
object Epsilon5 {
diff --git a/src/test/resources/regression/verification/xlang/invalid/Epsilon6.scala b/src/test/resources/regression/verification/xlang/invalid/Epsilon6.scala
index bc5aca78c3818a94df43146aba16077ffab50a71..0973387862ef0234d9b1800fbe0613dc0ec78bc2 100644
--- a/src/test/resources/regression/verification/xlang/invalid/Epsilon6.scala
+++ b/src/test/resources/regression/verification/xlang/invalid/Epsilon6.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
import leon.Utils._
object Epsilon6 {
diff --git a/src/test/resources/regression/verification/xlang/invalid/IfExpr1.scala b/src/test/resources/regression/verification/xlang/invalid/IfExpr1.scala
index 25ae2a2103b1e2cfd8bf886442adeabf12bb6dc3..b06ea8f8c36b4a7f0f4cef5d0a4707f0a628a439 100644
--- a/src/test/resources/regression/verification/xlang/invalid/IfExpr1.scala
+++ b/src/test/resources/regression/verification/xlang/invalid/IfExpr1.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
object IfExpr1 {
def foo(): Int = {
diff --git a/src/test/resources/regression/verification/xlang/invalid/IfExpr2.scala b/src/test/resources/regression/verification/xlang/invalid/IfExpr2.scala
index 1284904b5c7dfda8f601e130b6346680538aa99a..3f0149ccf7e59431e6a4602b98e7a122850e16f6 100644
--- a/src/test/resources/regression/verification/xlang/invalid/IfExpr2.scala
+++ b/src/test/resources/regression/verification/xlang/invalid/IfExpr2.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
object IfExpr2 {
def foo(): Int = {
diff --git a/src/test/resources/regression/verification/xlang/valid/Arithmetic.scala b/src/test/resources/regression/verification/xlang/valid/Arithmetic.scala
index be6246813ee92172c46f735aecf0a747d6f4c9ec..31a759ad8e8223977dc445539f619ce1ab6aed14 100644
--- a/src/test/resources/regression/verification/xlang/valid/Arithmetic.scala
+++ b/src/test/resources/regression/verification/xlang/valid/Arithmetic.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
import leon.Utils._
object Arithmetic {
diff --git a/src/test/resources/regression/verification/xlang/valid/Array1.scala b/src/test/resources/regression/verification/xlang/valid/Array1.scala
index 3815f03443448a28fb60475b49c09c981a1377f9..76784cb896305f047de81c6208907eafc498b2e9 100644
--- a/src/test/resources/regression/verification/xlang/valid/Array1.scala
+++ b/src/test/resources/regression/verification/xlang/valid/Array1.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
object Array1 {
def foo(): Int = {
diff --git a/src/test/resources/regression/verification/xlang/valid/Array10.scala b/src/test/resources/regression/verification/xlang/valid/Array10.scala
index ebb60ad6e0ba7556c55c74e1b1b624e6c34b4311..e073ebeff864c174f02091ef5d2befdfca73ddc0 100644
--- a/src/test/resources/regression/verification/xlang/valid/Array10.scala
+++ b/src/test/resources/regression/verification/xlang/valid/Array10.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
object Array10 {
def foo(a: Array[Int]): Int = {
diff --git a/src/test/resources/regression/verification/xlang/valid/Array2.scala b/src/test/resources/regression/verification/xlang/valid/Array2.scala
index 4f149a9305cb4b53a4a9353b82e25468c898bdc8..296c5fcc33f01cc25dd8e706089ff09539de2981 100644
--- a/src/test/resources/regression/verification/xlang/valid/Array2.scala
+++ b/src/test/resources/regression/verification/xlang/valid/Array2.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
object Array2 {
def foo(): Int = {
diff --git a/src/test/resources/regression/verification/xlang/valid/Array3.scala b/src/test/resources/regression/verification/xlang/valid/Array3.scala
index bbb1845b80c0ca747cb0c830828bacdc9668943f..cf41ef4f242da814b5df19b3c11828e566c1f7c1 100644
--- a/src/test/resources/regression/verification/xlang/valid/Array3.scala
+++ b/src/test/resources/regression/verification/xlang/valid/Array3.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
import leon.Utils._
object Array3 {
diff --git a/src/test/resources/regression/verification/xlang/valid/Array4.scala b/src/test/resources/regression/verification/xlang/valid/Array4.scala
index fd76e02faa83f8fd1bda5fef7c91e7df7fc29864..9337f21f18847798eca59efe1a90e60b261d88dd 100644
--- a/src/test/resources/regression/verification/xlang/valid/Array4.scala
+++ b/src/test/resources/regression/verification/xlang/valid/Array4.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
import leon.Utils._
object Array4 {
diff --git a/src/test/resources/regression/verification/xlang/valid/Array5.scala b/src/test/resources/regression/verification/xlang/valid/Array5.scala
index 14bed6eff332db69600353001488c46a3e56aa5d..a298a74292e293c692dd7b9b9ba8d018f78f8595 100644
--- a/src/test/resources/regression/verification/xlang/valid/Array5.scala
+++ b/src/test/resources/regression/verification/xlang/valid/Array5.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
import leon.Utils._
object Array5 {
diff --git a/src/test/resources/regression/verification/xlang/valid/Array6.scala b/src/test/resources/regression/verification/xlang/valid/Array6.scala
index bdd6b0c5d9bee06eec14b9f5917762c67af4751b..fb1dc5eee772cfacdd26a8ef4975df9e38f64b79 100644
--- a/src/test/resources/regression/verification/xlang/valid/Array6.scala
+++ b/src/test/resources/regression/verification/xlang/valid/Array6.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
import leon.Utils._
object Array6 {
diff --git a/src/test/resources/regression/verification/xlang/valid/Array7.scala b/src/test/resources/regression/verification/xlang/valid/Array7.scala
index 55bbbb72908e2b192152162d82d2ed9fea67923b..806fe5e327464d3295db2b5edcb96c2dd66f6431 100644
--- a/src/test/resources/regression/verification/xlang/valid/Array7.scala
+++ b/src/test/resources/regression/verification/xlang/valid/Array7.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
import leon.Utils._
object Array7 {
diff --git a/src/test/resources/regression/verification/xlang/valid/Array8.scala b/src/test/resources/regression/verification/xlang/valid/Array8.scala
index 270b181220b55af1588f63e7953221ae71f9bde3..cb65c7c1adbe6907f09c606b5851a399e64411bd 100644
--- a/src/test/resources/regression/verification/xlang/valid/Array8.scala
+++ b/src/test/resources/regression/verification/xlang/valid/Array8.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
object Array8 {
def foo(a: Array[Int]): Array[Int] = {
diff --git a/src/test/resources/regression/verification/xlang/valid/Array9.scala b/src/test/resources/regression/verification/xlang/valid/Array9.scala
index f49333236abfaf63caa278405a89670b1c9c115d..662e15bdab334333ab4c947046f0231dd96b9dcc 100644
--- a/src/test/resources/regression/verification/xlang/valid/Array9.scala
+++ b/src/test/resources/regression/verification/xlang/valid/Array9.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
object Array9 {
def foo(i: Int): Array[Int] = {
diff --git a/src/test/resources/regression/verification/xlang/valid/Assign1.scala b/src/test/resources/regression/verification/xlang/valid/Assign1.scala
index 0506c6afb39b49ac5a15c77dc10ab60f54de9ee6..343a41065496812344fa5271c85a20ab7563c7a7 100644
--- a/src/test/resources/regression/verification/xlang/valid/Assign1.scala
+++ b/src/test/resources/regression/verification/xlang/valid/Assign1.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
object Assign1 {
def foo(): Int = {
diff --git a/src/test/resources/regression/verification/xlang/valid/Choose1.scala b/src/test/resources/regression/verification/xlang/valid/Choose1.scala
index 702024e96bb89a6d1fa793e2b9b05663eba7fff7..1461f0d0cd898722d01d9caf484088f3bccc9329 100644
--- a/src/test/resources/regression/verification/xlang/valid/Choose1.scala
+++ b/src/test/resources/regression/verification/xlang/valid/Choose1.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
import leon.Utils._
object Test {
diff --git a/src/test/resources/regression/verification/xlang/valid/Epsilon1.scala b/src/test/resources/regression/verification/xlang/valid/Epsilon1.scala
index 2ae7201dd933e345fa71a6218b48599a61110f44..1d8402600d5d6d98cbe8503178f371697cd00f9c 100644
--- a/src/test/resources/regression/verification/xlang/valid/Epsilon1.scala
+++ b/src/test/resources/regression/verification/xlang/valid/Epsilon1.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
import leon.Utils._
object Epsilon1 {
diff --git a/src/test/resources/regression/verification/xlang/valid/Epsilon2.scala b/src/test/resources/regression/verification/xlang/valid/Epsilon2.scala
index 36e5268e2b1ccdbc710dc8d6410ce6968231c7d1..77315ca2f0ea326082a5b01feefb3cebce824f67 100644
--- a/src/test/resources/regression/verification/xlang/valid/Epsilon2.scala
+++ b/src/test/resources/regression/verification/xlang/valid/Epsilon2.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
import leon.Utils._
object Epsilon1 {
diff --git a/src/test/resources/regression/verification/xlang/valid/Epsilon3.scala b/src/test/resources/regression/verification/xlang/valid/Epsilon3.scala
index f652016d28976d0b7e110b009a0802a7aac10c99..9d114be164bc1a3c519d212eb856b22852deaf94 100644
--- a/src/test/resources/regression/verification/xlang/valid/Epsilon3.scala
+++ b/src/test/resources/regression/verification/xlang/valid/Epsilon3.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
import leon.Utils._
object Epsilon3 {
diff --git a/src/test/resources/regression/verification/xlang/valid/Epsilon4.scala b/src/test/resources/regression/verification/xlang/valid/Epsilon4.scala
index 174042863a690067fae5a2fd4aaf55f95bf29129..14fabbeb2c81c6f9ff816649a2876944ea20fc91 100644
--- a/src/test/resources/regression/verification/xlang/valid/Epsilon4.scala
+++ b/src/test/resources/regression/verification/xlang/valid/Epsilon4.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
import leon.Utils._
object Epsilon4 {
diff --git a/src/test/resources/regression/verification/xlang/valid/Epsilon5.scala b/src/test/resources/regression/verification/xlang/valid/Epsilon5.scala
index 0427cf086ba1050226ae8a3e28d6177a9904b460..a020beee84a436537c592bb0c88818444bea380a 100644
--- a/src/test/resources/regression/verification/xlang/valid/Epsilon5.scala
+++ b/src/test/resources/regression/verification/xlang/valid/Epsilon5.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
import leon.Utils._
object Epsilon5 {
diff --git a/src/test/resources/regression/verification/xlang/valid/IfExpr1.scala b/src/test/resources/regression/verification/xlang/valid/IfExpr1.scala
index 82db13d5285bc3c779010fd3e62b6e9e68e84e84..bb8989ca015f8e484a6098040cab3e078760c7e8 100644
--- a/src/test/resources/regression/verification/xlang/valid/IfExpr1.scala
+++ b/src/test/resources/regression/verification/xlang/valid/IfExpr1.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
object IfExpr1 {
def foo(): Int = {
diff --git a/src/test/resources/regression/verification/xlang/valid/IfExpr2.scala b/src/test/resources/regression/verification/xlang/valid/IfExpr2.scala
index 7a681bc7276d07e41884147342dc0874d0bbf93d..d581b13d0cbddde49932c9d52756a310508c3af3 100644
--- a/src/test/resources/regression/verification/xlang/valid/IfExpr2.scala
+++ b/src/test/resources/regression/verification/xlang/valid/IfExpr2.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
object IfExpr2 {
def foo(): Int = {
diff --git a/src/test/resources/regression/verification/xlang/valid/IfExpr3.scala b/src/test/resources/regression/verification/xlang/valid/IfExpr3.scala
index 86d4e494a7ce8fd22024020bb9580b393af8377a..12c91f38863bacdb7d01ed4bfa2d2413d3dda974 100644
--- a/src/test/resources/regression/verification/xlang/valid/IfExpr3.scala
+++ b/src/test/resources/regression/verification/xlang/valid/IfExpr3.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
object IfExpr1 {
def foo(a: Int): Int = {
diff --git a/src/test/resources/regression/verification/xlang/valid/IfExpr4.scala b/src/test/resources/regression/verification/xlang/valid/IfExpr4.scala
index 94b99fde39e6f7e10b1c898548d60592023ffbd6..494b2c4b1fd3ce721a755c25c97e994b246cbb1a 100644
--- a/src/test/resources/regression/verification/xlang/valid/IfExpr4.scala
+++ b/src/test/resources/regression/verification/xlang/valid/IfExpr4.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
object IfExpr4 {
def foo(a: Int): Int = {
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested1.scala b/src/test/resources/regression/verification/xlang/valid/Nested1.scala
index 7745f794f369cf59b529133fa6c73383466acec8..5041b81eb407e7501469e3cd61159a2033d48bde 100644
--- a/src/test/resources/regression/verification/xlang/valid/Nested1.scala
+++ b/src/test/resources/regression/verification/xlang/valid/Nested1.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
object Nested1 {
def foo(i: Int): Int = {
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested10.scala b/src/test/resources/regression/verification/xlang/valid/Nested10.scala
index b3c4f865367ca84a52091e89b655ac6438dc65a2..218010b683cd20bcabe4e14beea231f617c2e253 100644
--- a/src/test/resources/regression/verification/xlang/valid/Nested10.scala
+++ b/src/test/resources/regression/verification/xlang/valid/Nested10.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
object Nested10 {
def foo(i: Int): Int = {
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested11.scala b/src/test/resources/regression/verification/xlang/valid/Nested11.scala
index 0316fc5f2ba3497691bc48b1d573933ba2cea027..daf1c4f762cc77b3d29ee9e2559656f3cefda9a8 100644
--- a/src/test/resources/regression/verification/xlang/valid/Nested11.scala
+++ b/src/test/resources/regression/verification/xlang/valid/Nested11.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
object Nested11 {
abstract class A
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested12.scala b/src/test/resources/regression/verification/xlang/valid/Nested12.scala
index 05ac1569f630f1fc905a84f0550cbbaa42047906..d64f7a320f6403515310a8edca1db7ebcb7cb886 100644
--- a/src/test/resources/regression/verification/xlang/valid/Nested12.scala
+++ b/src/test/resources/regression/verification/xlang/valid/Nested12.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
object Nested12 {
abstract class A
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested13.scala b/src/test/resources/regression/verification/xlang/valid/Nested13.scala
index ccb742494564433dffe096210fac07b37a663dfe..4a0a21bc4ea25f737389a38a84a092147a821ee2 100644
--- a/src/test/resources/regression/verification/xlang/valid/Nested13.scala
+++ b/src/test/resources/regression/verification/xlang/valid/Nested13.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
object Nested13 {
abstract class D
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested14.scala b/src/test/resources/regression/verification/xlang/valid/Nested14.scala
index 9a79a4f6e4e7c28aa860d0636487a60a06e9e2ba..347c4958eafd965cb0fedd7232f241a9a2de7b4d 100644
--- a/src/test/resources/regression/verification/xlang/valid/Nested14.scala
+++ b/src/test/resources/regression/verification/xlang/valid/Nested14.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
object Nested14 {
def foo(i: Int): Int = {
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested2.scala b/src/test/resources/regression/verification/xlang/valid/Nested2.scala
index cc7220b02109c394e71c127e4cd3f53d6714ed7f..caff37f2f9b02e6d58655cd57fa89a4840823bce 100644
--- a/src/test/resources/regression/verification/xlang/valid/Nested2.scala
+++ b/src/test/resources/regression/verification/xlang/valid/Nested2.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
object Nested2 {
def foo(a: Int): Int = {
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested3.scala b/src/test/resources/regression/verification/xlang/valid/Nested3.scala
index be6e6d04a335d12d079a9e3dc1a4b14ec0164014..f4c5f052afe21301e5acb84e6e32ac9fcff7b379 100644
--- a/src/test/resources/regression/verification/xlang/valid/Nested3.scala
+++ b/src/test/resources/regression/verification/xlang/valid/Nested3.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
object Nested3 {
def foo(a: Int): Int = {
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested4.scala b/src/test/resources/regression/verification/xlang/valid/Nested4.scala
index ea1e6066c6f4b7aaf6df23065e3011b86471b7f4..5c0745acaf25efc237b37c63b2de9459cf373076 100644
--- a/src/test/resources/regression/verification/xlang/valid/Nested4.scala
+++ b/src/test/resources/regression/verification/xlang/valid/Nested4.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
object Nested4 {
def foo(a: Int, a2: Int): Int = {
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested5.scala b/src/test/resources/regression/verification/xlang/valid/Nested5.scala
index 6ba128f415ecc3c61ebcccb42b65100d15373982..1442e47d24718f01ed08641f70d9f7f17fdeaef2 100644
--- a/src/test/resources/regression/verification/xlang/valid/Nested5.scala
+++ b/src/test/resources/regression/verification/xlang/valid/Nested5.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
object Nested5 {
def foo(a: Int): Int = {
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested6.scala b/src/test/resources/regression/verification/xlang/valid/Nested6.scala
index 1c0220c0447dba10ccd710d60e5f19b1c1ec6e18..5a481fcb5fb9bde8373e3724888b082e66d1b712 100644
--- a/src/test/resources/regression/verification/xlang/valid/Nested6.scala
+++ b/src/test/resources/regression/verification/xlang/valid/Nested6.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
object Nested5 {
def foo(a: Int): Int = {
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested7.scala b/src/test/resources/regression/verification/xlang/valid/Nested7.scala
index 62f5a567f49be174873a24711e630f69e8469a22..81794c7d8724a3281e7a8d2f68dd855e05d48c92 100644
--- a/src/test/resources/regression/verification/xlang/valid/Nested7.scala
+++ b/src/test/resources/regression/verification/xlang/valid/Nested7.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
object Nested2 {
def foo(a: Int): Int = {
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested8.scala b/src/test/resources/regression/verification/xlang/valid/Nested8.scala
index e8a05e40e6cd1b2428e03bcf1a9f96c67797c698..6933d1cc2e4df69261205f5a8cabe9603126d6af 100644
--- a/src/test/resources/regression/verification/xlang/valid/Nested8.scala
+++ b/src/test/resources/regression/verification/xlang/valid/Nested8.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
import leon.Utils._
object Nested8 {
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested9.scala b/src/test/resources/regression/verification/xlang/valid/Nested9.scala
index 3344a2c7973bed9da2c42208742c34c184b458ac..2723d4c794e47a513bacba2a84c549cfc7bbf210 100644
--- a/src/test/resources/regression/verification/xlang/valid/Nested9.scala
+++ b/src/test/resources/regression/verification/xlang/valid/Nested9.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
object Nested4 {
def foo(a: Int, a2: Int): Int = {
diff --git a/src/test/resources/regression/verification/xlang/valid/NestedVar.scala b/src/test/resources/regression/verification/xlang/valid/NestedVar.scala
index a26b7312b2f5f85509c6e55cc706fb29845202b1..31716917258aa219ad4e4fc478546aef6240ec0a 100644
--- a/src/test/resources/regression/verification/xlang/valid/NestedVar.scala
+++ b/src/test/resources/regression/verification/xlang/valid/NestedVar.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
object NestedVar {
def foo(): Int = {
diff --git a/src/test/resources/regression/verification/xlang/valid/While1.scala b/src/test/resources/regression/verification/xlang/valid/While1.scala
index 0d868b399330c91342bd4ed26f7166f6b40dae5f..c36499dfc4e76fb060432246998bef354b9bf97e 100644
--- a/src/test/resources/regression/verification/xlang/valid/While1.scala
+++ b/src/test/resources/regression/verification/xlang/valid/While1.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
object While1 {
def foo(): Int = {
diff --git a/src/test/resources/regression/verification/xlang/valid/While2.scala b/src/test/resources/regression/verification/xlang/valid/While2.scala
index e841ed40ebf045e5545b584b5c16e80bfc11396a..9e2b245f2de4c8e1cefd0f0d68c1bb6c2af144a3 100644
--- a/src/test/resources/regression/verification/xlang/valid/While2.scala
+++ b/src/test/resources/regression/verification/xlang/valid/While2.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
object While1 {
def foo(): Int = {
diff --git a/src/test/resources/regression/verification/xlang/valid/While3.scala b/src/test/resources/regression/verification/xlang/valid/While3.scala
index da85d5dfab90410eb4d2ee23cea90627d1d40c93..0ea9a5f640208fa98de3dba36c3b1494427c8686 100644
--- a/src/test/resources/regression/verification/xlang/valid/While3.scala
+++ b/src/test/resources/regression/verification/xlang/valid/While3.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
object While3 {
def foo(): Int = {
diff --git a/src/test/scala/leon/test/TestUtils.scala b/src/test/scala/leon/test/TestUtils.scala
index 0177d25dc362236a913cc261d3366f9e6750962e..2f8b789ae1a3ff6ce04d4101f0acbd532c0694d2 100644
--- a/src/test/scala/leon/test/TestUtils.scala
+++ b/src/test/scala/leon/test/TestUtils.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package test
diff --git a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
index ce625a75e379b7ce0bdbd715be48ab80bdb5e3cc..27ba891159ebf47e3b0aacbdeddcd354fc9facc9 100644
--- a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
+++ b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon.test
package evaluators
diff --git a/src/test/scala/leon/test/purescala/DataGen.scala b/src/test/scala/leon/test/purescala/DataGen.scala
index 661b57674378e86f856eb24f0deeb2c08b4936bf..a3c9d5a40f1816cc403c32589f38de9810c1faaa 100644
--- a/src/test/scala/leon/test/purescala/DataGen.scala
+++ b/src/test/scala/leon/test/purescala/DataGen.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon.test
package purescala
diff --git a/src/test/scala/leon/test/purescala/LikelyEq.scala b/src/test/scala/leon/test/purescala/LikelyEq.scala
index 84744ee62252c16c352a8c8fe109b0794f338f5c..77bac755534bcef5b7e7418d3178b0b80707174a 100644
--- a/src/test/scala/leon/test/purescala/LikelyEq.scala
+++ b/src/test/scala/leon/test/purescala/LikelyEq.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon.test.purescala
import leon._
diff --git a/src/test/scala/leon/test/purescala/LikelyEqSuite.scala b/src/test/scala/leon/test/purescala/LikelyEqSuite.scala
index 4ba6a5845a67e0fbb602b47970f2feb95d80c405..3a4fa9371f6dcf36663ea00798aaac7d76900819 100644
--- a/src/test/scala/leon/test/purescala/LikelyEqSuite.scala
+++ b/src/test/scala/leon/test/purescala/LikelyEqSuite.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon.test.purescala
import org.scalatest.FunSuite
diff --git a/src/test/scala/leon/test/purescala/TreeNormalizationsTests.scala b/src/test/scala/leon/test/purescala/TreeNormalizationsTests.scala
index db3ff42cde22c1a68dc6cd734bcb4e087bf045ff..9199b38e7460c9a9f5b6f80d030b7c0b7f72fdca 100644
--- a/src/test/scala/leon/test/purescala/TreeNormalizationsTests.scala
+++ b/src/test/scala/leon/test/purescala/TreeNormalizationsTests.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon.test.purescala
import leon.purescala.Common._
diff --git a/src/test/scala/leon/test/purescala/TreeOpsTests.scala b/src/test/scala/leon/test/purescala/TreeOpsTests.scala
index a26d3bd0c4901329975616af533912afe01b17cd..44c9f6a37d03914191d76621e2c70589d10afa45 100644
--- a/src/test/scala/leon/test/purescala/TreeOpsTests.scala
+++ b/src/test/scala/leon/test/purescala/TreeOpsTests.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon.test.purescala
import leon.LeonContext
diff --git a/src/test/scala/leon/test/purescala/TreeTests.scala b/src/test/scala/leon/test/purescala/TreeTests.scala
index 3ca418ec5aac9603d1982ebbf8550d930dc23cea..45c341d494d6009c942258f78a553f2a70b2e06b 100644
--- a/src/test/scala/leon/test/purescala/TreeTests.scala
+++ b/src/test/scala/leon/test/purescala/TreeTests.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon.test.purescala
import leon.purescala.Common._
diff --git a/src/test/scala/leon/test/solvers/TimeoutSolverTests.scala b/src/test/scala/leon/test/solvers/TimeoutSolverTests.scala
index 38713552c547ab24315198d774c99b0d2e89e56d..46278779009648037fee20f461c87dade92de699 100644
--- a/src/test/scala/leon/test/solvers/TimeoutSolverTests.scala
+++ b/src/test/scala/leon/test/solvers/TimeoutSolverTests.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon.test.solvers
import org.scalatest.FunSuite
diff --git a/src/test/scala/leon/test/solvers/z3/FairZ3SolverTests.scala b/src/test/scala/leon/test/solvers/z3/FairZ3SolverTests.scala
index 8fd0458ae436246582436e016775c93039194f45..6cd6480cbe4a99dcc2640205c9197508c8988f1a 100644
--- a/src/test/scala/leon/test/solvers/z3/FairZ3SolverTests.scala
+++ b/src/test/scala/leon/test/solvers/z3/FairZ3SolverTests.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon.test.solvers.z3
import leon.LeonContext
diff --git a/src/test/scala/leon/test/solvers/z3/FairZ3SolverTestsNewAPI.scala b/src/test/scala/leon/test/solvers/z3/FairZ3SolverTestsNewAPI.scala
index 92dc5720289fa14f6ea63b8ab99588ca22fe7cf4..9bc961371137f1d85ea136f5d2c8891732bfff33 100644
--- a/src/test/scala/leon/test/solvers/z3/FairZ3SolverTestsNewAPI.scala
+++ b/src/test/scala/leon/test/solvers/z3/FairZ3SolverTestsNewAPI.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon.test.solvers.z3
import leon.LeonContext
diff --git a/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala b/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala
index 2a68caa854c00ad471811ee54e544617512f9d45..db492d3d3b350abd259464f1ff8317c6416bf236 100644
--- a/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala
+++ b/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon.test.solvers.z3
import leon.LeonContext
diff --git a/src/test/scala/leon/test/synthesis/AlgebraSuite.scala b/src/test/scala/leon/test/synthesis/AlgebraSuite.scala
index 240b613dc9082efe7de72f8b3fdaf4db2f62a43c..88fce145020da5d0fa2e4c39404f44b595b0cd82 100644
--- a/src/test/scala/leon/test/synthesis/AlgebraSuite.scala
+++ b/src/test/scala/leon/test/synthesis/AlgebraSuite.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon.test.synthesis
import org.scalatest.FunSuite
diff --git a/src/test/scala/leon/test/synthesis/LinearEquationsSuite.scala b/src/test/scala/leon/test/synthesis/LinearEquationsSuite.scala
index 95d8706beed1c963776c102ab1a6e3349cae1fb2..bd83fba3f93b28a5cdd6309692eea330b650da72 100644
--- a/src/test/scala/leon/test/synthesis/LinearEquationsSuite.scala
+++ b/src/test/scala/leon/test/synthesis/LinearEquationsSuite.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon.test.synthesis
import org.scalatest.FunSuite
diff --git a/src/test/scala/leon/test/synthesis/SynthesisSuite.scala b/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
index 85db7aa04af9d4bc24b434a861eade16141a6d0d..123310ac863cb4c42f874cc336ac7ea96425c68f 100644
--- a/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
+++ b/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon.test.synthesis
import leon._
diff --git a/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala b/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
index 8360c44c5126285884671807e4944c96987d0055..4d73eb949f6738ac5e62d6c31c2b05dc1c41e369 100644
--- a/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
+++ b/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package test
package verification
diff --git a/src/test/scala/leon/test/verification/XLangVerificationRegression.scala b/src/test/scala/leon/test/verification/XLangVerificationRegression.scala
index 187f33fc8e8a54fdd7d3fdf20f693ff8ea17f1b7..bd169c167f3a6cba62d7227a31f21f1b97ac71e4 100644
--- a/src/test/scala/leon/test/verification/XLangVerificationRegression.scala
+++ b/src/test/scala/leon/test/verification/XLangVerificationRegression.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
package leon
package test
package verification