Module Flags.Arrays

Arrays flags

val smt : unit -> bool

Use builtin theory of arrays in SMT solver

val set_smt : bool -> unit
val read_whole : unit -> bool

Whether the values of arrays in models are read whole, as terms, with the theory of arrays (see SMTSolver.get_var_values), rather than element by element. Off by default: the output of Kind 2 prints arrays element by element; kmoxi sets it. Not a command-line option.

val set_read_whole : 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