sig
  val deps : State.t list
  val slice_limit : unit -> int
  val disjunctive_invariants : unit -> bool
end