From 04fadacec65d277c7eb42d643f4b4b748e73eed2 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <etienne.kneuss@epfl.ch>
Date: Tue, 17 Feb 2015 17:59:19 +0100
Subject: [PATCH] Merge BigInts, new Leon 3.0 release
---
README.md | 9 ++++++++-
build.sbt | 2 +-
src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala | 3 ++-
3 files changed, 11 insertions(+), 3 deletions(-)
diff --git a/README.md b/README.md
index 462741ec2..9388d905a 100644
--- a/README.md
+++ b/README.md
@@ -1,4 +1,4 @@
-Leon 2.4 [](https://travis-ci.org/epfl-lara/leon)
+Leon 3.0 [](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 9c4c360f0..0c9dd4ca3 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 f73c0ae11..ab53266df 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 =>
--
GitLab