diff --git a/src/main/scala/leon/LeonContext.scala b/src/main/scala/leon/LeonContext.scala
index 761f882d2b7bc55e54ad9f25cd4eb142a2b20d33..91ad25d72c3ab688883ba83b2624d0570c1d32a5 100644
--- a/src/main/scala/leon/LeonContext.scala
+++ b/src/main/scala/leon/LeonContext.scala
@@ -16,5 +16,5 @@ case class LeonContext(
   settings: Settings = Settings(),
   options: Seq[LeonOption] = Seq(),
   files: Seq[File] = Seq(),
-  timers: StopwatchCollections = new StopwatchCollections
+  timers: TimerCollections = new TimerCollections
 )
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 343ed2da468953b867430e7d91634114a77a2953..7fbb19e6cb47065cd7c4909460bc694421049dbb 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -211,7 +211,7 @@ object Main {
   def main(args : Array[String]) {
     try {
       // Process options
-      val timer     = new Stopwatch().start
+      val timer     = new Timer().start
 
       val ctx = processOptions(args.toList)
 
diff --git a/src/main/scala/leon/datagen/DataGenerator.scala b/src/main/scala/leon/datagen/DataGenerator.scala
index add01c033cc4ee5113bcf3c06987d73dd6554ff9..c15f07a2b84eeb6bd6fa9018bfecac6946ea1469 100644
--- a/src/main/scala/leon/datagen/DataGenerator.scala
+++ b/src/main/scala/leon/datagen/DataGenerator.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
 package leon
 package datagen
 
diff --git a/src/main/scala/leon/plugin/ScalaCompiler.scala b/src/main/scala/leon/plugin/ScalaCompiler.scala
index f6052d60ac68b241a01235c5ff622927434cebe1..489404d02ec5a1e3428b4e68907bc9623e9cf64b 100644
--- a/src/main/scala/leon/plugin/ScalaCompiler.scala
+++ b/src/main/scala/leon/plugin/ScalaCompiler.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
 package leon
 package plugin
 
diff --git a/src/main/scala/leon/solvers/SimpleSolverAPI.scala b/src/main/scala/leon/solvers/SimpleSolverAPI.scala
index 4812f117115ad2a2a369eba0c2aa9b6f069199a2..fd4c65252e46a0d5c7460b79bae1a3a2f263892c 100644
--- a/src/main/scala/leon/solvers/SimpleSolverAPI.scala
+++ b/src/main/scala/leon/solvers/SimpleSolverAPI.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
 package leon
 package solvers
 
diff --git a/src/main/scala/leon/solvers/SolverFactory.scala b/src/main/scala/leon/solvers/SolverFactory.scala
index 2377224287383d1d1d2862d850cd0b69f5b47cc9..97e99d7d0051f6acde4a51463aadf88148df3ee1 100644
--- a/src/main/scala/leon/solvers/SolverFactory.scala
+++ b/src/main/scala/leon/solvers/SolverFactory.scala
@@ -3,6 +3,8 @@
 package leon
 package solvers
 
+import solvers.combinators._
+
 import utils._
 import purescala.Common._
 import purescala.Definitions._
diff --git a/src/main/scala/leon/solvers/TimeoutSolver.scala b/src/main/scala/leon/solvers/combinators/TimeoutSolverFactory.scala
similarity index 94%
rename from src/main/scala/leon/solvers/TimeoutSolver.scala
rename to src/main/scala/leon/solvers/combinators/TimeoutSolverFactory.scala
index fe8c590c0999e00cece981fbc8886043697808a3..ce9e50712cb3b05b2c0c2f5936dd905f631c5ee4 100644
--- a/src/main/scala/leon/solvers/TimeoutSolver.scala
+++ b/src/main/scala/leon/solvers/combinators/TimeoutSolverFactory.scala
@@ -2,6 +2,7 @@
 
 package leon
 package solvers
+package combinators
 
 import purescala.Common._
 import purescala.Definitions._
@@ -17,7 +18,7 @@ class TimeoutSolverFactory[S <: Solver](val sf: SolverFactory[S], val timeoutMs:
   val context = sf.context
   val program = sf.program
 
-  private class Timer(onTimeout: => Unit) extends Thread {
+  private class Countdown(onTimeout: => Unit) extends Thread {
     private var keepRunning = true
     private val asMillis : Long = timeoutMs
 
@@ -46,7 +47,7 @@ class TimeoutSolverFactory[S <: Solver](val sf: SolverFactory[S], val timeoutMs:
   }
 
   def withTimeout[T](solver: S)(body: => T): T = {
-    val timer = new Timer(timeout(solver))
+    val timer = new Countdown(timeout(solver))
     timer.start
     val res = body
     timer.finishedRunning
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 7eb35870843082f4b360dbfd994e6c6d987adec5..6e8dbd5f799d04e1c0b03bc8f7eb06e792169883 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -124,7 +124,7 @@ trait AbstractZ3Solver extends SolverFactory[Solver] {
   var isInitialized = false
   protected[leon] def initZ3() {
     if (!isInitialized) {
-      val initTime     = new Stopwatch().start
+      val initTime     = new Timer().start
       counter = 0
 
       z3 = new Z3Context(z3cfg)
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Component.scala b/src/main/scala/leon/solvers/z3/FairZ3Component.scala
index 14e3e4d55d1ce726cda05ad171938b2e6c7b734d..116ce98cf9125d36729108b712002cfb10f60e67 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Component.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Component.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
 package leon
 package solvers.z3
 
diff --git a/src/main/scala/leon/synthesis/SimpleSearch.scala b/src/main/scala/leon/synthesis/SimpleSearch.scala
index 39d7f0c774183ab7592b1056f1f03db94579b395..cb2dd57c192e12ce36d6040ac45ede0a68a686bd 100644
--- a/src/main/scala/leon/synthesis/SimpleSearch.scala
+++ b/src/main/scala/leon/synthesis/SimpleSearch.scala
@@ -160,7 +160,7 @@ class SimpleSearch(synth: Synthesizer,
 
 
   def searchStep() {
-    val t = new Stopwatch().start
+    val t = new Timer().start
     val nl = nextLeaf()
     synth.context.timers.get("Synthesis NextLeaf") += t
 
diff --git a/src/main/scala/leon/synthesis/Synthesizer.scala b/src/main/scala/leon/synthesis/Synthesizer.scala
index 40c3e49511c1f12801f45aca9c5decef86b460f6..b138fcc8aac6b1bbcdc56a934aedbba721a6772b 100644
--- a/src/main/scala/leon/synthesis/Synthesizer.scala
+++ b/src/main/scala/leon/synthesis/Synthesizer.scala
@@ -10,6 +10,7 @@ import purescala.Trees._
 import purescala.ScalaPrinter
 
 import solvers._
+import solvers.combinators._
 import solvers.z3._
 
 import java.io.File
diff --git a/src/main/scala/leon/synthesis/TaskRunRule.scala b/src/main/scala/leon/synthesis/TaskRunRule.scala
index 642820672d4a0cd4716ac8f131e7ecd0786cbe6c..a7f90e74f96c6bbe162de3e518525201293cef66 100644
--- a/src/main/scala/leon/synthesis/TaskRunRule.scala
+++ b/src/main/scala/leon/synthesis/TaskRunRule.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
 package leon
 package synthesis
 
diff --git a/src/main/scala/leon/synthesis/TaskTryRules.scala b/src/main/scala/leon/synthesis/TaskTryRules.scala
index 4ede43ce0bcfa266b590966aae4d78e9d4db4eaa..fd26092cf33bd57d4a5f6ea05d9198000eca96c5 100644
--- a/src/main/scala/leon/synthesis/TaskTryRules.scala
+++ b/src/main/scala/leon/synthesis/TaskTryRules.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
 package leon
 package synthesis
 
diff --git a/src/main/scala/leon/synthesis/search/AndOrGraphParallelSearch.scala b/src/main/scala/leon/synthesis/search/AndOrGraphParallelSearch.scala
index 8aba2ad6f15b874587d9bce689ef5f825ba65ed2..63ecfbafafbc2c31e2020f0d57ea7543d34ba275 100644
--- a/src/main/scala/leon/synthesis/search/AndOrGraphParallelSearch.scala
+++ b/src/main/scala/leon/synthesis/search/AndOrGraphParallelSearch.scala
@@ -22,8 +22,8 @@ abstract class AndOrGraphParallelSearch[WC,
 
   var system: ActorSystem = _
 
-  val sendWorkTimers = new StopwatchCollection("Synthesis-par SendWork")
-  val expandTimers   = new StopwatchCollection("Synthesis-par Expand")
+  val sendWorkTimers = new TimerCollection("Synthesis-par SendWork")
+  val expandTimers   = new TimerCollection("Synthesis-par Expand")
 
   def search(): Option[(S, Boolean)] = {
     system = ActorSystem("ParallelSearch")
@@ -96,7 +96,7 @@ abstract class AndOrGraphParallelSearch[WC,
 
       assert(idleWorkers.size > 0)
 
-      val t = new Stopwatch().start
+      val t = new Timer().start
 
       getNextLeaves(idleWorkers, workingWorkers) match {
         case Nil =>
@@ -136,7 +136,7 @@ abstract class AndOrGraphParallelSearch[WC,
       case WorkerAndTaskDone(w, res) =>
         workers.get(w) match {
           case Some(Some(l: g.AndLeaf)) =>
-            val t = new Stopwatch().start
+            val t = new Timer().start
             onExpansion(l, res)
             expandTimers += t
             workers += w -> None
@@ -147,7 +147,7 @@ abstract class AndOrGraphParallelSearch[WC,
       case WorkerOrTaskDone(w, res) =>
         workers.get(w) match {
           case Some(Some(l: g.OrLeaf)) =>
-            val t = new Stopwatch().start
+            val t = new Timer().start
             onExpansion(l, res)
             expandTimers += t
             workers += w -> None
diff --git a/src/main/scala/leon/synthesis/utils/Benchmarks.scala b/src/main/scala/leon/synthesis/utils/Benchmarks.scala
index 228e8720cda12474517a0ac5bab8314d77361479..55756ad45fcb69cee43293b5719bb056853ec4ac 100644
--- a/src/main/scala/leon/synthesis/utils/Benchmarks.scala
+++ b/src/main/scala/leon/synthesis/utils/Benchmarks.scala
@@ -142,7 +142,7 @@ object Benchmarks extends App {
   //                           "║ └────────────┘" + (" " * 71) + "║"
 
   //println(infoHeader2)
-  //for ((name, sw) <- StopwatchCollections.getAll.toSeq.sortBy(_._1)) {
+  //for ((name, sw) <- TimerCollections.getAll.toSeq.sortBy(_._1)) {
   //  println("║ %-70s %10s ms ║".format(name, sw.getMillis))
   //}
   //println(infoFooter)
diff --git a/src/main/scala/leon/utils/InterruptManager.scala b/src/main/scala/leon/utils/InterruptManager.scala
index d69786ca1063caa15421afa16a9d1f47d9b0b08c..d9a149aae6e668f35bcf94d7d0b301bb9d561989 100644
--- a/src/main/scala/leon/utils/InterruptManager.scala
+++ b/src/main/scala/leon/utils/InterruptManager.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
 package leon
 package utils
 
diff --git a/src/main/scala/leon/utils/Interruptible.scala b/src/main/scala/leon/utils/Interruptible.scala
index b9667d6bd6b04379d929241ba6d178d7a03b866c..b81e64ed8607d1d8623502f3054589be3ddeffc1 100644
--- a/src/main/scala/leon/utils/Interruptible.scala
+++ b/src/main/scala/leon/utils/Interruptible.scala
@@ -1,3 +1,5 @@
+/* Copyright 2009-2013 EPFL, Lausanne */
+
 package leon
 package utils
 
diff --git a/src/main/scala/leon/utils/Stopwatch.scala b/src/main/scala/leon/utils/Timer.scala
similarity index 76%
rename from src/main/scala/leon/utils/Stopwatch.scala
rename to src/main/scala/leon/utils/Timer.scala
index 9622a4bd8d005a86978ef3bca89ca3e462701507..853ae298d0ea2a107bad1a365b35a9c424ac82cb 100644
--- a/src/main/scala/leon/utils/Stopwatch.scala
+++ b/src/main/scala/leon/utils/Timer.scala
@@ -3,13 +3,13 @@
 package leon
 package utils
 
-class StopwatchCollection(val name: String) {
+class TimerCollection(val name: String) {
   var min: Long = 0L
   var tot: Long = 0L
   var max: Long = 0L
   var n: Int = 0
 
-  def +=(sw: Stopwatch) = synchronized { 
+  def +=(sw: Timer) = synchronized { 
     val ms = sw.getMillis
     if(n == 0 || ms < min) {
       min = ms
@@ -34,8 +34,8 @@ class StopwatchCollection(val name: String) {
   def getMillis = tot
 }
 
-/** Implements a stopwatch for profiling purposes */
-class Stopwatch(name: String = "Stopwatch") {
+/** Implements a timer for profiling purposes */
+class Timer(name: String = "Timer") {
   var beginning: Long = 0L
   var end: Long = 0L
   var acc: Long = 0L
@@ -73,16 +73,16 @@ class Stopwatch(name: String = "Stopwatch") {
   override def toString = "%20s: %5d%sms".format(name, getMillis, if (isRunning) "..." else "")
 }
 
-class StopwatchCollections {
-  private var all = Map[String, StopwatchCollection]()
+class TimerCollections {
+  private var all = Map[String, TimerCollection]()
 
-  def get(name: String): StopwatchCollection = all.getOrElse(name, {
-    val sw = new StopwatchCollection(name)
+  def get(name: String): TimerCollection = all.getOrElse(name, {
+    val sw = new TimerCollection(name)
     all += name -> sw
     sw
   })
 
-  def add(swc: StopwatchCollection) {
+  def add(swc: TimerCollection) {
     all += swc.name -> swc
   }
 
diff --git a/src/test/scala/leon/test/solvers/TimeoutSolverTests.scala b/src/test/scala/leon/test/solvers/TimeoutSolverTests.scala
index 988a514e980287a501f9c7fea099fed041f9f281..9745d3a123815d9d28eea90bdc444e9fe67b3208 100644
--- a/src/test/scala/leon/test/solvers/TimeoutSolverTests.scala
+++ b/src/test/scala/leon/test/solvers/TimeoutSolverTests.scala
@@ -5,6 +5,7 @@ package solvers
 
 import leon._
 import leon.solvers._
+import leon.solvers.combinators._
 import leon.purescala.Common._
 import leon.purescala.Definitions._
 import leon.purescala.Trees._