verify-contract not showing counter-examples

[dbp]

With the following example:

(: bad-mult (-> Real Real Real))
(define (bad-mult x y)
  (if (= x 10417)
      0
      (* x y)))
(check-contract bad-mult)

(: bad-mult-prop (-> Real Real True))
(define (bad-mult-prop x y)
  (= (bad-mult x y)
     (* x y)))
(check-contract bad-mult-prop)

(verify-contract bad-mult-prop)

Rosette correctly identifies that this is buggy, but doesn't give us the right counter-example (seems like it is printing the output?)

--------------------
unit tests > Unnamed test
FAILURE
name:       verify-contract
location:   /Users/dbp/code/lsl/lsl-lib/main.rkt:371:19
params:     '(#<procedure:...sl/lsl-lib/main.rkt:371:36>)

verification failure
  expected: True
  counterexample: #f
  blaming: /Users/dbp/teaching/logics24/website/lectures/6.rkt
--------------------
2 success(es) 1 failure(s) 0 error(s) 3 test(s) run