Module Flags.BmcKind
BMC / k-induction flags
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.