From 3cb6d843d1f984ee2cc4b6420f53d61076bb9c06 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Mon, 3 Jun 2013 17:14:06 +0200
Subject: [PATCH] Apply BSD 2 clauses license
---
LICENSE | 31 +++++++++++++++++++
library/src/main/scala/leon/Annotations.scala | 2 ++
library/src/main/scala/leon/Utils.scala | 2 ++
.../java/leon/codegen/runtime/CaseClass.java | 2 ++
.../LeonCodeGenEvaluationException.java | 2 ++
.../runtime/LeonCodeGenRuntimeException.java | 2 ++
src/main/java/leon/codegen/runtime/Map.java | 2 ++
src/main/java/leon/codegen/runtime/Set.java | 2 ++
src/main/java/leon/codegen/runtime/Tuple.java | 2 ++
src/main/scala/leon/LeonComponent.scala | 2 ++
src/main/scala/leon/LeonContext.scala | 2 ++
src/main/scala/leon/LeonFatalError.scala | 2 ++
src/main/scala/leon/LeonOption.scala | 2 ++
src/main/scala/leon/LeonPhase.scala | 2 ++
src/main/scala/leon/Main.scala | 2 ++
src/main/scala/leon/Pipeline.scala | 2 ++
src/main/scala/leon/Reporter.scala | 2 ++
src/main/scala/leon/Settings.scala | 2 ++
src/main/scala/leon/Stopwatch.scala | 2 ++
src/main/scala/leon/SubtypingPhase.scala | 2 ++
src/main/scala/leon/TypeChecking.scala | 2 ++
src/main/scala/leon/UnitElimination.scala | 2 ++
.../scala/leon/codegen/CodeGenPhase.scala | 2 ++
.../scala/leon/codegen/CodeGeneration.scala | 2 ++
.../leon/codegen/CompilationEnvironment.scala | 2 ++
.../leon/codegen/CompilationException.scala | 2 ++
.../leon/codegen/CompilationResult.scala | 2 ++
.../scala/leon/codegen/CompilationUnit.scala | 2 ++
.../leon/codegen/CompiledExpression.scala | 2 ++
.../leon/evaluators/CodeGenEvaluator.scala | 2 ++
.../leon/evaluators/DefaultEvaluator.scala | 2 ++
.../leon/evaluators/EvaluationResults.scala | 2 ++
.../scala/leon/evaluators/Evaluator.scala | 2 ++
.../scala/leon/plugin/AnalysisComponent.scala | 2 ++
.../scala/leon/plugin/CodeExtraction.scala | 2 ++
.../scala/leon/plugin/ExtractionPhase.scala | 2 ++
src/main/scala/leon/plugin/Extractors.scala | 2 ++
src/main/scala/leon/plugin/LeonPlugin.scala | 2 ++
.../scala/leon/plugin/SimpleReporter.scala | 2 ++
.../leon/plugin/TemporaryInputPhase.scala | 2 ++
src/main/scala/leon/purescala/Common.scala | 2 ++
src/main/scala/leon/purescala/DataGen.scala | 2 ++
.../scala/leon/purescala/Definitions.scala | 2 ++
.../scala/leon/purescala/Extractors.scala | 2 ++
.../scala/leon/purescala/PrettyPrinter.scala | 2 ++
.../scala/leon/purescala/ScalaPrinter.scala | 2 ++
.../leon/purescala/TreeNormalizations.scala | 2 ++
src/main/scala/leon/purescala/TreeOps.scala | 2 ++
src/main/scala/leon/purescala/Trees.scala | 2 ++
src/main/scala/leon/purescala/TypeTrees.scala | 2 ++
.../leon/solvers/IncrementalSolver.scala | 2 ++
.../leon/solvers/InterruptibleSolver.scala | 2 ++
.../scala/leon/solvers/ParallelSolver.scala | 2 ++
.../scala/leon/solvers/RandomSolver.scala | 2 ++
src/main/scala/leon/solvers/Solver.scala | 2 ++
.../scala/leon/solvers/TimeoutSolver.scala | 2 ++
.../scala/leon/solvers/TrivialSolver.scala | 2 ++
.../leon/solvers/z3/AbstractZ3Solver.scala | 2 ++
.../scala/leon/solvers/z3/FairZ3Solver.scala | 2 ++
.../leon/solvers/z3/FunctionTemplate.scala | 2 ++
.../solvers/z3/UninterpretedZ3Solver.scala | 2 ++
.../solvers/z3/Z3ModelReconstruction.scala | 2 ++
src/main/scala/leon/synthesis/Algebra.scala | 2 ++
.../scala/leon/synthesis/ChooseInfo.scala | 2 ++
src/main/scala/leon/synthesis/CostModel.scala | 2 ++
.../scala/leon/synthesis/FileInterface.scala | 2 ++
.../scala/leon/synthesis/Heuristics.scala | 2 ++
.../leon/synthesis/LinearEquations.scala | 2 ++
src/main/scala/leon/synthesis/Main.scala | 2 ++
.../scala/leon/synthesis/ManualSearch.scala | 2 ++
.../scala/leon/synthesis/ParallelSearch.scala | 2 ++
src/main/scala/leon/synthesis/Problem.scala | 2 ++
src/main/scala/leon/synthesis/Rules.scala | 2 ++
.../scala/leon/synthesis/SimpleSearch.scala | 2 ++
src/main/scala/leon/synthesis/Solution.scala | 2 ++
.../leon/synthesis/SynthesisContext.scala | 2 ++
.../leon/synthesis/SynthesisOptions.scala | 2 ++
.../scala/leon/synthesis/SynthesisPhase.scala | 2 ++
.../scala/leon/synthesis/Synthesizer.scala | 2 ++
src/main/scala/leon/synthesis/Task.scala | 2 ++
.../synthesis/heuristics/ADTInduction.scala | 2 ++
.../heuristics/ADTLongInduction.scala | 2 ++
.../synthesis/heuristics/InnerCaseSplit.scala | 2 ++
.../synthesis/heuristics/IntInduction.scala | 2 ++
.../heuristics/OptimisticInjection.scala | 2 ++
.../heuristics/SelectiveInlining.scala | 2 ++
src/main/scala/leon/synthesis/package.scala | 2 ++
.../scala/leon/synthesis/rules/ADTDual.scala | 2 ++
.../scala/leon/synthesis/rules/ADTSplit.scala | 2 ++
.../scala/leon/synthesis/rules/Assert.scala | 2 ++
.../leon/synthesis/rules/CaseSplit.scala | 2 ++
.../scala/leon/synthesis/rules/Cegis.scala | 2 ++
.../leon/synthesis/rules/DetupleInput.scala | 2 ++
.../leon/synthesis/rules/DetupleOutput.scala | 2 ++
.../leon/synthesis/rules/Disunification.scala | 2 ++
.../leon/synthesis/rules/EqualitySplit.scala | 2 ++
.../scala/leon/synthesis/rules/Ground.scala | 2 ++
.../synthesis/rules/InequalitySplit.scala | 2 ++
.../synthesis/rules/IntegerEquation.scala | 2 ++
.../synthesis/rules/IntegerInequalities.scala | 2 ++
.../scala/leon/synthesis/rules/OnePoint.scala | 2 ++
.../synthesis/rules/OptimisticGround.scala | 2 ++
.../synthesis/rules/UnconstrainedOutput.scala | 2 ++
.../leon/synthesis/rules/Unification.scala | 2 ++
.../leon/synthesis/rules/UnusedInput.scala | 2 ++
.../leon/synthesis/search/AndOrGraph.scala | 2 ++
.../search/AndOrGraphDotConverter.scala | 2 ++
.../search/AndOrGraphParallelSearch.scala | 2 ++
.../search/AndOrGraphPartialSolution.scala | 2 ++
.../synthesis/search/AndOrGraphSearch.scala | 2 ++
.../scala/leon/synthesis/search/Cost.scala | 2 ++
.../leon/synthesis/utils/Benchmarks.scala | 2 ++
.../SynthesisProblemExtractionPhase.scala | 2 ++
src/main/scala/leon/termination/SCC.scala | 2 ++
.../SimpleTerminationChecker.scala | 2 ++
.../leon/termination/TerminationChecker.scala | 2 ++
.../leon/termination/TerminationPhase.scala | 2 ++
.../leon/termination/TerminationReport.scala | 2 ++
src/main/scala/leon/testgen/CallGraph.scala | 2 ++
.../scala/leon/testgen/TestGeneration.scala | 2 ++
.../leon/verification/AnalysisPhase.scala | 2 ++
.../leon/verification/DefaultTactic.scala | 2 ++
.../leon/verification/InductionTactic.scala | 2 ++
src/main/scala/leon/verification/Tactic.scala | 2 ++
.../verification/VerificationCondition.scala | 2 ++
.../verification/VerificationContext.scala | 2 ++
.../verification/VerificationReport.scala | 2 ++
.../leon/xlang/ArrayTransformation.scala | 2 ++
.../scala/leon/xlang/EpsilonElimination.scala | 2 ++
.../scala/leon/xlang/FunctionClosure.scala | 2 ++
.../xlang/ImperativeCodeElimination.scala | 2 ++
src/main/scala/leon/xlang/TreeOps.scala | 2 ++
src/main/scala/leon/xlang/Trees.scala | 2 ++
.../scala/leon/xlang/XlangAnalysisPhase.scala | 2 ++
src/main/scala/leon/z3plugins/bapa/AST.scala | 2 ++
.../leon/z3plugins/bapa/BAPATheory.scala | 2 ++
.../z3plugins/bapa/BAPATheoryBubbles.scala | 2 ++
.../leon/z3plugins/bapa/BAPATheoryEqc.scala | 2 ++
.../scala/leon/z3plugins/bapa/Bubbles.scala | 2 ++
.../leon/z3plugins/bapa/NormalForms.scala | 2 ++
.../leon/z3plugins/bapa/PrettyPrinter.scala | 2 ++
.../leon/z3plugins/bapa/VennRegions.scala | 2 ++
.../purescala/error/InstanceOf1.scala | 2 ++
.../purescala/invalid/Choose1.scala | 2 ++
.../purescala/invalid/FiniteSort.scala | 2 ++
.../purescala/invalid/InsertionSort.scala | 2 ++
.../purescala/invalid/ListOperations.scala | 2 ++
.../purescala/invalid/MyTuple1.scala | 2 ++
.../purescala/invalid/MyTuple2.scala | 2 ++
.../purescala/invalid/MyTuple3.scala | 2 ++
.../invalid/PropositionalLogic.scala | 2 ++
.../purescala/invalid/RedBlackTree.scala | 2 ++
.../purescala/invalid/Unit1.scala | 2 ++
.../purescala/valid/AmortizedQueue.scala | 2 ++
.../purescala/valid/AssociativeList.scala | 2 ++
.../purescala/valid/BestRealTypes.scala | 2 ++
.../purescala/valid/CaseObject1.scala | 2 ++
.../purescala/valid/Choose1.scala | 2 ++
.../verification/purescala/valid/Field1.scala | 2 ++
.../verification/purescala/valid/Field2.scala | 2 ++
.../purescala/valid/FiniteSort.scala | 2 ++
.../purescala/valid/InsertionSort.scala | 2 ++
.../purescala/valid/InstanceOf1.scala | 2 ++
.../purescala/valid/ListOperations.scala | 2 ++
.../purescala/valid/LiteralMaps.scala | 2 ++
.../purescala/valid/MergeSort.scala | 2 ++
.../verification/purescala/valid/MyMap.scala | 2 ++
.../verification/purescala/valid/MySet.scala | 2 ++
.../purescala/valid/MyTuple1.scala | 2 ++
.../purescala/valid/MyTuple2.scala | 2 ++
.../purescala/valid/MyTuple3.scala | 2 ++
.../purescala/valid/MyTuple4.scala | 2 ++
.../purescala/valid/MyTuple5.scala | 2 ++
.../purescala/valid/MyTuple6.scala | 2 ++
.../purescala/valid/PropositionalLogic.scala | 2 ++
.../purescala/valid/RedBlackTree.scala | 2 ++
.../purescala/valid/SearchLinkedList.scala | 2 ++
.../purescala/valid/Subtyping1.scala | 2 ++
.../purescala/valid/Subtyping2.scala | 2 ++
.../purescala/valid/SumAndMax.scala | 2 ++
.../verification/purescala/valid/Unit1.scala | 2 ++
.../verification/purescala/valid/Unit2.scala | 2 ++
.../verification/xlang/error/Array1.scala | 2 ++
.../verification/xlang/error/Array10.scala | 2 ++
.../verification/xlang/error/Array2.scala | 2 ++
.../verification/xlang/error/Array3.scala | 2 ++
.../verification/xlang/error/Array4.scala | 2 ++
.../verification/xlang/error/Array5.scala | 2 ++
.../verification/xlang/error/Array6.scala | 2 ++
.../verification/xlang/error/Array7.scala | 2 ++
.../verification/xlang/error/Array8.scala | 2 ++
.../verification/xlang/error/Array9.scala | 2 ++
.../verification/xlang/invalid/Array1.scala | 2 ++
.../verification/xlang/invalid/Array2.scala | 2 ++
.../verification/xlang/invalid/Array3.scala | 2 ++
.../verification/xlang/invalid/Array4.scala | 2 ++
.../verification/xlang/invalid/Array5.scala | 2 ++
.../verification/xlang/invalid/Epsilon1.scala | 2 ++
.../verification/xlang/invalid/Epsilon2.scala | 2 ++
.../verification/xlang/invalid/Epsilon3.scala | 2 ++
.../verification/xlang/invalid/Epsilon4.scala | 2 ++
.../verification/xlang/invalid/Epsilon5.scala | 2 ++
.../verification/xlang/invalid/Epsilon6.scala | 2 ++
.../verification/xlang/invalid/IfExpr1.scala | 2 ++
.../verification/xlang/invalid/IfExpr2.scala | 2 ++
.../verification/xlang/valid/Arithmetic.scala | 2 ++
.../verification/xlang/valid/Array1.scala | 2 ++
.../verification/xlang/valid/Array10.scala | 2 ++
.../verification/xlang/valid/Array2.scala | 2 ++
.../verification/xlang/valid/Array3.scala | 2 ++
.../verification/xlang/valid/Array4.scala | 2 ++
.../verification/xlang/valid/Array5.scala | 2 ++
.../verification/xlang/valid/Array6.scala | 2 ++
.../verification/xlang/valid/Array7.scala | 2 ++
.../verification/xlang/valid/Array8.scala | 2 ++
.../verification/xlang/valid/Array9.scala | 2 ++
.../verification/xlang/valid/Assign1.scala | 2 ++
.../verification/xlang/valid/Choose1.scala | 2 ++
.../verification/xlang/valid/Epsilon1.scala | 2 ++
.../verification/xlang/valid/Epsilon2.scala | 2 ++
.../verification/xlang/valid/Epsilon3.scala | 2 ++
.../verification/xlang/valid/Epsilon4.scala | 2 ++
.../verification/xlang/valid/Epsilon5.scala | 2 ++
.../verification/xlang/valid/IfExpr1.scala | 2 ++
.../verification/xlang/valid/IfExpr2.scala | 2 ++
.../verification/xlang/valid/IfExpr3.scala | 2 ++
.../verification/xlang/valid/IfExpr4.scala | 2 ++
.../verification/xlang/valid/Nested1.scala | 2 ++
.../verification/xlang/valid/Nested10.scala | 2 ++
.../verification/xlang/valid/Nested11.scala | 2 ++
.../verification/xlang/valid/Nested12.scala | 2 ++
.../verification/xlang/valid/Nested13.scala | 2 ++
.../verification/xlang/valid/Nested14.scala | 2 ++
.../verification/xlang/valid/Nested2.scala | 2 ++
.../verification/xlang/valid/Nested3.scala | 2 ++
.../verification/xlang/valid/Nested4.scala | 2 ++
.../verification/xlang/valid/Nested5.scala | 2 ++
.../verification/xlang/valid/Nested6.scala | 2 ++
.../verification/xlang/valid/Nested7.scala | 2 ++
.../verification/xlang/valid/Nested8.scala | 2 ++
.../verification/xlang/valid/Nested9.scala | 2 ++
.../verification/xlang/valid/NestedVar.scala | 2 ++
.../verification/xlang/valid/While1.scala | 2 ++
.../verification/xlang/valid/While2.scala | 2 ++
.../verification/xlang/valid/While3.scala | 2 ++
src/test/scala/leon/test/TestUtils.scala | 2 ++
.../test/evaluators/EvaluatorsTests.scala | 2 ++
.../scala/leon/test/purescala/DataGen.scala | 2 ++
.../scala/leon/test/purescala/LikelyEq.scala | 2 ++
.../leon/test/purescala/LikelyEqSuite.scala | 2 ++
.../purescala/TreeNormalizationsTests.scala | 2 ++
.../leon/test/purescala/TreeOpsTests.scala | 2 ++
.../scala/leon/test/purescala/TreeTests.scala | 2 ++
.../test/solvers/TimeoutSolverTests.scala | 2 ++
.../test/solvers/z3/FairZ3SolverTests.scala | 2 ++
.../solvers/z3/FairZ3SolverTestsNewAPI.scala | 2 ++
.../z3/UninterpretedZ3SolverTests.scala | 2 ++
.../leon/test/synthesis/AlgebraSuite.scala | 2 ++
.../test/synthesis/LinearEquationsSuite.scala | 2 ++
.../leon/test/synthesis/SynthesisSuite.scala | 2 ++
.../PureScalaVerificationRegression.scala | 2 ++
.../XLangVerificationRegression.scala | 2 ++
262 files changed, 553 insertions(+)
create mode 100644 LICENSE
diff --git a/LICENSE b/LICENSE
new file mode 100644
index 000000000..2418ba1b5
--- /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 85e8c00e0..a44106640 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 366cc3975..ab3e84eb5 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 bbbdb92f8..8cda1d23a 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 f4ba02da8..d4d5c3588 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 8a3e6b86a..88af910a2 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 0bdb221c1..cd9c2eb6a 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 b38ba9070..f27167953 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 e010870ad..958a2340f 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 95f947b94..e69af9aa7 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 cdd1ecf4e..b271db3a4 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 6fc773292..8ceb4f3fd 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 9859fcc92..08ebbbb2c 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 1812b0239..4b00b7566 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 7549b1f55..9055d9bee 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 4cbf3dce3..80c834506 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 a9bff0440..83b9aec06 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 c267ba4d4..4271bf85d 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 b3e060ba5..9eab173d9 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 3c542e4a2..8a63663b4 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 41cda6b80..2733b8781 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 dc58a24be..3717cd585 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 c5e065575..4a6110d89 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 c436893e2..9e23300c0 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 760904eb1..52f4ec3e8 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 236cc586e..78948a451 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 dbb267c3c..50873242a 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 0d547d27a..1c5b5eac3 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 02cc93407..cf5369d89 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 b540a483c..87314546f 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 a1f66ae1c..d29f91c50 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 598121fd0..9a3d97123 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 a54e406e3..fd907bd0e 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 783d86b5c..49a62fcb4 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 06a6ac624..b03a8438f 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 c68f7f6b8..07f9f113f 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 c333df79f..e407a3508 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 0eebd19c9..badf32e8e 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 31cc4d7b1..549fb2589 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 89d26cf12..88717785c 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 16b8959f3..45142714e 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 0ace125ba..02e559d03 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 89c31d054..ae14f7b62 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 00ce83c66..704d6a7ae 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 11e98e534..964d4d905 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 9e2579f6c..d7ab7e3a4 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 fb34f35ed..7e450b3e9 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 ff38fc75d..818d125e4 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 b4c1762a6..21a23be82 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 22e1010ae..96265cf88 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 84215134e..700699e53 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 01620279c..e10e8ded9 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 e2a334df1..b812f3b7e 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 3ba1a3fa4..750270625 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 01a1e7336..5cc012e74 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 22a257031..207b3118d 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 3451aa759..c1ae27d26 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 1a94e295f..e024b5546 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 f736bf1fb..1a601470f 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 95a319a28..aacc63376 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 379d0bf03..f8d1bd492 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 2e65ca7e5..558274db5 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 c92b08980..17fab2cfb 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 888e923fb..aca20208f 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 7fd051d8e..128529c25 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 0fd787e73..aee3f4342 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 0170430b5..20bc9125a 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 e86ecf417..428c9ac69 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 a3704d349..69d6518d7 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 faea80ddc..4e075254f 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 dbdbe0517..57672fb4f 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 7810483af..57dc87a28 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 2357241c0..21d1e72e4 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 d042fc2e1..42546b01a 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 965b1f74a..53c25e93b 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 342e1766a..d12a05c5c 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 30f0de4f8..37408d3f7 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 230c250d0..1251de0ef 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 a94debc9e..6e4879944 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 e2d8d65fc..deefa844e 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 4d6342bae..2a7b60bd5 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 b6b470296..0437e52e3 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 8a76cd9f0..1f087f1cc 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 b94ceffd9..7799a01de 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 a4308de79..da7ccb3b9 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 b906d37e9..255095bfe 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 e2b051705..6e41da4a0 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 57c31c998..7f73a8198 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 2837c7abe..5203bd60f 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 efafc204d..240ed4685 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 f22f97be4..bd2a859e5 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 d2d5da250..5b6442206 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 736d89df1..5bb4045b0 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 3d475f336..6c026ad80 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 b496a4dd4..9c8ecada3 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 ae6d6da24..5d643659a 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 73b1a81a5..af1f48622 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 6c9e07d73..443040f7f 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 60101558d..06a2398fd 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 2c02d10ab..34902c9cb 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 1b44bbd06..d372a21d4 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 aeefe055e..e0935fefc 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 2572aebcc..4d5e0add3 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 005f13eed..bce329f13 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 a3b21fc28..56b869f50 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 50a7ab859..6fd4f3ca8 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 062ada1d7..6290f5c17 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 4ff625966..786d1970d 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 3f9fbdb68..beda712ac 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 00593edef..42643d7a7 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 0ec8ff140..5f7ce459f 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 04998922b..08226d925 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 c31a04a6a..a6abacc5d 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 c0c8f7588..54a13ec41 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 43d18726f..98303cd74 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 ed54acea4..442f59ab8 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 b59be3184..ca44e6433 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 4a4af2a6e..9004d3f10 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 2e87d8324..a81a56ee2 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 27426910b..7073f68f7 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 fe953a272..193ebcb75 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 cdc752a50..d866afdb4 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 ba7a210f1..26d9de252 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 3a00f2ab7..dc31d71e1 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 fee77a683..48b6a2e22 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 87300c40c..aede661c0 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 e40693199..34245e544 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 4a9017597..fb9309931 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 d36207822..7a9d3245f 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 c6fc16e1f..0feb5476c 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 aeda95f09..e68aa3638 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 5eb20b284..0e8c362aa 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 2773078e7..97313acf1 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 318e481cd..13c8d619f 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 2f2a328f3..6169a9f74 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 da9d93fe4..19355501b 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 16a792d8f..e59fcbe54 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 92fb7d267..412704648 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 f5a97d146..a60c99016 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 b1f931247..df3e7a55b 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 6b4c1ea31..9330832d8 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 4f5f3e616..3e8dde3ca 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 a1974b4bc..a9f9fa5d8 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 a0ac78daf..663c15d4e 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 4020135ac..f7b0ea17a 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 fd9d8d7b6..d8c2d029e 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 a4fc4f8dc..b3b8a2f90 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 f2b06b5b2..200bf2086 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 22b62dc75..b190043bf 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 da9f85b16..5a6d37dd3 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 a35c3ef9b..3018379cc 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 3baf9d015..f5478d734 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 789a8f058..ed3d6fcd3 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 dd5a75f89..81979fa4d 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 0356d8ec0..ad450a93c 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 e78cb0b0d..c68eb99b2 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 90dcdf064..4398b99c1 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 620b87811..ebcf96f17 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 116557ab7..f24e3896c 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 9a9661023..dd62e0a55 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 5a4e243b8..01f2caeed 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 a4fffee35..630518aa3 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 1c52338bb..14aaa5a16 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 27541d9bd..9f0b8da37 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 dab0d3741..70f1a32eb 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 c3592319f..32c0c2ddb 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 c71bfcf52..5d039ff94 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 3b6fdf42f..5be8bb6e7 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 48383898e..65a0ecfba 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 9fd21eb20..d9ffb9916 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 2e14c067b..981c83a5b 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 6fcfed661..9c68b867e 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 6a55bc8c9..21544dae2 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 a54710fbb..562fdcb97 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 5dd7d5057..60c1ef7a2 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 65d873ad4..3cbe4800d 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 2c137fd4a..64230dbd7 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 618d4c1c5..1bffd51ad 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 c6e792271..fc7f2e4ca 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 0aa4ce706..629dc6dba 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 a7b890d76..0f4d78ae9 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 ac659589a..08c96fc22 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 d0056f188..f8d420de5 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 9973626b8..ed596fec6 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 9154460c3..4de4eaf4d 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 a2c2fbd6d..b501eadbd 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 5ab0115af..bc9b5fd40 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 005d3d389..55eef8f26 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 15c87a085..818271c0c 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 abb83e1c0..079f2231b 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 89af32efd..098c001bb 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 5dc9d3aea..edbd5beb3 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 a8451250c..40ba7871a 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 54ab5e3c2..5390b4477 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 0c1bb76fd..deb28f736 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 5b5e74061..740f38a96 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 ecb003349..4cc49498f 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 c3c0a48be..51d72f961 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 20699fc42..7ed458cef 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 5ff47b6d6..d76d9a7f7 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 6619e59d6..72cb25fc1 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 b96fa7564..cd387c169 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 bc5aca78c..097338786 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 25ae2a210..b06ea8f8c 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 1284904b5..3f0149ccf 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 be6246813..31a759ad8 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 3815f0344..76784cb89 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 ebb60ad6e..e073ebeff 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 4f149a930..296c5fcc3 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 bbb1845b8..cf41ef4f2 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 fd76e02fa..9337f21f1 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 14bed6eff..a298a7429 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 bdd6b0c5d..fb1dc5eee 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 55bbbb729..806fe5e32 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 270b18122..cb65c7c1a 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 f49333236..662e15bda 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 0506c6afb..343a41065 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 702024e96..1461f0d0c 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 2ae7201dd..1d8402600 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 36e5268e2..77315ca2f 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 f652016d2..9d114be16 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 174042863..14fabbeb2 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 0427cf086..a020beee8 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 82db13d52..bb8989ca0 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 7a681bc72..d581b13d0 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 86d4e494a..12c91f388 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 94b99fde3..494b2c4b1 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 7745f794f..5041b81eb 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 b3c4f8653..218010b68 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 0316fc5f2..daf1c4f76 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 05ac1569f..d64f7a320 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 ccb742494..4a0a21bc4 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 9a79a4f6e..347c4958e 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 cc7220b02..caff37f2f 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 be6e6d04a..f4c5f052a 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 ea1e6066c..5c0745aca 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 6ba128f41..1442e47d2 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 1c0220c04..5a481fcb5 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 62f5a567f..81794c7d8 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 e8a05e40e..6933d1cc2 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 3344a2c79..2723d4c79 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 a26b7312b..317169172 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 0d868b399..c36499dfc 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 e841ed40e..9e2b245f2 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 da85d5dfa..0ea9a5f64 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 0177d25dc..2f8b789ae 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 ce625a75e..27ba89115 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 661b57674..a3c9d5a40 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 84744ee62..77bac7555 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 4ba6a5845..3a4fa9371 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 db3ff42cd..9199b38e7 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 a26d3bd0c..44c9f6a37 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 3ca418ec5..45c341d49 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 38713552c..462787790 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 8fd0458ae..6cd6480cb 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 92dc57202..9bc961371 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 2a68caa85..db492d3d3 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 240b613dc..88fce1450 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 95d8706be..bd83fba3f 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 85db7aa04..123310ac8 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 8360c44c5..4d73eb949 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 187f33fc8..bd169c167 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
--
GitLab