diff --git a/README.md b/README.md
index 462741ec206180313bdabd69cb51e6416bc316f3..9388d905a732e4888352d3326fcbe4f90164199d 100644
--- a/README.md
+++ b/README.md
@@ -1,4 +1,4 @@
-Leon 2.4 [![Build Status](https://travis-ci.org/epfl-lara/leon.png?branch=master)](https://travis-ci.org/epfl-lara/leon)
+Leon 3.0 [![Build Status](https://travis-ci.org/epfl-lara/leon.png?branch=master)](https://travis-ci.org/epfl-lara/leon)
 ==========
 
 Getting Started
@@ -158,6 +158,13 @@ but instead
 Changelog
 ---------
 
+#### v3.0
+*Released 17.02.2015*
+
+* Int is now treated as BitVector(32)
+* Introduce BigInt for natural numbers
+
+
 #### v2.4
 *Released 10.02.2015*
 
diff --git a/build.sbt b/build.sbt
index 9c4c360f094cf1f7fdc8baf90ecbcfabc8cdecd5..0c9dd4ca3908b210bc6fd14d4bfc9cf65f7c69c7 100644
--- a/build.sbt
+++ b/build.sbt
@@ -1,6 +1,6 @@
 name := "Leon"
 
-version := "2.4"
+version := "3.0"
 
 organization := "ch.epfl.lara"
 
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index f73c0ae11e506e664e52204cf4f7e5b68b191eac..ab53266df80d709b30adadea435c064142822151 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -379,6 +379,7 @@ trait AbstractZ3Solver
 
     //TODO: mkBitVectorType
     sorts += Int32Type -> z3.mkBVSort(32)
+    sorts += CharType -> z3.mkBVSort(32)
     sorts += IntegerType -> z3.mkIntSort
     sorts += BooleanType -> z3.mkBoolSort
     sorts += UnitType -> us
@@ -406,7 +407,7 @@ trait AbstractZ3Solver
 
   // assumes prepareSorts has been called....
   protected[leon] def typeToSort(oldtt: TypeTree): Z3Sort = normalizeType(oldtt) match {
-    case Int32Type | BooleanType | UnitType | IntegerType =>
+    case Int32Type | BooleanType | UnitType | IntegerType | CharType =>
       sorts.toZ3(oldtt)
 
     case act: AbstractClassType =>