diff --git a/src/main/scala/leon/LeonOption.scala b/src/main/scala/leon/LeonOption.scala
index 4678772d2468775867998cc045613be94081f882..1ad3cb99bd85505b0f85319e8f93af8d0e15527c 100644
--- a/src/main/scala/leon/LeonOption.scala
+++ b/src/main/scala/leon/LeonOption.scala
@@ -10,6 +10,14 @@ case class LeonFlagOption(name: String) extends LeonOption
 /** Options of the form --option=value. */
 case class LeonValueOption(name: String, value: String) extends LeonOption {
   def splitList : Seq[String] = value.split(':').map(_.trim).filter(!_.isEmpty)
+
+  def asInt(ctx : LeonContext) : Option[Int] = try {
+    Some(value.toInt)
+  } catch {
+    case _ : Throwable =>
+      ctx.reporter.error("Option --%s takes an integer as value.".format(name))
+      None
+  }
 }
 
 sealed abstract class LeonOptionDef {
diff --git a/src/main/scala/leon/synthesis/SynthesisPhase.scala b/src/main/scala/leon/synthesis/SynthesisPhase.scala
index 466abaf1df1c2d221ab6e1009eecd4c82c3f5df2..028c7dcdd9d1d0b2d9e2201132ba2fc299226ea1 100644
--- a/src/main/scala/leon/synthesis/SynthesisPhase.scala
+++ b/src/main/scala/leon/synthesis/SynthesisPhase.scala
@@ -47,12 +47,10 @@ object SynthesisPhase extends LeonPhase[Program, Program] {
           case None =>
             ctx.reporter.fatalError("Unknown cost model: "+cm)
         }
-      case LeonValueOption("timeout", t) =>
-        try {
+      case v @ LeonValueOption("timeout", _) =>
+        v.asInt(ctx).foreach { t =>
           options = options.copy(timeoutMs  = Some(t.toLong))
-        } catch {
-          case _: Throwable => 
-        }
+        } 
       case LeonFlagOption("firstonly") =>
         options = options.copy(firstOnly = true)
       case LeonFlagOption("parallel") =>
diff --git a/src/main/scala/leon/verification/AnalysisPhase.scala b/src/main/scala/leon/verification/AnalysisPhase.scala
index d88b7351997c27476f7dc36bf5d4709ac134d634..65e8dcce5d9c23aff3a391783127e4965c777bd9 100644
--- a/src/main/scala/leon/verification/AnalysisPhase.scala
+++ b/src/main/scala/leon/verification/AnalysisPhase.scala
@@ -28,12 +28,10 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
     for(opt <- ctx.options) opt match {
       case LeonValueOption("functions", ListValue(fs)) =>
         functionsToAnalyse ++= fs
-      case LeonValueOption("timeout", t) =>
-        try {
-          timeout = Some(t.toInt)
-        } catch {
-          case _: Throwable => 
-        }
+
+      case v @ LeonValueOption("timeout", _) =>
+        timeout = v.asInt(ctx)
+
       case _ =>
     }