Flags.Arrays
val smt : unit -> bool
Use builtin theory of arrays in SMT solver
val set_smt : bool -> unit
val inline : unit -> bool
Inline arrays with fixed bounds
val recdef : unit -> bool
Define recursive functions for arrays
val var_size : unit -> bool
Allow non constant array sizes