Module Flags.BmcKind

module BmcKind: sig .. end

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.