Module Flags.Arrays

module Arrays: sig .. end

Arrays flags



val smt : unit -> bool
Use builtin theory of arrays in SMT solver
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