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