Soundness bug: fact 4 >= 120

[dvanhorn]

trafficstars

This program is incorrectly proved safe.

(module factorial racket
  (define (fact x)
    (if (zero? x)
        1
        (* x (fact (sub1 x)))))

  (provide
   (contract-out
    [fact (-> (and/c integer? (>=/c 4))
              (and/c integer? (>=/c 120)))])))

[bennn]

Just tried this program. It's rejected. Then I tried changing (>=/c 4) to (>=/c 5) and it's still rejected (new issue?)

[philnguyen]

Rejecting (>=/c 5) would be a precision problem I suppose?