Module `Flags.Invgen`

Invgen flags

val prune_trivial : unit -> bool: InvGen will remove trivial invariants, i.e. invariants implied by the transition relation.

val set_max_depth : int option -> unit

Sets the max depth for invariant generation.

Gets the max depth for invariant generation.

val max_depth : unit -> int option: Gets the max depth for invariant generation.

val max_succ : unit -> int: Number of unrollings invariant generation should perform between switching to a different systems.

val lift_candidates : unit -> bool: InvGen will lift candidate terms from subsystems. *

val top_only : unit -> bool: InvGen will generate invariants only for top level. *

val all_out : unit -> bool: Forces invgen to consider a huge number of candidates.

val mine_trans : unit -> bool: InvGen will look for candidate terms in the transition predicate.

val two_state : unit -> bool: InvGen will run in two state mode.

val bool_eq_only : unit -> bool: Forces bool invgen to look for equalities only.

val arith_eq_only : unit -> bool: Forces arith invgen to look for equalities only.

val renice : unit -> int: Renice invariant generation process.