Module Verification.Globals

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

val setup : optimize:bool -> disable_counterexamples:bool -> unit
val 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 ??

val disable_counterexamples : unit -> bool

This should really be passed along through arguments