diff --git a/library/lang/Real.scala b/library/lang/Real.scala
new file mode 100644
index 0000000000000000000000000000000000000000..3e94b27c0d544307f693f3b2d159411c92bdcfd2
--- /dev/null
+++ b/library/lang/Real.scala
@@ -0,0 +1,17 @@
+package leon.lang
+import leon.annotation._
+
+@ignore
+class Real {
+
+   def +(a: Real): Real = ???
+   def -(a: Real): Real = ???
+   def *(a: Real): Real = ???
+   def /(a: Real): Real = ???
+
+   def unary_- : Real = ???
+}
+
+object Real {
+  def apply(n: BigInt, d: BigInt): Real = ???
+}
diff --git a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
index 402a7d7cf724659e0b240516281f28e22cc8e87f..348680e6ea5405efbaffec4bf94a52a35784d2b1 100644
--- a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
+++ b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
@@ -40,6 +40,7 @@ trait ASTExtractors {
   protected lazy val scalaSetSym        = classFromName("scala.collection.immutable.Set")
   protected lazy val setSym             = classFromName("leon.lang.Set")
   protected lazy val mapSym             = classFromName("leon.lang.Map")
+  protected lazy val realSym            = classFromName("leon.lang.Real")
   protected lazy val optionClassSym     = classFromName("scala.Option")
   protected lazy val arraySym           = classFromName("scala.Array")
   protected lazy val someClassSym       = classFromName("scala.Some")
@@ -72,6 +73,10 @@ trait ASTExtractors {
     getResolvedTypeSym(sym) == setSym
   }
 
+  def isRealSym(sym: Symbol) : Boolean = {
+    getResolvedTypeSym(sym) == realSym
+  }
+
   def isScalaSetSym(sym: Symbol) : Boolean = {
     getResolvedTypeSym(sym) == scalaSetSym
   }
@@ -242,6 +247,15 @@ trait ASTExtractors {
       }
     }
 
+    object ExRealLiteral {
+      def unapply(tree: Tree): Option[(Tree, Tree)] = tree  match {
+        case Apply(ExSelected("leon", "lang", "Real", "apply"), n :: d :: Nil) =>
+          Some((n, d))
+        case _ =>
+          None
+      }
+    }
+
 
     object ExIntToBigInt {
       def unapply(tree: Tree): Option[Tree] = tree  match {
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 1e995aaf643b8ca20048bdbfe2c0c63daff8fb09..d7cab0c0a6b232eba35b5b5a28191147e7bb70dd 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -1213,6 +1213,9 @@ trait CodeExtraction extends ASTExtractors {
           }
         }
 
+        case ExRealLiteral(n: Literal, d: Literal) =>
+          RealLiteral((BigInt(n.value.stringValue), BigInt(d.value.stringValue)))
+
         case ExInt32Literal(v) =>
           IntLiteral(v)
 
@@ -1505,6 +1508,24 @@ trait CodeExtraction extends ASTExtractors {
             case (IsTyped(a1, IntegerType), "<=", List(IsTyped(a2, IntegerType))) =>
               LessEquals(a1, a2)
 
+            //Real methods
+            case (IsTyped(a1, RealType), "+", List(IsTyped(a2, RealType))) =>
+              RealPlus(a1, a2)
+            case (IsTyped(a1, RealType), "-", List(IsTyped(a2, RealType))) =>
+              RealMinus(a1, a2)
+            case (IsTyped(a1, RealType), "*", List(IsTyped(a2, RealType))) =>
+              RealTimes(a1, a2)
+            case (IsTyped(a1, RealType), "/", List(IsTyped(a2, RealType))) =>
+              RealDivision(a1, a2)
+            case (IsTyped(a1, RealType), ">", List(IsTyped(a2, RealType))) =>
+              GreaterThan(a1, a2)
+            case (IsTyped(a1, RealType), ">=", List(IsTyped(a2, RealType))) =>
+              GreaterEquals(a1, a2)
+            case (IsTyped(a1, RealType), "<", List(IsTyped(a2, RealType))) =>
+              LessThan(a1, a2)
+            case (IsTyped(a1, RealType), "<=", List(IsTyped(a2, RealType))) =>
+              LessEquals(a1, a2)
+
             // Int methods
             case (IsTyped(a1, Int32Type), "+", List(IsTyped(a2, Int32Type))) =>
               BVPlus(a1, a2)
diff --git a/src/main/scala/leon/purescala/Expressions.scala b/src/main/scala/leon/purescala/Expressions.scala
index c25f9be4322e3494b75776c937414272515c8f14..12900e3ec8ce09cb1d2c1aed8e51a9a95c5a38bb 100644
--- a/src/main/scala/leon/purescala/Expressions.scala
+++ b/src/main/scala/leon/purescala/Expressions.scala
@@ -274,6 +274,9 @@ object Expressions {
   case class InfiniteIntegerLiteral(value: BigInt) extends Literal[BigInt] {
     val getType = IntegerType
   }
+  case class RealLiteral(value: (BigInt, BigInt)) extends Literal[(BigInt, BigInt)] {
+    val getType = RealType
+  }
 
   case class BooleanLiteral(value: Boolean) extends Literal[Boolean] {
     val getType = BooleanType
@@ -482,6 +485,29 @@ object Expressions {
   }
 
 
+  /* Integer arithmetic */
+  case class RealPlus(lhs: Expr, rhs: Expr) extends Expr {
+    require(lhs.getType == RealType && rhs.getType == RealType)
+    val getType = RealType
+  }
+  case class RealMinus(lhs: Expr, rhs: Expr) extends Expr { 
+    require(lhs.getType == RealType && rhs.getType == RealType)
+    val getType = RealType
+  }
+  case class RealUMinus(expr: Expr) extends Expr { 
+    require(expr.getType == RealType)
+    val getType = RealType
+  }
+  case class RealTimes(lhs: Expr, rhs: Expr) extends Expr { 
+    require(lhs.getType == RealType && rhs.getType == RealType)
+    val getType = RealType
+  }
+  case class RealDivision(lhs: Expr, rhs: Expr) extends Expr { 
+    require(lhs.getType == RealType && rhs.getType == RealType)
+    val getType = RealType
+  }
+
+
   /* Tuple operations */
 
   // If you are not sure about the requirement you should use
diff --git a/src/main/scala/leon/purescala/Types.scala b/src/main/scala/leon/purescala/Types.scala
index 6bb1f921dbb53d41937d4a6989d00148d8ca9734..3754b85342f48b6b8411ae3961b5c6597dbd2c81 100644
--- a/src/main/scala/leon/purescala/Types.scala
+++ b/src/main/scala/leon/purescala/Types.scala
@@ -47,6 +47,7 @@ object Types {
   case object UnitType extends TypeTree
   case object CharType extends TypeTree
   case object IntegerType extends TypeTree
+  case object RealType extends TypeTree
 
   case class BitVectorType(size: Int) extends TypeTree
   case object Int32Type extends TypeTree