Module `Flags.Arrays`

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