diff --git a/src/main/scala/leon/datagen/GrammarDataGen.scala b/src/main/scala/leon/datagen/GrammarDataGen.scala
index 614af333bbb79452ad49cc7491e70d7a2731cf09..7de37048797af75bde4891c1768b2b42174875f4 100644
--- a/src/main/scala/leon/datagen/GrammarDataGen.scala
+++ b/src/main/scala/leon/datagen/GrammarDataGen.scala
@@ -1,4 +1,4 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
+/* Copyright 2009-2015 EPFL, Lausanne */
 
 package leon
 package datagen
diff --git a/src/main/scala/leon/solvers/ADTManager.scala b/src/main/scala/leon/solvers/ADTManager.scala
index e282552673fc95ebe8bcfbafc6dd3d9ebc147fc1..0c29414816944d66602b829128648b992bbf1638 100644
--- a/src/main/scala/leon/solvers/ADTManager.scala
+++ b/src/main/scala/leon/solvers/ADTManager.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
 package leon
 package solvers
 
diff --git a/src/main/scala/leon/solvers/GroundSolver.scala b/src/main/scala/leon/solvers/GroundSolver.scala
index fd744bb6e43ad1c21c4e8ed9c00d03441354bb94..5cdaa5e42cbb219a60b1c7907589556d4982962c 100644
--- a/src/main/scala/leon/solvers/GroundSolver.scala
+++ b/src/main/scala/leon/solvers/GroundSolver.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
 package leon
 package solvers
 
diff --git a/src/main/scala/leon/solvers/RawArray.scala b/src/main/scala/leon/solvers/RawArray.scala
index 85c104ae7a39e2ee9051a62861daed44b93a9cd4..e63dbad12cc3facca75d14ca4bd86afb4e2340e0 100644
--- a/src/main/scala/leon/solvers/RawArray.scala
+++ b/src/main/scala/leon/solvers/RawArray.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
 package leon
 package solvers
 
diff --git a/src/main/scala/leon/solvers/package.scala b/src/main/scala/leon/solvers/package.scala
index e7bb86a63a3fb102a2a90051f8ffce6db1b189c1..e796cf4d1f6099e2c5270801bdd7d5a8a1086556 100644
--- a/src/main/scala/leon/solvers/package.scala
+++ b/src/main/scala/leon/solvers/package.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
 package leon
 
 import scala.reflect.runtime.universe._
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedSolver.scala
index bd2f3e05497a3ca3f087c714a5439686d143ee35..8a39d9fbb1bd33e86ab720d6b446d71942941ec7 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBZ3QuantifiedSolver.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
 package leon
 package solvers.smtlib
 
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index dd8e41851dcdf19d38ea79006990781afa68893b..2d2590da0b26f3fe324fe1fe1a537215245b646c 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -3,12 +3,9 @@
 package leon
 package synthesis
 
-import purescala.Common._
 import purescala.Definitions._
 import purescala.ExprOps._
 import purescala.DefOps._
-import purescala.Expressions._
-import purescala.Constructors._
 import purescala.ScalaPrinter
 import solvers._
 
diff --git a/src/main/scala/leon/synthesis/rules/CEGISLike.scala b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
index 686777f8e76b92b56d93d0beff473d3c6f93921d..2eabcfe44a0f7322012869382dd9935bfb61714d 100644
--- a/src/main/scala/leon/synthesis/rules/CEGISLike.scala
+++ b/src/main/scala/leon/synthesis/rules/CEGISLike.scala
@@ -39,7 +39,7 @@ abstract class CEGISLike[T <% Typed](name: String) extends Rule(name) {
     val exSolverTo  = 2000L
     val cexSolverTo = 2000L
 
-    // Track non-deterministic programs up to 50'000 programs, or give up
+    // Track non-deterministic programs up to 10'000 programs, or give up
     val nProgramsLimit = 100000
 
     val sctx = hctx.sctx
diff --git a/src/main/scala/leon/termination/SelfCallsProcessor.scala b/src/main/scala/leon/termination/SelfCallsProcessor.scala
index a18d292cd5e9dfaa96828961e4c144233bb7f31e..4f08355dc32264c05ce6f6318b6d7b5b90ccd7b7 100644
--- a/src/main/scala/leon/termination/SelfCallsProcessor.scala
+++ b/src/main/scala/leon/termination/SelfCallsProcessor.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
 package leon
 package termination
 
diff --git a/src/main/scala/leon/utils/Benchmarks.scala b/src/main/scala/leon/utils/Benchmarks.scala
index 39b635ba96dbed6ce0ef0f6b51011e165dd5319e..c3927ad12b089001ac0922545007b83b99948e57 100644
--- a/src/main/scala/leon/utils/Benchmarks.scala
+++ b/src/main/scala/leon/utils/Benchmarks.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
 package leon
 package utils
 
diff --git a/src/main/scala/leon/utils/SearchSpace.scala b/src/main/scala/leon/utils/SearchSpace.scala
index ee0424210a92a24c97f87666435b00b00330b192..b013077c9ad0feac378eba8d7142f37679495936 100644
--- a/src/main/scala/leon/utils/SearchSpace.scala
+++ b/src/main/scala/leon/utils/SearchSpace.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
 package leon.utils
 
 object SearchSpace {
diff --git a/src/main/scala/leon/xlang/FixReportLabels.scala b/src/main/scala/leon/xlang/FixReportLabels.scala
index 37c3fef240ddbaf49bc336421257fd354cadf1ec..6346402c2985855bfcc9e2973fdd6a6babc8a427 100644
--- a/src/main/scala/leon/xlang/FixReportLabels.scala
+++ b/src/main/scala/leon/xlang/FixReportLabels.scala
@@ -1,3 +1,4 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
 
 package leon
 package xlang