Flags.IC3QE
val check_inductive : unit -> bool
Check inductiveness of blocking clauses.
val print_to_file : unit -> string option
File for inductive blocking clauses.
val inductively_generalize : unit -> int
Tighten blocking clauses to an unsatisfiable core.
val block_in_future : unit -> bool
Block counterexample in future frames.
val block_in_future_first : unit -> bool
Block counterexample in future frames first before returning to frame.
val fwd_prop_non_gen : unit -> bool
Also propagate clauses before generalization.
val fwd_prop_ind_gen : unit -> bool
Inductively generalize all clauses after forward propagation.
val fwd_prop_subsume : unit -> bool
Subsumption in forward propagation.
val use_invgen : unit -> bool
Use invariants from invariant generators.
type abstr = [
| `None
| `IA
]
DEPRECATED: Legal abstraction mechanisms for in IC3.
val abstr : unit -> abstr
DEPRECATED: Abstraction mechanism IC3 should use.