diff --git a/library/io/StdIn.scala b/library/io/StdIn.scala
new file mode 100644
index 0000000000000000000000000000000000000000..57012be57c15f8837310384892c3cf8ee1f6e438
--- /dev/null
+++ b/library/io/StdIn.scala
@@ -0,0 +1,57 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+package leon.io
+
+import leon.annotation._
+
+object StdIn {
+
+  @library
+  case class State(var seed: BigInt)
+
+  @library
+  def newState: State = State(0)
+
+  @library
+  @isabelle.noBody()
+  def readInt(implicit state: State): Int = {
+    state.seed += 1
+    nativeReadInt
+  }
+
+  @library
+  @extern
+  @isabelle.noBody()
+  private def nativeReadInt(implicit state: State): Int = {
+    scala.io.StdIn.readInt
+  } ensuring((x: Int) => true)
+
+  @library
+  @isabelle.noBody()
+  def readBigInt(implicit state: State): BigInt = {
+    state.seed += 1
+    nativeReadBigInt
+  }
+
+  @library
+  @extern
+  @isabelle.noBody()
+  private def nativeReadBigInt(implicit state: State): BigInt = {
+    BigInt(scala.io.StdIn.readInt)
+  } ensuring((x: BigInt) => true)
+
+  @library
+  @isabelle.noBody()
+  def readBoolean(implicit state: State): Boolean = {
+    state.seed += 1
+    nativeReadBoolean
+  }
+
+  @library
+  @extern
+  @isabelle.noBody()
+  private def nativeReadBoolean(implicit state: State): Boolean = {
+    scala.io.StdIn.readBoolean
+  } ensuring((x: Boolean) => true)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/invalid/StdIn1.scala b/src/test/resources/regression/verification/xlang/invalid/StdIn1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..aa3a326ff377c805eef18dadd06f7b2fed8d1e0f
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/invalid/StdIn1.scala
@@ -0,0 +1,10 @@
+import leon.io._
+
+object StdIn1 {
+
+  def alwaysPos: Int = {
+    implicit val state = StdIn.newState
+    StdIn.readInt
+  } ensuring(_ >= 0)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/invalid/StdIn2.scala b/src/test/resources/regression/verification/xlang/invalid/StdIn2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..f9a24021251f5b2328e0531faa8722871d718053
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/invalid/StdIn2.scala
@@ -0,0 +1,13 @@
+import leon.io._
+
+object StdIn2 {
+
+  def anyTwoNumbers: Boolean = {
+    implicit val state = StdIn.newState
+    val n1 = StdIn.readInt
+    val n2 = StdIn.readInt
+
+    n1 == n2
+  } ensuring(res => res)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/invalid/StdIn3.scala b/src/test/resources/regression/verification/xlang/invalid/StdIn3.scala
new file mode 100644
index 0000000000000000000000000000000000000000..9511b21fd5dfa5b93d0272e4319bc246ffa85f1b
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/invalid/StdIn3.scala
@@ -0,0 +1,12 @@
+import leon.io._
+
+object StdIn3 {
+
+  //should be invalid because of MinInt
+  def abs: Int = {
+    implicit val state = StdIn.newState
+    val n = StdIn.readInt
+    if(n < 0) -n else n
+  } ensuring(_ >= 0)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/invalid/StdIn4.scala b/src/test/resources/regression/verification/xlang/invalid/StdIn4.scala
new file mode 100644
index 0000000000000000000000000000000000000000..79c357b1d3165bb3303f4d70b578c0d9d731f8d7
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/invalid/StdIn4.scala
@@ -0,0 +1,10 @@
+import leon.io._
+
+object StdIn4 {
+
+  def readBoolCanBeFalse: Boolean = {
+    implicit val state = StdIn.newState
+    StdIn.readBoolean
+  } ensuring(res => res)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/StdIn1.scala b/src/test/resources/regression/verification/xlang/valid/StdIn1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..1fad9efd665b9660d82585519e6c2de30b786947
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/StdIn1.scala
@@ -0,0 +1,11 @@
+import leon.io._
+
+object StdIn1 {
+
+  def abs: BigInt = {
+    implicit val state = StdIn.newState
+    val n = StdIn.readBigInt
+    if(n < 0) -n else n
+  } ensuring(_ >= 0)
+
+}