sig
  module SMT : Smt.Solver
  val unsafe : Ast.t_system -> Node.t -> unit
  val reached : Hstring.t list -> Types.SAtom.t -> Types.SAtom.t -> unit
  val assume_goal : Node.t -> unit
  val assume_node : Node.t -> Types.ArrayAtom.t -> unit
  val assume_goal_no_check : Node.t -> unit
  val assume_node_no_check : Node.t -> Types.ArrayAtom.t -> unit
  val check_guard : Hstring.t list -> Types.SAtom.t -> Types.SAtom.t -> unit
  val make_literal : Types.Atom.t -> Smt.Formula.t
  val make_formula : Types.ArrayAtom.t -> Smt.Formula.t
  val make_formula_set : Types.SAtom.t -> Smt.Formula.t
  val run : unit -> unit
  val assume_goal_nodes : Node.t -> (Node.t * Types.ArrayAtom.t) list -> unit
end