sig
  val horn_instr :
    Clause.state -> string -> Abstract.eva_instr -> Clause.clause list
  val horn_linstr :
    Clause.state -> string -> Abstract.eva_linstr -> Clause.clause list
  val horn_linstrlist :
    Clause.state -> Abstract.eva_linstr list -> Clause.clause list
  val horn_process :
    Clause.state -> Abstract.eva_process -> Clause.clause list
  val horn_lprotocol :
    Clause.state list -> Abstract.eva_lprotocol -> Clause.clause list
  val horn_lsession :
    Clause.state list ->
    Symbols.eva_symbol_list -> Abstract.eva_lsession -> Clause.clause list
  val horn_assume_lstatement : Abstract.eva_lstatement -> Clause.clause list
  val horn_claim_lstatement :
    string list ->
    Clause.state list -> Abstract.eva_lstatement -> Clause.clause list
  val horn_spec :
    Symbols.eva_symbol_list -> Abstract.eva_spec -> Clause.tclause list
end