Module Verification.GlobalsSource

This sub-lib relies on global refs in many places. This should be cleaned up.

Sourceval setup : optimize:bool -> disable_counterexamples:bool -> unit
Sourceval optimize : unit -> bool

Not sure what that means in this context: does it turn on optimisations in the verif backend, or trigger special handling that is dependent on the input code having been optimised ??

Sourceval disable_counterexamples : unit -> bool

This should really be passed along through arguments