diff --git a/cp-demo/RedBlackTree.scala b/cp-demo/RedBlackTree.scala
index b30df1da2be7bae8e0717e8c73f37bd7a5978ee7..46d611b7382e634e3797da5545af229596c1491d 100644
--- a/cp-demo/RedBlackTree.scala
+++ b/cp-demo/RedBlackTree.scala
@@ -1,5 +1,5 @@
 import cp.Definitions._
-import cp.Utils._
+import purescala.Stopwatch
 
 object RedBlackTree { 
   @spec sealed abstract class Color
@@ -96,12 +96,12 @@ object RedBlackTree {
 
     val solutionSet = scala.collection.mutable.Set[Tree]()
     println("Fixing size of trees to " + (bound))
-    val timer = new Timer("Fixed-size enumeration", true)
-    timer.start
+    val sw = new Stopwatch("Fixed-size enumeration", false)
+    sw.start
     for (tree <- findAll((t : Tree) => isRedBlackTree(t) && boundValues(t, bound - 1) && size(t) == bound)) {
       solutionSet += tree
     }
-    timer.stop
+    sw.stop
 
     // for (tree <- solutionSet)
     //   println(print(tree) + "\n-----------\n")
diff --git a/src/cp/RuntimeMethods.scala b/src/cp/RuntimeMethods.scala
index 5f2212fbd4fdc0c1ebadf0ce4b851b9129e053a0..6ecf0096b9899c28b74b22ec8c0ffd2f7f7e2873 100644
--- a/src/cp/RuntimeMethods.scala
+++ b/src/cp/RuntimeMethods.scala
@@ -11,8 +11,10 @@ object RuntimeMethods {
   import purescala.{DefaultReporter,QuietReporter}
   import purescala.FairZ3Solver
 
-  private def newReporter() = new QuietReporter()
-  // private def newReporter() = new DefaultReporter()
+  import purescala.Stopwatch
+  
+  private val silent = true
+  private def newReporter() = if (silent) new QuietReporter() else new DefaultReporter()
   private def newSolver() = new FairZ3Solver(newReporter())
 
   def chooseExec(progString : String, progId : Int, exprString : String, exprId : Int, outputVarsString : String, outputVarsId : Int, inputConstraints : Expr) : Seq[Expr] = {
@@ -325,7 +327,9 @@ object RuntimeMethods {
       override def hasNext : Boolean = nextModel match {
         case None => 
           // Check whether there are any more models
+          val stopwatch = new Stopwatch("hasNext", true).start
           val (outcome, model) = solver.decideWithModel(toCheck, false)
+          stopwatch.stop
           val toReturn = (outcome match {
             case Some(false) =>
               // there is a solution, we need to complete model for nonmentioned variables
@@ -362,7 +366,9 @@ object RuntimeMethods {
       override def next() : Map[Identifier, Expr] = nextModel match {
         case None => {
           // Let's compute the next model
+          val stopwatch = new Stopwatch("next", true).start
           val (outcome, model) = solver.decideWithModel(toCheck, false)
+          stopwatch.stop
           val toReturn = (outcome match {
             case Some(false) =>
               // there is a solution, we need to complete model for nonmentioned variables
diff --git a/src/cp/Utils.scala b/src/cp/Utils.scala
deleted file mode 100644
index 2eb9b5971d8664dcfde0f077c395ca99c06a5b4e..0000000000000000000000000000000000000000
--- a/src/cp/Utils.scala
+++ /dev/null
@@ -1,17 +0,0 @@
-package cp
-
-object Utils {
-  class Timer(description : String, verbose : Boolean = false) {
-    var beginning: Long = 0L
-    var end: Long = 0L
-    def start = {
-      beginning = System.currentTimeMillis
-    }
-    def stop : Double = {
-      end = System.currentTimeMillis
-      val seconds = (end - beginning) / 1000.0
-      if (verbose) println("Timer \"" + description + "\": " + seconds + " s")
-      seconds
-    }
-  }
-}
diff --git a/src/purescala/FairZ3Solver.scala b/src/purescala/FairZ3Solver.scala
index 246c930f45c9f1dd906032adf79b2f0ac5110e22..2e61161ab5c910d195336ff2a89bfc5deff75837 100644
--- a/src/purescala/FairZ3Solver.scala
+++ b/src/purescala/FairZ3Solver.scala
@@ -326,7 +326,9 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
         println(blockingSetAsZ3)
         z3.checkAssumptions(blockingSetAsZ3 : _*)
       } else {
+        val stopwatch = new Stopwatch("Z3 search", true).start
         val (a, m) = z3.checkAndGetModel()
+        stopwatch.stop
         (a, m, Seq.empty[Z3AST])
       }
 
diff --git a/src/purescala/Stopwatch.scala b/src/purescala/Stopwatch.scala
new file mode 100644
index 0000000000000000000000000000000000000000..86823fcbe3451800316befe793f8dc60808bd7e8
--- /dev/null
+++ b/src/purescala/Stopwatch.scala
@@ -0,0 +1,17 @@
+package purescala
+
+/** Implements a stopwatch for profiling purposes */
+class Stopwatch(description : String, verbose : Boolean = false) {
+  var beginning: Long = 0L
+  var end: Long = 0L
+  def start : Stopwatch = {
+    beginning = System.currentTimeMillis
+    this
+  }
+  def stop : Double = {
+    end = System.currentTimeMillis
+    val seconds = (end - beginning) / 1000.0
+    if (verbose) println("Stopwatch \"" + description + "\": " + seconds + " s")
+    seconds
+  }
+}