Module Flags.BmcKind

BMC / k-induction flags

val max : unit -> int

Maximal number of iterations in BMC.

val check_unroll : unit -> bool

Check that the unrolling of the system alone is satisfiable.

val print_cex : unit -> bool

Print counterexamples to induction.

val compress : unit -> bool

Compress inductive counterexample.

val compress_equal : unit -> bool

Compress inductive counterexample when states are equal modulo inputs.

val compress_same_succ : unit -> bool

Compress inductive counterexample when states have same successors.

val compress_same_pred : unit -> bool

Compress inductive counterexample when states have same predecessors.

val lazy_invariants : unit -> bool

Lazy assertion of invariants.