Failing to prove unsamplable

[pavpanchekha]

Here's a super simple benchmark that we aren't able to prove unsamplable:

(define (f)
  (log (+ (exp 1000000000000000000) 0)))
(explain f)

The (+ _ 0) operation is necessary; I think it avoids an optimizing rewrite.

[pavpanchekha]

Simple reason:

• The constants are, of course, double-immovable
• The exp then returns [large, inf !]
• The log thus outputs [something, inf !]

The "large" and "something" really are movable (the large not by a lot, the something also not by too much but by some) so it keeps trying

[pavpanchekha]

Thought about this a bit. It's tough to solve via the samplability stuff directly, but log(exp(a) + exp(b) is the hard pattern here, and we could write a special-case function for that.