#lang rosette (define (leap-year? year) (or (= (remainder year 400) 0) (and (= (remainder year 4) 0) (not (= (remainder year 100) 0))))) (define (zune days) (define year 1980) (while (> days 365) (define old-days days) (if (leap-year? year) (when (> days 366) (set! days (- days 366)) (set! year (add1 year))) (begin (set! days (- days 365)) (set! year (add1 year)))) (assert (< old-days days))) year) (define (find-bug) (define-symbolic days integer?) (verify (zune days))) ;(current-bitwidth 32) (define unroll (make-parameter 1)) (define-syntax-rule (while test body ...) (local [(define (loop bound) (define condition test) (if (and (<= bound 0) (or (not condition) (union? condition) (term? condition))) (assert (not condition)) (when condition body ... (loop (- bound 1)))))] (loop (unroll))))