diff --git a/src/main/scala/leon/Logger.scala b/src/main/scala/leon/Logger.scala
new file mode 100644
index 0000000000000000000000000000000000000000..fc4942535112af7037660c4e7608ade80d1395dc
--- /dev/null
+++ b/src/main/scala/leon/Logger.scala
@@ -0,0 +1,24 @@
+package leon
+
+object Logger {
+
+  //the debug level to display, from 0 (no debug information) to 5 (very verbose)
+  //var level = 0
+
+  //each debug information is tagged by a string, the tag variable only display the message with a tag in this set
+  //if the set is empty then all tags are displayed
+  //var tags: Set[String] = Set()
+
+  val defaultTag = "main"
+
+  private def output(msg: String, lvl: Int, tag: String) {
+    if(lvl <= Settings.debugLevel) {
+      if(Settings.debugTags.isEmpty || Settings.debugTags.contains(tag)) {
+        println("DEBUG: [" + tag + "] " + msg)
+      }
+    }
+  }
+
+  def debug(msg: String, lvl: Int, tag: String = defaultTag) = output(msg, lvl, tag)
+
+}
diff --git a/src/main/scala/leon/Main.scala b/src/main/scala/leon/Main.scala
index 3d93d5972f95729d872c022ef418e760f6a61e1f..d184f36b7e1001c3bb3e6897b0135dabce0fc94d 100644
--- a/src/main/scala/leon/Main.scala
+++ b/src/main/scala/leon/Main.scala
@@ -31,6 +31,7 @@ object Main {
   }
 
   private def defaultAction(program: Program, reporter: Reporter) : Unit = {
+    Logger.debug("Default action on program: " + program, 5, "main")
     val passManager = new PassManager(Seq(EpsilonElimination, ImperativeCodeElimination, UnitElimination, FunctionClosure, FunctionHoisting, Simplificator))
     val program2 = passManager.run(program)
     val analysis = new Analysis(program2, reporter)
diff --git a/src/main/scala/leon/PassManager.scala b/src/main/scala/leon/PassManager.scala
index 5381b7bee6a389ac120477c8316fcf1e97ccdc62..2ab8f44ad97ad069b5e4dcf93921c685128f461c 100644
--- a/src/main/scala/leon/PassManager.scala
+++ b/src/main/scala/leon/PassManager.scala
@@ -6,9 +6,9 @@ class PassManager(passes: Seq[Pass]) {
 
   def run(program: Program): Program = {
     passes.foldLeft(program)((pgm, pass) => {
-      println("Running Pass: " + pass.description)
+      Logger.debug("Running Pass: " + pass.description, 1, "passman")
       val newPgm = pass(pgm)
-      println("Resulting program: " + newPgm)
+      Logger.debug("Resulting program: " + newPgm, 5, "passman")
       newPgm
     })
   }
diff --git a/src/main/scala/leon/Settings.scala b/src/main/scala/leon/Settings.scala
index 9e7055638b46d401a55d9a49866ad8bc0e7751e3..b47a794655a2940ce306e1f1ece1acd46a16ee53 100644
--- a/src/main/scala/leon/Settings.scala
+++ b/src/main/scala/leon/Settings.scala
@@ -24,5 +24,6 @@ object Settings {
   var useParallel : Boolean = false
   // When this is None, use real integers
   var bitvectorBitwidth : Option[Int] = None
-  var verbose : Boolean = false
+  var debugLevel: Int = 0
+  var debugTags: Set[String] = Set.empty
 }
diff --git a/src/main/scala/leon/plugin/LeonPlugin.scala b/src/main/scala/leon/plugin/LeonPlugin.scala
index 3654de04ad807d2fd55a7470ce5c3fd97a131327..5fecbb605367f1141798fb67df18edfc957cc613 100644
--- a/src/main/scala/leon/plugin/LeonPlugin.scala
+++ b/src/main/scala/leon/plugin/LeonPlugin.scala
@@ -41,7 +41,9 @@ class LeonPlugin(val global: Global, val actionAfterExtraction : Option[Program=
     "  --parallel           Run all solvers in parallel" + "\n" +
     "  --noLuckyTests       Do not perform additional tests to potentially find models early" + "\n" +
     "  --noverifymodel      Do not verify the correctness of models returned by Z3" + "\n" +
-    "  --verbose            Print debugging informations"
+    "  --verbose            Print debugging informations" + "\n" +
+    "  --debug=[1-5]        Debug level" + "\n" +
+    "  --tags=t1:...        Filter out debug information that are not of one of the given tags"
   )
 
   /** Processes the command-line options. */
@@ -66,6 +68,8 @@ class LeonPlugin(val global: Global, val actionAfterExtraction : Option[Program=
         case "noLuckyTests" =>                   leon.Settings.luckyTest = false
         case "noverifymodel" =>                  leon.Settings.verifyModel = false
         case "verbose"    =>                     leon.Settings.verbose = true
+        case s if s.startsWith("debug=") =>       leon.Settings.debugLevel = try { s.substring("debug=".length, s.length).toInt } catch { case _ => 0 }
+        case s if s.startsWith("tags=") =>       leon.Settings.debugTags = Set(splitList(s.substring("tags=".length, s.length)): _*)
         case s if s.startsWith("unrolling=") =>  leon.Settings.unrollingLevel = try { s.substring("unrolling=".length, s.length).toInt } catch { case _ => 0 }
         case s if s.startsWith("functions=") =>  leon.Settings.functionsToAnalyse = Set(splitList(s.substring("functions=".length, s.length)): _*)
         case s if s.startsWith("extensions=") => leon.Settings.extensionNames = splitList(s.substring("extensions=".length, s.length))