diff --git a/mytest/Even.scala b/mytest/Even.scala
new file mode 100644
index 0000000000000000000000000000000000000000..f1fdfdce4ca11af66f4225d8971fddaa4a23e287
--- /dev/null
+++ b/mytest/Even.scala
@@ -0,0 +1,14 @@
+import leon.Utils._
+
+object Even {
+
+ //def getEven: Int = {
+ // val e = epsilon((i: Int) => true)
+ // e + e
+ //}) ensuring(isEven(_))
+
+ def double(i: Int): Int = (2*i) ensuring (isEven(_))
+
+ def isEven(i: Int): Boolean = i % 2 == 0
+
+}
diff --git a/src/main/scala/leon/Evaluator.scala b/src/main/scala/leon/Evaluator.scala
index aec3acfa1c0c20c797f0284b09ebb99f25a08a67..bd01412c2606d1e86dec168c8c493b2b64f9de7e 100644
--- a/src/main/scala/leon/Evaluator.scala
+++ b/src/main/scala/leon/Evaluator.scala
@@ -167,6 +167,10 @@ object Evaluator {
case (IntLiteral(i1), IntLiteral(i2)) => IntLiteral(i1 / i2)
case (le,re) => throw TypeErrorEx(TypeError(le, Int32Type))
}
+ case Modulo(l,r) => (rec(ctx,l), rec(ctx,r)) match {
+ case (IntLiteral(i1), IntLiteral(i2)) => IntLiteral(i1 % i2)
+ case (le,re) => throw TypeErrorEx(TypeError(le, Int32Type))
+ }
case LessThan(l,r) => (rec(ctx,l), rec(ctx,r)) match {
case (IntLiteral(i1), IntLiteral(i2)) => BooleanLiteral(i1 < i2)
case (le,re) => throw TypeErrorEx(TypeError(le, Int32Type))
diff --git a/src/main/scala/leon/FairZ3Solver.scala b/src/main/scala/leon/FairZ3Solver.scala
index 390a72ee9e5a41f9872ee1a10b50d56d893e27dd..549f18f97860e46198bd7283ad455c28cbd45d0d 100644
--- a/src/main/scala/leon/FairZ3Solver.scala
+++ b/src/main/scala/leon/FairZ3Solver.scala
@@ -903,6 +903,7 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
case Minus(l, r) => if(USEBV) z3.mkBVSub(rec(l), rec(r)) else z3.mkSub(rec(l), rec(r))
case Times(l, r) => if(USEBV) z3.mkBVMul(rec(l), rec(r)) else z3.mkMul(rec(l), rec(r))
case Division(l, r) => if(USEBV) z3.mkBVSdiv(rec(l), rec(r)) else z3.mkDiv(rec(l), rec(r))
+ case Modulo(l, r) => if(USEBV) sys.error("I don't know what to do here!") else z3.mkMod(rec(l), rec(r))
case UMinus(e) => if(USEBV) z3.mkBVNeg(rec(e)) else z3.mkUnaryMinus(rec(e))
case LessThan(l, r) => if(USEBV) z3.mkBVSlt(rec(l), rec(r)) else z3.mkLT(rec(l), rec(r))
case LessEquals(l, r) => if(USEBV) z3.mkBVSle(rec(l), rec(r)) else z3.mkLE(rec(l), rec(r))
@@ -1112,6 +1113,10 @@ class FairZ3Solver(reporter: Reporter) extends Solver(reporter) with AbstractZ3S
assert(argsSize == 2)
Division(rargs(0), rargs(1))
}
+ case OpMod => {
+ assert(argsSize == 2)
+ Modulo(rargs(0), rargs(1))
+ }
case OpAsArray => {
assert(argsSize == 0)
throw new Exception("encountered OpAsArray")
diff --git a/src/main/scala/leon/plugin/CodeExtraction.scala b/src/main/scala/leon/plugin/CodeExtraction.scala
index 1930fc7a0507f8d12451c127448a53b9089aa233..f1cfeb44c653e81e7fb95c84ae5d242aaafa6236 100644
--- a/src/main/scala/leon/plugin/CodeExtraction.scala
+++ b/src/main/scala/leon/plugin/CodeExtraction.scala
@@ -402,6 +402,7 @@ trait CodeExtraction extends Extractors {
case ExMinus(l, r) => Minus(rec(l), rec(r)).setType(Int32Type)
case ExTimes(l, r) => Times(rec(l), rec(r)).setType(Int32Type)
case ExDiv(l, r) => Division(rec(l), rec(r)).setType(Int32Type)
+ case ExMod(l, r) => Modulo(rec(l), rec(r)).setType(Int32Type)
case ExEquals(l, r) => {
val rl = rec(l)
val rr = rec(r)
diff --git a/src/main/scala/leon/plugin/Extractors.scala b/src/main/scala/leon/plugin/Extractors.scala
index ee684e97a56cd4e639958b67f9957d4bf2e751b0..6985e9b8f0e3262885916886509a2961334ca756 100644
--- a/src/main/scala/leon/plugin/Extractors.scala
+++ b/src/main/scala/leon/plugin/Extractors.scala
@@ -315,6 +315,13 @@ trait Extractors {
}
}
+ object ExMod {
+ def unapply(tree: Apply): Option[(Tree,Tree)] = tree match {
+ case Apply(Select(lhs, n), List(rhs)) if (n == nme.MOD) => Some((lhs,rhs))
+ case _ => None
+ }
+ }
+
object ExLocalCall {
def unapply(tree: Apply): Option[(Symbol,String,List[Tree])] = tree match {
case a @ Apply(Select(This(_), nme), args) => Some((a.symbol, nme.toString, args))
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index c5d2d7158ecd416ea8d25ecfaa84e0ecc882830f..b28cd76c102e61b569e52c22b42a4f7bb2102022 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -135,6 +135,7 @@ object PrettyPrinter {
case Minus(l,r) => ppBinary(sb, l, r, " - ", lvl)
case Times(l,r) => ppBinary(sb, l, r, " * ", lvl)
case Division(l,r) => ppBinary(sb, l, r, " / ", lvl)
+ case Modulo(l,r) => ppBinary(sb, l, r, " % ", lvl)
case LessThan(l,r) => ppBinary(sb, l, r, " < ", lvl)
case GreaterThan(l,r) => ppBinary(sb, l, r, " > ", lvl)
case LessEquals(l,r) => ppBinary(sb, l, r, " \u2264 ", lvl) // \leq
diff --git a/src/main/scala/leon/purescala/Trees.scala b/src/main/scala/leon/purescala/Trees.scala
index 7a289934acf62f1cdd94c4341455722e6edd3290..4d40b99a2bbd8dcde8509918f90b1828171a6c5f 100644
--- a/src/main/scala/leon/purescala/Trees.scala
+++ b/src/main/scala/leon/purescala/Trees.scala
@@ -261,6 +261,9 @@ object Trees {
case class Division(lhs: Expr, rhs: Expr) extends Expr with FixedType {
val fixedType = Int32Type
}
+ case class Modulo(lhs: Expr, rhs: Expr) extends Expr with FixedType {
+ val fixedType = Int32Type
+ }
case class LessThan(lhs: Expr, rhs: Expr) extends Expr with FixedType {
val fixedType = BooleanType
}
@@ -367,6 +370,7 @@ object Trees {
case Minus(t1,t2) => Some((t1,t2,Minus))
case Times(t1,t2) => Some((t1,t2,Times))
case Division(t1,t2) => Some((t1,t2,Division))
+ case Modulo(t1,t2) => Some((t1,t2,Modulo))
case LessThan(t1,t2) => Some((t1,t2,LessThan))
case GreaterThan(t1,t2) => Some((t1,t2,GreaterThan))
case LessEquals(t1,t2) => Some((t1,t2,LessEquals))