sig
  val max : unit -> int
  val check_unroll : unit -> bool
  val print_cex : unit -> bool
  val compress : unit -> bool
  val compress_equal : unit -> bool
  val compress_same_succ : unit -> bool
  val compress_same_pred : unit -> bool
  val lazy_invariants : unit -> bool
end