From edb35b1ca0e819a1c56fe2ded6666d2f4b2ca304 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Tue, 24 Nov 2015 14:20:19 +0100
Subject: [PATCH] We should really use BigInts there
---
.../regression/synthesis/SynthesisSuite.scala | 18 +++++++++---------
1 file changed, 9 insertions(+), 9 deletions(-)
diff --git a/src/test/scala/leon/regression/synthesis/SynthesisSuite.scala b/src/test/scala/leon/regression/synthesis/SynthesisSuite.scala
index f95d7b964..1667d7fb2 100644
--- a/src/test/scala/leon/regression/synthesis/SynthesisSuite.scala
+++ b/src/test/scala/leon/regression/synthesis/SynthesisSuite.scala
@@ -154,9 +154,9 @@ object Injection {
case class Nil() extends List
// proved with unrolling=0
- def size(l: List) : Int = (l match {
- case Nil() => 0
- case Cons(t) => 1 + size(t)
+ def size(l: List) : BigInt = (l match {
+ case Nil() => BigInt(0)
+ case Cons(t) => BigInt(1) + size(t)
}) ensuring(res => res >= 0)
def simple(in: List) = choose{out: List => size(out) == size(in) }
@@ -274,10 +274,10 @@ object ChurchNumerals {
case object Z extends Num
case class S(pred: Num) extends Num
- def value(n:Num) : Int = {
+ def value(n:Num) : BigInt = {
n match {
- case Z => 0
- case S(p) => 1 + value(p)
+ case Z => BigInt(0)
+ case S(p) => BigInt(1) + value(p)
}
} ensuring (_ >= 0)
@@ -309,10 +309,10 @@ object ChurchNumerals {
case object Z extends Num
case class S(pred: Num) extends Num
- def value(n:Num) : Int = {
+ def value(n:Num) : BigInt = {
n match {
- case Z => 0
- case S(p) => 1 + value(p)
+ case Z => BigInt(0)
+ case S(p) => BigInt(1) + value(p)
}
} ensuring (_ >= 0)
--
GitLab