sig val join_final_states : Cil_types.kernel_function -> return_lv:Cil_types.lval option -> State_set.t -> Cvalue.Model.t list val pretty_strategies : unit -> unit end