diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index d5bf1facfabd69ae22c8b6d1fcc8f5853b0dba9b..86e6ef578a24b37c63e45398e31fd4c30afaa15b 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -356,6 +356,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
(e(l), e(r)) match {
case (IntLiteral(i1), IntLiteral(i2)) => BooleanLiteral(i1 < i2)
case (InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2)) => BooleanLiteral(i1 < i2)
+ case (CharLiteral(c1), CharLiteral(c2)) => BooleanLiteral(c1 < c2)
case (le,re) => throw EvalError(typeErrorMsg(le, Int32Type))
}
@@ -363,6 +364,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
(e(l), e(r)) match {
case (IntLiteral(i1), IntLiteral(i2)) => BooleanLiteral(i1 > i2)
case (InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2)) => BooleanLiteral(i1 > i2)
+ case (CharLiteral(c1), CharLiteral(c2)) => BooleanLiteral(c1 > c2)
case (le,re) => throw EvalError(typeErrorMsg(le, Int32Type))
}
@@ -370,6 +372,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
(e(l), e(r)) match {
case (IntLiteral(i1), IntLiteral(i2)) => BooleanLiteral(i1 <= i2)
case (InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2)) => BooleanLiteral(i1 <= i2)
+ case (CharLiteral(c1), CharLiteral(c2)) => BooleanLiteral(c1 <= c2)
case (le,re) => throw EvalError(typeErrorMsg(le, Int32Type))
}
@@ -377,6 +380,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
(e(l), e(r)) match {
case (IntLiteral(i1), IntLiteral(i2)) => BooleanLiteral(i1 >= i2)
case (InfiniteIntegerLiteral(i1), InfiniteIntegerLiteral(i2)) => BooleanLiteral(i1 >= i2)
+ case (CharLiteral(c1), CharLiteral(c2)) => BooleanLiteral(c1 >= c2)
case (le,re) => throw EvalError(typeErrorMsg(le, Int32Type))
}
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index ce7661ceb720a73ac72322b798bb134b9a4c121d..b37b6672fe7c741e5c76e09408dd56bb2c55871d 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -1715,7 +1715,20 @@ trait CodeExtraction extends ASTExtractors {
case (IsTyped(a1, mt1: MapType), "++", List(IsTyped(a2, mt2: MapType))) if mt1 == mt2 =>
MapUnion(a1, a2)
-
+
+ // Char operations
+ case (IsTyped(a1, CharType), ">", List(IsTyped(a2, CharType))) =>
+ GreaterThan(a1, a2)
+
+ case (IsTyped(a1, CharType), ">=", List(IsTyped(a2, CharType))) =>
+ GreaterEquals(a1, a2)
+
+ case (IsTyped(a1, CharType), "<", List(IsTyped(a2, CharType))) =>
+ LessThan(a1, a2)
+
+ case (IsTyped(a1, CharType), "<=", List(IsTyped(a2, CharType))) =>
+ LessEquals(a1, a2)
+
case (_, name, _) =>
outOfSubsetError(tr, "Unknown call to "+name)
}
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
index c0dbf1e9ab91614bef500563cab6be2df8f5e6d8..3df3f89e57d809ba8d1ba6ef2785dbd078a71333 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
@@ -651,18 +651,22 @@ abstract class SMTLIBSolver(val context: LeonContext,
case LessThan(a,b) => a.getType match {
case Int32Type => FixedSizeBitVectors.SLessThan(toSMT(a), toSMT(b))
case IntegerType => Ints.LessThan(toSMT(a), toSMT(b))
+ case CharType => FixedSizeBitVectors.SLessThan(toSMT(a), toSMT(b))
}
case LessEquals(a,b) => a.getType match {
case Int32Type => FixedSizeBitVectors.SLessEquals(toSMT(a), toSMT(b))
case IntegerType => Ints.LessEquals(toSMT(a), toSMT(b))
+ case CharType => FixedSizeBitVectors.SLessEquals(toSMT(a), toSMT(b))
}
case GreaterThan(a,b) => a.getType match {
case Int32Type => FixedSizeBitVectors.SGreaterThan(toSMT(a), toSMT(b))
case IntegerType => Ints.GreaterThan(toSMT(a), toSMT(b))
+ case CharType => FixedSizeBitVectors.SGreaterThan(toSMT(a), toSMT(b))
}
case GreaterEquals(a,b) => a.getType match {
case Int32Type => FixedSizeBitVectors.SGreaterEquals(toSMT(a), toSMT(b))
case IntegerType => Ints.GreaterEquals(toSMT(a), toSMT(b))
+ case CharType => FixedSizeBitVectors.SGreaterEquals(toSMT(a), toSMT(b))
}
case BVPlus(a,b) => FixedSizeBitVectors.Add(toSMT(a), toSMT(b))
case BVMinus(a,b) => FixedSizeBitVectors.Sub(toSMT(a), toSMT(b))
@@ -701,6 +705,9 @@ abstract class SMTLIBSolver(val context: LeonContext,
case (_, UnitType) =>
UnitLiteral()
+ case (FixedSizeBitVectors.BitVectorConstant(n, b), CharType) if b == BigInt(32) =>
+ CharLiteral(n.toInt.toChar)
+
case (SHexadecimal(h), CharType) =>
CharLiteral(h.toInt.toChar)
diff --git a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
index 4a5e6ed572d2f2fa74d38facdf0235892e83d4b7..42d53fc24645c08931641eae4db37df3020e7143 100644
--- a/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/AbstractZ3Solver.scala
@@ -596,18 +596,22 @@ trait AbstractZ3Solver
case LessThan(l, r) => l.getType match {
case IntegerType => 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 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 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 Int32Type => z3.mkBVSge(rec(l), rec(r))
+ case CharType => z3.mkBVSge(rec(l), rec(r))
}
case c @ CaseClass(ct, args) =>
diff --git a/src/test/resources/regression/verification/purescala/invalid/CharCompare.scala b/src/test/resources/regression/verification/purescala/invalid/CharCompare.scala
new file mode 100644
index 0000000000000000000000000000000000000000..8dade4ccc2da3d9587cc46027d940b4a4712d5a4
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/invalid/CharCompare.scala
@@ -0,0 +1,5 @@
+import leon.lang._
+
+object foo {
+ def cmp(c1: Char, c2: Char): Boolean = { c1 < c2 }.holds
+}