diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
index 51df2bd3f4288f8ccf65dc0cff3ffc72f718fc1a..241dbd2e092bd77e40a89a84c51e7d2b3f2ae79a 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
@@ -585,6 +585,9 @@ abstract class SMTLIBSolver(val context: LeonContext,
     case (SDecimal(d), RealType) =>
       RealLiteral(d)
 
+    case (SNumeral(n), RealType) =>
+      RealLiteral(BigDecimal(n))
+
     case (Core.True(), BooleanType)  => BooleanLiteral(true)
     case (Core.False(), BooleanType)  => BooleanLiteral(false)
 
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index e3fd1fbc472cde897fe90916666c18e4fe09172d..1b33ca60db3dcc1f2baa1c340218361aea409895 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -252,6 +252,7 @@ trait AbstractZ3Solver
     sorts += Int32Type -> z3.mkBVSort(32)
     sorts += CharType -> z3.mkBVSort(32)
     sorts += IntegerType -> z3.mkIntSort
+    sorts += RealType -> z3.mkRealSort
     sorts += BooleanType -> z3.mkBoolSort
 
     testers.clear
@@ -265,7 +266,7 @@ trait AbstractZ3Solver
 
   // assumes prepareSorts has been called....
   protected[leon] def typeToSort(oldtt: TypeTree): Z3Sort = normalizeType(oldtt) match {
-    case Int32Type | BooleanType | IntegerType | CharType =>
+    case Int32Type | BooleanType | IntegerType | RealType | CharType =>
       sorts.toB(oldtt)
 
     case tpe @ (_: ClassType  | _: ArrayType | _: TupleType | UnitType) =>
@@ -382,6 +383,7 @@ trait AbstractZ3Solver
       case Not(e) => z3.mkNot(rec(e))
       case IntLiteral(v) => z3.mkInt(v, typeToSort(Int32Type))
       case InfiniteIntegerLiteral(v) => z3.mkNumeral(v.toString, typeToSort(IntegerType))
+      case RealLiteral(v) => z3.mkNumeral(v.toString, typeToSort(RealType))
       case CharLiteral(c) => z3.mkInt(c, typeToSort(CharType))
       case BooleanLiteral(v) => if (v) z3.mkTrue() else z3.mkFalse()
       case Equals(l, r) => z3.mkEq(rec( l ), rec( r ) )
@@ -405,6 +407,13 @@ trait AbstractZ3Solver
         z3.mkMod(rec(l), rec(r))
       }
       case UMinus(e) => z3.mkUnaryMinus(rec(e))
+
+      case RealPlus(l, r) => z3.mkAdd(rec(l), rec(r))
+      case RealMinus(l, r) => z3.mkSub(rec(l), rec(r))
+      case RealTimes(l, r) => z3.mkMul(rec(l), rec(r))
+      case RealDivision(l, r) => z3.mkDiv(rec(l), rec(r))
+      case RealUMinus(e) => z3.mkUnaryMinus(rec(e))
+
       case BVPlus(l, r) => z3.mkBVAdd(rec(l), rec(r))
       case BVMinus(l, r) => z3.mkBVSub(rec(l), rec(r))
       case BVTimes(l, r) => z3.mkBVMul(rec(l), rec(r))
@@ -420,21 +429,25 @@ trait AbstractZ3Solver
       case BVLShiftRight(l, r) => z3.mkBVLshr(rec(l), rec(r))
       case LessThan(l, r) => l.getType match {
         case IntegerType => z3.mkLT(rec(l), rec(r))
+        case RealType => z3.mkLT(rec(l), rec(r))
         case Int32Type => z3.mkBVSlt(rec(l), rec(r))
         case CharType => z3.mkBVSlt(rec(l), rec(r))
       }
       case LessEquals(l, r) => l.getType match {
         case IntegerType => z3.mkLE(rec(l), rec(r))
+        case RealType => z3.mkLE(rec(l), rec(r))
         case Int32Type => z3.mkBVSle(rec(l), rec(r))
         case CharType => z3.mkBVSle(rec(l), rec(r))
       }
       case GreaterThan(l, r) => l.getType match {
         case IntegerType => z3.mkGT(rec(l), rec(r))
+        case RealType => z3.mkGT(rec(l), rec(r))
         case Int32Type => z3.mkBVSgt(rec(l), rec(r))
         case CharType => z3.mkBVSgt(rec(l), rec(r))
       }
       case GreaterEquals(l, r) => l.getType match {
         case IntegerType => z3.mkGE(rec(l), rec(r))
+        case RealType => z3.mkGE(rec(l), rec(r))
         case Int32Type => z3.mkBVSge(rec(l), rec(r))
         case CharType => z3.mkBVSge(rec(l), rec(r))
       }
@@ -649,6 +662,9 @@ trait AbstractZ3Solver
             }
           }
         }
+        case Z3NumeralRealAST(num: BigInt, den: BigInt) => {
+          RealLiteral(BigDecimal(num) / BigDecimal(den))
+        }
         case Z3AppAST(decl, args) =>
           val argsSize = args.size
           if(argsSize == 0 && (variables containsB t)) {
diff --git a/src/test/resources/regression/verification/purescala/valid/BasicReal.scala b/src/test/resources/regression/verification/purescala/valid/BasicReal.scala
new file mode 100644
index 0000000000000000000000000000000000000000..7dac0622acce645c150decc8753c205eb7d97d8b
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/BasicReal.scala
@@ -0,0 +1,26 @@
+import leon.lang._
+import leon.annotation._
+
+object BasicReal {
+
+  def plusOfPositiveNumbers(x: Real, y: Real): Real = {
+    require(x >= Real(0) && y >= Real(0))
+    x + y
+  } ensuring(_ >= Real(0))
+
+
+  def max(x: Real, y: Real): Real = {
+    if(x >= y) x else y
+  } ensuring(res => (res == x || res == y) && res >= x && res >= y)
+
+
+  def divBy2(x: Real): Boolean = {
+    x/Real(2) == x*Real(1,2)
+  } holds
+
+  def twice(x: Real): Real = {
+    require(x > Real(0))
+    Real(2)*x
+  } ensuring(res => res > x)
+
+}
diff --git a/src/test/resources/regression/verification/purescala/valid/RealNonDiscrete.scala b/src/test/resources/regression/verification/purescala/valid/RealNonDiscrete.scala
new file mode 100644
index 0000000000000000000000000000000000000000..3a234b88b83b50934cf3dcc7095b26e118ec30f2
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/RealNonDiscrete.scala
@@ -0,0 +1,11 @@
+import leon.lang._
+import leon.annotation._
+
+object RealNonDiscrete {
+
+  def nonDiscrete(x: Real): Boolean = {
+    require(x > Real(1) && x < Real(3))
+    x == Real(2)
+  } holds
+
+}