Module Flags.Quant

val inst_finite : unit -> bool

Expand quantifiers over finite domains (Booleans, enumerated types) into conjunctions/disjunctions

val set_inst_finite : bool -> unit
val inst_finite_budget : unit -> int

Maximal size, in term nodes, of the term the expansion of a single quantifier may produce