sig
  val check : Node.t -> Node.t list -> int list option
  val pure_smt_check : Node.t -> Node.t list -> int list option
end