Improved the date conversion benchmark

testcases/synthesis/ZuneBug.scala

@@ -7,20 +7,24 @@ import leon.lang.synthesis._
 */
 
 object ZuneBug {
+  @inline
   def leapsTill(year: BigInt): BigInt = {
     require(year >= 0)
     val y1 = year - 1
     y1/4 + y1/100 + y1/400
   }
+
+  @inline
   def isLeap(year: BigInt): Boolean = {
     require(year >= 0)
     leapsTill(year+1) > leapsTill(year)
   }
 
-  def yearDay(daysSince1980: BigInt): (BigInt, BigInt) = {
+  // wrong, accidentaly underspecified
+  def yearDayConfused(daysSince1980: BigInt): (BigInt, BigInt) = {
     require(daysSince1980 >= 0)
     ???[(BigInt,BigInt)]
-  } ensuring (res => {    
+  } ensuring (res => {
     val (year, day) = res
     year >= 1980 &&
     0 <= day && day <= 366 &&
@@ -28,4 +32,27 @@ object ZuneBug {
     daysSince1980 == (year - 1980)*365 +
       leapsTill(year) - leapsTill(1980) + day
   })
+
+  // should be correct
+  def yearDay(daysSince1980: BigInt): (BigInt, BigInt) = {
+    require(daysSince1980 >= 0)
+    ???[(BigInt,BigInt)]
+  } ensuring (res => {
+    val (year, day) = res
+    year >= 1980 &&
+    0 <= day && day <= 365 &&
+    (day == 365 ==> isLeap(year)) &&
+    daysSince1980 == (year - 1980)*365 +
+      leapsTill(year) - leapsTill(1980) + day
+  })
+
+  // test run-time constraint solving. smt-cvc4 seems fastest
+  def testYearDay = {
+    (yearDay(364),
+     yearDay(365),
+     yearDay(366),
+     yearDay(366+364),
+     yearDay(366+365))
+  }
+
 }