From 0e89606bef3e50942f2314fcfaf9de959ef320d3 Mon Sep 17 00:00:00 2001
From: Viktor Kuncak <viktor.kuncak@epfl.ch>
Date: Tue, 29 Sep 2015 11:13:10 +0200
Subject: [PATCH] Zune bug test case
---
testcases/synthesis/ZuneBug.scala | 31 +++++++++++++++++++++++++++++++
1 file changed, 31 insertions(+)
create mode 100644 testcases/synthesis/ZuneBug.scala
diff --git a/testcases/synthesis/ZuneBug.scala b/testcases/synthesis/ZuneBug.scala
new file mode 100644
index 000000000..c6ea3522b
--- /dev/null
+++ b/testcases/synthesis/ZuneBug.scala
@@ -0,0 +1,31 @@
+import leon.lang._
+import leon.lang.synthesis._
+
+/* Inspired by the Zune bug that caused looping.
+ This encodes the task of date conversion into
+ integer linear arithmetic and tries to synthesize it.
+*/
+
+object ZuneBug {
+ def leapsTill(year: BigInt): BigInt = {
+ require(year >= 0)
+ val y1 = year - 1
+ y1/4 + y1/100 + y1/400
+ }
+ def isLeap(year: BigInt): Boolean = {
+ require(year >= 0)
+ leapsTill(year+1) > leapsTill(year)
+ }
+
+ def yearDay(daysSince1980: BigInt): (BigInt, BigInt) = {
+ require(daysSince1980 >= 0)
+ ???[(BigInt,BigInt)]
+ } ensuring (res => {
+ val (year, day) = res
+ year >= 1980 &&
+ 0 <= day && day <= 366 &&
+ (day == 366 ==> isLeap(year)) &&
+ daysSince1980 == (year - 1980)*365 +
+ leapsTill(year) - leapsTill(1980) + day
+ })
+}
--
GitLab